diff options
author | 2010-01-08 17:36:28 +0000 | |
---|---|---|
committer | 2010-01-08 17:36:28 +0000 | |
commit | 6477ab0f7ea03a0563ca7ba2731d6aae1d3aa447 (patch) | |
tree | 32419bbc5c0cf5b03624a2ede42fa3ac0429b0c7 /theories/Numbers/Natural | |
parent | ff01cafe8104f7620aacbfdde5dba738dbadc326 (diff) |
Numbers: BigN and BigZ get instantiations of all properties about div and mod
NB: for declaring div and mod as a morphism, even when divisor is zero,
I've slightly changed the definition of div_eucl: it now starts by a
check of whether the divisor is zero. Not very nice, but this way
we can say that BigN.div and BigZ.div _always_ answer like Zdiv.Zdiv.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12646 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Numbers/Natural')
-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 |
4 files changed, 47 insertions, 25 deletions
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. |