Stream: Coq users

Topic: Help with induction


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

view this post on Zulip Gaëtan Gilbert (Sep 19 2021 at 20:50):

what's your proof attempt like?

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

view this post on Zulip Gaëtan Gilbert (Sep 19 2021 at 21:04):

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

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

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

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

view this post on Zulip BezAj (Sep 19 2021 at 21:23):

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

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

view this post on Zulip BezAj (Sep 19 2021 at 21:31):

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

view this post on Zulip Karl Palmskog (Sep 19 2021 at 21:33):

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

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

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

view this post on Zulip Gaëtan Gilbert (Sep 20 2021 at 07:25):

use Print to see the details


Last updated: Jan 31 2023 at 14:03 UTC