diff options
-rw-r--r-- | theories/Numbers/Integer/BigZ/BigZ.v | 7 | ||||
-rw-r--r-- | theories/Numbers/Integer/BigZ/ZMake.v | 50 | ||||
-rw-r--r-- | theories/Numbers/Integer/SpecViaZ/ZSig.v | 7 | ||||
-rw-r--r-- | theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v | 55 | ||||
-rw-r--r-- | theories/Numbers/NatInt/NZDiv.v | 2 | ||||
-rw-r--r-- | theories/Numbers/Natural/BigN/BigN.v | 9 | ||||
-rw-r--r-- | theories/Numbers/Natural/BigN/NMake_gen.ml | 27 | ||||
-rw-r--r-- | theories/Numbers/Natural/SpecViaZ/NSig.v | 8 | ||||
-rw-r--r-- | theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v | 28 |
9 files changed, 136 insertions, 57 deletions
diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v index 1ec7960ae..fc94f693a 100644 --- a/theories/Numbers/Integer/BigZ/BigZ.v +++ b/theories/Numbers/Integer/BigZ/BigZ.v @@ -11,10 +11,7 @@ (*i $Id$ i*) Require Export BigN. -Require Import ZProperties. -Require Import ZSig. -Require Import ZSigZAxioms. -Require Import ZMake. +Require Import ZProperties ZDivFloor ZSig ZSigZAxioms ZMake. Module BigZ <: ZType := ZMake.Make BigN. @@ -22,6 +19,7 @@ Module BigZ <: ZType := ZMake.Make BigN. Module Export BigZAxiomsMod := ZSig_ZAxioms BigZ. Module Export BigZPropMod := ZPropFunct BigZAxiomsMod. +Module Export BigZDivPropMod := ZDivPropFunct BigZAxiomsMod BigZPropMod. (** Notations about [BigZ] *) @@ -71,6 +69,7 @@ Infix "<=" := BigZ.le : bigZ_scope. Notation "x > y" := (BigZ.lt y x)(only parsing) : bigZ_scope. Notation "x >= y" := (BigZ.le y x)(only parsing) : bigZ_scope. Notation "[ i ]" := (BigZ.to_Z i) : bigZ_scope. +Infix "mod" := modulo (at level 40, no associativity) : bigN_scope. Local Open Scope bigZ_scope. diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v index 827877fc5..0ab509650 100644 --- a/theories/Numbers/Integer/BigZ/ZMake.v +++ b/theories/Numbers/Integer/BigZ/ZMake.v @@ -369,17 +369,17 @@ Module Make (N:NType) <: ZType. end. - Theorem spec_div_eucl: forall x y, + Theorem spec_div_eucl_nz: forall x y, to_Z y <> 0 -> let (q,r) := div_eucl x y in (to_Z q, to_Z r) = Zdiv_eucl (to_Z x) (to_Z y). unfold div_eucl, to_Z; intros [x | x] [y | y] H. assert (H1: 0 < N.to_Z y). generalize (N.spec_pos y); auto with zarith. - generalize (N.spec_div_eucl x y H1); case N.div_eucl; auto. + generalize (N.spec_div_eucl x y); case N.div_eucl; auto. assert (HH: 0 < N.to_Z y). generalize (N.spec_pos y); auto with zarith. - generalize (N.spec_div_eucl x y HH); case N.div_eucl; auto. + generalize (N.spec_div_eucl x y); case N.div_eucl; auto. intros q r; generalize (N.spec_pos x) HH; unfold Zdiv_eucl; case_eq (N.to_Z x); case_eq (N.to_Z y); try (intros; apply False_ind; auto with zarith; fail). @@ -411,7 +411,7 @@ Module Make (N:NType) <: ZType. intros; apply False_ind; auto with zarith. assert (HH: 0 < N.to_Z y). generalize (N.spec_pos y); auto with zarith. - generalize (N.spec_div_eucl x y HH); case N.div_eucl; auto. + generalize (N.spec_div_eucl x y); case N.div_eucl; auto. intros q r; generalize (N.spec_pos x) HH; unfold Zdiv_eucl; case_eq (N.to_Z x); case_eq (N.to_Z y); try (intros; apply False_ind; auto with zarith; fail). @@ -441,7 +441,7 @@ Module Make (N:NType) <: ZType. rewrite N.spec_0; generalize (N.spec_pos r); intros; apply False_ind; auto with zarith. assert (H1: 0 < N.to_Z y). generalize (N.spec_pos y); auto with zarith. - generalize (N.spec_div_eucl x y H1); case N.div_eucl; auto. + generalize (N.spec_div_eucl x y); case N.div_eucl; auto. intros q r; generalize (N.spec_pos x) H1; unfold Zdiv_eucl; case_eq (N.to_Z x); case_eq (N.to_Z y); try (intros; apply False_ind; auto with zarith; fail). @@ -455,11 +455,43 @@ Module Make (N:NType) <: ZType. rewrite <- H2; auto. Qed. + Lemma Zdiv_eucl_0 : forall a, Zdiv_eucl a 0 = (0,0). + Proof. destruct a; auto. Qed. + + Theorem spec_div_eucl: forall x y, + let (q,r) := div_eucl x y in + (to_Z q, to_Z r) = Zdiv_eucl (to_Z x) (to_Z y). + Proof. + intros. destruct (Z_eq_dec (to_Z y) 0) as [EQ|NEQ]; + [|apply spec_div_eucl_nz; auto]. + unfold div_eucl. + destruct x; destruct y; simpl in *. + generalize (N.spec_div_eucl t0 t1). destruct N.div_eucl; simpl; auto. + generalize (N.spec_div_eucl t0 t1). destruct N.div_eucl; simpl; auto. + assert (EQ' : N.to_Z t1 = 0) by auto with zarith. + rewrite EQ'. simpl. rewrite Zdiv_eucl_0. injection 1; intros. + generalize (N.spec_compare N.zero t3); destruct N.compare. + simpl. intros. f_equal; auto with zarith. + rewrite N.spec_0; intro; exfalso; auto with zarith. + rewrite N.spec_0; intro; exfalso; auto with zarith. + generalize (N.spec_div_eucl t0 t1). destruct N.div_eucl; simpl; auto. + assert (EQ' : N.to_Z t1 = 0) by auto with zarith. + rewrite EQ'. simpl. rewrite 2 Zdiv_eucl_0. injection 1; intros. + generalize (N.spec_compare N.zero t3); destruct N.compare. + simpl. intros. f_equal; auto with zarith. + rewrite N.spec_0; intro; exfalso; auto with zarith. + rewrite N.spec_0; intro; exfalso; auto with zarith. + generalize (N.spec_div_eucl t0 t1). destruct N.div_eucl; simpl; auto. + assert (EQ' : N.to_Z t1 = 0) by auto with zarith. + rewrite EQ'. simpl. rewrite 2 Zdiv_eucl_0. injection 1; intros. + f_equal; auto with zarith. + Qed. + Definition div x y := fst (div_eucl x y). Definition spec_div: forall x y, - to_Z y <> 0 -> to_Z (div x y) = to_Z x / to_Z y. - intros x y H1; generalize (spec_div_eucl x y H1); unfold div, Zdiv. + to_Z (div x y) = to_Z x / to_Z y. + intros x y; generalize (spec_div_eucl x y); unfold div, Zdiv. case div_eucl; case Zdiv_eucl; simpl; auto. intros q r q11 r1 H; injection H; auto. Qed. @@ -467,8 +499,8 @@ Module Make (N:NType) <: ZType. Definition modulo x y := snd (div_eucl x y). Theorem spec_modulo: - forall x y, to_Z y <> 0 -> to_Z (modulo x y) = to_Z x mod to_Z y. - intros x y H1; generalize (spec_div_eucl x y H1); unfold modulo, Zmod. + forall x y, to_Z (modulo x y) = to_Z x mod to_Z y. + intros x y; generalize (spec_div_eucl x y); unfold modulo, Zmod. case div_eucl; case Zdiv_eucl; simpl; auto. intros q r q11 r1 H; injection H; auto. Qed. diff --git a/theories/Numbers/Integer/SpecViaZ/ZSig.v b/theories/Numbers/Integer/SpecViaZ/ZSig.v index ef3cd5c34..a7c5473aa 100644 --- a/theories/Numbers/Integer/SpecViaZ/ZSig.v +++ b/theories/Numbers/Integer/SpecViaZ/ZSig.v @@ -98,17 +98,16 @@ Module Type ZType. Parameter div_eucl : t -> t -> t * t. - Parameter spec_div_eucl: forall x y, [y] <> 0 -> + Parameter spec_div_eucl: forall x y, let (q,r) := div_eucl x y in ([q], [r]) = Zdiv_eucl [x] [y]. Parameter div : t -> t -> t. - Parameter spec_div: forall x y, [y] <> 0 -> [div x y] = [x] / [y]. + Parameter spec_div: forall x y, [div x y] = [x] / [y]. Parameter modulo : t -> t -> t. - Parameter spec_modulo: forall x y, [y] <> 0 -> - [modulo x y] = [x] mod [y]. + Parameter spec_modulo: forall x y, [modulo x y] = [x] mod [y]. Parameter gcd : t -> t -> t. diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v index 80166d5bf..cb5a771da 100644 --- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v +++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v @@ -8,11 +8,15 @@ (*i $Id$ i*) -Require Import ZArith ZAxioms ZSgnAbs ZSig. +Require Import ZArith ZAxioms ZDivFloor ZSig. -(** * The interface [ZSig.ZType] implies the interface [ZAxiomsSig] *) +(** * The interface [ZSig.ZType] implies the interface [ZAxiomsSig] -Module ZSig_ZAxioms (Z:ZType) <: ZAxiomsExtSig. + It also provides [sgn], [abs], [div], [mod] +*) + + +Module ZSig_ZAxioms (Z:ZType) <: ZAxiomsSig <: ZDivSig. Local Notation "[ x ]" := (Z.to_Z x). Local Infix "==" := Z.eq (at level 70). @@ -26,7 +30,7 @@ Local Infix "<" := Z.lt. Hint Rewrite Z.spec_0 Z.spec_1 Z.spec_add Z.spec_sub Z.spec_pred Z.spec_succ - Z.spec_mul Z.spec_opp Z.spec_of_Z : zspec. + Z.spec_mul Z.spec_opp Z.spec_of_Z Z.spec_div Z.spec_modulo: zspec. Ltac zsimpl := unfold Z.eq in *; autorewrite with zspec. Ltac zcongruence := repeat red; intros; zsimpl; congruence. @@ -235,32 +239,53 @@ 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. +intros n. red. rewrite spec_le, Z.spec_0, Z.spec_abs. apply Zabs_eq. 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. +intros n. red. rewrite spec_le, Z.spec_0, Z.spec_abs, Z.spec_opp. + apply Zabs_non_eq. 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. +intros n. unfold Z.eq. rewrite Z.spec_sgn, Z.spec_0. rewrite Zsgn_null; 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. +intros n. red. rewrite spec_lt, Z.spec_sgn. zsimpl. rewrite Zsgn_pos; 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. +intros n. red. rewrite spec_lt, Z.spec_sgn. zsimpl. rewrite Zsgn_neg; auto. +Qed. + +Program Instance div_wd : Proper (Z.eq==>Z.eq==>Z.eq) Z.div. +Program Instance mod_wd : Proper (Z.eq==>Z.eq==>Z.eq) Z.modulo. + +Theorem div_mod : forall a b, ~b==0 -> a == b*(Z.div a b) + (Z.modulo a b). +Proof. +intros a b. unfold Z.eq; zsimpl. intros. +apply Z_div_mod_eq_full; auto. +Qed. + +Theorem mod_pos_bound : + forall a b, 0 < b -> 0 <= Z.modulo a b /\ Z.modulo a b < b. +Proof. +intros a b. rewrite 2 spec_lt, spec_le, Z.spec_0. intros. +rewrite Z.spec_modulo; auto with zarith. +apply Z_mod_lt; auto with zarith. +Qed. + +Theorem mod_neg_bound : + forall a b, b < 0 -> b < Z.modulo a b /\ Z.modulo a b <= 0. +Proof. +intros a b. rewrite 2 spec_lt, spec_le, Z.spec_0. intros. +rewrite Z.spec_modulo; auto with zarith. +apply Z_mod_neg; auto with zarith. Qed. (** Aliases *) @@ -280,5 +305,7 @@ Definition min := Z.min. Definition max := Z.max. Definition abs := Z.abs. Definition sgn := Z.sgn. +Definition div := Z.div. +Definition modulo := Z.modulo. End ZSig_ZAxioms. diff --git a/theories/Numbers/NatInt/NZDiv.v b/theories/Numbers/NatInt/NZDiv.v index 4acd6540d..b189d5b29 100644 --- a/theories/Numbers/NatInt/NZDiv.v +++ b/theories/Numbers/NatInt/NZDiv.v @@ -13,7 +13,7 @@ Require Import NZAxioms NZMulOrder. (** The first signatures will be common to all divisions over NZ, N and Z *) Module Type DivMod (Import T:Typ). - Parameters div modulo : t -> t -> t. + Parameters Inline div modulo : t -> t -> t. End DivMod. Module Type DivModNotation (T:Typ)(Import NZ:DivMod T). diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v index bc2f3ecdf..b87056a63 100644 --- a/theories/Numbers/Natural/BigN/BigN.v +++ b/theories/Numbers/Natural/BigN/BigN.v @@ -15,12 +15,7 @@ Author: Arnaud Spiwack *) Require Export Int31. -Require Import CyclicAxioms. -Require Import Cyclic31. -Require Import NSig. -Require Import NSigNAxioms. -Require Import NMake. -Require Import NProperties. +Require Import CyclicAxioms Cyclic31 NSig NSigNAxioms NMake NProperties NDiv. Module BigN <: NType := NMake.Make Int31Cyclic. @@ -28,6 +23,7 @@ Module BigN <: NType := NMake.Make Int31Cyclic. Module Export BigNAxiomsMod := NSig_NAxioms BigN. Module Export BigNPropMod := NPropFunct BigNAxiomsMod. +Module Export BigDivModProp := NDivPropFunct BigNAxiomsMod BigNPropMod. (** Notations about [BigN] *) @@ -73,6 +69,7 @@ Infix "<=" := BigN.le : bigN_scope. Notation "x > y" := (BigN.lt y x)(only parsing) : bigN_scope. Notation "x >= y" := (BigN.le y x)(only parsing) : bigN_scope. Notation "[ i ]" := (BigN.to_Z i) : bigN_scope. +Infix "mod" := modulo (at level 40, no associativity) : bigN_scope. Local Open Scope bigN_scope. diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml index 769d804d7..b8e879c66 100644 --- a/theories/Numbers/Natural/BigN/NMake_gen.ml +++ b/theories/Numbers/Natural/BigN/NMake_gen.ml @@ -1956,6 +1956,7 @@ let _ = pr ""; pr " Definition div_eucl x y :="; + pr " if eq_bool y zero then (zero,zero) else"; pr " match compare x y with"; pr " | Eq => (one, zero)"; pr " | Lt => (zero, x)"; @@ -1964,7 +1965,6 @@ let _ = pr ""; pr " Theorem spec_div_eucl: forall x y,"; - pr " 0 < [y] ->"; pr " let (q,r) := div_eucl x y in"; pr " ([q], [r]) = Zdiv_eucl [x] [y]."; pa " Admitted."; @@ -1973,8 +1973,13 @@ let _ = pp " exact (spec_0 w0_spec)."; pp " assert (F1: [one] = 1)."; pp " exact (spec_1 w0_spec)."; - pp " intros x y H; generalize (spec_compare x y);"; - pp " unfold div_eucl; case compare; try rewrite F0;"; + pp " intros x y. unfold div_eucl."; + pp " generalize (spec_eq_bool y zero). destruct eq_bool; rewrite F0."; + pp " intro H. rewrite H. destruct [x]; auto."; + pp " intro H'."; + pp " assert (0 < [y]) by (generalize (spec_pos y); auto with zarith)."; + pp " clear H'."; + pp " generalize (spec_compare x y); case compare; try rewrite F0;"; pp " try rewrite F1; intros; auto with zarith."; pp " rewrite H0; generalize (Z_div_same [y] (Zlt_gt _ _ H))"; pp " (Z_mod_same [y] (Zlt_gt _ _ H));"; @@ -1994,10 +1999,10 @@ let _ = pr ""; pr " Theorem spec_div:"; - pr " forall x y, 0 < [y] -> [div x y] = [x] / [y]."; + pr " forall x y, [div x y] = [x] / [y]."; pa " Admitted."; pp " Proof."; - pp " intros x y H1; unfold div; generalize (spec_div_eucl x y H1);"; + pp " intros x y; unfold div; generalize (spec_div_eucl x y);"; pp " case div_eucl; simpl fst."; pp " intros xx yy; unfold Zdiv; case Zdiv_eucl; intros qq rr H; "; pp " injection H; auto."; @@ -2099,6 +2104,7 @@ let _ = pr ""; pr " Definition modulo x y := "; + pr " if eq_bool y zero then zero else"; pr " match compare x y with"; pr " | Eq => zero"; pr " | Lt => x"; @@ -2107,15 +2113,20 @@ let _ = pr ""; pr " Theorem spec_modulo:"; - pr " forall x y, 0 < [y] -> [modulo x y] = [x] mod [y]."; + pr " forall x y, [modulo x y] = [x] mod [y]."; pa " Admitted."; pp " Proof."; pp " assert (F0: [zero] = 0)."; pp " exact (spec_0 w0_spec)."; pp " assert (F1: [one] = 1)."; pp " exact (spec_1 w0_spec)."; - pp " intros x y H; generalize (spec_compare x y);"; - pp " unfold modulo; case compare; try rewrite F0;"; + pp " intros x y. unfold modulo."; + pp " generalize (spec_eq_bool y zero). destruct eq_bool; rewrite F0."; + pp " intro H; rewrite H. destruct [x]; auto."; + pp " intro H'."; + pp " assert (H : 0 < [y]) by (generalize (spec_pos y); auto with zarith)."; + pp " clear H'."; + pp " generalize (spec_compare x y); case compare; try rewrite F0;"; pp " try rewrite F1; intros; try split; auto with zarith."; pp " rewrite H0; apply sym_equal; apply Z_mod_same; auto with zarith."; pp " apply sym_equal; apply Zmod_small; auto with zarith."; diff --git a/theories/Numbers/Natural/SpecViaZ/NSig.v b/theories/Numbers/Natural/SpecViaZ/NSig.v index 2dfa783aa..ecb49d32d 100644 --- a/theories/Numbers/Natural/SpecViaZ/NSig.v +++ b/theories/Numbers/Natural/SpecViaZ/NSig.v @@ -94,17 +94,15 @@ Module Type NType. Parameter div_eucl : t -> t -> t * t. Parameter spec_div_eucl: forall x y, - 0 < [y] -> - let (q,r) := div_eucl x y in ([q], [r]) = Zdiv_eucl [x] [y]. + let (q,r) := div_eucl x y in ([q], [r]) = Zdiv_eucl [x] [y]. Parameter div : t -> t -> t. - Parameter spec_div: forall x y, 0 < [y] -> [div x y] = [x] / [y]. + Parameter spec_div: forall x y, [div x y] = [x] / [y]. Parameter modulo : t -> t -> t. - Parameter spec_modulo: - forall x y, 0 < [y] -> [modulo x y] = [x] mod [y]. + Parameter spec_modulo: forall x y, [modulo x y] = [x] mod [y]. Parameter gcd : t -> t -> t. diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v index 66d3a89c2..8a34185d9 100644 --- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v +++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v @@ -8,14 +8,11 @@ (*i $Id$ i*) -Require Import ZArith. -Require Import Nnat. -Require Import NAxioms. -Require Import NSig. +Require Import ZArith Nnat NAxioms NDiv NSig. (** * The interface [NSig.NType] implies the interface [NAxiomsSig] *) -Module NSig_NAxioms (N:NType) <: NAxiomsSig. +Module NSig_NAxioms (N:NType) <: NAxiomsSig <: NDivSig. Delimit Scope NumScope with Num. Bind Scope NumScope with N.t. @@ -28,7 +25,8 @@ Local Infix "-" := N.sub : NumScope. Local Infix "*" := N.mul : NumScope. Hint Rewrite - N.spec_0 N.spec_succ N.spec_add N.spec_mul N.spec_pred N.spec_sub : num. + N.spec_0 N.spec_succ N.spec_add N.spec_mul N.spec_pred N.spec_sub + N.spec_div N.spec_modulo : num. Ltac nsimpl := autorewrite with num. Ltac ncongruence := unfold N.eq; repeat red; intros; nsimpl; congruence. @@ -212,6 +210,22 @@ Proof. red; nsimpl; auto. Qed. +Program Instance div_wd : Proper (N.eq==>N.eq==>N.eq) N.div. +Program Instance mod_wd : Proper (N.eq==>N.eq==>N.eq) N.modulo. + +Theorem div_mod : forall a b, ~b==0 -> a == b*(N.div a b) + (N.modulo a b). +Proof. +intros a b. unfold N.eq. nsimpl. intros. +apply Z_div_mod_eq_full; auto. +Qed. + +Theorem mod_upper_bound : forall a b, ~b==0 -> N.modulo a b < b. +Proof. +intros a b. unfold N.eq. rewrite spec_lt. nsimpl. intros. +destruct (Z_mod_lt [a] [b]); auto. +generalize (N.spec_pos b); auto with zarith. +Qed. + Definition recursion (A : Type) (a : A) (f : N.t -> A -> A) (n : N.t) := Nrect (fun _ => A) a (fun n a => f (N.of_N n) a) (N.to_N n). Implicit Arguments recursion [A]. @@ -282,5 +296,7 @@ Definition lt := N.lt. Definition le := N.le. Definition min := N.min. Definition max := N.max. +Definition div := N.div. +Definition modulo := N.modulo. End NSig_NAxioms. |