Arith NArith et ZArith exportent ring + nettoyage dans Ring_polynom

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9210 85f007b7-540e-0410-9357-904b9bb8a0f7

9 files changed, 19 insertions, 298 deletions

diff --git a/.depend.coq b/.depend.coq
index 881c88432..e4ec4b5ce 100644
--- a/.depend.coq
+++ b/.depend.coq
@@ -121,14 +121,14 @@ theories/Logic/ClassicalEpsilon.vo: theories/Logic/ClassicalEpsilon.v theories/L
 theories/Logic/ClassicalUniqueChoice.vo: theories/Logic/ClassicalUniqueChoice.v theories/Logic/Classical.vo theories/Setoids/Setoid.vo
 theories/Logic/DecidableType.vo: theories/Logic/DecidableType.v theories/Lists/SetoidList.vo
 theories/Logic/DecidableTypeEx.vo: theories/Logic/DecidableTypeEx.v theories/Logic/DecidableType.vo theories/FSets/OrderedType.vo theories/FSets/OrderedTypeEx.vo
-theories/Arith/Arith.vo: theories/Arith/Arith.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Plus.vo theories/Arith/Gt.vo theories/Arith/Minus.vo theories/Arith/Mult.vo theories/Arith/Between.vo theories/Arith/Peano_dec.vo theories/Arith/Compare_dec.vo theories/Arith/Factorial.vo
+theories/Arith/Arith.vo: theories/Arith/Arith.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Plus.vo theories/Arith/Gt.vo theories/Arith/Minus.vo theories/Arith/Mult.vo theories/Arith/Between.vo theories/Arith/Peano_dec.vo theories/Arith/Compare_dec.vo theories/Arith/Factorial.vo contrib/setoid_ring/ArithRing.vo
 theories/Arith/Gt.vo: theories/Arith/Gt.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Plus.vo
 theories/Arith/Between.vo: theories/Arith/Between.v theories/Arith/Le.vo theories/Arith/Lt.vo
 theories/Arith/Le.vo: theories/Arith/Le.v
 theories/Arith/Compare.vo: theories/Arith/Compare.v theories/Arith/Arith.vo theories/Arith/Peano_dec.vo theories/Arith/Compare_dec.vo theories/Arith/Wf_nat.vo theories/Arith/Min.vo
 theories/Arith/Lt.vo: theories/Arith/Lt.v theories/Arith/Le.vo
 theories/Arith/Compare_dec.vo: theories/Arith/Compare_dec.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Gt.vo theories/Logic/Decidable.vo
-theories/Arith/Min.vo: theories/Arith/Min.v theories/Arith/Arith.vo
+theories/Arith/Min.vo: theories/Arith/Min.v theories/Arith/Le.vo
 theories/Arith/Div2.vo: theories/Arith/Div2.v theories/Arith/Lt.vo theories/Arith/Plus.vo theories/Arith/Compare_dec.vo theories/Arith/Even.vo
 theories/Arith/Minus.vo: theories/Arith/Minus.v theories/Arith/Lt.vo theories/Arith/Le.vo
 theories/Arith/Mult.vo: theories/Arith/Mult.v theories/Arith/Plus.vo theories/Arith/Minus.vo theories/Arith/Lt.vo theories/Arith/Le.vo
@@ -151,7 +151,7 @@ theories/Bool/Bvector.vo: theories/Bool/Bvector.v theories/Bool/Bool.vo theories
 theories/NArith/BinPos.vo: theories/NArith/BinPos.v
 theories/NArith/Pnat.vo: theories/NArith/Pnat.v theories/NArith/BinPos.vo theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Gt.vo theories/Arith/Plus.vo theories/Arith/Mult.vo theories/Arith/Minus.vo
 theories/NArith/BinNat.vo: theories/NArith/BinNat.v theories/NArith/BinPos.vo
-theories/NArith/NArith.vo: theories/NArith/NArith.v theories/NArith/BinPos.vo theories/NArith/BinNat.vo
+theories/NArith/NArith.vo: theories/NArith/NArith.v theories/NArith/BinPos.vo theories/NArith/BinNat.vo contrib/setoid_ring/NArithRing.vo
 theories/NArith/Nnat.vo: theories/NArith/Nnat.v theories/Arith/Arith.vo theories/Arith/Compare_dec.vo theories/Bool/Sumbool.vo theories/Arith/Div2.vo theories/NArith/BinPos.vo theories/NArith/BinNat.vo theories/NArith/Pnat.vo
 theories/NArith/Ndigits.vo: theories/NArith/Ndigits.v theories/Bool/Bool.vo theories/Bool/Bvector.vo theories/NArith/BinPos.vo theories/NArith/BinNat.vo
 theories/NArith/Ndec.vo: theories/NArith/Ndec.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Arith/Arith.vo theories/NArith/BinPos.vo theories/NArith/BinNat.vo theories/NArith/Pnat.vo theories/NArith/Nnat.vo theories/NArith/Ndigits.vo
@@ -366,9 +366,9 @@ contrib/setoid_ring/Ring_tac.vo: contrib/setoid_ring/Ring_tac.v theories/Setoids
 contrib/setoid_ring/Ring_base.vo: contrib/setoid_ring/Ring_base.v contrib/setoid_ring/newring.cmo contrib/setoid_ring/Ring_theory.vo contrib/setoid_ring/Ring_tac.vo
 contrib/setoid_ring/InitialRing.vo: contrib/setoid_ring/InitialRing.v theories/ZArith/ZArith_base.vo theories/ZArith/BinInt.vo theories/NArith/BinNat.vo theories/Setoids/Setoid.vo contrib/setoid_ring/Ring_base.vo contrib/setoid_ring/Ring_polynom.vo
 contrib/setoid_ring/Ring_equiv.vo: contrib/setoid_ring/Ring_equiv.v contrib/ring/Setoid_ring_theory.vo contrib/ring/LegacyRing_theory.vo contrib/setoid_ring/Ring_theory.vo
-contrib/setoid_ring/Ring.vo: contrib/setoid_ring/Ring.v theories/Bool/Bool.vo contrib/setoid_ring/Ring_theory.vo contrib/setoid_ring/Ring_base.vo contrib/setoid_ring/InitialRing.vo contrib/setoid_ring/Ring_equiv.vo
-contrib/setoid_ring/ArithRing.vo: contrib/setoid_ring/ArithRing.v theories/Arith/Arith.vo contrib/setoid_ring/Ring.vo
-contrib/setoid_ring/NArithRing.vo: contrib/setoid_ring/NArithRing.v theories/NArith/NArith.vo contrib/setoid_ring/Ring.vo contrib/setoid_ring/InitialRing.vo
+contrib/setoid_ring/Ring.vo: contrib/setoid_ring/Ring.v theories/Bool/Bool.vo contrib/setoid_ring/Ring_theory.vo contrib/setoid_ring/Ring_base.vo contrib/setoid_ring/InitialRing.vo
+contrib/setoid_ring/ArithRing.vo: contrib/setoid_ring/ArithRing.v theories/Arith/Mult.vo contrib/setoid_ring/Ring_base.vo
+contrib/setoid_ring/NArithRing.vo: contrib/setoid_ring/NArithRing.v theories/NArith/BinPos.vo theories/NArith/BinNat.vo contrib/setoid_ring/Ring_base.vo contrib/setoid_ring/InitialRing.vo
 contrib/setoid_ring/ZArithRing.vo: contrib/setoid_ring/ZArithRing.v contrib/setoid_ring/Ring.vo theories/ZArith/ZArith_base.vo
 contrib/setoid_ring/Field_theory.vo: contrib/setoid_ring/Field_theory.v contrib/setoid_ring/Ring.vo theories/ZArith/ZArith_base.vo
 contrib/setoid_ring/Field_tac.vo: contrib/setoid_ring/Field_tac.v contrib/setoid_ring/Ring_tac.vo contrib/setoid_ring/Ring_polynom.vo contrib/setoid_ring/InitialRing.vo contrib/setoid_ring/Field_theory.vo
diff --git a/contrib/setoid_ring/ArithRing.v b/contrib/setoid_ring/ArithRing.v
index bd4c6062c..70554372a 100644
--- a/contrib/setoid_ring/ArithRing.v
+++ b/contrib/setoid_ring/ArithRing.v
@@ -6,8 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import Arith.
-Require Export Ring.
+Require Import Mult.
+Require Import Ring_base.
 Set Implicit Arguments.
 
 Ltac isnatcst t :=
diff --git a/contrib/setoid_ring/NArithRing.v b/contrib/setoid_ring/NArithRing.v
index abee90b13..92c23e4a5 100644
--- a/contrib/setoid_ring/NArithRing.v
+++ b/contrib/setoid_ring/NArithRing.v
@@ -6,9 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import NArith.
-Require Export Ring.
-Require Import InitialRing.
+Require Import BinPos BinNat.
+Require Import Ring_base InitialRing.
 
 Set Implicit Arguments.
 
diff --git a/contrib/setoid_ring/Ring.v b/contrib/setoid_ring/Ring.v
index 72571c72e..cda2e0e50 100644
--- a/contrib/setoid_ring/Ring.v
+++ b/contrib/setoid_ring/Ring.v
@@ -10,7 +10,6 @@ Require Import Bool.
 Require Export Ring_theory.
 Require Export Ring_base.
 Require Import InitialRing.
-Require Import Ring_equiv.
 
 Lemma BoolTheory :
   ring_theory false true xorb andb xorb (fun b:bool => b) (eq(A:=bool)).
diff --git a/contrib/setoid_ring/Ring_polynom.v b/contrib/setoid_ring/Ring_polynom.v
index a06991c7e..af065ee9f 100644
--- a/contrib/setoid_ring/Ring_polynom.v
+++ b/contrib/setoid_ring/Ring_polynom.v
@@ -917,289 +917,6 @@ Section MakeRingPol.
    forall l pe npe, norm pe = npe -> PEeval l pe == Pphi_dev l npe.
  Proof.
   intros l pe npe npe_eq; subst npe; apply Pphi_dev_gen_ok.
- Qed.
- 
-(* The same but building a PExpr *)
-(*
- Fixpoint Pmkmult (r:PExpr) (lm:list PExpr) {struct lm}: PExpr :=
-  match lm with
-  | nil => r
-  | cons h t => Pmkmult (PEmul r h) t
-  end.
-		       
- Definition Pmkadd_mult rP lm :=
-  match lm with
-  | nil => PEadd rP (PEc cI)
-  | cons h t => PEadd rP (Pmkmult h t)
-  end.
-
- Fixpoint Ppowl (i:positive) (x:PExpr) (l:list PExpr) {struct i}: list PExpr :=
-  match i with
-  | xH => cons x l
-  | xO i => Ppowl i x (Ppowl i x l)
-  | xI i => Ppowl i x (Ppowl i x (cons x l))
-  end.
-			       
- Fixpoint Padd_mult_dev
-     (rP:PExpr) (P:Pol) (fv lm:list PExpr) {struct P} : PExpr :=
-  (* rP + P@l * lm *)
-  match P with
-  | Pc c => if c ?=! cI then Pmkadd_mult rP (rev lm) 
-    else Pmkadd_mult rP (cons [PEc c] (rev lm))
-  | Pinj j Q => Padd_mult_dev rP Q (jump j fv) lm
-  | PX P i Q => 
-     let rP := Padd_mult_dev rP P fv (Ppowl i (hd P0 fv) lm) in
-     if Q ?== P0 then rP else Padd_mult_dev rP Q (tail fv) lm
-  end.
- 
- Definition Pmkmult1 lm :=
-  match lm with
-  | nil => PEc cI
-  | cons h t => Pmkmult h t
-  end.
-   
- Fixpoint Pmult_dev (P:Pol) (fv lm : list PExpr) {struct P} : PExpr :=
-  (* P@l * lm *)							      
-  match P with
-  | Pc c => if c ?=! cI then Pmkmult1 (rev lm) else Pmkmult [PEc c] (rev lm)
-  | Pinj j Q => Pmult_dev Q (jump j fv) lm
-  | PX P i Q => 
-     let rP := Pmult_dev P fv (Ppowl i (hd (PEc r0) fv) lm) in
-     if Q ?== P0 then rP else Padd_mult_dev rP Q (tail fv) lm
-  end. 
-
- Definition Pphi_dev2 fv P := Pmult_dev P fv nil.
-
-...
-*)
-  (************************************************)
- (* avec des parentheses mais un peu plus efficace *)
-
-
- (**************************************************
-
-  Fixpoint pow_mult (i:positive) (x r:R){struct i}:R :=
-  match i with
-  | xH => r * x
-  | xO i => pow_mult i x (pow_mult i x r)
-  | xI i => pow_mult i x (pow_mult i x (r * x))
-  end.
- 
- Definition pow_dev i x :=
-  match i with
-  | xH => x
-  | xO i => pow_mult (Pdouble_minus_one i) x x
-  | xI i => pow_mult (xO i) x x
-  end.
-
- Lemma pow_mult_pow : forall i x r, pow_mult i x r == pow x i * r.
- Proof.
-  induction i;simpl;intros.
-  rewrite (IHi x (pow_mult i x (r * x)));rewrite (IHi x (r*x));rsimpl.
-  mul_push x;rrefl.
-  rewrite (IHi x (pow_mult i x r));rewrite (IHi x r);rsimpl.
-  apply ARth.(ARmul_sym).
- Qed.
-
- Lemma pow_dev_pow : forall p x, pow_dev p x == pow x p.
- Proof.
-  destruct p;simpl;intros.
-  rewrite (pow_mult_pow p x (pow_mult p x x)).
-  rewrite (pow_mult_pow p x x);rsimpl;mul_push x;rrefl.
-  rewrite (pow_mult_pow (Pdouble_minus_one p) x x).
-  rewrite (ARth.(ARmul_sym) (pow x (Pdouble_minus_one p)) x).
-  rewrite <- (pow_Psucc x (Pdouble_minus_one p)).
-  rewrite Psucc_o_double_minus_one_eq_xO;simpl; rrefl.
-  rrefl.
- Qed.
-
- Fixpoint Pphi_dev (fv:list R) (P:Pol) {struct P} : R :=
-  match P with
-  | Pc c => [c]
-  | Pinj j Q => Pphi_dev (jump j fv) Q
-  | PX P i Q => 
-    let rP := mult_dev P fv (pow_dev i (hd 0 fv)) in
-    add_dev rP Q (tail fv)
-  end
-
- with add_dev (ra:R) (P:Pol) (fv:list R) {struct P} : R :=
-   match P with
-  | Pc c => if c ?=! cO then ra else ra + [c] 
-  | Pinj j Q => add_dev ra Q (jump j fv)
-  | PX P i Q =>
-    let ra := add_mult_dev ra P fv (pow_dev i (hd 0 fv)) in
-    add_dev ra Q (tail fv)
-  end
- 
- with mult_dev (P:Pol) (fv:list R) (rm:R) {struct P} : R :=
-  match P with
-  | Pc c => if c ?=! cI then rm else [c]*rm
-  | Pinj j Q => mult_dev Q (jump j fv) rm
-  | PX P i Q =>
-    let ra := mult_dev P fv (pow_mult i (hd 0 fv) rm) in
-    add_mult_dev ra Q (tail fv) rm
-  end
-
- with add_mult_dev (ra:R) (P:Pol) (fv:list R) (rm:R) {struct P} : R :=
-  match P with
-  | Pc c =>  if c ?=! cO then ra else ra + [c]*rm
-  | Pinj j Q => add_mult_dev ra Q (jump j fv) rm
-  | PX P i Q =>
-    let rmP := pow_mult i (hd 0 fv) rm in
-    let raP := add_mult_dev ra P fv rmP in
-    add_mult_dev raP Q (tail fv) rm
-  end.
- 
- Lemma Pphi_add_mult_dev : forall P ra fv rm,
-    add_mult_dev ra P fv rm == ra + P@fv * rm.
- Proof.
-  induction P;simpl;intros.
-  assert (H := CRmorph.(morph_eq) c cO).
-   destruct (c ?=! cO).
-    rewrite (H (refl_equal true));rewrite CRmorph.(morph0);Esimpl.
-    rrefl.
-  apply IHP.
-  rewrite (IHP2 (add_mult_dev ra P2 fv (pow_mult p (hd 0 fv) rm)) (tail fv) rm).
-  rewrite (IHP1 ra fv (pow_mult p (hd 0 fv) rm)).
-  rewrite (pow_mult_pow p (hd 0 fv) rm);rsimpl.
- Qed.
-  
- Lemma Pphi_add_dev : forall P ra fv, add_dev ra P fv == ra + P@fv.
- Proof.
-  induction P;simpl;intros.
-  assert (H := CRmorph.(morph_eq) c cO).
-   destruct (c ?=! cO).
-    rewrite (H (refl_equal true));rewrite CRmorph.(morph0);Esimpl.
-    rrefl.
-  apply IHP.
-  rewrite (IHP2 (add_mult_dev ra P2 fv (pow_dev p (hd 0 fv))) (tail fv)).
-  rewrite (Pphi_add_mult_dev P2 ra fv (pow_dev p (hd 0 fv))).
-  rewrite  (pow_dev_pow p (hd 0 fv));rsimpl. 
- Qed.
-
- Lemma Pphi_mult_dev : forall P fv rm, mult_dev P fv rm == P@fv * rm.
- Proof.
-  induction P;simpl;intros.
-  assert (H := CRmorph.(morph_eq) c cI).
-   destruct (c ?=! cI).
-    rewrite (H (refl_equal true));rewrite CRmorph.(morph1);Esimpl.
-    rrefl.
-  apply IHP.
-  rewrite (Pphi_add_mult_dev P3 
-	    (mult_dev P2 fv (pow_mult p (hd 0 fv) rm)) (tail fv) rm).
-  rewrite (IHP1 fv  (pow_mult p (hd 0 fv) rm)).
-  rewrite (pow_mult_pow p (hd 0 fv) rm);rsimpl.
- Qed.
-
- Lemma Pphi_Pphi_dev : forall P fv, P@fv == Pphi_dev fv P.
- Proof.
-  induction P;simpl;intros.
-  rrefl. trivial.
-  rewrite (Pphi_add_dev P3 (mult_dev P2 fv (pow_dev p (hd 0 fv))) (tail fv)).
-  rewrite (Pphi_mult_dev P2 fv (pow_dev p (hd 0 fv))).
-  rewrite (pow_dev_pow p (hd 0 fv));rsimpl.
- Qed.
-
- Lemma Pphi_dev_ok :  forall l pe,  PEeval l pe == Pphi_dev l (norm pe).
- Proof.
-  intros l pe;rewrite <- (Pphi_Pphi_dev (norm pe) l);apply norm_ok.
- Qed.
-
- Ltac Trev l :=  
-  let rec rev_append rev l :=
-   match l with
-   | (nil _) => constr:(rev)
-   | (cons ?h ?t) => let rev := constr:(cons h rev) in rev_append rev t 
-   end in
- rev_append (@nil R) l.
-
- Ltac TPphi_dev add mul :=
-  let tl l := match l with (cons ?h ?t) => constr:(t) end in
-  let rec jump j l :=
-   match j with
-   | xH => tl l
-   | (xO ?j) => let l := jump j l in jump j l
-   | (xI ?j) => let t := tl l in let l := jump j l in jump j l
-   end in
-  let rec pow_mult i x r :=
-   match i with
-   | xH => constr:(mul r x)
-   | (xO ?i) => let r := pow_mult i x r in pow_mult i x r
-   | (xI ?i) => 
-     let r := constr:(mul r x) in
-     let r := pow_mult i x r in 
-     pow_mult i x r
-   end in
-  let pow_dev i x :=
-   match i with
-   | xH => x
-   | (xO ?i) => 
-      let i := eval compute in (Pdouble_minus_one i) in pow_mult i x x
-   | (xI ?i) => pow_mult (xO i) x x
-   end in
-  let rec add_mult_dev ra P fv rm :=
-   match P with
-   | (Pc ?c) => 
-     match eval compute in (c ?=! cO) with
-     | true => constr:ra 
-     | _ => let rc := eval compute in [c] in constr:(add ra (mul rc rm))
-     end
-   | (Pinj ?j ?Q) => 
-     let fv := jump j fv in add_mult_dev ra Q fv rm
-   | (PX ?P ?i ?Q) =>
-     match fv with 
-     | (cons ?hd ?tl) =>
-       let rmP := pow_mult i hd rm in
-       let raP := add_mult_dev ra P fv rmP in
-       add_mult_dev raP Q tl rm
-     end
-   end in
-  let rec mult_dev P fv rm :=
-   match P with
-   | (Pc ?c) =>
-     match eval compute in (c ?=! cI) with
-     | true => constr:rm 
-     | false => let rc := eval compute in [c] in constr:(mul rc rm)
-     end
-   | (Pinj ?j ?Q) => let fv := jump j fv in mult_dev Q fv rm
-   | (PX ?P ?i ?Q) =>
-     match fv with
-     | (cons ?hd ?tl) =>
-       let rmP := pow_mult i hd rm in
-       let ra := mult_dev P fv rmP in
-       add_mult_dev ra Q tl rm
-     end
-   end in
-  let rec add_dev ra P fv :=
-   match P with
-   | (Pc ?c) =>
-     match eval compute in (c ?=! cO) with
-     | true => ra
-     | false => let rc := eval compute in [c] in constr:(add ra rc)
-     end
-   | (Pinj ?j ?Q) => let fv := jump j fv in add_dev ra Q fv
-   | (PX ?P ?i ?Q) =>
-     match fv with
-     | (cons ?hd ?tl) =>
-       let rmP := pow_dev i hd in
-       let ra := add_mult_dev ra P fv rmP in
-       add_dev ra Q tl
-     end
-   end in
-  let rec Pphi_dev fv P :=
-   match P with
-   | (Pc ?c) => eval compute in [c]
-   | (Pinj ?j ?Q) => let fv := jump j fv in Pphi_dev fv Q
-   | (PX ?P ?i ?Q) =>
-     match fv with
-     | (cons ?hd ?tl) =>
-       let rm := pow_dev i hd in
-       let rP := mult_dev P fv rm in
-       add_dev rP Q tl
-     end
-   end in
-  Pphi_dev.
- 
- **************************************************************)
+ Qed. 
 
 End MakeRingPol. 
diff --git a/theories/Arith/Arith.v b/theories/Arith/Arith.v
index b076de2af..c522e01b3 100644
--- a/theories/Arith/Arith.v
+++ b/theories/Arith/Arith.v
@@ -18,3 +18,5 @@ Require Export Between.
 Require Export Peano_dec.
 Require Export Compare_dec.
 Require Export Factorial.
+
+Require Export ArithRing.
diff --git a/theories/Arith/Min.v b/theories/Arith/Min.v
index 3e64980cb..d86d7f116 100644
--- a/theories/Arith/Min.v
+++ b/theories/Arith/Min.v
@@ -8,7 +8,7 @@
 
 (*i $Id$ i*)
 
-Require Import Arith.
+Require Import Le.
 
 Open Local Scope nat_scope.
 
diff --git a/theories/NArith/NArith.v b/theories/NArith/NArith.v
index a37387792..5a2eeda48 100644
--- a/theories/NArith/NArith.v
+++ b/theories/NArith/NArith.v
@@ -11,4 +11,6 @@
 (** Library for binary natural numbers *)
 
 Require Export BinPos.
-Require Export BinNat.
\ No newline at end of file
+Require Export BinNat.
+
+Require Export NArithRing.
diff --git a/theories/ZArith/ZArith.v b/theories/ZArith/ZArith.v
index 169a253fe..5747afc9a 100644
--- a/theories/ZArith/ZArith.v
+++ b/theories/ZArith/ZArith.v
@@ -19,3 +19,5 @@ Require Export Zsqrt.
 Require Export Zpower.
 Require Export Zdiv.
 Require Export Zlogarithm.
+
+Export ZArithRing.