fixed ring/field warning about hyp cleaning up

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

2 files changed, 117 insertions, 90 deletions

diff --git a/contrib/setoid_ring/Field_tac.v b/contrib/setoid_ring/Field_tac.v
index a88fb1ac5a..b31ebda558 100644
--- a/contrib/setoid_ring/Field_tac.v
+++ b/contrib/setoid_ring/Field_tac.v
@@ -243,7 +243,6 @@ Ltac Field_norm_gen f n FLD lH rl :=
   let main_tac H := protect_fv "field" in H; f H in
   (* generate and use equations for each expression *)
   ReflexiveRewriteTactic mkFFV mkFE lemma_tac main_tac fv0 rl;
-  (* simplifying the denominator condition *)
   try simpl_PCond FLD.
 
 Ltac Field_simplify_gen f FLD lH rl := 
@@ -251,7 +250,8 @@ Ltac Field_simplify_gen f FLD lH rl :=
   Field_norm_gen f ring_subst_niter FLD lH rl; 
   get_FldPost FLD ().
 
-Ltac Field_simplify := Field_simplify_gen ltac:(fun H => rewrite H).
+Ltac Field_simplify :=
+  Field_simplify_gen ltac:(fun H => rewrite H).
 
 Tactic Notation (at level 0) "field_simplify" constr_list(rl) :=
   let G := Get_goal in
@@ -267,7 +267,7 @@ Tactic Notation "field_simplify" constr_list(rl) "in" hyp(H):=
   let t := type of H in   
   let g := fresh "goal" in
   set (g:= G);
-  generalize H;clear H;
+  revert H;
   field_lookup (PackField Field_simplify) [] rl t;
   intro H;
   unfold g;clear g.
@@ -278,7 +278,7 @@ Tactic Notation "field_simplify"
   let t := type of H in   
   let g := fresh "goal" in
   set (g:= G);
-  generalize H;clear H;
+  revert H;
   field_lookup (PackField Field_simplify) [lH] rl t;
   intro H;
   unfold g;clear g.
@@ -323,7 +323,8 @@ Ltac Field_Scheme Simpl_tac n lemma FLD lH :=
               apply ilemma 
                || fail "field anomaly: failed in applying lemma";
               [ Simpl_tac | simpl_PCond FLD]);
-    clear vlpe nlemma in
+    clear nlemma;
+    subst vlpe in
   OnEquation req Main_eq.
 
 (* solve completely a field equation, leaving non-zero conditions to be
@@ -413,6 +414,89 @@ Tactic Notation (at level 0)
   [ try exact I
   |clear H;intro H].
  
+(* More generic tactics to build variants of field *) 
+
+(* This tactic reifies c and pass to F:
+   - the FLD structure gathering all info in the field DB
+   - the atom list
+   - the expression (FExpr)
+ *)
+Ltac gen_with_field F c :=
+  let MetaExpr FLD _ rl :=
+    let R := get_FldCarrier FLD in
+    let mkFFV := get_FFV FLD in
+    let mkFE  := get_Meta FLD in
+    let csr :=
+      match rl with
+      | List.cons ?r _ => r
+      | _ => fail 1 "anomaly: ill-formed list"
+      end in
+    let fv := mkFFV csr (@List.nil R) in
+    let expr := mkFE csr fv in
+    F FLD fv expr in
+  field_lookup (PackField MetaExpr) [] (c=c).
+
+
+(* pushes the equation expr = ope(expr) in the goal, and
+   discharge it with field *)
+Ltac prove_field_eqn ope FLD fv expr :=
+  let res := ope expr in
+  let expr' := fresh "input_expr" in
+  pose (expr' := expr);
+  let res' := fresh "result" in
+  pose (res' := res);
+  let lemma := get_L1 FLD in
+  let lemma :=
+    constr:(lemma O fv List.nil expr' res' I List.nil (refl_equal _)) in
+  let ty := type of lemma in
+  let lhs := match ty with
+    forall _, ?lhs=_ -> _ => lhs
+    end in
+  let rhs := match ty with
+    forall _, _=_ -> forall _, ?rhs=_ -> _ => rhs
+    end in
+  let lhs' := fresh "lhs" in let lhs_eq := fresh "lhs_eq" in
+  let rhs' := fresh "rhs" in let rhs_eq := fresh "rhs_eq" in
+  compute_assertion lhs_eq lhs' lhs;
+  compute_assertion rhs_eq rhs' rhs;
+  let H := fresh "fld_eqn" in
+  refine (_ (lemma lhs' lhs_eq rhs' rhs_eq _ _));
+    (* main goal *)
+    [intro H;protect_fv "field" in H; revert H
+    (* ring-nf(lhs') = ring-nf(rhs') *)
+    | vm_compute; reflexivity || fail "field cannot prove this equality"
+    (* denominator condition *)
+    | simpl_PCond FLD];
+  clear lhs_eq rhs_eq; subst lhs' rhs'.
+
+Ltac prove_with_field ope c :=
+  gen_with_field ltac:(prove_field_eqn ope) c.
+
+(* Prove an equation x=ope(x) and rewrite with it *)
+Ltac prove_rw ope x :=
+  prove_with_field ope x;
+  [ let H := fresh "Heq_maple" in
+    intro H; rewrite H; clear H
+  |..].
+
+(* Apply ope (FExpr->FExpr) on an expression *)
+Ltac reduce_field_expr ope kont FLD fv expr :=
+  let evfun := get_FEeval FLD in
+  let res := ope expr in
+  let c := (eval simpl_field_expr in (evfun fv res)) in
+  kont c.
+
+(* Hack to let a Ltac return a term in the context of a primitive tactic *)
+Ltac return_term x := generalize (refl_equal x).
+
+(* Turn an operation on field expressions (FExpr) into a reduction
+   on terms (in the field carrier). Because of field_lookup,
+   the tactic cannot return a term directly, so it is returned 
+   via the conclusion of the goal (return_term). *)
+Ltac reduce_field_ope ope c :=
+  gen_with_field ltac:(reduce_field_expr ope return_term) c.
+
+
 (* Adding a new field *)
 
 Ltac ring_of_field f :=
diff --git a/contrib/setoid_ring/Ring_tac.v b/contrib/setoid_ring/Ring_tac.v
index 53679cd5cc..44e97bda77 100644
--- a/contrib/setoid_ring/Ring_tac.v
+++ b/contrib/setoid_ring/Ring_tac.v
@@ -50,7 +50,7 @@ Ltac OnMainSubgoal H ty :=
   end.
 
 (* A generic pattern to have reflexive tactics do some computation:
-   lemmas of the form [forall x', x=x' -> P(x')] is understood as
+   lemmas of the form [forall x', x=x' -> P(x')] are understood as:
    compute the normal form of x, instantiate x' with it, prove
    hypothesis x=x' with vm_compute and reflexivity, and pass the
    instantiated lemma to the continuation.
@@ -63,17 +63,33 @@ Ltac ProveLemmaHyp lemma :=
         let H := fresh "res_eq" in
         compute_assertion H x' x;
         let lemma' := constr:(lemma x' H) in
-        kont (lemma x' H);
-        (clear x' H||idtac"ProveLemmaHyp: cleanup failed"))
-  | _ => (fun _ => fail "ProveLemmaHyp: lemma not of the expexted form")
+        kont lemma';
+        (clear H||idtac"ProveLemmaHyp: cleanup failed");
+        subst x')
+  | _ => (fun _ => fail "ProveLemmaHyp: lemma not of the expected form")
   end.
 
+Ltac ProveLemmaHyps lemma :=
+  match type of lemma with
+    forall x', ?x = x' -> _ =>
+      (fun kont => 
+        let x' := fresh "res" in 
+        let H := fresh "res_eq" in
+        compute_assertion H x' x;
+        let lemma' := constr:(lemma x' H) in
+        ProveLemmaHyps lemma' kont;
+        (clear H||idtac"ProveLemmaHyps: cleanup failed");
+        subst x')
+  | _ => (fun kont => kont lemma)
+  end.
+
+(*
 Ltac ProveLemmaHyps lemma := (* expects a continuation *)
   let try_step := ProveLemmaHyp lemma in
   (fun kont =>
     try_step ltac:(fun lemma' => ProveLemmaHyps lemma' kont) ||
     kont lemma).
-
+*)
 Ltac ApplyLemmaThen lemma expr kont :=
   let lem := constr:(lemma expr) in
   ProveLemmaHyp lem ltac:(fun lem' =>
@@ -97,9 +113,9 @@ Ltac ApplyLemmaThenAndCont lemma expr tac CONT_tac cont_arg :=
   OnMainSubgoal Heq ltac:(type of Heq)
     ltac:(try tac Heq; clear Heq pe';CONT_tac cont_arg)).
 *)
-Ltac ApplyLemmaThenAndCont lemma expr tac CONT_tac cont_arg :=
+Ltac ApplyLemmaThenAndCont lemma expr tac CONT_tac :=
   ApplyLemmaThen lemma expr
-    ltac:(fun lemma' => try tac lemma'; CONT_tac cont_arg).
+    ltac:(fun lemma' => try tac lemma'; CONT_tac()).
 
 (* General scheme of reflexive tactics using of correctness lemma
    that involves normalisation of one expression
@@ -119,11 +135,11 @@ Ltac ReflexiveRewriteTactic
   (* extend the atom list *)
   let fv := list_fold_left FV_tac fv terms in
   let RW_tac lemma := 
-     let fcons term CONT_tac cont_arg := 
+     let fcons term CONT_tac :=
       let expr := SYN_tac term fv in
-      (ApplyLemmaThenAndCont lemma expr MAIN_tac CONT_tac cont_arg) in
+      (ApplyLemmaThenAndCont lemma expr MAIN_tac CONT_tac) in
      (* rewrite steps *)
-     lazy_list_fold_right fcons ltac:(idtac) terms in
+     lazy_list_fold_right fcons ltac:(fun _=>idtac) terms in
   LEMMA_tac fv RW_tac.
 
 (********************************************************)
@@ -340,7 +356,8 @@ Ltac Ring_norm_gen f RNG lemma lH rl :=
       || fail "type error when build the rewriting lemma");
     clear vlmp_eq;
     kont H;
-    (clear H vlmp vlpe||idtac"Ring_norm_gen: cleanup failed") in
+    (clear H||idtac"Ring_norm_gen: cleanup failed");
+    subst vlpe vlmp in
   let simpl_ring H := (protect_fv "ring" in H; f H) in
   ReflexiveRewriteTactic mkFV mkPol lemma_tac simpl_ring fv rl.
 
@@ -410,77 +427,3 @@ Tactic Notation
   intro H;
   unfold g;clear g.
 
-
-
-(*     LE RESTE MARCHE PAS DOMMAGE  .....  *)
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-(*
-
-
-
-
-
-
-
-
-Ltac Ring_simplify_in hyp:= Ring_simplify_gen ltac:(fun H => rewrite H in hyp).
-
-
-Tactic Notation (at level 0) 
-  "ring_simplify" "[" constr_list(lH) "]" constr_list(rl) := 
-  match goal with [|- ?G] => ring_lookup Ring_simplify [lH] rl G end.
-
-Tactic Notation (at level 0) 
-  "ring_simplify" constr_list(rl) := 
-  match goal with [|- ?G] => ring_lookup Ring_simplify [] rl G end.
-
-Tactic Notation (at level 0) 
-  "ring_simplify" "[" constr_list(lH) "]" constr_list(rl) "in" hyp(h):= 
-  let t := type of h in
-  ring_lookup 
-   (fun req sth ext morph arth cst_tac pow_tac lemma1 lemma2 pre post lH rl =>
-     pre(); 
-     Ring_norm_gen ltac:(fun EQ => rewrite EQ in h) cst_tac pow_tac lemma2 req ring_subst_niter lH rl; 
-     post()) 
-  [lH] rl t. 
-(*  ring_lookup ltac:(Ring_simplify_in h) [lH] rl [t]. NE MARCHE PAS ??? *)
-
-Ltac Ring_simpl_in hyp := Ring_norm_gen ltac:(fun H => rewrite H in hyp).
-
-Tactic Notation (at level 0) 
-  "ring_simplify" constr_list(rl) "in" constr(h):= 
-  let t := type of h in
-  ring_lookup   
-   (fun req sth ext morph arth cst_tac pow_tac lemma1 lemma2 pre post lH rl =>
-     pre(); 
-     Ring_simpl_in h cst_tac pow_tac lemma2 req ring_subst_niter lH rl; 
-     post())
- [] rl t.
-
-Ltac rw_in H Heq := rewrite Heq in H.
-
-Ltac simpl_in H := 
-  let t := type of H in
-   ring_lookup 
-   (fun req sth ext morph arth cst_tac pow_tac lemma1 lemma2 pre post lH rl =>
-     pre(); 
-     Ring_norm_gen ltac:(fun Heq => rewrite Heq in H) cst_tac pow_tac lemma2 req ring_subst_niter lH rl; 
-     post()) 
-   [] t.
-
-
-*)