Ring

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

1 files changed, 633 insertions, 0 deletions

diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml
new file mode 100644
index 000000000..2418e1abe
--- /dev/null
+++ b/contrib/ring/ring.ml
@@ -0,0 +1,633 @@
+
+(* $Id$ *)
+
+(* ML part of the Ring tactic *)
+
+open Pp
+open Util
+open Term
+open Names
+open Reduction
+open Tacmach
+open Proof_type
+open Proof_trees
+open Printer
+open Equality
+open Vernacinterp
+open Libobject
+open Closure 
+open Tactics
+open Pattern 
+open Hiddentac
+open Quote
+
+let mt_evd = Evd.empty
+let constr_of com = Astterm.interp_constr mt_evd (Global.env()) com
+
+let constant sp id = 
+  Declare.global_sp_reference (path_of_string sp) (id_of_string id)
+
+(* Ring_theory *)
+
+let coq_Ring_Theory = 
+  lazy (constant "#Ring_theory#Ring_Theory.cci" "Ring_Theory")
+let coq_Semi_Ring_Theory = 
+  lazy (constant "#Ring_theory#Semi_Ring_Theory.cci" "Semi_Ring_Theory")
+
+(* Ring_normalize *)
+let coq_SPplus = lazy (constant "#Ring_normalize#spolynomial.cci" "SPplus")
+let coq_SPmult = lazy (constant "#Ring_normalize#spolynomial.cci" "SPmult")
+let coq_SPvar = lazy (constant "#Ring_normalize#spolynomial.cci" "SPvar")
+let coq_SPconst = lazy (constant "#Ring_normalize#spolynomial.cci" "SPconst")
+let coq_Pplus = lazy (constant "#Ring_normalize#polynomial.cci" "Pplus")
+let coq_Pmult = lazy (constant "#Ring_normalize#polynomial.cci" "Pmult")
+let coq_Pvar = lazy (constant "#Ring_normalize#polynomial.cci" "Pvar")
+let coq_Pconst = lazy (constant "#Ring_normalize#polynomial.cci" "Pconst")
+let coq_Popp = lazy (constant "#Ring_normalize#polynomial.cci" "Popp")
+let coq_interp_sp = lazy (constant "#Ring_normalize#interp_sp.cci" "interp_sp")
+let coq_interp_p = lazy (constant "#Ring_normalize#interp_p.cci" "interp_p")
+let coq_interp_cs = lazy (constant "#Ring_normalize#interp_cs.cci" "interp_cs")
+let coq_spolynomial_simplify = 
+  lazy (constant "#Ring_normalize#spolynomial_simplify.cci" 
+	  "spolynomial_simplify")
+let coq_polynomial_simplify = 
+  lazy (constant "#Ring_normalize#polynomial_simplify.cci"
+	  "polynomial_simplify")
+let coq_spolynomial_simplify_ok = 
+  lazy (constant "#Ring_normalize#spolynomial_simplify_ok.cci"
+	  "spolynomial_simplify_ok")
+let coq_polynomial_simplify_ok = 
+  lazy (constant "#Ring_normalize#polynomial_simplify_ok.cci"
+	  "polynomial_simplify_ok")
+
+(* Ring_abstract *)
+let coq_ASPplus = lazy (constant "#Ring_abstract#aspolynomial.cci" "ASPplus")
+let coq_ASPmult = lazy (constant "#Ring_abstract#aspolynomial.cci" "ASPmult")
+let coq_ASPvar = lazy (constant "#Ring_abstract#aspolynomial.cci" "ASPvar")
+let coq_ASP0 = lazy (constant "#Ring_abstract#aspolynomial.cci" "ASP0")
+let coq_ASP1 = lazy (constant "#Ring_abstract#aspolynomial.cci" "ASP1")
+let coq_APplus = lazy (constant "#Ring_abstract#apolynomial.cci" "APplus")
+let coq_APmult = lazy (constant "#Ring_abstract#apolynomial.cci" "APmult")
+let coq_APvar = lazy (constant "#Ring_abstract#apolynomial.cci" "APvar")
+let coq_AP0 = lazy (constant "#Ring_abstract#apolynomial.cci" "AP0")
+let coq_AP1 = lazy (constant "#Ring_abstract#apolynomial.cci" "AP1")
+let coq_APopp = lazy (constant "#Ring_abstract#apolynomial.cci" "APopp")
+let coq_interp_asp = 
+  lazy (constant "#Ring_abstract#interp_asp.cci" "interp_asp")
+let coq_interp_ap = 
+  lazy (constant "#Ring_abstract#interp_ap.cci" "interp_ap")
+let coq_interp_acs = 
+  lazy (constant "#Ring_abstract#interp_acs.cci" "interp_acs")
+let coq_interp_sacs = 
+  lazy (constant "#Ring_abstract#interp_sacs.cci" "interp_sacs")
+let coq_aspolynomial_normalize = 
+  lazy (constant "#Ring_abstract#aspolynomial_normalize.cci"
+	  "aspolynomial_normalize")
+let coq_apolynomial_normalize = 
+  lazy (constant "#Ring_abstract#apolynomial_normalize.cci"
+	  "apolynomial_normalize")
+let coq_aspolynomial_normalize_ok = 
+  lazy (constant "#Ring_abstract#aspolynomial_normalize_ok.cci" 
+	  "aspolynomial_normalize_ok")
+let coq_apolynomial_normalize_ok = 
+  lazy (constant "#Ring_abstract#apolynomial_normalize_ok.cci"
+	  "apolynomial_simplify_ok")
+
+(* Logic *)
+let coq_f_equal2 = lazy (constant "#Logic#f_equal2.cci" "f_equal2")
+let coq_eq = lazy (constant "#Logic#eq.cci" "eq")
+let coq_eqT = lazy (constant "#Logic_Type#eqT.cci" "eqT")
+
+(*********** Useful types and functions ************)
+
+module OperSet = 
+  Set.Make (struct 
+	      type t = sorts oper
+	      let compare = (Pervasives.compare : t->t->int)
+	    end)	
+
+type theory =
+    { th_ring : bool;                  (* false for a semi-ring *)
+      th_abstract : bool;
+      th_a : constr;                   (* e.g. nat *)
+      th_plus : constr;
+      th_mult : constr;
+      th_one : constr;
+      th_zero : constr;
+      th_opp : constr;                 (* Not used if semi-ring *)
+      th_eq : constr;
+      th_t : constr;                   (* e.g. NatTheory *)
+      th_closed : ConstrSet.t;         (* e.g. [S; O] *)
+                                       (* Must be empty for an abstract ring *)
+    }
+
+(* Theories are stored in a table which is synchronised with the Reset 
+   mechanism. *)
+
+module Cmap = Map.Make(struct type t = constr let compare = compare end)
+
+let theories_map = ref Cmap.empty
+
+let theories_map_add (c,t) = theories_map := Cmap.add c t !theories_map
+let theories_map_find c = Cmap.find c !theories_map
+let theories_map_mem c = Cmap.mem c !theories_map
+
+let _ = 
+  Summary.declare_summary "tactic-ring-table"
+    { Summary.freeze_function = (fun () -> !theories_map);
+      Summary.unfreeze_function = (fun t -> theories_map := t);
+      Summary.init_function = (fun () -> theories_map := Cmap.empty) }
+
+(* declare a new type of object in the environment, "tactic-ring-theory"
+   The functions theory_to_obj and obj_to_theory do the conversions
+   between theories and environement objects. *)
+
+let (theory_to_obj, obj_to_theory) = 
+  let cache_th (_,(c, th)) = theories_map_add (c,th)
+  and spec_th x = x in
+  declare_object ("tactic-ring-theory",
+		  { load_function = (fun _ -> ());
+		    open_function = (fun _ -> ());
+                    cache_function = cache_th;
+		    specification_function = spec_th })
+
+(* from the set A, guess the associated theory *)
+(* With this simple solution, the theory to use is automatically guessed *)
+(* But only one theory can be declared for a given Set *)
+
+let guess_theory a =
+  try 
+    theories_map_find a
+  with Not_found -> 
+    errorlabstrm "Ring" 
+      [< 'sTR "No Declared Ring Theory for ";
+	 prterm a; 'fNL;
+	 'sTR "Use Add [Semi] Ring to declare it">]
+
+(* Add a Ring or a Semi-Ring to the database after a type verification *)
+
+let add_theory want_ring want_abstract a aplus amult aone azero aopp aeq t cset = 
+  if theories_map_mem a then errorlabstrm "Add Semi Ring" 
+    [< 'sTR "A (Semi-)Ring Structure is already declared for "; prterm a >];
+  let env = Global.env () in
+  if (want_ring & 
+      not (is_conv env Evd.empty (Typing.type_of env Evd.empty t)
+	     (mkAppL [| Lazy.force coq_Ring_Theory; a; aplus; amult;
+			aone; azero; aopp; aeq |]))) then
+    errorlabstrm "addring" [< 'sTR "Not a valid Ring theory" >];
+  if (not want_ring &
+      not (is_conv  env Evd.empty (Typing.type_of env Evd.empty t) 
+	     (mkAppL [| Lazy.force coq_Semi_Ring_Theory; a; 
+			aplus; amult; aone; azero; aeq |]))) then 
+    errorlabstrm "addring" [< 'sTR "Not a valid Semi-Ring theory" >];
+  Lib.add_anonymous_leaf
+    (theory_to_obj 
+       (a, { th_ring = want_ring;
+	     th_abstract = want_abstract;
+	     th_a = a;
+	     th_plus = aplus;
+	     th_mult = amult;
+	     th_one = aone;
+	     th_zero = azero;
+	     th_opp = aopp;
+	     th_eq = aeq;
+	     th_t = t;
+	     th_closed = cset }))
+
+(* The vernac commands "Add Ring" and "Add Semi Ring" *)
+(* see file Ring.v for examples of this command *)
+
+let constr_of_comarg = function 
+  | VARG_CONSTR c -> constr_of c
+  | _ -> anomaly "Add (Semi) Ring"
+  
+let cset_of_comarg_list l = 
+  List.fold_right ConstrSet.add (List.map constr_of_comarg l) ConstrSet.empty
+
+let _ = 
+  vinterp_add "AddSemiRing"
+    (function
+       | (VARG_CONSTR a)::(VARG_CONSTR aplus)::(VARG_CONSTR amult)
+	 ::(VARG_CONSTR aone)::(VARG_CONSTR azero)::(VARG_CONSTR aeq)
+	 ::(VARG_CONSTR t)::l -> 
+	   (fun () -> (add_theory false false
+			 (constr_of a)
+			 (constr_of aplus)
+			 (constr_of amult)
+			 (constr_of aone)
+			 (constr_of azero)
+			 (mkXtra "not a term")
+			 (constr_of aeq)
+			 (constr_of t)
+			 (cset_of_comarg_list l)))
+       | _ -> anomaly "AddSemiRing")
+
+let _ = 
+  vinterp_add "AddRing"
+    (function 
+       | (VARG_CONSTR a)::(VARG_CONSTR aplus)::(VARG_CONSTR amult)
+	 ::(VARG_CONSTR aone)::(VARG_CONSTR azero)::(VARG_CONSTR aopp)
+	 ::(VARG_CONSTR aeq)::(VARG_CONSTR t)::l -> 
+	   (fun () -> (add_theory true false
+			 (constr_of a)
+			 (constr_of aplus)
+			 (constr_of amult)
+			 (constr_of aone)
+			 (constr_of azero)
+			 (constr_of aopp)
+			 (constr_of aeq)
+			 (constr_of t)
+			 (cset_of_comarg_list l)))
+       | _ -> anomaly "AddRing")
+    
+let _ = 
+  vinterp_add "AddAbstractSemiRing"
+    (function 
+       | [VARG_CONSTR a; VARG_CONSTR aplus; 
+	  VARG_CONSTR amult; VARG_CONSTR aone;
+	  VARG_CONSTR azero; VARG_CONSTR aeq; VARG_CONSTR t] -> 
+	   (fun () -> (add_theory false false
+			 (constr_of a)
+			 (constr_of aplus)
+			 (constr_of amult)
+			 (constr_of aone)
+			 (constr_of azero)
+			 (mkXtra "not a term")
+			 (constr_of aeq)
+			 (constr_of t)
+			 ConstrSet.empty))
+       | _ -> anomaly "AddAbstractSemiRing")
+    
+let _ = 
+  vinterp_add "AddAbstractRing"
+    (function 
+       | [ VARG_CONSTR a; VARG_CONSTR aplus; 
+	   VARG_CONSTR amult; VARG_CONSTR aone;
+	   VARG_CONSTR azero; VARG_CONSTR aopp; 
+	   VARG_CONSTR aeq; VARG_CONSTR t ] -> 
+	   (fun () -> (add_theory true true
+			 (constr_of a)
+			 (constr_of aplus)
+			 (constr_of amult)
+			 (constr_of aone)
+			 (constr_of azero)
+			 (constr_of aopp)
+			 (constr_of aeq)
+			 (constr_of t)
+			 ConstrSet.empty))
+       | _ -> anomaly "AddAbstractRing")
+    
+(******** The tactic itself *********)
+
+(*
+   gl : goal sigma
+   th : semi-ring theory (concrete)
+   cl : constr list [c1; c2; ...]
+ 
+Builds 
+   - a list of tuples [(c1, c'1, c''1, c'1_eq_c''1); ... ] 
+  where c'i is convertible with ci and
+  c'i_eq_c''i is a proof of equality of c'i and c''i
+
+*)
+
+let build_spolynom gl th lc =
+  let varhash  = (Hashtbl.create 17 : (constr, constr) Hashtbl.t) in
+  let varlist = ref ([] : constr list) in (* list of variables *)
+  let counter = ref 1 in (* number of variables created + 1 *)
+  (* aux creates the spolynom p by a recursive destructuration of c 
+     and builds the varmap with side-effects *)
+  let rec aux c = 
+    match (kind_of_term (whd_castapp c)) with 
+      | IsAppL (binop,[c1; c2]) when pf_conv_x gl binop th.th_plus ->
+	  mkAppL [| Lazy.force coq_SPplus; th.th_a; aux c1; aux c2 |]
+      | IsAppL (binop,[c1; c2]) when pf_conv_x gl binop th.th_mult ->
+	  mkAppL [| Lazy.force coq_SPmult; th.th_a; aux c1; aux c2 |]
+      | _ when closed_under th.th_closed c ->
+	  mkAppL [| Lazy.force coq_SPconst; th.th_a; c |]
+      | _ -> 
+	  try Hashtbl.find varhash c 
+	  with Not_found -> 
+	    let newvar = mkAppL [| Lazy.force coq_SPvar; th.th_a; 
+				   (path_of_int !counter) |] in
+	    begin 
+	      incr counter;
+	      varlist := c :: !varlist;
+	      Hashtbl.add varhash c newvar;
+	      newvar
+	    end
+  in 
+  let lp = List.map aux lc in
+  let v = btree_of_array (Array.of_list (List.rev !varlist)) th.th_a in
+  List.map 
+    (fun p -> 
+       (mkAppL [| Lazy.force coq_interp_sp; th.th_a; th.th_plus; th.th_mult; 
+		  th.th_zero; v; p |],
+	mkAppL [| Lazy.force coq_interp_cs; th.th_a; th.th_plus; th.th_mult; 
+		  th.th_one; th.th_zero; v;
+		  pf_reduce cbv_betadeltaiota gl 
+		    (mkAppL [| Lazy.force coq_spolynomial_simplify; 
+			       th.th_a; th.th_plus; th.th_mult; 
+			       th.th_one; th.th_zero; 
+			       th.th_eq; p|]) |],
+	mkAppL [| Lazy.force coq_spolynomial_simplify_ok;
+		  th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; 
+		  th.th_eq; v; th.th_t; p |]))
+    lp
+
+(*
+   gl : goal sigma
+   th : ring theory (concrete)
+   cl : constr list [c1; c2; ...]
+ 
+Builds 
+   - a list of tuples [(c1, c'1, c''1, c'1_eq_c''1); ... ] 
+  where c'i is convertible with ci and
+  c'i_eq_c''i is a proof of equality of c'i and c''i
+
+*)
+
+let build_polynom gl th lc =
+  let varhash  = (Hashtbl.create 17 : (constr, constr) Hashtbl.t) in
+  let varlist = ref ([] : constr list) in (* list of variables *)
+  let counter = ref 1 in (* number of variables created + 1 *)
+  let rec aux c = 
+    match (kind_of_term (whd_castapp c)) with 
+      | IsAppL (binop, [c1; c2]) when pf_conv_x gl binop th.th_plus ->
+	  mkAppL [| Lazy.force coq_Pplus; th.th_a; aux c1; aux c2 |]
+      | IsAppL (binop, [c1; c2]) when pf_conv_x gl binop th.th_mult ->
+	  mkAppL [| Lazy.force coq_Pmult; th.th_a; aux c1; aux c2 |]
+      (* The special case of Zminus *)
+      | IsAppL (binop, [c1; c2])
+	  when pf_conv_x gl c (mkAppL [| th.th_plus; c1; 
+	                                 mkAppL [| th.th_opp; c2 |] |]) ->
+	    mkAppL [| Lazy.force coq_Pplus; th.th_a; aux c1;
+	              mkAppL [| Lazy.force coq_Popp; th.th_a; aux c2 |] |]
+      | IsAppL (unop, [c1]) when pf_conv_x gl unop th.th_opp ->
+	  mkAppL [| Lazy.force coq_Popp; th.th_a; aux c1 |]
+      | _ when closed_under th.th_closed c ->
+	  mkAppL [| Lazy.force coq_Pconst; th.th_a; c |]
+      | _ -> 
+	  try Hashtbl.find varhash c 
+	  with Not_found -> 
+	    let newvar = mkAppL [| Lazy.force coq_Pvar; th.th_a; 
+				   (path_of_int !counter) |] in
+	    begin 
+	      incr counter;
+	      varlist := c :: !varlist;
+	      Hashtbl.add varhash c newvar;
+	      newvar
+	    end
+  in
+  let lp = List.map aux lc in
+  let v = (btree_of_array (Array.of_list (List.rev !varlist)) th.th_a) in
+  List.map 
+    (fun p -> 
+       (mkAppL [| Lazy.force coq_interp_p;
+		  th.th_a; th.th_plus; th.th_mult; th.th_zero; th.th_opp;
+		  v; p |],
+	mkAppL [| Lazy.force coq_interp_cs;
+		  th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; v;
+		  pf_reduce cbv_betadeltaiota gl 
+		    (mkAppL [| Lazy.force coq_polynomial_simplify; 
+			       th.th_a; th.th_plus; th.th_mult; 
+			       th.th_one; th.th_zero; 
+			       th.th_opp; th.th_eq; p |]) |],
+	mkAppL [| Lazy.force coq_polynomial_simplify_ok;
+		  th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; 
+		  th.th_opp; th.th_eq; v; th.th_t; p |]))
+    lp
+
+(*
+   gl : goal sigma
+   th : semi-ring theory (abstract)
+   cl : constr list [c1; c2; ...]
+ 
+Builds 
+   - a list of tuples [(c1, c'1, c''1, c'1_eq_c''1); ... ] 
+  where c'i is convertible with ci and
+  c'i_eq_c''i is a proof of equality of c'i and c''i
+
+*)
+
+let build_aspolynom gl th lc =
+  let varhash  = (Hashtbl.create 17 : (constr, constr) Hashtbl.t) in
+  let varlist = ref ([] : constr list) in (* list of variables *)
+  let counter = ref 1 in (* number of variables created + 1 *)
+  (* aux creates the aspolynom p by a recursive destructuration of c 
+     and builds the varmap with side-effects *)
+  let rec aux c = 
+    match (kind_of_term (whd_castapp c)) with 
+      | IsAppL (binop, [c1; c2]) when pf_conv_x gl binop th.th_plus ->
+	  mkAppL [| Lazy.force coq_ASPplus; aux c1; aux c2 |]
+      | IsAppL (binop, [c1; c2]) when pf_conv_x gl binop th.th_mult ->
+	  mkAppL [| Lazy.force coq_ASPmult; aux c1; aux c2 |]
+      | _ when pf_conv_x gl c th.th_zero -> Lazy.force coq_ASP0
+      | _ when pf_conv_x gl c th.th_one -> Lazy.force coq_ASP1
+      | _ -> 
+	  try Hashtbl.find varhash c 
+	  with Not_found -> 
+	    let newvar = mkAppL [| Lazy.force coq_ASPvar; 
+				   (path_of_int !counter) |] in
+	    begin 
+	      incr counter;
+	      varlist := c :: !varlist;
+	      Hashtbl.add varhash c newvar;
+	      newvar
+	    end
+  in 
+  let lp = List.map aux lc in
+  let v = btree_of_array (Array.of_list (List.rev !varlist)) th.th_a in
+  List.map 
+    (fun p -> 
+       (mkAppL [| Lazy.force coq_interp_asp; th.th_a; th.th_plus; th.th_mult; 
+		  th.th_one; th.th_zero; v; p |],
+	mkAppL [| Lazy.force coq_interp_acs; th.th_a; th.th_plus; th.th_mult; 
+		  th.th_one; th.th_zero; v;
+		  pf_reduce cbv_betadeltaiota gl 
+		    (mkAppL [| Lazy.force coq_aspolynomial_normalize; p|]) |],
+	mkAppL [| Lazy.force coq_spolynomial_simplify_ok;
+		  th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; 
+		  th.th_eq; v; th.th_t; p |]))
+    lp
+
+(*
+   gl : goal sigma
+   th : ring theory (abstract)
+   cl : constr list [c1; c2; ...]
+ 
+Builds 
+   - a list of tuples [(c1, c'1, c''1, c'1_eq_c''1); ... ] 
+  where c'i is convertible with ci and
+  c'i_eq_c''i is a proof of equality of c'i and c''i
+
+*)
+
+let build_apolynom gl th lc =
+  let varhash  = (Hashtbl.create 17 : (constr, constr) Hashtbl.t) in
+  let varlist = ref ([] : constr list) in (* list of variables *)
+  let counter = ref 1 in (* number of variables created + 1 *)
+  let rec aux c = 
+    match (kind_of_term (whd_castapp c)) with 
+      | IsAppL (binop, [c1; c2]) when pf_conv_x gl binop th.th_plus ->
+	  mkAppL [| Lazy.force coq_APplus; aux c1; aux c2 |]
+      | IsAppL (binop, [c1; c2]) when pf_conv_x gl binop th.th_mult ->
+	  mkAppL [| Lazy.force coq_APmult; aux c1; aux c2 |]
+      (* The special case of Zminus *)
+      | IsAppL (binop, [c1; c2]) 
+	  when pf_conv_x gl c (mkAppL [| th.th_plus; c1; 
+	                                 mkAppL [| th.th_opp; c2 |] |]) ->
+	    mkAppL [| Lazy.force coq_APplus; aux c1;
+	              mkAppL [| Lazy.force coq_APopp; aux c2 |] |]
+      | IsAppL (unop, [c1]) when pf_conv_x gl unop th.th_opp ->
+	  mkAppL [| Lazy.force coq_APopp; aux c1 |]
+      | _ when pf_conv_x gl c th.th_zero -> Lazy.force coq_AP0
+      | _ when pf_conv_x gl c th.th_one -> Lazy.force coq_AP1
+      | _ -> 
+	  try Hashtbl.find varhash c 
+	  with Not_found -> 
+	    let newvar = mkAppL [| Lazy.force coq_APvar; 
+				   (path_of_int !counter) |] in
+	    begin 
+	      incr counter;
+	      varlist := c :: !varlist;
+	      Hashtbl.add varhash c newvar;
+	      newvar
+	    end
+  in
+  let lp = List.map aux lc in
+  let v = (btree_of_array (Array.of_list (List.rev !varlist)) th.th_a) in
+  List.map 
+    (fun p -> 
+       (mkAppL [| Lazy.force coq_interp_ap;
+		  th.th_a; th.th_plus; th.th_mult; th.th_one; 
+		  th.th_zero; th.th_opp; v; p |],
+	mkAppL [| Lazy.force coq_interp_sacs;
+		  th.th_a; th.th_plus; th.th_mult; 
+		  th.th_one; th.th_zero; th.th_opp; v; 
+		  pf_reduce cbv_betadeltaiota gl 
+		    (mkAppL [| Lazy.force coq_apolynomial_normalize; p |]) |],
+	mkAppL [| Lazy.force coq_apolynomial_normalize_ok;
+		  th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; 
+		  th.th_opp; th.th_eq; v; th.th_t; p |]))
+    lp
+    
+module SectionPathSet = 
+  Set.Make(struct
+	     type t = section_path
+	     let compare = Pervasives.compare
+	   end)
+
+let constants_to_unfold = 
+  List.fold_right SectionPathSet.add 
+    [ path_of_string "#Ring_normalize#interp_cs.cci";
+      path_of_string "#Ring_normalize#interp_var.cci";
+      path_of_string "#Ring_normalize#interp_vl.cci";
+      path_of_string "#Ring_abstract#interp_acs.cci";
+      path_of_string "#Ring_abstract#interp_sacs.cci";
+      path_of_string "#Quote#varmap_find.cci" ]
+    SectionPathSet.empty 
+
+(* Unfolds the functions interp and find_btree in the term c of goal gl *)
+let polynom_unfold_tac =
+  let flags = 
+    (UNIFORM,
+     { r_beta = true;
+       r_delta = (function
+                    | Const sp -> SectionPathSet.mem sp constants_to_unfold
+                    | Abst sp -> SectionPathSet.mem sp constants_to_unfold
+                    | _ -> false);
+       r_iota = true })
+  in
+  reduct_in_concl (cbv_norm_flags flags)
+      
+(* lc : constr list *)
+(* th : theory associated to t *)
+(* op : clause (None for conclusion or Some id for hypothesis id) *)
+(* gl : goal  *)
+(* Does the rewriting c_i -> (interp R RC v (polynomial_simplify p_i)) 
+   where the ring R, the Ring theory RC, the varmap v and the polynomials p_i
+   are guessed and such that c_i = (interp R RC v p_i) *)
+let raw_polynom th op lc gl =
+  (* first we sort the terms : if t' is a subterm of t it must appear
+     after t in the list. This is to avoid that the normalization of t'
+     modifies t in a non-desired way *)
+  let lc = sort_subterm gl lc in
+  let ltriplets = 
+    if th.th_abstract then 
+      if th.th_ring
+      then build_apolynom gl th lc
+      else build_aspolynom gl th lc
+    else
+      if th.th_ring 
+      then build_polynom gl th lc
+      else build_spolynom gl th lc in 
+  let polynom_tac = 
+    List.fold_right2 
+      (fun ci (c'i, c''i, c'i_eq_c''i) tac ->
+	 tclTHENS 
+	   (elim_type (mkAppL [| Lazy.force coq_eqT; th.th_a; c'i; ci |]))
+	   [ tclTHENS 
+	       (elim_type 
+		  (mkAppL [| Lazy.force coq_eqT; th.th_a; c''i; c'i |]))
+	       [ tac;
+		 h_exact c'i_eq_c''i ];
+	     h_reflexivity])
+      lc ltriplets polynom_unfold_tac 
+  in
+  polynom_tac gl
+
+let guess_eq_tac th = 
+  (tclORELSE reflexivity
+     (tclTHEN 
+	polynom_unfold_tac
+	(tclREPEAT 
+	   (tclORELSE 
+	      (apply (mkAppL [| Lazy.force coq_f_equal2;
+				th.th_a; th.th_a; th.th_a;
+				th.th_plus |])) 
+	      (apply (mkAppL [| Lazy.force coq_f_equal2;
+				th.th_a; th.th_a; th.th_a; 
+				th.th_mult |]))))))
+
+let polynom lcom gl =
+  let lc = (List.map (pf_interp_constr gl) lcom) in
+  match lc with 
+   (* If no argument is given, try to recognize either an equality or
+      a declared relation with arguments c1 ... cn, 
+      do "Ring c1 c2 ... cn" and then try to apply the simplification
+      theorems declared for the relation *)
+    | [] ->
+	(match Hipattern.match_with_equation (pf_concl gl) with
+	   | Some (eq,t::args) ->
+	       let th = guess_theory t in
+	       if List.exists 
+		 (fun c1 -> not (pf_conv_x gl t (pf_type_of gl c1))) args
+	       then 
+		 errorlabstrm "Ring :"
+		   [< 'sTR" All terms must have the same type" >];
+	       (tclTHEN (raw_polynom th None args) (guess_eq_tac th)) gl
+	   | _ -> 
+	       errorlabstrm "polynom :" 
+		 [< 'sTR" This goal is not an equality" >])
+    (* Elsewhere, guess the theory, check that all terms have the same type
+       and apply raw_polynom *)
+    | c :: lc' -> 
+	let t = pf_type_of gl c in 
+	let th = guess_theory t in 
+	if List.exists 
+	  (fun c1 -> not (pf_conv_x gl t (pf_type_of gl c1))) lc'
+	then 
+	  errorlabstrm "Ring :"
+	    [< 'sTR" All terms must have the same type" >];
+	(tclTHEN (raw_polynom th None lc) polynom_unfold_tac) gl
+
+let dyn_polynom ltacargs =  
+  polynom (List.map 
+	     (function 
+		| Command c -> c 
+		| _ -> anomaly "dyn_polynom")
+	     ltacargs) 
+
+let v_polynom = add_tactic "Ring" dyn_polynom
+