From 6477ab0f7ea03a0563ca7ba2731d6aae1d3aa447 Mon Sep 17 00:00:00 2001 From: letouzey Date: Fri, 8 Jan 2010 17:36:28 +0000 Subject: 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 --- theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v | 28 +++++++++++++++++++------ 1 file changed, 22 insertions(+), 6 deletions(-) (limited to 'theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v') 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. -- cgit v1.2.3