bug dans field_simplify

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

4 files changed, 60 insertions, 38 deletions

diff --git a/contrib/setoid_ring/Field_tac.v b/contrib/setoid_ring/Field_tac.v
index eafcb41a7..660a39b50 100644
--- a/contrib/setoid_ring/Field_tac.v
+++ b/contrib/setoid_ring/Field_tac.v
@@ -70,24 +70,25 @@ Ltac fold_field_cond req rO :=
   end.
 
 Ltac simpl_PCond req rO :=
-  protect_fv "field";
+  protect_fv "field_cond";
   try (exact I);
   fold_field_cond req rO.
 
 (* Rewriting (field_simplify) *)
-Ltac Field_rewrite_list lemma Cond_lemma req Cst_tac :=
+Ltac Make_field_simplify_tac lemma Cond_lemma req Cst_tac :=
   let Make_tac :=
     match type of lemma with
     | forall l fe nfe,
       _ = nfe -> 
       PCond _ _ _ _ _ _ _ _ _ ->
-      req (@FEeval ?R ?rO ?radd ?rmul ?rsub ?ropp ?rdiv ?rinv ?C ?phi l fe) _ =>
+      req (FEeval ?rO ?radd ?rmul ?rsub ?ropp ?rdiv ?rinv (C:=?C) ?phi l fe)
+        _ =>
         let mkFV := FFV Cst_tac radd rmul rsub ropp rdiv rinv in
         let mkFE := mkFieldexpr C Cst_tac radd rmul rsub ropp rdiv rinv in
-        let simpl_field H := (*protect_fv "field" in H*)
-unfold Pphi_dev in H;simpl in H in 
-        (fun f => f mkFV mkFE simpl_field lemma req;
-                  try (apply Cond_lemma; simpl_PCond req rO))
+        let simpl_field H := protect_fv "field" in H in
+(*unfold Pphi_dev in H;simpl in H in *)
+        (fun f rl => (f mkFV mkFE simpl_field lemma req rl;
+                      try (apply Cond_lemma; simpl_PCond req rO)))
     | _ => fail 1 "field anomaly: bad correctness lemma (rewr)"
     end in
   Make_tac ReflexiveRewriteTactic.
diff --git a/contrib/setoid_ring/Field_theory.v b/contrib/setoid_ring/Field_theory.v
index b71eb0596..fd054f5d2 100644
--- a/contrib/setoid_ring/Field_theory.v
+++ b/contrib/setoid_ring/Field_theory.v
@@ -754,16 +754,19 @@ simpl; apply (morph0 CRmorph); auto.
 Qed.
 
 (* simplify a field expression into a fraction *)
+(* TODO: simplify when den is constant... *)
+Definition display_linear l num den :=
+  NPphi_dev l num / NPphi_dev l den.
+
 Theorem Pphi_dev_div_ok:
  forall l fe nfe,
  Fnorm fe = nfe ->
  PCond l (condition nfe) ->
- FEeval l fe ==
- NPphi_dev l (Nnorm (num nfe)) / NPphi_dev l (Nnorm (denum nfe)).
+ FEeval l fe == display_linear l (Nnorm (num nfe)) (Nnorm (denum nfe)).
 Proof.
   intros l fe nfe eq_nfe H; subst nfe.
   apply eq_trans with (1 := Fnorm_FEeval_PEeval _ _ H).
-  apply SRdiv_ext;
+  unfold display_linear; apply SRdiv_ext;
   apply (Pphi_dev_ok Rsth Reqe ARth CRmorph); reflexivity.
 Qed.
 
diff --git a/contrib/setoid_ring/Ring_tac.v b/contrib/setoid_ring/Ring_tac.v
index bfb83fbe0..a6460ed5c 100644
--- a/contrib/setoid_ring/Ring_tac.v
+++ b/contrib/setoid_ring/Ring_tac.v
@@ -22,20 +22,29 @@ Ltac OnEquation req :=
   | _ => fail 1 "Goal is not an equation (of expected equality)"
   end.
 
+
+Ltac OnMainSubgoal H ty :=
+  match ty with
+  | _ -> ?ty' =>
+     let subtac := OnMainSubgoal H ty' in
+     (fun tac => (lapply H; [clear H; intro H; subtac tac | idtac]))
+  | _ => (fun tac => tac)
+  end.
+
 Ltac ApplyLemmaAndSimpl tac lemma pe:=
   let npe := fresh "ast_nf" in
   let H := fresh "eq_nf" in
   let Heq := fresh "thm" in
   let npe_spec :=
     match type of (lemma pe) with
-      forall (npe:_), ?npe_spec = npe -> _ => npe_spec
+      forall npe, ?npe_spec = npe -> _ => npe_spec
     | _ => fail 1 "ApplyLemmaAndSimpl: cannot find norm expression"
     end in
   (compute_assertion H npe npe_spec;
    (assert (Heq:=lemma _ _ H) || fail "anomaly: failed to apply lemma");
    clear H;
-   tac Heq;
-   rewrite Heq; clear Heq npe).
+   OnMainSubgoal Heq ltac:(type of Heq)
+     ltac:(tac Heq; rewrite Heq; clear Heq npe)).
 
 (* General scheme of reflexive tactics using of correctness lemma
    that involves normalisation of one expression *)
diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4
index 7c41ed63e..40fa3a904 100644
--- a/contrib/setoid_ring/newring.ml4
+++ b/contrib/setoid_ring/newring.ml4
@@ -39,29 +39,30 @@ open Entries
 (****************************************************************************)
 (* controlled reduction *)
 
-let mark_arg i c = mkEvar(i,[|c|]);;
+let mark_arg i c = mkEvar(i,[|c|])
 let unmark_arg f c =
   match destEvar c with
     | (i,[|c|]) -> f i c
-    | _ -> assert false;;
+    | _ -> assert false
 
-type protect_flag = Eval|Prot|Rec ;;
+type protect_flag = Eval|Prot|Rec
 
-let tag_arg tag_rec map i c =
+let tag_arg tag_rec map subs i c =
   match map i with
-      Eval -> inject c
+      Eval -> mk_clos subs c
     | Prot -> mk_atom c
-    | Rec -> if i = -1 then inject c else tag_rec c
+    | Rec -> if i = -1 then mk_clos subs c else tag_rec c
 
-let rec mk_clos_but f_map t =
+let rec mk_clos_but f_map subs t =
   match f_map t with
-    | Some map -> tag_arg (mk_clos_but f_map) map (-1) t
+    | Some map -> tag_arg (mk_clos_but f_map subs) map subs (-1) t
     | None ->
         (match kind_of_term t with
-            App(f,args) -> mk_clos_app_but f_map f args 0
+            App(f,args) -> mk_clos_app_but f_map subs f args 0
+          | Prod _ -> mk_clos_deep (mk_clos_but f_map) subs t
           | _ -> mk_atom t)
 
-and mk_clos_app_but f_map f args n =
+and mk_clos_app_but f_map subs f args n =
   if n >= Array.length args then mk_atom(mkApp(f, args))
   else
     let fargs, args' = array_chop n args in
@@ -69,11 +70,11 @@ and mk_clos_app_but f_map f args n =
     match f_map f' with
         Some map ->
           mk_clos_deep
-            (fun _ -> unmark_arg (tag_arg (mk_clos_but f_map) map))
-            (Esubst.ESID 0)
+            (fun s' -> unmark_arg (tag_arg (mk_clos_but f_map s') map s'))
+            subs
             (mkApp (mark_arg (-1) f', Array.mapi mark_arg args'))
-      | None -> mk_clos_app_but f_map f args (n+1)
-;;
+      | None -> mk_clos_app_but f_map subs f args (n+1)
+
 
 let interp_map l c =
   try
@@ -97,7 +98,7 @@ let lookup_map map =
 
 let protect_red map env sigma c =
   kl (create_clos_infos betadeltaiota env)
-    (mk_clos_but (lookup_map map c) c);;
+    (mk_clos_but (lookup_map map c) (Esubst.ESID 0) c);;
 
 let protect_tac map =
   Tactics.reduct_option (protect_red map,DEFAULTcast) None ;;
@@ -227,12 +228,14 @@ let coq_nil = mk_cst list_dir "nil"
 
 let lapp f args = mkApp(Lazy.force f,args)
 
-let dest_rel t =
+let rec dest_rel t =
   match kind_of_term t with
       App(f,args) when Array.length args >= 2 ->
-        (mkApp(f,Array.sub args 0 (Array.length args - 2)),
-         args.(Array.length args - 2),
-         args.(Array.length args - 1))
+        let rel = mkApp(f,Array.sub args 0 (Array.length args - 2)) in
+        if closed0 rel then
+          (rel,args.(Array.length args - 2),args.(Array.length args - 1))
+        else error "ring: cannot find relation (not closed)"
+    | Prod(_,_,c) -> dest_rel c
     | _ -> error "ring: cannot find relation"
 
 (* Equality: do not evaluate but make recursive call on both sides *)
@@ -747,16 +750,22 @@ let _ = add_map "field"
   (map_with_eq
     [coq_cons,(function -1->Eval|2->Rec|_->Prot);
     coq_nil, (function -1->Eval|_ -> Prot);
-    (* Pphi_dev: evaluate polynomial and coef operations, protect
-       ring operations and make recursive call on the var map *)
-    pol_cst "Pphi_dev", (function -1|6|7|8|9|11->Eval|10->Rec|_->Prot);
+    (* display_linear: evaluate polynomials and coef operations, protect
+       field operations and make recursive call on the var map *)
+    fld_cst "display_linear",
+      (function -1|7|8|9|10|12|13->Eval|11->Rec|_->Prot);
     (* PEeval: evaluate morphism and polynomial, protect ring 
        operations and make recursive call on the var map *)
-    pol_cst "PEeval", (function -1|7|9->Eval|8->Rec|_->Prot);
-(*    fld_cst "FEeval", (function -1|9|11->Eval|10->Rec|_->Prot);*)
+    fld_cst "FEeval", (function -1|9|11->Eval|10->Rec|_->Prot)]);;
+
+
+let _ = add_map "field_cond"
+  (map_with_eq
+    [coq_cons,(function -1->Eval|2->Rec|_->Prot);
+     coq_nil, (function -1->Eval|_ -> Prot);
     (* PCond: evaluate morphism and denum list, protect ring
        operations and make recursive call on the var map *)
-    fld_cst "PCond", (function -1|8|10->Eval|9->Rec|_->Prot)]);;
+     fld_cst "PCond", (function -1|8|10->Eval|9->Rec|_->Prot)]);;
 
 
 let dest_field env sigma th_spec =