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

2 files changed, 44 insertions, 13 deletions

diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v
index 1ec7960ae4..fc94f693af 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 827877fc5b..0ab509650a 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.