The Coq mailing list

[Razvan Voicu <razvan AT comp.nus.edu.sg>]

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