Stream: Coq users

Topic: Keeping an equation in case analysis


view this post on Zulip Guillaume Dubach (Oct 26 2020 at 14:40):

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!

view this post on Zulip Jakob Botsch Nielsen (Oct 26 2020 at 14:43):

You can use either case_eq or destruct (evenb n) eqn:eq to keep an equation.

view this post on Zulip Guillaume Dubach (Oct 26 2020 at 14:48):

...and it works indeed! Thank you!


Last updated: Jan 29 2023 at 01:02 UTC