Stream: Coq users

Topic: Help with induction

BezAj (Sep 19 2021 at 20:37):

Hello, i learning CoQ and have little idea on how things goes from threre... I am trying to prove that Even + Even = Even. But no matter how i go around it i always end up going into infinite induction cases...

Also, that's my definition for Even and Odd.

Inductive even: nat -> Prop :=
  | even_0 : even O
  | even_s : forall n:nat, odd n -> even (S n)
with odd: nat -> Prop :=
  | odd_s : forall n:nat, even n -> odd (S n).

Gaëtan Gilbert (Sep 19 2021 at 20:50):

what's your proof attempt like?

BezAj (Sep 19 2021 at 20:57):

I've tried other strategies but everything ends like that:

Theorem ev_sum :
  forall n m, even n -> even m -> even (add n m).
Proof.
  intros n m H G.
  induction H.
  exact G.
  simpl.
  apply even_s.

And then i have to prove odd (add n m)... But it's never ending.

Gaëtan Gilbert (Sep 19 2021 at 21:04):

oh right the auto generated induction schemes for mutual inductives are useless

BezAj (Sep 19 2021 at 21:06):

Huh, how could i run with that ? I am trying my best to not use a double successor for even (like even_ss), and i know that works. But now i am trying to just use even_s and odd_s...

Gaëtan Gilbert (Sep 19 2021 at 21:12):

you can prove

Fixpoint double_even_ind (P:nat -> Prop) (p0 : P 0) (pSS : forall n, even n -> P n -> P (S (S n)))
         n (H:even n) : P n.
Proof.
  destruct H as [|? [n H]].
  - exact p0.
  - apply (pSS _ H).
    apply double_even_ind;auto.
Qed.

then do induction H using double_even_ind
or you can do

Scheme even_odd_ind := Induction for even Sort Prop
  with odd_even_ind := Induction for odd Sort Prop.

and apply the resulting terms (the induction tactic won't work with them though)

Karl Palmskog (Sep 19 2021 at 21:16):

I think the standard advice is to not express even and odd as mutually inductive but as regular inductives, whence there is no need for the Scheme command for custom induction principles

BezAj (Sep 19 2021 at 21:23):

I am really lost about how to do that, so how i do without mutually inductive definition ?

Karl Palmskog (Sep 19 2021 at 21:26):

you will define two different inductive predicates. The base case of the first one is 0, the base case of the second is 1.

BezAj (Sep 19 2021 at 21:31):

But how can i do that without using double successor definition ?

Karl Palmskog (Sep 19 2021 at 21:33):

I'm not sure I see why double successors would be bad in themselves.

BezAj (Sep 19 2021 at 21:50):

Yeah sure, but first i have to prove it :)

And, @Gaëtan Gilbert solution works, i am still working into proving double_even_ind properly, but as i am doing it i can just prove even_ss and go with it...

so far, this works !

Fixpoint suce_even (P:nat -> Prop) (p0 : P 0) (pSS : forall n, even n -> P n -> P(S (S n)))
  n (H:even n) : P n.
Proof.
  destruct H as [| ? [n H]].
  exact p0.
  apply (pSS _ H).
  apply suce_even ; auto.
Qed.

Theorem ev_sum :
  forall n m, even n -> even m -> even (add n m).
Proof.
  intros n m H G.
  induction H using suce_even.
  exact G.
  simpl.
  apply even_s.
  apply odd_s.
  exact IHeven.
Qed.

BezAj (Sep 19 2021 at 22:11):

@Gaëtan Gilbert Also, sorry to ask but, there's a way that i can use this as a Lemma or Axiom ? Specially for trying to get into a more hands into details here... But honestly i'd be happy knowing more about Fixpoints and maybe doing it without Auto...

Gaëtan Gilbert (Sep 20 2021 at 07:25):

use Print to see the details

Last updated: Oct 03 2023 at 04:02 UTC