diff options
Diffstat (limited to 'theories/Arith/Even.v')
| -rw-r--r-- | theories/Arith/Even.v | 387 |
1 files changed, 198 insertions, 189 deletions
diff --git a/theories/Arith/Even.v b/theories/Arith/Even.v index cdbc86df..83c0ce17 100644 --- a/theories/Arith/Even.v +++ b/theories/Arith/Even.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Even.v 5920 2004-07-16 20:01:26Z herbelin $ i*) +(*i $Id: Even.v 9245 2006-10-17 12:53:34Z notin $ i*) (** Here we define the predicates [even] and [odd] by mutual induction and we prove the decidability and the exclusion of those predicates. @@ -16,6 +16,9 @@ Open Local Scope nat_scope. Implicit Types m n : nat. + +(** * Definition of [even] and [odd], and basic facts *) + Inductive even : nat -> Prop := | even_O : even 0 | even_S : forall n, odd n -> even (S n) @@ -27,279 +30,285 @@ Hint Constructors odd: arith. Lemma even_or_odd : forall n, even n \/ odd n. Proof. -induction n. -auto with arith. -elim IHn; auto with arith. + induction n. + auto with arith. + elim IHn; auto with arith. Qed. Lemma even_odd_dec : forall n, {even n} + {odd n}. Proof. -induction n. -auto with arith. -elim IHn; auto with arith. + induction n. + auto with arith. + elim IHn; auto with arith. Qed. Lemma not_even_and_odd : forall n, even n -> odd n -> False. Proof. -induction n. -intros. inversion H0. -intros. inversion H. inversion H0. auto with arith. + induction n. + intros even_0 odd_0. inversion odd_0. + intros even_Sn odd_Sn. inversion even_Sn. inversion odd_Sn. auto with arith. Qed. + +(** * Facts about [even] & [odd] wrt. [plus] *) + Lemma even_plus_aux : - forall n m, - (odd (n + m) <-> odd n /\ even m \/ even n /\ odd m) /\ - (even (n + m) <-> even n /\ even m \/ odd n /\ odd m). + forall n m, + (odd (n + m) <-> odd n /\ even m \/ even n /\ odd m) /\ + (even (n + m) <-> even n /\ even m \/ odd n /\ odd m). Proof. -intros n; elim n; simpl in |- *; auto with arith. -intros m; split; auto. -split. -intros H; right; split; auto with arith. -intros H'; case H'; auto with arith. -intros H'0; elim H'0; intros H'1 H'2; inversion H'1. -intros H; elim H; auto. -split; auto with arith. -intros H'; elim H'; auto with arith. -intros H; elim H; auto. -intros H'0; elim H'0; intros H'1 H'2; inversion H'1. -intros n0 H' m; elim (H' m); intros H'1 H'2; elim H'1; intros E1 E2; elim H'2; - intros E3 E4; clear H'1 H'2. -split; split. -intros H'0; case E3. -inversion H'0; auto. -intros H; elim H; intros H0 H1; clear H; auto with arith. -intros H; elim H; intros H0 H1; clear H; auto with arith. -intros H'0; case H'0; intros C0; case C0; intros C1 C2. -apply odd_S. -apply E4; left; split; auto with arith. -inversion C1; auto. -apply odd_S. -apply E4; right; split; auto with arith. -inversion C1; auto. -intros H'0. -case E1. -inversion H'0; auto. -intros H; elim H; intros H0 H1; clear H; auto with arith. -intros H; elim H; intros H0 H1; clear H; auto with arith. -intros H'0; case H'0; intros C0; case C0; intros C1 C2. -apply even_S. -apply E2; left; split; auto with arith. -inversion C1; auto. -apply even_S. -apply E2; right; split; auto with arith. -inversion C1; auto. + intros n; elim n; simpl in |- *; auto with arith. + intros m; split; auto. + split. + intros H; right; split; auto with arith. + intros H'; case H'; auto with arith. + intros H'0; elim H'0; intros H'1 H'2; inversion H'1. + intros H; elim H; auto. + split; auto with arith. + intros H'; elim H'; auto with arith. + intros H; elim H; auto. + intros H'0; elim H'0; intros H'1 H'2; inversion H'1. + intros n0 H' m; elim (H' m); intros H'1 H'2; elim H'1; intros E1 E2; elim H'2; + intros E3 E4; clear H'1 H'2. + split; split. + intros H'0; case E3. + inversion H'0; auto. + intros H; elim H; intros H0 H1; clear H; auto with arith. + intros H; elim H; intros H0 H1; clear H; auto with arith. + intros H'0; case H'0; intros C0; case C0; intros C1 C2. + apply odd_S. + apply E4; left; split; auto with arith. + inversion C1; auto. + apply odd_S. + apply E4; right; split; auto with arith. + inversion C1; auto. + intros H'0. + case E1. + inversion H'0; auto. + intros H; elim H; intros H0 H1; clear H; auto with arith. + intros H; elim H; intros H0 H1; clear H; auto with arith. + intros H'0; case H'0; intros C0; case C0; intros C1 C2. + apply even_S. + apply E2; left; split; auto with arith. + inversion C1; auto. + apply even_S. + apply E2; right; split; auto with arith. + inversion C1; auto. Qed. Lemma even_even_plus : forall n m, even n -> even m -> even (n + m). Proof. -intros n m; case (even_plus_aux n m). -intros H H0; case H0; auto. + intros n m; case (even_plus_aux n m). + intros H H0; case H0; auto. Qed. Lemma odd_even_plus : forall n m, odd n -> odd m -> even (n + m). Proof. -intros n m; case (even_plus_aux n m). -intros H H0; case H0; auto. + intros n m; case (even_plus_aux n m). + intros H H0; case H0; auto. Qed. - + Lemma even_plus_even_inv_r : forall n m, even (n + m) -> even n -> even m. Proof. -intros n m H; case (even_plus_aux n m). -intros H' H'0; elim H'0. -intros H'1; case H'1; auto. -intros H0; elim H0; auto. -intros H0 H1 H2; case (not_even_and_odd n); auto. -case H0; auto. + intros n m H; case (even_plus_aux n m). + intros H' H'0; elim H'0. + intros H'1; case H'1; auto. + intros H0; elim H0; auto. + intros H0 H1 H2; case (not_even_and_odd n); auto. + case H0; auto. Qed. Lemma even_plus_even_inv_l : forall n m, even (n + m) -> even m -> even n. Proof. -intros n m H; case (even_plus_aux n m). -intros H' H'0; elim H'0. -intros H'1; case H'1; auto. -intros H0; elim H0; auto. -intros H0 H1 H2; case (not_even_and_odd m); auto. -case H0; auto. + intros n m H; case (even_plus_aux n m). + intros H' H'0; elim H'0. + intros H'1; case H'1; auto. + intros H0; elim H0; auto. + intros H0 H1 H2; case (not_even_and_odd m); auto. + case H0; auto. Qed. - + Lemma even_plus_odd_inv_r : forall n m, even (n + m) -> odd n -> odd m. Proof. -intros n m H; case (even_plus_aux n m). -intros H' H'0; elim H'0. -intros H'1; case H'1; auto. -intros H0 H1 H2; case (not_even_and_odd n); auto. -case H0; auto. -intros H0; case H0; auto. + intros n m H; case (even_plus_aux n m). + intros H' H'0; elim H'0. + intros H'1; case H'1; auto. + intros H0 H1 H2; case (not_even_and_odd n); auto. + case H0; auto. + intros H0; case H0; auto. Qed. - + Lemma even_plus_odd_inv_l : forall n m, even (n + m) -> odd m -> odd n. Proof. -intros n m H; case (even_plus_aux n m). -intros H' H'0; elim H'0. -intros H'1; case H'1; auto. -intros H0 H1 H2; case (not_even_and_odd m); auto. -case H0; auto. -intros H0; case H0; auto. + intros n m H; case (even_plus_aux n m). + intros H' H'0; elim H'0. + intros H'1; case H'1; auto. + intros H0 H1 H2; case (not_even_and_odd m); auto. + case H0; auto. + intros H0; case H0; auto. Qed. Hint Resolve even_even_plus odd_even_plus: arith. - + Lemma odd_plus_l : forall n m, odd n -> even m -> odd (n + m). Proof. -intros n m; case (even_plus_aux n m). -intros H; case H; auto. + intros n m; case (even_plus_aux n m). + intros H; case H; auto. Qed. Lemma odd_plus_r : forall n m, even n -> odd m -> odd (n + m). Proof. -intros n m; case (even_plus_aux n m). -intros H; case H; auto. + intros n m; case (even_plus_aux n m). + intros H; case H; auto. Qed. Lemma odd_plus_even_inv_l : forall n m, odd (n + m) -> odd m -> even n. Proof. -intros n m H; case (even_plus_aux n m). -intros H' H'0; elim H'. -intros H'1; case H'1; auto. -intros H0 H1 H2; case (not_even_and_odd m); auto. -case H0; auto. -intros H0; case H0; auto. + intros n m H; case (even_plus_aux n m). + intros H' H'0; elim H'. + intros H'1; case H'1; auto. + intros H0 H1 H2; case (not_even_and_odd m); auto. + case H0; auto. + intros H0; case H0; auto. Qed. Lemma odd_plus_even_inv_r : forall n m, odd (n + m) -> odd n -> even m. Proof. -intros n m H; case (even_plus_aux n m). -intros H' H'0; elim H'. -intros H'1; case H'1; auto. -intros H0; case H0; auto. -intros H0 H1 H2; case (not_even_and_odd n); auto. -case H0; auto. + intros n m H; case (even_plus_aux n m). + intros H' H'0; elim H'. + intros H'1; case H'1; auto. + intros H0; case H0; auto. + intros H0 H1 H2; case (not_even_and_odd n); auto. + case H0; auto. Qed. Lemma odd_plus_odd_inv_l : forall n m, odd (n + m) -> even m -> odd n. Proof. -intros n m H; case (even_plus_aux n m). -intros H' H'0; elim H'. -intros H'1; case H'1; auto. -intros H0; case H0; auto. -intros H0 H1 H2; case (not_even_and_odd m); auto. -case H0; auto. + intros n m H; case (even_plus_aux n m). + intros H' H'0; elim H'. + intros H'1; case H'1; auto. + intros H0; case H0; auto. + intros H0 H1 H2; case (not_even_and_odd m); auto. + case H0; auto. Qed. - + Lemma odd_plus_odd_inv_r : forall n m, odd (n + m) -> even n -> odd m. Proof. -intros n m H; case (even_plus_aux n m). -intros H' H'0; elim H'. -intros H'1; case H'1; auto. -intros H0 H1 H2; case (not_even_and_odd n); auto. -case H0; auto. -intros H0; case H0; auto. + intros n m H; case (even_plus_aux n m). + intros H' H'0; elim H'. + intros H'1; case H'1; auto. + intros H0 H1 H2; case (not_even_and_odd n); auto. + case H0; auto. + intros H0; case H0; auto. Qed. Hint Resolve odd_plus_l odd_plus_r: arith. - + + +(** * Facts about [even] and [odd] wrt. [mult] *) + Lemma even_mult_aux : - forall n m, - (odd (n * m) <-> odd n /\ odd m) /\ (even (n * m) <-> even n \/ even m). + forall n m, + (odd (n * m) <-> odd n /\ odd m) /\ (even (n * m) <-> even n \/ even m). Proof. -intros n; elim n; simpl in |- *; auto with arith. -intros m; split; split; auto with arith. -intros H'; inversion H'. -intros H'; elim H'; auto. -intros n0 H' m; split; split; auto with arith. -intros H'0. -elim (even_plus_aux m (n0 * m)); intros H'3 H'4; case H'3; intros H'1 H'2; - case H'1; auto. -intros H'5; elim H'5; intros H'6 H'7; auto with arith. -split; auto with arith. -case (H' m). -intros H'8 H'9; case H'9. -intros H'10; case H'10; auto with arith. -intros H'11 H'12; case (not_even_and_odd m); auto with arith. -intros H'5; elim H'5; intros H'6 H'7; case (not_even_and_odd (n0 * m)); auto. -case (H' m). -intros H'8 H'9; case H'9; auto. -intros H'0; elim H'0; intros H'1 H'2; clear H'0. -elim (even_plus_aux m (n0 * m)); auto. -intros H'0 H'3. -elim H'0. -intros H'4 H'5; apply H'5; auto. -left; split; auto with arith. -case (H' m). -intros H'6 H'7; elim H'7. -intros H'8 H'9; apply H'9. -left. -inversion H'1; auto. -intros H'0. -elim (even_plus_aux m (n0 * m)); intros H'3 H'4; case H'4. -intros H'1 H'2. -elim H'1; auto. -intros H; case H; auto. -intros H'5; elim H'5; intros H'6 H'7; auto with arith. -left. -case (H' m). -intros H'8; elim H'8. -intros H'9; elim H'9; auto with arith. -intros H'0; elim H'0; intros H'1. -case (even_or_odd m); intros H'2. -apply even_even_plus; auto. -case (H' m). -intros H H0; case H0; auto. -apply odd_even_plus; auto. -inversion H'1; case (H' m); auto. -intros H1; case H1; auto. -apply even_even_plus; auto. -case (H' m). -intros H H0; case H0; auto. + intros n; elim n; simpl in |- *; auto with arith. + intros m; split; split; auto with arith. + intros H'; inversion H'. + intros H'; elim H'; auto. + intros n0 H' m; split; split; auto with arith. + intros H'0. + elim (even_plus_aux m (n0 * m)); intros H'3 H'4; case H'3; intros H'1 H'2; + case H'1; auto. + intros H'5; elim H'5; intros H'6 H'7; auto with arith. + split; auto with arith. + case (H' m). + intros H'8 H'9; case H'9. + intros H'10; case H'10; auto with arith. + intros H'11 H'12; case (not_even_and_odd m); auto with arith. + intros H'5; elim H'5; intros H'6 H'7; case (not_even_and_odd (n0 * m)); auto. + case (H' m). + intros H'8 H'9; case H'9; auto. + intros H'0; elim H'0; intros H'1 H'2; clear H'0. + elim (even_plus_aux m (n0 * m)); auto. + intros H'0 H'3. + elim H'0. + intros H'4 H'5; apply H'5; auto. + left; split; auto with arith. + case (H' m). + intros H'6 H'7; elim H'7. + intros H'8 H'9; apply H'9. + left. + inversion H'1; auto. + intros H'0. + elim (even_plus_aux m (n0 * m)); intros H'3 H'4; case H'4. + intros H'1 H'2. + elim H'1; auto. + intros H; case H; auto. + intros H'5; elim H'5; intros H'6 H'7; auto with arith. + left. + case (H' m). + intros H'8; elim H'8. + intros H'9; elim H'9; auto with arith. + intros H'0; elim H'0; intros H'1. + case (even_or_odd m); intros H'2. + apply even_even_plus; auto. + case (H' m). + intros H H0; case H0; auto. + apply odd_even_plus; auto. + inversion H'1; case (H' m); auto. + intros H1; case H1; auto. + apply even_even_plus; auto. + case (H' m). + intros H H0; case H0; auto. Qed. - + Lemma even_mult_l : forall n m, even n -> even (n * m). Proof. -intros n m; case (even_mult_aux n m); auto. -intros H H0; case H0; auto. + intros n m; case (even_mult_aux n m); auto. + intros H H0; case H0; auto. Qed. Lemma even_mult_r : forall n m, even m -> even (n * m). Proof. -intros n m; case (even_mult_aux n m); auto. -intros H H0; case H0; auto. + intros n m; case (even_mult_aux n m); auto. + intros H H0; case H0; auto. Qed. Hint Resolve even_mult_l even_mult_r: arith. - + Lemma even_mult_inv_r : forall n m, even (n * m) -> odd n -> even m. Proof. -intros n m H' H'0. -case (even_mult_aux n m). -intros H'1 H'2; elim H'2. -intros H'3; elim H'3; auto. -intros H; case (not_even_and_odd n); auto. + intros n m H' H'0. + case (even_mult_aux n m). + intros H'1 H'2; elim H'2. + intros H'3; elim H'3; auto. + intros H; case (not_even_and_odd n); auto. Qed. Lemma even_mult_inv_l : forall n m, even (n * m) -> odd m -> even n. Proof. -intros n m H' H'0. -case (even_mult_aux n m). -intros H'1 H'2; elim H'2. -intros H'3; elim H'3; auto. -intros H; case (not_even_and_odd m); auto. + intros n m H' H'0. + case (even_mult_aux n m). + intros H'1 H'2; elim H'2. + intros H'3; elim H'3; auto. + intros H; case (not_even_and_odd m); auto. Qed. Lemma odd_mult : forall n m, odd n -> odd m -> odd (n * m). Proof. -intros n m; case (even_mult_aux n m); intros H; case H; auto. + intros n m; case (even_mult_aux n m); intros H; case H; auto. Qed. Hint Resolve even_mult_l even_mult_r odd_mult: arith. Lemma odd_mult_inv_l : forall n m, odd (n * m) -> odd n. Proof. -intros n m H'. -case (even_mult_aux n m). -intros H'1 H'2; elim H'1. -intros H'3; elim H'3; auto. + intros n m H'. + case (even_mult_aux n m). + intros H'1 H'2; elim H'1. + intros H'3; elim H'3; auto. Qed. - + Lemma odd_mult_inv_r : forall n m, odd (n * m) -> odd m. Proof. -intros n m H'. -case (even_mult_aux n m). -intros H'1 H'2; elim H'1. -intros H'3; elim H'3; auto. + intros n m H'. + case (even_mult_aux n m). + intros H'1 H'2; elim H'1. + intros H'3; elim H'3; auto. Qed. |