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.
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: Jan 31 2023 at 14:03 UTC