Heavy reworking of the Ltac series

6 files changed, 489 insertions, 508 deletions

diff --git a/site/index.org b/site/index.org
index bc400af..f530c43 100644
--- a/site/index.org
+++ b/site/index.org
@@ -2,8 +2,6 @@
 
 #+BEGIN_EXPORT html
 <h1>Technical Articles</h1>
-
-<article class="index">
 #+END_EXPORT
 
 Over the past years, I have tried to capitalize on my findings. What I have
@@ -22,19 +20,23 @@ language with nice dependent types together with an environment for writing
 machine-checked proofs.
 
 - A Series on Strongly-Specified Funcions in Coq ::
-  Coq ~Prop~ sort allows for defining properties function arguments have to
-  satisfy, such that using such a function requires providing a proof the
-  property is satisfied.
+  Using dependent types and the ~Prop~ sort, it becomes possible to specify
+  functions whose arguments and results are constrained by properties.
+  Using such a “strongly-specified” function requires to provide a proof that
+  the supplied arguments satisfy the expected properties, and allows for soundly
+  assuming the results are correct too. However, implementing dependently-typed
+  functions can be challenging. In this series, we explore several approaches
+  available to Coq developers.
 
   1. [[./posts/StronglySpecifiedFunctions.html][Using the ~refine~ Tactics]]
   2. [[./posts/StronglySpecifiedFunctionsProgram.html][Using the ~Program~ Framework]]
 
-- A Series on Ltac ::
-  Ltac is the “tactic language” of Coq. It allows for writing proof scripts
-  which construct proof terms later checked by Coq.
-
-  1. [[./posts/Ltac101.html][Ltac 101]]
-  2. [[./posts/MixingLtacAndGallina.html][Mixing Ltac and Gallina for Fun and Profit]]
+- [[./posts/Ltac.org][A Series on Ltac]] ::
+  Ltac is the “tactic language” of Coq. It is commonly advertised as the common
+  approach to write proofs, which tends to bias how it is introduced to new Coq
+  users (/e.g./, in Master courses). In this series, we present Ltac as the
+  metaprogramming tool it is, since fundamentally it is an imperative language
+  which allows for constructing Coq terms interactively and incrementally.
 
 - [[./posts/RewritingInCoq.html][Rewriting in Coq]] ::
   The ~rewrite~ tactics are really useful, since they are not limited to the Coq
@@ -65,15 +67,9 @@ type system.
   Monads are hard to get right, monad transformers are harder. Yet, they remain
   a very powerful abstraction.
 
-* About Common Lisp
-
-Common Lisp is a venerable programming languages like no other I know.
+* Miscellaneous
 
 - [[./posts/DiscoveringCommonLisp.html][Discovering Common Lisp with ~trivial-gamekit~]] ::
-  From the creation of a Lisp package up to the creation of a standalone
-  executable.
-
-
-#+BEGIN_EXPORT html
-</article>
-#+END_Export
+  Common Lisp is a venerable programming languages like no other I know.  From
+  the creation of a Lisp package up to the creation of a standalone executable,
+  we explore the shore of this strange beast.
diff --git a/site/posts/Ltac.org b/site/posts/Ltac.org
new file mode 100644
index 0000000..caba76c
--- /dev/null
+++ b/site/posts/Ltac.org
@@ -0,0 +1,30 @@
+#+BEGIN_EXPORT html
+<h1>A Series on Ltac</h1>
+#+END_EXPORT
+
+Ltac is the “tactic language” of Coq. It is commonly advertised as the common
+approach to write proofs, which tends to bias how it is introduced to new Coq
+users (/e.g./, in Master courses). In this series, we present Ltac as the
+metaprogramming tool it is, since fundamentally it is an imperative language
+which allows for constructing Coq terms interactively and incrementally.
+
+- [[./LtacMetaprogramming.html][Ltac is an Imperative Metaprogramming Language]] ::
+  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.
+
+- [[./LtacPatternMatching.html][Pattern Matching on Types and Contexts]] ::
+  Ltac allows for pattern matching on types and contexts. In this article, we
+  give a short introduction on this feature of key importance. Ltac programs
+  (“proof scripts”) generate terms, and the shape of said terms can be very
+  different regarding the initial context. For instance, ~induction x~ will
+  refine the current goal using an inductive principle dedicated to the type of
+  ~x~.
+
+- [[./MixingLtacAndGallina.html][Mixing Ltac and Gallina Together for Fun and Profit]] ::
+  One of the most misleading introduction to Coq is to say that “Gallina is for
+  programs, while tactics are for proofs.” Gallina is the preferred way to
+  construct programs, and tactics are the preferred way to construct proofs.
+  The key word here is “preferred.” Coq actually allows for /mixing/
+  Ltac and Gallina together.
diff --git a/site/posts/Ltac101.v b/site/posts/Ltac101.v
deleted file mode 100644
index 2b71a8f..0000000
--- a/site/posts/Ltac101.v
+++ /dev/null
@@ -1,308 +0,0 @@
-(** * Ltac 101 *)
-
-(** We give an overview of my findings about the Ltac language, more
-    precisely how it can be used to automate the construction of proof terms. If
-    you never wrote a tactic in Coq and are curious about the subject, it might
-    be a good starting point.
-
-    This write-up (originally published on #<span
-    id="original-created-at">October 16, 2017</span>#) is the first part of a
-    series on Ltac. The next part explains #<a
-    href="/posts/MixingLtacAndGallina.html">how to mix Gallina and Ltac</a>#. *)
-
-(** #<div id="generate-toc"></div>#
-
-    #<div id="history">site/posts/Ltac101.v</div># *)
-
-(** ** Tactics Aliases *)
-
-(** The first thing you will probably want to do with Ltac is define aliases for
-    recurring (sequences of) tactics.
-
-    To take a concrete example, the very first tactic I wrote was for a project
-    called SpecCert where _many_ lemmas are basically about proving a given
-    property [P] is a state invariant of a given transition system. As a
-    consequence, they have the very same “shape”:
-    #<span class="imath">#\forall s\ l\ s', P(s) \wedge s \overset{l\ }{\mapsto}
-    s' \rightarrow P(s')#</span>#, that is, if [P] is satisfied for [s], and there
-    exists a transition from [s] to [s'], then [P] is satisfied for [s'].
-
-    Both states and labels are encoded in record, and the first thing I was
-    doing at the time with them was [destruct]ing them. Similarly, the predicate
-    [P] is an aggregation of sub-predicates (using #<span
-    class="imath">#\wedge#</span>#). In practice, most of my proofs started with
-    something like [intros [x1 [y1 z1]] [a b] [x2 [y2 z2]] [HP1 [HP2 [HP3 HP4]]]
-    [R1|R2]]. Nothing copy/past cannot solve at first, of course, but as soon as
-    the definitions change, you have to change every single [intros] and it is
-    quite boring, to say the least.
-
-    The solution is simple: define a new tactic to use in place of your “raw”
-    [intros]: *)
-
-Ltac my_intros_1 :=
-  intros [x1 [y1 z1]] [a b] [x2 [y2 z2]] [HP1 [HP2 [HP3 HP4]]] [R1|R2].
-
-(** As a more concrete example, we consider the following goal: *)
-
-Goal (forall (P Q : Prop), P /\ Q -> P).
-
-(** A typical way to move the premises of this statement from the goal to the
-    context is by means of [intro], and it is possible to destruct the term [p
-    /\ q] with a pattern. *)
-
-  intros P Q [p q].
-
-(** which leaves the following goal to prove:
-
-<<
-  P, Q : Prop
-  p : P
-  q : Q
-  ============================
-  P
->>
-
-    Rather than having to remember the exact syntax of the intro-pattern, Coq
-    users can write a specialized tactic. *)
-
-(* begin hide *)
-Undo.
-(* end hide *)
-
-Ltac and_intro := intros [p q].
-
-(** [and_intro] is just another tactic, and therefore is straightforward to
-    use. *)
-
-  intros P Q.
-  and_intro.
-
-(** This leaves the goal to prove in the exact same state as in our previous
-    attempt, which is great because it was exactly the point. However, there is
-    an issue with the [and_intro] command. To demonstrate it, let us consider a
-    slightly different goal.  *)
-
-(* begin hide *)
-Abort.
-(* end hide *)
-
-Goal (forall (P Q : Prop), P /\ Q -> Q /\ P -> P).
-
-(** The statement is not very interesting from a logical standpoint, but bear
-    with me while I try to prove it. *)
-
-Proof.
-  intros P Q.
-  and_intro.
-
-(** Again, the goal is as we expect it to be:
-
-<<
-  P, Q : Prop
-  p : P
-  q : Q
-  ============================
-  P /\ Q -> P
->>
-
-    We still have a premise of the form [P /\ Q] in the current goal… but at the
-    same time, we also have hypotheses named [p] and [q] (the named used by
-    <<and_intro>>) in the context. If we try to use <<and_intro>> again, Coq
-    legitimely complains.
-
-<<
-p is already used.
->> *)
-(* begin hide *)
-Reset and_intro.
-(* end hide *)
-
-(** To tackle this apparent issue, Ltac provides a mechanic to fetch “fresh”
-    (unused in the current context) names. *)
-
-Ltac and_intro :=
-  let p := fresh "p" in
-  let q := fresh "q" in
-  intros [p q].
-
-(** This time, using [and_intro] several time works fine. In our previous
-    example, the resulting goal is the following: *)
-
-(**
-<<
-  P, Q : Prop
-  p : P
-  q, p0 : Q
-  q0 : P
-  ============================
-  P
->> *)
-
-(** Finally, tactics can take a set of arguments. They can be of various forms,
-    but the most common to my experience is hypothesis name. For instance, we
-    can write a tactic call <<destruct_and>> to… well, destruct an hypothesis of
-    type [P /\ Q]. *)
-
-Ltac destruct_and H :=
-  let p := fresh "p" in
-  let q := fresh "q" in
-  destruct H as [Hl Hr].
-
-(** With that, you can already write some very useful tactic aliases. It can
-    save you quite some time when refactoring your definitions, but Ltac is
-    capable of much more. *)
-
-(** ** Printing Messages *)
-
-(** One thing that can be useful while writing/debugging a tactic is the ability
-    to print a message. You have to strategies available in Ltac as far as I
-    know: [idtac] and [fail], where [idtac] does not stop the proof script on an
-    error whereas [fail] does. *)
-
-(** ** It Is Just Pattern Matching, Really *)
-
-(** If you need to remember one thing from this blogpost, it is probably this:
-    Ltac pattern matching features are amazing. That is, you will try to find in
-    your goal and hypotheses relevant terms and sub terms you can work with.
-
-    You can pattern match a value as you would do in Gallina, but in Ltac, the
-    pattern match is also capable of more. The first case scenario is when you
-    have a hypothesis name and you want to check its type: *)
-
-Ltac and_or_destruct H :=
-  let Hl := fresh "Hl" in
-  let Hr := fresh "Hr" in
-  match type of H with
-  | _ /\ _
-    => destruct H as [Hl Hr]
-  | _ \/ _
-    => destruct H as [Hl|Hr]
-  end.
-
-(** For the following incomplete proof script: *)
-
-Goal (forall P Q, P /\ Q -> Q \/ P -> True).
-  intros P Q H1 H2.
-  and_or_destruct H1.
-  and_or_destruct H2.
-
-(** We get two sub goals:
-
-<<
-2 subgoals, subgoal 1 (ID 20)
-
-  P, Q : Prop
-  Hl : P
-  Hr, Hl0 : Q
-  ============================
-  True
-
-subgoal 2 (ID 21) is:
- True
->>
- *)
-
-Abort.
-
-(** We are not limited to constructors with the [type of] keyword, We can
-    also pattern match using our own definitions. For instance: *)
-
-Parameter (my_predicate: nat -> Prop).
-
-Ltac and_my_predicate_simpl H :=
-  match type of H with
-  | my_predicate _ /\ _
-    => destruct H as [Hmy_pred _]
-  | _ /\ my_predicate _
-    => destruct H as [_ Hmy_pred]
-  end.
-
-(** Last but not least, it is possible to introspect the current goal of your
-    proof development: *)
-
-Ltac rewrite_something :=
-  match goal with
-  | H:  ?x = _ |- context[?x]
-    => rewrite H
-  end.
-
-(** So once again, as an example, the following proof script: *)
-
-Goal (forall (x :nat) (equ : x = 2), x + 2 = 4).
-  intros x equ.
-  rewrite_something.
-
-(** This leaves the following goal to prove:
-
-<<
-1 subgoal, subgoal 1 (ID 6)
-
-  x : nat
-  Heq : x = 2
-  ============================
-  2 + 2 = 4
->> *)
-(* begin hide *)
-Abort.
-(* end hide *)
-(** The [rewrite_something] tactic will search an equality relation to use to
-    modify your goal. How does it work?
-
-      - [match goal with] tells Coq we want to pattern match on the whole proof
-        state, not only a known named hypothesis
-      - [ H: ?x = _ |- _ ] is a pattern to tell coq we are looking for a
-        hypothesis [_ = _]
-      - [?x] is a way to bind the left operand of [=] to the name [x]
-      - The right side of [|-] is dedicated to the current goal
-      - [context[?x]] is a way to tell Coq we don’t really want to pattern-match
-        the goal as a whole, but rather we are looking for a subterm of the form
-        [?x]
-      - [rewrite H] will be used in case Coq is able to satisfy the constrains
-        specified by the pattern, with [H] being the hypothesis selected by Coq
-
-
-    Finally, there is one last thing you really need to know before writing a
-    tactic: the difference between [match] and [lazymatch]. Fortunately, it is
-    pretty simple. One the one hand, with [match], if one pattern matches, but
-    the branch body fails, Coq will backtrack and try the next branch. On the
-    other hand, [lazymatch] will stop on error.
-
-    So, for instance, the two following tactics will print two different
-    messages: *)
-
-Ltac match_failure :=
-  match goal with
-  | [ |- _ ]
-    => fail "fail in first branch"
-  | _
-    => fail "fail in second branch"
-  end.
-
-Ltac match_failure' :=
-  lazymatch goal with
-  | [ |- _ ]
-    => fail "fail in first branch"
-  | _
-    => fail "fail in second branch"
-  end.
-
-(** We can try that quite easily by starting a dumb goal (eg. [Goal (True).])
-    and call our tactic. For [match_failure], we get:
-
-<<
-Ltac call to "match_failure" failed.
-Error: Tactic failure: fail in second branch.
->>
-
-    On the other hand, for [lazymatch_failure], we get:
-
-<<
-Ltac call to "match_failure'" failed.
-Error: Tactic failure: fail in first branch.
->> *)
-
-(** ** Conclusion *)
-
-(** I were able to tackle my automation needs with these Ltac features. As
-    always with Coq, there is more to learn. For instance, I saw that there is a
-    third kind of pattern match ([multimatch]) I know nothing about. *)
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. *)
diff --git a/site/posts/LtacPatternMatching.v b/site/posts/LtacPatternMatching.v
new file mode 100644
index 0000000..d52d0bf
--- /dev/null
+++ b/site/posts/LtacPatternMatching.v
@@ -0,0 +1,184 @@
+(** * Pattern Matching on Types and Contexts  *)
+
+(** In the #<a href="LtacMetaprogramming.html">#previous article#</a># of our
+    series on Ltac, we have shown how tactics allow for constructing Coq terms
+    incrementally.  Ltac programs (“proof scripts”) generate terms, and the
+    shape of said terms can be very different regarding the initial context. For
+    instance, [induction x] will refine the current goal using an inductive
+    principle dedicated to the type of [x].
+
+    This is possible because Ltac allows for pattern matching on types and
+    contexts. In this article, we give a short introduction on this feature of
+    key importance. *)
+
+(** #<div id="generate-toc"></div>#
+
+    #<div id="history">site/posts/LtacPatternMatching.v</div># *)
+
+(** ** To [lazymatch] or to [match] *)
+
+(** Gallina provides one pattern matching construction, whose semantics is
+    always the same: for a given term, the first pattern to match will always be
+    selected. On the contrary, Ltac provides several pattern matching
+    constructions with different semantics. This key difference has probably
+    been motivated because Ltac is not a total language: a tactic may not always
+    succeed.
+
+    Ltac programmers can use [match] or [lazymatch]. One the one hand, with
+    [match], if one pattern matches, but the branch body fails, Coq will
+    backtrack and try the next branch. On the other hand, [lazymatch] will stop
+    on error.
+
+    So, for instance, the two following tactics will print two different
+    messages: *)
+
+Ltac match_failure :=
+  match goal with
+  | _
+    => fail "fail in first branch"
+  | _
+    => fail "fail in second branch"
+  end.
+
+Ltac lazymatch_failure :=
+  lazymatch goal with
+  | _
+    => fail "fail in first branch"
+  | _
+    => fail "fail in second branch"
+  end.
+
+(** We can try that quite easily by starting a dumb goal (eg. [Goal (True).])
+    and call our tactic. For [match_failure], we get:
+
+<<
+Ltac call to "match_failure" failed.
+Error: Tactic failure: fail in second branch.
+>>
+
+    On the other hand, for [lazymatch_failure], we get:
+
+<<
+Ltac call to "match_failure'" failed.
+Error: Tactic failure: fail in first branch.
+>>
+
+    Moreover, pattern matching allows for matching over _patterns_, not just
+    constants. Here, Ltac syntax differs from Gallina’s. In Gallina, if a
+    variable name is used in a pattern, Gallina creates a new variable in the
+    scope of the related branch. If a variable with the same name already
+    existed, it is shadowed. On the contrary, in Ltac, using a variable name
+    as-is in a pattern implies an equality check.
+
+    To illustrate this difference, we can take the example of the following
+    tactic. *)
+
+Ltac successive x y :=
+  lazymatch y with
+  | S x => idtac
+  | _ => fail
+  end.
+
+(** [successive x y] will fails if [y] is not the successor of [x]. On the
+    contrary, the “syntactically equivalent” function in Gallina will exhibit
+    a totally different behavior. *)
+
+Definition successor (x y : nat) : bool :=
+  match y with
+  | S x => true
+  | _ => false
+  end.
+
+(** Here, the first branch of the pattern match is systematically selected when
+    [y] is not O, and in this branch, the argument [x] is shadowed by the
+    predecessor of [y].
+
+    For Ltac to adopt a behavior similar to Gallina, the [?] prefix shall be
+    used. For instance, the following tactic will check whether its argument
+    has a known successor, prints it if it does, or fail otherwise. *)
+
+Ltac print_pred_or_zero x :=
+  match x with
+  | S ?x => idtac x
+  | _ => fail
+  end.
+
+(** On the one hand, [print_pred_or_zero 3] will print [2]. On the other hand,
+    if there exists a variable [x : nat] in the context, calling
+    [print_pred_or_zero x] will fail, since the exact value of [x] is not
+    known. *)
+
+(** ** Pattern Matching on Types with [type of] *)
+
+(** The [type of] operator can be used in conjunction to pattern matching to
+    generate different terms according to the type of a variable. We could
+    leverage this to reimplement <<induction>> for instance.
+
+    As an example, we propose the following <<not_nat>> tactic which, given an
+    argument [x], fails if [x] is of type [nat]. *)
+
+Ltac not_nat x :=
+  lazymatch type of x with
+  | nat => fail "argument is of type nat"
+  | _ => idtac
+  end.
+
+(** With this definition, <<not_nat true>> succeeds since [true] is of type
+    [bool], and [not_nat O] since [O] encodes #<span class="imath">#0#</span># in
+    [nat].
+
+    We can also use the [?] prefix to write true pattern. For instance, the
+    following tactic will fail if the type of its supplied argument has at least
+    one parameter. *)
+
+Ltac not_param_type x :=
+  lazymatch type of x with
+  | ?f ?a => fail "argument is of type with parameter"
+  | _ => idtac
+  end.
+
+(** Both <<not_param_type (@nil nat)>> of type [list nat] and <<(@eq_refl nat
+    0)>> of type [0 = 0] fail, but <<not_param_type 0>> of type [nat]
+    succeeds. *)
+
+(** ** Pattern Matching on the Context with [goal] *)
+
+(** Lastly, we discuss how Ltac allows for inspecting the context (i.e., the
+    hypotheses and the goal) using the [goal] keyword.
+
+    For instance, we propose a naive implementation of the [subst] tactic
+    as follows. *)
+
+Ltac subst' :=
+  repeat
+    match goal with
+    | H :  ?x = _ |- context[?x]
+      => repeat rewrite H; clear H
+    end.
+
+(** With [goal], patterns are of the form <<H : (pattern), ... |- (pattern)>>.
+
+      - At the left side of [|-], we match on hypotheses. Beware that
+        contrary to variable name in pattern, hypothesis names behaves as in
+        Gallina (i.e., fresh binding, shadowing, etc.). In the branch, we are
+        looking for equations, i.e., an hypothesis of the form [?x = _].
+      - At the right side of [|-], we match on the goal.
+
+    In both cases, Ltac makes available an interesting operator,
+    [context[(pattern)]], which is satisfies if [(pattern)] appears somewhere in
+    the object we are pattern matching against. So, the branch of the [match]
+    reads as follows: we are looking for an equation [H] which specifies the
+    value of an object [x] which appears in the goal. If such an equation
+    exists, <<subst'>> tries to <<rewrite>> [x] as many time as possible.
+
+    This implementation of [subst'] is very fragile, and will not work if the
+    equation is of the form [_ = ?x], and it may behaves poorly if we have
+    “transitive equations”, such as there exists hypotheses [?x = ?y] and [?y =
+    _]. Motivated readers may be interested in proposing more robust
+    implementation of [subst']. *)
+
+(** ** Conclusion *)
+
+(** This concludes our tour on Ltac pattern matching capabilities. In the #<a
+    href="MixingLtacAndGallina.html">#next article of this series#</a>#, we
+    explain how Ltac and Gallina can actually be used simultaneously. *)
diff --git a/site/posts/MixingLtacAndGallina.v b/site/posts/MixingLtacAndGallina.v
index 1fd1228..4e6b28d 100644
--- a/site/posts/MixingLtacAndGallina.v
+++ b/site/posts/MixingLtacAndGallina.v
@@ -1,10 +1,6 @@
 (** * Mixing Ltac and Gallina for Fun and Profit *)
 
-(** This write-up is the second part of a series on Ltac, the default tactic
-    language of Coq. The first part explains #<a href="/posts/Ltac101.html">how
-    Coq users can define their own tactics</a>#.
-
-    One of the most misleading introduction to Coq is to say that “Gallina is
+(** One of the most misleading introduction to Coq is to say that “Gallina is
     for programs, while tactics are for proofs.”  Indeed, in Coq we construct
     terms of given types, always. Terms encodes both programs and proofs about
     these programs. Gallina is the preferred way to construct programs, and
@@ -12,190 +8,22 @@
 
     The key word here is “preferred.” We do not always need to use tactics to
     construct a proof term. Conversly, there are some occasions where
-    constructing a program with tactics become handy. Furthermore, Coq allows
-    for calling tactics from Gallina definitions. Compare to Gallina, Ltac
-    provides two very interesting features:
+    constructing a program with tactics become handy. Furthermore, Coq actually
+    allows for _mixing together_ Ltac and Gallina.
+
+    In the #<a href="LtacPatternMatching.html">#previous article of this
+    series#</a>#, we discuss how Ltac provides two very interesting features:
 
       - With [match goal with] it can inspect its context
       - With [match type of _ with] it can pattern matches on types
 
     It turns out these features are more than handy when it comes to
-    metaprogramming (that is, the generation of programs by programs).
-
-    We proceed as follows. First, we try to demystify how Ltac actually works
-    under the hood. Then, we detail which bridges exists between Gallian and
-    Ltac. Finally, we quickly discuss the risk of using Ltac to generate
-    terms that do not encode proofs. *)
+    metaprogramming (that is, the generation of programs by programs). *)
 
 (** #<div id="generate-toc"></div>#
 
     #<div id="history">site/posts/MixingLtacAndGallina.v</div># *)
 
-(** ** What Do Tactics Do? *)
-
-(** The Coq proof environment is basically a State monad, where said state is
-    an incomplete terms that is being gradually constructed. This term is hidden
-    to the user, and Coq rather presents so-called “goals.”
-
-    From this perspective, a goal in Coq in basically a hole within the term we
-    are constructing. 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. *)
-
-Definition identity : forall (α : Type), α -> α.
-
-(** At this point, we have tell Coq that we want to construct a term of type
-    [forall (α : Type), α -> α]. *)
-
-Proof.
-
-(** Coq presents us one goal of the form
-
-    #<div class="dmath">#\vdash \forall (\alpha : \mathrm{Type}),\ \alpha \rightarrow \alpha#</div>#
-
-    As for the term that we want to construct and that Coq is hiding from us, it
-    is just a hole.
-
-    In a Coq course, you will learn than the <<intro>> allows for turning the
-    premise of an implication into an hypothesis within the context, that is
-
-    #<div class="dmath">#C \vdash P \rightarrow Q#</div>#
-
-    becomes
-
-    #<div class="dmath">#C,\ P \vdash Q#</div>#
-
-    What <<intro>> actually does in refining the “hidden” terms, by inserting
-    an anonymous function. So, when we use *)
-
-  intro α.
-
-(** it refines the term
-
-<<
-_1
->>
-
-    into
-
-<<
-fun (α : Type) => _2
->>
-
-    Similarly, *)
-
-  intros x.
-
-(** refines <<_2>> into
-
-<<
-fun (x : α) => _3
->>
-
-    which means the term constructed (and hidden) by Coq is now
-
-<<
-fun (α : Type) (x : α) => _3
->>
-
-    In the scope wherein <<_3>> lives, two variables are available: [α] and
-    [x]. Therefore, the goal presented by Coq is
-
-    #<div class="dmath">#\alpha : \mathrm{Type},\ x : \alpha \vdash \alpha#</div>#
-
-    The [assert] tactic is used to “add an hypothesis to the context, assuming
-    you can prove the hypothesis is true from the context.” What [assert] does
-    under the hood is refine the term we are constructed using [let _ in _].
-
-    More precisely, when we use *)
-
-  assert (y : α).
-
-(** It refines the hole [_3] into
-
-<<
-let y : α := _4 in _5
->>
-
-    which means the term we are constructing becomes
-
-<<
-fun (α : Type) (x : α) => let y : α := _4 in _5
->>
-
-    On the one hand, there are two variables availabre inside the scope wherein <<_4>> lives,
-    so the related goal is
-
-    #<div class="dmath">#α : \mathrm{Type},\ x : α \vdash \alpha#</div>#
-
-    On the other hand, there are _three_ variables available for defining
-    <<_5>> and the goal presented to the user is now
-
-    #<div class="dmath">#\alpha : \mathrm{Type},\ x : \alpha,\ y : \alpha \vdash \alpha#</div>#
-
-    To conclude this first example, we can discuss the [exact] tactic. This
-    tactic takes a term as its argument, and fills the current hole (solves the
-    current goal) with this term. We solve the two subgoals generated by
-    [assert] using [exact].
-
-    First, we fill <<_4>> with [x]. *)
-
-  + exact x.
-
-(** Therefore, <<_4>> becomes [x], and the terms that we are gradually defining
-    now is
-
-<<
-fun (α : Type) (x : α) => let y : α := x in _5
->>
-
-    Similarly, *)
-
-  + exact y.
-
-(** fill the last hole with [y].
-<<
-fun (α : Type) (x : α) => let y : α := x in y
->>
-
-    The term that we are constructing does not have any hole we need to fill,
-    and therefore Coq does not present us any more “goals to solve.”
-
-    This is not the end of the story, though. Tactics in Coq are not trusted.
-    It is assumed they can be buggy, which would mean that they can in theory
-    generate incorrect terms. As a consequence, we need to tell Coq to check the
-    term (or verify the proof) using [Qed] or [Defined]. *)
-
-Defined.
-
-(** Coq accepts the [Defined] command without complaining. It means that the
-    term generated by the tactics typechecks.
-
-    To some extend, the [refine] tactics is actually the most basic tool you may
-    need. For instance,
-
-    - [intro x] is equivalent to [refine (fun x => _)]
-    - [assert (x : T)] is equivalent to [refine (let x : T := _ in _)]
-    - [exact x] is equivalent to [refine x]
-
-    And so on. As a consequence, we can rewrite the previous proof script using
-    [refine]. *)
-
-Definition identity' : forall (α : Type), α -> α.
-
-Proof.
-  refine (fun (α : Type) => _).
-  refine (fun (x : α) => _).
-  unshelve refine (let y : α := _ in _).
-  + refine x.
-  + refine y.
-Defined.
-
 (** ** A Tale of Two Worlds, and Some Bridges *)
 
 (** Constructing terms proofs directly in Gallina often happens when one is