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: Jul 15 2024 at 20:02 UTC