changement de la fonction norm_subst

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

2 files changed, 55 insertions, 7 deletions

diff --git a/contrib/setoid_ring/Field_theory.v b/contrib/setoid_ring/Field_theory.v
index 0c7f235120..ea8421cf16 100644
--- a/contrib/setoid_ring/Field_theory.v
+++ b/contrib/setoid_ring/Field_theory.v
@@ -458,11 +458,12 @@ Qed.
 Definition NPEpow x n :=
   match n with
   | N0 => PEc cI
-  | Npos p => 
+  | Npos p =>
+    if positive_eq p xH then x else
     match x with 
     | PEc c => 
       if ceqb c cI then PEc cI else if ceqb c cO then PEc cO else PEc (pow_pos cmul c p)  
-    | _ => PEpow x n
+    | _ => PEpow x n         
     end
   end.
 
@@ -471,7 +472,10 @@ Theorem NPEpow_correct : forall l e n,
 Proof.
  destruct n;simpl.
  rewrite pow_th.(rpow_pow_N);simpl;auto.
- destruct e;simpl;auto.
+ generalize (positive_eq_correct p xH).
+ destruct (positive_eq p 1);intros.
+ rewrite H;rewrite  pow_th.(rpow_pow_N). trivial.
+ clear H;destruct e;simpl;auto.
  repeat apply ceqb_rect;simpl;intros;rewrite pow_th.(rpow_pow_N);simpl.
  symmetry;induction p;simpl;trivial; ring [IHp H CRmorph.(morph1)].
  symmetry; induction p;simpl;trivial;ring [IHp CRmorph.(morph0)].
@@ -1194,8 +1198,10 @@ intros n l lpe fe Hlpe H H1;
  apply eq_trans with (1 := Fnorm_FEeval_PEeval l fe H1).
 apply rdiv8; auto.
 transitivity (NPEeval l (PEc cO)); auto.
-apply (ring_correct Rsth Reqe ARth CRmorph) with n lpe;trivial.
-simpl; apply (morph0 CRmorph); auto.
+rewrite (norm_subst_ok Rsth Reqe ARth CRmorph pow_th n l lpe);auto.
+change (NPEeval l (PEc cO)) with (Pphi 0 radd rmul phi l (Pc cO)).
+apply (Peq_ok Rsth Reqe CRmorph);auto.
+simpl. apply (morph0 CRmorph); auto.
 Qed.
 
 (* simplify a field expression into a fraction *)
diff --git a/contrib/setoid_ring/Ring_polynom.v b/contrib/setoid_ring/Ring_polynom.v
index 8567037d91..b79f2fe200 100644
--- a/contrib/setoid_ring/Ring_polynom.v
+++ b/contrib/setoid_ring/Ring_polynom.v
@@ -1191,8 +1191,25 @@ Section POWER.
   Variable lmp:list (Mon*Pol).
   Let subst_l P := PNSubstL P lmp n n.
   Let Pmul_subst P1 P2 := subst_l (Pmul P1 P2).
-  Let Ppow_subst := Ppow_N subst_l. 
-  
+  Let Ppow_subst := Ppow_N subst_l.
+
+  Fixpoint norm_aux (pe:PExpr) : Pol :=
+   match pe with
+   | PEc c => Pc c
+   | PEX j => mk_X j  
+   | PEadd (PEopp pe1) pe2 => Psub (norm_aux pe2) (norm_aux pe1)
+   | PEadd pe1 (PEopp pe2) => 
+     Psub (norm_aux pe1) (norm_aux pe2)
+   | PEadd pe1 pe2 => Padd (norm_aux  pe1) (norm_aux pe2)
+   | PEsub pe1 pe2 => Psub (norm_aux pe1) (norm_aux pe2)
+   | PEmul pe1 pe2 => Pmul (norm_aux pe1) (norm_aux pe2) 
+   | PEopp pe1 => Popp (norm_aux pe1)
+   | PEpow pe1 n => Ppow_N (fun p => p) (norm_aux pe1) n
+   end.
+
+  Definition norm_subst pe := subst_l (norm_aux pe).
+
+ (* 
   Fixpoint norm_subst (pe:PExpr) : Pol :=
    match pe with
    | PEc c => Pc c
@@ -1227,7 +1244,32 @@ Section POWER.
    induction p;simpl;try rewrite IHp;try rewrite IHpe;repeat rewrite Pms_ok; 
       repeat rewrite Pmul_ok;rrefl.
   Qed.
+*)
+ Lemma norm_aux_spec : 
+     forall l pe, MPcond lmp l ->
+       PEeval l pe == (norm_aux pe)@l. 
+  Proof.
+   intros.
+   induction pe;simpl;Esimpl3.
+   apply mkX_ok.
+   rewrite IHpe1;rewrite IHpe2;destruct pe1;destruct pe2;Esimpl3. 
+   rewrite IHpe1;rewrite IHpe2;rrefl.
+   rewrite IHpe1;rewrite IHpe2. rewrite Pmul_ok. rrefl.
+   rewrite IHpe;rrefl.
+   rewrite Ppow_N_ok. intros;rrefl.
+   rewrite pow_th.(rpow_pow_N). destruct n0;Esimpl3.
+   induction p;simpl;try rewrite IHp;try rewrite IHpe;repeat rewrite Pms_ok; 
+      repeat rewrite Pmul_ok;rrefl.
+  Qed.
 
+ Lemma norm_subst_spec : 
+     forall l pe, MPcond lmp l ->
+       PEeval l pe == (norm_subst pe)@l.
+ Proof.
+  intros;unfold norm_subst.
+  unfold subst_l;rewrite <- PNSubstL_ok;trivial. apply norm_aux_spec. trivial.
+ Qed. 
+ 
  End NORM_SUBST_REC.
   
  Fixpoint interp_PElist (l:list R) (lpe:list (PExpr*PExpr)) {struct lpe} : Prop :=