diff options
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZDivEucl.v | 112 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZDivFloor.v | 4 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZDivTrunc.v | 27 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZProperties.v | 9 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZSgnAbs.v | 348 | ||||
| -rw-r--r-- | theories/Numbers/Integer/BigZ/ZMake.v | 16 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Binary/ZBinary.v | 16 | ||||
| -rw-r--r-- | theories/Numbers/Integer/SpecViaZ/ZSig.v | 8 | ||||
| -rw-r--r-- | theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v | 38 | ||||
| -rw-r--r-- | theories/Numbers/vo.itarget | 1 |
10 files changed, 462 insertions, 117 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v index ba79ae24b..d0f530fef 100644 --- a/theories/Numbers/Integer/Abstract/ZDivEucl.v +++ b/theories/Numbers/Integer/Abstract/ZDivEucl.v @@ -23,16 +23,15 @@ Require Import ZAxioms ZProperties NZDiv. -Module Type ZDivSpecific (Import Z : ZAxiomsSig')(Import DM : DivMod' Z). - Definition abs z := max z (-z). +Module Type ZDivSpecific (Import Z : ZAxiomsExtSig')(Import DM : DivMod' Z). Axiom mod_always_pos : forall a b, 0 <= a mod b < abs b. End ZDivSpecific. -Module Type ZDiv (Z:ZAxiomsSig) +Module Type ZDiv (Z:ZAxiomsExtSig) := DivMod Z <+ NZDivCommon Z <+ ZDivSpecific Z. -Module Type ZDivSig := ZAxiomsSig <+ ZDiv. -Module Type ZDivSig' := ZAxiomsSig' <+ ZDiv <+ DivModNotation. +Module Type ZDivSig := ZAxiomsExtSig <+ ZDiv. +Module Type ZDivSig' := ZAxiomsExtSig' <+ ZDiv <+ DivModNotation. Module ZDivPropFunct (Import Z : ZDivSig')(Import ZP : ZPropSig Z). @@ -42,9 +41,8 @@ Module ZDivPropFunct (Import Z : ZDivSig')(Import ZP : ZPropSig Z). Include Z. Lemma mod_bound : forall a b, 0<=a -> 0<b -> 0 <= a mod b < b. Proof. - intros. rewrite <- (max_l b (-b)) at 3. + intros. rewrite <- (abs_eq b) at 3 by now apply lt_le_incl. apply mod_always_pos. - apply le_trans with 0; [ rewrite opp_nonpos_nonneg |]; order. Qed. End Z'. Module Import NZDivP := NZDivPropFunct Z' ZP. @@ -64,53 +62,6 @@ Ltac pos_or_neg a := let LE := fresh "LE" in destruct (le_gt_cases 0 a) as [LE|LT]; [|rewrite <- opp_pos_neg in LT]. -(*TODO: To migrate later ... *) -Lemma abs_pos : forall z, 0<=z -> abs z == z. -Proof. -intros; apply max_l. apply le_trans with 0; trivial. -now rewrite opp_nonpos_nonneg. -Qed. -Lemma abs_neg : forall z, 0<=-z -> abs z == -z. -Proof. -intros; apply max_r. apply le_trans with 0; trivial. -now rewrite <- opp_nonneg_nonpos. -Qed. -Instance abs_wd : Proper (eq==>eq) abs. -Proof. -intros x y EQ. pos_or_neg x. -rewrite 2 abs_pos; trivial. now rewrite <- EQ. -rewrite 2 abs_neg; try order. now rewrite opp_inj_wd. rewrite <- EQ; order. -Qed. -Lemma abs_opp : forall z, abs (-z) == abs z. -Proof. -intros. pos_or_neg z. -rewrite (abs_pos z), (abs_neg (-z)); rewrite ? opp_involutive; order. -rewrite (abs_pos (-z)), (abs_neg z); order. -Qed. -Lemma abs_nonneg : forall z, 0<=abs z. -Proof. -intros. pos_or_neg z. -rewrite abs_pos; trivial. -rewrite <-abs_opp, abs_pos; order. -Qed. -Lemma abs_nz : forall z, z~=0 -> 0<abs z. -Proof. -intros. pos_or_neg z. -rewrite abs_pos; order. -rewrite <-abs_opp, abs_pos; order. -Qed. -Lemma abs_mul : forall a b, abs (a*b) == abs a * abs b. -Proof. -assert (Aux1 : forall a b, 0<=a -> abs (a*b) == a * abs b). - intros. pos_or_neg b. - rewrite 2 abs_pos; try order. now apply mul_nonneg_nonneg. - rewrite 2 abs_neg; try order. now rewrite mul_opp_r. - rewrite <-mul_opp_r; apply mul_nonneg_nonneg; order. -intros. pos_or_neg a. rewrite Aux1, (abs_pos a); order. -rewrite <- mul_opp_opp, Aux1, abs_opp, (abs_neg a); order. -Qed. -(*/TODO *) - (** Uniqueness theorems *) Theorem div_mod_unique : forall b q1 q2 r1 r2 : t, @@ -119,9 +70,9 @@ Theorem div_mod_unique : forall b q1 q2 r1 r2 : t, Proof. intros b q1 q2 r1 r2 Hr1 Hr2 EQ. pos_or_neg b. -rewrite abs_pos in * by trivial. +rewrite abs_eq in * by trivial. apply div_mod_unique with b; trivial. -rewrite abs_neg in *; try order. +rewrite abs_neq' in * by auto using lt_le_incl. rewrite eq_sym_iff. apply div_mod_unique with (-b); trivial. rewrite 2 mul_opp_l. rewrite add_move_l, sub_opp_r. @@ -136,8 +87,8 @@ Proof. intros a b q r Hr EQ. assert (Hb : b~=0). pos_or_neg b. - rewrite abs_pos in Hr; intuition; order. - rewrite <- opp_0, eq_opp_r. rewrite abs_neg in Hr; intuition; order. + rewrite abs_eq in Hr; intuition; order. + rewrite <- opp_0, eq_opp_r. rewrite abs_neq' in Hr; intuition; order. destruct (div_mod_unique b q (a/b) r (a mod b)); trivial. now apply mod_always_pos. now rewrite <- div_mod. @@ -149,22 +100,13 @@ Proof. intros a b q r Hr EQ. assert (Hb : b~=0). pos_or_neg b. - rewrite abs_pos in Hr; intuition; order. - rewrite <- opp_0, eq_opp_r. rewrite abs_neg in Hr; intuition; order. + rewrite abs_eq in Hr; intuition; order. + rewrite <- opp_0, eq_opp_r. rewrite abs_neq' in Hr; intuition; order. destruct (div_mod_unique b q (a/b) r (a mod b)); trivial. now apply mod_always_pos. now rewrite <- div_mod. Qed. -(** TODO: Provide a [sign] function *) -Parameter sign : t -> t. -Parameter sign_pos : forall t, sign t == 1 <-> 0<t. -Parameter sign_0 : forall t, sign t == 0 <-> t==0. -Parameter sign_neg : forall t, sign t == -(1) <-> t<0. -Parameter sign_abs : forall t, t * sign t == abs t. -(** END TODO *) - - (** Sign rules *) Lemma div_opp_r : forall a b, b~=0 -> a/(-b) == -(a/b). @@ -189,12 +131,12 @@ Proof. intros a b Hb Hab. symmetry. apply div_unique with (-(a mod b)). rewrite Hab, opp_0. split; [order|]. -pos_or_neg b; [rewrite abs_pos | rewrite abs_neg]; order. +pos_or_neg b; [rewrite abs_eq | rewrite abs_neq']; order. now rewrite mul_opp_r, <-opp_add_distr, <-div_mod. Qed. Lemma div_opp_l_nz : forall a b, b~=0 -> a mod b ~= 0 -> - (-a)/b == -(a/b)-sign b. + (-a)/b == -(a/b)-sgn b. Proof. intros a b Hb Hab. symmetry. apply div_unique with (abs b -(a mod b)). @@ -204,7 +146,7 @@ rewrite <- (add_0_l (abs b)) at 2. rewrite <- add_lt_mono_r. destruct (mod_always_pos a b); intuition order. rewrite <- 2 add_opp_r, mul_add_distr_l, 2 mul_opp_r. -rewrite sign_abs. +rewrite sgn_abs. rewrite add_shuffle2, add_opp_diag_l; nzsimpl. rewrite <-opp_add_distr, <-div_mod; order. Qed. @@ -214,7 +156,7 @@ Lemma mod_opp_l_z : forall a b, b~=0 -> a mod b == 0 -> Proof. intros a b Hb Hab. symmetry. apply mod_unique with (-(a/b)). -split; [order|now apply abs_nz]. +split; [order|now rewrite abs_pos]. now rewrite <-opp_0, <-Hab, mul_opp_r, <-opp_add_distr, <-div_mod. Qed. @@ -222,14 +164,14 @@ Lemma mod_opp_l_nz : forall a b, b~=0 -> a mod b ~= 0 -> (-a) mod b == abs b - (a mod b). Proof. intros a b Hb Hab. symmetry. -apply mod_unique with (-(a/b)-sign b). +apply mod_unique with (-(a/b)-sgn b). rewrite lt_sub_lt_add_l. rewrite <- le_add_le_sub_l. nzsimpl. rewrite <- (add_0_l (abs b)) at 2. rewrite <- add_lt_mono_r. destruct (mod_always_pos a b); intuition order. rewrite <- 2 add_opp_r, mul_add_distr_l, 2 mul_opp_r. -rewrite sign_abs. +rewrite sgn_abs. rewrite add_shuffle2, add_opp_diag_l; nzsimpl. rewrite <-opp_add_distr, <-div_mod; order. Qed. @@ -241,7 +183,7 @@ intros. now rewrite div_opp_r, div_opp_l_z, opp_involutive. Qed. Lemma div_opp_opp_nz : forall a b, b~=0 -> a mod b ~= 0 -> - (-a)/(-b) == a/b + sign(b). + (-a)/(-b) == a/b + sgn(b). Proof. intros. rewrite div_opp_r, div_opp_l_nz by trivial. now rewrite opp_sub_distr, opp_involutive. @@ -264,7 +206,7 @@ Qed. Lemma div_same : forall a, a~=0 -> a/a == 1. Proof. intros. symmetry. apply div_unique with 0. -split; [order|now apply abs_nz]. +split; [order|now rewrite abs_pos]. now nzsimpl. Qed. @@ -319,7 +261,7 @@ Proof. exact mod_1_l. Qed. Lemma div_mul : forall a b, b~=0 -> (a*b)/b == a. Proof. intros. symmetry. apply div_unique with 0. -split; [order|now apply abs_nz]. +split; [order|now rewrite abs_pos]. nzsimpl; apply mul_comm. Qed. @@ -353,10 +295,10 @@ rewrite (div_mod a b Hb), EQ; nzsimpl. apply mod_always_pos. intros. pos_or_neg b. apply div_small. -now rewrite <- (abs_pos b). +now rewrite <- (abs_eq b). apply opp_inj; rewrite opp_0, <- div_opp_r by trivial. apply div_small. -rewrite <- (abs_neg b) by order. trivial. +rewrite <- (abs_neq' b) by order. trivial. Qed. Lemma mod_small_iff : forall a b, b~=0 -> (a mod b == a <-> 0<=a<abs b). @@ -390,7 +332,7 @@ rewrite (div_mod b c) at 1 by order. rewrite <- add_assoc, <- add_le_mono_l. apply le_trans with (c+0). nzsimpl; destruct (mod_always_pos b c); try order. -rewrite abs_pos in *; order. +rewrite abs_eq in *; order. rewrite <- add_le_mono_l. destruct (mod_always_pos a c); order. Qed. @@ -420,7 +362,7 @@ nzsimpl. rewrite (div_mod a b) at 1; try order. rewrite <- add_lt_mono_l. destruct (mod_always_pos a b). -rewrite abs_pos in *; order. +rewrite abs_eq in *; order. Qed. Lemma mul_pred_div_gt: forall a b, b<0 -> a < b*(P (a/b)). @@ -430,7 +372,7 @@ rewrite mul_pred_r, <- add_opp_r. rewrite (div_mod a b) at 1; try order. rewrite <- add_lt_mono_l. destruct (mod_always_pos a b). -rewrite <- opp_pos_neg in Hb. rewrite abs_neg in *; order. +rewrite <- opp_pos_neg in Hb. rewrite abs_neq' in *; order. Qed. (** NB: The three previous properties could be used as @@ -521,7 +463,7 @@ intros. symmetry. apply div_unique with ((a mod b)*c). (* ineqs *) -rewrite abs_mul, (abs_pos c) by order. +rewrite abs_mul, (abs_eq c) by order. rewrite <-(mul_0_l c), <-mul_lt_mono_pos_r, <-mul_le_mono_pos_r by trivial. apply mod_always_pos. (* equation *) @@ -626,7 +568,7 @@ Proof. apply mul_nonneg_nonneg; order. apply lt_le_trans with (b*((a/b) mod c) + abs b). now rewrite <- add_lt_mono_l. - rewrite (abs_pos b) by order. + rewrite (abs_eq b) by order. now rewrite <- mul_succ_r, <- mul_le_mono_pos_l, le_succ_l. (* end 0<= ... < abs(b*c) *) rewrite (div_mod a b) at 1 by order. diff --git a/theories/Numbers/Integer/Abstract/ZDivFloor.v b/theories/Numbers/Integer/Abstract/ZDivFloor.v index 99df15f23..b94affd79 100644 --- a/theories/Numbers/Integer/Abstract/ZDivFloor.v +++ b/theories/Numbers/Integer/Abstract/ZDivFloor.v @@ -34,8 +34,8 @@ End ZDivSpecific. Module Type ZDiv (Z:ZAxiomsSig) := DivMod Z <+ NZDivCommon Z <+ ZDivSpecific Z. -Module Type ZDivSig := ZAxiomsSig <+ ZDiv. -Module Type ZDivSig' := ZAxiomsSig' <+ ZDiv <+ DivModNotation. +Module Type ZDivSig := ZAxiomsExtSig <+ ZDiv. +Module Type ZDivSig' := ZAxiomsExtSig' <+ ZDiv <+ DivModNotation. Module ZDivPropFunct (Import Z : ZDivSig')(Import ZP : ZPropSig Z). diff --git a/theories/Numbers/Integer/Abstract/ZDivTrunc.v b/theories/Numbers/Integer/Abstract/ZDivTrunc.v index 0468b3bf5..6b6b71703 100644 --- a/theories/Numbers/Integer/Abstract/ZDivTrunc.v +++ b/theories/Numbers/Integer/Abstract/ZDivTrunc.v @@ -35,8 +35,8 @@ End ZDivSpecific. Module Type ZDiv (Z:ZAxiomsSig) := DivMod Z <+ NZDivCommon Z <+ ZDivSpecific Z. -Module Type ZDivSig := ZAxiomsSig <+ ZDiv. -Module Type ZDivSig' := ZAxiomsSig' <+ ZDiv <+ DivModNotation. +Module Type ZDivSig := ZAxiomsExtSig <+ ZDiv. +Module Type ZDivSig' := ZAxiomsExtSig' <+ ZDiv <+ DivModNotation. Module ZDivPropFunct (Import Z : ZDivSig')(Import ZP : ZPropSig Z). @@ -205,31 +205,16 @@ Proof. exact div_pos. Qed. Lemma div_str_pos : forall a b, 0<b<=a -> 0 < a/b. Proof. exact div_str_pos. Qed. -(** TODO: TO MIGRATE LATER *) -Definition abs z := max z (-z). -Lemma abs_pos : forall z, 0<=z -> abs z == z. -Proof. -intros; apply max_l. apply le_trans with 0; trivial. -now rewrite opp_nonpos_nonneg. -Qed. -Lemma abs_neg : forall z, 0<=-z -> abs z == -z. -Proof. -intros; apply max_r. apply le_trans with 0; trivial. -now rewrite <- opp_nonneg_nonpos. -Qed. - -(** END TODO *) - Lemma div_small_iff : forall a b, b~=0 -> (a/b==0 <-> abs a < abs b). Proof. intros. pos_or_neg a; pos_or_neg b. -rewrite div_small_iff; try order. rewrite 2 abs_pos; intuition; order. +rewrite div_small_iff; try order. rewrite 2 abs_eq; intuition; order. rewrite <- opp_inj_wd, opp_0, <- div_opp_r, div_small_iff by order. - rewrite (abs_pos a), (abs_neg b); intuition; order. + rewrite (abs_eq a), (abs_neq' b); intuition; order. rewrite <- opp_inj_wd, opp_0, <- div_opp_l, div_small_iff by order. - rewrite (abs_neg a), (abs_pos b); intuition; order. + rewrite (abs_neq' a), (abs_eq b); intuition; order. rewrite <- div_opp_opp, div_small_iff by order. - rewrite (abs_neg a), (abs_neg b); intuition; order. + rewrite (abs_neq' a), (abs_neq' b); intuition; order. Qed. Lemma mod_small_iff : forall a b, b~=0 -> (a mod b == a <-> abs a < abs b). diff --git a/theories/Numbers/Integer/Abstract/ZProperties.v b/theories/Numbers/Integer/Abstract/ZProperties.v index 9b6f0ff64..dc46eddab 100644 --- a/theories/Numbers/Integer/Abstract/ZProperties.v +++ b/theories/Numbers/Integer/Abstract/ZProperties.v @@ -8,16 +8,17 @@ (*i $Id$ i*) -Require Export ZAxioms ZMulOrder. +Require Export ZAxioms ZMulOrder ZSgnAbs. (** This functor summarizes all known facts about Z. For the moment it is only an alias to [ZMulOrderPropFunct], which - subsumes all others. + subsumes all others, plus properties of [sgn] and [abs]. *) -Module Type ZPropSig := ZMulOrderPropFunct. +Module Type ZPropSig (Z:ZAxiomsExtSig) := + ZMulOrderPropFunct Z <+ ZSgnAbsPropSig Z. -Module ZPropFunct (Z:ZAxiomsSig) <: ZPropSig Z. +Module ZPropFunct (Z:ZAxiomsExtSig) <: ZPropSig Z. Include ZPropSig Z. End ZPropFunct. diff --git a/theories/Numbers/Integer/Abstract/ZSgnAbs.v b/theories/Numbers/Integer/Abstract/ZSgnAbs.v new file mode 100644 index 000000000..8b1916132 --- /dev/null +++ b/theories/Numbers/Integer/Abstract/ZSgnAbs.v @@ -0,0 +1,348 @@ +(************************************************************************) +(* 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 Export ZMulOrder. + +(** An axiomatization of [abs]. *) + +Module Type HasAbs(Import Z : ZAxiomsSig'). + Parameter Inline abs : t -> t. + Axiom abs_eq : forall n, 0<=n -> abs n == n. + Axiom abs_neq : forall n, n<=0 -> abs n == -n. +End HasAbs. + +(** Since we already have [max], we could have defined [abs]. *) + +Module GenericAbs (Import Z : ZAxiomsSig') + (Import ZP : ZMulOrderPropFunct Z) <: HasAbs Z. + Definition abs n := max n (-n). + Lemma abs_eq : forall n, 0<=n -> abs n == n. + Proof. + intros. unfold abs. apply max_l. + apply le_trans with 0; auto. + rewrite opp_nonpos_nonneg; auto. + Qed. + Lemma abs_neq : forall n, n<=0 -> abs n == -n. + Proof. + intros. unfold abs. apply max_r. + apply le_trans with 0; auto. + rewrite opp_nonneg_nonpos; auto. + Qed. +End GenericAbs. + +(** An Axiomatization of [sgn]. *) + +Module Type HasSgn (Import Z : ZAxiomsSig'). + Parameter Inline sgn : t -> t. + Axiom sgn_null : forall n, n==0 -> sgn n == 0. + Axiom sgn_pos : forall n, 0<n -> sgn n == 1. + Axiom sgn_neg : forall n, n<0 -> sgn n == -(1). +End HasSgn. + +(** We can deduce a [sgn] function from a [compare] function *) + +Module Type ZDecAxiomsSig := ZAxiomsSig <+ HasCompare. +Module Type ZDecAxiomsSig' := ZAxiomsSig' <+ HasCompare. + +Module Type GenericSgn (Import Z : ZDecAxiomsSig') + (Import ZP : ZMulOrderPropFunct Z) <: HasSgn Z. + Definition sgn n := + match compare 0 n with Eq => 0 | Lt => 1 | Gt => -(1) end. + Lemma sgn_null : forall n, n==0 -> sgn n == 0. + Proof. unfold sgn; intros. destruct (compare_spec 0 n); order. Qed. + Lemma sgn_pos : forall n, 0<n -> sgn n == 1. + Proof. unfold sgn; intros. destruct (compare_spec 0 n); order. Qed. + Lemma sgn_neg : forall n, n<0 -> sgn n == -(1). + Proof. unfold sgn; intros. destruct (compare_spec 0 n); order. Qed. +End GenericSgn. + +Module Type ZAxiomsExtSig := ZAxiomsSig <+ HasAbs <+ HasSgn. +Module Type ZAxiomsExtSig' := ZAxiomsSig' <+ HasAbs <+ HasSgn. + +Module Type ZSgnAbsPropSig (Import Z : ZAxiomsExtSig') + (Import ZP : ZMulOrderPropFunct Z). + +Ltac destruct_max n := + destruct (le_ge_cases 0 n); + [rewrite (abs_eq n) by auto | rewrite (abs_neq n) by auto]. + +Instance abs_wd : Proper (eq==>eq) abs. +Proof. + intros x y EQ. destruct_max x. + rewrite abs_eq; trivial. now rewrite <- EQ. + rewrite abs_neq; try order. now rewrite opp_inj_wd. +Qed. + +Lemma abs_max : forall n, abs n == max n (-n). +Proof. + intros n. destruct_max n. + rewrite max_l; auto with relations. + apply le_trans with 0; auto. + rewrite opp_nonpos_nonneg; auto. + rewrite max_r; auto with relations. + apply le_trans with 0; auto. + rewrite opp_nonneg_nonpos; auto. +Qed. + +Lemma abs_neq' : forall n, 0<=-n -> abs n == -n. +Proof. + intros. apply abs_neq. now rewrite <- opp_nonneg_nonpos. +Qed. + +Lemma abs_nonneg : forall n, 0 <= abs n. +Proof. + intros n. destruct_max n; auto. + now rewrite opp_nonneg_nonpos. +Qed. + +Lemma abs_eq_iff : forall n, abs n == n <-> 0<=n. +Proof. + split; try apply abs_eq. intros EQ. + rewrite <- EQ. apply abs_nonneg. +Qed. + +Lemma abs_neq_iff : forall n, abs n == -n <-> n<=0. +Proof. + split; try apply abs_neq. intros EQ. + rewrite <- opp_nonneg_nonpos, <- EQ. apply abs_nonneg. +Qed. + +Lemma abs_opp : forall n, abs (-n) == abs n. +Proof. + intros. destruct_max n. + rewrite (abs_neq (-n)), opp_involutive. reflexivity. + now rewrite opp_nonpos_nonneg. + rewrite (abs_eq (-n)). reflexivity. + now rewrite opp_nonneg_nonpos. +Qed. + +Lemma abs_0 : abs 0 == 0. +Proof. + apply abs_eq. apply le_refl. +Qed. + +Lemma abs_0_iff : forall n, abs n == 0 <-> n==0. +Proof. + split. destruct_max n; auto. + now rewrite eq_opp_l, opp_0. + intros EQ; rewrite EQ. rewrite abs_eq; auto using eq_refl, le_refl. +Qed. + +Lemma abs_pos : forall n, 0 < abs n <-> n~=0. +Proof. + intros. rewrite <- abs_0_iff. split; [intros LT| intros NEQ]. + intro EQ. rewrite EQ in LT. now elim (lt_irrefl 0). + assert (LE : 0 <= abs n) by apply abs_nonneg. + rewrite lt_eq_cases in LE; destruct LE; auto. + elim NEQ; auto with relations. +Qed. + +Lemma abs_eq_or_opp : forall n, abs n == n \/ abs n == -n. +Proof. + intros. destruct_max n; auto with relations. +Qed. + +Lemma abs_or_opp_abs : forall n, n == abs n \/ n == - abs n. +Proof. + intros. destruct_max n; rewrite ? opp_involutive; auto with relations. +Qed. + +Lemma abs_involutive : forall n, abs (abs n) == abs n. +Proof. + intros. apply abs_eq. apply abs_nonneg. +Qed. + +Lemma abs_spec : forall n, + (0 <= n /\ abs n == n) \/ (n < 0 /\ abs n == -n). +Proof. + intros. destruct (le_gt_cases 0 n). + left; split; auto. now apply abs_eq. + right; split; auto. apply abs_neq. now apply lt_le_incl. +Qed. + +Lemma abs_case_strong : + forall (P:t->Prop) n, Proper (eq==>iff) P -> + (0<=n -> P n) -> (n<=0 -> P (-n)) -> P (abs n). +Proof. + intros. destruct_max n; auto. +Qed. + +Lemma abs_case : forall (P:t->Prop) n, Proper (eq==>iff) P -> + P n -> P (-n) -> P (abs n). +Proof. intros. now apply abs_case_strong. Qed. + +Lemma abs_eq_cases : forall n m, abs n == abs m -> n == m \/ n == - m. +Proof. + intros n m EQ. destruct (abs_or_opp_abs n) as [EQn|EQn]. + rewrite EQn, EQ. apply abs_eq_or_opp. + rewrite EQn, EQ, opp_inj_wd, eq_opp_l, or_comm. apply abs_eq_or_opp. +Qed. + +(** Triangular inequality *) + +Lemma abs_triangle : forall n m, abs (n + m) <= abs n + abs m. +Proof. + intros. destruct_max n; destruct_max m. + rewrite abs_eq. apply le_refl. now apply add_nonneg_nonneg. + destruct_max (n+m); try rewrite opp_add_distr; + apply add_le_mono_l || apply add_le_mono_r. + apply le_trans with 0; auto. now rewrite opp_nonneg_nonpos. + apply le_trans with 0; auto. now rewrite opp_nonpos_nonneg. + destruct_max (n+m); try rewrite opp_add_distr; + apply add_le_mono_l || apply add_le_mono_r. + apply le_trans with 0; auto. now rewrite opp_nonneg_nonpos. + apply le_trans with 0; auto. now rewrite opp_nonpos_nonneg. + rewrite abs_neq, opp_add_distr. apply le_refl. + now apply add_nonpos_nonpos. +Qed. + +Lemma abs_sub_triangle : forall n m, abs n - abs m <= abs (n-m). +Proof. + intros. + rewrite le_sub_le_add_l, add_comm. + rewrite <- (sub_simpl_r n m) at 1. + apply abs_triangle. +Qed. + +(** Absolute value and multiplication *) + +Lemma abs_mul : forall n m, abs (n * m) == abs n * abs m. +Proof. + assert (H : forall n m, 0<=n -> abs (n*m) == n * abs m). + intros. destruct_max m. + rewrite abs_eq. apply eq_refl. now apply mul_nonneg_nonneg. + rewrite abs_neq, mul_opp_r. reflexivity. now apply mul_nonneg_nonpos . + intros. destruct_max n. now apply H. + rewrite <- mul_opp_opp, H, abs_opp. reflexivity. + now apply opp_nonneg_nonpos. +Qed. + +Lemma abs_square : forall n, abs n * abs n == n * n. +Proof. + intros. rewrite <- abs_mul. apply abs_eq. apply le_0_square. +Qed. + +(** Some results about the sign function. *) + +Ltac destruct_sgn n := + let LT := fresh "LT" in + let EQ := fresh "EQ" in + let GT := fresh "GT" in + destruct (lt_trichotomy 0 n) as [LT|[EQ|GT]]; + [rewrite (sgn_pos n) by auto| + rewrite (sgn_null n) by auto with relations| + rewrite (sgn_neg n) by auto]. + +Instance sgn_wd : Proper (eq==>eq) sgn. +Proof. + intros x y Hxy. destruct_sgn x. + rewrite sgn_pos; auto with relations. rewrite <- Hxy; auto. + rewrite sgn_null; auto with relations. rewrite <- Hxy; auto with relations. + rewrite sgn_neg; auto with relations. rewrite <- Hxy; auto. +Qed. + +Lemma sgn_spec : forall n, + 0 < n /\ sgn n == 1 \/ + 0 == n /\ sgn n == 0 \/ + 0 > n /\ sgn n == -(1). +Proof. + intros n. + destruct_sgn n; [left|right;left|right;right]; auto with relations. +Qed. + +Lemma sgn_0 : sgn 0 == 0. +Proof. + now apply sgn_null. +Qed. + +Lemma sgn_pos_iff : forall n, sgn n == 1 <-> 0<n. +Proof. + split; try apply sgn_pos. destruct_sgn n; auto. + intros. elim (lt_neq 0 1); auto. apply lt_0_1. + intros. elim (lt_neq (-(1)) 1); auto. + apply lt_trans with 0. rewrite opp_neg_pos. apply lt_0_1. apply lt_0_1. +Qed. + +Lemma sgn_null_iff : forall n, sgn n == 0 <-> n==0. +Proof. + split; try apply sgn_null. destruct_sgn n; auto with relations. + intros. elim (lt_neq 0 1); auto with relations. apply lt_0_1. + intros. elim (lt_neq (-(1)) 0); auto. + rewrite opp_neg_pos. apply lt_0_1. +Qed. + +Lemma sgn_neg_iff : forall n, sgn n == -(1) <-> n<0. +Proof. + split; try apply sgn_neg. destruct_sgn n; auto with relations. + intros. elim (lt_neq (-(1)) 1); auto with relations. + apply lt_trans with 0. rewrite opp_neg_pos. apply lt_0_1. apply lt_0_1. + intros. elim (lt_neq (-(1)) 0); auto with relations. + rewrite opp_neg_pos. apply lt_0_1. +Qed. + +Lemma sgn_opp : forall n, sgn (-n) == - sgn n. +Proof. + intros. destruct_sgn n. + apply sgn_neg. now rewrite opp_neg_pos. + setoid_replace n with 0 by auto with relations. + rewrite opp_0. apply sgn_0. + rewrite opp_involutive. apply sgn_pos. now rewrite opp_pos_neg. +Qed. + +Lemma sgn_nonneg : forall n, 0 <= sgn n <-> 0 <= n. +Proof. + split. + destruct_sgn n; intros. + now apply lt_le_incl. + order. + elim (lt_irrefl 0). apply lt_le_trans with 1; auto using lt_0_1. + now rewrite <- opp_nonneg_nonpos. + rewrite lt_eq_cases; destruct 1. + rewrite sgn_pos by auto. apply lt_le_incl, lt_0_1. + rewrite sgn_null by auto with relations. apply le_refl. +Qed. + +Lemma sgn_nonpos : forall n, sgn n <= 0 <-> n <= 0. +Proof. + intros. rewrite <- 2 opp_nonneg_nonpos, <- sgn_opp. apply sgn_nonneg. +Qed. + +Lemma sgn_mul : forall n m, sgn (n*m) == sgn n * sgn m. +Proof. + intros. destruct_sgn n; nzsimpl. + destruct_sgn m. + apply sgn_pos. now apply mul_pos_pos. + apply sgn_null. rewrite eq_mul_0; auto with relations. + apply sgn_neg. now apply mul_pos_neg. + apply sgn_null. rewrite eq_mul_0; auto with relations. + destruct_sgn m; try rewrite mul_opp_opp; nzsimpl. + apply sgn_neg. now apply mul_neg_pos. + apply sgn_null. rewrite eq_mul_0; auto with relations. + apply sgn_pos. now apply mul_neg_neg. +Qed. + +Lemma sgn_abs : forall n, n * sgn n == abs n. +Proof. + intros. symmetry. + destruct_sgn n; try rewrite mul_opp_r; nzsimpl. + apply abs_eq. now apply lt_le_incl. + rewrite abs_0_iff; auto with relations. + apply abs_neq. now apply lt_le_incl. +Qed. + +Lemma abs_sgn : forall n, abs n * sgn n == n. +Proof. + intros. + destruct_sgn n; try rewrite mul_opp_r; nzsimpl; auto. + apply abs_eq. now apply lt_le_incl. + rewrite eq_opp_l. apply abs_neq. now apply lt_le_incl. +Qed. + +End ZSgnAbsPropSig. + + diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v index 615b8d139..827877fc5 100644 --- a/theories/Numbers/Integer/BigZ/ZMake.v +++ b/theories/Numbers/Integer/BigZ/ZMake.v @@ -488,4 +488,20 @@ Module Make (N:NType) <: ZType. case N.to_Z; simpl; auto with zarith. Qed. + Definition sgn x := + match compare zero x with + | Lt => one + | Eq => zero + | Gt => minus_one + end. + + Lemma spec_sgn : forall x, to_Z (sgn x) = Zsgn (to_Z x). + Proof. + intros. unfold sgn. generalize (spec_compare zero x). + destruct compare. + rewrite spec_0. intros <-; auto. + rewrite spec_0, spec_1. symmetry. rewrite Zsgn_pos; auto. + rewrite spec_0, spec_m1. symmetry. rewrite Zsgn_neg; auto with zarith. + Qed. + End Make. diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v index 516827616..6a2745d34 100644 --- a/theories/Numbers/Integer/Binary/ZBinary.v +++ b/theories/Numbers/Integer/Binary/ZBinary.v @@ -18,7 +18,7 @@ Local Open Scope Z_scope. (** * Implementation of [ZAxiomsSig] by [BinInt.Z] *) -Module ZBinAxiomsMod <: ZAxiomsSig. +Module ZBinAxiomsMod <: ZAxiomsExtSig. (** Bi-directional induction. *) @@ -70,6 +70,18 @@ Definition succ_pred n := eq_sym (Zsucc_pred n). Definition opp_0 := Zopp_0. Definition opp_succ := Zopp_succ. +(** Absolute value and sign *) + +Definition abs_eq := Zabs_eq. +Definition abs_neq := Zabs_non_eq. + +Lemma sgn_null : forall x, x = 0 -> Zsgn x = 0. +Proof. intros. apply <- Zsgn_null; auto. Qed. +Lemma sgn_pos : forall x, 0 < x -> Zsgn x = 1. +Proof. intros. apply <- Zsgn_pos; auto. Qed. +Lemma sgn_neg : forall x, x < 0 -> Zsgn x = -1. +Proof. intros. apply <- Zsgn_neg; auto. Qed. + (** The instantiation of operations. Placing them at the very end avoids having indirections in above lemmas. *) @@ -86,6 +98,8 @@ Definition le := Zle. Definition min := Zmin. Definition max := Zmax. Definition opp := Zopp. +Definition abs := Zabs. +Definition sgn := Zsgn. End ZBinAxiomsMod. diff --git a/theories/Numbers/Integer/SpecViaZ/ZSig.v b/theories/Numbers/Integer/SpecViaZ/ZSig.v index 00e292db0..ef3cd5c34 100644 --- a/theories/Numbers/Integer/SpecViaZ/ZSig.v +++ b/theories/Numbers/Integer/SpecViaZ/ZSig.v @@ -114,4 +114,12 @@ Module Type ZType. Parameter spec_gcd: forall a b, [gcd a b] = Zgcd (to_Z a) (to_Z b). + Parameter sgn : t -> t. + + Parameter spec_sgn : forall x, [sgn x] = Zsgn [x]. + + Parameter abs : t -> t. + + Parameter spec_abs : forall x, [abs x] = Zabs [x]. + End ZType. diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v index 666ce5454..80166d5bf 100644 --- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v +++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v @@ -8,13 +8,11 @@ (*i $Id$ i*) -Require Import ZArith. -Require Import ZAxioms. -Require Import ZSig. +Require Import ZArith ZAxioms ZSgnAbs ZSig. (** * The interface [ZSig.ZType] implies the interface [ZAxiomsSig] *) -Module ZSig_ZAxioms (Z:ZType) <: ZAxiomsSig. +Module ZSig_ZAxioms (Z:ZType) <: ZAxiomsExtSig. Local Notation "[ x ]" := (Z.to_Z x). Local Infix "==" := Z.eq (at level 70). @@ -235,6 +233,36 @@ Proof. intros; zsimpl; auto with zarith. Qed. +Theorem abs_eq : forall n, 0 <= n -> Z.abs n == n. +Proof. +intros. red. rewrite Z.spec_abs. apply Zabs_eq. + rewrite <- Z.spec_0, <- spec_le; auto. +Qed. + +Theorem abs_neq : forall n, n <= 0 -> Z.abs n == -n. +Proof. +intros. red. rewrite Z.spec_abs, Z.spec_opp. apply Zabs_non_eq. + rewrite <- Z.spec_0, <- spec_le; auto. +Qed. + +Theorem sgn_null : forall n, n==0 -> Z.sgn n == 0. +Proof. +intros. red. rewrite Z.spec_sgn, Z.spec_0. rewrite Zsgn_null. + rewrite <- Z.spec_0; auto. +Qed. + +Theorem sgn_pos : forall n, 0<n -> Z.sgn n == Z.succ 0. +Proof. +intros. red. rewrite Z.spec_sgn. zsimpl. rewrite Zsgn_pos. + rewrite <- Z.spec_0, <- spec_lt; auto. +Qed. + +Theorem sgn_neg : forall n, n<0 -> Z.sgn n == Z.opp (Z.succ 0). +Proof. +intros. red. rewrite Z.spec_sgn. zsimpl. rewrite Zsgn_neg. + rewrite <- Z.spec_0, <- spec_lt; auto. +Qed. + (** Aliases *) Definition t := Z.t. @@ -250,5 +278,7 @@ Definition lt := Z.lt. Definition le := Z.le. Definition min := Z.min. Definition max := Z.max. +Definition abs := Z.abs. +Definition sgn := Z.sgn. End ZSig_ZAxioms. diff --git a/theories/Numbers/vo.itarget b/theories/Numbers/vo.itarget index b6d2e42aa..070149a11 100644 --- a/theories/Numbers/vo.itarget +++ b/theories/Numbers/vo.itarget @@ -21,6 +21,7 @@ Integer/Abstract/ZBase.vo Integer/Abstract/ZLt.vo Integer/Abstract/ZMulOrder.vo Integer/Abstract/ZMul.vo +Integer/Abstract/ZSgnAbs.vo Integer/Abstract/ZProperties.vo Integer/Abstract/ZDivFloor.vo Integer/Abstract/ZDivTrunc.vo |