I have a problem that I managed to squeeze to a minimal example:
Fixpoint mod2 n :=
match n with
| 0 => 0
| 1 => 1
| S (S n) => n
end.
Fixpoint lt2 n :=
match n with
| 0 => true
| 1 => true
| _ => false
end.
Goal forall n, lt2 (mod_2 n).
Proof.
induction n.
by [].
induction n.
by [].
rewrite/mod2.
I can get here, but the induction hypothesis is not what I was expecting. What am I doing wrong?
You probably want to change mod2
to
Fixpoint mod2 n :=
match n with
| 0 => 0
| 1 => 1
| S (S n) => mod2 n
end.
I am not sure which induction hypothesis you are expecting, but you can strengthen it by changing your goal to forall n, lt2 (mod2 n) /\ lt2 (mod2 (S n))
for instance.
Thanks. That solved the problem I had! But since my case is way more convoluted, now that creates me an entire new problem
Generalizing the goal to obtain the right induction invariant can be applied in many cases though.
xixejas has marked this topic as resolved.
Last updated: Mar 28 2024 at 21:01 UTC