The Coq mailing list

[David Pichardie <david.pichardie AT irisa.fr>]

Hi,

Here are the scripts I would propose for such proofs.
For the second proof, my solution is closed from what Luke proposed.
Comments are welcome.

David.

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

Ltac inv H :=   inversion H; try (subst; clear H).

Require Export Omega.

Lemma multiples:
 forall n, even n -> m3 n -> m6 n.
Proof.
  induction n using lt_wf_ind; intros.
  destruct n.
  constructor.
  repeat match goal with
           | [ id : m3 (S _) |- _ ] => inv id
           | [ id : even (S _) |- _ ] => inv id
         end.
  constructor; auto with zarith.
Qed.

(*************)
Hint Constructors even.

Lemma evenSS : forall n, even (S (S n)) -> even n.
 intros n H; inversion H; assumption.
Qed.

Hint Resolve evenSS.

Lemma even_or_not_even':
 forall n, (even n /\ ~ even (S n))  \/ (~ even n /\ even (S n)).
Proof.
  induction n.
  left; split.
  constructor.
  intros H0; inv H0.
  intuition.
Qed.

Lemma even_or_not_even:
 forall n, even n \/ ~ even n.
Proof.
  intros n; elim even_or_not_even' with n; intuition.
Qed.