I am working with the following function nat->bool defined inductively:

Fixpoint evenb (n:nat) : bool :=

match n with

| O => true

| S O => false

| S (S m) => evenb m

end.

and I intend to use at some point a simple case analysis: "either n is even and ..., or n is odd and ..., qed." If I understand well, this is precisely what "case (evenb n)" is supposed to do. My problem is: it does create two subgoals, but does not add anything to the context. I have attempted various things with other tactics such as destruct, induction, etc. but with no better result. So, what did I do wrong? Or what is the right syntax to use? Many thanks in advance for your help!

You can use either `case_eq`

or `destruct (evenb n) eqn:eq`

to keep an equation.

...and it works indeed! Thank you!

Last updated: Oct 05 2023 at 02:01 UTC