## 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).
``````

#### 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