The Coq mailing list

[Luke Palmer <lrpalmer AT gmail.com>]

I am no expert, and I'm sure others on this list will be able to provide much more concise and elegant proofs, but here's what I consider a clearer, more transparent version of the latter.  In particular, I prefer to use more intermediate lemmas.

Inductive even : nat -> Prop :=

| e0 : even 0

| eS : forall n, even n -> even (S (S n)).

Lemma eS_inverse : forall n, even (S (S n)) -> even n.

 intros n ; inversion H ; assumption.

Qed.

Lemma contrapositive : forall A B : Prop, (A -> B) -> ~B -> ~A.  intuition. Qed.

Lemma even_or_not_even' : forall n, (even n \/ ~even n) /\ (even (S n) \/ ~even (S n)).

 induction n ; split.

  left ; exact e0.

  right ; intro H ; inversion H.

 

 exact (proj2 IHn).

 destruct (proj1 IHn).

  left ; exact (eS _ H).

  right ; exact (contrapositive _ _ (eS_inverse n) H).

Qed.

Theorem even_or_not_even : forall n, even n \/ ~even n. 

 exact (fun n => proj1 (even_or_not_even' n)).

Qed.

On Sat, May 2, 2009 at 2:41 AM, Razvan Voicu <razvan AT comp.nus.edu.sg> wrote:

Dear Coq Users,

I would like to submit two inductive proofs to your attention. To me, they appear to be the "most straightforward" proofs for the given goals. But then, I happen to be biased by a background of proving entailment/equivalence of logic programs using fold/unfold transformations. So I would like to know your opinion: what would be, for you, the most straightforward proofs for the goals in question? I understand that the answers will be very subjective. However, it would be useful for me to be able to gauge what the Coq community perceives as typical inductive proofs for goals where predefined induction schemes do not seem to apply directly.

Below are my two proofs. Do note that the use of "refine" can be replaced by "fix" in Coq 8.2, as shown in the comment on the same line.

(***********************)
Inductive even : nat -> Prop :=
 | e0: even 0
 | eS: forall n, even n -> even (S (S n)).

Inductive m3: nat -> Prop :=
 | m30: m3 0
 | m3S: forall n, m3 n -> m3 (S (S (S n))).

Inductive m6: nat -> Prop :=
 | m60: m6 0
 | m6S: forall n, m6 n -> m6 (S (S (S (S (S (S n)))))).

Lemma multiples:
 forall n, even n -> m3 n -> m6 n.
Proof.
refine (* In Coq 8.2: fix 3 ; intros n H1 H2. *)
 (fix multiples
    (n : nat) (H1 : even n) (H2 : m3 n) {struct H2} := _).
destruct H2.
constructor.
destruct H2.
 inversion H1.
 inversion H0.
 inversion_clear H1 as [H| H3 H0].
 inversion_clear H0 as [H| H3 H].
 inversion_clear H as [H0| H3 H0].
 constructor.
 apply multiples.
 exact H0.
 exact H2.
Save.

Lemma even_or_not_even:
 forall n, even n \/ ~ even n.
Proof.
refine (* In Coq 8.2: fix 1; intro n. *)
 (fix even_or_not_even (n : nat) := _).
destruct n.
left.
constructor.
destruct n.
 right.
 intro H.
 inversion H.
 destruct (even_or_not_even n) as [H| H].
 left.
 constructor.
 exact H.
 right.
 intro H0.
 apply H.
 inversion H0.
 trivial.
Save.

(******************************)

Thank you in advance,

Razvan

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
        http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club