diff options
author | 2006-10-05 10:12:15 +0000 | |
---|---|---|
committer | 2006-10-05 10:12:15 +0000 | |
commit | 4524219d80c2d5ea50ca8bba819bbc14bd6b9988 (patch) | |
tree | f5204b39bba079321a8c6a21d400f5f84f9d9c91 /contrib | |
parent | 685d10fa1691ced3b44f77ae8587e0b27f57810b (diff) |
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
Diffstat (limited to 'contrib')
-rw-r--r-- | contrib/setoid_ring/ArithRing.v | 4 | ||||
-rw-r--r-- | contrib/setoid_ring/NArithRing.v | 5 | ||||
-rw-r--r-- | contrib/setoid_ring/Ring.v | 1 | ||||
-rw-r--r-- | contrib/setoid_ring/Ring_polynom.v | 285 |
4 files changed, 5 insertions, 290 deletions
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. |