Remove duplicate conditions in Field + Monomial substitution function for PExpr

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

2 files changed, 558 insertions, 17 deletions

diff --git a/contrib/setoid_ring/Field_theory.v b/contrib/setoid_ring/Field_theory.v
index fd054f5d2..206367ba2 100644
--- a/contrib/setoid_ring/Field_theory.v
+++ b/contrib/setoid_ring/Field_theory.v
@@ -198,6 +198,27 @@ apply (Radd_ext Reqe).
    transitivity (r2 * r3); auto.
 Qed.
 
+
+Theorem rdiv2b:
+ forall r1 r2 r3 r4 r5,
+ ~ (r2*r5) == 0 ->
+ ~ (r4*r5) == 0 ->
+ r1 / (r2*r5) + r3 / (r4*r5) == (r1 * r4 + r3 * r2) / (r2 * (r4 * r5)).
+Proof.
+intros r1 r2 r3 r4 r5 H H0.
+assert (HH1: ~ r2 == 0) by (intros HH; case H; rewrite HH; ring).
+assert (HH2: ~ r5 == 0) by (intros HH; case H; rewrite HH; ring).
+assert (HH3: ~ r4 == 0) by (intros HH; case H0; rewrite HH; ring).
+assert (HH4: ~ r2 * (r4 * r5) == 0) 
+   by complete (repeat apply field_is_integral_domain; trivial).
+apply rmul_reg_l with (r2 * (r4 * r5)); trivial.
+rewrite rdiv_simpl in |- *; trivial.
+rewrite (ARdistr_r Rsth Reqe ARth) in |- *.
+apply (Radd_ext Reqe).
+ transitivity ((r2 * r5) * (r1 / (r2 * r5)) * r4); [  ring | auto ].
+ transitivity ((r4 * r5) * (r3 / (r4 * r5)) * r2); [  ring | auto ].
+Qed.
+
 Theorem rdiv5: forall r1 r2,  - (r1 / r2) == - r1 / r2.
 intros r1 r2.
 transitivity (- (r1 * / r2)); auto.
@@ -220,6 +241,22 @@ apply SRdiv_ext; auto.
 transitivity (r1 * r4 + - (r3 * r2)); symmetry; auto.
 Qed.
 
+
+Theorem rdiv3b:
+ forall r1 r2 r3 r4 r5,
+ ~ (r2 * r5) == 0 ->
+ ~ (r4 * r5) == 0 ->
+ r1 / (r2*r5) - r3 / (r4*r5) == (r1 * r4 - r3 * r2) / (r2 * (r4 * r5)).
+Proof.
+intros r1 r2 r3 r4 r5 H H0.
+transitivity (r1 / (r2 * r5) + - (r3 / (r4 * r5))); auto.
+transitivity (r1 / (r2 * r5) + - r3 / (r4 * r5)); auto.
+transitivity ((r1 * r4 + - r3 * r2) / (r2 * (r4 * r5))).
+apply rdiv2b; auto; try ring.
+apply (SRdiv_ext); auto.
+transitivity (r1 * r4 + - (r3 * r2)); symmetry; auto.
+Qed.
+
 Theorem rdiv6:
  forall r1 r2,
  ~ r1 == 0 -> ~ r2 == 0 ->  / (r1 / r2) == r2 / r1.
@@ -547,24 +584,176 @@ Qed.
                                                                           
   ***************************************************************************)
 
-Fixpoint Fnorm (e : FExpr) : linear :=
+
+Fixpoint isIn (e1 e2: PExpr C) {struct e2}: option (PExpr C) :=
+  match e2 with
+  | PEmul e3 e4 =>
+       match isIn e1 e3 with
+         Some e5 => Some (NPEmul e5 e4)
+       | None => match isIn e1 e4 with
+                 | Some e5 => Some (NPEmul e3 e5)
+                 | None => None
+                 end
+       end
+  | _ =>
+       if PExpr_eq e1 e2 then Some (PEc cI) else None
+   end.
+
+Theorem isIn_correct: forall l e1 e2,
+  match isIn e1 e2 with 
+    (Some e3) => NPEeval l e2 == NPEeval l (NPEmul e1 e3)
+  |  _ => True
+  end.
+Proof.
+intros l e1 e2; elim e2; simpl; auto.
+  intros c;
+   generalize (PExpr_eq_semi_correct l e1 (PEc c));
+   case (PExpr_eq e1 (PEc c)); simpl; auto; intros H.
+   rewrite NPEmul_correct; simpl; auto.
+   rewrite H; auto; simpl. 
+   rewrite (morph1 CRmorph); rewrite (ARmul_1_r Rsth ARth); auto.
+  intros p;
+   generalize (PExpr_eq_semi_correct l e1 (PEX C p));
+   case (PExpr_eq e1 (PEX C p)); simpl; auto; intros H.
+   rewrite NPEmul_correct; simpl; auto.
+   rewrite H; auto; simpl. 
+   rewrite (morph1 CRmorph); rewrite (ARmul_1_r Rsth ARth); auto.
+ intros p Hrec p1 Hrec1.
+   generalize (PExpr_eq_semi_correct l e1 (PEadd p p1));
+   case (PExpr_eq e1 (PEadd p p1)); simpl; auto; intros H.
+   rewrite NPEmul_correct; simpl; auto.
+   rewrite H; auto; simpl. 
+   rewrite (morph1 CRmorph); rewrite (ARmul_1_r Rsth ARth); auto.
+ intros p Hrec p1 Hrec1.
+   generalize (PExpr_eq_semi_correct l e1 (PEsub p p1));
+   case (PExpr_eq e1 (PEsub p p1)); simpl; auto; intros H.
+   rewrite NPEmul_correct; simpl; auto.
+   rewrite H; auto; simpl. 
+   rewrite (morph1 CRmorph); rewrite (ARmul_1_r Rsth ARth); auto.
+ intros p; case (isIn e1 p).
+   intros p2 Hrec p1 Hrec1.
+   rewrite Hrec; auto; simpl. 
+   repeat (rewrite NPEmul_correct; simpl; auto).
+   intros _ p1; case (isIn e1 p1); auto.
+   intros p2 H; rewrite H.
+   repeat (rewrite NPEmul_correct; simpl; auto).
+   ring.
+  intros p;
+   generalize (PExpr_eq_semi_correct l e1 (PEopp p));
+   case (PExpr_eq e1 (PEopp p)); simpl; auto; intros H.
+   rewrite NPEmul_correct; simpl; auto.
+   rewrite H; auto; simpl. 
+   rewrite (morph1 CRmorph); rewrite (ARmul_1_r Rsth ARth); auto.
+Qed.
+
+Record rsplit : Type := mk_rsplit {
+   left : PExpr C;
+   common : PExpr C;
+   right : PExpr C}.
+
+
+Fixpoint split (e1 e2: PExpr C) {struct e1}: rsplit :=
+  match e1 with
+  | PEmul e3 e4 =>
+      let r1 := split e3 e2 in
+      let r2 := split e4 (right r1) in
+          mk_rsplit (NPEmul (left r1) (left r2))
+                    (NPEmul (common r1) (common r2))
+                    (right r2)
+  | _ => 
+       match isIn e1 e2 with
+         Some e3 => mk_rsplit (PEc cI) e1 e3
+       | None => mk_rsplit e1 (PEc cI) e2
+       end
+  end. 
+
+Theorem split_correct: forall l e1 e2,
+  NPEeval l e1 == NPEeval l (NPEmul (left (split e1 e2))
+                                   (common (split e1 e2)))
+/\
+  NPEeval l e2 == NPEeval l (NPEmul (right (split e1 e2))
+                                   (common (split e1 e2))).
+Proof.
+intros l e1; elim e1; simpl; auto.
+  intros c e2; generalize (isIn_correct l (PEc c) e2);
+    case (isIn (PEc c) e2); auto; intros p;
+    [intros Hp1; rewrite Hp1 | idtac];
+    simpl left; simpl common;  simpl right; auto;
+    repeat rewrite NPEmul_correct; simpl; split; 
+    try rewrite  (morph1 CRmorph); ring.
+  intros p e2; generalize (isIn_correct l (PEX C p) e2);
+    case (isIn (PEX C p) e2); auto; intros p1;
+    [intros Hp1; rewrite Hp1 | idtac];
+    simpl left; simpl common;  simpl right; auto;
+    repeat rewrite NPEmul_correct; simpl; split; 
+    try rewrite  (morph1 CRmorph); ring.
+  intros p1 _ p2 _ e2; generalize (isIn_correct l (PEadd p1 p2) e2);
+    case (isIn (PEadd p1 p2) e2); auto; intros p;
+    [intros Hp1; rewrite Hp1 | idtac];
+    simpl left; simpl common;  simpl right; auto;
+    repeat rewrite NPEmul_correct; simpl; split; 
+    try rewrite  (morph1 CRmorph); ring.
+  intros p1 _ p2 _ e2; generalize (isIn_correct l (PEsub p1 p2) e2);
+    case (isIn (PEsub p1 p2) e2); auto; intros p;
+    [intros Hp1; rewrite Hp1 | idtac];
+    simpl left; simpl common;  simpl right; auto;
+    repeat rewrite NPEmul_correct; simpl; split; 
+    try rewrite  (morph1 CRmorph); ring.
+  intros p1 Hp1 p2 Hp2 e2.
+    repeat rewrite NPEmul_correct; simpl; split.
+    case (Hp1 e2); case (Hp2 (right (split p1 e2))).
+    intros tmp1 _ tmp2 _; rewrite tmp1; rewrite tmp2.
+    repeat rewrite NPEmul_correct; simpl.
+    ring.
+    case (Hp1 e2); case (Hp2 (right (split p1 e2))).
+    intros _ tmp1 _ tmp2; rewrite tmp2;
+    repeat rewrite NPEmul_correct; simpl.
+    rewrite tmp1.
+    repeat rewrite NPEmul_correct; simpl.
+    ring.
+  intros p _ e2; generalize (isIn_correct l (PEopp p) e2);
+    case (isIn (PEopp p) e2); auto; intros p1;
+    [intros Hp1; rewrite Hp1 | idtac];
+    simpl left; simpl common;  simpl right; auto;
+    repeat rewrite NPEmul_correct; simpl; split; 
+    try rewrite  (morph1 CRmorph); ring.
+Qed.
+
+
+Theorem split_correct_l: forall l e1 e2,
+  NPEeval l e1 == NPEeval l (NPEmul (left (split e1 e2))
+                                   (common (split e1 e2))).
+Proof.
+intros l e1 e2; case (split_correct l e1 e2); auto.
+Qed.
+
+Theorem split_correct_r: forall l e1 e2,
+  NPEeval l e2 == NPEeval l (NPEmul (right (split e1 e2))
+                                   (common (split e1 e2))).
+Proof.
+intros l e1 e2; case (split_correct l e1 e2); auto.
+Qed.
+
+Fixpoint Fnorm (e : FExpr) : linear := 
   match e with
   | FEc c => mk_linear (PEc c) (PEc cI) nil
   | FEX x => mk_linear (PEX C x) (PEc cI) nil
   | FEadd e1 e2 =>
       let x := Fnorm e1 in
       let y := Fnorm e2 in
+      let s := split (denum x) (denum y) in
       mk_linear
-        (NPEadd (NPEmul (num x) (denum y)) (NPEmul (num y) (denum x)))
-        (NPEmul (denum x) (denum y))
+        (NPEadd (NPEmul (num x) (right s)) (NPEmul (num y) (left s)))
+        (NPEmul (left s) (NPEmul (right s) (common s)))
         (condition x ++ condition y)
+ 
   | FEsub e1 e2 =>
       let x := Fnorm e1 in
       let y := Fnorm e2 in
+      let s := split (denum x) (denum y) in
       mk_linear
-        (NPEsub (NPEmul (num x) (denum y))
-                (NPEmul (num y) (denum x)))
-        (NPEmul (denum x) (denum y))
+        (NPEsub (NPEmul (num x) (right s)) (NPEmul (num y) (left s)))
+        (NPEmul (left s) (NPEmul (right s) (common s)))
         (condition x ++ condition y)
   | FEmul e1 e2 =>
       let x := Fnorm e1 in
@@ -608,20 +797,26 @@ intros l e; elim e.
    rewrite NPEmul_correct in |- *.
    simpl in |- *.
    apply field_is_integral_domain.
-  apply Hrec1.
-    apply PCond_app_inv_l with (1 := Hcond).
-  apply Hrec2.
-    apply PCond_app_inv_r with (1 := Hcond).
+   intros HH; case Hrec1; auto.
+     apply PCond_app_inv_l with (1 := Hcond).
+   rewrite (split_correct_l l (denum (Fnorm e1)) (denum (Fnorm e2))).
+   rewrite NPEmul_correct; simpl; rewrite HH; ring.
+   intros HH; case Hrec2; auto.
+     apply PCond_app_inv_r with (1 := Hcond).
+   rewrite (split_correct_r l (denum (Fnorm e1)) (denum (Fnorm e2))); auto.
  intros e1 Hrec1 e2 Hrec2 Hcond.
    simpl condition in Hcond.
    simpl denum in |- *.
    rewrite NPEmul_correct in |- *.
    simpl in |- *.
    apply field_is_integral_domain.
-  apply Hrec1.
-    apply PCond_app_inv_l with (1 := Hcond).
-  apply Hrec2.
-    apply PCond_app_inv_r with (1 := Hcond).
+   intros HH; case Hrec1; auto.
+     apply PCond_app_inv_l with (1 := Hcond).
+   rewrite (split_correct_l l (denum (Fnorm e1)) (denum (Fnorm e2))).
+   rewrite NPEmul_correct; simpl; rewrite HH; ring.
+   intros HH; case Hrec2; auto.
+     apply PCond_app_inv_r with (1 := Hcond).
+   rewrite (split_correct_r l (denum (Fnorm e1)) (denum (Fnorm e2))); auto.
  intros e1 Hrec1 e2 Hrec2 Hcond.
    simpl condition in Hcond.
    simpl denum in |- *.
@@ -676,7 +871,13 @@ apply PCond_app_inv_r with ( 1 := HH ).
 rewrite (He1 HH1); rewrite (He2 HH2).
 rewrite NPEadd_correct; simpl.
 repeat rewrite NPEmul_correct; simpl.
-apply rdiv2; auto.
+generalize (split_correct_l l (denum (Fnorm e1)) (denum (Fnorm e2)))
+   (split_correct_r l (denum (Fnorm e1)) (denum (Fnorm e2))).
+repeat rewrite NPEmul_correct; simpl.
+intros U1 U2; rewrite U1; rewrite U2.
+apply rdiv2b; auto.
+  rewrite <- U1; auto.
+  rewrite <- U2; auto.
 
 intros e1 He1 e2 He2 HH.
 assert (HH1: PCond l (condition (Fnorm e1))).
@@ -686,7 +887,13 @@ apply PCond_app_inv_r with ( 1 := HH ).
 rewrite (He1 HH1); rewrite (He2 HH2).
 rewrite NPEsub_correct; simpl.
 repeat rewrite NPEmul_correct; simpl.
-apply rdiv3; auto.
+generalize (split_correct_l l (denum (Fnorm e1)) (denum (Fnorm e2)))
+   (split_correct_r l (denum (Fnorm e1)) (denum (Fnorm e2))).
+repeat rewrite NPEmul_correct; simpl.
+intros U1 U2; rewrite U1; rewrite U2.
+apply rdiv3b; auto.
+  rewrite <- U1; auto.
+  rewrite <- U2; auto.
 
 intros e1 He1 e2 He2 HH.
 assert (HH1: PCond l (condition (Fnorm e1))).
@@ -974,6 +1181,30 @@ Definition Pcond_simpl_complete :=
 
 End Fcons_simpl.
 
+Let Mpc := MPcond_map cO cI cadd cmul csub copp ceqb.
+Let Mp := MPcond_dev rO rI radd rmul req cO cI ceqb phi.
+Let Subst := PNSubstL cO cI cadd cmul ceqb.
+
+(* simplification + rewriting *)
+Theorem Field_subst_correct :
+forall l ul fe m n,
+ PCond l (Fapp Fcons00 (condition (Fnorm fe)) BinList.nil) ->
+ Mp (Mpc ul) l ->
+ Peq ceqb (Subst (Nnorm (num (Fnorm fe))) (Mpc ul) m n) (Pc cO) = true ->
+ FEeval l fe == 0.
+intros l ul fe m n H H1 H2.
+assert (H3 := (Pcond_simpl_gen _ _ H)).
+apply eq_trans with (1 := Fnorm_FEeval_PEeval l fe 
+                           (Pcond_simpl_gen _ _ H)).
+apply rdiv8; auto.
+rewrite (PNSubstL_dev_ok Rsth Reqe ARth CRmorph m n
+              _ (num (Fnorm fe)) l H1).
+rewrite <-(Ring_polynom.Pphi_Pphi_dev Rsth Reqe ARth CRmorph).
+rewrite (fun x => Peq_ok Rsth Reqe CRmorph x (Pc cO)); auto.
+simpl; apply (morph0 CRmorph); auto.
+Qed.
+
+
 End AlmostField.
 
 Section FieldAndSemiField.
diff --git a/contrib/setoid_ring/Ring_polynom.v b/contrib/setoid_ring/Ring_polynom.v
index e26bcd567..2be6f5fc7 100644
--- a/contrib/setoid_ring/Ring_polynom.v
+++ b/contrib/setoid_ring/Ring_polynom.v
@@ -323,7 +323,13 @@ Section MakeRingPol.
   end.
  Notation "P ** P'" := (Pmul P P').
  
- (** Evaluation of a polynomial towards R *)
+
+ (** Monomial **)
+     
+  Inductive Mon: Set :=
+    mon0: Mon 
+  | zmon: positive -> Mon -> Mon 
+  | vmon: positive -> Mon -> Mon.
 
  Fixpoint pow (x:R) (i:positive) {struct i}: R :=
   match i with
@@ -332,6 +338,96 @@ Section MakeRingPol.
   | xI i => let p := pow x i in x * p * p
   end.
 
+ Fixpoint Mphi(l:list R) (M: Mon) {struct M} : R :=
+  match M with
+     mon0 => rI
+  | zmon j M1  => Mphi (jump j l) M1
+  | vmon i M1 =>
+     let x := hd 0 l in
+     let xi := pow x i in
+    (Mphi (tail l) M1) * xi 
+  end.
+
+ Definition zmon_pred j M :=
+   match j with xH => M | _ => zmon (Ppred j) M end.
+
+ Definition mkZmon j M :=
+   match M with mon0 => mon0 | _ => zmon j M end.
+
+ Fixpoint MFactor (P: Pol) (M: Mon) {struct P}: Pol * Pol :=
+   match P, M with
+        _, mon0 => (Pc cO, P)
+   | Pc _, _    => (P, Pc cO)
+   | Pinj j1 P1, zmon j2 M1 =>
+      match (j1 ?= j2) Eq with
+        Eq => let (R,S) := MFactor P1 M1 in
+                 (mkPinj j1 R, mkPinj j1 S)
+      | Lt => let (R,S) := MFactor P1 (zmon (j2 - j1) M1) in
+                 (mkPinj j1 R, mkPinj j1 S)
+      | Gt => (P, Pc cO)
+      end
+  | Pinj _ _, vmon _ _ => (P, Pc cO)
+  | PX P1 i Q1, zmon j M1 =>
+             let M2 := zmon_pred j M1 in
+             let (R1, S1) := MFactor P1 M in
+             let (R2, S2) := MFactor Q1 M2 in
+               (mkPX R1 i R2, mkPX S1 i S2)
+  | PX P1 i Q1, vmon j M1 =>
+      match (i ?= j) Eq with
+        Eq => let (R1,S1) := MFactor P1 (mkZmon xH M1) in
+                 (mkPX R1 i Q1, S1)
+      | Lt => let (R1,S1) := MFactor P1 (vmon (j - i) M1) in
+                 (mkPX R1 i Q1, S1)
+      | Gt => let (R1,S1) := MFactor P1 (mkZmon xH M1) in
+                 (mkPX R1 i Q1, mkPX S1 (i-j) (Pc cO))
+      end
+   end.
+
+  Definition POneSubst (P1: Pol) (M1: Mon) (P2: Pol): option Pol :=
+    let (Q1,R1) := MFactor P1 M1 in
+    match R1 with 
+     (Pc c) => if c ?=! cO then None 
+               else Some (Padd Q1 (Pmul P2 R1))
+    | _ => Some (Padd Q1 (Pmul P2 R1))
+    end.
+
+  Fixpoint PNSubst1 (P1: Pol) (M1: Mon) (P2: Pol) (n: nat) {struct n}: Pol :=
+    match POneSubst P1 M1 P2 with 
+     Some P3 => match n with S n1 => PNSubst1 P3 M1 P2 n1 | _ => P3 end
+    | _ => P1
+    end.
+
+  Definition PNSubst (P1: Pol) (M1: Mon) (P2: Pol) (n: nat): option Pol :=
+    match POneSubst P1 M1 P2 with 
+     Some P3 => match n with S n1 => Some (PNSubst1 P3 M1 P2 n1) | _ => None end
+    | _ => None
+    end.
+            
+  Fixpoint PSubstL1 (P1: Pol) (LM1: list (Mon * Pol)) (n: nat) {struct LM1}: 
+     Pol :=
+    match LM1 with 
+     cons (M1,P2) LM2 => PSubstL1 (PNSubst1 P1 M1 P2 n) LM2 n
+    | _ => P1
+    end.
+
+  Fixpoint PSubstL (P1: Pol) (LM1: list (Mon * Pol)) (n: nat) {struct LM1}: option Pol :=
+    match LM1 with 
+     cons (M1,P2) LM2 =>
+      match PNSubst P1 M1 P2 n with 
+        Some P3 => Some (PSubstL1 P3 LM2 n)
+     |  None => PSubstL P1 LM2 n
+     end
+    | _ => None
+    end.
+
+  Fixpoint PNSubstL (P1: Pol) (LM1: list (Mon * Pol)) (m n: nat) {struct m}: Pol :=
+    match PSubstL P1 LM1 n with 
+     Some P3 => match m with S m1 => PNSubstL P3 LM1 m1 n | _ => P3 end
+    | _ => P1
+    end.
+
+ (** Evaluation of a polynomial towards R *)
+
  Fixpoint Pphi(l:list R) (P:Pol) {struct P} : R :=
   match P with
   | Pc c => [c]
@@ -658,6 +754,191 @@ Section MakeRingPol.
   rewrite (ARmul_sym ARth (P' @ l));rrefl.
  Qed.
 
+
+ Lemma mkZmon_ok: forall M j l,
+   Mphi l (mkZmon j M) == Mphi l (zmon j M).
+ intros M j l; case M; simpl; intros; rsimpl.
+ Qed.
+
+ Lemma Mphi_ok: forall P M l, 
+    let (Q,R) := MFactor P M in
+      P@l == Q@l + (Mphi l M) * (R@l).
+ Proof.
+ intros P; elim P; simpl; auto; clear P.
+   intros c M l; case M; simpl; auto; try intro p; try intro m;
+   try rewrite (morph0 CRmorph); rsimpl.
+
+   intros i P Hrec M l; case M; simpl; clear M.
+     rewrite (morph0 CRmorph); rsimpl.
+     intros j M.
+     case_eq ((i ?= j) Eq); intros He; simpl.
+       rewrite (Pcompare_Eq_eq _ _ He).
+       generalize (Hrec M (jump j l)); case (MFactor P M);
+        simpl; intros P2 Q2 H; repeat rewrite mkPinj_ok; auto.
+       generalize (Hrec (zmon (j -i) M) (jump i l)); 
+       case (MFactor P (zmon (j -i) M)); simpl.
+       intros P2 Q2 H; repeat rewrite mkPinj_ok; auto.
+       rewrite  <- (Pplus_minus _ _ (ZC2 _ _ He)).
+       rewrite Pplus_comm; rewrite jump_Pplus; auto.
+       rewrite (morph0 CRmorph); rsimpl.
+       intros P2 m; rewrite (morph0 CRmorph); rsimpl.
+
+   intros P2 Hrec1 i Q2 Hrec2 M l; case M; simpl; auto.
+   rewrite (morph0 CRmorph); rsimpl.
+   intros j M1.
+     generalize (Hrec1 (zmon j M1) l); 
+     case (MFactor P2 (zmon j M1)).
+     intros R1 S1 H1.
+     generalize (Hrec2 (zmon_pred j M1) (List.tail l)); 
+     case (MFactor Q2 (zmon_pred j M1)); simpl.
+     intros R2 S2 H2; rewrite H1; rewrite H2.
+     repeat rewrite mkPX_ok; simpl.
+     rsimpl.  
+     apply radd_ext; rsimpl.
+     rewrite (ARadd_sym ARth); rsimpl.
+     apply radd_ext; rsimpl.
+     rewrite (ARadd_sym ARth); rsimpl.
+     case j; simpl; auto; try intros j1; rsimpl.
+     rewrite jump_Pdouble_minus_one; rsimpl.
+   intros j M1.
+     case_eq ((i ?= j) Eq); intros He; simpl.
+       rewrite (Pcompare_Eq_eq _ _ He).
+       generalize (Hrec1 (mkZmon xH M1) l); case (MFactor P2 (mkZmon xH M1));
+        simpl; intros P3 Q3 H; repeat rewrite mkPinj_ok; auto.
+       rewrite H; rewrite mkPX_ok; rsimpl.
+       repeat (rewrite <-(ARadd_assoc ARth)).
+       apply radd_ext; rsimpl.
+       rewrite (ARadd_sym ARth); rsimpl.
+       apply radd_ext; rsimpl.
+       repeat (rewrite <-(ARmul_assoc ARth)).
+       rewrite mkZmon_ok.
+       apply rmul_ext; rsimpl.
+       rewrite (ARmul_sym ARth); rsimpl.
+       generalize (Hrec1 (vmon (j - i) M1) l); 
+             case (MFactor P2 (vmon (j - i) M1));
+        simpl; intros P3 Q3 H; repeat rewrite mkPinj_ok; auto.
+       rewrite H; rsimpl; repeat rewrite mkPinj_ok; auto.
+       rewrite mkPX_ok; rsimpl.
+       repeat (rewrite <-(ARadd_assoc ARth)).
+       apply radd_ext; rsimpl.
+       rewrite (ARadd_sym ARth); rsimpl.
+       apply radd_ext; rsimpl.
+       repeat (rewrite <-(ARmul_assoc ARth)).
+       apply rmul_ext; rsimpl.
+       rewrite (ARmul_sym ARth); rsimpl.
+       apply rmul_ext; rsimpl.
+       rewrite <- pow_Pplus.
+       rewrite (Pplus_minus _ _ (ZC2 _ _ He)); rsimpl.
+       generalize (Hrec1 (mkZmon 1 M1) l); 
+             case (MFactor P2 (mkZmon 1 M1));
+        simpl; intros P3 Q3 H; repeat rewrite mkPinj_ok; auto.
+       rewrite H; rsimpl.
+       rewrite mkPX_ok; rsimpl.
+       repeat (rewrite <-(ARadd_assoc ARth)).
+       apply radd_ext; rsimpl.
+       rewrite (ARadd_sym ARth); rsimpl.
+       apply radd_ext; rsimpl.
+       rewrite mkZmon_ok.
+       repeat (rewrite <-(ARmul_assoc ARth)).
+       apply rmul_ext; rsimpl.
+       rewrite (ARmul_sym ARth); rsimpl.
+       rewrite mkPX_ok; simpl; rsimpl.
+       rewrite (morph0 CRmorph); rsimpl.
+       repeat (rewrite <-(ARmul_assoc ARth)).
+       rewrite (ARmul_sym ARth (Q3@l)); rsimpl.
+       apply rmul_ext; rsimpl.
+       rewrite <- pow_Pplus.
+       rewrite (Pplus_minus _ _ He); rsimpl.
+ Qed.
+
+
+ Lemma POneSubst_ok: forall P1 M1 P2 P3 l,
+    POneSubst P1 M1 P2 = Some P3 -> Mphi l M1 == P2@l -> P1@l == P3@l.
+ intros P2 M1 P3 P4 l; unfold POneSubst.
+ generalize (Mphi_ok P2 M1 l); case (MFactor P2 M1); simpl; auto.
+ intros Q1 R1; case R1.
+   intros c H; rewrite H.
+   generalize (morph_eq CRmorph c cO);
+        case (c ?=! cO); simpl; auto.
+   intros H1 H2; rewrite H1; auto; rsimpl.
+   discriminate.
+   intros _ H1 H2; injection H1; intros; subst.
+   rewrite H2; rsimpl.
+   rewrite Padd_ok; rewrite Pmul_ok; rsimpl.
+ intros i P5 H; rewrite H.
+   intros HH H1; injection HH; intros; subst; rsimpl.
+   rewrite Padd_ok; rewrite Pmul_ok; rewrite H1; rsimpl.
+ intros i P5 P6 H1 H2 H3; rewrite H1; rewrite H3.
+   injection H2; intros; subst; rsimpl.
+   rewrite Padd_ok; rewrite Pmul_ok; rsimpl.
+ Qed.
+
+
+ Lemma PNSubst1_ok: forall n P1 M1 P2 l,
+    Mphi l M1 == P2@l -> P1@l == (PNSubst1 P1 M1 P2 n)@l.
+ Proof.
+ intros n; elim n; simpl; auto.
+   intros P2 M1 P3 l H.
+   generalize (fun P4 => @POneSubst_ok P2 M1 P3 P4 l); 
+   case (POneSubst P2 M1 P3); [idtac | intros; rsimpl].
+   intros P4 Hrec; rewrite (Hrec P4); auto; rsimpl.
+ intros n1 Hrec P2 M1 P3 l H.
+   generalize (fun P4 => @POneSubst_ok P2 M1 P3 P4 l); 
+   case (POneSubst P2 M1 P3); [idtac | intros; rsimpl].
+   intros P4 Hrec1; rewrite (Hrec1 P4); auto; rsimpl.
+ Qed.
+
+ Lemma PNSubst_ok: forall n P1 M1 P2 l P3,
+    PNSubst P1 M1 P2 n = Some P3 -> Mphi l M1 == P2@l -> P1@l == P3@l.
+ Proof.
+ intros n P2 M1 P3 l P4; unfold PNSubst.
+ generalize (fun P4 => @POneSubst_ok P2 M1 P3 P4 l); 
+ case (POneSubst P2 M1 P3); [idtac | intros; discriminate].
+ intros P5 H1; case n; try (intros; discriminate). 
+ intros n1 H2; injection H2; intros; subst.
+ rewrite <- PNSubst1_ok; auto.
+ Qed.
+
+ Fixpoint MPcond (LM1: list (Mon * Pol)) (l: list R) {struct LM1} : Prop :=            
+    match LM1 with 
+     cons (M1,P2) LM2 =>  (Mphi l M1 == P2@l) /\ (MPcond LM2 l)
+    | _ => True
+    end.
+
+ Lemma PSubstL1_ok: forall n LM1 P1 l,
+    MPcond LM1 l ->  P1@l == (PSubstL1 P1 LM1 n)@l.
+ Proof.
+ intros n LM1; elim LM1; simpl; auto.
+   intros; rsimpl.
+ intros (M2,P2) LM2 Hrec P3 l [H H1].
+ rewrite <- Hrec; auto.
+ apply PNSubst1_ok; auto.
+ Qed.
+
+ Lemma PSubstL_ok: forall n LM1 P1 P2 l,
+   PSubstL P1 LM1 n = Some P2 -> MPcond LM1 l ->  P1@l == P2@l.
+ Proof.
+ intros n LM1; elim LM1; simpl; auto.
+   intros; discriminate.
+ intros (M2,P2) LM2 Hrec P3 P4 l.
+ generalize (PNSubst_ok n P3 M2 P2); case (PNSubst P3 M2 P2 n).
+   intros P5 H0 H1 [H2 H3]; injection H1; intros; subst.
+   rewrite <- PSubstL1_ok; auto.
+ intros l1 H [H1 H2]; auto.
+ Qed.
+
+ Lemma PNSubstL_ok: forall m n LM1 P1 l,
+    MPcond LM1 l ->  P1@l == (PNSubstL P1 LM1 m n)@l.
+ Proof.
+ intros m; elim m; simpl; auto.
+   intros n LM1 P2 l H; generalize (fun P3 => @PSubstL_ok n LM1 P2 P3 l);
+     case (PSubstL P2 LM1 n); intros; rsimpl; auto.
+ intros m1 Hrec n LM1 P2 l H.
+ generalize (fun P3 => @PSubstL_ok n LM1 P2 P3 l);
+     case (PSubstL P2 LM1 n); intros; rsimpl; auto.
+ rewrite <- Hrec; auto.
+ Qed.
+
  (** Definition of polynomial expressions *)
 
  Inductive PExpr : Type :=
@@ -919,4 +1200,33 @@ Section MakeRingPol.
   intros l pe npe npe_eq; subst npe; apply Pphi_dev_gen_ok.
  Qed. 
 
+ Fixpoint MPcond_dev (LM1: list (Mon * Pol)) (l: list R) {struct LM1} : Prop :=            
+    match LM1 with 
+     cons (M1,P2) LM2 =>  (Mphi l M1 == Pphi_dev l P2) /\ (MPcond_dev LM2 l)
+    | _ => True
+    end.
+
+ Fixpoint MPcond_map (LM1: list (Mon * PExpr)): list (Mon * Pol) :=            
+    match LM1 with 
+     cons (M1,P2) LM2 =>  cons (M1, norm P2) (MPcond_map LM2)
+    | _ => nil
+    end.
+
+ Lemma MP_cond_dev_imp_MP_cond: forall LM1 l,
+     MPcond_dev LM1 l -> MPcond LM1 l.
+ Proof.
+ intros LM1; elim LM1; simpl; auto.
+ intros (M2,P2) LM2 Hrec l [H1 H2]; split; auto.
+ rewrite H1; rewrite Pphi_Pphi_dev; rsimpl. 
+ Qed.
+
+ Lemma PNSubstL_dev_ok: forall m n lm pe l,
+    let LM :=  MPcond_map lm in
+    MPcond_dev LM l -> PEeval l pe == Pphi_dev l (PNSubstL (norm pe) LM m n).
+ intros m n lm p3 l LM H.
+ rewrite <- Pphi_Pphi_dev; rewrite <- PNSubstL_ok; auto.
+   apply MP_cond_dev_imp_MP_cond; auto.
+ rewrite Pphi_Pphi_dev; apply Pphi_dev_ok; auto.
+ Qed.
+
 End MakeRingPol.