Stream: math-comp users

Topic: Double induction


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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