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

Your Answer

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

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