1 files changed, 251 insertions, 0 deletions
diff --git a/site/posts/LtacMetaprogramming.v b/site/posts/LtacMetaprogramming.v
new file mode 100644
index 0000000..2a4fe50
--- /dev/null
+++ b/site/posts/LtacMetaprogramming.v
@@ -0,0 +1,251 @@
+(** * 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. *)