# How do I prove an expression in Coq that involves pattern matching?

I'm working on a proof in Coq and my proof state is as follows:

n: Z
H: 1 < n
1/1
match factorial (Z.to_nat n) with
| 0 => 0
| Z.pos y' => Z.pos y'
| Z.neg y' => Z.neg y'
end = factorial (Z.to_nat n)


My factorial function, in turn, is:

Fixpoint factorial (n : nat) : Z :=
match n with
| O => 1
| S p => Z.of_nat n * factorial p
end.


I am not sure which tactics to use to complete this proof. It seems pretty straightforward, but nothing seems to be working to get rid of the pattern matching expression. Can anybody help me?

you can do destruct (factorial (Z.to_nat n)).

• This worked like a charm! Thank you very much. I had never seen destruct used like this, only directly on variables. This is good to know. Apr 14 at 8:22
• destruct is a very powerful tactic. Don't hesitate to look it up in the doc. I think you could also use destruct factorial, it will have automatically selected the term in your goal on which to perform the case analysis.
– Lolo
Apr 14 at 8:28
• Yep, tried just destruct factorial and that also worked. I'll be sure to check it out in the docs. I'm relatively new to Coq, and I find proofs difficult because often I don't even know which tactic I need, so I'm not sure which one to look up. I'm sure I'll get the hang of it. Apr 14 at 8:31
• don´t hesitate to aks questions in StackExchange!!
– Lolo
Apr 14 at 8:35