summaryrefslogtreecommitdiffstats log msg author committer range
path: root/site/posts/Ltac101.v
blob: a9d4d686788736e8140d15d1039d8beb0a7eb024 (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  .highlight .hll { background-color: #ffffcc } .highlight .c { color: #888888 } /* Comment */ .highlight .err { color: #a61717; background-color: #e3d2d2 } /* Error */ .highlight .k { color: #008800; font-weight: bold } /* Keyword */ .highlight .ch { color: #888888 } /* Comment.Hashbang */ .highlight .cm { color: #888888 } /* Comment.Multiline */ .highlight .cp { color: #cc0000; font-weight: bold } /* Comment.Preproc */ .highlight .cpf { color: #888888 } /* Comment.PreprocFile */ .highlight .c1 { color: #888888 } /* Comment.Single */ .highlight .cs { color: #cc0000; font-weight: bold; background-color: #fff0f0 } /* Comment.Special */ .highlight .gd { color: #000000; background-color: #ffdddd } /* Generic.Deleted */ .highlight .ge { font-style: italic } /* Generic.Emph */ .highlight .gr { color: #aa0000 } /* Generic.Error */ .highlight .gh { color: #333333 } /* Generic.Heading */ .highlight .gi { color: #000000; background-color: #ddffdd } /* Generic.Inserted */ .highlight .go { color: #888888 } /* Generic.Output */ .highlight .gp { color: #555555 } /* Generic.Prompt */ .highlight .gs { font-weight: bold } /* Generic.Strong */ .highlight .gu { color: #666666 } /* Generic.Subheading */ .highlight .gt { color: #aa0000 } /* Generic.Traceback */ .highlight .kc { color: #008800; font-weight: bold } /* Keyword.Constant */ .highlight .kd { color: #008800; font-weight: bold } /* Keyword.Declaration */ .highlight .kn { color: #008800; font-weight: bold } /* Keyword.Namespace */ .highlight .kp { color: #008800 } /* Keyword.Pseudo */ .highlight .kr { color: #008800; font-weight: bold } /* Keyword.Reserved */ .highlight .kt { color: #888888; font-weight: bold } /* Keyword.Type */ .highlight .m { color: #0000DD; font-weight: bold } /* Literal.Number */ .highlight .s { color: #dd2200; background-color: #fff0f0 } /* Literal.String */ .highlight .na { color: #336699 } /* Name.Attribute */ .highlight .nb { color: #003388 } /* Name.Builtin */ .highlight .nc { color: #bb0066; font-weight: bold } /* Name.Class */ .highlight .no { color: #003366; font-weight: bold } /* Name.Constant */ .highlight .nd { color: #555555 } /* Name.Decorator */ .highlight .ne { color: #bb0066; font-weight: bold } /* Name.Exception */ .highlight .nf { color: #0066bb; font-weight: bold } /* Name.Function */ .highlight .nl { color: #336699; font-style: italic } /* Name.Label */ .highlight .nn { color: #bb0066; font-weight: bold } /* Name.Namespace */ .highlight .py { color: #336699; font-weight: bold } /* Name.Property */ .highlight .nt { color: #bb0066; font-weight: bold } /* Name.Tag */ .highlight .nv { color: #336699 } /* Name.Variable */ .highlight .ow { color: #008800 } /* Operator.Word */ .highlight .w { color: #bbbbbb } /* Text.Whitespace */ .highlight .mb { color: #0000DD; font-weight: bold } /* Literal.Number.Bin */ .highlight .mf { color: #0000DD; font-weight: bold } /* Literal.Number.Float */ .highlight .mh { color: #0000DD; font-weight: bold } /* Literal.Number.Hex */ .highlight .mi { color: #0000DD; font-weight: bold } /* Literal.Number.Integer */ .highlight .mo { color: #0000DD; font-weight: bold } /* Literal.Number.Oct */ .highlight .sa { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Affix */ .highlight .sb { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Backtick */ .highlight .sc { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Char */ .highlight .dl { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Delimiter */ .highlight .sd { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Doc */ .highlight .s2 { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Double */ .highlight .se { color: #0044dd; background-color: #fff0f0 } /* Literal.String.Escape */ .highlight .sh { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Heredoc */ .highlight .si { color: #3333bb; background-color: #fff0f0 } /* Literal.String.Interpol */ .highlight .sx { color: #22bb22; background-color: #f0fff0 } /* Literal.String.Other */ .highlight .sr { color: #008800; background-color: #fff0ff } /* Literal.String.Regex */ .highlight .s1 { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Single */ .highlight .ss { color: #aa6600; background-color: #fff0f0 } /* Literal.String.Symbol */ .highlight .bp { color: #003388 } /* Name.Builtin.Pseudo */ .highlight .fm { color: #0066bb; font-weight: bold } /* Name.Function.Magic */ .highlight .vc { color: #336699 } /* Name.Variable.Class */ .highlight .vg { color: #dd7700 } /* Name.Variable.Global */ .highlight .vi { color: #3333bb } /* Name.Variable.Instance */ .highlight .vm { color: #336699 } /* Name.Variable.Magic */ .highlight .il { color: #0000DD; font-weight: bold } /* Literal.Number.Integer.Long */(** #

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