summaryrefslogtreecommitdiffstats
path: root/site/posts/MixingLtacAndGallina.v
blob: fb30186745e73e0b7856fb5a6f3b29b1809de8f2 (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
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
(** * Mixing Ltac and Gallina for Fun and Benefits *)

(** 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
    tactics are the preferred way to construct proofs.

    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:

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

(** #<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
    writing dependently-typed definition. For instance, we can write a type safe
    [from_option] function (inspired by #<a
    href="https://plv.csail.mit.edu/blog/unwrapping-options.html">#this very
    nice write-up#</a>#) such that the option to unwrap shall be accompagnied by
    a proof that said option contains something. This extra argument is used in
    the [None] case to derive a proof of [False], from which we can derive
    anything. *)

Definition is_some {α} (x : option α) : bool :=
  match x with Some _ => true | None => false end.

Lemma is_some_None {α} (x : option α)
  : x = None -> is_some x <> true.
Proof. intros H. rewrite H. discriminate. Qed.

Definition from_option {α}
    (x : option α) (some : is_some x = true)
  : α :=
  match x as y return x = y -> α with
  | Some x => fun _ => x
  | None => fun equ => False_rect α (is_some_None x equ some)
  end eq_refl.

(** In [from_option], we construct two proofs without using tactics:

      - [False_rect α (is_some_None x equ some)] to exclude the absurd case
      - [eq_refl] in conjunction with a dependent pattern matching (if you are
        not familiar with this trick: the main idea is to allow Coq to
        “remember” that [x = None] in the second branch)

    We can use another approach. We can decide to implement [from_option]
    with a proof script. *)

Definition from_option' {α}
    (x : option α) (some : is_some x = true)
  : α.

Proof.
  case_eq x.
  + intros y _.
    exact y.
  + intros equ.
    rewrite equ in some.
    now apply is_some_None in some.
Defined.

(** There is a third approach we can consider: mixing Gallina terms, and
    tactics. This is possible thanks to the [ltac:()] feature. *)

Definition from_option'' {α}
    (x : option α) (some : is_some x = true)
  : α :=
  match x as y return x = y -> α with
  | Some x => fun _ => x
  | None => fun equ => ltac:(rewrite equ in some;
                             now apply is_some_None in some)
  end eq_refl.

(** When Coq encounters [ltac:()], it treats it as a hole. It sets up a
    corresponding goal, and tries to solve it with the supplied tactic.

    Conversly, there exists ways to construct terms in Gallina when writing a
    proof script. Certains tactics takes such terms as arguments. Besides, Ltac
    provides [constr:()] and [uconstr:()] which work similarly to [ltac:()].
    The difference between [constr:()] and [uconstr:()] is that Coq will try to
    assign a type to the argument of [constr:()], but will leave the argument of
    [uconstr:()] untyped.

    For instance, consider the following tactic definition. *)

Tactic Notation "wrap_id" uconstr(x) :=
  let f := uconstr:(fun x => x) in
  exact (f x).

(** Both [x] the argument of [wrap_id] and [f] the anonymous identity function
    are not typed. It is only when they are composed together as an argument of
    [exact] (which expects a typed argument, more precisely of the type of the
    goal) that Coq actually tries to typecheck it.

    As a consequence, [wrap_id] generates a specialized identity function for
    each specific context. *)

Definition zero : nat := ltac:(wrap_id 0).

(** The generated anonymous identity function is [fun x : nat => x]. *)

Definition empty_list α : list α := ltac:(wrap_id nil).

(** The generated anonymous identity function is [fun x : list α => x]. Besides,
    we do not need to give more type information about [nil]. If [wrap_id] were
    to be expecting a typed term, we would have to replace [nil] by [(@nil
    α)]. *)

(** ** Beware the Automation Elephant in the Room *)

(** Proofs and computational programs are encoded in Coq as terms, but there is
    a fundamental difference between them, and it is highlighted by one of the
    axiom provided by the Coq standard library: proof irrelevance.

    Proof irrelevance states that two proofs of the same theorem (i.e., two
    proof terms which share the same type) are essentially equivalent, and can
    be substituted without threatening the trustworthiness of the system. From a
    formal methods point of view, it makes sense. Even if we value “beautiful
    proofs,” we mostly want correct proofs.

    The same reasoning does _not_ apply to computational programs. Two functions
    of type [nat -> nat -> nat] are unlikely to be equivalent.  For instance,
    [add], [mul] or [sub] share the same type, but computes totally different
    results.

    Using tactics such as [auto] to generate terms which do not live inside
    [Prop] is risky, to say the least. For instance, *)

Definition add (x y : nat) : nat := ltac:(auto).

(** This works, but it is certainly not what you would expect:

<<
add = fun _ y : nat => y
     : nat -> nat -> nat
>>

    That being said, if we keep that in mind, and assert the correctness of the
    generated programs (either by providing a proof, or by extensively testing
    it), there is no particular reason not to use Ltac to generate terms when it
    makes sens.

    Dependently-typed programming can help here. If we decorate the return type
    of a function with the expected properties of the result wrt. the function’s
    arguments, we can ensure the function is correct, and conversly prevent
    tactics such as [auto] to generate “incorrect” terms. Interested readers may
    refer to #<a href="/posts/StronglySpecifiedFunctions.html">#the dedicated
    series on this very website#</a>. *)