**diff options**

Diffstat (limited to 'site/posts/MixingLtacAndGallina.v')

-rw-r--r-- | site/posts/MixingLtacAndGallina.v | 330 |

1 files changed, 330 insertions, 0 deletions

diff --git a/site/posts/MixingLtacAndGallina.v b/site/posts/MixingLtacAndGallina.v new file mode 100644 index 0000000..fb30186 --- /dev/null +++ b/site/posts/MixingLtacAndGallina.v @@ -0,0 +1,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>. *) |