From cfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sun, 1 Feb 2009 00:54:40 +0100 Subject: Imported Upstream version 8.2~rc2+dfsg --- theories/Arith/Div2.v | 64 +++++++++----------- theories/Arith/Even.v | 158 +++++++++++++++----------------------------------- theories/Arith/Max.v | 6 +- 3 files changed, 78 insertions(+), 150 deletions(-) (limited to 'theories/Arith') diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v index 1216a545..7cab976f 100644 --- a/theories/Arith/Div2.v +++ b/theories/Arith/Div2.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Div2.v 10625 2008-03-06 11:21:01Z notin $ i*) +(*i $Id: Div2.v 11735 2009-01-02 17:22:31Z herbelin $ i*) Require Import Lt. Require Import Plus. @@ -60,45 +60,38 @@ Hint Resolve lt_div2: arith. (** Properties related to the parity *) -Lemma even_odd_div2 : - forall n, - (even n <-> div2 n = div2 (S n)) /\ (odd n <-> S (div2 n) = div2 (S n)). +Lemma even_div2 : forall n, even n -> div2 n = div2 (S n) +with odd_div2 : forall n, odd n -> S (div2 n) = div2 (S n). Proof. - intro n. pattern n in |- *. apply ind_0_1_SS. - (* n = 0 *) - split. split; auto with arith. - split. intro H. inversion H. - intro H. absurd (S (div2 0) = div2 1); auto with arith. - (* n = 1 *) - split. split. intro. inversion H. inversion H1. - intro H. absurd (div2 1 = div2 2). - simpl in |- *. discriminate. assumption. - split; auto with arith. - (* n = (S (S n')) *) - intros. decompose [and] H. unfold iff in H0, H1. - decompose [and] H0. decompose [and] H1. clear H H0 H1. - split; split; auto with arith. - intro H. inversion H. inversion H1. - change (S (div2 n0) = S (div2 (S n0))) in |- *. auto with arith. - intro H. inversion H. inversion H1. - change (S (S (div2 n0)) = S (div2 (S n0))) in |- *. auto with arith. + destruct n; intro H. + (* 0 *) trivial. + (* S n *) inversion_clear H. apply odd_div2 in H0 as <-. trivial. + destruct n; intro. + (* 0 *) inversion H. + (* S n *) inversion_clear H. apply even_div2 in H0 as <-. trivial. Qed. -(** Specializations *) - -Lemma even_div2 : forall n, even n -> div2 n = div2 (S n). -Proof fun n => proj1 (proj1 (even_odd_div2 n)). +Lemma div2_even : forall n, div2 n = div2 (S n) -> even n +with div2_odd : forall n, S (div2 n) = div2 (S n) -> odd n. +Proof. + destruct n; intro H. + (* 0 *) constructor. + (* S n *) constructor. apply div2_odd. rewrite H. trivial. + destruct n; intro H. + (* 0 *) discriminate. + (* S n *) constructor. apply div2_even. injection H as <-. trivial. +Qed. -Lemma div2_even : forall n, div2 n = div2 (S n) -> even n. -Proof fun n => proj2 (proj1 (even_odd_div2 n)). +Hint Resolve even_div2 div2_even odd_div2 div2_odd: arith. -Lemma odd_div2 : forall n, odd n -> S (div2 n) = div2 (S n). -Proof fun n => proj1 (proj2 (even_odd_div2 n)). +Lemma even_odd_div2 : + forall n, + (even n <-> div2 n = div2 (S n)) /\ (odd n <-> S (div2 n) = div2 (S n)). +Proof. + auto decomp using div2_odd, div2_even, odd_div2, even_div2. +Qed. -Lemma div2_odd : forall n, S (div2 n) = div2 (S n) -> odd n. -Proof fun n => proj2 (proj2 (even_odd_div2 n)). -Hint Resolve even_div2 div2_even odd_div2 div2_odd: arith. (** Properties related to the double ([2n]) *) @@ -132,8 +125,7 @@ Proof. split; split; auto with arith. intro H. inversion H. inversion H1. (* n = (S (S n')) *) - intros. decompose [and] H. unfold iff in H0, H1. - decompose [and] H0. decompose [and] H1. clear H H0 H1. + intros. destruct H as ((IH1,IH2),(IH3,IH4)). split; split. intro H. inversion H. inversion H1. simpl in |- *. rewrite (double_S (div2 n0)). auto with arith. @@ -142,8 +134,6 @@ Proof. simpl in |- *. rewrite (double_S (div2 n0)). auto with arith. simpl in |- *. rewrite (double_S (div2 n0)). intro H. injection H. auto with arith. Qed. - - (** Specializations *) Lemma even_double : forall n, even n -> n = double (div2 n). diff --git a/theories/Arith/Even.v b/theories/Arith/Even.v index 1484666b..59209370 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 10410 2007-12-31 13:11:55Z msozeau $ i*) +(*i $Id: Even.v 11512 2008-10-27 12:28:36Z herbelin $ i*) (** Here we define the predicates [even] and [odd] by mutual induction and we prove the decidability and the exclusion of those predicates. @@ -52,153 +52,91 @@ 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). +Lemma even_plus_split : forall n m, + (even (n + m) -> even n /\ even m \/ odd n /\ odd m) +with odd_plus_split : forall n m, + odd (n + m) -> odd n /\ even m \/ even 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. clear even_plus_split. destruct n; simpl in *. + auto with arith. + inversion_clear H; + apply odd_plus_split in H0 as [(H0,?)|(H0,?)]; auto with arith. +intros. clear odd_plus_split. destruct n; simpl in *. + auto with arith. + inversion_clear H; + apply even_plus_split in H0 as [(H0,?)|(H0,?)]; auto with arith. Qed. - -Lemma even_even_plus : forall n m, even n -> even m -> even (n + m). + +Lemma even_even_plus : forall n m, even n -> even m -> even (n + m) +with 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 H0; case H0; auto. +intros n m [|] ?. trivial. apply even_S, odd_plus_l; trivial. +intros n m [] ?. apply odd_S, even_even_plus; trivial. Qed. - -Lemma odd_even_plus : forall n m, odd n -> odd m -> even (n + m). + +Lemma odd_plus_r : forall n m, even n -> odd m -> odd (n + m) +with 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 [|] ?. trivial. apply odd_S, odd_even_plus; trivial. +intros n m [] ?. apply even_S, odd_plus_r; trivial. +Qed. + +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). +Proof. +split; split; auto using odd_plus_split, even_plus_split. +intros [[]|[]]; auto using odd_plus_r, odd_plus_l. +intros [[]|[]]; auto using even_even_plus, odd_even_plus. 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; destruct (even_plus_split n m) as [[]|[]]; auto. + intro; destruct (not_even_and_odd n); 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; destruct (even_plus_split n m) as [[]|[]]; auto. + intro; destruct (not_even_and_odd m); 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; destruct (even_plus_split n m) as [[]|[]]; auto. + intro; destruct (not_even_and_odd n); 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; destruct (even_plus_split n m) as [[]|[]]; auto. + intro; destruct (not_even_and_odd m); 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. -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. -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; destruct (odd_plus_split n m) as [[]|[]]; auto. + intro; destruct (not_even_and_odd m); 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; destruct (odd_plus_split n m) as [[]|[]]; auto. + intro; destruct (not_even_and_odd n); 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; destruct (odd_plus_split n m) as [[]|[]]; auto. + intro; destruct (not_even_and_odd m); 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; destruct (odd_plus_split n m) as [[]|[]]; auto. + intro; destruct (not_even_and_odd n); auto. Qed. Hint Resolve odd_plus_l odd_plus_r: arith. diff --git a/theories/Arith/Max.v b/theories/Arith/Max.v index 95af67f8..5de2298d 100644 --- a/theories/Arith/Max.v +++ b/theories/Arith/Max.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Max.v 9883 2007-06-07 18:44:59Z letouzey $ i*) +(*i $Id: Max.v 11735 2009-01-02 17:22:31Z herbelin $ i*) Require Import Le. @@ -74,13 +74,13 @@ Lemma max_dec : forall n m, {max n m = n} + {max n m = m}. Proof. induction n; induction m; simpl in |- *; auto with arith. elim (IHn m); intro H; elim H; auto. -Qed. +Defined. Lemma max_case : forall n m (P:nat -> Type), P n -> P m -> P (max n m). Proof. induction n; simpl in |- *; auto with arith. induction m; intros; simpl in |- *; auto with arith. pattern (max n m) in |- *; apply IHn; auto with arith. -Qed. +Defined. Notation max_case2 := max_case (only parsing). -- cgit v1.2.3