1
$\begingroup$

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?

$\endgroup$

1 Answer 1

1
$\begingroup$

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

$\endgroup$
4
  • $\begingroup$ 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. $\endgroup$ Apr 14 at 8:22
  • $\begingroup$ 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. $\endgroup$
    – Lolo
    Apr 14 at 8:28
  • $\begingroup$ 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. $\endgroup$ Apr 14 at 8:31
  • $\begingroup$ don´t hesitate to aks questions in StackExchange!! $\endgroup$
    – Lolo
    Apr 14 at 8:35

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.