Guillaume Dubach (Oct 26 2020 at 14:40): 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!
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.
Guillaume Dubach (Oct 26 2020 at 14:48):...and it works indeed! Thank you!
Last updated: Oct 13 2024 at 01:02 UTC