(*|
:Authors: Yannick Forster, Théo Winterhalter
:Files:
  - `Source <../files/lesson4_part4.v>`_
  - `Exercise sheet <../files/tp4.v>`_
  - `MetaRocq prelude <../files/MetaRocqPrelude.v>`_

.. role:: coq(code)
   :language: coq
   :class: highlight

.. default-role:: coq
|*)

(*| .. coq:: none |*)

Axiom REPLACE_ME : forall {A : Type}, A.

From Stdlib Require Import Lia List ZArith.
Import ListNotations.

Create HintDb indb.
From Stdlib Require Import Classical.

#[export] Hint Extern 3 (@eq nat _ _) => lia : indb.

#[export] Hint Extern 3 (@eq Z _ _) => lia : indb.

From Stdlib Require Import Setoid.

Set Default Goal Selector "!".

Ltac split_or_apply :=
  match goal with
  | |- ?A /\ ?B => split
  | h : ?B -> ?A |- ?A => apply h (* Here we match on any hypothesis *)
  (* The name [h] is of our choosing, it's going to apply to hypothesis
     [H : nat -> bool] for instance. *)
  end.

Ltac my_assumption :=
  match goal with
  | H : ?A |- ?A => apply H
  end.

Ltac splits :=
  lazymatch goal with
  | |- ?A * ?B => split ; splits
  | _ => idtac
  end.

Ltac handle_hyp h :=
  lazymatch type of h with
  | (?A * ?B)%type => destruct h
  | nat => induction h
  | _ => idtac
  end.

Ltac fwd h :=
  match type of h with
  | ?P -> _ =>
    let h' := fresh in
    assert (h' : P) ; [| specialize (h h') ; clear h' ]
  end.

Ltac forward_gen h tac :=
  match type of h with
  | ?P -> _ =>
    let h' := fresh in
    assert (h' : P) ; [ tac | specialize (h h') ; clear h' ]
  end.
Tactic Notation "forward" constr(H) := forward_gen H ltac:(idtac).
Tactic Notation "forward" constr(H) "by" tactic(tac) := forward_gen H tac.

Ltac my_tauto :=
  lazymatch goal with
  | h : ?P |- ?P => exact h

  | |- True => constructor
  | |- _ /\ _ => split ; my_tauto
  | |- _ -> _ => intro ; my_tauto

  | h : False |- _ => destruct h
  | h : _ /\ _ |- _ => destruct h ; my_tauto
  | h : _ \/ _ |- _ => destruct h ; my_tauto

  | h1 : ?P -> ?Q, h2 : ?P |- _ => specialize (h1 h2) ; my_tauto

  | |- _ \/ _ => (left ; my_tauto) || (right ; my_tauto)
  end.

Require Import MetaRocqPrelude.

(*| |*)

(*|
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Manipulating commands with MetaRocq
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Finally, MetaRocq also contains a representation of Rocq vernacular commands
like ``Definition``, ``Print``, ``Locate``, which can be useful to write more
complex meta-programs. |*)

MetaRocq Run (
  t <- tmLemma "tm_foo" nat ;;
  tmDefinition "tm_bar" (t + t + 2)
).
Next Obligation. (*| This is how we prove a ``tmLemma`` |*)
  exact 12.
Defined.

(*| After we prove ``tm_foo``, the program continues and defines ``tm_bar``. |*)
Print tm_bar. (*| ``tm_foo + tm_foo + 2`` |*)

MetaRocq Run (
  t <- tmLemma "baz" nat ;;
  st <- tmEval all t ;;
  tmDefinition "simpl_baz" st
).
Next Obligation.
  exact (10 + 2).
Defined.

Print simpl_baz.

(*|
.. raw:: html

   <details class="exercise"><summary>Exercise: Deriving (hard)</summary>

..
|*)

(*|
We promised MetaRocq could be used to derive automatically certain things.
Let's see how this can be done by automatically deriving update functions for
a record.

We assume that there is no dependency between the fields, otherwise it's
unclear what an update function should do.

This exercise is hard, so it makes sense to make some assumptions first
such as the absence of parameters (like in `triple` below) or of local
definitions (like in `trap` below).
Don't hesitate to ask questions if you are stuck.

We'll start with a few record definitions, together with one example of an
update function, don't hesitate to write your own and quote them to understand
what you need to write.
|*)

Record point3D := {
  px : nat ;
  py : nat ;
  pz : nat
}.

Record Zalt := {
  num : nat ;
  positive : bool
}.

Record triple A B C := {
  p1 : A ;
  p2 : B ;
  p3 : C
}.

Record trap := {
  v1 : nat ;
  v2 := 10 ^ v1 ;
  v3 : nat
}.

(*| We write an update for `num` by hand. |*)
Definition upd_num (f : nat -> nat) (x : Zalt) :=
  match x with
  | Build_Zalt num positive => Build_Zalt (f num) positive
  end.

(*|
.. note::

   There are other ways to write it, but this one might be the easiest to
   automate.
|*)

(*| Now we can look at how it is quoted.

We use `$Quote` rather than `$quote` to unfold the constant `upd_num` when
quoting it. Otherwise we would get some `tConst` which is not as informative.
|*)

Definition q_upd_num := $Quote upd_num.
Print q_upd_num.

(*| Below is a meta-program that gives you the definition of an inductive.

Hint: It may be useful to you later, perhaps no as-is, but with some
modification to also get the argument of `tInd`.
|*)
Definition get_inductive {A} (ind : A) :=
  t <- tmQuote ind ;;
  match t with
  | tInd ind _ =>
    let kn := ind.(inductive_mind) in
    tmQuoteInductive kn
  | _ => tmFail "Not an inductive type"
  end.

(*| We use it like this to define `Zalt_def` to inspect at our leisure. |*)
MetaRocq Run (
  mib <- get_inductive Zalt ;;
  tmDefinition "Zalt_def" mib
).

(*| This now contains the definition of `Zalt`.

You may compare the information you see in here with what appeared in
`q_upd_num`. It might be useful to copy paste them to better compare.
|*)
Print Zalt_def.

(*| To help you build the `derive_updates` meta-program, we'll give you some
useful tools.

Also check out the following useful constructs:

- `tmMkDefinition` takes a `string` and a `term` and produces a definition
  using that name (if fresh, otherwise it fails) and unquoting the given term.
- `tmFreshName` takes a `string` and will return a new string that is fresh in
  the current environment, based on the given one (typically by adding a
  number at the end).

If you plan to handle parameters:

- `it_mkLambda_or_LetIn` takes `c : context` and `t : term` and produces
  a new λ-abstraction with body `t` and quantifying over `c`.
  Basically it does the right thing by inserting as many `tLam` as necessary.
- `subst l 0 t` will substitute the variables of `t` using the terms provided
  in `l`. For this exercise, you can provide garbage (just some random
  `tRel k` will suffice), what matters is the number of terms you provide.
  Providing `3` will reduce `tRel 5` to `tRel 2`.
|*)

(*| Handy concatenation notation. |*)
Notation "a # b" := (String.append a b).

(*| To debug we recommend you use the following in place of `tmMkDefinition` |*)
Definition tmDebugDefinition na (t : term) :=
  t <- tmEval all t ;;
  tmDefinition na t.

(*| `mkr 3 2` will produce `[ tRel 4 ; tRel 3 ; tRel 2 ]` |*)
Fixpoint mkr i off :=
  match i with
  | 0 => []
  | S i => tRel (off + i) :: mkr i off
  end.

(*| Extract the name from `aname` or use `d` as default. |*)
Definition get_name (a : aname) d :=
  match a.(binder_name) with
  | nNamed na => na
  | nAnon => d
  end.

Definition derive_updates {A} (ind : A) : TemplateMonad unit :=
  REPLACE_ME.

(*|
.. tip::

   Use the same as `derive_updates` with `tmDebugDefinition` instead of
   `tmMkDefinition`. It will help debug because I don't expect the error messages
   to be very useful.
|*)
Definition debug_derive_updates {A} (ind : A) : TemplateMonad unit :=
  REPLACE_ME.

(*| Below, one of them should always fail. |*)
Fail MetaRocq Run (derive_updates nat).

(*| Test that it works. If you manage to execute those lines, it's very likely that it does, but
better safe than sorry.
|*)

(*|
.. raw:: html

   </details>

..
|*)

(*| 
^^^^^^^^^^^^^^^^^^^^
Proof by reflection
^^^^^^^^^^^^^^^^^^^^

Proof by reflection is a powerful technique to solve difficult proof goals efficiently if they can be transformed into a computational problem.

Instead of constructing a complex proof term for a difficult goal we
1. Define a syntactic representation of the shape of goals we want to solve and an interpretation function from shape to actual goals -- a reflection procedure.
2. Implement a decision procedure for goals that have this syntactic shape
3. Prove the decision procedure correct
4. We implement a "reification" procedure translating a goal into its shape, using meta-programming.
4. When trying to prove a difficult goal, we employ the decision procedure on the shape of the goal.

The process of going from a goal to its shape is called reification.

In this example, we will care about propositional logic of the following shape:

|*)

Inductive form: Type :=
| var (x: nat)
| top
| bot
| imp (s t: form)
| and (s t : form)
| or (s t : form).

(*|

We write a reflection procedure from form to Propositions:

|*)

Fixpoint reflect (env : nat -> Prop) (s : form) :=
  match s with
  | var x => env x
  | top => True
  | bot => False
  | imp s t => reflect env s -> reflect env t
  | and s t => (reflect env s) /\ (reflect env t)
  | or s t => (reflect env s) \/ (reflect env t)
  end.

(*|

We now write a decision procedure employing boolean logic:

|*)

Fixpoint decider (env : nat -> bool) (s : form) :=
  match s with
  | var x => env x
  | top => true
  | bot => false
  | imp s t => if decider env s then decider env t else true
  | and s t => andb (decider env s) (decider env t)
  | or s t => orb (decider env s) (decider env t)
  end.

(*|

We prove the decision procedure correct:

|*)

Lemma decider_iff envb env s :
  (forall n, env n <-> envb n = true) ->
  reflect env s <-> decider envb s = true.
Proof.
  intros Henv.
  induction s; cbn.
  all: try now firstorder congruence.
  all: destruct (decider envb s1), (decider envb s2); firstorder.
Qed.

(*|

We now turn to implementing a reification procedure.
Crucially, the reification procedure must map
parts of the goal that do not fall into the shapes defined as form as var.
To ensure that the same goals are mapped to the same variable, we implement the following procedure adding
an element to a list if it is not in there, and otherwise returning the index of the element in the list:

|*)

Fixpoint index {A} (d : A -> A -> bool) a l :=
  match l with
  | [] => None
  | x :: l =>
      if d x a then Some 0 else
      match index d a l with
      | Some n => Some (S n)
      | None => None
      end
  end.

Definition list_add {A} (d : A -> A -> bool) a l :=
  match index d a l with
  | Some n => (n, l)
  | None => (length l, l ++ [a])
  end.

(*|

We now write the recursive reification procedure using MetaRocq:

|*)

From MetaRocq.Utils Require Import ReflectEq.

Fixpoint reify_rec f l : (form * list term) :=
  let catchall := fun _ : unit =>
       let '(n, s_env) := list_add term_eqb f l in
       (var n, s_env) in
  match f with
  | tInd {| inductive_mind := cst;
            inductive_ind := 0 |} [] =>
      if cst == (MPfile ["Logic"; "Init"; "Corelib"], "False")
      then
        (bot, [])
      else if cst == (MPfile ["Logic"; "Init"; "Corelib"], "True") then
        (top, [])
      else catchall tt
  | tApp (tConst cst []) [s] =>
      if cst == (MPfile ["Logic"; "Init"; "Corelib"], "not")
      then
        let (s_form, s_env) := reify_rec s l in
        (imp s_form bot, s_env)
      else
        catchall tt
  | tApp (tInd {| inductive_mind := cst;
                  inductive_ind := 0 |} []) [s; t]
  | tApp (tConst cst []) [s; t] =>
      if cst == (MPfile ["Logic"; "Init"; "Corelib"], "and")
      then
        let (s_form, s_env) := reify_rec s l in
        let (t_form, t_env) := reify_rec t s_env in
        (and s_form t_form, t_env)
      else if cst == (MPfile ["Logic"; "Init"; "Corelib"], "or")
      then
        let (s_form, s_env) := reify_rec s l in
        let (t_form, t_env) := reify_rec t s_env in
        (or s_form t_form, t_env)
      else if cst == (MPfile ["Logic"; "Init"; "Corelib"], "iff")
      then
        let (s_form, s_env) := reify_rec s l in
        let (t_form, t_env) := reify_rec t s_env in
        (and (imp s_form t_form) (imp t_form s_form), t_env)
      else
        catchall tt
  | tProd na s t =>
      let (s_form, s_env) := reify_rec s l in
      let (t_form, t_env) := reify_rec t s_env in
      (imp s_form t_form, t_env)
  | _ => catchall tt
  end.

(*|

We write a reification tactic which takes a proposition as input,

1. quotes it into MetaRocq syntax,
2. runs the recursive reification function, and
3. unquotes all variable denotations in the variable list again into Propositions

|*)

Ltac reify f :=
  constr:(ltac:(
                  run_template_program (mlet t <- tmQuote f ;;
                                        let (x, lx) := reify_rec t (@nil term) in
                                        mlet lx' <- monad_map (tmUnquoteTyped Prop) lx ;;
                                        ret (x, lx'))
                    (fun x => exact x))).

(*|

We now assume a strong form of classical logic to prove reification correct:

|*)

Axiom dec : forall P, {P} + {~P}.

Lemma decider_reflect env s :
  decider (fun n => if dec (env n) then true else false) s ->
  reflect env s.
Proof.
  intros H.
  eapply decider_iff.
  2: eassumption.
  cbn. intros n. destruct (dec (env n)); firstorder congruence.
Qed.

(*|

Lastly, we write a tactic which reifies a goal,
applies the correctness theorem of the decider;
and then repeatedly destruct the dec axiom to solve the goal:

|*)

Ltac cauto_r :=
  lazymatch goal with
  | |- ?G =>
      lazymatch reify G with
      | (?fx, ?lx) =>
          change (reflect (fun n => List.nth n lx False) fx);
          apply decider_reflect
      end
  end.

Ltac intro_Prop :=
  match goal with
  | |- forall P : Prop, _ => intro
  end.

Ltac cauto :=
  repeat intro_Prop;
  cauto_r;
  cbn; repeat destruct dec; try reflexivity.

Goal forall A B : Prop, A -> B -> A.
Proof.
  cauto.
Qed.

Goal forall A B C : Prop, ~ A \/ ~ B \/ (C /\ True) <-> ~ (A /\ B /\ ~ C).
Proof.
  cauto.
Qed.

(*|

Note that the tactic nicely generates counterexamples if it does not work:

|*)

Goal forall A B : Prop, A -> B.
Proof.
  cauto.
Abort.