diff options
Diffstat (limited to 'theories/Numbers/Natural')
-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 |
4 files changed, 153 insertions, 7 deletions
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. |