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

what's your proof attempt like?

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.

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

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

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)

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

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

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

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

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

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

@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...

use Print to see the details

Last updated: Oct 03 2023 at 04:02 UTC