summaryrefslogtreecommitdiffstats
path: root/site/posts/LtacPatternMatching.v
diff options
context:
space:
mode:
authorThomas Letan <lthms@soap.coffee>2020-08-28 19:37:02 +0200
committerThomas Letan <lthms@soap.coffee>2020-08-28 20:10:04 +0200
commita7e45316109aa220bd7be9da0888dfbbf86e6aec (patch)
treeba613dc8a8abe396d209e75fc49d7897bee3349b /site/posts/LtacPatternMatching.v
parente456e7c3a4814373ada40d0c69c870a656baeb29 (diff)
Heavy reworking of the Ltac series
Diffstat (limited to 'site/posts/LtacPatternMatching.v')
-rw-r--r--site/posts/LtacPatternMatching.v184
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. *)