aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/extraction/extraction.ml16
-rw-r--r--plugins/extraction/mlutil.ml3
-rw-r--r--plugins/funind/gen_principle.ml7
-rw-r--r--plugins/ltac/rewrite.ml8
-rw-r--r--plugins/ltac/taccoerce.ml7
-rw-r--r--plugins/ltac/taccoerce.mli2
-rw-r--r--plugins/micromega/certificate.ml8
-rw-r--r--plugins/micromega/g_zify.mlg22
-rw-r--r--plugins/micromega/zify.ml251
-rw-r--r--plugins/micromega/zify.mli3
-rw-r--r--plugins/omega/coq_omega.ml1939
-rw-r--r--plugins/omega/coq_omega.mli11
-rw-r--r--plugins/omega/dune7
-rw-r--r--plugins/omega/g_omega.mlg29
-rw-r--r--plugins/omega/omega.ml708
-rw-r--r--plugins/omega/omega_plugin.mlpack3
-rw-r--r--plugins/ssr/ssrparser.mlg126
-rw-r--r--plugins/ssrmatching/ssrmatching.ml20
18 files changed, 296 insertions, 2874 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 0cad192332..30f90dd1fc 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -22,7 +22,6 @@ open Reductionops
open Inductive
open Termops
open Inductiveops
-open Recordops
open Namegen
open Miniml
open Table
@@ -428,6 +427,7 @@ and extract_really_ind env kn mib =
(* Everything concerning parameters. *)
(* We do that first, since they are common to all the [mib]. *)
let mip0 = mib.mind_packets.(0) in
+ let ndecls = List.length mib.mind_params_ctxt in
let npar = mib.mind_nparams in
let epar = push_rel_context mib.mind_params_ctxt env in
let sg = Evd.from_env env in
@@ -463,17 +463,17 @@ and extract_really_ind env kn mib =
if not p.ip_logical then
let types = arities_of_constructors env ((kn,i),u) in
for j = 0 to Array.length types - 1 do
- let t = snd (decompose_prod_n npar types.(j)) in
+ let t = snd (decompose_prod_n_assum ndecls types.(j)) in
let prods,head = dest_prod epar t in
let nprods = List.length prods in
let args = match Constr.kind head with
| App (f,args) -> args (* [Constr.kind f = Ind ip] *)
| _ -> [||]
in
- let dbmap = parse_ind_args p.ip_sign args (nprods + npar) in
- let db = db_from_ind dbmap npar in
+ let dbmap = parse_ind_args p.ip_sign args (nprods + ndecls) in
+ let db = db_from_ind dbmap ndecls in
p.ip_types.(j) <-
- extract_type_cons epar sg db dbmap (EConstr.of_constr t) (npar+1)
+ extract_type_cons epar sg db dbmap (EConstr.of_constr t) (ndecls+1)
done
done;
(* Third pass: we determine special cases. *)
@@ -531,7 +531,7 @@ and extract_really_ind env kn mib =
let n = nb_default_params env sg (EConstr.of_constr ty) in
let check_proj kn = if Cset.mem kn !projs then add_projection n kn ip
in
- List.iter (Option.iter check_proj) (lookup_projections ip)
+ List.iter (Option.iter check_proj) (Structures.Structure.find_projections ip)
with Not_found -> ()
end;
Record field_glob
@@ -1129,7 +1129,7 @@ let extract_constant env kn cb =
(match cb.const_body with
| Primitive _ | Undef _ -> warn_info (); mk_typ_ax ()
| Def c ->
- (match Recordops.find_primitive_projection kn with
+ (match Structures.PrimitiveProjections.find_opt kn with
| None -> mk_typ (get_body c)
| Some p ->
let body = fake_match_projection env p in
@@ -1142,7 +1142,7 @@ let extract_constant env kn cb =
(match cb.const_body with
| Primitive _ | Undef _ -> warn_info (); mk_ax ()
| Def c ->
- (match Recordops.find_primitive_projection kn with
+ (match Structures.PrimitiveProjections.find_opt kn with
| None -> mk_def (get_body c)
| Some p ->
let body = fake_match_projection env p in
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index cfdaac710b..268d4bf9e9 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -1525,8 +1525,7 @@ let inline_test r t =
else
let c = match r with GlobRef.ConstRef c -> c | _ -> assert false in
let has_body =
- try constant_has_body (Global.lookup_constant c)
- with Not_found -> false
+ Environ.mem_constant c (Global.env()) && constant_has_body (Global.lookup_constant c)
in
has_body &&
(let t1 = eta_red t in
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index cbdebb7bbc..6236a5147d 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -2058,13 +2058,12 @@ let make_graph (f_ref : GlobRef.t) =
let sigma = Evd.from_env env in
let c, c_body =
match f_ref with
- | GlobRef.ConstRef c -> (
- try (c, Global.lookup_constant c)
- with Not_found ->
+ | GlobRef.ConstRef c ->
+ if Environ.mem_constant c (Global.env ()) then (c, Global.lookup_constant c) else
CErrors.user_err
Pp.(
str "Cannot find "
- ++ Printer.pr_leconstr_env env sigma (EConstr.mkConst c)) )
+ ++ Printer.pr_leconstr_env env sigma (EConstr.mkConst c))
| _ -> CErrors.user_err Pp.(str "Not a function reference")
in
match Global.body_of_constant_body Library.indirect_accessor c_body with
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index c7bda43465..1640bff43b 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -373,11 +373,6 @@ end) = struct
end
-(* let my_type_of env evars c = Typing.e_type_of env evars c *)
-(* let mytypeofkey = CProfile.declare_profile "my_type_of";; *)
-(* let my_type_of = CProfile.profile3 mytypeofkey my_type_of *)
-
-
let type_app_poly env env evd f args =
let evars, c = app_poly_nocheck env evd f args in
let evd', t = Typing.type_of env (goalevars evars) c in
@@ -2066,9 +2061,6 @@ let get_hyp gl (c,l) clause l2r =
let general_rewrite_flags = { under_lambdas = false; on_morphisms = true }
-(* let rewriteclaustac_key = CProfile.declare_profile "cl_rewrite_clause_tac";; *)
-(* let cl_rewrite_clause_tac = CProfile.profile5 rewriteclaustac_key cl_rewrite_clause_tac *)
-
(** Setoid rewriting when called with "rewrite" *)
let general_s_rewrite cl l2r occs (c,l) ~new_goals =
Proofview.Goal.enter begin fun gl ->
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index 5e88bf7c79..f2f5fc16a6 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -91,6 +91,13 @@ let to_int v =
Some (out_gen (topwit wit_int) v)
else None
+let of_ident id = in_gen (topwit wit_ident) id
+
+let to_ident v =
+ if has_type v (topwit wit_ident) then
+ Some (out_gen (topwit wit_ident) v)
+ else None
+
let to_list v = prj Val.typ_list v
let to_option v = prj Val.typ_opt v
diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli
index 8ca2510459..c748fb3d1a 100644
--- a/plugins/ltac/taccoerce.mli
+++ b/plugins/ltac/taccoerce.mli
@@ -39,6 +39,8 @@ sig
val to_uconstr : t -> Ltac_pretype.closed_glob_constr option
val of_int : int -> t
val to_int : t -> int option
+ val of_ident : Id.t -> t
+ val to_ident : t -> Id.t option
val to_list : t -> t list option
val to_option : t -> t option option
val to_pair : t -> (t * t) option
diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml
index 53aa619d10..1018271751 100644
--- a/plugins/micromega/certificate.ml
+++ b/plugins/micromega/certificate.ml
@@ -449,6 +449,8 @@ let bound_monomials (sys : WithProof.t list) =
in
List.map snd (List.filter has_mon bounds) @ snd l
+let bound_monomials = tr_sys "bound_monomials" bound_monomials
+
let develop_constraints prfdepth n_spec sys =
LinPoly.MonT.clear ();
max_nb_cstr := compute_max_nb_cstr sys prfdepth;
@@ -1181,10 +1183,12 @@ let nlia enum prfdepth sys =
It would only be safe if the variable is linear...
*)
let sys1 =
- elim_simple_linear_equality (WithProof.subst_constant true sys)
+ normalise
+ (elim_simple_linear_equality (WithProof.subst_constant true sys))
in
+ let bnd1 = bound_monomials sys1 in
let sys2 = saturate_by_linear_equalities sys1 in
- let sys3 = nlinear_preprocess (sys1 @ sys2) in
+ let sys3 = nlinear_preprocess (rev_concat [bnd1; sys1; sys2]) in
let sys4 = make_cstr_system (*sys2@*) sys3 in
(* [reduction_equations] is too brutal - there should be some non-linear reasoning *)
xlia (List.map fst sys) enum reduction_equations sys4
diff --git a/plugins/micromega/g_zify.mlg b/plugins/micromega/g_zify.mlg
index 74b0708743..d18065088c 100644
--- a/plugins/micromega/g_zify.mlg
+++ b/plugins/micromega/g_zify.mlg
@@ -24,17 +24,17 @@ let warn_deprecated_Spec =
DECLARE PLUGIN "zify_plugin"
VERNAC COMMAND EXTEND DECLAREINJECTION CLASSIFIED AS SIDEFF
-| ["Add" "Zify" "InjTyp" constr(t) ] -> { Zify.InjTable.register t }
-| ["Add" "Zify" "BinOp" constr(t) ] -> { Zify.BinOp.register t }
-| ["Add" "Zify" "UnOp" constr(t) ] -> { Zify.UnOp.register t }
-| ["Add" "Zify" "CstOp" constr(t) ] -> { Zify.CstOp.register t }
-| ["Add" "Zify" "BinRel" constr(t) ] -> { Zify.BinRel.register t }
-| ["Add" "Zify" "PropOp" constr(t) ] -> { Zify.PropBinOp.register t }
-| ["Add" "Zify" "PropBinOp" constr(t) ] -> { Zify.PropBinOp.register t }
-| ["Add" "Zify" "PropUOp" constr(t) ] -> { Zify.PropUnOp.register t }
-| ["Add" "Zify" "BinOpSpec" constr(t) ] -> { Zify.BinOpSpec.register t }
-| ["Add" "Zify" "UnOpSpec" constr(t) ] -> { Zify.UnOpSpec.register t }
-| ["Add" "Zify" "Saturate" constr(t) ] -> { Zify.Saturate.register t }
+| ["Add" "Zify" "InjTyp" reference(t) ] -> { Zify.InjTable.register t }
+| ["Add" "Zify" "BinOp" reference(t) ] -> { Zify.BinOp.register t }
+| ["Add" "Zify" "UnOp" reference(t) ] -> { Zify.UnOp.register t }
+| ["Add" "Zify" "CstOp" reference(t) ] -> { Zify.CstOp.register t }
+| ["Add" "Zify" "BinRel" reference(t) ] -> { Zify.BinRel.register t }
+| ["Add" "Zify" "PropOp" reference(t) ] -> { Zify.PropBinOp.register t }
+| ["Add" "Zify" "PropBinOp" reference(t) ] -> { Zify.PropBinOp.register t }
+| ["Add" "Zify" "PropUOp" reference(t) ] -> { Zify.PropUnOp.register t }
+| ["Add" "Zify" "BinOpSpec" reference(t) ] -> { Zify.BinOpSpec.register t }
+| ["Add" "Zify" "UnOpSpec" reference(t) ] -> { Zify.UnOpSpec.register t }
+| ["Add" "Zify" "Saturate" reference(t) ] -> { Zify.Saturate.register t }
END
TACTIC EXTEND ITER
diff --git a/plugins/micromega/zify.ml b/plugins/micromega/zify.ml
index 61966b60c0..3ea7408067 100644
--- a/plugins/micromega/zify.ml
+++ b/plugins/micromega/zify.ml
@@ -23,6 +23,19 @@ let zify str =
(UnivGen.constr_of_monomorphic_global
(Coqlib.lib_ref ("ZifyClasses." ^ str)))
+(** classes *)
+let coq_InjTyp = lazy (Coqlib.lib_ref "ZifyClasses.InjTyp")
+
+let coq_BinOp = lazy (Coqlib.lib_ref "ZifyClasses.BinOp")
+let coq_UnOp = lazy (Coqlib.lib_ref "ZifyClasses.UnOp")
+let coq_CstOp = lazy (Coqlib.lib_ref "ZifyClasses.CstOp")
+let coq_BinRel = lazy (Coqlib.lib_ref "ZifyClasses.BinRel")
+let coq_PropBinOp = lazy (Coqlib.lib_ref "ZifyClasses.PropBinOp")
+let coq_PropUOp = lazy (Coqlib.lib_ref "ZifyClasses.PropUOp")
+let coq_BinOpSpec = lazy (Coqlib.lib_ref "ZifyClasses.BinOpSpec")
+let coq_UnOpSpec = lazy (Coqlib.lib_ref "ZifyClasses.UnOpSpec")
+let coq_Saturate = lazy (Coqlib.lib_ref "ZifyClasses.Saturate")
+
(* morphism like lemma *)
let mkapp2 = lazy (zify "mkapp2")
@@ -33,6 +46,7 @@ let mkrel = lazy (zify "mkrel")
let iff_refl = lazy (zify "iff_refl")
let eq_iff = lazy (zify "eq_iff")
let rew_iff = lazy (zify "rew_iff")
+let rew_iff_rev = lazy (zify "rew_iff_rev")
(* propositional logic *)
@@ -46,7 +60,7 @@ let op_iff_morph = lazy (zify "iff_morph")
let op_not = lazy (zify "not")
let op_not_morph = lazy (zify "not_morph")
let op_True = lazy (zify "True")
-let whd = Reductionops.clos_whd_flags CClosure.all
+let op_I = lazy (zify "I")
(** [unsafe_to_constr c] returns a [Constr.t] without considering an evar_map.
This is useful for calling Constr.hash *)
@@ -59,6 +73,7 @@ let gl_pr_constr e =
let evd = Evd.from_env genv in
pr_constr genv evd e
+let whd = Reductionops.clos_whd_flags CClosure.all
let is_convertible env evd t1 t2 = Reductionops.(is_conv env evd t1 t2)
(** [get_type_of] performs beta reduction ;
@@ -66,14 +81,36 @@ let is_convertible env evd t1 t2 = Reductionops.(is_conv env evd t1 t2)
let get_type_of env evd e =
Tacred.cbv_beta env evd (Retyping.get_type_of env evd e)
+(* arguments are dealt with in a second step *)
+
let rec find_option pred l =
match l with
| [] -> raise Not_found
| e :: l -> ( match pred e with Some r -> r | None -> find_option pred l )
-(** [HConstr] is a map indexed by EConstr.t.
- It should only be used using closed terms.
- *)
+module ConstrMap = struct
+ open Names.GlobRef
+
+ type 'a t = 'a list Map.t
+
+ let add gr e m =
+ Map.update gr (function None -> Some [e] | Some l -> Some (e :: l)) m
+
+ let empty = Map.empty
+
+ let find evd h m =
+ match Map.find (fst (EConstr.destRef evd h)) m with
+ | e :: _ -> e
+ | [] -> assert false
+
+ let find_all evd h m = Map.find (fst (EConstr.destRef evd h)) m
+
+ let fold f m acc =
+ Map.fold
+ (fun k l acc -> List.fold_left (fun acc e -> f k e acc) acc l)
+ m acc
+end
+
module HConstr = struct
module M = Map.Make (struct
type t = EConstr.t
@@ -81,20 +118,11 @@ module HConstr = struct
let compare c c' = Constr.compare (unsafe_to_constr c) (unsafe_to_constr c')
end)
- type 'a t = 'a list M.t
-
- let lfind h m = try M.find h m with Not_found -> []
-
- let add h e m =
- let l = lfind h m in
- M.add h (e :: l) m
+ type 'a t = 'a M.t
+ let add h e m = M.add h e m
let empty = M.empty
- let find h m = match lfind h m with e :: _ -> e | [] -> raise Not_found
- let find_all = lfind
-
- let fold f m acc =
- M.fold (fun k l acc -> List.fold_left (fun acc e -> f k e acc) acc l) m acc
+ let find = M.find
end
(** [get_projections_from_constant (evd,c) ]
@@ -331,7 +359,8 @@ module type Elt = sig
(** name *)
val name : string
- val table : (term_kind * decl_kind) HConstr.t ref
+ val gref : GlobRef.t Lazy.t
+ val table : (term_kind * decl_kind) ConstrMap.t ref
val cast : elt decl -> decl_kind
val dest : decl_kind -> elt decl option
@@ -346,12 +375,12 @@ module type Elt = sig
(* val arity : int*)
end
-let table = Summary.ref ~name:"zify_table" HConstr.empty
-let saturate = Summary.ref ~name:"zify_saturate" HConstr.empty
-let specs = Summary.ref ~name:"zify_specs" HConstr.empty
-let table_cache = ref HConstr.empty
-let saturate_cache = ref HConstr.empty
-let specs_cache = ref HConstr.empty
+let table = Summary.ref ~name:"zify_table" ConstrMap.empty
+let saturate = Summary.ref ~name:"zify_saturate" ConstrMap.empty
+let specs = Summary.ref ~name:"zify_specs" ConstrMap.empty
+let table_cache = ref ConstrMap.empty
+let saturate_cache = ref ConstrMap.empty
+let specs_cache = ref ConstrMap.empty
(** Each type-class gives rise to a different table.
They only differ on how projections are extracted. *)
@@ -362,6 +391,7 @@ module EInj = struct
type elt = EInjT.t
let name = "EInj"
+ let gref = coq_InjTyp
let table = table
let cast x = InjTyp x
let dest = function InjTyp x -> Some x | _ -> None
@@ -419,6 +449,7 @@ module EBinOp = struct
open EBinOpT
let name = "BinOp"
+ let gref = coq_BinOp
let table = table
let mk_elt evd i a =
@@ -460,6 +491,7 @@ module ECstOp = struct
open ECstOpT
let name = "CstOp"
+ let gref = coq_CstOp
let table = table
let cast x = CstOp x
let dest = function CstOp x -> Some x | _ -> None
@@ -486,6 +518,7 @@ module EUnOp = struct
open EUnOpT
let name = "UnOp"
+ let gref = coq_UnOp
let table = table
let cast x = UnOp x
let dest = function UnOp x -> Some x | _ -> None
@@ -518,6 +551,7 @@ module EBinRel = struct
open EBinRelT
let name = "BinRel"
+ let gref = coq_BinRel
let table = table
let cast x = BinRel x
let dest = function BinRel x -> Some x | _ -> None
@@ -544,6 +578,7 @@ module EPropBinOp = struct
open EPropBinOpT
let name = "PropBinOp"
+ let gref = coq_PropBinOp
let table = table
let cast x = PropOp x
let dest = function PropOp x -> Some x | _ -> None
@@ -556,7 +591,8 @@ module EPropUnOp = struct
open EPropUnOpT
- let name = "PropUnOp"
+ let name = "PropUOp"
+ let gref = coq_PropUOp
let table = table
let cast x = PropUnOp x
let dest = function PropUnOp x -> Some x | _ -> None
@@ -567,7 +603,7 @@ end
let constr_of_term_kind = function Application c -> c | OtherTerm c -> c
module type S = sig
- val register : Constrexpr.constr_expr -> unit
+ val register : Libnames.qualid -> unit
val print : unit -> unit
end
@@ -586,17 +622,26 @@ module MakeTable (E : Elt) = struct
failwith ("Cannot register term " ^ t)
| Some a -> E.mk_elt evd i a
+ let safe_ref evd c =
+ try
+ fst (EConstr.destRef evd c)
+ with DestKO -> CErrors.user_err Pp.(str "Add Zify "++str E.name ++ str ": the term "++
+ gl_pr_constr c ++ str " should be a global reference")
+
let register_hint evd t elt =
match EConstr.kind evd t with
| App (c, _) ->
- E.table := HConstr.add c (Application t, E.cast elt) !E.table
- | _ -> E.table := HConstr.add t (OtherTerm t, E.cast elt) !E.table
+ let gr = safe_ref evd c in
+ E.table := ConstrMap.add gr (Application t, E.cast elt) !E.table
+ | _ ->
+ let gr = safe_ref evd t in
+ E.table := ConstrMap.add gr (OtherTerm t, E.cast elt) !E.table
let register_constr env evd c =
let c = EConstr.of_constr c in
let t = get_type_of env evd c in
match EConstr.kind evd t with
- | App (intyp, args) ->
+ | App (intyp, args) when EConstr.isRefX evd (Lazy.force E.gref) intyp ->
let styp = args.(E.get_key) in
let elt = {decl = c; deriv = make_elt (evd, c)} in
register_hint evd styp elt
@@ -605,10 +650,11 @@ module MakeTable (E : Elt) = struct
raise
(CErrors.user_err
Pp.(
- str ": Cannot register term "
- ++ pr_constr env evd c ++ str ". It has type "
- ++ pr_constr env evd t
- ++ str " which should be of the form [F X1 .. Xn]"))
+ str "Cannot register " ++ pr_constr env evd c
+ ++ str ". It has type " ++ pr_constr env evd t
+ ++ str " instead of type "
+ ++ Printer.pr_global (Lazy.force E.gref)
+ ++ str " X1 ... Xn"))
let register_obj : Constr.constr -> Libobject.obj =
let cache_constr (_, c) =
@@ -622,22 +668,24 @@ module MakeTable (E : Elt) = struct
("register-zify-" ^ E.name)
~cache:cache_constr ~subst:(Some subst_constr)
- (** [register c] is called from the VERNACULAR ADD [name] constr(t).
+ (** [register c] is called from the VERNACULAR ADD [name] reference(t).
The term [c] is interpreted and
registered as a [superglobal_object_nodischarge].
TODO: pre-compute [get_type_of] - [cache_constr] is using another environment.
*)
let register c =
- let env = Global.env () in
- let evd = Evd.from_env env in
- let evd, c = Constrintern.interp_open_constr env evd c in
- let _ = Lib.add_anonymous_leaf (register_obj (EConstr.to_constr evd c)) in
- ()
+ try
+ let c = UnivGen.constr_of_monomorphic_global (Nametab.locate c) in
+ let _ = Lib.add_anonymous_leaf (register_obj c) in
+ ()
+ with Not_found ->
+ raise
+ (CErrors.user_err Pp.(Libnames.pr_qualid c ++ str " does not exist."))
let pp_keys () =
let env = Global.env () in
let evd = Evd.from_env env in
- HConstr.fold
+ ConstrMap.fold
(fun _ (k, d) acc ->
match E.dest d with
| None -> acc
@@ -656,6 +704,7 @@ module ESat = struct
open ESatT
let name = "Saturate"
+ let gref = coq_Saturate
let table = saturate
let cast x = Saturate x
let dest = function Saturate x -> Some x | _ -> None
@@ -669,6 +718,7 @@ module EUnopSpec = struct
type elt = ESpecT.t
let name = "UnopSpec"
+ let gref = coq_UnOpSpec
let table = specs
let cast x = UnOpSpec x
let dest = function UnOpSpec x -> Some x | _ -> None
@@ -682,6 +732,7 @@ module EBinOpSpec = struct
type elt = ESpecT.t
let name = "BinOpSpec"
+ let gref = coq_BinOpSpec
let table = specs
let cast x = BinOpSpec x
let dest = function BinOpSpec x -> Some x | _ -> None
@@ -947,9 +998,11 @@ let app_binop evd src binop arg1 prf1 arg2 prf2 =
type typed_constr = {constr : EConstr.t; typ : EConstr.t; inj : EInjT.t}
let get_injection env evd t =
- match snd (HConstr.find t !table_cache) with
- | InjTyp i -> i
- | _ -> raise Not_found
+ try
+ match snd (ConstrMap.find evd t !table_cache) with
+ | InjTyp i -> i
+ | _ -> raise Not_found
+ with DestKO -> raise Not_found
(* [arrow] is the term (fun (x:Prop) (y : Prop) => x -> y) *)
let arrow =
@@ -1087,7 +1140,7 @@ let declared_term env evd hd args =
| PropUnOp _ -> decomp t 1
| _ -> None )
in
- find_option match_operator (HConstr.find_all hd !table)
+ find_option match_operator (ConstrMap.find_all evd hd !table)
let rec trans_expr env evd e =
let inj = e.inj in
@@ -1099,7 +1152,7 @@ let rec trans_expr env evd e =
let k, t =
find_option
(match_operator env evd c a)
- (HConstr.find_all c !table_cache)
+ (ConstrMap.find_all evd c !table_cache)
in
let n = Array.length a in
match k with
@@ -1243,7 +1296,7 @@ let rec trans_prop env evd e =
let k, t =
find_option
(match_operator env evd c a)
- (HConstr.find_all c !table_cache)
+ (ConstrMap.find_all evd c !table_cache)
in
let n = Array.length a in
match k with
@@ -1262,7 +1315,7 @@ let rec trans_prop env evd e =
in
trans_binrel evd e rop a.(n - 2) a1 a.(n - 1) a2
| _ -> IProof
- with Not_found -> IProof )
+ with Not_found | DestKO -> IProof )
let trans_check_prop env evd t =
if is_prop env evd t then Some (trans_prop env evd t) else None
@@ -1319,7 +1372,15 @@ let trans_concl prfp =
Tactics.change_concl t')
| TProof (t, prf) ->
Proofview.Goal.enter (fun gl ->
- Equality.general_rewrite true Locus.AllOccurrences true false prf)
+ let env = Tacmach.New.pf_env gl in
+ let evd = Tacmach.New.project gl in
+ let typ = get_type_of env evd prf in
+ match EConstr.kind evd typ with
+ | App (c, a) when Array.length a = 2 ->
+ Tactics.apply
+ (EConstr.mkApp (Lazy.force rew_iff_rev, [|a.(0); a.(1); prf|]))
+ | _ ->
+ raise (CErrors.anomaly Pp.(str "zify cannot transform conclusion")))
let tclTHENOpt e tac tac' =
match e with None -> tac' | Some e' -> Tacticals.New.tclTHEN (tac e') tac'
@@ -1359,7 +1420,7 @@ let do_let tac (h : Constr.named_declaration) =
find_option
(match_operator env evd eq
[|EConstr.of_constr ty; EConstr.mkVar x; EConstr.of_constr t|])
- (HConstr.find_all eq !table_cache));
+ (ConstrMap.find_all evd eq !table_cache));
tac x (EConstr.of_constr t) (EConstr.of_constr ty)
with Not_found -> Tacticals.New.tclIDTAC)
@@ -1453,12 +1514,12 @@ let rec spec_of_term env evd (senv : spec_env) t =
try (EConstr.mkVar (HConstr.find t' senv'.map), senv')
with Not_found -> (
try
- match snd (HConstr.find c !specs_cache) with
+ match snd (ConstrMap.find evd c !specs_cache) with
| UnOpSpec s | BinOpSpec s ->
let thm = EConstr.mkApp (s.deriv.ESpecT.spec, a') in
register_constr senv' t' thm
| _ -> (get_name t' senv', senv')
- with Not_found -> (t', senv') )
+ with Not_found | DestKO -> (t', senv') )
let interp_pscript s =
match s with
@@ -1493,47 +1554,58 @@ let spec_of_hyps =
let iter_specs = spec_of_hyps
let find_hyp evd t l =
- try Some (fst (List.find (fun (h, t') -> EConstr.eq_constr evd t t') l))
+ try
+ Some
+ (EConstr.mkVar
+ (fst (List.find (fun (h, t') -> EConstr.eq_constr evd t t') l)))
with Not_found -> None
-let sat_constr c d =
- Proofview.Goal.enter (fun gl ->
- let evd = Tacmach.New.project gl in
- let env = Tacmach.New.pf_env gl in
- let hyps = Tacmach.New.pf_hyps_types gl in
- match EConstr.kind evd c with
- | App (c, args) ->
- if Array.length args = 2 then
- let h1 =
- Tacred.cbv_beta env evd
- (EConstr.mkApp (d.ESatT.parg1, [|args.(0)|]))
- in
- let h2 =
- Tacred.cbv_beta env evd
- (EConstr.mkApp (d.ESatT.parg2, [|args.(1)|]))
- in
- match (find_hyp evd h1 hyps, find_hyp evd h2 hyps) with
- | Some h1, Some h2 ->
- let n =
- Tactics.fresh_id_in_env Id.Set.empty
- (Names.Id.of_string "__sat")
- env
- in
- let trm =
- EConstr.mkApp
- ( d.ESatT.satOK
- , [|args.(0); args.(1); EConstr.mkVar h1; EConstr.mkVar h2|] )
- in
- Tactics.pose_proof (Names.Name n) trm
- | _, _ -> Tacticals.New.tclIDTAC
- else Tacticals.New.tclIDTAC
- | _ -> Tacticals.New.tclIDTAC)
+let find_proof evd t l =
+ if EConstr.eq_constr evd t (Lazy.force op_True) then Some (Lazy.force op_I)
+ else find_hyp evd t l
+
+(** [sat_constr env evd sub taclist hyps c d]= (sub',taclist',hyps') where
+ - sub' is a fresh subscript obtained from sub
+ - taclist' is obtained from taclist by posing the lemma 'd' applied to 'c'
+ - hyps' is obtained from hyps'
+ taclist and hyps are threaded to avoid adding duplicates
+ *)
+let sat_constr env evd (sub,taclist, hyps) c d =
+ match EConstr.kind evd c with
+ | App (c, args) ->
+ if Array.length args = 2 then
+ let h1 =
+ Tacred.cbv_beta env evd
+ (EConstr.mkApp (d.ESatT.parg1, [|args.(0)|]))
+ in
+ let h2 =
+ Tacred.cbv_beta env evd
+ (EConstr.mkApp (d.ESatT.parg2, [|args.(1)|]))
+ in
+ let n = Nameops.add_subscript (Names.Id.of_string "__sat") sub in
+ let trm =
+ match (find_proof evd h1 hyps, find_proof evd h2 hyps) with
+ | Some h1, Some h2 ->
+ (EConstr.mkApp (d.ESatT.satOK, [|args.(0); args.(1); h1; h2|]))
+ | Some h1, _ ->
+ EConstr.mkApp (d.ESatT.satOK, [|args.(0); args.(1); h1|])
+ | _, _ -> EConstr.mkApp (d.ESatT.satOK, [|args.(0); args.(1)|])
+ in
+ let rtrm = Tacred.cbv_beta env evd trm in
+ let typ = Retyping.get_type_of env evd rtrm in
+ match find_hyp evd typ hyps with
+ | None -> (Nameops.Subscript.succ sub, (Tactics.pose_proof (Names.Name n) rtrm :: taclist) , (n,typ)::hyps)
+ | Some _ -> (sub, taclist, hyps)
+ else (sub,taclist,hyps)
+ | _ -> (sub,taclist,hyps)
+
let get_all_sat env evd c =
List.fold_left
(fun acc e -> match e with _, Saturate s -> s :: acc | _ -> acc)
[]
- (HConstr.find_all c !saturate_cache)
+ ( try ConstrMap.find_all evd c !saturate_cache
+ with DestKO | Not_found -> [] )
let saturate =
Proofview.Goal.enter (fun gl ->
@@ -1550,8 +1622,10 @@ let saturate =
Array.iter sat args;
if Array.length args = 2 then
let ds = get_all_sat env evd c in
- if ds = [] then ()
- else List.iter (fun x -> CstrTable.HConstr.add table t x.deriv) ds
+ if ds = [] || CstrTable.HConstr.mem table t
+ then ()
+ else List.iter (fun x ->
+ CstrTable.HConstr.add table t x.deriv) ds
else ()
| Prod (a, t1, t2) when a.Context.binder_name = Names.Anonymous ->
sat t1; sat t2
@@ -1560,5 +1634,6 @@ let saturate =
(* Collect all the potential saturation lemma *)
sat concl;
List.iter (fun (_, t) -> sat t) hyps;
- Tacticals.New.tclTHENLIST
- (CstrTable.HConstr.fold (fun c d acc -> sat_constr c d :: acc) table []))
+ let s0 = fresh_subscript env in
+ let (_,tacs,_) = CstrTable.HConstr.fold (fun c d acc -> sat_constr env evd acc c d) table (s0,[],hyps) in
+ Tacticals.New.tclTHENLIST tacs)
diff --git a/plugins/micromega/zify.mli b/plugins/micromega/zify.mli
index 555bb4c7fb..68f23393ee 100644
--- a/plugins/micromega/zify.mli
+++ b/plugins/micromega/zify.mli
@@ -7,10 +7,9 @@
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-open Constrexpr
module type S = sig
- val register : constr_expr -> unit
+ val register : Libnames.qualid -> unit
val print : unit -> unit
end
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
deleted file mode 100644
index 9d92ffde74..0000000000
--- a/plugins/omega/coq_omega.ml
+++ /dev/null
@@ -1,1939 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * Copyright INRIA, CNRS and contributors *)
-(* <O___,, * (see version control and CREDITS file for authors & dates) *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(* * (see LICENSE file for the text of the license) *)
-(************************************************************************)
-(**************************************************************************)
-(* *)
-(* Omega: a solver of quantifier-free problems in Presburger Arithmetic *)
-(* *)
-(* Pierre Crégut (CNET, Lannion, France) *)
-(* *)
-(**************************************************************************)
-
-open CErrors
-open Util
-open Names
-open Constr
-open Context
-open Nameops
-open EConstr
-open Tacticals.New
-open Tacmach.New
-open Tactics
-open Libnames
-open Nametab
-open Contradiction
-open Tactypes
-open Context.Named.Declaration
-
-module NamedDecl = Context.Named.Declaration
-
-module ZOmega = struct
- type bigint = Z.t
- let equal = Z.equal
- let less_than = Z.lt
- let add = Z.add
- let sub = Z.sub
- let mult = Z.mul
- let euclid = Z.div_rem
- let neg = Z.neg
- let zero = Z.zero
- let one = Z.one
- let to_string = Z.to_string
-end
-
-module OmegaSolver = Omega.MakeOmegaSolver (ZOmega)
-open OmegaSolver
-
-(* Added by JCF, 09/03/98 *)
-
-let elim_id id = simplest_elim (mkVar id)
-
-let resolve_id id = apply (mkVar id)
-
-let display_system_flag = ref false
-let display_action_flag = ref false
-let old_style_flag = ref false
-let letin_flag = ref true
-
-(* Should we reset all variable labels between two runs of omega ? *)
-
-let reset_flag = ref true
-
-(* Coq < 8.5 was not performing such resets, hence omega was slightly
- non-deterministic: successive runs of omega on the same problem may
- lead to distinct proof-terms.
- At the very least, these terms differed on the inner
- variable names, but they could even be non-convertible :
- the OmegaSolver relies on Hashtbl.iter, it can hence find a different
- solution when variable indices differ. *)
-
-let read f () = !f
-let write f x = f:=x
-
-open Goptions
-
-let () =
- declare_bool_option
- { optdepr = false;
- optkey = ["Omega";"System"];
- optread = read display_system_flag;
- optwrite = write display_system_flag }
-
-let () =
- declare_bool_option
- { optdepr = false;
- optkey = ["Omega";"Action"];
- optread = read display_action_flag;
- optwrite = write display_action_flag }
-
-let () =
- declare_bool_option
- { optdepr = false;
- optkey = ["Omega";"OldStyle"];
- optread = read old_style_flag;
- optwrite = write old_style_flag }
-
-let () =
- declare_bool_option
- { optdepr = true;
- optkey = ["Stable";"Omega"];
- optread = read reset_flag;
- optwrite = write reset_flag }
-
-let () =
- declare_bool_option
- { optdepr = false;
- optkey = ["Omega";"UseLocalDefs"];
- optread = read letin_flag;
- optwrite = write letin_flag }
-
-let intref, reset_all_references =
- let refs = ref [] in
- (fun n -> let r = ref n in refs := (r,n) :: !refs; r),
- (fun () -> List.iter (fun (r,n) -> r:=n) !refs)
-
-let new_identifier =
- let cpt = intref 0 in
- (fun () -> let s = "Omega" ^ string_of_int !cpt in incr cpt; Id.of_string s)
-
-let new_identifier_var =
- let cpt = intref 0 in
- (fun () -> let s = "Zvar" ^ string_of_int !cpt in incr cpt; Id.of_string s)
-
-let new_id =
- let cpt = intref 0 in fun () -> incr cpt; !cpt
-
-let new_var_num =
- let cpt = intref 1000 in (fun () -> incr cpt; !cpt)
-
-let new_var =
- let cpt = intref 0 in fun () -> incr cpt; Nameops.make_ident "WW" (Some !cpt)
-
-let display_var i = Printf.sprintf "X%d" i
-
-let intern_id,unintern_id,reset_intern_tables =
- let cpt = ref 0 in
- let table = Hashtbl.create 7 and co_table = Hashtbl.create 7 in
- (fun (name : Id.t) ->
- try Hashtbl.find table name with Not_found ->
- let idx = !cpt in
- Hashtbl.add table name idx;
- Hashtbl.add co_table idx name;
- incr cpt; idx),
- (fun idx ->
- try Hashtbl.find co_table idx with Not_found ->
- let v = new_var () in
- Hashtbl.add table v idx; Hashtbl.add co_table idx v; v),
- (fun () -> cpt := 0; Hashtbl.clear table)
-
-let mk_then tacs = tclTHENLIST tacs
-
-let exists_tac c = constructor_tac false (Some 1) 1 (ImplicitBindings [c])
-
-let generalize_tac t = generalize t
-let unfold s = Tactics.unfold_in_concl [Locus.AllOccurrences, Lazy.force s]
-let pf_nf gl c = pf_apply Tacred.simpl gl c
-
-let rev_assoc k =
- let rec loop = function
- | [] -> raise Not_found
- | (v,k')::_ when Int.equal k k' -> v
- | _ :: l -> loop l
- in
- loop
-
-let tag_hypothesis, hyp_of_tag, clear_tags =
- let l = ref ([]:(Id.t * int) list) in
- (fun h id -> l := (h,id):: !l),
- (fun h -> try rev_assoc h !l with Not_found -> failwith "tag_hypothesis"),
- (fun () -> l := [])
-
-let hide_constr,find_constr,clear_constr_tables,dump_tables =
- let l = ref ([]:(constr * (Id.t * Id.t * bool)) list) in
- (fun h id eg b -> l := (h,(id,eg,b)):: !l),
- (fun sigma h ->
- try List.assoc_f (eq_constr_nounivs sigma) h !l with Not_found -> failwith "find_contr"),
- (fun () -> l := []),
- (fun () -> !l)
-
-let reset_all () =
- if !reset_flag then begin
- reset_all_references ();
- reset_intern_tables ();
- clear_tags ();
- clear_constr_tables ()
- end
-
-(* Lazy evaluation is used for Coq constants, because this code
- is evaluated before the compiled modules are loaded.
- To use the constant Zplus, one must type "Lazy.force coq_Zplus"
- This is the right way to access to Coq constants in tactics ML code *)
-
-let gen_constant k = lazy (k |> Coqlib.lib_ref |> UnivGen.constr_of_monomorphic_global
- |> EConstr.of_constr)
-
-
-(* Zarith *)
-let coq_xH = gen_constant "num.pos.xH"
-let coq_xO = gen_constant "num.pos.xO"
-let coq_xI = gen_constant "num.pos.xI"
-let coq_Z0 = gen_constant "num.Z.Z0"
-let coq_Zpos = gen_constant "num.Z.Zpos"
-let coq_Zneg = gen_constant "num.Z.Zneg"
-let coq_Z = gen_constant "num.Z.type"
-let coq_comparison = gen_constant "core.comparison.type"
-let coq_Gt = gen_constant "core.comparison.Gt"
-let coq_Zplus = gen_constant "num.Z.add"
-let coq_Zmult = gen_constant "num.Z.mul"
-let coq_Zopp = gen_constant "num.Z.opp"
-let coq_Zminus = gen_constant "num.Z.sub"
-let coq_Zsucc = gen_constant "num.Z.succ"
-let coq_Zpred = gen_constant "num.Z.pred"
-let coq_Z_of_nat = gen_constant "num.Z.of_nat"
-let coq_inj_plus = gen_constant "num.Nat2Z.inj_add"
-let coq_inj_mult = gen_constant "num.Nat2Z.inj_mul"
-let coq_inj_minus1 = gen_constant "num.Nat2Z.inj_sub"
-let coq_inj_minus2 = gen_constant "plugins.omega.inj_minus2"
-let coq_inj_S = gen_constant "num.Nat2Z.inj_succ"
-let coq_inj_eq = gen_constant "plugins.omega.inj_eq"
-let coq_inj_neq = gen_constant "plugins.omega.inj_neq"
-let coq_inj_le = gen_constant "plugins.omega.inj_le"
-let coq_inj_lt = gen_constant "plugins.omega.inj_lt"
-let coq_inj_ge = gen_constant "plugins.omega.inj_ge"
-let coq_inj_gt = gen_constant "plugins.omega.inj_gt"
-let coq_fast_Zplus_assoc_reverse = gen_constant "plugins.omega.fast_Zplus_assoc_reverse"
-let coq_fast_Zplus_assoc = gen_constant "plugins.omega.fast_Zplus_assoc"
-let coq_fast_Zmult_assoc_reverse = gen_constant "plugins.omega.fast_Zmult_assoc_reverse"
-let coq_fast_Zplus_permute = gen_constant "plugins.omega.fast_Zplus_permute"
-let coq_fast_Zplus_comm = gen_constant "plugins.omega.fast_Zplus_comm"
-let coq_fast_Zmult_comm = gen_constant "plugins.omega.fast_Zmult_comm"
-let coq_Zmult_le_approx = gen_constant "plugins.omega.Zmult_le_approx"
-let coq_OMEGA1 = gen_constant "plugins.omega.OMEGA1"
-let coq_OMEGA2 = gen_constant "plugins.omega.OMEGA2"
-let coq_OMEGA3 = gen_constant "plugins.omega.OMEGA3"
-let coq_OMEGA4 = gen_constant "plugins.omega.OMEGA4"
-let coq_OMEGA5 = gen_constant "plugins.omega.OMEGA5"
-let coq_OMEGA6 = gen_constant "plugins.omega.OMEGA6"
-let coq_OMEGA7 = gen_constant "plugins.omega.OMEGA7"
-let coq_OMEGA8 = gen_constant "plugins.omega.OMEGA8"
-let coq_OMEGA9 = gen_constant "plugins.omega.OMEGA9"
-let coq_fast_OMEGA10 = gen_constant "plugins.omega.fast_OMEGA10"
-let coq_fast_OMEGA11 = gen_constant "plugins.omega.fast_OMEGA11"
-let coq_fast_OMEGA12 = gen_constant "plugins.omega.fast_OMEGA12"
-let coq_fast_OMEGA13 = gen_constant "plugins.omega.fast_OMEGA13"
-let coq_fast_OMEGA14 = gen_constant "plugins.omega.fast_OMEGA14"
-let coq_fast_OMEGA15 = gen_constant "plugins.omega.fast_OMEGA15"
-let coq_fast_OMEGA16 = gen_constant "plugins.omega.fast_OMEGA16"
-let coq_OMEGA17 = gen_constant "plugins.omega.OMEGA17"
-let coq_OMEGA18 = gen_constant "plugins.omega.OMEGA18"
-let coq_OMEGA19 = gen_constant "plugins.omega.OMEGA19"
-let coq_OMEGA20 = gen_constant "plugins.omega.OMEGA20"
-let coq_fast_Zred_factor0 = gen_constant "plugins.omega.fast_Zred_factor0"
-let coq_fast_Zred_factor1 = gen_constant "plugins.omega.fast_Zred_factor1"
-let coq_fast_Zred_factor2 = gen_constant "plugins.omega.fast_Zred_factor2"
-let coq_fast_Zred_factor3 = gen_constant "plugins.omega.fast_Zred_factor3"
-let coq_fast_Zred_factor4 = gen_constant "plugins.omega.fast_Zred_factor4"
-let coq_fast_Zred_factor5 = gen_constant "plugins.omega.fast_Zred_factor5"
-let coq_fast_Zred_factor6 = gen_constant "plugins.omega.fast_Zred_factor6"
-let coq_fast_Zmult_plus_distr_l = gen_constant "plugins.omega.fast_Zmult_plus_distr_l"
-let coq_fast_Zopp_plus_distr = gen_constant "plugins.omega.fast_Zopp_plus_distr"
-let coq_fast_Zopp_mult_distr_r = gen_constant "plugins.omega.fast_Zopp_mult_distr_r"
-let coq_fast_Zopp_eq_mult_neg_1 = gen_constant "plugins.omega.fast_Zopp_eq_mult_neg_1"
-let coq_Zegal_left = gen_constant "plugins.omega.Zegal_left"
-let coq_Zne_left = gen_constant "plugins.omega.Zne_left"
-let coq_Zlt_left = gen_constant "plugins.omega.Zlt_left"
-let coq_Zge_left = gen_constant "plugins.omega.Zge_left"
-let coq_Zgt_left = gen_constant "plugins.omega.Zgt_left"
-let coq_Zle_left = gen_constant "plugins.omega.Zle_left"
-let coq_new_var = gen_constant "plugins.omega.new_var"
-let coq_intro_Z = gen_constant "plugins.omega.intro_Z"
-
-let coq_dec_eq = gen_constant "num.Z.eq_decidable"
-let coq_dec_Zne = gen_constant "plugins.omega.dec_Zne"
-let coq_dec_Zle = gen_constant "num.Z.le_decidable"
-let coq_dec_Zlt = gen_constant "num.Z.lt_decidable"
-let coq_dec_Zgt = gen_constant "plugins.omega.dec_Zgt"
-let coq_dec_Zge = gen_constant "plugins.omega.dec_Zge"
-
-let coq_not_Zeq = gen_constant "plugins.omega.not_Zeq"
-let coq_not_Zne = gen_constant "plugins.omega.not_Zne"
-let coq_Znot_le_gt = gen_constant "plugins.omega.Znot_le_gt"
-let coq_Znot_lt_ge = gen_constant "plugins.omega.Znot_lt_ge"
-let coq_Znot_ge_lt = gen_constant "plugins.omega.Znot_ge_lt"
-let coq_Znot_gt_le = gen_constant "plugins.omega.Znot_gt_le"
-let coq_neq = gen_constant "plugins.omega.neq"
-let coq_Zne = gen_constant "plugins.omega.Zne"
-let coq_Zle = gen_constant "num.Z.le"
-let coq_Zlt = gen_constant "num.Z.lt"
-let coq_Zge = gen_constant "num.Z.ge"
-let coq_Zgt = gen_constant "num.Z.gt"
-
-(* Peano/Datatypes *)
-let coq_nat = gen_constant "num.nat.type"
-let coq_O = gen_constant "num.nat.O"
-let coq_S = gen_constant "num.nat.S"
-let coq_le = gen_constant "num.nat.le"
-let coq_lt = gen_constant "num.nat.lt"
-let coq_ge = gen_constant "num.nat.ge"
-let coq_gt = gen_constant "num.nat.gt"
-let coq_plus = gen_constant "num.nat.add"
-let coq_minus = gen_constant "num.nat.sub"
-let coq_mult = gen_constant "num.nat.mul"
-let coq_pred = gen_constant "num.nat.pred"
-
-(* Compare_dec/Peano_dec/Minus *)
-let coq_pred_of_minus = gen_constant "num.nat.pred_of_minus"
-let coq_le_gt_dec = gen_constant "num.nat.le_gt_dec"
-let coq_dec_eq_nat = gen_constant "num.nat.eq_dec"
-let coq_dec_le = gen_constant "num.nat.dec_le"
-let coq_dec_lt = gen_constant "num.nat.dec_lt"
-let coq_dec_ge = gen_constant "num.nat.dec_ge"
-let coq_dec_gt = gen_constant "num.nat.dec_gt"
-let coq_not_eq = gen_constant "num.nat.not_eq"
-let coq_not_le = gen_constant "num.nat.not_le"
-let coq_not_lt = gen_constant "num.nat.not_lt"
-let coq_not_ge = gen_constant "num.nat.not_ge"
-let coq_not_gt = gen_constant "num.nat.not_gt"
-
-(* Logic/Decidable *)
-let coq_eq_ind_r = gen_constant "core.eq.ind_r"
-
-let coq_dec_or = gen_constant "core.dec.or"
-let coq_dec_and = gen_constant "core.dec.and"
-let coq_dec_imp = gen_constant "core.dec.imp"
-let coq_dec_iff = gen_constant "core.dec.iff"
-let coq_dec_not = gen_constant "core.dec.not"
-let coq_dec_False = gen_constant "core.dec.False"
-let coq_dec_not_not = gen_constant "core.dec.not_not"
-let coq_dec_True = gen_constant "core.dec.True"
-
-let coq_not_or = gen_constant "core.dec.not_or"
-let coq_not_and = gen_constant "core.dec.not_and"
-let coq_not_imp = gen_constant "core.dec.not_imp"
-let coq_not_iff = gen_constant "core.dec.not_iff"
-let coq_not_not = gen_constant "core.dec.dec_not_not"
-let coq_imp_simp = gen_constant "core.dec.imp_simp"
-let coq_iff = gen_constant "core.iff.type"
-let coq_not = gen_constant "core.not.type"
-let coq_and = gen_constant "core.and.type"
-let coq_or = gen_constant "core.or.type"
-let coq_eq = gen_constant "core.eq.type"
-let coq_ex = gen_constant "core.ex.type"
-let coq_False = gen_constant "core.False.type"
-let coq_True = gen_constant "core.True.type"
-
-(* uses build_coq_and, build_coq_not, build_coq_or, build_coq_ex *)
-
-(* For unfold *)
-let evaluable_ref_of_constr s c =
- let env = Global.env () in
- let evd = Evd.from_env env in
- let open Tacred in
- match EConstr.kind evd (Lazy.force c) with
- | Const (kn,u) when is_evaluable env (EvalConstRef kn) ->
- EvalConstRef kn
- | _ -> anomaly ~label:"Coq_omega" (Pp.str (s^" is not an evaluable constant."))
-
-let sp_Zsucc = lazy (evaluable_ref_of_constr "Z.succ" coq_Zsucc)
-let sp_Zpred = lazy (evaluable_ref_of_constr "Z.pred" coq_Zpred)
-let sp_Zminus = lazy (evaluable_ref_of_constr "Z.sub" coq_Zminus)
-let sp_Zle = lazy (evaluable_ref_of_constr "Z.le" coq_Zle)
-let sp_Zgt = lazy (evaluable_ref_of_constr "Z.gt" coq_Zgt)
-let sp_not = lazy (evaluable_ref_of_constr "not" coq_not)
-
-let mk_plus t1 t2 = mkApp (Lazy.force coq_Zplus, [| t1; t2 |])
-let mk_times t1 t2 = mkApp (Lazy.force coq_Zmult, [| t1; t2 |])
-let mk_minus t1 t2 = mkApp (Lazy.force coq_Zminus, [| t1;t2 |])
-let mk_gen_eq ty t1 t2 = mkApp (Lazy.force coq_eq, [| ty; t1; t2 |])
-let mk_eq t1 t2 = mk_gen_eq (Lazy.force coq_Z) t1 t2
-let mk_gt t1 t2 = mkApp (Lazy.force coq_Zgt, [| t1; t2 |])
-let mk_inv t = mkApp (Lazy.force coq_Zopp, [| t |])
-let mk_and t1 t2 = mkApp (Lazy.force coq_and, [| t1; t2 |])
-let mk_or t1 t2 = mkApp (Lazy.force coq_or, [| t1; t2 |])
-let mk_not t = mkApp (Lazy.force coq_not, [| t |])
-let mk_inj t = mkApp (Lazy.force coq_Z_of_nat, [| t |])
-
-let mk_integer n =
- let rec loop n =
- if n =? one then Lazy.force coq_xH else
- mkApp((if n mod two =? zero then Lazy.force coq_xO else Lazy.force coq_xI),
- [| loop (n/two) |])
- in
- if n =? zero then Lazy.force coq_Z0
- else mkApp ((if n >? zero then Lazy.force coq_Zpos else Lazy.force coq_Zneg),
- [| loop (abs n) |])
-
-type omega_constant =
- | Zplus | Zmult | Zminus | Zsucc | Zopp | Zpred
- | Plus | Mult | Minus | Pred | S | O
- | Zpos | Zneg | Z0 | Z_of_nat
- | Eq | Neq
- | Zne | Zle | Zlt | Zge | Zgt
- | Z | Nat
- | And | Or | False | True | Not | Iff
- | Le | Lt | Ge | Gt
- | Other of string
-
-type result =
- | Kvar of Id.t
- | Kapp of omega_constant * constr list
- | Kimp of constr * constr
- | Kufo
-
-(* Nota: Kimp correspond to a binder (Prod), but hopefully we won't
- have to bother with term lifting: Kimp will correspond to anonymous
- product, for which (Rel 1) doesn't occur in the right term.
- Moreover, we'll work on fully introduced goals, hence no Rel's in
- the term parts that we manipulate, but rather Var's.
- Said otherwise: all constr manipulated here are closed *)
-
-let destructurate_prop sigma t =
- let eq_constr c1 c2 = eq_constr sigma c1 c2 in
- let c, args = decompose_app sigma t in
- match EConstr.kind sigma c, args with
- | _, [_;_;_] when eq_constr (Lazy.force coq_eq) c -> Kapp (Eq,args)
- | _, [_;_] when eq_constr c (Lazy.force coq_neq) -> Kapp (Neq,args)
- | _, [_;_] when eq_constr c (Lazy.force coq_Zne) -> Kapp (Zne,args)
- | _, [_;_] when eq_constr c (Lazy.force coq_Zle) -> Kapp (Zle,args)
- | _, [_;_] when eq_constr c (Lazy.force coq_Zlt) -> Kapp (Zlt,args)
- | _, [_;_] when eq_constr c (Lazy.force coq_Zge) -> Kapp (Zge,args)
- | _, [_;_] when eq_constr c (Lazy.force coq_Zgt) -> Kapp (Zgt,args)
- | _, [_;_] when eq_constr c (Lazy.force coq_and) -> Kapp (And,args)
- | _, [_;_] when eq_constr c (Lazy.force coq_or) -> Kapp (Or,args)
- | _, [_;_] when eq_constr c (Lazy.force coq_iff) -> Kapp (Iff, args)
- | _, [_] when eq_constr c (Lazy.force coq_not) -> Kapp (Not,args)
- | _, [] when eq_constr c (Lazy.force coq_False) -> Kapp (False,args)
- | _, [] when eq_constr c (Lazy.force coq_True) -> Kapp (True,args)
- | _, [_;_] when eq_constr c (Lazy.force coq_le) -> Kapp (Le,args)
- | _, [_;_] when eq_constr c (Lazy.force coq_lt) -> Kapp (Lt,args)
- | _, [_;_] when eq_constr c (Lazy.force coq_ge) -> Kapp (Ge,args)
- | _, [_;_] when eq_constr c (Lazy.force coq_gt) -> Kapp (Gt,args)
- | Const (sp,_), args ->
- Kapp (Other (string_of_path (path_of_global (GlobRef.ConstRef sp))),args)
- | Construct (csp,_) , args ->
- Kapp (Other (string_of_path (path_of_global (GlobRef.ConstructRef csp))), args)
- | Ind (isp,_), args ->
- Kapp (Other (string_of_path (path_of_global (GlobRef.IndRef isp))),args)
- | Var id,[] -> Kvar id
- | Prod ({binder_name=Anonymous},typ,body), [] -> Kimp(typ,body)
- | Prod ({binder_name=Name _},_,_),[] -> CErrors.user_err Pp.(str "Omega: Not a quantifier-free goal")
- | _ -> Kufo
-
-let nf = Tacred.simpl
-
-let destructurate_type env sigma t =
- let is_conv = Reductionops.is_conv env sigma in
- let c, args = decompose_app sigma (nf env sigma t) in
- match EConstr.kind sigma c, args with
- | _, [] when is_conv c (Lazy.force coq_Z) -> Kapp (Z,args)
- | _, [] when is_conv c (Lazy.force coq_nat) -> Kapp (Nat,args)
- | _ -> Kufo
-
-let destructurate_term sigma t =
- let eq_constr c1 c2 = eq_constr sigma c1 c2 in
- let c, args = decompose_app sigma t in
- match EConstr.kind sigma c, args with
- | _, [_;_] when eq_constr c (Lazy.force coq_Zplus) -> Kapp (Zplus,args)
- | _, [_;_] when eq_constr c (Lazy.force coq_Zmult) -> Kapp (Zmult,args)
- | _, [_;_] when eq_constr c (Lazy.force coq_Zminus) -> Kapp (Zminus,args)
- | _, [_] when eq_constr c (Lazy.force coq_Zsucc) -> Kapp (Zsucc,args)
- | _, [_] when eq_constr c (Lazy.force coq_Zpred) -> Kapp (Zpred,args)
- | _, [_] when eq_constr c (Lazy.force coq_Zopp) -> Kapp (Zopp,args)
- | _, [_;_] when eq_constr c (Lazy.force coq_plus) -> Kapp (Plus,args)
- | _, [_;_] when eq_constr c (Lazy.force coq_mult) -> Kapp (Mult,args)
- | _, [_;_] when eq_constr c (Lazy.force coq_minus) -> Kapp (Minus,args)
- | _, [_] when eq_constr c (Lazy.force coq_pred) -> Kapp (Pred,args)
- | _, [_] when eq_constr c (Lazy.force coq_S) -> Kapp (S,args)
- | _, [] when eq_constr c (Lazy.force coq_O) -> Kapp (O,args)
- | _, [_] when eq_constr c (Lazy.force coq_Zpos) -> Kapp (Zneg,args)
- | _, [_] when eq_constr c (Lazy.force coq_Zneg) -> Kapp (Zpos,args)
- | _, [] when eq_constr c (Lazy.force coq_Z0) -> Kapp (Z0,args)
- | _, [_] when eq_constr c (Lazy.force coq_Z_of_nat) -> Kapp (Z_of_nat,args)
- | Var id,[] -> Kvar id
- | _ -> Kufo
-
-let recognize_number sigma t =
- let eq_constr c1 c2 = eq_constr sigma c1 c2 in
- let rec loop t =
- match decompose_app sigma t with
- | f, [t] when eq_constr f (Lazy.force coq_xI) -> one + two * loop t
- | f, [t] when eq_constr f (Lazy.force coq_xO) -> two * loop t
- | f, [] when eq_constr f (Lazy.force coq_xH) -> one
- | _ -> failwith "not a number"
- in
- match decompose_app sigma t with
- | f, [t] when eq_constr f (Lazy.force coq_Zpos) -> loop t
- | f, [t] when eq_constr f (Lazy.force coq_Zneg) -> neg (loop t)
- | f, [] when eq_constr f (Lazy.force coq_Z0) -> zero
- | _ -> failwith "not a number"
-
-type constr_path =
- | P_APP of int
- (* Abstraction and product *)
- | P_TYPE
-
-let context sigma operation path (t : constr) =
- let rec loop i p0 t =
- match (p0,EConstr.kind sigma t) with
- | (p, Cast (c,k,t)) -> mkCast (loop i p c,k,t)
- | ([], _) -> operation i t
- | ((P_APP n :: p), App (f,v)) ->
- let v' = Array.copy v in
- v'.(pred n) <- loop i p v'.(pred n); mkApp (f, v')
- | (p, Fix ((_,n as ln),(tys,lna,v))) ->
- let l = Array.length v in
- let v' = Array.copy v in
- v'.(n)<- loop (Util.(+) i l) p v.(n); (mkFix (ln,(tys,lna,v')))
- | ((P_TYPE :: p), Prod (n,t,c)) ->
- (mkProd (n,loop i p t,c))
- | ((P_TYPE :: p), Lambda (n,t,c)) ->
- (mkLambda (n,loop i p t,c))
- | ((P_TYPE :: p), LetIn (n,b,t,c)) ->
- (mkLetIn (n,b,loop i p t,c))
- | (p, _) ->
- failwith ("abstract_path " ^ string_of_int(List.length p))
- in
- loop 1 path t
-
-let occurrence sigma path (t : constr) =
- let rec loop p0 t = match (p0,EConstr.kind sigma t) with
- | (p, Cast (c,_,_)) -> loop p c
- | ([], _) -> t
- | ((P_APP n :: p), App (f,v)) -> loop p v.(pred n)
- | (p, Fix((_,n) ,(_,_,v))) -> loop p v.(n)
- | ((P_TYPE :: p), Prod (n,term,c)) -> loop p term
- | ((P_TYPE :: p), Lambda (n,term,c)) -> loop p term
- | ((P_TYPE :: p), LetIn (n,b,term,c)) -> loop p term
- | (p, _) ->
- failwith ("occurrence " ^ string_of_int(List.length p))
- in
- loop path t
-
-let abstract_path sigma typ path t =
- let term_occur = ref (mkRel 0) in
- let abstract = context sigma (fun i t -> term_occur:= t; mkRel i) path t in
- mkLambda (make_annot (Name (Id.of_string "x")) Sorts.Relevant, typ, abstract), !term_occur
-
-let focused_simpl path =
- let open Tacmach.New in
- Proofview.Goal.enter begin fun gl ->
- let newc = context (project gl) (fun i t -> pf_nf gl t) (List.rev path) (pf_concl gl) in
- convert_concl ~check:false newc DEFAULTcast
- end
-
-let focused_simpl path = focused_simpl path
-
-type oformula =
- | Oplus of oformula * oformula
- | Otimes of oformula * oformula
- | Oatom of Id.t
- | Oz of bigint
- | Oufo of constr
-
-let rec oprint = function
- | Oplus(t1,t2) ->
- print_string "("; oprint t1; print_string "+";
- oprint t2; print_string ")"
- | Otimes (t1,t2) ->
- print_string "("; oprint t1; print_string "*";
- oprint t2; print_string ")"
- | Oatom s -> print_string (Id.to_string s)
- | Oz i -> print_string (string_of_bigint i)
- | Oufo f -> print_string "?"
-
-let rec weight = function
- | Oatom c -> intern_id c
- | Oz _ -> -1
- | Otimes(c,_) -> weight c
- | Oplus _ -> failwith "weight"
- | Oufo _ -> -1
-
-let rec val_of = function
- | Oatom c -> mkVar c
- | Oz c -> mk_integer c
- | Otimes (t1,t2) -> mkApp (Lazy.force coq_Zmult, [| val_of t1; val_of t2 |])
- | Oplus(t1,t2) -> mkApp (Lazy.force coq_Zplus, [| val_of t1; val_of t2 |])
- | Oufo c -> c
-
-let compile name kind =
- let rec loop accu = function
- | Oplus(Otimes(Oatom v,Oz n),r) -> loop ({v=intern_id v; c=n} :: accu) r
- | Oz n ->
- let id = new_id () in
- tag_hypothesis name id;
- {kind = kind; body = List.rev accu; constant = n; id = id}
- | _ -> anomaly (Pp.str "compile_equation.")
- in
- loop []
-
-let decompile af =
- let rec loop = function
- | ({v=v; c=n}::r) -> Oplus(Otimes(Oatom (unintern_id v),Oz n),loop r)
- | [] -> Oz af.constant
- in
- loop af.body
-
-(** Backward compat to emulate the old Refine: normalize the goal conclusion *)
-let new_hole env sigma c =
- let c = Reductionops.nf_betaiota env sigma c in
- Evarutil.new_evar env sigma c
-
-let clever_rewrite_base_poly typ p result theorem =
- let open Tacmach.New in
- Proofview.Goal.enter begin fun gl ->
- let full = pf_concl gl in
- let env = pf_env gl in
- let (abstracted,occ) = abstract_path (project gl) typ (List.rev p) full in
- Refine.refine ~typecheck:false begin fun sigma ->
- let t =
- applist
- (mkLambda
- (make_annot (Name (Id.of_string "P")) Sorts.Relevant,
- mkArrow typ Sorts.Relevant mkProp,
- mkLambda
- (make_annot (Name (Id.of_string "H")) Sorts.Relevant,
- applist (mkRel 1,[result]),
- mkApp (Lazy.force coq_eq_ind_r,
- [| typ; result; mkRel 2; mkRel 1; occ; theorem |]))),
- [abstracted])
- in
- let argt = mkApp (abstracted, [|result|]) in
- let (sigma, hole) = new_hole env sigma argt in
- (sigma, applist (t, [hole]))
- end
- end
-
-let clever_rewrite_base p result theorem =
- clever_rewrite_base_poly (Lazy.force coq_Z) p result theorem
-
-let clever_rewrite_base_nat p result theorem =
- clever_rewrite_base_poly (Lazy.force coq_nat) p result theorem
-
-let clever_rewrite_gen p result (t,args) =
- let theorem = applist(t, args) in
- clever_rewrite_base p result theorem
-
-let clever_rewrite_gen_nat p result (t,args) =
- let theorem = applist(t, args) in
- clever_rewrite_base_nat p result theorem
-
-(** Solve using the term the term [t _] *)
-let refine_app gl t =
- let open Tacmach.New in
- Refine.refine ~typecheck:false begin fun sigma ->
- let env = pf_env gl in
- let ht = match EConstr.kind sigma (pf_get_type_of gl t) with
- | Prod (_, t, _) -> t
- | _ -> assert false
- in
- let (sigma, hole) = new_hole env sigma ht in
- (sigma, applist (t, [hole]))
- end
-
-let clever_rewrite p vpath t =
- let open Tacmach.New in
- Proofview.Goal.enter begin fun gl ->
- let full = pf_concl gl in
- let (abstracted,occ) = abstract_path (project gl) (Lazy.force coq_Z) (List.rev p) full in
- let vargs = List.map (fun p -> occurrence (project gl) p occ) vpath in
- let t' = applist(t, (vargs @ [abstracted])) in
- refine_app gl t'
- end
-
-(** simpl_coeffs :
- The subterm at location [path_init] in the current goal should
- look like [(v1*c1 + (v2*c2 + ... (vn*cn + k)))], and we reduce
- via "simpl" each [ci] and the final constant [k].
- The path [path_k] gives the location of constant [k].
- Earlier, the whole was a mere call to [focused_simpl],
- leading to reduction inside the atoms [vi], which is bad,
- for instance when the atom is an evaluable definition
- (see #4132). *)
-
-let simpl_coeffs path_init path_k =
- Proofview.Goal.enter begin fun gl ->
- let sigma = project gl in
- let rec loop n t =
- if Int.equal n 0 then pf_nf gl t
- else
- (* t should be of the form ((v * c) + ...) *)
- match EConstr.kind sigma t with
- | App(f,[|t1;t2|]) ->
- (match EConstr.kind sigma t1 with
- | App (g,[|v;c|]) ->
- let c' = pf_nf gl c in
- let t2' = loop (pred n) t2 in
- mkApp (f,[|mkApp (g,[|v;c'|]);t2'|])
- | _ -> assert false)
- | _ -> assert false
- in
- let n = Util.(-) (List.length path_k) (List.length path_init) in
- let newc = context sigma (fun _ t -> loop n t) (List.rev path_init) (pf_concl gl)
- in
- convert_concl ~check:false newc DEFAULTcast
- end
-
-let rec shuffle p (t1,t2) =
- match t1,t2 with
- | Oplus(l1,r1), Oplus(l2,r2) ->
- if weight l1 > weight l2 then
- let (tac,t') = shuffle (P_APP 2 :: p) (r1,t2) in
- (clever_rewrite p [[P_APP 1;P_APP 1];
- [P_APP 1; P_APP 2];[P_APP 2]]
- (Lazy.force coq_fast_Zplus_assoc_reverse)
- :: tac,
- Oplus(l1,t'))
- else
- let (tac,t') = shuffle (P_APP 2 :: p) (t1,r2) in
- (clever_rewrite p [[P_APP 1];[P_APP 2;P_APP 1];[P_APP 2;P_APP 2]]
- (Lazy.force coq_fast_Zplus_permute)
- :: tac,
- Oplus(l2,t'))
- | Oplus(l1,r1), t2 ->
- if weight l1 > weight t2 then
- let (tac,t') = shuffle (P_APP 2 :: p) (r1,t2) in
- clever_rewrite p [[P_APP 1;P_APP 1]; [P_APP 1; P_APP 2];[P_APP 2]]
- (Lazy.force coq_fast_Zplus_assoc_reverse)
- :: tac,
- Oplus(l1, t')
- else
- [clever_rewrite p [[P_APP 1];[P_APP 2]]
- (Lazy.force coq_fast_Zplus_comm)],
- Oplus(t2,t1)
- | t1,Oplus(l2,r2) ->
- if weight l2 > weight t1 then
- let (tac,t') = shuffle (P_APP 2 :: p) (t1,r2) in
- clever_rewrite p [[P_APP 1];[P_APP 2;P_APP 1];[P_APP 2;P_APP 2]]
- (Lazy.force coq_fast_Zplus_permute)
- :: tac,
- Oplus(l2,t')
- else [],Oplus(t1,t2)
- | Oz t1,Oz t2 ->
- [focused_simpl p], Oz(Z.add t1 t2)
- | t1,t2 ->
- if weight t1 < weight t2 then
- [clever_rewrite p [[P_APP 1];[P_APP 2]]
- (Lazy.force coq_fast_Zplus_comm)],
- Oplus(t2,t1)
- else [],Oplus(t1,t2)
-
-let shuffle_mult p_init k1 e1 k2 e2 =
- let rec loop p = function
- | (({c=c1;v=v1}::l1) as l1'),(({c=c2;v=v2}::l2) as l2') ->
- if Int.equal v1 v2 then
- let tac =
- clever_rewrite p [[P_APP 1; P_APP 1; P_APP 1; P_APP 1];
- [P_APP 1; P_APP 1; P_APP 1; P_APP 2];
- [P_APP 2; P_APP 1; P_APP 1; P_APP 2];
- [P_APP 1; P_APP 1; P_APP 2];
- [P_APP 2; P_APP 1; P_APP 2];
- [P_APP 1; P_APP 2];
- [P_APP 2; P_APP 2]]
- (Lazy.force coq_fast_OMEGA10)
- in
- if Z.add (Z.mul k1 c1) (Z.mul k2 c2) =? zero then
- let tac' =
- clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 2]]
- (Lazy.force coq_fast_Zred_factor5) in
- tac :: focused_simpl (P_APP 2::P_APP 1:: p) :: tac' ::
- loop p (l1,l2)
- else tac :: loop (P_APP 2 :: p) (l1,l2)
- else if v1 > v2 then
- clever_rewrite p [[P_APP 1; P_APP 1; P_APP 1; P_APP 1];
- [P_APP 1; P_APP 1; P_APP 1; P_APP 2];
- [P_APP 1; P_APP 1; P_APP 2];
- [P_APP 2];
- [P_APP 1; P_APP 2]]
- (Lazy.force coq_fast_OMEGA11) ::
- loop (P_APP 2 :: p) (l1,l2')
- else
- clever_rewrite p [[P_APP 2; P_APP 1; P_APP 1; P_APP 1];
- [P_APP 2; P_APP 1; P_APP 1; P_APP 2];
- [P_APP 1];
- [P_APP 2; P_APP 1; P_APP 2];
- [P_APP 2; P_APP 2]]
- (Lazy.force coq_fast_OMEGA12) ::
- loop (P_APP 2 :: p) (l1',l2)
- | ({c=c1;v=v1}::l1), [] ->
- clever_rewrite p [[P_APP 1; P_APP 1; P_APP 1; P_APP 1];
- [P_APP 1; P_APP 1; P_APP 1; P_APP 2];
- [P_APP 1; P_APP 1; P_APP 2];
- [P_APP 2];
- [P_APP 1; P_APP 2]]
- (Lazy.force coq_fast_OMEGA11) ::
- loop (P_APP 2 :: p) (l1,[])
- | [],({c=c2;v=v2}::l2) ->
- clever_rewrite p [[P_APP 2; P_APP 1; P_APP 1; P_APP 1];
- [P_APP 2; P_APP 1; P_APP 1; P_APP 2];
- [P_APP 1];
- [P_APP 2; P_APP 1; P_APP 2];
- [P_APP 2; P_APP 2]]
- (Lazy.force coq_fast_OMEGA12) ::
- loop (P_APP 2 :: p) ([],l2)
- | [],[] -> [simpl_coeffs p_init p]
- in
- loop p_init (e1,e2)
-
-let shuffle_mult_right p_init e1 k2 e2 =
- let rec loop p = function
- | (({c=c1;v=v1}::l1) as l1'),(({c=c2;v=v2}::l2) as l2') ->
- if Int.equal v1 v2 then
- let tac =
- clever_rewrite p
- [[P_APP 1; P_APP 1; P_APP 1];
- [P_APP 1; P_APP 1; P_APP 2];
- [P_APP 2; P_APP 1; P_APP 1; P_APP 2];
- [P_APP 1; P_APP 2];
- [P_APP 2; P_APP 1; P_APP 2];
- [P_APP 2; P_APP 2]]
- (Lazy.force coq_fast_OMEGA15)
- in
- if Z.add c1 (Z.mul k2 c2) =? zero then
- let tac' =
- clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 2]]
- (Lazy.force coq_fast_Zred_factor5)
- in
- tac :: focused_simpl (P_APP 2::P_APP 1:: p) :: tac' ::
- loop p (l1,l2)
- else tac :: loop (P_APP 2 :: p) (l1,l2)
- else if v1 > v2 then
- clever_rewrite p [[P_APP 1;P_APP 1]; [P_APP 1; P_APP 2];[P_APP 2]]
- (Lazy.force coq_fast_Zplus_assoc_reverse) ::
- loop (P_APP 2 :: p) (l1,l2')
- else
- clever_rewrite p [[P_APP 2; P_APP 1; P_APP 1; P_APP 1];
- [P_APP 2; P_APP 1; P_APP 1; P_APP 2];
- [P_APP 1];
- [P_APP 2; P_APP 1; P_APP 2];
- [P_APP 2; P_APP 2]]
- (Lazy.force coq_fast_OMEGA12) ::
- loop (P_APP 2 :: p) (l1',l2)
- | ({c=c1;v=v1}::l1), [] ->
- clever_rewrite p [[P_APP 1;P_APP 1]; [P_APP 1; P_APP 2];[P_APP 2]]
- (Lazy.force coq_fast_Zplus_assoc_reverse) ::
- loop (P_APP 2 :: p) (l1,[])
- | [],({c=c2;v=v2}::l2) ->
- clever_rewrite p [[P_APP 2; P_APP 1; P_APP 1; P_APP 1];
- [P_APP 2; P_APP 1; P_APP 1; P_APP 2];
- [P_APP 1];
- [P_APP 2; P_APP 1; P_APP 2];
- [P_APP 2; P_APP 2]]
- (Lazy.force coq_fast_OMEGA12) ::
- loop (P_APP 2 :: p) ([],l2)
- | [],[] -> [simpl_coeffs p_init p]
- in
- loop p_init (e1,e2)
-
-let rec shuffle_cancel p = function
- | [] -> [focused_simpl p]
- | ({c=c1}::l1) ->
- let tac =
- clever_rewrite p [[P_APP 1; P_APP 1; P_APP 1];[P_APP 1; P_APP 2];
- [P_APP 2; P_APP 2];
- [P_APP 1; P_APP 1; P_APP 2; P_APP 1]]
- (if c1 >? zero then
- (Lazy.force coq_fast_OMEGA13)
- else
- (Lazy.force coq_fast_OMEGA14))
- in
- tac :: shuffle_cancel p l1
-
-let rec scalar p n = function
- | Oplus(t1,t2) ->
- let tac1,t1' = scalar (P_APP 1 :: p) n t1 and
- tac2,t2' = scalar (P_APP 2 :: p) n t2 in
- clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 1;P_APP 2];[P_APP 2]]
- (Lazy.force coq_fast_Zmult_plus_distr_l) ::
- (tac1 @ tac2), Oplus(t1',t2')
- | Otimes(t1,Oz x) ->
- [clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 1;P_APP 2];[P_APP 2]]
- (Lazy.force coq_fast_Zmult_assoc_reverse);
- focused_simpl (P_APP 2 :: p)],
- Otimes(t1,Oz (n*x))
- | Otimes(t1,t2) -> CErrors.user_err Pp.(str "Omega: Can't solve a goal with non-linear products")
- | (Oatom _ as t) -> [], Otimes(t,Oz n)
- | Oz i -> [focused_simpl p],Oz(n*i)
- | Oufo c -> [], Oufo (mkApp (Lazy.force coq_Zmult, [| mk_integer n; c |]))
-
-let scalar_norm p_init =
- let rec loop p = function
- | [] -> [simpl_coeffs p_init p]
- | (_::l) ->
- clever_rewrite p
- [[P_APP 1; P_APP 1; P_APP 1];[P_APP 1; P_APP 1; P_APP 2];
- [P_APP 1; P_APP 2];[P_APP 2]]
- (Lazy.force coq_fast_OMEGA16) :: loop (P_APP 2 :: p) l
- in
- loop p_init
-
-let norm_add p_init =
- let rec loop p = function
- | [] -> [simpl_coeffs p_init p]
- | _:: l ->
- clever_rewrite p [[P_APP 1;P_APP 1]; [P_APP 1; P_APP 2];[P_APP 2]]
- (Lazy.force coq_fast_Zplus_assoc_reverse) ::
- loop (P_APP 2 :: p) l
- in
- loop p_init
-
-let scalar_norm_add p_init =
- let rec loop p = function
- | [] -> [simpl_coeffs p_init p]
- | _ :: l ->
- clever_rewrite p
- [[P_APP 1; P_APP 1; P_APP 1; P_APP 1];
- [P_APP 1; P_APP 1; P_APP 1; P_APP 2];
- [P_APP 1; P_APP 1; P_APP 2]; [P_APP 2]; [P_APP 1; P_APP 2]]
- (Lazy.force coq_fast_OMEGA11) :: loop (P_APP 2 :: p) l
- in
- loop p_init
-
-let rec negate p = function
- | Oplus(t1,t2) ->
- let tac1,t1' = negate (P_APP 1 :: p) t1 and
- tac2,t2' = negate (P_APP 2 :: p) t2 in
- clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 1;P_APP 2]]
- (Lazy.force coq_fast_Zopp_plus_distr) ::
- (tac1 @ tac2),
- Oplus(t1',t2')
- | Otimes(t1,Oz x) ->
- [clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 1;P_APP 2]]
- (Lazy.force coq_fast_Zopp_mult_distr_r);
- focused_simpl (P_APP 2 :: p)], Otimes(t1,Oz (neg x))
- | Otimes(t1,t2) -> CErrors.user_err Pp.(str "Omega: Can't solve a goal with non-linear products")
- | (Oatom _ as t) ->
- let r = Otimes(t,Oz(negone)) in
- [clever_rewrite p [[P_APP 1]] (Lazy.force coq_fast_Zopp_eq_mult_neg_1)], r
- | Oz i -> [focused_simpl p],Oz(neg i)
- | Oufo c -> [], Oufo (mkApp (Lazy.force coq_Zopp, [| c |]))
-
-let rec transform sigma p t =
- let default isnat t' =
- try
- let v,th,_ = find_constr sigma t' in
- [clever_rewrite_base p (mkVar v) (mkVar th)], Oatom v
- with e when CErrors.noncritical e ->
- let v = new_identifier_var ()
- and th = new_identifier () in
- hide_constr t' v th isnat;
- [clever_rewrite_base p (mkVar v) (mkVar th)], Oatom v
- in
- try match destructurate_term sigma t with
- | Kapp(Zplus,[t1;t2]) ->
- let tac1,t1' = transform sigma (P_APP 1 :: p) t1
- and tac2,t2' = transform sigma (P_APP 2 :: p) t2 in
- let tac,t' = shuffle p (t1',t2') in
- tac1 @ tac2 @ tac, t'
- | Kapp(Zminus,[t1;t2]) ->
- let tac,t =
- transform sigma p
- (mkApp (Lazy.force coq_Zplus,
- [| t1; (mkApp (Lazy.force coq_Zopp, [| t2 |])) |])) in
- unfold sp_Zminus :: tac,t
- | Kapp(Zsucc,[t1]) ->
- let tac,t = transform sigma p (mkApp (Lazy.force coq_Zplus,
- [| t1; mk_integer one |])) in
- unfold sp_Zsucc :: tac,t
- | Kapp(Zpred,[t1]) ->
- let tac,t = transform sigma p (mkApp (Lazy.force coq_Zplus,
- [| t1; mk_integer negone |])) in
- unfold sp_Zpred :: tac,t
- | Kapp(Zmult,[t1;t2]) ->
- let tac1,t1' = transform sigma (P_APP 1 :: p) t1
- and tac2,t2' = transform sigma (P_APP 2 :: p) t2 in
- begin match t1',t2' with
- | (_,Oz n) -> let tac,t' = scalar p n t1' in tac1 @ tac2 @ tac,t'
- | (Oz n,_) ->
- let sym =
- clever_rewrite p [[P_APP 1];[P_APP 2]]
- (Lazy.force coq_fast_Zmult_comm) in
- let tac,t' = scalar p n t2' in tac1 @ tac2 @ (sym :: tac),t'
- | _ -> default false t
- end
- | Kapp((Zpos|Zneg|Z0),_) ->
- (try ([],Oz(recognize_number sigma t))
- with e when CErrors.noncritical e -> default false t)
- | Kvar s -> [],Oatom s
- | Kapp(Zopp,[t]) ->
- let tac,t' = transform sigma (P_APP 1 :: p) t in
- let tac',t'' = negate p t' in
- tac @ tac', t''
- | Kapp(Z_of_nat,[t']) -> default true t'
- | _ -> default false t
- with e when noncritical e -> default false t
-
-let shrink_pair p f1 f2 =
- match f1,f2 with
- | Oatom v,Oatom _ ->
- let r = Otimes(Oatom v,Oz two) in
- clever_rewrite p [[P_APP 1]] (Lazy.force coq_fast_Zred_factor1), r
- | Oatom v, Otimes(_,c2) ->
- let r = Otimes(Oatom v,Oplus(c2,Oz one)) in
- clever_rewrite p [[P_APP 1];[P_APP 2;P_APP 2]]
- (Lazy.force coq_fast_Zred_factor2), r
- | Otimes (v1,c1),Oatom v ->
- let r = Otimes(Oatom v,Oplus(c1,Oz one)) in
- clever_rewrite p [[P_APP 2];[P_APP 1;P_APP 2]]
- (Lazy.force coq_fast_Zred_factor3), r
- | Otimes (Oatom v,c1),Otimes (v2,c2) ->
- let r = Otimes(Oatom v,Oplus(c1,c2)) in
- clever_rewrite p
- [[P_APP 1;P_APP 1];[P_APP 1;P_APP 2];[P_APP 2;P_APP 2]]
- (Lazy.force coq_fast_Zred_factor4),r
- | t1,t2 ->
- begin
- oprint t1; print_newline (); oprint t2; print_newline ();
- flush stdout; CErrors.user_err Pp.(str "shrink.1")
- end
-
-let reduce_factor p = function
- | Oatom v ->
- let r = Otimes(Oatom v,Oz one) in
- [clever_rewrite p [[]] (Lazy.force coq_fast_Zred_factor0)],r
- | Otimes(Oatom v,Oz n) as f -> [],f
- | Otimes(Oatom v,c) ->
- let rec compute = function
- | Oz n -> n
- | Oplus(t1,t2) -> Z.add (compute t1) (compute t2)
- | _ -> CErrors.user_err Pp.(str "condense.1")
- in
- [focused_simpl (P_APP 2 :: p)], Otimes(Oatom v,Oz(compute c))
- | t -> oprint t; CErrors.user_err Pp.(str "reduce_factor.1")
-
-let rec condense p = function
- | Oplus(f1,(Oplus(f2,r) as t)) ->
- if Int.equal (weight f1) (weight f2) then begin
- let shrink_tac,t = shrink_pair (P_APP 1 :: p) f1 f2 in
- let assoc_tac =
- clever_rewrite p
- [[P_APP 1];[P_APP 2;P_APP 1];[P_APP 2;P_APP 2]]
- (Lazy.force coq_fast_Zplus_assoc) in
- let tac_list,t' = condense p (Oplus(t,r)) in
- (assoc_tac :: shrink_tac :: tac_list), t'
- end else begin
- let tac,f = reduce_factor (P_APP 1 :: p) f1 in
- let tac',t' = condense (P_APP 2 :: p) t in
- (tac @ tac'), Oplus(f,t')
- end
- | Oplus(f1,Oz n) ->
- let tac,f1' = reduce_factor (P_APP 1 :: p) f1 in tac,Oplus(f1',Oz n)
- | Oplus(f1,f2) ->
- if Int.equal (weight f1) (weight f2) then begin
- let tac_shrink,t = shrink_pair p f1 f2 in
- let tac,t' = condense p t in
- tac_shrink :: tac,t'
- end else begin
- let tac,f = reduce_factor (P_APP 1 :: p) f1 in
- let tac',t' = condense (P_APP 2 :: p) f2 in
- (tac @ tac'),Oplus(f,t')
- end
- | Oz _ as t -> [],t
- | t ->
- let tac,t' = reduce_factor p t in
- let final = Oplus(t',Oz zero) in
- let tac' = clever_rewrite p [[]] (Lazy.force coq_fast_Zred_factor6) in
- tac @ [tac'], final
-
-let rec clear_zero p = function
- | Oplus(Otimes(Oatom v,Oz n),r) when n =? zero ->
- let tac =
- clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 2]]
- (Lazy.force coq_fast_Zred_factor5) in
- let tac',t = clear_zero p r in
- tac :: tac',t
- | Oplus(f,r) ->
- let tac,t = clear_zero (P_APP 2 :: p) r in tac,Oplus(f,t)
- | t -> [],t
-
-open Proofview
-open Proofview.Notations
-
-let replay_history tactic_normalisation =
- let aux = Id.of_string "auxiliary" in
- let aux1 = Id.of_string "auxiliary_1" in
- let aux2 = Id.of_string "auxiliary_2" in
- let izero = mk_integer zero in
- let rec loop t : unit Proofview.tactic =
- match t with
- | HYP e :: l ->
- begin
- try
- tclTHEN
- (Id.List.assoc (hyp_of_tag e.id) tactic_normalisation)
- (loop l)
- with Not_found -> loop l end
- | NEGATE_CONTRADICT (e2,e1,b) :: l ->
- let eq1 = decompile e1
- and eq2 = decompile e2 in
- let id1 = hyp_of_tag e1.id
- and id2 = hyp_of_tag e2.id in
- let k = if b then negone else one in
- let p_initial = [P_APP 1;P_TYPE] in
- let tac= shuffle_mult_right p_initial e1.body k e2.body in
- tclTHENLIST [
- generalize_tac
- [mkApp (Lazy.force coq_OMEGA17, [|
- val_of eq1;
- val_of eq2;
- mk_integer k;
- mkVar id1; mkVar id2 |])];
- mk_then tac;
- intro_using_then aux (fun aux ->
- resolve_id aux);
- reflexivity
- ]
- | CONTRADICTION (e1,e2) :: l ->
- let eq1 = decompile e1
- and eq2 = decompile e2 in
- let p_initial = [P_APP 2;P_TYPE] in
- let tac = shuffle_cancel p_initial e1.body in
- let solve_le =
- let not_sup_sup = mkApp (Lazy.force coq_eq,
- [|
- Lazy.force coq_comparison;
- Lazy.force coq_Gt;
- Lazy.force coq_Gt |])
- in
- tclTHENS
- (tclTHENLIST [
- unfold sp_Zle;
- simpl_in_concl;
- intro;
- (absurd not_sup_sup) ])
- [ assumption ; reflexivity ]
- in
- let theorem =
- mkApp (Lazy.force coq_OMEGA2, [|
- val_of eq1; val_of eq2;
- mkVar (hyp_of_tag e1.id);
- mkVar (hyp_of_tag e2.id) |])
- in
- Proofview.tclTHEN (tclTHEN (generalize_tac [theorem]) (mk_then tac)) solve_le
- | DIVIDE_AND_APPROX (e1,e2,k,d) :: l ->
- let id = hyp_of_tag e1.id in
- let eq1 = val_of(decompile e1)
- and eq2 = val_of(decompile e2) in
- let kk = mk_integer k
- and dd = mk_integer d in
- let rhs = mk_plus (mk_times eq2 kk) dd in
- let state_eg = mk_eq eq1 rhs in
- let tac = scalar_norm_add [P_APP 3] e2.body in
- tclTHENS
- (cut state_eg)
- [ tclTHENS
- (intro_using_then aux (fun aux ->
- tclTHENLIST [
- (generalize_tac
- [mkApp (Lazy.force coq_OMEGA1,
- [| eq1; rhs; mkVar aux; mkVar id |])]);
- (clear [aux;id]);
- (intro_mustbe_force id);
- (cut (mk_gt kk dd)) ]))
- [ tclTHENS
- (cut (mk_gt kk izero))
- [ intro_using_then aux1 (fun aux1 ->
- intro_using_then aux2 (fun aux2 ->
- tclTHENLIST [
- (generalize_tac
- [mkApp (Lazy.force coq_Zmult_le_approx,
- [| kk;eq2;dd;mkVar aux1;mkVar aux2; mkVar id |])]);
- (clear [aux1;aux2;id]);
- (intro_mustbe_force id);
- (loop l) ]));
- tclTHENLIST [
- (unfold sp_Zgt);
- simpl_in_concl;
- reflexivity ] ];
- tclTHENLIST [ unfold sp_Zgt; simpl_in_concl; reflexivity ]
- ];
- tclTHEN (mk_then tac) reflexivity ]
-
- | NOT_EXACT_DIVIDE (e1,k) :: l ->
- let c = floor_div e1.constant k in
- let d = Z.sub e1.constant (Z.mul c k) in
- let e2 = {id=e1.id; kind=EQUA;constant = c;
- body = map_eq_linear (fun c -> c / k) e1.body } in
- let eq2 = val_of(decompile e2) in
- let kk = mk_integer k
- and dd = mk_integer d in
- let tac = scalar_norm_add [P_APP 2] e2.body in
- tclTHENS
- (cut (mk_gt dd izero))
- [ tclTHENS (cut (mk_gt kk dd))
- [ intro_using_then aux2 (fun aux2 ->
- intro_using_then aux1 (fun aux1 ->
- tclTHENLIST [
- (generalize_tac
- [mkApp (Lazy.force coq_OMEGA4,
- [| dd;kk;eq2;mkVar aux1; mkVar aux2 |])]);
- (clear [aux1;aux2]);
- unfold sp_not;
- intro_using_then aux (fun aux ->
- tclTHENLIST [
- resolve_id aux;
- mk_then tac;
- assumption
- ])])) ;
- tclTHENLIST [
- unfold sp_Zgt;
- simpl_in_concl;
- reflexivity ] ];
- tclTHENLIST [
- unfold sp_Zgt;
- simpl_in_concl;
- reflexivity ] ]
- | EXACT_DIVIDE (e1,k) :: l ->
- let id = hyp_of_tag e1.id in
- let e2 = map_eq_afine (fun c -> c / k) e1 in
- let eq1 = val_of(decompile e1)
- and eq2 = val_of(decompile e2) in
- let kk = mk_integer k in
- let state_eq = mk_eq eq1 (mk_times eq2 kk) in
- if e1.kind == DISE then
- let tac = scalar_norm [P_APP 3] e2.body in
- tclTHENS
- (cut state_eq)
- [ intro_using_then aux1 (fun aux1 ->
- tclTHENLIST [
- (generalize_tac
- [mkApp (Lazy.force coq_OMEGA18,
- [| eq1;eq2;kk;mkVar aux1; mkVar id |])]);
- (clear [aux1;id]);
- (intro_mustbe_force id);
- (loop l) ]);
- tclTHEN (mk_then tac) reflexivity ]
- else
- let tac = scalar_norm [P_APP 3] e2.body in
- tclTHENS (cut state_eq)
- [
- tclTHENS
- (cut (mk_gt kk izero))
- [ intro_using_then aux2 (fun aux2 ->
- intro_using_then aux1 (fun aux1 ->
- tclTHENLIST [
- (generalize_tac
- [mkApp (Lazy.force coq_OMEGA3,
- [| eq1; eq2; kk; mkVar aux2; mkVar aux1;mkVar id|])]);
- (clear [aux1;aux2;id]);
- (intro_mustbe_force id);
- (loop l) ]));
- tclTHENLIST [
- unfold sp_Zgt;
- simpl_in_concl;
- reflexivity ] ];
- tclTHEN (mk_then tac) reflexivity ]
- | (MERGE_EQ(e3,e1,e2)) :: l ->
- let id = new_identifier () in
- tag_hypothesis id e3;
- let id1 = hyp_of_tag e1.id
- and id2 = hyp_of_tag e2 in
- let eq1 = val_of(decompile e1)
- and eq2 = val_of (decompile (negate_eq e1)) in
- let tac =
- clever_rewrite [P_APP 3] [[P_APP 1]]
- (Lazy.force coq_fast_Zopp_eq_mult_neg_1) ::
- scalar_norm [P_APP 3] e1.body
- in
- tclTHENS
- (cut (mk_eq eq1 (mk_inv eq2)))
- [ intro_using_then aux (fun aux ->
- tclTHENLIST [
- (generalize_tac
- [mkApp (Lazy.force coq_OMEGA8, [| eq1;eq2;mkVar id1;mkVar id2; mkVar aux|])]);
- (clear [id1;id2;aux]);
- (intro_mustbe_force id);
- (loop l) ]);
- tclTHEN (mk_then tac) reflexivity]
-
- | STATE {st_new_eq=e;st_def=def;st_orig=orig;st_coef=m;st_var=v} :: l ->
- let id = new_identifier ()
- and id2 = hyp_of_tag orig.id in
- tag_hypothesis id e.id;
- let eq1 = val_of(decompile def)
- and eq2 = val_of(decompile orig) in
- let vid = unintern_id v in
- let theorem =
- mkApp (Lazy.force coq_ex, [|
- Lazy.force coq_Z;
- mkLambda
- (make_annot (Name vid) Sorts.Relevant,
- Lazy.force coq_Z,
- mk_eq (mkRel 1) eq1) |])
- in
- let mm = mk_integer m in
- let p_initial = [P_APP 2;P_TYPE] in
- let tac =
- clever_rewrite (P_APP 1 :: P_APP 1 :: P_APP 2 :: p_initial)
- [[P_APP 1]] (Lazy.force coq_fast_Zopp_eq_mult_neg_1) ::
- shuffle_mult_right p_initial
- orig.body m ({c= negone;v= v}::def.body) in
- tclTHENS
- (cut theorem)
- [ tclTHENLIST [ intro_using_then aux (fun aux ->
- (elim_id aux) <*>
- (clear [aux]));
- intro_using_then vid (fun vid ->
- intro_using_then aux (fun aux ->
- tclTHENLIST [
- (generalize_tac
- [mkApp (Lazy.force coq_OMEGA9,
- [| mkVar vid;eq2;eq1;mm; mkVar id2;mkVar aux |])]);
- mk_then tac;
- (clear [aux]);
- (intro_mustbe_force id);
- (loop l) ]))];
- tclTHEN (exists_tac eq1) reflexivity ]
- | SPLIT_INEQ(e,(e1,act1),(e2,act2)) :: l ->
- let id1 = new_identifier ()
- and id2 = new_identifier () in
- tag_hypothesis id1 e1; tag_hypothesis id2 e2;
- let id = hyp_of_tag e.id in
- let tac1 = norm_add [P_APP 2;P_TYPE] e.body in
- let tac2 = scalar_norm_add [P_APP 2;P_TYPE] e.body in
- let eq = val_of(decompile e) in
- tclTHENS
- (simplest_elim (applist (Lazy.force coq_OMEGA19, [eq; mkVar id])))
- [tclTHENLIST [ mk_then tac1; (intro_mustbe_force id1); (loop act1) ];
- tclTHENLIST [ mk_then tac2; (intro_mustbe_force id2); (loop act2) ]]
- | SUM(e3,(k1,e1),(k2,e2)) :: l ->
- let id = new_identifier () in
- tag_hypothesis id e3;
- let id1 = hyp_of_tag e1.id
- and id2 = hyp_of_tag e2.id in
- let eq1 = val_of(decompile e1)
- and eq2 = val_of(decompile e2) in
- if k1 =? one && e2.kind == EQUA then
- let tac_thm =
- match e1.kind with
- | EQUA -> Lazy.force coq_OMEGA5
- | INEQ -> Lazy.force coq_OMEGA6
- | DISE -> Lazy.force coq_OMEGA20
- in
- let kk = mk_integer k2 in
- let p_initial =
- if e1.kind == DISE then [P_APP 1; P_TYPE] else [P_APP 2; P_TYPE] in
- let tac = shuffle_mult_right p_initial e1.body k2 e2.body in
- tclTHENLIST [
- (generalize_tac
- [mkApp (tac_thm, [| eq1; eq2; kk; mkVar id1; mkVar id2 |])]);
- mk_then tac;
- (intro_mustbe_force id);
- (loop l)
- ]
- else
- let kk1 = mk_integer k1
- and kk2 = mk_integer k2 in
- let p_initial = [P_APP 2;P_TYPE] in
- let tac= shuffle_mult p_initial k1 e1.body k2 e2.body in
- tclTHENS (cut (mk_gt kk1 izero))
- [tclTHENS
- (cut (mk_gt kk2 izero))
- [ intro_using_then aux2 (fun aux2 ->
- intro_using_then aux1 (fun aux1 ->
- tclTHENLIST [
- (generalize_tac
- [mkApp (Lazy.force coq_OMEGA7, [|
- eq1;eq2;kk1;kk2;
- mkVar aux1;mkVar aux2;
- mkVar id1;mkVar id2 |])]);
- (clear [aux1;aux2]);
- mk_then tac;
- (intro_mustbe_force id);
- (loop l) ]));
- tclTHENLIST [
- unfold sp_Zgt;
- simpl_in_concl;
- reflexivity ] ];
- tclTHENLIST [
- unfold sp_Zgt;
- simpl_in_concl;
- reflexivity ] ]
- | CONSTANT_NOT_NUL(e,k) :: l ->
- tclTHEN ((generalize_tac [mkVar (hyp_of_tag e)])) Equality.discrConcl
- | CONSTANT_NUL(e) :: l ->
- tclTHEN (resolve_id (hyp_of_tag e)) reflexivity
- | CONSTANT_NEG(e,k) :: l ->
- tclTHENLIST [
- (generalize_tac [mkVar (hyp_of_tag e)]);
- unfold sp_Zle;
- simpl_in_concl;
- unfold sp_not;
- intro_using_then aux (fun aux ->
- resolve_id aux <*> reflexivity)
- ]
- | _ -> Proofview.tclUNIT ()
- in
- loop
-
-let normalize sigma p_initial t =
- let (tac,t') = transform sigma p_initial t in
- let (tac',t'') = condense p_initial t' in
- let (tac'',t''') = clear_zero p_initial t'' in
- tac @ tac' @ tac'' , t'''
-
-let normalize_equation sigma id flag theorem pos t t1 t2 (tactic,defs) =
- let p_initial = [P_APP pos ;P_TYPE] in
- let (tac,t') = normalize sigma p_initial t in
- let shift_left =
- tclTHEN
- (generalize_tac [mkApp (theorem, [| t1; t2; mkVar id |]) ])
- (tclTRY (clear [id]))
- in
- if not (List.is_empty tac) then
- let id' = new_identifier () in
- ((id',(tclTHENLIST [ shift_left; mk_then tac; (intro_mustbe_force id') ]))
- :: tactic,
- compile id' flag t' :: defs)
- else
- (tactic,defs)
-
-let destructure_omega env sigma tac_def (id,c) =
- if String.equal (atompart_of_id id) "State" then
- tac_def
- else
- try match destructurate_prop sigma c with
- | Kapp(Eq,[typ;t1;t2])
- when begin match destructurate_type env sigma typ with Kapp(Z,[]) -> true | _ -> false end ->
- let t = mk_plus t1 (mk_inv t2) in
- normalize_equation sigma
- id EQUA (Lazy.force coq_Zegal_left) 2 t t1 t2 tac_def
- | Kapp(Zne,[t1;t2]) ->
- let t = mk_plus t1 (mk_inv t2) in
- normalize_equation sigma
- id DISE (Lazy.force coq_Zne_left) 1 t t1 t2 tac_def
- | Kapp(Zle,[t1;t2]) ->
- let t = mk_plus t2 (mk_inv t1) in
- normalize_equation sigma
- id INEQ (Lazy.force coq_Zle_left) 2 t t1 t2 tac_def
- | Kapp(Zlt,[t1;t2]) ->
- let t = mk_plus (mk_plus t2 (mk_integer negone)) (mk_inv t1) in
- normalize_equation sigma
- id INEQ (Lazy.force coq_Zlt_left) 2 t t1 t2 tac_def
- | Kapp(Zge,[t1;t2]) ->
- let t = mk_plus t1 (mk_inv t2) in
- normalize_equation sigma
- id INEQ (Lazy.force coq_Zge_left) 2 t t1 t2 tac_def
- | Kapp(Zgt,[t1;t2]) ->
- let t = mk_plus (mk_plus t1 (mk_integer negone)) (mk_inv t2) in
- normalize_equation sigma
- id INEQ (Lazy.force coq_Zgt_left) 2 t t1 t2 tac_def
- | _ -> tac_def
- with e when noncritical e -> tac_def
-
-let reintroduce id =
- (* [id] cannot be cleared if dependent: protect it by a try *)
- tclTHEN (tclTRY (clear [id])) (intro_using_then id (fun _ -> tclUNIT()))
-
-let coq_omega =
- Proofview.Goal.enter begin fun gl ->
- clear_constr_tables ();
- let hyps_types = Tacmach.New.pf_hyps_types gl in
- let destructure_omega = Tacmach.New.pf_apply destructure_omega gl in
- let tactic_normalisation, system =
- List.fold_left destructure_omega ([],[]) hyps_types in
- let prelude,sys =
- List.fold_left
- (fun (tac,sys) (t,(v,th,b)) ->
- if b then
- let id = new_identifier () in
- let i = new_id () in
- tag_hypothesis id i;
- (tclTHENLIST [
- (simplest_elim (applist (Lazy.force coq_intro_Z, [t])));
- (intros_mustbe_force [v; id]);
- (elim_id id);
- (clear [id]);
- (intros_mustbe_force [th;id]);
- tac ]),
- {kind = INEQ;
- body = [{v=intern_id v; c=one}];
- constant = zero; id = i} :: sys
- else
- (tclTHENLIST [
- (simplest_elim (applist (Lazy.force coq_new_var, [t])));
- (intros_mustbe_force [v;th]);
- tac ]),
- sys)
- (Proofview.tclUNIT (),[]) (dump_tables ())
- in
- let system = system @ sys in
- if !display_system_flag then display_system display_var system;
- if !old_style_flag then begin
- try
- let _ = simplify (new_id,new_var_num,display_var) false system in
- Proofview.tclUNIT ()
- with UNSOLVABLE ->
- let _,path = depend [] [] (history ()) in
- if !display_action_flag then display_action display_var path;
- (tclTHEN prelude (replay_history tactic_normalisation path))
- end else begin
- try
- let path = simplify_strong (new_id,new_var_num,display_var) system in
- if !display_action_flag then display_action display_var path;
- tclTHEN prelude (replay_history tactic_normalisation path)
- with NO_CONTRADICTION as e ->
- let _, info = Exninfo.capture e in
- tclZEROMSG ~info (Pp.str"Omega can't solve this system")
- end
- end
-
-let coq_omega = coq_omega
-
-let nat_inject =
- Proofview.Goal.enter begin fun gl ->
- let is_conv = Tacmach.New.pf_apply Reductionops.is_conv gl in
- let rec explore p t : unit Proofview.tactic =
- Proofview.tclEVARMAP >>= fun sigma ->
- try match destructurate_term sigma t with
- | Kapp(Plus,[t1;t2]) ->
- tclTHENLIST [
- (clever_rewrite_gen p (mk_plus (mk_inj t1) (mk_inj t2))
- ((Lazy.force coq_inj_plus),[t1;t2]));
- (explore (P_APP 1 :: p) t1);
- (explore (P_APP 2 :: p) t2)
- ]
- | Kapp(Mult,[t1;t2]) ->
- tclTHENLIST [
- (clever_rewrite_gen p (mk_times (mk_inj t1) (mk_inj t2))
- ((Lazy.force coq_inj_mult),[t1;t2]));
- (explore (P_APP 1 :: p) t1);
- (explore (P_APP 2 :: p) t2)
- ]
- | Kapp(Minus,[t1;t2]) ->
- let id = new_identifier () in
- tclTHENS
- (tclTHEN
- (simplest_elim (applist (Lazy.force coq_le_gt_dec, [t2;t1])))
- (intro_mustbe_force id))
- [
- tclTHENLIST [
- (clever_rewrite_gen p
- (mk_minus (mk_inj t1) (mk_inj t2))
- ((Lazy.force coq_inj_minus1),[t1;t2;mkVar id]));
- (loop [id,mkApp (Lazy.force coq_le, [| t2;t1 |])]);
- (explore (P_APP 1 :: p) t1);
- (explore (P_APP 2 :: p) t2) ];
- (tclTHEN
- (clever_rewrite_gen p (mk_integer zero)
- ((Lazy.force coq_inj_minus2),[t1;t2;mkVar id]))
- (loop [id,mkApp (Lazy.force coq_gt, [| t2;t1 |])]))
- ]
- | Kapp(S,[t']) ->
- let rec is_number t =
- try match destructurate_term sigma t with
- Kapp(S,[t]) -> is_number t
- | Kapp(O,[]) -> true
- | _ -> false
- with e when noncritical e -> false
- in
- let rec loop p t : unit Proofview.tactic =
- try match destructurate_term sigma t with
- Kapp(S,[t]) ->
- (tclTHEN
- (clever_rewrite_gen p
- (mkApp (Lazy.force coq_Zsucc, [| mk_inj t |]))
- ((Lazy.force coq_inj_S),[t]))
- (loop (P_APP 1 :: p) t))
- | _ -> explore p t
- with e when noncritical e -> explore p t
- in
- if is_number t' then focused_simpl p else loop p t
- | Kapp(Pred,[t]) ->
- let t_minus_one =
- mkApp (Lazy.force coq_minus, [| t;
- mkApp (Lazy.force coq_S, [| Lazy.force coq_O |]) |]) in
- tclTHEN
- (clever_rewrite_gen_nat (P_APP 1 :: p) t_minus_one
- ((Lazy.force coq_pred_of_minus),[t]))
- (explore p t_minus_one)
- | Kapp(O,[]) -> focused_simpl p
- | _ -> Proofview.tclUNIT ()
- with e when noncritical e -> Proofview.tclUNIT ()
-
- and loop = function
- | [] -> Proofview.tclUNIT ()
- | (i,t)::lit ->
- Proofview.tclEVARMAP >>= fun sigma ->
- begin try match destructurate_prop sigma t with
- Kapp(Le,[t1;t2]) ->
- tclTHENLIST [
- (generalize_tac
- [mkApp (Lazy.force coq_inj_le, [| t1;t2;mkVar i |]) ]);
- (explore [P_APP 1; P_TYPE] t1);
- (explore [P_APP 2; P_TYPE] t2);
- (reintroduce i);
- (loop lit)
- ]
- | Kapp(Lt,[t1;t2]) ->
- tclTHENLIST [
- (generalize_tac
- [mkApp (Lazy.force coq_inj_lt, [| t1;t2;mkVar i |]) ]);
- (explore [P_APP 1; P_TYPE] t1);
- (explore [P_APP 2; P_TYPE] t2);
- (reintroduce i);
- (loop lit)
- ]
- | Kapp(Ge,[t1;t2]) ->
- tclTHENLIST [
- (generalize_tac
- [mkApp (Lazy.force coq_inj_ge, [| t1;t2;mkVar i |]) ]);
- (explore [P_APP 1; P_TYPE] t1);
- (explore [P_APP 2; P_TYPE] t2);
- (reintroduce i);
- (loop lit)
- ]
- | Kapp(Gt,[t1;t2]) ->
- tclTHENLIST [
- (generalize_tac
- [mkApp (Lazy.force coq_inj_gt, [| t1;t2;mkVar i |]) ]);
- (explore [P_APP 1; P_TYPE] t1);
- (explore [P_APP 2; P_TYPE] t2);
- (reintroduce i);
- (loop lit)
- ]
- | Kapp(Neq,[t1;t2]) ->
- tclTHENLIST [
- (generalize_tac
- [mkApp (Lazy.force coq_inj_neq, [| t1;t2;mkVar i |]) ]);
- (explore [P_APP 1; P_TYPE] t1);
- (explore [P_APP 2; P_TYPE] t2);
- (reintroduce i);
- (loop lit)
- ]
- | Kapp(Eq,[typ;t1;t2]) ->
- if is_conv typ (Lazy.force coq_nat) then
- tclTHENLIST [
- (generalize_tac
- [mkApp (Lazy.force coq_inj_eq, [| t1;t2;mkVar i |]) ]);
- (explore [P_APP 2; P_TYPE] t1);
- (explore [P_APP 3; P_TYPE] t2);
- (reintroduce i);
- (loop lit)
- ]
- else loop lit
- | _ -> loop lit
- with e when noncritical e -> loop lit end
- in
- let hyps_types = Tacmach.New.pf_hyps_types gl in
- loop (List.rev hyps_types)
- end
-
-let dec_binop = function
- | Zne -> coq_dec_Zne
- | Zle -> coq_dec_Zle
- | Zlt -> coq_dec_Zlt
- | Zge -> coq_dec_Zge
- | Zgt -> coq_dec_Zgt
- | Le -> coq_dec_le
- | Lt -> coq_dec_lt
- | Ge -> coq_dec_ge
- | Gt -> coq_dec_gt
- | _ -> raise Not_found
-
-let not_binop = function
- | Zne -> coq_not_Zne
- | Zle -> coq_Znot_le_gt
- | Zlt -> coq_Znot_lt_ge
- | Zge -> coq_Znot_ge_lt
- | Zgt -> coq_Znot_gt_le
- | Le -> coq_not_le
- | Lt -> coq_not_lt
- | Ge -> coq_not_ge
- | Gt -> coq_not_gt
- | _ -> raise Not_found
-
-(** A decidability check : for some [t], could we build a term
- of type [decidable t] (i.e. [t\/~t]) ? Otherwise, we raise
- [Undecidable]. Note that a successful check implies that
- [t] has type Prop.
-*)
-
-exception Undecidable
-
-let rec decidability env sigma t =
- match destructurate_prop sigma t with
- | Kapp(Or,[t1;t2]) ->
- mkApp (Lazy.force coq_dec_or, [| t1; t2;
- decidability env sigma t1; decidability env sigma t2 |])
- | Kapp(And,[t1;t2]) ->
- mkApp (Lazy.force coq_dec_and, [| t1; t2;
- decidability env sigma t1; decidability env sigma t2 |])
- | Kapp(Iff,[t1;t2]) ->
- mkApp (Lazy.force coq_dec_iff, [| t1; t2;
- decidability env sigma t1; decidability env sigma t2 |])
- | Kimp(t1,t2) ->
- (* This is the only situation where it's not obvious that [t]
- is in Prop. The recursive call on [t2] will ensure that. *)
- mkApp (Lazy.force coq_dec_imp,
- [| t1; t2; decidability env sigma t1; decidability env sigma t2 |])
- | Kapp(Not,[t1]) ->
- mkApp (Lazy.force coq_dec_not, [| t1; decidability env sigma t1 |])
- | Kapp(Eq,[typ;t1;t2]) ->
- begin match destructurate_type env sigma typ with
- | Kapp(Z,[]) -> mkApp (Lazy.force coq_dec_eq, [| t1;t2 |])
- | Kapp(Nat,[]) -> mkApp (Lazy.force coq_dec_eq_nat, [| t1;t2 |])
- | _ -> raise Undecidable
- end
- | Kapp(op,[t1;t2]) ->
- (try mkApp (Lazy.force (dec_binop op), [| t1; t2 |])
- with Not_found -> raise Undecidable)
- | Kapp(False,[]) -> Lazy.force coq_dec_False
- | Kapp(True,[]) -> Lazy.force coq_dec_True
- | _ -> raise Undecidable
-
-let fresh_id avoid id gl =
- fresh_id_in_env avoid id (Proofview.Goal.env gl)
-
-let onClearedName id tac =
- (* We cannot ensure that hyps can be cleared (because of dependencies), *)
- (* so renaming may be necessary *)
- tclTHEN
- (tclTRY (clear [id]))
- (Proofview.Goal.enter begin fun gl ->
- let id = fresh_id Id.Set.empty id gl in
- tclTHEN (introduction id) (tac id)
- end)
-
-let onClearedName2 id tac =
- tclTHEN
- (tclTRY (clear [id]))
- (Proofview.Goal.enter begin fun gl ->
- let id1 = fresh_id Id.Set.empty (add_suffix id "_left") gl in
- let id2 = fresh_id (Id.Set.singleton id1) (add_suffix id "_right") gl in
- tclTHENLIST [ introduction id1; introduction id2; tac id1 id2 ]
- end)
-
-let destructure_hyps =
- Proofview.Goal.enter begin fun gl ->
- let env = Proofview.Goal.env gl in
- let sigma = Proofview.Goal.sigma gl in
- let decidability = decidability env sigma in
- let rec loop = function
- | [] -> (tclTHEN nat_inject coq_omega)
- | LocalDef (i,body,typ) :: lit when !letin_flag ->
- Proofview.tclEVARMAP >>= fun sigma ->
- begin
- try
- match destructurate_type env sigma typ with
- | Kapp(Nat,_) | Kapp(Z,_) ->
- let hid = fresh_id Id.Set.empty (add_suffix i.binder_name "_eqn") gl in
- let hty = mk_gen_eq typ (mkVar i.binder_name) body in
- tclTHEN
- (assert_by (Name hid) hty reflexivity)
- (loop (LocalAssum (make_annot hid Sorts.Relevant, hty) :: lit))
- | _ -> loop lit
- with e when noncritical e -> loop lit
- end
- | decl :: lit -> (* variable without body (or !letin_flag isn't set) *)
- let i = NamedDecl.get_id decl in
- Proofview.tclEVARMAP >>= fun sigma ->
- begin try match destructurate_prop sigma (NamedDecl.get_type decl) with
- | Kapp(False,[]) -> elim_id i
- | Kapp((Zle|Zge|Zgt|Zlt|Zne),[t1;t2]) -> loop lit
- | Kapp(Or,[t1;t2]) ->
- (tclTHENS
- (elim_id i)
- [ onClearedName i (fun i -> (loop (LocalAssum (make_annot i Sorts.Relevant,t1)::lit)));
- onClearedName i (fun i -> (loop (LocalAssum (make_annot i Sorts.Relevant,t2)::lit))) ])
- | Kapp(And,[t1;t2]) ->
- tclTHEN
- (elim_id i)
- (onClearedName2 i (fun i1 i2 ->
- loop (LocalAssum (make_annot i1 Sorts.Relevant,t1) ::
- LocalAssum (make_annot i2 Sorts.Relevant,t2) :: lit)))
- | Kapp(Iff,[t1;t2]) ->
- tclTHEN
- (elim_id i)
- (onClearedName2 i (fun i1 i2 ->
- loop (LocalAssum (make_annot i1 Sorts.Relevant,mkArrow t1 Sorts.Relevant t2) ::
- LocalAssum (make_annot i2 Sorts.Relevant,mkArrow t2 Sorts.Relevant t1) :: lit)))
- | Kimp(t1,t2) ->
- (* t1 and t2 might be in Type rather than Prop.
- For t1, the decidability check will ensure being Prop. *)
- if Termops.is_Prop sigma (Retyping.get_type_of env sigma t2)
- then
- let d1 = decidability t1 in
- tclTHENLIST [
- (generalize_tac [mkApp (Lazy.force coq_imp_simp,
- [| t1; t2; d1; mkVar i|])]);
- (onClearedName i (fun i ->
- (loop (LocalAssum (make_annot i Sorts.Relevant,mk_or (mk_not t1) t2) :: lit))))
- ]
- else
- loop lit
- | Kapp(Not,[t]) ->
- begin match destructurate_prop sigma t with
- Kapp(Or,[t1;t2]) ->
- tclTHENLIST [
- (generalize_tac
- [mkApp (Lazy.force coq_not_or,[| t1; t2; mkVar i |])]);
- (onClearedName i (fun i ->
- (loop (LocalAssum (make_annot i Sorts.Relevant,mk_and (mk_not t1) (mk_not t2)) :: lit))))
- ]
- | Kapp(And,[t1;t2]) ->
- let d1 = decidability t1 in
- tclTHENLIST [
- (generalize_tac
- [mkApp (Lazy.force coq_not_and,
- [| t1; t2; d1; mkVar i |])]);
- (onClearedName i (fun i ->
- (loop (LocalAssum (make_annot i Sorts.Relevant,mk_or (mk_not t1) (mk_not t2)) :: lit))))
- ]
- | Kapp(Iff,[t1;t2]) ->
- let d1 = decidability t1 in
- let d2 = decidability t2 in
- tclTHENLIST [
- (generalize_tac
- [mkApp (Lazy.force coq_not_iff,
- [| t1; t2; d1; d2; mkVar i |])]);
- (onClearedName i (fun i ->
- (loop (LocalAssum (make_annot i Sorts.Relevant,mk_or (mk_and t1 (mk_not t2))
- (mk_and (mk_not t1) t2)) :: lit))))
- ]
- | Kimp(t1,t2) ->
- (* t2 must be in Prop otherwise ~(t1->t2) wouldn't be ok.
- For t1, being decidable implies being Prop. *)
- let d1 = decidability t1 in
- tclTHENLIST [
- (generalize_tac
- [mkApp (Lazy.force coq_not_imp,
- [| t1; t2; d1; mkVar i |])]);
- (onClearedName i (fun i ->
- (loop (LocalAssum (make_annot i Sorts.Relevant,mk_and t1 (mk_not t2)) :: lit))))
- ]
- | Kapp(Not,[t]) ->
- let d = decidability t in
- tclTHENLIST [
- (generalize_tac
- [mkApp (Lazy.force coq_not_not, [| t; d; mkVar i |])]);
- (onClearedName i (fun i -> (loop (LocalAssum (make_annot i Sorts.Relevant,t) :: lit))))
- ]
- | Kapp(op,[t1;t2]) ->
- (try
- let thm = not_binop op in
- tclTHENLIST [
- (generalize_tac
- [mkApp (Lazy.force thm, [| t1;t2;mkVar i|])]);
- (onClearedName i (fun _ -> loop lit))
- ]
- with Not_found -> loop lit)
- | Kapp(Eq,[typ;t1;t2]) ->
- if !old_style_flag then begin
- match destructurate_type env sigma typ with
- | Kapp(Nat,_) ->
- tclTHENLIST [
- (simplest_elim
- (mkApp
- (Lazy.force coq_not_eq, [|t1;t2;mkVar i|])));
- (onClearedName i (fun _ -> loop lit))
- ]
- | Kapp(Z,_) ->
- tclTHENLIST [
- (simplest_elim
- (mkApp
- (Lazy.force coq_not_Zeq, [|t1;t2;mkVar i|])));
- (onClearedName i (fun _ -> loop lit))
- ]
- | _ -> loop lit
- end else begin
- match destructurate_type env sigma typ with
- | Kapp(Nat,_) ->
- (tclTHEN
- (Tactics.convert_hyp ~check:false ~reorder:false (NamedDecl.set_type (mkApp (Lazy.force coq_neq, [| t1;t2|]))
- decl))
- (loop lit))
- | Kapp(Z,_) ->
- (tclTHEN
- (Tactics.convert_hyp ~check:false ~reorder:false (NamedDecl.set_type (mkApp (Lazy.force coq_Zne, [| t1;t2|]))
- decl))
- (loop lit))
- | _ -> loop lit
- end
- | _ -> loop lit
- end
- | _ -> loop lit
- with
- | Undecidable -> loop lit
- | e when noncritical e -> loop lit
- end
- in
- let hyps = Proofview.Goal.hyps gl in
- loop hyps
- end
-
-let destructure_goal =
- Proofview.Goal.enter begin fun gl ->
- let concl = Proofview.Goal.concl gl in
- let env = Proofview.Goal.env gl in
- let sigma = Proofview.Goal.sigma gl in
- let decidability = decidability env sigma in
- let rec loop t =
- Proofview.tclEVARMAP >>= fun sigma ->
- let prop () = Proofview.tclUNIT (destructurate_prop sigma t) in
- Proofview.V82.wrap_exceptions prop >>= fun prop ->
- match prop with
- | Kapp(Not,[t]) ->
- (tclTHEN
- (tclTHEN (unfold sp_not) intro)
- destructure_hyps)
- | Kimp(a,b) -> (tclTHEN intro (loop b))
- | Kapp(False,[]) -> destructure_hyps
- | _ ->
- let goal_tac =
- try
- let dec = decidability t in
- tclTHEN
- (Proofview.Goal.enter begin fun gl ->
- refine_app gl (mkApp (Lazy.force coq_dec_not_not, [| t; dec |]))
- end)
- intro
- with Undecidable -> Tactics.elim_type (Lazy.force coq_False)
- | e when Proofview.V82.catchable_exception e ->
- let e, info = Exninfo.capture e in
- Proofview.tclZERO ~info e
- in
- tclTHEN goal_tac destructure_hyps
- in
- (loop concl)
- end
-
-let destructure_goal = destructure_goal
-
-let warn_omega_is_deprecated =
- let name = "omega-is-deprecated" in
- let category = "deprecated" in
- CWarnings.create ~name ~category (fun () ->
- Pp.str "omega is deprecated since 8.12; use “lia” instead.")
-
-let omega_solver =
- Proofview.tclUNIT () >>= fun () -> (* delay for [check_required_library] *)
- warn_omega_is_deprecated ();
- Coqlib.check_required_library ["Coq";"omega";"Omega"];
- reset_all ();
- destructure_goal
diff --git a/plugins/omega/coq_omega.mli b/plugins/omega/coq_omega.mli
deleted file mode 100644
index e723082803..0000000000
--- a/plugins/omega/coq_omega.mli
+++ /dev/null
@@ -1,11 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * Copyright INRIA, CNRS and contributors *)
-(* <O___,, * (see version control and CREDITS file for authors & dates) *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(* * (see LICENSE file for the text of the license) *)
-(************************************************************************)
-
-val omega_solver : unit Proofview.tactic
diff --git a/plugins/omega/dune b/plugins/omega/dune
index a3c9342322..e69de29bb2 100644
--- a/plugins/omega/dune
+++ b/plugins/omega/dune
@@ -1,7 +0,0 @@
-(library
- (name omega_plugin)
- (public_name coq-core.plugins.omega)
- (synopsis "Coq's omega plugin")
- (libraries coq-core.plugins.ltac))
-
-(coq.pp (modules g_omega))
diff --git a/plugins/omega/g_omega.mlg b/plugins/omega/g_omega.mlg
deleted file mode 100644
index 888a62b2bc..0000000000
--- a/plugins/omega/g_omega.mlg
+++ /dev/null
@@ -1,29 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * Copyright INRIA, CNRS and contributors *)
-(* <O___,, * (see version control and CREDITS file for authors & dates) *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(* * (see LICENSE file for the text of the license) *)
-(************************************************************************)
-(**************************************************************************)
-(* *)
-(* Omega: a solver of quantifier-free problems in Presburger Arithmetic *)
-(* *)
-(* Pierre Crégut (CNET, Lannion, France) *)
-(* *)
-(**************************************************************************)
-
-
-DECLARE PLUGIN "omega_plugin"
-
-{
-
-open Ltac_plugin
-
-}
-
-TACTIC EXTEND omega
-| [ "omega" ] -> { Coq_omega.omega_solver }
-END
diff --git a/plugins/omega/omega.ml b/plugins/omega/omega.ml
deleted file mode 100644
index 24cd342e42..0000000000
--- a/plugins/omega/omega.ml
+++ /dev/null
@@ -1,708 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * Copyright INRIA, CNRS and contributors *)
-(* <O___,, * (see version control and CREDITS file for authors & dates) *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(* * (see LICENSE file for the text of the license) *)
-(************************************************************************)
-(**************************************************************************)
-(* *)
-(* Omega: a solver of quantifier-free problems in Presburger Arithmetic *)
-(* *)
-(* Pierre Crégut (CNET, Lannion, France) *)
-(* *)
-(* 13/10/2002 : modified to cope with an external numbering of equations *)
-(* and hypothesis. Its use for Omega is not more complex and it makes *)
-(* things much simpler for the reflexive version where we should limit *)
-(* the number of source of numbering. *)
-(**************************************************************************)
-
-module type INT = sig
- type bigint
- val equal : bigint -> bigint -> bool
- val less_than : bigint -> bigint -> bool
- val add : bigint -> bigint -> bigint
- val sub : bigint -> bigint -> bigint
- val mult : bigint -> bigint -> bigint
- val euclid : bigint -> bigint -> bigint * bigint
- val neg : bigint -> bigint
- val zero : bigint
- val one : bigint
- val to_string : bigint -> string
-end
-
-let debug = ref false
-
-module MakeOmegaSolver (I:INT) = struct
-
-type bigint = I.bigint
-let (=?) = I.equal
-let (<?) = I.less_than
-let (<=?) x y = I.less_than x y || x = y
-let (>?) x y = I.less_than y x
-let (>=?) x y = I.less_than y x || x = y
-let (+) = I.add
-let (-) = I.sub
-let ( * ) = I.mult
-let (/) x y = fst (I.euclid x y)
-let (mod) x y = snd (I.euclid x y)
-let zero = I.zero
-let one = I.one
-let two = one + one
-let negone = I.neg one
-let abs x = if I.less_than x zero then I.neg x else x
-let string_of_bigint = I.to_string
-let neg = I.neg
-
-(* To ensure that polymorphic (<) is not used mistakenly on big integers *)
-(* Warning: do not use (=) either on big int *)
-let (<) = ((<) : int -> int -> bool)
-let (>) = ((>) : int -> int -> bool)
-let (<=) = ((<=) : int -> int -> bool)
-let (>=) = ((>=) : int -> int -> bool)
-
-let pp i = print_int i; print_newline (); flush stdout
-
-let push v l = l := v :: !l
-
-let rec pgcd x y = if y =? zero then x else pgcd y (x mod y)
-
-let pgcd_l = function
- | [] -> failwith "pgcd_l"
- | x :: l -> List.fold_left pgcd x l
-
-let floor_div a b =
- match a >=? zero , b >? zero with
- | true,true -> a / b
- | false,false -> a / b
- | true, false -> (a-one) / b - one
- | false,true -> (a+one) / b - one
-
-type coeff = {c: bigint ; v: int}
-
-type linear = coeff list
-
-type eqn_kind = EQUA | INEQ | DISE
-
-type afine = {
- (* a number uniquely identifying the equation *)
- id: int ;
- (* a boolean true for an eq, false for an ineq (Sigma a_i x_i >= 0) *)
- kind: eqn_kind;
- (* the variables and their coefficient *)
- body: coeff list;
- (* a constant *)
- constant: bigint }
-
-type state_action = {
- st_new_eq : afine;
- st_def : afine; (* /!\ this represents [st_def = st_var] *)
- st_orig : afine;
- st_coef : bigint;
- st_var : int }
-
-type action =
- | DIVIDE_AND_APPROX of afine * afine * bigint * bigint
- | NOT_EXACT_DIVIDE of afine * bigint
- | FORGET_C of int
- | EXACT_DIVIDE of afine * bigint
- | SUM of int * (bigint * afine) * (bigint * afine)
- | STATE of state_action
- | HYP of afine
- | FORGET of int * int
- | FORGET_I of int * int
- | CONTRADICTION of afine * afine
- | NEGATE_CONTRADICT of afine * afine * bool
- | MERGE_EQ of int * afine * int
- | CONSTANT_NOT_NUL of int * bigint
- | CONSTANT_NUL of int
- | CONSTANT_NEG of int * bigint
- | SPLIT_INEQ of afine * (int * action list) * (int * action list)
- | WEAKEN of int * bigint
-
-exception UNSOLVABLE
-
-exception NO_CONTRADICTION
-
-let display_eq print_var (l,e) =
- let _ =
- List.fold_left
- (fun not_first f ->
- print_string
- (if f.c <? zero then "- " else if not_first then "+ " else "");
- let c = abs f.c in
- if c =? one then
- Printf.printf "%s " (print_var f.v)
- else
- Printf.printf "%s %s " (string_of_bigint c) (print_var f.v);
- true)
- false l
- in
- if e >? zero then
- Printf.printf "+ %s " (string_of_bigint e)
- else if e <? zero then
- Printf.printf "- %s " (string_of_bigint (abs e))
-
-let rec trace_length l =
- let action_length accu = function
- | SPLIT_INEQ (_,(_,l1),(_,l2)) ->
- accu + one + trace_length l1 + trace_length l2
- | _ -> accu + one in
- List.fold_left action_length zero l
-
-let operator_of_eq = function
- | EQUA -> "=" | DISE -> "!=" | INEQ -> ">="
-
-let kind_of = function
- | EQUA -> "equation" | DISE -> "disequation" | INEQ -> "inequation"
-
-let display_system print_var l =
- List.iter
- (fun { kind=b; body=e; constant=c; id=id} ->
- Printf.printf "E%d: " id;
- display_eq print_var (e,c);
- Printf.printf "%s 0\n" (operator_of_eq b))
- l;
- print_string "------------------------\n\n"
-
-let display_inequations print_var l =
- List.iter (fun e -> display_eq print_var e;print_string ">= 0\n") l;
- print_string "------------------------\n\n"
-
-let sbi = string_of_bigint
-
-let rec display_action print_var = function
- | act :: l -> begin match act with
- | DIVIDE_AND_APPROX (e1,e2,k,d) ->
- Printf.printf
- "Inequation E%d is divided by %s and the constant coefficient is \
- rounded by subtracting %s.\n" e1.id (sbi k) (sbi d)
- | NOT_EXACT_DIVIDE (e,k) ->
- Printf.printf
- "Constant in equation E%d is not divisible by the pgcd \
- %s of its other coefficients.\n" e.id (sbi k)
- | EXACT_DIVIDE (e,k) ->
- Printf.printf
- "Equation E%d is divided by the pgcd \
- %s of its coefficients.\n" e.id (sbi k)
- | WEAKEN (e,k) ->
- Printf.printf
- "To ensure a solution in the dark shadow \
- the equation E%d is weakened by %s.\n" e (sbi k)
- | SUM (e,(c1,e1),(c2,e2)) ->
- Printf.printf
- "We state %s E%d = %s %s E%d + %s %s E%d.\n"
- (kind_of e1.kind) e (sbi c1) (kind_of e1.kind) e1.id (sbi c2)
- (kind_of e2.kind) e2.id
- | STATE { st_new_eq = e } ->
- Printf.printf "We define a new equation E%d: " e.id;
- display_eq print_var (e.body,e.constant);
- print_string (operator_of_eq e.kind); print_string " 0"
- | HYP e ->
- Printf.printf "We define E%d: " e.id;
- display_eq print_var (e.body,e.constant);
- print_string (operator_of_eq e.kind); print_string " 0\n"
- | FORGET_C e -> Printf.printf "E%d is trivially satisfiable.\n" e
- | FORGET (e1,e2) -> Printf.printf "E%d subsumes E%d.\n" e1 e2
- | FORGET_I (e1,e2) -> Printf.printf "E%d subsumes E%d.\n" e1 e2
- | MERGE_EQ (e,e1,e2) ->
- Printf.printf "E%d and E%d can be merged into E%d.\n" e1.id e2 e
- | CONTRADICTION (e1,e2) ->
- Printf.printf
- "Equations E%d and E%d imply a contradiction on their \
- constant factors.\n" e1.id e2.id
- | NEGATE_CONTRADICT(e1,e2,b) ->
- Printf.printf
- "Equations E%d and E%d state that their body is at the same time \
- equal and different\n" e1.id e2.id
- | CONSTANT_NOT_NUL (e,k) ->
- Printf.printf "Equation E%d states %s = 0.\n" e (sbi k)
- | CONSTANT_NEG(e,k) ->
- Printf.printf "Equation E%d states %s >= 0.\n" e (sbi k)
- | CONSTANT_NUL e ->
- Printf.printf "Inequation E%d states 0 != 0.\n" e
- | SPLIT_INEQ (e,(e1,l1),(e2,l2)) ->
- Printf.printf "Equation E%d is split in E%d and E%d\n\n" e.id e1 e2;
- display_action print_var l1;
- print_newline ();
- display_action print_var l2;
- print_newline ()
- end; display_action print_var l
- | [] ->
- flush stdout
-
-let default_print_var v = Printf.sprintf "X%d" v (* For debugging *)
-
-(*""*)
-let add_event, history, clear_history =
- let accu = ref [] in
- (fun (v:action) -> if !debug then display_action default_print_var [v]; push v accu),
- (fun () -> !accu),
- (fun () -> accu := [])
-
-let nf_linear = List.sort (fun x y -> Util.(-) y.v x.v)
-
-let nf ((b : bool),(e,(x : int))) = (b,(nf_linear e,x))
-
-let map_eq_linear f =
- let rec loop = function
- | x :: l -> let c = f x.c in if c=?zero then loop l else {v=x.v; c=c} :: loop l
- | [] -> []
- in
- loop
-
-let map_eq_afine f e =
- { id = e.id; kind = e.kind; body = map_eq_linear f e.body;
- constant = f e.constant }
-
-let negate_eq = map_eq_afine (fun x -> neg x)
-
-let rec sum p0 p1 = match (p0,p1) with
- | ([], l) -> l | (l, []) -> l
- | (((x1::l1) as l1'), ((x2::l2) as l2')) ->
- if x1.v = x2.v then
- let c = x1.c + x2.c in
- if c =? zero then sum l1 l2 else {v=x1.v;c=c} :: sum l1 l2
- else if x1.v > x2.v then
- x1 :: sum l1 l2'
- else
- x2 :: sum l1' l2
-
-let sum_afine new_eq_id eq1 eq2 =
- { kind = eq1.kind; id = new_eq_id ();
- body = sum eq1.body eq2.body; constant = eq1.constant + eq2.constant }
-
-exception FACTOR1
-
-let rec chop_factor_1 = function
- | x :: l ->
- if abs x.c =? one then x,l else let (c',l') = chop_factor_1 l in (c',x::l')
- | [] -> raise FACTOR1
-
-exception CHOPVAR
-
-let rec chop_var v = function
- | f :: l -> if f.v = v then f,l else let (f',l') = chop_var v l in (f',f::l')
- | [] -> raise CHOPVAR
-
-let normalize ({id=id; kind=eq_flag; body=e; constant =x} as eq) =
- if e = [] then begin
- match eq_flag with
- | EQUA ->
- if x =? zero then [] else begin
- add_event (CONSTANT_NOT_NUL(id,x)); raise UNSOLVABLE
- end
- | DISE ->
- if x <> zero then [] else begin
- add_event (CONSTANT_NUL id); raise UNSOLVABLE
- end
- | INEQ ->
- if x >=? zero then [] else begin
- add_event (CONSTANT_NEG(id,x)); raise UNSOLVABLE
- end
- end else
- let gcd = pgcd_l (List.map (fun f -> abs f.c) e) in
- if eq_flag=EQUA && x mod gcd <> zero then begin
- add_event (NOT_EXACT_DIVIDE (eq,gcd)); raise UNSOLVABLE
- end else if eq_flag=DISE && x mod gcd <> zero then begin
- add_event (FORGET_C eq.id); []
- end else if gcd <> one then begin
- let c = floor_div x gcd in
- let d = x - c * gcd in
- let new_eq = {id=id; kind=eq_flag; constant=c;
- body=map_eq_linear (fun c -> c / gcd) e} in
- add_event (if eq_flag=EQUA || eq_flag = DISE then EXACT_DIVIDE(eq,gcd)
- else DIVIDE_AND_APPROX(eq,new_eq,gcd,d));
- [new_eq]
- end else [eq]
-
-let eliminate_with_in new_eq_id {v=v;c=c_unite} eq2
- ({body=e1; constant=c1} as eq1) =
- try
- let (f,_) = chop_var v e1 in
- let coeff = if c_unite=?one then neg f.c else if c_unite=? negone then f.c
- else failwith "eliminate_with_in" in
- let res = sum_afine new_eq_id eq1 (map_eq_afine (fun c -> c * coeff) eq2) in
- add_event (SUM (res.id,(one,eq1),(coeff,eq2))); res
- with CHOPVAR -> eq1
-
-let omega_mod a b = a - b * floor_div (two * a + b) (two * b)
-let banerjee_step (new_eq_id,new_var_id,print_var) original l1 l2 =
- let e = original.body in
- let sigma = new_var_id () in
- if e == [] then begin
- display_system print_var [original] ; failwith "TL"
- end;
- let smallest,var =
- List.fold_left (fun (v,p) c -> if v >? (abs c.c) then abs c.c,c.v else (v,p))
- (abs (List.hd e).c, (List.hd e).v) (List.tl e)
- in
- let m = smallest + one in
- let new_eq =
- { constant = omega_mod original.constant m;
- body = {c= neg m;v=sigma} ::
- map_eq_linear (fun a -> omega_mod a m) original.body;
- id = new_eq_id (); kind = EQUA } in
- let definition =
- { constant = neg (floor_div (two * original.constant + m) (two * m));
- body = map_eq_linear (fun a -> neg (floor_div (two * a + m) (two * m)))
- original.body;
- id = new_eq_id (); kind = EQUA } in
- add_event (STATE {st_new_eq = new_eq; st_def = definition;
- st_orig = original; st_coef = m; st_var = sigma});
- let new_eq = List.hd (normalize new_eq) in
- let eliminated_var, def = chop_var var new_eq.body in
- let other_equations =
- Util.List.map_append
- (fun e ->
- normalize (eliminate_with_in new_eq_id eliminated_var new_eq e)) l1 in
- let inequations =
- Util.List.map_append
- (fun e ->
- normalize (eliminate_with_in new_eq_id eliminated_var new_eq e)) l2 in
- let original' = eliminate_with_in new_eq_id eliminated_var new_eq original in
- let mod_original = map_eq_afine (fun c -> c / m) original' in
- add_event (EXACT_DIVIDE (original',m));
- List.hd (normalize mod_original),other_equations,inequations
-
-let rec eliminate_one_equation ((new_eq_id,new_var_id,print_var) as new_ids) (e,other,ineqs) =
- if !debug then display_system print_var (e::other);
- try
- let v,def = chop_factor_1 e.body in
- (Util.List.map_append
- (fun e' -> normalize (eliminate_with_in new_eq_id v e e')) other,
- Util.List.map_append
- (fun e' -> normalize (eliminate_with_in new_eq_id v e e')) ineqs)
- with FACTOR1 ->
- eliminate_one_equation new_ids (banerjee_step new_ids e other ineqs)
-
-let rec banerjee ((_,_,print_var) as new_ids) (sys_eq,sys_ineq) =
- let rec fst_eq_1 = function
- (eq::l) ->
- if List.exists (fun x -> abs x.c =? one) eq.body then eq,l
- else let (eq',l') = fst_eq_1 l in (eq',eq::l')
- | [] -> raise Not_found in
- match sys_eq with
- [] -> if !debug then display_system print_var sys_ineq; sys_ineq
- | (e1::rest) ->
- let eq,other = try fst_eq_1 sys_eq with Not_found -> (e1,rest) in
- if eq.body = [] then
- if eq.constant =? zero then begin
- add_event (FORGET_C eq.id); banerjee new_ids (other,sys_ineq)
- end else begin
- add_event (CONSTANT_NOT_NUL(eq.id,eq.constant)); raise UNSOLVABLE
- end
- else
- banerjee new_ids
- (eliminate_one_equation new_ids (eq,other,sys_ineq))
-
-type kind = INVERTED | NORMAL
-
-let redundancy_elimination new_eq_id system =
- let normal = function
- ({body=f::_} as e) when f.c <? zero -> negate_eq e, INVERTED
- | e -> e,NORMAL in
- let table = Hashtbl.create 7 in
- List.iter
- (fun e ->
- let ({body=ne} as nx) ,kind = normal e in
- if ne = [] then
- if nx.constant <? zero then begin
- add_event (CONSTANT_NEG(nx.id,nx.constant)); raise UNSOLVABLE
- end else add_event (FORGET_C nx.id)
- else
- try
- let (optnormal,optinvert) = Hashtbl.find table ne in
- let final =
- if kind = NORMAL then begin
- match optnormal with
- Some v ->
- let kept =
- if v.constant <? nx.constant
- then begin add_event (FORGET (v.id,nx.id));v end
- else begin add_event (FORGET (nx.id,v.id));nx end in
- (Some(kept),optinvert)
- | None -> Some nx,optinvert
- end else begin
- match optinvert with
- Some v ->
- let _kept =
- if v.constant >? nx.constant
- then begin add_event (FORGET_I (v.id,nx.id));v end
- else begin add_event (FORGET_I (nx.id,v.id));nx end in
- (optnormal,Some(if v.constant >? nx.constant then v else nx))
- | None -> optnormal,Some nx
- end in
- begin match final with
- (Some high, Some low) ->
- if high.constant <? low.constant then begin
- add_event(CONTRADICTION (high,negate_eq low));
- raise UNSOLVABLE
- end
- | _ -> () end;
- Hashtbl.remove table ne;
- Hashtbl.add table ne final
- with Not_found ->
- Hashtbl.add table ne
- (if kind = NORMAL then (Some nx,None) else (None,Some nx)))
- system;
- let accu_eq = ref [] in
- let accu_ineq = ref [] in
- Hashtbl.iter
- (fun p0 p1 -> match (p0,p1) with
- | (e, (Some x, Some y)) when x.constant =? y.constant ->
- let id=new_eq_id () in
- add_event (MERGE_EQ(id,x,y.id));
- push {id=id; kind=EQUA; body=x.body; constant=x.constant} accu_eq
- | (e, (optnorm,optinvert)) ->
- begin match optnorm with
- Some x -> push x accu_ineq | _ -> () end;
- begin match optinvert with
- Some x -> push (negate_eq x) accu_ineq | _ -> () end)
- table;
- !accu_eq,!accu_ineq
-
-exception SOLVED_SYSTEM
-
-let select_variable system =
- let table = Hashtbl.create 7 in
- let push v c=
- try let r = Hashtbl.find table v in r := max !r (abs c)
- with Not_found -> Hashtbl.add table v (ref (abs c)) in
- List.iter (fun {body=l} -> List.iter (fun f -> push f.v f.c) l) system;
- let vmin,cmin = ref (-1), ref zero in
- let var_cpt = ref 0 in
- Hashtbl.iter
- (fun v ({contents = c}) ->
- incr var_cpt;
- if c <? !cmin || !vmin = (-1) then begin vmin := v; cmin := c end)
- table;
- if !var_cpt < 1 then raise SOLVED_SYSTEM;
- !vmin
-
-let classify v system =
- List.fold_left
- (fun (not_occ,below,over) eq ->
- try let f,eq' = chop_var v eq.body in
- if f.c >=? zero then (not_occ,((f.c,eq) :: below),over)
- else (not_occ,below,((neg f.c,eq) :: over))
- with CHOPVAR -> (eq::not_occ,below,over))
- ([],[],[]) system
-
-let product new_eq_id dark_shadow low high =
- List.fold_left
- (fun accu (a,eq1) ->
- List.fold_left
- (fun accu (b,eq2) ->
- let eq =
- sum_afine new_eq_id (map_eq_afine (fun c -> c * b) eq1)
- (map_eq_afine (fun c -> c * a) eq2) in
- add_event(SUM(eq.id,(b,eq1),(a,eq2)));
- match normalize eq with
- | [eq] ->
- let final_eq =
- if dark_shadow then
- let delta = (a - one) * (b - one) in
- add_event(WEAKEN(eq.id,delta));
- {id = eq.id; kind=INEQ; body = eq.body;
- constant = eq.constant - delta}
- else eq
- in final_eq :: accu
- | (e::_) -> failwith "Product dardk"
- | [] -> accu)
- accu high)
- [] low
-
-let fourier_motzkin (new_eq_id,_,print_var) dark_shadow system =
- let v = select_variable system in
- let (ineq_out, ineq_low,ineq_high) = classify v system in
- let expanded = ineq_out @ product new_eq_id dark_shadow ineq_low ineq_high in
- if !debug then display_system print_var expanded; expanded
-
-let simplify ((new_eq_id,new_var_id,print_var) as new_ids) dark_shadow system =
- if List.exists (fun e -> e.kind = DISE) system then
- failwith "disequation in simplify";
- clear_history ();
- List.iter (fun e -> add_event (HYP e)) system;
- let system = Util.List.map_append normalize system in
- let eqs,ineqs = List.partition (fun e -> e.kind=EQUA) system in
- let simp_eq,simp_ineq = redundancy_elimination new_eq_id ineqs in
- let system = (eqs @ simp_eq,simp_ineq) in
- let rec loop1a system =
- let sys_ineq = banerjee new_ids system in
- loop1b sys_ineq
- and loop1b sys_ineq =
- let simp_eq,simp_ineq = redundancy_elimination new_eq_id sys_ineq in
- if simp_eq = [] then simp_ineq else loop1a (simp_eq,simp_ineq)
- in
- let rec loop2 system =
- try
- let expanded = fourier_motzkin new_ids dark_shadow system in
- loop2 (loop1b expanded)
- with SOLVED_SYSTEM ->
- if !debug then display_system print_var system; system
- in
- loop2 (loop1a system)
-
-let rec depend relie_on accu = function
- | act :: l ->
- begin match act with
- | DIVIDE_AND_APPROX (e,_,_,_) ->
- if Int.List.mem e.id relie_on then depend relie_on (act::accu) l
- else depend relie_on accu l
- | EXACT_DIVIDE (e,_) ->
- if Int.List.mem e.id relie_on then depend relie_on (act::accu) l
- else depend relie_on accu l
- | WEAKEN (e,_) ->
- if Int.List.mem e relie_on then depend relie_on (act::accu) l
- else depend relie_on accu l
- | SUM (e,(_,e1),(_,e2)) ->
- if Int.List.mem e relie_on then
- depend (e1.id::e2.id::relie_on) (act::accu) l
- else
- depend relie_on accu l
- | STATE {st_new_eq=e;st_orig=o} ->
- if Int.List.mem e.id relie_on then depend (o.id::relie_on) (act::accu) l
- else depend relie_on accu l
- | HYP e ->
- if Int.List.mem e.id relie_on then depend relie_on (act::accu) l
- else depend relie_on accu l
- | FORGET_C _ -> depend relie_on accu l
- | FORGET _ -> depend relie_on accu l
- | FORGET_I _ -> depend relie_on accu l
- | MERGE_EQ (e,e1,e2) ->
- if Int.List.mem e relie_on then
- depend (e1.id::e2::relie_on) (act::accu) l
- else
- depend relie_on accu l
- | NOT_EXACT_DIVIDE (e,_) -> depend (e.id::relie_on) (act::accu) l
- | CONTRADICTION (e1,e2) ->
- depend (e1.id::e2.id::relie_on) (act::accu) l
- | CONSTANT_NOT_NUL (e,_) -> depend (e::relie_on) (act::accu) l
- | CONSTANT_NEG (e,_) -> depend (e::relie_on) (act::accu) l
- | CONSTANT_NUL e -> depend (e::relie_on) (act::accu) l
- | NEGATE_CONTRADICT (e1,e2,_) ->
- depend (e1.id::e2.id::relie_on) (act::accu) l
- | SPLIT_INEQ _ -> failwith "depend"
- end
- | [] -> relie_on, accu
-
-let negation (eqs,ineqs) =
- let diseq,_ = List.partition (fun e -> e.kind = DISE) ineqs in
- let normal = function
- | ({body=f::_} as e) when f.c <? zero -> negate_eq e, INVERTED
- | e -> e,NORMAL in
- let table = Hashtbl.create 7 in
- List.iter (fun e ->
- let {body=ne;constant=c} ,kind = normal e in
- Hashtbl.add table (ne,c) (kind,e)) diseq;
- List.iter (fun e ->
- assert (e.kind = EQUA);
- let {body=ne;constant=c},kind = normal e in
- try
- let (kind',e') = Hashtbl.find table (ne,c) in
- add_event (NEGATE_CONTRADICT (e,e',kind=kind'));
- raise UNSOLVABLE
- with Not_found -> ()) eqs
-
-exception FULL_SOLUTION of action list * int list
-
-let simplify_strong ((new_eq_id,new_var_id,print_var) as new_ids) system =
- clear_history ();
- List.iter (fun e -> add_event (HYP e)) system;
- (* Initial simplification phase *)
- let rec loop1a system =
- negation system;
- let sys_ineq = banerjee new_ids system in
- loop1b sys_ineq
- and loop1b sys_ineq =
- let dise,ine = List.partition (fun e -> e.kind = DISE) sys_ineq in
- let simp_eq,simp_ineq = redundancy_elimination new_eq_id ine in
- if simp_eq = [] then dise @ simp_ineq
- else loop1a (simp_eq,dise @ simp_ineq)
- in
- let rec loop2 system =
- try
- let expanded = fourier_motzkin new_ids false system in
- loop2 (loop1b expanded)
- with SOLVED_SYSTEM -> if !debug then display_system print_var system; system
- in
- let rec explode_diseq = function
- | (de::diseq,ineqs,expl_map) ->
- let id1 = new_eq_id ()
- and id2 = new_eq_id () in
- let e1 =
- {id = id1; kind=INEQ; body = de.body; constant = de.constant -one} in
- let e2 =
- {id = id2; kind=INEQ; body = map_eq_linear neg de.body;
- constant = neg de.constant - one} in
- let new_sys =
- List.map (fun (what,sys) -> ((de.id,id1,true)::what, e1::sys))
- ineqs @
- List.map (fun (what,sys) -> ((de.id,id2,false)::what,e2::sys))
- ineqs
- in
- explode_diseq (diseq,new_sys,(de.id,(de,id1,id2))::expl_map)
- | ([],ineqs,expl_map) -> ineqs,expl_map
- in
- try
- let system = Util.List.map_append normalize system in
- let eqs,ineqs = List.partition (fun e -> e.kind=EQUA) system in
- let dise,ine = List.partition (fun e -> e.kind = DISE) ineqs in
- let simp_eq,simp_ineq = redundancy_elimination new_eq_id ine in
- let system = (eqs @ simp_eq,simp_ineq @ dise) in
- let system' = loop1a system in
- let diseq,ineq = List.partition (fun e -> e.kind = DISE) system' in
- let first_segment = history () in
- let sys_exploded,explode_map = explode_diseq (diseq,[[],ineq],[]) in
- let all_solutions =
- List.map
- (fun (decomp,sys) ->
- clear_history ();
- try let _ = loop2 sys in raise NO_CONTRADICTION
- with UNSOLVABLE ->
- let relie_on,path = depend [] [] (history ()) in
- let dc,_ = List.partition (fun (_,id,_) -> Int.List.mem id relie_on) decomp in
- let red = List.map (fun (x,_,_) -> x) dc in
- (red,relie_on,decomp,path))
- sys_exploded
- in
- let max_count sys =
- let tbl = Hashtbl.create 7 in
- let augment x =
- try incr (Hashtbl.find tbl x)
- with Not_found -> Hashtbl.add tbl x (ref 1) in
- let eq = ref (-1) and c = ref 0 in
- List.iter (function
- | ([],r_on,_,path) -> raise (FULL_SOLUTION (path,r_on))
- | (l,_,_,_) -> List.iter augment l) sys;
- Hashtbl.iter (fun x v -> if !v > !c then begin eq := x; c := !v end) tbl;
- !eq
- in
- let rec solve systems =
- try
- let id = max_count systems in
- let rec sign = function
- | ((id',_,b)::l) -> if id=id' then b else sign l
- | [] -> failwith "solve" in
- let s1,s2 =
- List.partition (fun (_,_,decomp,_) -> sign decomp) systems in
- let remove_int (dep,ro,dc,pa) =
- (Util.List.except Int.equal id dep,ro,dc,pa)
- in
- let s1' = List.map remove_int s1 in
- let s2' = List.map remove_int s2 in
- let (r1,relie1) = solve s1'
- and (r2,relie2) = solve s2' in
- let (eq,id1,id2) = Int.List.assoc id explode_map in
- [SPLIT_INEQ(eq,(id1,r1),(id2, r2))],
- eq.id :: Util.List.union Int.equal relie1 relie2
- with FULL_SOLUTION (x0,x1) -> (x0,x1)
- in
- let act,relie_on = solve all_solutions in
- snd(depend relie_on act first_segment)
- with UNSOLVABLE -> snd (depend [] [] (history ()))
-
-end
diff --git a/plugins/omega/omega_plugin.mlpack b/plugins/omega/omega_plugin.mlpack
deleted file mode 100644
index df7f1047f2..0000000000
--- a/plugins/omega/omega_plugin.mlpack
+++ /dev/null
@@ -1,3 +0,0 @@
-Omega
-Coq_omega
-G_omega
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 935cef58b9..ad85f68b03 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -46,6 +46,7 @@ open Ssrtacticals
open Ssrbwd
open Ssrequality
open Ssripats
+open Libobject
(** Ssreflect load check. *)
@@ -79,8 +80,39 @@ let ssrtac_entry name = {
mltac_index = 0;
}
-let register_ssrtac name f =
- Tacenv.register_ml_tactic (ssrtac_name name) [|f|]
+let cache_tactic_notation (_, (key, body, parule)) =
+ Tacenv.register_alias key body;
+ Pptactic.declare_notation_tactic_pprule key parule
+
+type tactic_grammar_obj = KerName.t * Tacenv.alias_tactic * Pptactic.pp_tactic
+
+let inSsrGrammar : tactic_grammar_obj -> obj =
+ declare_object {(default_object "SsrGrammar") with
+ load_function = (fun _ -> cache_tactic_notation);
+ cache_function = cache_tactic_notation;
+ classify_function = (fun x -> Keep x)}
+
+let path = MPfile (DirPath.make @@ List.map Id.of_string ["ssreflect"; "ssr"; "Coq"])
+
+let register_ssrtac name f prods =
+ let open Pptactic in
+ Tacenv.register_ml_tactic (ssrtac_name name) [|f|];
+ let map id = Reference (Locus.ArgVar (CAst.make id)) in
+ let get_id = function
+ | TacTerm s -> None
+ | TacNonTerm (_, (_, ido)) -> ido in
+ let ids = List.map_filter get_id prods in
+ let tac = TacML (CAst.make (ssrtac_entry name, List.map map ids)) in
+ let key = KerName.make path (Label.make ("ssrparser_" ^ name)) in
+ let body = Tacenv.{ alias_args = ids; alias_body = tac; alias_deprecation = None } in
+ let parule = {
+ pptac_level = 0;
+ pptac_prods = prods
+ } in
+ let obj () =
+ Lib.add_anonymous_leaf (inSsrGrammar (key, body, parule)) in
+ Mltop.declare_cache_obj obj __coq_plugin_name;
+ key
let cast_arg wit v = Taccoerce.Value.cast (Genarg.topwit wit) v
@@ -933,7 +965,7 @@ END
{
let pr_intros sep intrs =
- if intrs = [] then mt() else sep () ++ str "=>" ++ pr_ipats intrs
+ if intrs = [] then mt() else sep () ++ str "=>" ++ sep () ++ pr_ipats intrs
let pr_ssrintros _ _ _ = pr_intros mt
}
@@ -963,15 +995,6 @@ END
{
-let () = register_ssrtac "tclintros" begin fun args ist -> match args with
-| [arg] ->
- let arg = cast_arg wit_ssrintrosarg arg in
- let tac, intros = arg in
- ssrevaltac ist tac <*> tclIPATssr intros
-| _ -> assert false
-end
-
-
(** Defined identifier *)
let pr_ssrfwdid id = pr_spc () ++ pr_id id
@@ -1672,20 +1695,28 @@ let _ = add_internal_name (is_tagged perm_tag)
{
-type ssrargfmt = ArgSsr of string | ArgSep of string
+ let ssrtac_expr ?loc key args =
+ TacAlias (CAst.make ?loc (key, (List.map (fun x -> Tacexpr.TacGeneric (None, x)) args)))
-let set_pr_ssrtac name prec afmt = (* FIXME *) () (*
- let fmt = List.map (function
- | ArgSep s -> Egramml.GramTerminal s
- | ArgSsr s -> Egramml.GramTerminal s
- | ArgCoq at -> Egramml.GramTerminal "COQ_ARG") afmt in
- let tacname = ssrtac_name name in () *)
+let mk_non_term wit id =
+ let open Pptactic in
+ TacNonTerm (None, (Extend.Uentry (Genarg.ArgT.Any (Genarg.get_arg_tag wit)), Some id))
-let ssrtac_expr ?loc name args = TacML (CAst.make ?loc (ssrtac_entry name, args))
+let tclintroskey =
+ let prods =
+ [ mk_non_term wit_ssrintrosarg (Names.Id.of_string "arg") ] in
+ let tac = begin fun args ist -> match args with
+ | [arg] ->
+ let arg = cast_arg wit_ssrintrosarg arg in
+ let tac, intros = arg in
+ ssrevaltac ist tac <*> tclIPATssr intros
+ | _ -> assert false
+ end in
+ register_ssrtac "tclintros" tac prods
let tclintros_expr ?loc tac ipats =
- let args = [Tacexpr.TacGeneric (None, in_gen (rawwit wit_ssrintrosarg) (tac, ipats))] in
- ssrtac_expr ?loc "tclintros" args
+ let args = [in_gen (rawwit wit_ssrintrosarg) (tac, ipats)] in
+ ssrtac_expr ?loc tclintroskey args
}
@@ -1768,18 +1799,20 @@ END
{
-let () = register_ssrtac "tcldo" begin fun args ist -> match args with
-| [arg] ->
- let arg = cast_arg wit_ssrdoarg arg in
- ssrdotac ist arg
-| _ -> assert false
-end
-
-let _ = set_pr_ssrtac "tcldo" 3 [ArgSep "do "; ArgSsr "doarg"]
+let tcldokey =
+ let open Pptactic in
+ let prods = [ TacTerm "do"; mk_non_term wit_ssrdoarg (Names.Id.of_string "arg") ] in
+ let tac = begin fun args ist -> match args with
+ | [arg] ->
+ let arg = cast_arg wit_ssrdoarg arg in
+ ssrdotac ist arg
+ | _ -> assert false
+ end in
+ register_ssrtac "tcldo" tac prods
let ssrdotac_expr ?loc n m tac clauses =
let arg = ((n, m), tac), clauses in
- ssrtac_expr ?loc "tcldo" [Tacexpr.TacGeneric (None, in_gen (rawwit wit_ssrdoarg) arg)]
+ ssrtac_expr ?loc tcldokey [in_gen (rawwit wit_ssrdoarg) arg]
}
@@ -1815,22 +1848,26 @@ END
{
-let () = register_ssrtac "tclseq" begin fun args ist -> match args with
-| [tac; dir; arg] ->
- let tac = cast_arg wit_ssrtclarg tac in
- let dir = cast_arg wit_ssrseqdir dir in
- let arg = cast_arg wit_ssrseqarg arg in
- tclSEQAT ist tac dir arg
-| _ -> assert false
-end
-
-let _ = set_pr_ssrtac "tclseq" 5 [ArgSsr "tclarg"; ArgSsr "seqdir"; ArgSsr "seqarg"]
+let tclseqkey =
+ let prods =
+ [ mk_non_term wit_ssrtclarg (Names.Id.of_string "tac")
+ ; mk_non_term wit_ssrseqdir (Names.Id.of_string "dir")
+ ; mk_non_term wit_ssrseqarg (Names.Id.of_string "arg") ] in
+ let tac = begin fun args ist -> match args with
+ | [tac; dir; arg] ->
+ let tac = cast_arg wit_ssrtclarg tac in
+ let dir = cast_arg wit_ssrseqdir dir in
+ let arg = cast_arg wit_ssrseqarg arg in
+ tclSEQAT ist tac dir arg
+ | _ -> assert false
+ end in
+ register_ssrtac "tclseq" tac prods
let tclseq_expr ?loc tac dir arg =
let arg1 = in_gen (rawwit wit_ssrtclarg) tac in
let arg2 = in_gen (rawwit wit_ssrseqdir) dir in
let arg3 = in_gen (rawwit wit_ssrseqarg) (check_seqtacarg dir arg) in
- ssrtac_expr ?loc "tclseq" (List.map (fun x -> Tacexpr.TacGeneric (None, x)) [arg1; arg2; arg3])
+ ssrtac_expr ?loc tclseqkey [arg1; arg2; arg3]
}
@@ -2453,8 +2490,9 @@ GRAMMAR EXTEND Gram
GLOBAL: ltac_expr;
ltac_expr: LEVEL "3"
[ RIGHTA [ IDENT "abstract"; gens = ssrdgens ->
- { ssrtac_expr ~loc "abstract"
- [Tacexpr.TacGeneric (None, Genarg.in_gen (Genarg.rawwit wit_ssrdgens) gens)] } ]];
+ { TacML (CAst.make ~loc (
+ ssrtac_entry "abstract", [Tacexpr.TacGeneric (None, Genarg.in_gen (Genarg.rawwit wit_ssrdgens) gens)]))
+ } ]];
END
TACTIC EXTEND ssrabstract
| [ "abstract" ssrdgens(gens) ] -> {
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index 7774258fca..805be1fc87 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -22,7 +22,6 @@ open Vars
open Libnames
open Tactics
open Termops
-open Recordops
open Tacmach
open Glob_term
open Util
@@ -333,7 +332,8 @@ type tpattern = {
let all_ok _ _ = true
let proj_nparams c =
- try 1 + Recordops.find_projection_nparams (GlobRef.ConstRef c) with _ -> 0
+ try 1 + Structures.Structure.projection_nparams c
+ with Not_found -> 0
let isRigid c = match kind c with
| Prod _ | Sort _ | Lambda _ | Case _ | Fix _ | CoFix _ -> true
@@ -429,9 +429,13 @@ let ungen_upat lhs (sigma, uc, t) u =
| _ -> KpatRigid in
sigma, uc, {u with up_k = k; up_FO = lhs; up_f = f; up_a = a; up_t = t}
-let nb_cs_proj_args pc f u =
+let nb_cs_proj_args ise pc f u =
+ let open Structures in
+ let open ValuePattern in
let na k =
- List.length (snd (lookup_canonical_conversion (Global.env()) (GlobRef.ConstRef pc, k))).o_TCOMPS in
+ let open CanonicalSolution in
+ let _, { cvalue_arguments } = find (Global.env()) ise (GlobRef.ConstRef pc, k) in
+ List.length cvalue_arguments in
let nargs_of_proj t = match kind t with
| App(_,args) -> Array.length args
| Proj _ -> 0 (* if splay_app calls expand_projection, this has to be
@@ -441,7 +445,7 @@ let nb_cs_proj_args pc f u =
| Prod _ -> na Prod_cs
| Sort s -> na (Sort_cs (Sorts.family s))
| Const (c',_) when Constant.CanOrd.equal c' pc -> nargs_of_proj u.up_f
- | Proj (c',_) when Constant.CanOrd.equal (Projection.constant c') pc -> nargs_of_proj u.up_f
+ | Proj (c',_) when Constant.CanOrd.equal (Names.Projection.constant c') pc -> nargs_of_proj u.up_f
| Var _ | Ind _ | Construct _ | Const _ -> na (Const_cs (fst @@ destRef f))
| _ -> -1
with Not_found -> -1
@@ -467,7 +471,7 @@ let splay_app ise =
| Cast _ | Evar _ -> loop c [| |]
| _ -> c, [| |]
-let filter_upat i0 f n u fpats =
+let filter_upat ise i0 f n u fpats =
let na = Array.length u.up_a in
if n < na then fpats else
let np = match u.up_k with
@@ -479,7 +483,7 @@ let filter_upat i0 f n u fpats =
| KpatRigid when isRigid f -> na
| KpatFlex -> na
| KpatProj pc ->
- let np = na + nb_cs_proj_args pc f u in if n < np then -1 else np
+ let np = na + nb_cs_proj_args ise pc f u in if n < np then -1 else np
| _ -> -1 in
if np < na then fpats else
let () = if !i0 < np then i0 := n in (u, np) :: fpats
@@ -568,7 +572,7 @@ let match_upats_HO ~on_instance upats env sigma0 ise c =
let failed_because_of_TC = ref false in
let rec aux upats env sigma0 ise c =
let f, a = splay_app ise c in let i0 = ref (-1) in
- let fpats = List.fold_right (filter_upat i0 f (Array.length a)) upats [] in
+ let fpats = List.fold_right (filter_upat ise i0 f (Array.length a)) upats [] in
while !i0 >= 0 do
let i = !i0 in i0 := -1;
let one_match (u, np) =
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 10:49:51 +0000