(** * Ltac is an Imperative Metaprogramming Language *)

(** #<div id="history">site/posts/LtacMetaprogramming.v</div># *)

(** Coq is often depicted as an _interactive_ proof assistant, thanks to its
    proof environment. Inside the proof environment, Coq presents the user a
    goal, and said user solves said goal by means of tactics which describes a
    logical reasoning. For instance, to reason by induction, one can use the
    <<induction>> tactic, while a simple case analysis can rely on the
    <<destruct>> or <<case_eq>> tactics, etc.  It is not uncommon for new Coq
    users to be introduced to Ltac, the Coq default tactic language, using this
    proof-centric approach. This is not surprising, since writing proofs remains
    the main use-case for Ltac. In practice though, this discourse remains an
    abstraction which hides away what actually happens under the hood when Coq
    executes a proof scripts.

    To really understand what Ltac is about, we need to recall ourselves that
    Coq kernel is mostly a typechecker. A theorem statement is expressed as a
    “type” (which lives in a dedicated sort called [Prop]), and a proof of this
    theorem is a term of this type, just like the term [S (S O)] (#<span
    class="im">#2#</span>#) is of type [nat].  Proving a theorem in Coq requires
    to construct a term of the type encoding said theorem, and Ltac allows for
    incrementally constructing this term, one step at a time.

    Ltac generates terms, therefore it is a metaprogramming language. It does it
    incrementally, by using primitives to modifying an implicit state, therefore
    it is an imperative language. Henceforth, it is an imperative
    metaprogramming language.

    To summarize, a goal presented by Coq inside the environment proof is a hole
    within the term being constructed. It is presented to users as:

      - A list of “hypotheses,” which are nothing more than the variables
        in the scope of the hole
      - A type, which is the type of the term to construct to fill the hole

    We illustrate what happens under the hood of Coq executes a simple proof
    script. One can use the <<Show Proof>> vernacular command to exhibit
    this.

    We illustrate how Ltac works with the following example. *)

Theorem add_n_O : forall (n : nat), n + O = n.

Proof.

(** The <<Proof>> vernacular command starts the proof environment. Since no
    tactic has been used, the term we are trying to construct consists solely in
    a hole, while Coq presents us a goal with no hypothesis, and with the exact
    type of our theorem, that is [forall (n : nat), n + O = n].

    A typical Coq course will explain students the <<intro>> tactic allows for
    turning the premise of an implication into an hypothesis within the context.

    #<div class="dmath">#C \vdash P \rightarrow Q#</div>#

    becomes

    #<div class="dmath">#C,\ P \vdash Q#</div>#

    This is a fundamental rule of deductive reasoning, and <<intro>> encodes it.
    It achieves this by refining the current hole into an anymous function.
    When we use *)

  intro n.

(** it refines the term

<<
  ?Goal1
>>

    into

<<
  fun (n : nat) => ?Goal2
>>

    The next step of this proof is to reason about induction on [n]. For [nat],
    it means that to be able to prove

    #<div class="dmath">#\forall n, \mathrm{P}\ n#</div>#

    we need to prove that

      -  #<div class="imath">#\mathrm{P}\ 0#</div>#
      -  #<div class="imath">#\forall n, \mathrm{P}\ n \rightarrow \mathrm{P}\ (S n)#</div>#

     The <<induction>> tactic effectively turns our goal into two subgoals. But
     why is that? Because, under the hood, Ltac is refining the current goal
     using the [nat_ind] function automatically generated by Coq when [nat] was
     defined. The type of [nat_ind] is

<<
  forall (P : nat -> Prop),
    P 0
    -> (forall n : nat, P n -> P (S n))
    -> forall n : nat, P n
>>
    Interestingly enough, [nat_ind] is not an axiom. It is a regular Coq function, whose definition is

<<
  fun (P : nat -> Prop) (f : P 0)
      (f0 : forall n : nat, P n -> P (S n)) =>
  fix F (n : nat) : P n :=
    match n as n0 return (P n0) with
    | 0 => f
    | S n0 => f0 n0 (F n0)
    end
>>

    So, after executing *)

  induction n.

(** The hidden term we are constructing becomes

<<
  (fun n : nat =>
     nat_ind
       (fun n0 : nat => n0 + 0 = n0)
       ?Goal3
       (fun (n0 : nat) (IHn : n0 + 0 = n0) => ?Goal4)
       n)
>>

    And Coq presents us two goals.

    First, we need to prove #<span class="dmath">#\mathrm{P}\ 0#</span>#, i.e.,
    #<span class="dmath">#0 + 0 = 0#</span>#. Similarly to Coq presenting a goal
    when what we are actually doing is constructing a term, the use of #<span
    class="dmath">#+#</span># and #<span class="dmath">#+#</span># (i.e., Coq
    notations mechanism) hide much here. We can ask Coq to be more explicit by
    using the vernacular command <<Set Printing All>> to learn that when Coq
    presents us a goal of the form [0 + 0 = 0], it is actually looking for a
    term of type [@eq nat (Nat.add O O) O].

    [Nat.add] is a regular Coq (recursive) function.

<<
  fix add (n m : nat) {struct n} : nat :=
    match n with
    | 0 => m
    | S p => S (add p m)
    end
>>

    Similarly, [eq] is _not_ an axiom. It is a regular inductive type, defined
    as follows.

<<
Inductive eq (A : Type) (x : A) : A -> Prop :=
| eq_refl : eq A x x
>>

    Coming back to our current goal, proving [@eq nat (Nat.add 0 0) 0] (i.e., [0
    + 0 = 0]) requires to construct a term of a type whose only constructor is
    [eq_refl]. [eq_refl] accepts one argument, and encodes the proof that said
    argument is equal to itself. In practice, Coq typechecker will accept the
    term [@eq_refl _ x] when it expects a term of type [@eq _ x y] _if_ it can
    reduce [x] and [y] to the same term.

    Is it the case for [0 + 0 = 0]? It is, since by definition of [Nat.add], [0
    + x] is reduced to [x]. We can use the <<reflexivity>> tactic to tell Coq to
    fill the current hole with [eq_refl]. *)

  + reflexivity.

 (** Suspicious readers may rely on <<Show Proof>> to verify this assertion
     assert:
<<
  (fun n : nat =>
     nat_ind
       (fun n0 : nat => n0 + 0 = n0)
       eq_refl
       (fun (n0 : nat) (IHn : n0 + 0 = n0) => ?Goal4)
       n)
>>

    <<?Goal3>> has indeed be replaced by [eq_refl].

    One goal remains, as we need to prove that if [n + 0 = n], then [S n + 0 = S
    n]. Coq can reduce [S n + 0] to [S (n + 0)] by definition of [Nat.add], but
    it cannot reduce [S n] more than it already is. We can request it to do so
    using tactics such as [cbn]. *)

  + cbn.

(** We cannot just use <<reflexivity>> here (i.e., fill the hole with
    [eq_refl]), since [S (n + 0)] and [S n] cannot be reduced to the same term.
    However, at this point of the proof, we have the [IHn] hypothesis (i.e., the
    [IHn] argument of the anonymous function whose body we are trying to
    construct). The <<rewrite>> tactic allows for substituting in a type an
    occurence of [x] by [y] as long as we have a proof of [x = y]. *)

    rewrite IHn.

 (** Similarly to <<induction>> using a dedicated function , <<rewrite>> refines
     the current hole with the [eq_ind_r] function (not an axiom!). Replacing [n
     + 0] with [n] transforms the goal into [S n = S n]. Here, we can use
     <<reflexivity>> (i.e., [eq_refl]) to conclude. *)

    reflexivity.

(** After this last tactic, the work is done. There is no more goal to fill
    inside the proof term that we have carefully constructed.

<<
  (fun n : nat =>
     nat_ind
       (fun n0 : nat => n0 + 0 = n0)
       eq_refl
       (fun (n0 : nat) (IHn : n0 + 0 = n0) =>
          eq_ind_r (fun n1 : nat => S n1 = S n0) eq_refl IHn)
       n)
>>

    We can finally use [Qed] or [Defined] to tell Coq to typecheck this
    term. That is, Coq does not trust Ltac, but rather typecheck the term to
    verify it is correct. This way, in case Ltac has a bug which makes it
    construct ill-formed type, at the very least Coq can reject it. *)

Qed.

(** In conclusion, tactics are used to incrementally refine hole inside a term
    until the latter is complete. They do it in a very specific manner, to
    encode certain reasoning rule.

    On the other hand, the <<refine>> tactic provides a generic, low-level way
    to do the same thing. Knowing how a given tactic works allows for mimicking
    its behavior using the <<refine>> tactic.

    If we take the previous theorem as an example, we can prove it using this
    alternative proof script. *)

Theorem add_n_O' : forall (n : nat), n + O = n.

Proof.
  refine (fun n => _).
  refine (nat_ind (fun n => n + 0 = n) _ _ n).
  + refine eq_refl.
  + refine (fun m IHm => _).
    refine (eq_ind_r (fun n => S n = S m) _ IHm).
    refine eq_refl.
Qed.

(** ** Conclusion *)

(** This concludes our introduction to Ltac as an imperative metaprogramming
    language. In the #<a href="LtacPatternMatching.html">#next part of this series#</a>#, we
    present Ltac powerful pattern matching capabilities. *)