(************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) (* $Id: ring.ml 11094 2008-06-10 19:35:23Z herbelin $ *) (* 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); Summary.survive_module = false; Summary.survive_section = false } (* 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) and export_th x = Some x 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); export_function = export_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 " ++ 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 = 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 = section_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.ring.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 (Setoid_replace.general_s_rewrite true Termops.all_occurrences c'i_eq_c''i ~new_goals:[]) (Setoid_replace.general_s_rewrite false Termops.all_occurrences c'i_eq_c''i ~new_goals:[])) [tac])) else (tclORELSE (tclORELSE (h_exact c'i_eq_c''i) (h_exact (mkApp(build_coq_sym_eq (), [|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 *) | [] -> (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 (safe_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 | _ -> (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