path: root/plugins/ring/ring.ml

(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(* $Id$ *)

(* ML part of the Ring tactic *)

open Pp
open Util
open Flags
open Term
open Names
open Libnames
open Nameops
open Reductionops
open Tacticals
open Tacexpr
open Tacmach
open Proof_trees
open Printer
open Equality
open Vernacinterp
open Vernacexpr
open Libobject
open Closure
open Tacred
open Tactics
open Pattern
open Hiddentac
open Nametab
open Quote
open Mod_subst

let mt_evd = Evd.empty
let constr_of c = Constrintern.interp_constr mt_evd (Global.env()) c

let ring_dir = ["Coq";"ring"]
let setoids_dir = ["Coq";"Setoids"]

let ring_constant = Coqlib.gen_constant_in_modules "Ring"
  [ring_dir@["LegacyRing_theory"];
   ring_dir@["Setoid_ring_theory"];
   ring_dir@["Ring_normalize"];
   ring_dir@["Ring_abstract"];
   setoids_dir@["Setoid"];
   ring_dir@["Setoid_ring_normalize"]]

(* Ring theory *)
let coq_Ring_Theory = lazy (ring_constant "Ring_Theory")
let coq_Semi_Ring_Theory = lazy (ring_constant "Semi_Ring_Theory")

(* Setoid ring theory *)
let coq_Setoid_Ring_Theory = lazy (ring_constant "Setoid_Ring_Theory")
let coq_Semi_Setoid_Ring_Theory = lazy(ring_constant "Semi_Setoid_Ring_Theory")

(* Ring normalize *)
let coq_SPplus = lazy (ring_constant "SPplus")
let coq_SPmult = lazy (ring_constant "SPmult")
let coq_SPvar = lazy (ring_constant "SPvar")
let coq_SPconst = lazy (ring_constant "SPconst")
let coq_Pplus = lazy (ring_constant "Pplus")
let coq_Pmult = lazy (ring_constant "Pmult")
let coq_Pvar = lazy (ring_constant "Pvar")
let coq_Pconst = lazy (ring_constant "Pconst")
let coq_Popp = lazy (ring_constant "Popp")
let coq_interp_sp = lazy (ring_constant "interp_sp")
let coq_interp_p = lazy (ring_constant "interp_p")
let coq_interp_cs = lazy (ring_constant "interp_cs")
let coq_spolynomial_simplify = lazy (ring_constant "spolynomial_simplify")
let coq_polynomial_simplify = lazy (ring_constant "polynomial_simplify")
let coq_spolynomial_simplify_ok = lazy(ring_constant "spolynomial_simplify_ok")
let coq_polynomial_simplify_ok = lazy (ring_constant "polynomial_simplify_ok")

(* Setoid theory *)
let coq_Setoid_Theory = lazy(ring_constant "Setoid_Theory")

let coq_seq_refl = lazy(ring_constant "Seq_refl")
let coq_seq_sym = lazy(ring_constant "Seq_sym")
let coq_seq_trans = lazy(ring_constant "Seq_trans")

(* Setoid Ring normalize *)
let coq_SetSPplus = lazy (ring_constant "SetSPplus")
let coq_SetSPmult = lazy (ring_constant "SetSPmult")
let coq_SetSPvar = lazy (ring_constant "SetSPvar")
let coq_SetSPconst = lazy (ring_constant "SetSPconst")
let coq_SetPplus = lazy (ring_constant "SetPplus")
let coq_SetPmult = lazy (ring_constant "SetPmult")
let coq_SetPvar = lazy (ring_constant "SetPvar")
let coq_SetPconst = lazy (ring_constant "SetPconst")
let coq_SetPopp = lazy (ring_constant "SetPopp")
let coq_interp_setsp = lazy (ring_constant "interp_setsp")
let coq_interp_setp = lazy (ring_constant "interp_setp")
let coq_interp_setcs = lazy (ring_constant "interp_setcs")
let coq_setspolynomial_simplify =
  lazy (ring_constant "setspolynomial_simplify")
let coq_setpolynomial_simplify =
  lazy (ring_constant "setpolynomial_simplify")
let coq_setspolynomial_simplify_ok =
  lazy (ring_constant "setspolynomial_simplify_ok")
let coq_setpolynomial_simplify_ok =
  lazy (ring_constant "setpolynomial_simplify_ok")

(* Ring abstract *)
let coq_ASPplus = lazy (ring_constant "ASPplus")
let coq_ASPmult = lazy (ring_constant "ASPmult")
let coq_ASPvar = lazy (ring_constant "ASPvar")
let coq_ASP0 = lazy (ring_constant "ASP0")
let coq_ASP1 = lazy (ring_constant "ASP1")
let coq_APplus = lazy (ring_constant "APplus")
let coq_APmult = lazy (ring_constant "APmult")
let coq_APvar = lazy (ring_constant "APvar")
let coq_AP0 = lazy (ring_constant "AP0")
let coq_AP1 = lazy (ring_constant "AP1")
let coq_APopp = lazy (ring_constant "APopp")
let coq_interp_asp = lazy (ring_constant "interp_asp")
let coq_interp_ap = lazy (ring_constant "interp_ap")
let coq_interp_acs = lazy (ring_constant "interp_acs")
let coq_interp_sacs = lazy (ring_constant "interp_sacs")
let coq_aspolynomial_normalize = lazy (ring_constant "aspolynomial_normalize")
let coq_apolynomial_normalize = lazy (ring_constant "apolynomial_normalize")
let coq_aspolynomial_normalize_ok =
  lazy (ring_constant "aspolynomial_normalize_ok")
let coq_apolynomial_normalize_ok =
  lazy (ring_constant "apolynomial_normalize_ok")

(* Logic --> to be found in Coqlib *)
open Coqlib

let mkLApp(fc,v) = mkApp(Lazy.force fc, v)

(*********** Useful types and functions ************)

module OperSet =
  Set.Make (struct
	      type t = global_reference
	      let compare = (Pervasives.compare : t->t->int)
	    end)

type morph =
    { plusm : constr;
      multm : constr;
      oppm : constr option;
    }

type theory =
    { th_ring : bool;                  (* false for a semi-ring *)
      th_abstract : bool;
      th_setoid : bool;                (* true for a setoid ring *)
      th_equiv : constr option;
      th_setoid_th : constr option;
      th_morph : morph option;
      th_a : constr;                   (* e.g. nat *)
      th_plus : constr;
      th_mult : constr;
      th_one : constr;
      th_zero : constr;
      th_opp : constr option;          (* None 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 subst_morph subst morph =
  let plusm' = subst_mps subst morph.plusm in
  let multm' = subst_mps subst morph.multm in
  let oppm' = Option.smartmap (subst_mps subst) morph.oppm in
    if plusm' == morph.plusm
      && multm' == morph.multm
      && oppm' == morph.oppm then
	morph
    else
      { plusm = plusm' ;
	multm = multm' ;
	oppm = oppm' ;
      }

let subst_set subst cset =
  let same = ref true in
  let copy_subst c newset =
    let c' = subst_mps subst c in
      if not (c' == c) then same := false;
      ConstrSet.add c' newset
  in
  let cset' = ConstrSet.fold copy_subst cset ConstrSet.empty in
    if !same then cset else cset'

let subst_theory subst th =
  let th_equiv' = Option.smartmap (subst_mps subst) th.th_equiv in
  let th_setoid_th' = Option.smartmap (subst_mps subst) th.th_setoid_th in
  let th_morph' = Option.smartmap (subst_morph subst) th.th_morph in
  let th_a' = subst_mps subst th.th_a in
  let th_plus' = subst_mps subst th.th_plus in
  let th_mult' = subst_mps subst th.th_mult in
  let th_one' = subst_mps subst th.th_one in
  let th_zero' = subst_mps subst th.th_zero in
  let th_opp' = Option.smartmap (subst_mps subst) th.th_opp in
  let th_eq' = subst_mps subst th.th_eq in
  let th_t' = subst_mps subst th.th_t in
  let th_closed' = subst_set subst th.th_closed in
    if th_equiv' == th.th_equiv
      && th_setoid_th' == th.th_setoid_th
      && th_morph' == th.th_morph
      && th_a' == th.th_a
      && th_plus' == th.th_plus
      && th_mult' == th.th_mult
      && th_one' == th.th_one
      && th_zero' == th.th_zero
      && th_opp' == th.th_opp
      && th_eq' == th.th_eq
      && th_t' == th.th_t
      && th_closed' == th.th_closed
    then
      th
    else
    { th_ring = th.th_ring ;
      th_abstract = th.th_abstract ;
      th_setoid = th.th_setoid ;
      th_equiv = th_equiv' ;
      th_setoid_th = th_setoid_th' ;
      th_morph = th_morph' ;
      th_a = th_a' ;
      th_plus = th_plus' ;
      th_mult = th_mult' ;
      th_one = th_one' ;
      th_zero = th_zero' ;
      th_opp = th_opp' ;
      th_eq = th_eq' ;
      th_t = th_t' ;
      th_closed = th_closed' ;
    }


let subst_th (subst,(c,th as obj)) =
  let c' = subst_mps subst c in
  let th' = subst_theory subst th in
    if c' == c && th' == th then obj else
      (c',th')


let (theory_to_obj, obj_to_theory) =
  let cache_th (_,(c, th)) = theories_map_add (c,th) in
  declare_object {(default_object "tactic-ring-theory") with
		    open_function = (fun i o -> if i=1 then cache_th o);
                    cache_function = cache_th;
		    subst_function = subst_th;
		    classify_function = (fun x -> Substitute x) }

(* 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 " ++
	 pr_lconstr a ++ fnl () ++
	 str "Use Add [Semi] Ring to declare it")

(* Looks up an option *)

let unbox = function
  | Some w -> w
  | None -> anomaly "Ring : Not in case of a setoid ring."

(* Protects the convertibility test against undue exceptions when using it
   with untyped terms *)

let safe_pf_conv_x gl c1 c2 = try pf_conv_x gl c1 c2 with _ -> false


(* Add a Ring or a Semi-Ring to the database after a type verification *)

let implement_theory env t th args =
  is_conv env Evd.empty (Typing.type_of env Evd.empty t) (mkLApp (th, args))

(* (\* The following test checks whether the provided morphism is the default *)
(*    one for the given operation. In principle the test is too strict, since *)
(*    it should possible to provide another proof for the same fact (proof *)
(*    irrelevance). In particular, the error message is be not very explicative. *\) *)
let states_compatibility_for env plus mult opp morphs =
 let check op compat = true in
(*   is_conv env Evd.empty (Setoid_replace.default_morphism op).Setoid_replace.lem *)
(*    compat in *)
 check plus morphs.plusm &&
 check mult morphs.multm &&
 (match (opp,morphs.oppm) with
     None, None -> true
   | Some opp, Some compat -> check opp compat
   | _,_ -> assert false)

let add_theory want_ring want_abstract want_setoid a aequiv asetth amorph aplus amult aone azero aopp aeq t cset =
  if theories_map_mem a then errorlabstrm "Add Semi Ring"
    (str "A (Semi-)(Setoid-)Ring Structure is already declared for " ++
       pr_lconstr a);
  let env = Global.env () in
    if (want_ring & want_setoid & (
	not (implement_theory env t coq_Setoid_Ring_Theory
	  [| a; (unbox aequiv); aplus; amult; aone; azero; (unbox aopp); aeq|])
        ||
	not (implement_theory env (unbox asetth) coq_Setoid_Theory
	  [| a; (unbox aequiv) |]) ||
        not (states_compatibility_for env aplus amult aopp (unbox amorph))
        )) then
      errorlabstrm "addring" (str "Not a valid Setoid-Ring theory");
    if (not want_ring & want_setoid & (
        not (implement_theory env t coq_Semi_Setoid_Ring_Theory
	  [| a; (unbox aequiv); aplus; amult; aone; azero; aeq|]) ||
	not (implement_theory env (unbox asetth) coq_Setoid_Theory
	  [| a; (unbox aequiv) |]) ||
        not (states_compatibility_for env aplus amult aopp (unbox amorph))))
    then
      errorlabstrm "addring" (str "Not a valid Semi-Setoid-Ring theory");
    if (want_ring & not want_setoid &
	not (implement_theory env t coq_Ring_Theory
	  [| a; aplus; amult; aone; azero; (unbox aopp); aeq |])) then
      errorlabstrm "addring" (str "Not a valid Ring theory");
    if (not want_ring & not want_setoid &
	not (implement_theory env t 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_setoid = want_setoid;
	       th_equiv = aequiv;
	       th_setoid_th = asetth;
	       th_morph = amorph;
	       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 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 (strip_outer_cast c)) with
      | App (binop,[|c1; c2|]) when safe_pf_conv_x gl binop th.th_plus ->
	  mkLApp(coq_SPplus, [|th.th_a; aux c1; aux c2 |])
      | App (binop,[|c1; c2|]) when safe_pf_conv_x gl binop th.th_mult ->
	  mkLApp(coq_SPmult, [|th.th_a; aux c1; aux c2 |])
      | _ when closed_under th.th_closed c ->
	  mkLApp(coq_SPconst, [|th.th_a; c |])
      | _ ->
	  try Hashtbl.find varhash c
	  with Not_found ->
	    let newvar =
              mkLApp(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 ->
       (mkLApp (coq_interp_sp,
               [|th.th_a; th.th_plus; th.th_mult; th.th_zero; v; p |]),
	mkLApp (coq_interp_cs,
               [|th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; v;
		  pf_reduce cbv_betadeltaiota gl
		    (mkLApp (coq_spolynomial_simplify,
			    [| th.th_a; th.th_plus; th.th_mult;
			       th.th_one; th.th_zero;
			       th.th_eq; p|])) |]),
	mkLApp (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 (strip_outer_cast c)) with
      | App (binop, [|c1; c2|]) when safe_pf_conv_x gl binop th.th_plus ->
	  mkLApp(coq_Pplus, [|th.th_a; aux c1; aux c2 |])
      | App (binop, [|c1; c2|]) when safe_pf_conv_x gl binop th.th_mult ->
	  mkLApp(coq_Pmult, [|th.th_a; aux c1; aux c2 |])
      (* The special case of Zminus *)
      | App (binop, [|c1; c2|])
	  when safe_pf_conv_x gl c
            (mkApp (th.th_plus, [|c1; mkApp(unbox th.th_opp, [|c2|])|])) ->
	    mkLApp(coq_Pplus,
                  [|th.th_a; aux c1;
	            mkLApp(coq_Popp, [|th.th_a; aux c2|]) |])
      | App (unop, [|c1|]) when safe_pf_conv_x gl unop (unbox th.th_opp) ->
	  mkLApp(coq_Popp, [|th.th_a; aux c1|])
      | _ when closed_under th.th_closed c ->
	  mkLApp(coq_Pconst, [|th.th_a; c |])
      | _ ->
	  try Hashtbl.find varhash c
	  with Not_found ->
	    let newvar =
              mkLApp(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 ->
       (mkLApp(coq_interp_p,
	       [| th.th_a; th.th_plus; th.th_mult; th.th_zero;
                 (unbox th.th_opp); v; p |])),
	mkLApp(coq_interp_cs,
	       [| th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; v;
		  pf_reduce cbv_betadeltaiota gl
		    (mkLApp(coq_polynomial_simplify,
			    [| th.th_a; th.th_plus; th.th_mult;
			       th.th_one; th.th_zero;
			       (unbox th.th_opp); th.th_eq; p |])) |]),
	mkLApp(coq_polynomial_simplify_ok,
	       [| th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero;
		  (unbox 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 (strip_outer_cast c)) with
      | App (binop, [|c1; c2|]) when safe_pf_conv_x gl binop th.th_plus ->
	  mkLApp(coq_ASPplus, [| aux c1; aux c2 |])
      | App (binop, [|c1; c2|]) when safe_pf_conv_x gl binop th.th_mult ->
	  mkLApp(coq_ASPmult, [| aux c1; aux c2 |])
      | _ when safe_pf_conv_x gl c th.th_zero -> Lazy.force coq_ASP0
      | _ when safe_pf_conv_x gl c th.th_one -> Lazy.force coq_ASP1
      | _ ->
	  try Hashtbl.find varhash c
	  with Not_found ->
	    let newvar = mkLApp(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 ->
       (mkLApp(coq_interp_asp,
               [| th.th_a; th.th_plus; th.th_mult;
		  th.th_one; th.th_zero; v; p |]),
	mkLApp(coq_interp_acs,
               [| th.th_a; th.th_plus; th.th_mult;
		  th.th_one; th.th_zero; v;
		  pf_reduce cbv_betadeltaiota gl
		    (mkLApp(coq_aspolynomial_normalize,[|p|])) |]),
	mkLApp(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 (strip_outer_cast c)) with
      | App (binop, [|c1; c2|]) when safe_pf_conv_x gl binop th.th_plus ->
	  mkLApp(coq_APplus, [| aux c1; aux c2 |])
      | App (binop, [|c1; c2|]) when safe_pf_conv_x gl binop th.th_mult ->
	  mkLApp(coq_APmult, [| aux c1; aux c2 |])
      (* The special case of Zminus *)
      | App (binop, [|c1; c2|])
	  when safe_pf_conv_x gl c
            (mkApp(th.th_plus, [|c1; mkApp(unbox th.th_opp,[|c2|]) |])) ->
	    mkLApp(coq_APplus,
                   [|aux c1; mkLApp(coq_APopp,[|aux c2|]) |])
      | App (unop, [|c1|]) when safe_pf_conv_x gl unop (unbox th.th_opp) ->
	  mkLApp(coq_APopp, [| aux c1 |])
      | _ when safe_pf_conv_x gl c th.th_zero -> Lazy.force coq_AP0
      | _ when safe_pf_conv_x gl c th.th_one -> Lazy.force coq_AP1
      | _ ->
	  try Hashtbl.find varhash c
	  with Not_found ->
	    let newvar =
              mkLApp(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 ->
       (mkLApp(coq_interp_ap,
	       [| th.th_a; th.th_plus; th.th_mult; th.th_one;
		  th.th_zero; (unbox th.th_opp); v; p |]),
	mkLApp(coq_interp_sacs,
	       [| th.th_a; th.th_plus; th.th_mult;
		  th.th_one; th.th_zero; (unbox th.th_opp); v;
		  pf_reduce cbv_betadeltaiota gl
		    (mkLApp(coq_apolynomial_normalize, [|p|])) |]),
	mkLApp(coq_apolynomial_normalize_ok,
	       [| th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero;
		  (unbox th.th_opp); th.th_eq; v; th.th_t; p |])))
    lp

(*
   gl : goal sigma
   th : setoid 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_setpolynom 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 (strip_outer_cast c)) with
      | App (binop, [|c1; c2|]) when safe_pf_conv_x gl binop th.th_plus ->
	  mkLApp(coq_SetPplus, [|th.th_a; aux c1; aux c2 |])
      | App (binop, [|c1; c2|]) when safe_pf_conv_x gl binop th.th_mult ->
	  mkLApp(coq_SetPmult, [|th.th_a; aux c1; aux c2 |])
      (* The special case of Zminus *)
      | App (binop, [|c1; c2|])
	  when safe_pf_conv_x gl c
	    (mkApp(th.th_plus, [|c1; mkApp(unbox th.th_opp,[|c2|])|])) ->
	      mkLApp(coq_SetPplus,
                     [| th.th_a; aux c1;
			mkLApp(coq_SetPopp, [|th.th_a; aux c2|]) |])
      | App (unop, [|c1|]) when safe_pf_conv_x gl unop (unbox th.th_opp) ->
	  mkLApp(coq_SetPopp, [| th.th_a; aux c1 |])
      | _ when closed_under th.th_closed c ->
	  mkLApp(coq_SetPconst, [| th.th_a; c |])
      | _ ->
	  try Hashtbl.find varhash c
	  with Not_found ->
	    let newvar =
              mkLApp(coq_SetPvar, [| 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 ->
       (mkLApp(coq_interp_setp,
	       [| th.th_a; th.th_plus; th.th_mult; th.th_zero;
                  (unbox th.th_opp); v; p |]),
	mkLApp(coq_interp_setcs,
	       [| th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; v;
		  pf_reduce cbv_betadeltaiota gl
		    (mkLApp(coq_setpolynomial_simplify,
			    [| th.th_a; th.th_plus; th.th_mult;
			       th.th_one; th.th_zero;
			       (unbox th.th_opp); th.th_eq; p |])) |]),
	mkLApp(coq_setpolynomial_simplify_ok,
	       [| th.th_a; (unbox th.th_equiv); th.th_plus;
                  th.th_mult; th.th_one; th.th_zero;(unbox th.th_opp);
                  th.th_eq; (unbox th.th_setoid_th);
		  (unbox th.th_morph).plusm; (unbox th.th_morph).multm;
		  (unbox (unbox th.th_morph).oppm); v; th.th_t; p |])))
    lp

(*
   gl : goal sigma
   th : semi setoid 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_setspolynom 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 (strip_outer_cast c)) with
      | App (binop, [|c1; c2|]) when safe_pf_conv_x gl binop th.th_plus ->
	  mkLApp(coq_SetSPplus, [|th.th_a; aux c1; aux c2 |])
      | App (binop, [|c1; c2|]) when safe_pf_conv_x gl binop th.th_mult ->
	  mkLApp(coq_SetSPmult, [| th.th_a; aux c1; aux c2 |])
      | _ when closed_under th.th_closed c ->
	  mkLApp(coq_SetSPconst, [| th.th_a; c |])
      | _ ->
	  try Hashtbl.find varhash c
	  with Not_found ->
	    let newvar =
              mkLApp(coq_SetSPvar, [|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 ->
       (mkLApp(coq_interp_setsp,
	       [| th.th_a; th.th_plus; th.th_mult; th.th_zero; v; p |]),
	mkLApp(coq_interp_setcs,
               [| th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; v;
		  pf_reduce cbv_betadeltaiota gl
		    (mkLApp(coq_setspolynomial_simplify,
			    [| th.th_a; th.th_plus; th.th_mult;
			       th.th_one; th.th_zero;
			       th.th_eq; p |])) |]),
	mkLApp(coq_setspolynomial_simplify_ok,
	       [| th.th_a; (unbox th.th_equiv); th.th_plus;
                  th.th_mult; th.th_one; th.th_zero; th.th_eq;
                  (unbox th.th_setoid_th);
		  (unbox th.th_morph).plusm;
                  (unbox th.th_morph).multm; v; th.th_t; p |])))
    lp

module SectionPathSet =
  Set.Make(struct
	     type t = full_path
	     let compare = Pervasives.compare
	   end)

(* Avec l'uniformisation des red_kind, on perd ici sur la structure
   SectionPathSet; peut-être faudra-t-il la déplacer dans Closure *)
let constants_to_unfold =
(*  List.fold_right SectionPathSet.add *)
  let transform s =
    let sp = path_of_string s in
    let dir, id = repr_path sp in
      Libnames.encode_con dir id
  in
  List.map transform
    [ "Coq.ring.Ring_normalize.interp_cs";
      "Coq.ring.Ring_normalize.interp_var";
      "Coq.ring.Ring_normalize.interp_vl";
      "Coq.ring.Ring_abstract.interp_acs";
      "Coq.ring.Ring_abstract.interp_sacs";
      "Coq.quote.Quote.varmap_find";
      (* anciennement des Local devenus Definition *)
      "Coq.ring.Ring_normalize.ics_aux";
      "Coq.ring.Ring_normalize.ivl_aux";
      "Coq.ring.Ring_normalize.interp_m";
      "Coq.ring.Ring_abstract.iacs_aux";
      "Coq.ring.Ring_abstract.isacs_aux";
      "Coq.ring.Setoid_ring_normalize.interp_cs";
      "Coq.ring.Setoid_ring_normalize.interp_var";
      "Coq.ring.Setoid_ring_normalize.interp_vl";
      "Coq.ring.Setoid_ring_normalize.ics_aux";
      "Coq.ring.Setoid_ring_normalize.ivl_aux";
      "Coq.ring.Setoid_ring_normalize.interp_m";
    ]
(*    SectionPathSet.empty *)

(* Unfolds the functions interp and find_btree in the term c of goal gl *)
open RedFlags
let polynom_unfold_tac =
  let flags =
    (mkflags(fBETA::fIOTA::(List.map fCONST constants_to_unfold))) in
  reduct_in_concl (cbv_norm_flags flags,DEFAULTcast)

let polynom_unfold_tac_in_term gl =
  let flags =
    (mkflags(fBETA::fIOTA::fZETA::(List.map fCONST constants_to_unfold)))
  in
  cbv_norm_flags flags (pf_env gl) (project gl)

(* 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_setoid then
      if th.th_ring
      then build_setpolynom gl th lc
      else build_setspolynom gl th lc
    else
      if th.th_ring then
	if th.th_abstract
	then build_apolynom gl th lc
	else build_polynom gl th lc
      else
	if th.th_abstract
	then build_aspolynom 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 ->
         let c'''i =
	   if !term_quality then polynom_unfold_tac_in_term gl c''i else c''i
	 in
         if !term_quality && safe_pf_conv_x gl c'''i ci then
	   tac (* convertible terms *)
         else if th.th_setoid
	 then
           (tclORELSE
              (tclORELSE
		 (h_exact c'i_eq_c''i)
		 (h_exact (mkLApp(coq_seq_sym,
				  [| th.th_a; (unbox th.th_equiv);
                                     (unbox th.th_setoid_th);
				     c'''i; ci; c'i_eq_c''i |]))))
	      (tclTHENS
		 (tclORELSE
                   (Equality.general_rewrite true
		     Termops.all_occurrences false c'i_eq_c''i)
                   (Equality.general_rewrite false
		     Termops.all_occurrences false c'i_eq_c''i))
                 [tac]))
	 else
           (tclORELSE
              (tclORELSE
		 (h_exact c'i_eq_c''i)
		 (h_exact (mkApp(build_coq_eq_sym (),
				 [|th.th_a; c'''i; ci; c'i_eq_c''i |]))))
	      (tclTHENS
		 (elim_type
		    (mkApp(build_coq_eq (), [|th.th_a; c'''i; ci |])))
		 [ tac;
                   h_exact c'i_eq_c''i ]))
)
      lc ltriplets polynom_unfold_tac
  in
  polynom_tac gl

let guess_eq_tac th =
  (tclORELSE reflexivity
     (tclTHEN
	polynom_unfold_tac
        (tclTHEN
	   (* Normalized sums associate on the right *)
	   (tclREPEAT
	      (tclTHENFIRST
		 (apply (mkApp(build_coq_f_equal2 (),
		               [| th.th_a; th.th_a; th.th_a;
				  th.th_plus |])))
		 reflexivity))
	   (tclTRY
	      (tclTHENLAST
		 (apply (mkApp(build_coq_f_equal2 (),
			       [| th.th_a; th.th_a; th.th_a;
				  th.th_plus |])))
		 reflexivity)))))

let guess_equiv_tac th =
  (tclORELSE (apply (mkLApp(coq_seq_refl,
			    [| th.th_a; (unbox th.th_equiv);
			       (unbox th.th_setoid_th)|])))
     (tclTHEN
	polynom_unfold_tac
	(tclREPEAT
	   (tclORELSE
	      (apply (unbox th.th_morph).plusm)
	      (apply (unbox th.th_morph).multm)))))

let match_with_equiv c = match (kind_of_term c) with
  | App (e,a) ->
      if (List.mem e []) (*  (Setoid_replace.equiv_list ())) *)
      then Some (decompose_app c)
      else None
  | _ -> None

let polynom lc gl =
  Coqlib.check_required_library ["Coq";"ring";"LegacyRing"];
  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 *)
    | [] ->
	(try
	  match Hipattern.match_with_equation (pf_concl gl) with
	   | _,_,Hipattern.PolymorphicLeibnizEq (t,c1,c2) ->
	       let th = guess_theory t in
	       (tclTHEN (raw_polynom th None [c1;c2]) (guess_eq_tac th)) gl
	   | _,_,Hipattern.HeterogenousEq (t1,c1,t2,c2)
	       when safe_pf_conv_x gl t1 t2 ->
	       let th = guess_theory t1 in
	       (tclTHEN (raw_polynom th None [c1;c2]) (guess_eq_tac th)) gl
	   | _ -> raise Exit
	  with Hipattern.NoEquationFound | Exit ->
	          (match match_with_equiv (pf_concl gl) with
		     | Some (equiv, c1::args) ->
			 let t = (pf_type_of gl c1) in
			 let th = (guess_theory t) in
			   if List.exists
			     (fun c2 -> not (safe_pf_conv_x gl t (pf_type_of gl c2))) args
			   then
			     errorlabstrm "Ring :"
			       (str" All terms must have the same type");
			   (tclTHEN (raw_polynom th None (c1::args)) (guess_equiv_tac th)) gl
		     | _ -> errorlabstrm "polynom :"
			 (str" This goal is not an equality nor a setoid equivalence")))
    (* 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 (safe_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