From 9754a53fdc14f6ee4cf00f851cda68d69889bdcd Mon Sep 17 00:00:00 2001
From: Thomas Letan
Date: Tue, 4 Feb 2020 18:13:38 +0100
Subject: Initial commit with previous content and a minimal theme
---
site/posts/Ltac101.v | 304 +++++++++++++++++++++++++++++++++++++++++++++++++++
1 file changed, 304 insertions(+)
create mode 100644 site/posts/Ltac101.v
(limited to 'site/posts/Ltac101.v')
diff --git a/site/posts/Ltac101.v b/site/posts/Ltac101.v
new file mode 100644
index 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. *)
--
cgit v1.2.3