## Stream: math-comp users

### Topic: Double induction

#### xixejas (Oct 01 2022 at 20:09):

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?

#### Kenji Maillard (Oct 01 2022 at 20:25):

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.

#### xixejas (Oct 01 2022 at 20:47):

Thanks. That solved the problem I had! But since my case is way more convoluted, now that creates me an entire new problem

#### Kenji Maillard (Oct 01 2022 at 20:52):

Generalizing the goal to obtain the right induction invariant can be applied in many cases though.

Last updated: Jan 29 2023 at 19:02 UTC