diff options
| -rw-r--r-- | theories/Arith/Max.v | 21 | ||||
| -rw-r--r-- | theories/Arith/Min.v | 15 | ||||
| -rw-r--r-- | theories/Arith/MinMax.v | 62 | ||||
| -rw-r--r-- | theories/Arith/vo.itarget | 1 | ||||
| -rw-r--r-- | theories/NArith/NArith.v | 6 | ||||
| -rw-r--r-- | theories/NArith/Nminmax.v | 87 | ||||
| -rw-r--r-- | theories/NArith/vo.itarget | 1 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZMaxMin.v | 179 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZProperties.v | 6 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NMaxMin.v | 135 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NProperties.v | 6 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NSub.v | 11 | ||||
| -rw-r--r-- | theories/Numbers/Natural/BigN/NMake.v | 8 | ||||
| -rw-r--r-- | theories/Numbers/vo.itarget | 2 | ||||
| -rw-r--r-- | theories/ZArith/ZArith.v | 2 | ||||
| -rw-r--r-- | theories/ZArith/ZArith_base.v | 2 | ||||
| -rw-r--r-- | theories/ZArith/Zdiv.v | 2 | ||||
| -rw-r--r-- | theories/ZArith/Zmax.v | 37 | ||||
| -rw-r--r-- | theories/ZArith/Zmin.v | 27 | ||||
| -rw-r--r-- | theories/ZArith/Zminmax.v | 130 |
20 files changed, 404 insertions, 336 deletions
diff --git a/theories/Arith/Max.v b/theories/Arith/Max.v index e49251a71..036b47ba2 100644 --- a/theories/Arith/Max.v +++ b/theories/Arith/Max.v @@ -8,21 +8,20 @@ (*i $Id$ i*) -(** THIS FILE IS DEPRECATED. Use [NPeano] and [MinMax] instead. *) +(** THIS FILE IS DEPRECATED. Use [NPeano.Nat] instead. *) Require Import NPeano. -Require Export MinMax. Local Open Scope nat_scope. Implicit Types m n p : nat. Notation max := NPeano.max (only parsing). -Definition max_0_l := max_0_l. -Definition max_0_r := max_0_r. -Definition succ_max_distr := succ_max_distr. -Definition plus_max_distr_l := plus_max_distr_l. -Definition plus_max_distr_r := plus_max_distr_r. +Definition max_0_l := Nat.max_0_l. +Definition max_0_r := Nat.max_0_r. +Definition succ_max_distr := Nat.succ_max_distr. +Definition plus_max_distr_l := Nat.add_max_distr_l. +Definition plus_max_distr_r := Nat.add_max_distr_r. Definition max_case_strong := Nat.max_case_strong. Definition max_spec := Nat.max_spec. Definition max_dec := Nat.max_dec. @@ -41,5 +40,11 @@ Definition max_lub := Nat.max_lub. (* begin hide *) (* Compatibility *) Notation max_case2 := max_case (only parsing). -Notation max_SS := succ_max_distr (only parsing). +Notation max_SS := Nat.succ_max_distr (only parsing). (* end hide *) + +Hint Resolve + Nat.max_l Nat.max_r Nat.le_max_l Nat.le_max_r : arith v62. + +Hint Resolve + Nat.min_l Nat.min_r Nat.le_min_l Nat.le_min_r : arith v62. diff --git a/theories/Arith/Min.v b/theories/Arith/Min.v index 44060b56c..521285a08 100644 --- a/theories/Arith/Min.v +++ b/theories/Arith/Min.v @@ -8,21 +8,20 @@ (*i $Id$ i*) -(** THIS FILE IS DEPRECATED. Use [NPeano] and [MinMax] instead. *) +(** THIS FILE IS DEPRECATED. Use [NPeano.Nat] instead. *) Require Import NPeano. -Require Export MinMax. Open Local Scope nat_scope. Implicit Types m n p : nat. Notation min := NPeano.min (only parsing). -Definition min_0_l := min_0_l. -Definition min_0_r := min_0_r. -Definition succ_min_distr := succ_min_distr. -Definition plus_min_distr_l := plus_min_distr_l. -Definition plus_min_distr_r := plus_min_distr_r. +Definition min_0_l := Nat.min_0_l. +Definition min_0_r := Nat.min_0_r. +Definition succ_min_distr := Nat.succ_min_distr. +Definition plus_min_distr_l := Nat.add_min_distr_l. +Definition plus_min_distr_r := Nat.add_min_distr_r. Definition min_case_strong := Nat.min_case_strong. Definition min_spec := Nat.min_spec. Definition min_dec := Nat.min_dec. @@ -41,5 +40,5 @@ Definition min_glb := Nat.min_glb. (* begin hide *) (* Compatibility *) Notation min_case2 := min_case (only parsing). -Notation min_SS := succ_min_distr (only parsing). +Notation min_SS := Nat.succ_min_distr (only parsing). (* end hide *)
\ No newline at end of file diff --git a/theories/Arith/MinMax.v b/theories/Arith/MinMax.v deleted file mode 100644 index 9ce43ab8c..000000000 --- a/theories/Arith/MinMax.v +++ /dev/null @@ -1,62 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -Require Import Orders NPeano. - -(** The Definition of maximum and minimum of two natural numbers - is now in NPeano, as well as generic properties. *) - -(** * Properties specific to the [nat] domain *) - -(** Simplifications *) - -Lemma max_0_l : forall n, max 0 n = n. -Proof. reflexivity. Qed. - -Lemma max_0_r : forall n, max n 0 = n. -Proof. destruct n; auto. Qed. - -Lemma min_0_l : forall n, min 0 n = 0. -Proof. reflexivity. Qed. - -Lemma min_0_r : forall n, min n 0 = 0. -Proof. destruct n; auto. Qed. - -(** Compatibilities (consequences of monotonicity) *) - -Lemma succ_max_distr : forall n m, S (max n m) = max (S n) (S m). -Proof. auto. Qed. - -Lemma succ_min_distr : forall n m, S (min n m) = min (S n) (S m). -Proof. auto. Qed. - -Lemma plus_max_distr_l : forall n m p, max (p + n) (p + m) = p + max n m. -Proof. -intros. apply Nat.max_monotone. repeat red; auto with arith. -Qed. - -Lemma plus_max_distr_r : forall n m p, max (n + p) (m + p) = max n m + p. -Proof. -intros. apply Nat.max_monotone with (f:=fun x => x + p). -repeat red; auto with arith. -Qed. - -Lemma plus_min_distr_l : forall n m p, min (p + n) (p + m) = p + min n m. -Proof. -intros. apply Nat.min_monotone. repeat red; auto with arith. -Qed. - -Lemma plus_min_distr_r : forall n m p, min (n + p) (m + p) = min n m + p. -Proof. -intros. apply Nat.min_monotone with (f:=fun x => x + p). -repeat red; auto with arith. -Qed. - -Hint Resolve - Nat.max_l Nat.max_r Nat.le_max_l Nat.le_max_r - Nat.min_l Nat.min_r Nat.le_min_l Nat.le_min_r : arith v62. diff --git a/theories/Arith/vo.itarget b/theories/Arith/vo.itarget index d8bff0ab9..0b6564e15 100644 --- a/theories/Arith/vo.itarget +++ b/theories/Arith/vo.itarget @@ -19,4 +19,3 @@ Mult.vo Peano_dec.vo Plus.vo Wf_nat.vo -MinMax.vo diff --git a/theories/NArith/NArith.v b/theories/NArith/NArith.v index 3a87880ac..0d936ae83 100644 --- a/theories/NArith/NArith.v +++ b/theories/NArith/NArith.v @@ -15,9 +15,11 @@ Require Export BinNat. Require Export Nnat. Require Export Ndigits. Require Export NArithRing. -Require NBinary Nminmax. +Require NBinary. -Module N := NBinary.N <+ Nminmax.Nextend. +Module N. + Include NBinary.N. +End N. (** [N] contains An [order] tactic for natural numbers *) diff --git a/theories/NArith/Nminmax.v b/theories/NArith/Nminmax.v deleted file mode 100644 index 53c7ecae7..000000000 --- a/theories/NArith/Nminmax.v +++ /dev/null @@ -1,87 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -Require Import Orders BinNat Nnat NBinary. - -(** * Maximum and Minimum of two [N] numbers *) - -Local Open Scope N_scope. - -(** Generic properties of min and max are already in [NBinary.N]. - We add here the ones specific to N. *) - -Module Type Nextend (N:NBinary.N). - -(** Simplifications *) - -Lemma max_0_l : forall n, Nmax 0 n = n. -Proof. - intros. unfold Nmax. rewrite <- Ncompare_antisym. generalize (Ncompare_0 n). - destruct (n ?= 0); intuition. -Qed. - -Lemma max_0_r : forall n, Nmax n 0 = n. -Proof. intros. rewrite N.max_comm. apply max_0_l. Qed. - -Lemma min_0_l : forall n, Nmin 0 n = 0. -Proof. - intros. unfold Nmin. rewrite <- Ncompare_antisym. generalize (Ncompare_0 n). - destruct (n ?= 0); intuition. -Qed. - -Lemma min_0_r : forall n, Nmin n 0 = 0. -Proof. intros. rewrite N.min_comm. apply min_0_l. Qed. - -(** Compatibilities (consequences of monotonicity) *) - -Lemma succ_max_distr : - forall n m, Nsucc (Nmax n m) = Nmax (Nsucc n) (Nsucc m). -Proof. - intros. symmetry. apply N.max_monotone. - intros x x'. unfold Nle. - rewrite 2 nat_of_Ncompare, 2 nat_of_Nsucc. - simpl; auto. -Qed. - -Lemma succ_min_distr : forall n m, Nsucc (Nmin n m) = Nmin (Nsucc n) (Nsucc m). -Proof. - intros. symmetry. apply N.min_monotone. - intros x x'. unfold Nle. - rewrite 2 nat_of_Ncompare, 2 nat_of_Nsucc. - simpl; auto. -Qed. - -Lemma add_max_distr_l : forall n m p, Nmax (p + n) (p + m) = p + Nmax n m. -Proof. - intros. apply N.max_monotone. - intros x x'. unfold Nle. - rewrite 2 nat_of_Ncompare, 2 nat_of_Nplus. - rewrite <- 2 Compare_dec.nat_compare_le. auto with arith. -Qed. - -Lemma add_max_distr_r : forall n m p, Nmax (n + p) (m + p) = Nmax n m + p. -Proof. - intros. rewrite (N.add_comm n p), (N.add_comm m p), (N.add_comm _ p). - apply add_max_distr_l. -Qed. - -Lemma add_min_distr_l : forall n m p, Nmin (p + n) (p + m) = p + Nmin n m. -Proof. - intros. apply N.min_monotone. - intros x x'. unfold Nle. - rewrite 2 nat_of_Ncompare, 2 nat_of_Nplus. - rewrite <- 2 Compare_dec.nat_compare_le. auto with arith. -Qed. - -Lemma add_min_distr_r : forall n m p, Nmin (n + p) (m + p) = Nmin n m + p. -Proof. - intros. rewrite (N.add_comm n p), (N.add_comm m p), (N.add_comm _ p). - apply add_min_distr_l. -Qed. - -End Nextend.
\ No newline at end of file diff --git a/theories/NArith/vo.itarget b/theories/NArith/vo.itarget index 17ac948b0..b80d4d7c8 100644 --- a/theories/NArith/vo.itarget +++ b/theories/NArith/vo.itarget @@ -8,4 +8,3 @@ Nnat.vo Pnat.vo POrderedType.vo Pminmax.vo -Nminmax.vo diff --git a/theories/Numbers/Integer/Abstract/ZMaxMin.v b/theories/Numbers/Integer/Abstract/ZMaxMin.v new file mode 100644 index 000000000..93b7966b0 --- /dev/null +++ b/theories/Numbers/Integer/Abstract/ZMaxMin.v @@ -0,0 +1,179 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +Require Import ZAxioms ZMulOrder GenericMinMax. + +(** * Properties of minimum and maximum specific to integer numbers *) + +Module Type ZMaxMinProp (Import Z : ZAxiomsSig'). +Include ZMulOrderPropFunct Z. + +(** The following results are concrete instances of [max_monotone] + and similar lemmas. *) + +(** Succ *) + +Lemma succ_max_distr : forall n m, S (max n m) == max (S n) (S m). +Proof. + intros. destruct (le_ge_cases n m); + [rewrite 2 max_r | rewrite 2 max_l]; now rewrite <- ?succ_le_mono. +Qed. + +Lemma succ_min_distr : forall n m, S (min n m) == min (S n) (S m). +Proof. + intros. destruct (le_ge_cases n m); + [rewrite 2 min_l | rewrite 2 min_r]; now rewrite <- ?succ_le_mono. +Qed. + +(** Pred *) + +Lemma pred_max_distr : forall n m, P (max n m) == max (P n) (P m). +Proof. + intros. destruct (le_ge_cases n m); + [rewrite 2 max_r | rewrite 2 max_l]; now rewrite <- ?pred_le_mono. +Qed. + +Lemma pred_min_distr : forall n m, P (min n m) == min (P n) (P m). +Proof. + intros. destruct (le_ge_cases n m); + [rewrite 2 min_l | rewrite 2 min_r]; now rewrite <- ?pred_le_mono. +Qed. + +(** Add *) + +Lemma add_max_distr_l : forall n m p, max (p + n) (p + m) == p + max n m. +Proof. + intros. destruct (le_ge_cases n m); + [rewrite 2 max_r | rewrite 2 max_l]; now rewrite <- ?add_le_mono_l. +Qed. + +Lemma add_max_distr_r : forall n m p, max (n + p) (m + p) == max n m + p. +Proof. + intros. destruct (le_ge_cases n m); + [rewrite 2 max_r | rewrite 2 max_l]; now rewrite <- ?add_le_mono_r. +Qed. + +Lemma add_min_distr_l : forall n m p, min (p + n) (p + m) == p + min n m. +Proof. + intros. destruct (le_ge_cases n m); + [rewrite 2 min_l | rewrite 2 min_r]; now rewrite <- ?add_le_mono_l. +Qed. + +Lemma add_min_distr_r : forall n m p, min (n + p) (m + p) == min n m + p. +Proof. + intros. destruct (le_ge_cases n m); + [rewrite 2 min_l | rewrite 2 min_r]; now rewrite <- ?add_le_mono_r. +Qed. + +(** Opp *) + +Lemma opp_max_distr : forall n m, -(max n m) == min (-n) (-m). +Proof. + intros. destruct (le_ge_cases n m). + rewrite max_r by trivial. symmetry. apply min_r. now rewrite <- opp_le_mono. + rewrite max_l by trivial. symmetry. apply min_l. now rewrite <- opp_le_mono. +Qed. + +Lemma opp_min_distr : forall n m, -(min n m) == max (-n) (-m). +Proof. + intros. destruct (le_ge_cases n m). + rewrite min_l by trivial. symmetry. apply max_l. now rewrite <- opp_le_mono. + rewrite min_r by trivial. symmetry. apply max_r. now rewrite <- opp_le_mono. +Qed. + +(** Sub *) + +Lemma sub_max_distr_l : forall n m p, max (p - n) (p - m) == p - min n m. +Proof. + intros. destruct (le_ge_cases n m). + rewrite min_l by trivial. apply max_l. now rewrite <- sub_le_mono_l. + rewrite min_r by trivial. apply max_r. now rewrite <- sub_le_mono_l. +Qed. + +Lemma sub_max_distr_r : forall n m p, max (n - p) (m - p) == max n m - p. +Proof. + intros. destruct (le_ge_cases n m); + [rewrite 2 max_r | rewrite 2 max_l]; try order; now apply sub_le_mono_r. +Qed. + +Lemma sub_min_distr_l : forall n m p, min (p - n) (p - m) == p - max n m. +Proof. + intros. destruct (le_ge_cases n m). + rewrite max_r by trivial. apply min_r. now rewrite <- sub_le_mono_l. + rewrite max_l by trivial. apply min_l. now rewrite <- sub_le_mono_l. +Qed. + +Lemma sub_min_distr_r : forall n m p, min (n - p) (m - p) == min n m - p. +Proof. + intros. destruct (le_ge_cases n m); + [rewrite 2 min_l | rewrite 2 min_r]; try order; now apply sub_le_mono_r. +Qed. + +(** Mul *) + +Lemma mul_max_distr_nonneg_l : forall n m p, 0 <= p -> + max (p * n) (p * m) == p * max n m. +Proof. + intros. destruct (le_ge_cases n m); + [rewrite 2 max_r | rewrite 2 max_l]; try order; now apply mul_le_mono_nonneg_l. +Qed. + +Lemma mul_max_distr_nonneg_r : forall n m p, 0 <= p -> + max (n * p) (m * p) == max n m * p. +Proof. + intros. destruct (le_ge_cases n m); + [rewrite 2 max_r | rewrite 2 max_l]; try order; now apply mul_le_mono_nonneg_r. +Qed. + +Lemma mul_min_distr_nonneg_l : forall n m p, 0 <= p -> + min (p * n) (p * m) == p * min n m. +Proof. + intros. destruct (le_ge_cases n m); + [rewrite 2 min_l | rewrite 2 min_r]; try order; now apply mul_le_mono_nonneg_l. +Qed. + +Lemma mul_min_distr_nonneg_r : forall n m p, 0 <= p -> + min (n * p) (m * p) == min n m * p. +Proof. + intros. destruct (le_ge_cases n m); + [rewrite 2 min_l | rewrite 2 min_r]; try order; now apply mul_le_mono_nonneg_r. +Qed. + +Lemma mul_max_distr_nonpos_l : forall n m p, p <= 0 -> + max (p * n) (p * m) == p * min n m. +Proof. + intros. destruct (le_ge_cases n m). + rewrite min_l by trivial. rewrite max_l. reflexivity. now apply mul_le_mono_nonpos_l. + rewrite min_r by trivial. rewrite max_r. reflexivity. now apply mul_le_mono_nonpos_l. +Qed. + +Lemma mul_max_distr_nonpos_r : forall n m p, p <= 0 -> + max (n * p) (m * p) == min n m * p. +Proof. + intros. destruct (le_ge_cases n m). + rewrite min_l by trivial. rewrite max_l. reflexivity. now apply mul_le_mono_nonpos_r. + rewrite min_r by trivial. rewrite max_r. reflexivity. now apply mul_le_mono_nonpos_r. +Qed. + +Lemma mul_min_distr_nonpos_l : forall n m p, p <= 0 -> + min (p * n) (p * m) == p * max n m. +Proof. + intros. destruct (le_ge_cases n m). + rewrite max_r by trivial. rewrite min_r. reflexivity. now apply mul_le_mono_nonpos_l. + rewrite max_l by trivial. rewrite min_l. reflexivity. now apply mul_le_mono_nonpos_l. +Qed. + +Lemma mul_min_distr_nonpos_r : forall n m p, p <= 0 -> + min (n * p) (m * p) == max n m * p. +Proof. + intros. destruct (le_ge_cases n m). + rewrite max_r by trivial. rewrite min_r. reflexivity. now apply mul_le_mono_nonpos_r. + rewrite max_l by trivial. rewrite min_l. reflexivity. now apply mul_le_mono_nonpos_r. +Qed. + +End ZMaxMinProp. diff --git a/theories/Numbers/Integer/Abstract/ZProperties.v b/theories/Numbers/Integer/Abstract/ZProperties.v index dc46eddab..45662d3b6 100644 --- a/theories/Numbers/Integer/Abstract/ZProperties.v +++ b/theories/Numbers/Integer/Abstract/ZProperties.v @@ -8,15 +8,15 @@ (*i $Id$ i*) -Require Export ZAxioms ZMulOrder ZSgnAbs. +Require Export ZAxioms ZMaxMin ZSgnAbs. (** This functor summarizes all known facts about Z. - For the moment it is only an alias to [ZMulOrderPropFunct], which + For the moment it is only an alias to the last functor which subsumes all others, plus properties of [sgn] and [abs]. *) Module Type ZPropSig (Z:ZAxiomsExtSig) := - ZMulOrderPropFunct Z <+ ZSgnAbsPropSig Z. + ZMaxMinProp Z <+ ZSgnAbsPropSig Z. Module ZPropFunct (Z:ZAxiomsExtSig) <: ZPropSig Z. Include ZPropSig Z. diff --git a/theories/Numbers/Natural/Abstract/NMaxMin.v b/theories/Numbers/Natural/Abstract/NMaxMin.v new file mode 100644 index 000000000..9406bce22 --- /dev/null +++ b/theories/Numbers/Natural/Abstract/NMaxMin.v @@ -0,0 +1,135 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +Require Import NAxioms NSub GenericMinMax. + +(** * Properties of minimum and maximum specific to natural numbers *) + +Module Type NMaxMinProp (Import N : NAxiomsSig'). +Include NSubPropFunct N. + +(** Zero *) + +Lemma max_0_l : forall n, max 0 n == n. +Proof. + intros. apply max_r. apply le_0_l. +Qed. + +Lemma max_0_r : forall n, max n 0 == n. +Proof. + intros. apply max_l. apply le_0_l. +Qed. + +Lemma min_0_l : forall n, min 0 n == 0. +Proof. + intros. apply min_l. apply le_0_l. +Qed. + +Lemma min_0_r : forall n, min n 0 == 0. +Proof. + intros. apply min_r. apply le_0_l. +Qed. + +(** The following results are concrete instances of [max_monotone] + and similar lemmas. *) + +(** Succ *) + +Lemma succ_max_distr : forall n m, S (max n m) == max (S n) (S m). +Proof. + intros. destruct (le_ge_cases n m); + [rewrite 2 max_r | rewrite 2 max_l]; now rewrite <- ?succ_le_mono. +Qed. + +Lemma succ_min_distr : forall n m, S (min n m) == min (S n) (S m). +Proof. + intros. destruct (le_ge_cases n m); + [rewrite 2 min_l | rewrite 2 min_r]; now rewrite <- ?succ_le_mono. +Qed. + +(** Add *) + +Lemma add_max_distr_l : forall n m p, max (p + n) (p + m) == p + max n m. +Proof. + intros. destruct (le_ge_cases n m); + [rewrite 2 max_r | rewrite 2 max_l]; now rewrite <- ?add_le_mono_l. +Qed. + +Lemma add_max_distr_r : forall n m p, max (n + p) (m + p) == max n m + p. +Proof. + intros. destruct (le_ge_cases n m); + [rewrite 2 max_r | rewrite 2 max_l]; now rewrite <- ?add_le_mono_r. +Qed. + +Lemma add_min_distr_l : forall n m p, min (p + n) (p + m) == p + min n m. +Proof. + intros. destruct (le_ge_cases n m); + [rewrite 2 min_l | rewrite 2 min_r]; now rewrite <- ?add_le_mono_l. +Qed. + +Lemma add_min_distr_r : forall n m p, min (n + p) (m + p) == min n m + p. +Proof. + intros. destruct (le_ge_cases n m); + [rewrite 2 min_l | rewrite 2 min_r]; now rewrite <- ?add_le_mono_r. +Qed. + +(** Mul *) + +Lemma mul_max_distr_l : forall n m p, max (p * n) (p * m) == p * max n m. +Proof. + intros. destruct (le_ge_cases n m); + [rewrite 2 max_r | rewrite 2 max_l]; try order; now apply mul_le_mono_l. +Qed. + +Lemma mul_max_distr_r : forall n m p, max (n * p) (m * p) == max n m * p. +Proof. + intros. destruct (le_ge_cases n m); + [rewrite 2 max_r | rewrite 2 max_l]; try order; now apply mul_le_mono_r. +Qed. + +Lemma mul_min_distr_l : forall n m p, min (p * n) (p * m) == p * min n m. +Proof. + intros. destruct (le_ge_cases n m); + [rewrite 2 min_l | rewrite 2 min_r]; try order; now apply mul_le_mono_l. +Qed. + +Lemma mul_min_distr_r : forall n m p, min (n * p) (m * p) == min n m * p. +Proof. + intros. destruct (le_ge_cases n m); + [rewrite 2 min_l | rewrite 2 min_r]; try order; now apply mul_le_mono_r. +Qed. + +(** Sub *) + +Lemma sub_max_distr_l : forall n m p, max (p - n) (p - m) == p - min n m. +Proof. + intros. destruct (le_ge_cases n m). + rewrite min_l by trivial. apply max_l. now apply sub_le_mono_l. + rewrite min_r by trivial. apply max_r. now apply sub_le_mono_l. +Qed. + +Lemma sub_max_distr_r : forall n m p, max (n - p) (m - p) == max n m - p. +Proof. + intros. destruct (le_ge_cases n m); + [rewrite 2 max_r | rewrite 2 max_l]; try order; now apply sub_le_mono_r. +Qed. + +Lemma sub_min_distr_l : forall n m p, min (p - n) (p - m) == p - max n m. +Proof. + intros. destruct (le_ge_cases n m). + rewrite max_r by trivial. apply min_r. now apply sub_le_mono_l. + rewrite max_l by trivial. apply min_l. now apply sub_le_mono_l. +Qed. + +Lemma sub_min_distr_r : forall n m p, min (n - p) (m - p) == min n m - p. +Proof. + intros. destruct (le_ge_cases n m); + [rewrite 2 min_l | rewrite 2 min_r]; try order; now apply sub_le_mono_r. +Qed. + +End NMaxMinProp. diff --git a/theories/Numbers/Natural/Abstract/NProperties.v b/theories/Numbers/Natural/Abstract/NProperties.v index 30262bd9f..9fc9b290e 100644 --- a/theories/Numbers/Natural/Abstract/NProperties.v +++ b/theories/Numbers/Natural/Abstract/NProperties.v @@ -8,14 +8,14 @@ (*i $Id$ i*) -Require Export NAxioms NSub. +Require Export NAxioms NMaxMin. (** This functor summarizes all known facts about N. - For the moment it is only an alias to [NSubPropFunct], which + For the moment it is only an alias to the last functor which subsumes all others. *) -Module Type NPropSig := NSubPropFunct. +Module Type NPropSig := NMaxMinProp. Module NPropFunct (N:NAxiomsSig) <: NPropSig N. Include NPropSig N. diff --git a/theories/Numbers/Natural/Abstract/NSub.v b/theories/Numbers/Natural/Abstract/NSub.v index de0c2da1b..1df032ea3 100644 --- a/theories/Numbers/Natural/Abstract/NSub.v +++ b/theories/Numbers/Natural/Abstract/NSub.v @@ -214,6 +214,17 @@ apply add_sub_eq_nz in EQ; [|order]. rewrite (add_lt_mono_r _ _ n), add_0_l in LT. order. Qed. +Lemma sub_le_mono_r : forall n m p, n <= m -> n-p <= m-p. +Proof. + intros. rewrite le_sub_le_add_r. transitivity m. assumption. apply sub_add_le. +Qed. + +Lemma sub_le_mono_l : forall n m p, n <= m -> p-m <= p-n. +Proof. + intros. rewrite le_sub_le_add_r. + transitivity (p-n+n); [ apply sub_add_le | now apply add_le_mono_l]. +Qed. + (** Sub and mul *) Theorem mul_pred_r : forall n m, n * (P m) == n * m - n. diff --git a/theories/Numbers/Natural/BigN/NMake.v b/theories/Numbers/Natural/BigN/NMake.v index b3f7befc8..e9b3d8cc8 100644 --- a/theories/Numbers/Natural/BigN/NMake.v +++ b/theories/Numbers/Natural/BigN/NMake.v @@ -807,13 +807,13 @@ Module Make (W0:CyclicType) <: NType. assert (H2 := ZnZ.spec_to_Z (ZnZ.zdigits (dom_op n))). assert (H3 := head0_zdigits n x). rewrite Zmod_small by auto with zarith. - rewrite (ZBinary.ZBinPropMod.mul_lt_mono_pos_l (2^(ZnZ.to_Z (ZnZ.head0 x)))); + rewrite (Z.mul_lt_mono_pos_l (2^(ZnZ.to_Z (ZnZ.head0 x)))); auto with zarith. - rewrite (ZBinary.ZBinPropMod.mul_le_mono_pos_l _ _ (2^(ZnZ.to_Z (ZnZ.head0 x)))); + rewrite (Z.mul_le_mono_pos_l _ _ (2^(ZnZ.to_Z (ZnZ.head0 x)))); auto with zarith. rewrite <- 2 Zpower_exp; auto with zarith. - rewrite ZBinary.ZBinPropMod.add_sub_assoc, Zplus_minus. - rewrite ZBinary.ZBinPropMod.sub_simpl_r, Zplus_minus. + rewrite Z.add_sub_assoc, Zplus_minus. + rewrite Z.sub_simpl_r, Zplus_minus. rewrite ZnZ.spec_zdigits. rewrite pow2_pos_minus_1 by (red; auto). apply ZnZ.spec_head0; auto with zarith. diff --git a/theories/Numbers/vo.itarget b/theories/Numbers/vo.itarget index 175a15e92..787eee55c 100644 --- a/theories/Numbers/vo.itarget +++ b/theories/Numbers/vo.itarget @@ -27,6 +27,7 @@ Integer/Abstract/ZProperties.vo Integer/Abstract/ZDivFloor.vo Integer/Abstract/ZDivTrunc.vo Integer/Abstract/ZDivEucl.vo +Integer/Abstract/ZMaxMin.vo Integer/BigZ/BigZ.vo Integer/BigZ/ZMake.vo Integer/Binary/ZBinary.vo @@ -56,6 +57,7 @@ Natural/Abstract/NStrongRec.vo Natural/Abstract/NSub.vo Natural/Abstract/NProperties.vo Natural/Abstract/NDiv.vo +Natural/Abstract/NMaxMin.vo Natural/BigN/BigN.vo Natural/BigN/Nbasic.vo Natural/BigN/NMake_gen.vo diff --git a/theories/ZArith/ZArith.v b/theories/ZArith/ZArith.v index a263ab379..7a68bd511 100644 --- a/theories/ZArith/ZArith.v +++ b/theories/ZArith/ZArith.v @@ -22,6 +22,6 @@ Require Export Zlogarithm. Export ZArithRing. -(** Final Z module, cumulating ZBinary.Z, Zminmax.Z, and Zdiv.Z *) +(** Final Z module, cumulating ZBinary.Z and Zdiv.Z *) Module Z := Zdiv.Z. diff --git a/theories/ZArith/ZArith_base.v b/theories/ZArith/ZArith_base.v index 1ce877b18..cd866c375 100644 --- a/theories/ZArith/ZArith_base.v +++ b/theories/ZArith/ZArith_base.v @@ -34,5 +34,3 @@ Hint Resolve Zle_refl Zplus_comm Zplus_assoc Zmult_comm Zmult_assoc Zplus_0_l Zmult_plus_distr_r: zarith. Require Export Zhints. - -Module Z := Zminmax.Z. diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v index 4477d559e..66e275b61 100644 --- a/theories/ZArith/Zdiv.v +++ b/theories/ZArith/Zdiv.v @@ -317,7 +317,7 @@ Module Z. Proof. intros; apply Z_mod_lt; auto with zarith. Qed. Definition mod_neg_bound := Z_mod_neg. - Include ZBinary.Z (* ideally: Zminmax.Z *) <+ ZDivFloor.ZDivPropFunct. + Include ZBinary.Z <+ ZDivFloor.ZDivPropFunct. End Z. diff --git a/theories/ZArith/Zmax.v b/theories/ZArith/Zmax.v index 84303a326..1d9b1f108 100644 --- a/theories/ZArith/Zmax.v +++ b/theories/ZArith/Zmax.v @@ -7,15 +7,13 @@ (************************************************************************) (*i $Id$ i*) -(** THIS FILE IS DEPRECATED. Use [Zminmax] instead. *) +(** THIS FILE IS DEPRECATED. Use [ZBinary.Z] instead. *) -Require Export BinInt Zcompare Zorder Zminmax. +Require Export BinInt Zcompare Zorder ZBinary. Open Local Scope Z_scope. -(** [Zmax] is now [BinInt.Zmax]. Code that do things like - [unfold Zmax.Zmax] will have to be adapted, and neither - a [Definition] or a [Notation] here can help much. *) +(** Definition [Zmax] is now [BinInt.Zmax]. *) (** * Characterization of maximum on binary integer numbers *) @@ -78,24 +76,35 @@ Definition Zsucc_max_distr : := Z.succ_max_distr. Definition Zplus_max_distr_l : forall n m p:Z, Zmax (p + n) (p + m) = p + Zmax n m - := Z.plus_max_distr_l. + := Z.add_max_distr_l. Definition Zplus_max_distr_r : forall n m p:Z, Zmax (n + p) (m + p) = Zmax n m + p - := Z.plus_max_distr_r. + := Z.add_max_distr_r. (** * Maximum and Zpos *) -Definition Zpos_max : forall p q, Zpos (Pmax p q) = Zmax (Zpos p) (Zpos q) - := Z.pos_max. +Lemma Zpos_max : forall p q, Zpos (Pmax p q) = Zmax (Zpos p) (Zpos q). +Proof. + intros; unfold Zmax, Pmax; simpl; generalize (Pcompare_Eq_eq p q). + destruct Pcompare; auto. + intro H; rewrite H; auto. +Qed. -Definition Zpos_max_1 : forall p, Zmax 1 (Zpos p) = Zpos p - := Z.pos_max_1. +Lemma Zpos_max_1 : forall p, Zmax 1 (Zpos p) = Zpos p. +Proof. + intros; unfold Zmax; simpl; destruct p; simpl; auto. +Qed. (** * Characterization of Pminus in term of Zminus and Zmax *) -Definition Zpos_minus : - forall p q, Zpos (Pminus p q) = Zmax 1 (Zpos p - Zpos q) - := Zpos_minus. +Lemma Zpos_minus : forall p q, Zpos (Pminus p q) = Zmax 1 (Zpos p - Zpos q). +Proof. + intros; simpl. destruct (Pcompare p q Eq) as [ ]_eqn:H. + rewrite (Pcompare_Eq_eq _ _ H). + unfold Pminus; rewrite Pminus_mask_diag; reflexivity. + rewrite Pminus_Lt; auto. + symmetry. apply Zpos_max_1. +Qed. (* begin hide *) (* Compatibility *) diff --git a/theories/ZArith/Zmin.v b/theories/ZArith/Zmin.v index 4703faace..e1599d943 100644 --- a/theories/ZArith/Zmin.v +++ b/theories/ZArith/Zmin.v @@ -7,16 +7,13 @@ (************************************************************************) (*i $Id$ i*) -(** THIS FILE IS DEPRECATED. Use [Zminmax] instead. *) +(** THIS FILE IS DEPRECATED. Use [ZBinary.Z] instead. *) -Require Import BinInt Zcompare Zorder Zminmax. +Require Import BinInt Zcompare Zorder ZBinary. Open Local Scope Z_scope. -(** [Zmin] is now [BinInt.Zmin]. Code that do things like - [unfold Zmin.Zmin] will have to be adapted, and neither - a [Definition] or a [Notation] here can help much. *) - +(** Definition [Zmin] is now [BinInt.Zmin]. *) (** * Characterization of the minimum on binary integer numbers *) @@ -77,14 +74,24 @@ Notation Zmin_SS := Z.succ_min_distr (only parsing). Definition Zplus_min_distr_r : forall n m p, Zmin (n + p) (m + p) = Zmin n m + p - := Z.plus_min_distr_r. + := Z.add_min_distr_r. -Notation Zmin_plus := Z.plus_min_distr_r (only parsing). +Notation Zmin_plus := Z.add_min_distr_r (only parsing). (** * Minimum and Zpos *) -Definition Zpos_min : forall p q, Zpos (Pmin p q) = Zmin (Zpos p) (Zpos q) - := Z.pos_min. +Lemma Zpos_min : forall p q, Zpos (Pmin p q) = Zmin (Zpos p) (Zpos q). +Proof. + intros; unfold Zmin, Pmin; simpl; generalize (Pcompare_Eq_eq p q). + destruct Pcompare; auto. +Qed. + +Lemma Zpos_min_1 : forall p, Zmin 1 (Zpos p) = 1. +Proof. + intros; unfold Zmax; simpl; destruct p; simpl; auto. +Qed. + + diff --git a/theories/ZArith/Zminmax.v b/theories/ZArith/Zminmax.v index 70f72568f..3f2cd5a5f 100644 --- a/theories/ZArith/Zminmax.v +++ b/theories/ZArith/Zminmax.v @@ -8,135 +8,7 @@ Require Import Orders BinInt Zcompare Zorder ZBinary. -(** * Maximum and Minimum of two [Z] numbers *) - -Local Open Scope Z_scope. - -(* All generic properties about max and min are already in [ZBinary.Z]. - We prove here in addition some results specific to Z. -*) - -Module Z. -Include ZBinary.Z. - -(** Compatibilities (consequences of monotonicity) *) - -Lemma plus_max_distr_l : forall n m p, Zmax (p + n) (p + m) = p + Zmax n m. -Proof. - intros. apply max_monotone. - intros x y. apply Zplus_le_compat_l. -Qed. - -Lemma plus_max_distr_r : forall n m p, Zmax (n + p) (m + p) = Zmax n m + p. -Proof. - intros. rewrite (Zplus_comm n p), (Zplus_comm m p), (Zplus_comm _ p). - apply plus_max_distr_l. -Qed. - -Lemma plus_min_distr_l : forall n m p, Zmin (p + n) (p + m) = p + Zmin n m. -Proof. - intros. apply Z.min_monotone. - intros x y. apply Zplus_le_compat_l. -Qed. - -Lemma plus_min_distr_r : forall n m p, Zmin (n + p) (m + p) = Zmin n m + p. -Proof. - intros. rewrite (Zplus_comm n p), (Zplus_comm m p), (Zplus_comm _ p). - apply plus_min_distr_l. -Qed. - -Lemma succ_max_distr : forall n m, Zsucc (Zmax n m) = Zmax (Zsucc n) (Zsucc m). -Proof. - unfold Zsucc. intros. symmetry. apply plus_max_distr_r. -Qed. - -Lemma succ_min_distr : forall n m, Zsucc (Zmin n m) = Zmin (Zsucc n) (Zsucc m). -Proof. - unfold Zsucc. intros. symmetry. apply plus_min_distr_r. -Qed. - -Lemma pred_max_distr : forall n m, Zpred (Zmax n m) = Zmax (Zpred n) (Zpred m). -Proof. - unfold Zpred. intros. symmetry. apply plus_max_distr_r. -Qed. - -Lemma pred_min_distr : forall n m, Zsucc (Zmin n m) = Zmin (Zsucc n) (Zsucc m). -Proof. - unfold Zpred. intros. symmetry. apply plus_min_distr_r. -Qed. - -(** Anti-monotonicity swaps the role of [min] and [max] *) - -Lemma opp_max_distr : forall n m : Z, -(Zmax n m) = Zmin (- n) (- m). -Proof. - intros. symmetry. apply min_max_antimonotone. - intros x x'. red. red. rewrite <- Zcompare_opp; auto. -Qed. - -Lemma opp_min_distr : forall n m : Z, - (Zmin n m) = Zmax (- n) (- m). -Proof. - intros. symmetry. apply max_min_antimonotone. - intros x x'. red. red. rewrite <- Zcompare_opp; auto. -Qed. - -Lemma minus_max_distr_l : forall n m p, Zmax (p - n) (p - m) = p - Zmin n m. -Proof. - unfold Zminus. intros. rewrite opp_min_distr. apply plus_max_distr_l. -Qed. - -Lemma minus_max_distr_r : forall n m p, Zmax (n - p) (m - p) = Zmax n m - p. -Proof. - unfold Zminus. intros. apply plus_max_distr_r. -Qed. - -Lemma minus_min_distr_l : forall n m p, Zmin (p - n) (p - m) = p - Zmax n m. -Proof. - unfold Zminus. intros. rewrite opp_max_distr. apply plus_min_distr_l. -Qed. - -Lemma minus_min_distr_r : forall n m p, Zmin (n - p) (m - p) = Zmin n m - p. -Proof. - unfold Zminus. intros. apply plus_min_distr_r. -Qed. - -(** Compatibility with [Zpos] *) - -Lemma pos_max : forall p q, Zpos (Pmax p q) = Zmax (Zpos p) (Zpos q). -Proof. - intros; unfold Zmax, Pmax; simpl; generalize (Pcompare_Eq_eq p q). - destruct Pcompare; auto. - intro H; rewrite H; auto. -Qed. - -Lemma pos_min : forall p q, Zpos (Pmin p q) = Zmin (Zpos p) (Zpos q). -Proof. - intros; unfold Zmin, Pmin; simpl; generalize (Pcompare_Eq_eq p q). - destruct Pcompare; auto. -Qed. - -Lemma pos_max_1 : forall p, Zmax 1 (Zpos p) = Zpos p. -Proof. - intros; unfold Zmax; simpl; destruct p; simpl; auto. -Qed. - -Lemma pos_min_1 : forall p, Zmin 1 (Zpos p) = 1. -Proof. - intros; unfold Zmax; simpl; destruct p; simpl; auto. -Qed. - -End Z. - -(** * Characterization of Pminus in term of Zminus and Zmax *) - -Lemma Zpos_minus : forall p q, Zpos (Pminus p q) = Zmax 1 (Zpos p - Zpos q). -Proof. - intros; simpl. destruct (Pcompare p q Eq) as [ ]_eqn:H. - rewrite (Pcompare_Eq_eq _ _ H). - unfold Pminus; rewrite Pminus_mask_diag; reflexivity. - rewrite Pminus_Lt; auto. - symmetry. apply Z.pos_max_1. -Qed. - +(** THIS FILE IS DEPRECATED. Use [ZBinary.Z] instead. *) (*begin hide*) (* Compatibility with names of the old Zminmax file *) |