diff options
author | Thomas Letan <lthms@soap.coffee> | 2020-08-28 19:37:02 +0200 |
---|---|---|
committer | Thomas Letan <lthms@soap.coffee> | 2020-08-28 20:10:04 +0200 |
commit | a7e45316109aa220bd7be9da0888dfbbf86e6aec (patch) | |
tree | ba613dc8a8abe396d209e75fc49d7897bee3349b /site/posts/Ltac101.v | |
parent | Add a page to display my keystrokes reporting (diff) |
Heavy reworking of the Ltac series
Diffstat (limited to 'site/posts/Ltac101.v')
-rw-r--r-- | site/posts/Ltac101.v | 308 |
1 files changed, 0 insertions, 308 deletions
diff --git a/site/posts/Ltac101.v b/site/posts/Ltac101.v deleted file mode 100644 index 2b71a8f..0000000 --- a/site/posts/Ltac101.v +++ /dev/null @@ -1,308 +0,0 @@ -(** * Ltac 101 *) - -(** We 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. - - This write-up (originally published on #<span - id="original-created-at">October 16, 2017</span>#) is the first part of a - series on Ltac. The next part explains #<a - href="/posts/MixingLtacAndGallina.html">how to mix Gallina and Ltac</a>#. *) - -(** #<div id="generate-toc"></div># - - #<div id="history">site/posts/Ltac101.v</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”: - #<span class="imath">#\forall s\ l\ s', P(s) \wedge s \overset{l\ }{\mapsto} - s' \rightarrow P(s')#</span>#, 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 #<span - class="imath">#\wedge#</span>#). 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. *) |