# Pattern Matching on Types and Contexts

## Revisions

This revisions table has been automatically generated
from the
`git`

history of this website repository, and the
change descriptions may not always be as useful as they should.

You can consult the source of this file in its current version here.

2021-03-28 | 2021 Spring redesign | 495f9db |

2020-08-28 | Heavy reworking of the Ltac series | a7e4531 |

## To lazymatch or to match §

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:
On the other hand, for lazymatch_failure, we get:
Moreover, pattern matching allows for matching over
To illustrate this difference, we can take the example of the following
tactic.

Ltac call to "match_failure" failed. Error: Tactic failure: fail in second branch.

Ltac call to "match_failure'" failed. Error: Tactic failure: fail in first branch.

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

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.

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.
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
As an example, we propose the following

## Pattern Matching on Types with type of §

`induction`

for instance.
`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,
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.

`not_nat true`

succeeds since true is of type
bool, and not_nat O since O encodes $0$
in
nat.
Ltac not_param_type x :=

lazymatch type of x with

| ?f ?a => fail "argument is of type with parameter"

| _ => idtac

end.

Both
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.

`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 §

With goal, patterns are of the form
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,
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'.
This concludes our tour on Ltac pattern matching capabilities. In the next article of this series, we
explain how Ltac and Gallina can actually be used simultaneously.

`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.

`subst'`

tries to `rewrite`

x as many time as possible.