How to match the expression "match"?

Question

I am trying to write a rule for hypotheses formulated using match construction:

 Goal forall x:nat, (match x with | 1 => 5 | _ => 10 end = 5 -> x = 1)%nat. intros. x : nat H : match x with | 0%nat => 10%nat | 1%nat => 5%nat | S (S _) => 10%nat end = 5%nat ============================ x = 1%nat 

How can I compare such hypotheses? The following direct line method does not work:

 match goal with |[H:match ?e with | ?a => ?x | ?b => ?y | ?c => ?z end = ?b] => idtac end. > Syntax error: 'end' expected after [branches] (in [match_constr]). 

Answer 1

Comparing patterns in match statements is somewhat strange.

The first thing you should know is that inside Coq there is no such thing as match for several variables or with deep correspondence: everything is translated in terms of simpler match operators. So you actually wrote syntactic sugar on the following term:

 match x with | 0 => 10 | S x' => match x' with | 0 => 5 | S x'' => 10 end end 

what Coq points to when he prints your proof. The problem is that this syntax sugar does not work on Ltac templates: thus, when writing an Ltac template that mentions match , you should always try to match it as if it were a sibling match .

The second problem is that you cannot bind part of the template to match : something like

 match goal with | H : match ?x => _ | ?y => _ end = 5 |- _ => (* ... *) end 

doesn't really make sense in Ltac.

You have two options for solving your problem:

• Write down the match you expect with an exact list of constructors of your type on part of the template, for example.

   match goal with | H : match x with 0 => _ | S _ => _ end = 5 |- _ => (* ... *) end 

• Use the special match (* ... *) with _ => _ end syntax match (* ... *) with _ => _ end , which matches any match :

   match goal with | H : match x with _ => _ end = 5 |- _ => (* ... *) end 

Often, as in your case, you still need to consider all match branches, including deep ones. This idiom is often useful in this case:

 repeat match goal with | H : match ?x with _ => _ end = _ |- _ => destruct x; try solve [inversion H] end.