summaryrefslogtreecommitdiffstats log msg author committer range
path: root/site/posts/Ltac101.v
diff options
 context: 12345678910152025303540 space: includeignore mode: unifiedssdiffstat only
Diffstat (limited to 'site/posts/Ltac101.v')
-rw-r--r--site/posts/Ltac101.v304
1 files changed, 304 insertions, 0 deletions
 diff --git a/site/posts/Ltac101.v b/site/posts/Ltac101.vnew file mode 100644index 0000000..a9d4d68--- /dev/null+++ b/site/posts/Ltac101.v@@ -0,0 +1,304 @@+(** #+

Ltac 101

++ # *)++(** 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. *)++(** #
# *)++(** ** 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+ <>) in the context. If we try to use <> 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 <> 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. *)