summaryrefslogtreecommitdiffstats
path: root/site/posts/LtacMetaprogramming.v
diff options
context:
space:
mode:
authorThomas Letan <lthms@soap.coffee>2020-08-28 19:37:02 +0200
committerThomas Letan <lthms@soap.coffee>2020-08-28 20:10:04 +0200
commita7e45316109aa220bd7be9da0888dfbbf86e6aec (patch)
treeba613dc8a8abe396d209e75fc49d7897bee3349b /site/posts/LtacMetaprogramming.v
parente456e7c3a4814373ada40d0c69c870a656baeb29 (diff)
Heavy reworking of the Ltac series
Diffstat (limited to 'site/posts/LtacMetaprogramming.v')
-rw-r--r--site/posts/LtacMetaprogramming.v251
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. *)