summaryrefslogtreecommitdiffstats
path: root/site/posts/LtacMetaprogramming.v
blob: 6b086e39ba05874d32baeeb4f4a4cfbde306020f (plain) (blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
(** #<nav><p class="series">Ltac.html</p>
     <p class="series-next">LtacPatternMatching.html</p></nav># *)

(** * 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. *)