summaryrefslogtreecommitdiffstats
path: root/site/posts/Ltac101.v
blob: a9d4d686788736e8140d15d1039d8beb0a7eb024 (plain)
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
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
(** #
<h1>Ltac 101</h1>
<time datetime="2017-10-16">2017-10-16</time>
    # *)

(** In this article, I 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. *)

(** #<div id="generate-toc"></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:”

    \( \forall s\ l\ s', P(s) \wedge s \overset{l\ }{\mapsto} s' \rightarrow  P(s') \),
    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 \( \wedge \)). 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. *)