1 files changed, 266 insertions, 70 deletions

diff --git a/contrib/setoid_ring/Ring_tac.v b/contrib/setoid_ring/Ring_tac.v
index 95efde7f..7419f184 100644
--- a/contrib/setoid_ring/Ring_tac.v
+++ b/contrib/setoid_ring/Ring_tac.v
@@ -3,16 +3,23 @@ Require Import Setoid.
 Require Import BinPos.
 Require Import Ring_polynom.
 Require Import BinList.
+Require Import InitialRing.
 Declare ML Module "newring".
-
+  
 
 (* adds a definition id' on the normal form of t and an hypothesis id
    stating that t = id' (tries to produces a proof as small as possible) *)
 Ltac compute_assertion id  id' t :=
   let t' := eval vm_compute in t in
-  (pose (id' := t');
-   assert (id : t = id');
-   [exact_no_check (refl_equal id')|idtac]).
+  pose (id' := t');
+  assert (id : t = id');
+  [vm_cast_no_check (refl_equal id')|idtac].
+(* [exact_no_check (refl_equal id'<: t = id')|idtac]). *)
+
+Ltac getGoal :=
+  match goal with 
+  | |- ?G => G
+  end.
 
 (********************************************************************)
 (* Tacticals to build reflexive tactics *)
@@ -23,7 +30,6 @@ Ltac OnEquation req :=
   | _ => fail 1 "Goal is not an equation (of expected equality)"
   end.
 
-
 Ltac OnMainSubgoal H ty :=
   match ty with
   | _ -> ?ty' =>
@@ -32,43 +38,54 @@ Ltac OnMainSubgoal H ty :=
   | _ => (fun tac => tac)
   end.
 
-Ltac ApplyLemmaAndSimpl tac lemma pe:=
-  let npe := fresh "ast_nf" in
+Ltac ApplyLemmaThen lemma expr tac :=
+  let nexpr := fresh "expr_nf" in
+  let H := fresh "eq_nf" in
+  let Heq := fresh "thm" in
+  let nf_spec :=
+    match type of (lemma expr) with
+      forall x, ?nf_spec = x -> _ => nf_spec
+    | _ => fail 1 "ApplyLemmaThen: cannot find norm expression"
+    end in
+  (compute_assertion H nexpr nf_spec;
+   (assert (Heq:=lemma _ _ H) || fail "anomaly: failed to apply lemma");
+   clear H;
+   OnMainSubgoal Heq ltac:(type of Heq) ltac:(tac Heq; clear Heq nexpr)).
+
+Ltac ApplyLemmaThenAndCont lemma expr tac CONT_tac cont_arg :=
+  let npe := fresh "expr_nf" in
   let H := fresh "eq_nf" in
   let Heq := fresh "thm" in
   let npe_spec :=
-    match type of (lemma pe) with
+    match type of (lemma expr) with
       forall npe, ?npe_spec = npe -> _ => npe_spec
-    | _ => fail 1 "ApplyLemmaAndSimpl: cannot find norm expression"
+    | _ => fail 1 "ApplyLemmaThenAndCont: cannot find norm expression"
     end in
   (compute_assertion H npe npe_spec;
    (assert (Heq:=lemma _ _ H) || fail "anomaly: failed to apply lemma");
    clear H;
    OnMainSubgoal Heq ltac:(type of Heq)
-     ltac:(tac Heq; rewrite Heq; clear Heq npe)).
+     ltac:(try tac Heq; clear Heq npe;CONT_tac cont_arg)).
 
 (* General scheme of reflexive tactics using of correctness lemma
    that involves normalisation of one expression *)
-Ltac ReflexiveRewriteTactic FV_tac SYN_tac SIMPL_tac lemma2 req rl :=
-  let R := match type of req with ?R -> _ => R end in
-  (* build the atom list *)
-  let fv := list_fold_left FV_tac (@List.nil R) rl in
-  (* some type-checking to avoid late errors *)
-  (check_fv fv;
-   (* rewrite steps *)
-   list_iter
-     ltac:(fun r =>
-       let ast := SYN_tac r fv in
-       try ApplyLemmaAndSimpl SIMPL_tac (lemma2 fv) ast)
-     rl).
+
+Ltac ReflexiveRewriteTactic FV_tac SYN_tac MAIN_tac LEMMA_tac fv terms :=
+  (* 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 expr := SYN_tac term fv in
+      (ApplyLemmaThenAndCont lemma expr MAIN_tac CONT_tac cont_arg) in
+     (* rewrite steps *)
+     lazy_list_fold_right fcons ltac:(idtac) terms in
+  LEMMA_tac fv RW_tac.
 
 (********************************************************)
 
-(* An object to return when an expression is not recognized as a constant *)
-Definition NotConstant := false.
-		      
+
 (* Building the atom list of a ring expression *)
-Ltac FV Cst add mul sub opp t fv :=
+Ltac FV Cst CstPow add mul sub opp pow t fv :=
  let rec TFV t fv :=
   match Cst t with
   | NotConstant =>
@@ -77,6 +94,11 @@ Ltac FV Cst add mul sub opp t fv :=
       | (mul ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv)
       | (sub ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv)
       | (opp ?t1) => TFV t1 fv
+      | (pow ?t1 ?n) =>
+        match CstPow n with
+        | InitialRing.NotConstant => AddFvTail t fv
+        | _ => TFV t1 fv
+        end
       | _ => AddFvTail t fv
       end
   | _ => fv
@@ -84,10 +106,10 @@ Ltac FV Cst add mul sub opp t fv :=
  in TFV t fv.
 
  (* syntaxification of ring expressions *)
- Ltac mkPolexpr C Cst radd rmul rsub ropp t fv := 
+Ltac mkPolexpr C Cst CstPow radd rmul rsub ropp rpow t fv := 
  let rec mkP t :=
     match Cst t with
-    | NotConstant =>
+    | InitialRing.NotConstant =>
         match t with 
         | (radd ?t1 ?t2) => 
           let e1 := mkP t1 in
@@ -100,6 +122,12 @@ Ltac FV Cst add mul sub opp t fv :=
           let e2 := mkP t2 in constr:(PEsub e1 e2)
         | (ropp ?t1) =>
           let e1 := mkP t1 in constr:(PEopp e1)
+        | (rpow ?t1 ?n) =>
+          match CstPow n with
+          | InitialRing.NotConstant => 
+            let p := Find_at t fv in constr:(PEX C p)
+          | ?c => let e1 := mkP t1 in constr:(PEpow e1 c)
+          end
         | _ =>
           let p := Find_at t fv in constr:(PEX C p)
         end
@@ -107,54 +135,222 @@ Ltac FV Cst add mul sub opp t fv :=
     end
  in mkP t.
 
+Ltac ParseRingComponents lemma :=
+  match type of lemma with
+  | context
+     [@PEeval ?R ?rO ?add ?mul ?sub ?opp ?C ?phi ?Cpow ?powphi ?pow _ _] =>
+      (fun f => f R add mul sub opp pow C)
+  | _ => fail 1 "ring anomaly: bad correctness lemma (parse)"
+  end.
+
+
 (* ring tactics *)
 
- Ltac Ring Cst_tac lemma1 req :=
-  let Make_tac :=
-    match type of lemma1 with
-    | forall (l:list ?R) (pe1 pe2:PExpr ?C),
-      _ = true ->
-      req (PEeval ?rO ?add ?mul ?sub ?opp ?phi l pe1) _ =>
-        let mkFV := FV Cst_tac add mul sub opp in
-        let mkPol := mkPolexpr C Cst_tac add mul sub opp in
-        fun f => f R mkFV mkPol
-    | _ => fail 1 "ring anomaly: bad correctness lemma"
+Ltac FV_hypo_tac mkFV req lH :=
+  let R := match type of req with ?R -> _ => R end in
+  let FV_hypo_l_tac h :=
+    match h with @mkhypo (req ?pe _) _ => mkFV pe end in
+  let FV_hypo_r_tac h :=
+    match h with @mkhypo (req _ ?pe) _ => mkFV pe end in
+  let fv := list_fold_right FV_hypo_l_tac (@nil R) lH in
+  list_fold_right FV_hypo_r_tac fv lH.
+
+Ltac mkHyp_tac C req mkPE lH :=
+  let mkHyp h res := 
+   match h with 
+   | @mkhypo (req ?r1 ?r2) _ =>
+     let pe1 := mkPE r1 in
+     let pe2 := mkPE r2 in
+     constr:(cons (pe1,pe2) res)
+   | _ => fail "hypothesis is not a ring equality"
+   end in
+  list_fold_right mkHyp (@nil (PExpr C * PExpr C)) lH.
+     
+Ltac proofHyp_tac lH :=
+  let get_proof h :=
+    match h with
+    | @mkhypo _ ?p => p
     end in
-  let Main r1 r2 R mkFV mkPol :=
-    let fv := mkFV r1 (@List.nil R) in
-    let fv := mkFV r2 fv in
-    check_fv fv;
-    (let pe1 := mkPol r1 fv in
-     let pe2 := mkPol r2 fv in
-     apply (lemma1 fv pe1 pe2) || fail "typing error while applying ring";
-     vm_compute;
-     exact (refl_equal true) || fail "not a valid ring equation") in
-  Make_tac ltac:(OnEquation req Main).
-
-Ltac Ring_simplify Cst_tac lemma2 req rl :=
-  let Make_tac :=
-    match type of lemma2 with 
-      forall (l:list ?R) (pe:PExpr ?C) (npe:Pol ?C),
-      _ = npe ->
-      req (PEeval ?rO ?add ?mul ?sub ?opp ?phi l pe) _ =>
-      let mkFV := FV Cst_tac add mul sub opp in
-      let mkPol := mkPolexpr C Cst_tac add mul sub opp in
-      let simpl_ring H := protect_fv "ring" in H in
-      (fun tac => tac mkFV mkPol simpl_ring lemma2 req rl)
-    | _ => fail 1 "ring anomaly: bad correctness lemma"
+  let rec bh l :=
+    match l with
+    | nil => constr:(I)
+    | cons ?h nil => get_proof h
+    | cons ?h ?tl => 
+      let l := get_proof h in
+      let r := bh tl in  
+      constr:(conj l r)
     end in
-  Make_tac ReflexiveRewriteTactic.
+  bh lH.
+
+Definition ring_subst_niter := (10*10*10)%nat.
+ 
+Ltac Ring Cst_tac CstPow_tac lemma1 req n lH :=
+  let Main lhs rhs R radd rmul rsub ropp rpow C :=
+    let mkFV := FV Cst_tac CstPow_tac radd rmul rsub ropp rpow in
+    let mkPol := mkPolexpr C Cst_tac CstPow_tac radd rmul rsub ropp rpow in
+    let fv := FV_hypo_tac mkFV req lH in
+    let fv := mkFV lhs fv in
+    let fv := mkFV rhs fv in
+    check_fv fv;
+    let pe1 := mkPol lhs fv in
+    let pe2 := mkPol rhs fv in
+    let lpe := mkHyp_tac C req ltac:(fun t => mkPol t fv) lH in
+    let vlpe := fresh "hyp_list" in
+    let vfv := fresh "fv_list" in
+    pose (vlpe := lpe);
+    pose (vfv := fv);
+    (apply (lemma1 n vfv vlpe pe1 pe2)
+      || fail "typing error while applying ring");
+    [ ((let prh := proofHyp_tac lH in exact prh)
+        || idtac "can not automatically proof hypothesis : maybe a left member of a hypothesis is not a monomial") 
+    | vm_compute;
+      (exact (refl_equal true) || fail "not a valid ring equation")] in
+  ParseRingComponents lemma1 ltac:(OnEquation req Main).
+
+Ltac Ring_norm_gen f Cst_tac CstPow_tac lemma2 req n lH rl :=
+  let Main R add mul sub opp pow C :=
+    let mkFV := FV Cst_tac CstPow_tac add mul sub opp pow in
+    let mkPol := mkPolexpr C Cst_tac CstPow_tac add mul sub opp pow in
+    let fv := FV_hypo_tac mkFV req lH in
+    let simpl_ring H := (protect_fv "ring" in H; f H) in
+    let Coeffs :=
+      match type of lemma2 with
+      | context [mk_monpol_list ?cO ?cI ?cadd ?cmul ?csub ?copp ?ceqb _] =>
+        (fun f => f cO cI cadd cmul csub copp ceqb)
+      | _ => fail 1 "ring_simplify anomaly: bad correctness lemma"
+      end in
+    let lemma_tac fv RW_tac := 
+      let rr_lemma := fresh "r_rw_lemma" in
+      let lpe := mkHyp_tac C req ltac:(fun t => mkPol t fv) lH in
+      let vlpe := fresh "list_hyp" in
+      let vlmp := fresh "list_hyp_norm" in
+      let vlmp_eq := fresh "list_hyp_norm_eq" in
+      let prh := proofHyp_tac lH in
+      pose (vlpe := lpe);
+      Coeffs ltac:(fun cO cI cadd cmul csub copp ceqb =>
+        compute_assertion vlmp_eq vlmp 
+            (mk_monpol_list cO cI cadd cmul csub copp ceqb vlpe);
+        assert (rr_lemma := lemma2 n vlpe fv prh vlmp vlmp_eq)
+         || fail "type error when build the rewriting lemma";
+        RW_tac rr_lemma;
+        try clear rr_lemma vlmp_eq vlmp vlpe) in
+    ReflexiveRewriteTactic mkFV mkPol simpl_ring lemma_tac fv rl in
+  ParseRingComponents lemma2 Main.
 
+Ltac Ring_gen
+  req sth ext morph arth cst_tac pow_tac lemma1 lemma2 pre post lH rl :=
+  pre();Ring cst_tac pow_tac lemma1 req ring_subst_niter lH.
 
 Tactic Notation (at level 0) "ring" :=
-  ring_lookup
-    (fun req sth ext morph arth cst_tac lemma1 lemma2 pre post rl =>
-       pre(); Ring cst_tac lemma1 req).
+  let G := getGoal in ring_lookup Ring_gen [] [G].
+
+Tactic Notation (at level 0) "ring" "[" constr_list(lH) "]" :=
+  let G := getGoal in ring_lookup Ring_gen [lH] [G].
+
+(* Simplification *)
+
+Ltac Ring_simplify_gen f :=
+  fun req sth ext morph arth cst_tac pow_tac lemma1 lemma2 pre post lH rl =>
+     let l := fresh "to_rewrite" in
+     pose (l:= rl);
+     generalize (refl_equal l);
+     unfold l at 2;
+     pre(); 
+     match goal with
+     | [|- l = ?RL -> _ ] =>
+       let Heq := fresh "Heq" in
+       intros Heq;clear Heq l;
+       Ring_norm_gen f cst_tac pow_tac lemma2 req ring_subst_niter lH RL; 
+       post()
+     | _ => fail 1 "ring_simplify anomaly: bad goal after pre"
+     end.
+
+Ltac Ring_simplify := Ring_simplify_gen ltac:(fun H => rewrite H).
+
+Ltac Ring_nf Cst_tac lemma2 req rl f :=
+  let on_rhs H :=
+   match type of H with
+   | req _ ?rhs => clear H; f rhs
+   end in
+  Ring_norm_gen on_rhs Cst_tac lemma2 req rl.
+
+
+Tactic Notation (at level 0) 
+  "ring_simplify" "[" constr_list(lH) "]" constr_list(rl) :=
+  let G := getGoal in ring_lookup Ring_simplify [lH] rl [G].
+
+Tactic Notation (at level 0) 
+  "ring_simplify" constr_list(rl) := 
+  let G := getGoal in ring_lookup Ring_simplify [] rl [G].
+
+
+Tactic Notation "ring_simplify" constr_list(rl) "in" hyp(H):=   
+ let G := getGoal in
+ let t := type of H in   
+ let g := fresh "goal" in
+ set (g:= G);
+ generalize H;clear H;
+ ring_lookup Ring_simplify [] rl [t];
+ intro H;
+ unfold g;clear g.
+
+Tactic Notation "ring_simplify" "["constr_list(lH)"]" constr_list(rl) "in" hyp(H):=   
+ let G := getGoal in
+ let t := type of H in   
+ let g := fresh "goal" in
+ set (g:= G);
+ generalize H;clear H;
+ ring_lookup Ring_simplify [lH] rl [t];
+ intro H;
+ unfold g;clear g.
+
+
+(*
+
+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].
 
-Tactic Notation (at level 0) "ring_simplify" constr_list(rl) :=
-  ring_lookup
-    (fun req sth ext morph arth cst_tac lemma1 lemma2 pre post rl =>
-       pre(); Ring_simplify cst_tac lemma2 req rl; post()) rl.
 
-(* A simple macro tactic to be prefered to ring_simplify *)
-Ltac ring_replace t1 t2 := replace t1 with t2 by ring.
+*)