**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/LtacPatternMatching.v | |

parent | e456e7c3a4814373ada40d0c69c870a656baeb29 (diff) |

Heavy reworking of the Ltac series

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

-rw-r--r-- | site/posts/LtacPatternMatching.v | 184 |

1 files changed, 184 insertions, 0 deletions

diff --git a/site/posts/LtacPatternMatching.v b/site/posts/LtacPatternMatching.v new file mode 100644 index 0000000..d52d0bf --- /dev/null +++ b/site/posts/LtacPatternMatching.v @@ -0,0 +1,184 @@ +(** * Pattern Matching on Types and Contexts *) + +(** In the #<a href="LtacMetaprogramming.html">#previous article#</a># of our + series on Ltac, we have shown how tactics allow for constructing Coq terms + incrementally. Ltac programs (“proof scripts”) generate terms, and the + shape of said terms can be very different regarding the initial context. For + instance, [induction x] will refine the current goal using an inductive + principle dedicated to the type of [x]. + + This is possible because Ltac allows for pattern matching on types and + contexts. In this article, we give a short introduction on this feature of + key importance. *) + +(** #<div id="generate-toc"></div># + + #<div id="history">site/posts/LtacPatternMatching.v</div># *) + +(** ** To [lazymatch] or to [match] *) + +(** Gallina provides one pattern matching construction, whose semantics is + always the same: for a given term, the first pattern to match will always be + selected. On the contrary, Ltac provides several pattern matching + constructions with different semantics. This key difference has probably + been motivated because Ltac is not a total language: a tactic may not always + succeed. + + Ltac programmers can use [match] or [lazymatch]. 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 lazymatch_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. +>> + + Moreover, pattern matching allows for matching over _patterns_, not just + constants. Here, Ltac syntax differs from Gallina’s. In Gallina, if a + variable name is used in a pattern, Gallina creates a new variable in the + scope of the related branch. If a variable with the same name already + existed, it is shadowed. On the contrary, in Ltac, using a variable name + as-is in a pattern implies an equality check. + + To illustrate this difference, we can take the example of the following + tactic. *) + +Ltac successive x y := + lazymatch y with + | S x => idtac + | _ => fail + end. + +(** [successive x y] will fails if [y] is not the successor of [x]. On the + contrary, the “syntactically equivalent” function in Gallina will exhibit + a totally different behavior. *) + +Definition successor (x y : nat) : bool := + match y with + | S x => true + | _ => false + end. + +(** Here, the first branch of the pattern match is systematically selected when + [y] is not O, and in this branch, the argument [x] is shadowed by the + predecessor of [y]. + + For Ltac to adopt a behavior similar to Gallina, the [?] prefix shall be + used. For instance, the following tactic will check whether its argument + has a known successor, prints it if it does, or fail otherwise. *) + +Ltac print_pred_or_zero x := + match x with + | S ?x => idtac x + | _ => fail + end. + +(** On the one hand, [print_pred_or_zero 3] will print [2]. On the other hand, + if there exists a variable [x : nat] in the context, calling + [print_pred_or_zero x] will fail, since the exact value of [x] is not + known. *) + +(** ** Pattern Matching on Types with [type of] *) + +(** The [type of] operator can be used in conjunction to pattern matching to + generate different terms according to the type of a variable. We could + leverage this to reimplement <<induction>> for instance. + + As an example, we propose the following <<not_nat>> tactic which, given an + argument [x], fails if [x] is of type [nat]. *) + +Ltac not_nat x := + lazymatch type of x with + | nat => fail "argument is of type nat" + | _ => idtac + end. + +(** With this definition, <<not_nat true>> succeeds since [true] is of type + [bool], and [not_nat O] since [O] encodes #<span class="imath">#0#</span># in + [nat]. + + We can also use the [?] prefix to write true pattern. For instance, the + following tactic will fail if the type of its supplied argument has at least + one parameter. *) + +Ltac not_param_type x := + lazymatch type of x with + | ?f ?a => fail "argument is of type with parameter" + | _ => idtac + end. + +(** Both <<not_param_type (@nil nat)>> of type [list nat] and <<(@eq_refl nat + 0)>> of type [0 = 0] fail, but <<not_param_type 0>> of type [nat] + succeeds. *) + +(** ** Pattern Matching on the Context with [goal] *) + +(** Lastly, we discuss how Ltac allows for inspecting the context (i.e., the + hypotheses and the goal) using the [goal] keyword. + + For instance, we propose a naive implementation of the [subst] tactic + as follows. *) + +Ltac subst' := + repeat + match goal with + | H : ?x = _ |- context[?x] + => repeat rewrite H; clear H + end. + +(** With [goal], patterns are of the form <<H : (pattern), ... |- (pattern)>>. + + - At the left side of [|-], we match on hypotheses. Beware that + contrary to variable name in pattern, hypothesis names behaves as in + Gallina (i.e., fresh binding, shadowing, etc.). In the branch, we are + looking for equations, i.e., an hypothesis of the form [?x = _]. + - At the right side of [|-], we match on the goal. + + In both cases, Ltac makes available an interesting operator, + [context[(pattern)]], which is satisfies if [(pattern)] appears somewhere in + the object we are pattern matching against. So, the branch of the [match] + reads as follows: we are looking for an equation [H] which specifies the + value of an object [x] which appears in the goal. If such an equation + exists, <<subst'>> tries to <<rewrite>> [x] as many time as possible. + + This implementation of [subst'] is very fragile, and will not work if the + equation is of the form [_ = ?x], and it may behaves poorly if we have + “transitive equations”, such as there exists hypotheses [?x = ?y] and [?y = + _]. Motivated readers may be interested in proposing more robust + implementation of [subst']. *) + +(** ** Conclusion *) + +(** This concludes our tour on Ltac pattern matching capabilities. In the #<a + href="MixingLtacAndGallina.html">#next article of this series#</a>#, we + explain how Ltac and Gallina can actually be used simultaneously. *) |