(************************************************************************) (* * The Rocq Prover / The Rocq 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) *) (************************************************************************)
open Pp open CErrors open Util open Names open Constr open Context open EConstr open Vars open Tacticals open Tactics open Pretype_errors open Evd open Tactypes open Locus open Locusops open Elimschemes open Environ open Termops open EConstr open Proofview.Notations open Context.Named.Declaration
let bind_global lib s = let gr = lazy (Rocqlib.lib_ref (lib ^ "." ^ s)) in fun env (evd,cstrs) -> let (evd, c) = Evd.fresh_global env evd (Lazy.force gr) in
(evd, cstrs), c
(** Utility for dealing with polymorphic applications *)
(** Global constants. *)
let rocq_eq_ref () = Rocqlib.lib_ref "core.eq.type" let rocq_eq = bind_global "core.eq""type" let rocq_f_equal = bind_global "core.eq""congr" let rocq_all = bind_global "core""all" let impl = bind_global "core""impl"
let default_relation = bind_global "rewrite""DefaultRelation"
(** Bookkeeping which evars are constraints so that we can
remove them at the end of the tactic. *)
let goalevars evars = fst evars let cstrevars evars = snd evars
let new_cstr_evar (evd,cstrs) env t = (* We handle the typeclass resolution of constraints ourselves *) let (evd', t) = Evarutil.new_evar env evd ~typeclass_candidate:false t in let ev, _ = destEvar evd' t in
(evd', Evar.Set.add ev cstrs), t
(** Building or looking up instances. *)
let extends_undefined evars evars' = let f ev evi found = found || not (Evd.mem evars ev) in fold_undefined f evars' false
let app_poly_check env evars f args = let (evars, cstrs), fc = f env evars in let evars, t = Typing.checked_appvect env evars fc args in
(evars, cstrs), t
let app_poly_nocheck env evars f args = let evars, fc = f env evars in
evars, mkApp (fc, args)
let app_poly_sort b = if b then app_poly_nocheck else app_poly_check
let find_class_proof proof_type proof_method env evars carrier relation = try let evars, goal = app_poly_check env evars proof_type [| carrier ; relation |] in let evars', c = Class_tactics.resolve_one_typeclass env (goalevars evars) goal in if extends_undefined (goalevars evars) evars' then raise Not_found else app_poly_check env (evars',cstrevars evars) proof_method [| carrier; relation; c |] with e when CErrors.noncritical e -> raise Not_found
let eq_pb (ty, env, x, y as pb) (ty', env', x', y' as pb') = let equal x y = Constr.equal (EConstr.Unsafe.to_constr x) (EConstr.Unsafe.to_constr y) in
pb == pb' || (ty == ty' && equal x x' && equal y y')
let problem_inclusion x y = List.for_all (fun pb -> List.exists (fun pb' -> eq_pb pb pb') y) x
let evd_convertible env evd x y = try (* Unfortunately, the_conv_x might say they are unifiable even if some unsolvable constraints remain, so we check that this unification
does not introduce any new problem. *) let _, pbs = Evd.extract_all_conv_pbs evd in let evd' = Evarconv.unify_delay env evd x y in let _, pbs' = Evd.extract_all_conv_pbs evd'in if evd' == evd || problem_inclusion pbs' pbs then Some evd' else None with e when CErrors.noncritical e -> None
let error_no_relation () = user_err Pp.(str "Cannot find a relation to rewrite.")
let rec decompose_app_rel env evd t = (* Head normalize for compatibility with the old meta mechanism *) let t = Reductionops.whd_betaiota env evd t in match EConstr.kind evd t with
| App (f, [||]) -> assert false
| App (f, [|arg|]) -> (* This treats the special case `g (R x y)`, turning it into
the relation `(fun x y => g (R x y))`. Useful when g is negation in particular. *) let (f', argl, argr) = decompose_app_rel env evd arg in let ty = Retyping.get_type_of env evd argl in let ty' = Retyping.get_type_of env evd argr in let r = Retyping.relevance_of_type env evd ty in let r' = Retyping.relevance_of_type env evd ty'in let f'' = mkLambda (make_annot (Name Namegen.default_dependent_ident) r, ty,
mkLambda (make_annot (Name (Id.of_string "y")) r', lift 1 ty',
mkApp (lift 2 f, [| mkApp (lift 2 f', [| mkRel 2; mkRel 1 |]) |]))) in (f'', argl, argr)
| App (f, args) -> let len = Array.length args in let fargs = Array.sub args 0 (Array.length args - 2) in let rel = mkApp (f, fargs) in
rel, args.(len - 2), args.(len - 1)
| _ -> error_no_relation ()
let decompose_app_rel env evd t = let (rel, t1, t2) = decompose_app_rel env evd t in let ty = try Retyping.get_type_of ~lax:true env evd rel with Retyping.RetypeError _ -> error_no_relation () in ifnot (Reductionops.is_arity env evd ty) then None else match Reductionops.splay_arity env evd ty with
| [_, ty2; _, ty1], concl -> if noccurn evd 1 ty2 then
Some (rel, ty1, subst1 mkProp ty2, concl, t1, t2) else None
| _ -> assert false
let decompose_app_rel_error env evd t = match decompose_app_rel env evd t with
| Some e -> e
| None -> error_no_relation ()
let decompose_applied_relation env sigma (c,l) = letopen Context.Rel.Declaration in let ctype = Retyping.get_type_of env sigma c in let find_rel ty = let sigma, cl = EClause.make_evar_clause env sigma ty in let sigma = EClause.solve_evar_clause env sigma true cl l in let { EClause.cl_holes = holes; EClause.cl_concl = t } = cl in match decompose_app_rel env sigma t with
| None -> None
| Some (equiv, ty1, ty2, concl, c1, c2) -> match evd_convertible env sigma ty1 ty2 with
| None -> None
| Some sigma -> let args = Array.map_of_list (fun h -> h.EClause.hole_evar) holes in let value = mkApp (c, args) in
Some (sigma, { prf=value;
car=ty1; rel = equiv; sort = Sorts.is_prop (ESorts.kind sigma concl);
c1=c1; c2=c2; holes }) in match find_rel ctype with
| Some c -> c
| None -> let ctx,t' = Reductionops.whd_decompose_prod env sigma ctype in (* Search for underlying eq *) let t' = it_mkProd_or_LetIn t' (List.map (fun (n,t) -> LocalAssum (n, t)) ctx) in match find_rel t' with
| Some c -> c
| None -> user_err Pp.(str "Cannot find a homogeneous relation to rewrite.")
(** Utility functions *)
module GlobalBindings (M : sig val prefix : string val app_poly : env -> evars -> (env -> evars -> evars * constr) -> constr array -> evars * constr val arrow : env -> evars -> evars * constr end) = struct open M open Context.Rel.Declaration
let bind_rewrite s = bind_global prefix s let bind_rewrite_ref s = bind_global_ref prefix s
let reflexive_type = bind_rewrite "Reflexive" let reflexive_proof = bind_rewrite "reflexivity"
let symmetric_type = bind_rewrite "Symmetric" let symmetric_proof = bind_rewrite "symmetry"
let transitive_type = bind_rewrite "Transitive" let transitive_proof = bind_rewrite "transitivity"
let forall_relation = bind_rewrite "forall_relation" let pointwise_relation = bind_rewrite "pointwise_relation"
let forall_relation_ref = bind_global_ref prefix "forall_relation" let pointwise_relation_ref = bind_global_ref prefix "pointwise_relation"
let respectful = bind_rewrite "respectful"
let rocq_forall = bind_rewrite "forall_def"
let subrelation = bind_rewrite "subrelation" let do_subrelation = bind_rewrite "do_subrelation" let apply_subrelation = bind_rewrite "apply_subrelation"
let rewrite_relation_class = bind_rewrite "RewriteRelation"
let proper_class = let r = lazy (bind_rewrite_ref "Proper" ()) in fun () -> Option.get (TC.class_info (Lazy.force r))
let proper_proxy_class = let r = lazy (bind_rewrite_ref "ProperProxy" ()) in fun () -> Option.get (TC.class_info (Lazy.force r))
let proper_proj () = bind_rewrite_ref "proper_prf" ()
let proper_type env (sigma,cstrs) = let l = (proper_class ()).TC.cl_impl in let (sigma, c) = Evd.fresh_global env sigma l in
(sigma, cstrs), c
let proper_proxy_type env (sigma,cstrs) = let l = (proper_proxy_class ()).TC.cl_impl in let (sigma, c) = Evd.fresh_global env sigma l in
(sigma, cstrs), c
let proper_proof env evars carrier relation x = let evars, goal = app_poly env evars proper_proxy_type [| carrier ; relation; x |] in
new_cstr_evar evars env goal
let get_reflexive_proof env = find_class_proof reflexive_type reflexive_proof env let get_symmetric_proof env = find_class_proof symmetric_type symmetric_proof env let get_transitive_proof env = find_class_proof transitive_type transitive_proof env
let mk_relation env evars ty = let evars', ty = Evarsolve.refresh_universes ~onlyalg:true ~status:(Evd.UnivFlexible false)
(Some false) env (fst evars) ty in
app_poly env (evars', snd evars) relation [| ty |]
(** Build an inferred signature from constraints on the arguments and expected output
relation *)
let build_signature evars env m (cstrs : (types * types option) optionlist)
(finalcstr : (types * types option) option) = let mk_relty evars newenv ty obj = match obj with
| None | Some (_, None) -> let evars, relty = mk_relation newenv evars ty in if closed0 (goalevars evars) ty then let env' = Environ.reset_with_named_context (Environ.named_context_val env) env in
new_cstr_evar evars env' relty else new_cstr_evar evars newenv relty
| Some (x, Some rel) -> evars, rel in let rec aux env evars ty l = let t = Reductionops.whd_all env (goalevars evars) ty in match EConstr.kind (goalevars evars) t, l with
| Prod (na, ty, b), obj :: cstrs -> let b = Reductionops.nf_betaiota env (goalevars evars) b in if noccurn (goalevars evars) 1 b (* non-dependent product *) then let ty = Reductionops.nf_betaiota env (goalevars evars) ty in let (evars, b', arg, cstrs) = aux env evars (subst1 mkProp b) cstrs in let evars, relty = mk_relty evars env ty obj in let evars', b' = Evarsolve.refresh_universes ~onlyalg:true ~status:(Evd.UnivFlexible false)
(Some false) env (fst evars) b' in let evars, newarg = app_poly env (evars', snd evars) respectful [| ty ; b' ; relty ; arg |] in
evars, mkProd(na, ty, b), newarg, (ty, Some relty) :: cstrs else let (evars, b, arg, cstrs) =
aux (push_rel (LocalAssum (na, ty)) env) evars b cstrs in let ty = Reductionops.nf_betaiota env (goalevars evars) ty in let pred = mkLambda (na, ty, b) in let liftarg = mkLambda (na, ty, arg) in let evars, arg' = app_poly env evars forall_relation [| ty ; pred ; liftarg |] in ifOption.is_empty obj then evars, mkProd(na, ty, b), arg', (ty, None) :: cstrs else user_err Pp.(str "build_signature: no constraint can apply on a dependent argument")
| _, obj :: _ -> anomaly ~label:"build_signature" (Pp.str "not enough products.")
| _, [] ->
(match finalcstr with
| None | Some (_, None) -> let t = Reductionops.nf_betaiota env (fst evars) ty in let evars, rel = mk_relty evars env t None in
evars, t, rel, [t, Some rel]
| Some (t, Some rel) -> evars, t, rel, [t, Some rel]) in aux env evars m cstrs
(** Folding/unfolding of the tactic constants. *)
let unfold_impl n sigma t = match EConstr.kind sigma t with
| App (arrow, [| a; b |])(* when eq_constr arrow (Lazy.force impl) *) ->
mkProd (make_annot n ERelevance.relevant, a, lift 1 b)
| _ -> assert false
let unfold_all sigma t = match EConstr.kind sigma t with
| App (id, [| a; b |]) (* when eq_constr id (Lazy.force rocq_all) *) ->
(match EConstr.kind sigma b with
| Lambda (n, ty, b) -> mkProd (n, ty, b)
| _ -> assert false)
| _ -> assert false
let unfold_forall sigma t = match EConstr.kind sigma t with
| App (id, [| a; b |]) (* when eq_constr id (Lazy.force rocq_all) *) ->
(match EConstr.kind sigma b with
| Lambda (n, ty, b) -> mkProd (n, ty, b)
| _ -> assert false)
| _ -> assert false
let arrow_morphism env evd n ta tb a b = let ap = is_Prop (goalevars evd) ta and bp = is_Prop (goalevars evd) tb in if ap && bp then app_poly env evd impl [| a; b |], unfold_impl n elseif ap then(* Domain in Prop, CoDomain in Type *)
(app_poly env evd arrow [| a; b |]), unfold_impl n (* (evd, mkProd (Anonymous, a, b)), (fun x -> x) *) elseif bp then(* Dummy forall *)
(app_poly env evd rocq_all [| a; mkLambda (make_annot n ERelevance.relevant, a, lift 1 b) |]), unfold_forall else(* None in Prop, use arrow *)
(app_poly env evd arrow [| a; b |]), unfold_impl n
let rec decomp_pointwise env sigma n c = if Int.equal n 0 then Some c else match EConstr.kind sigma c with
| App (f, [| a; b; relb |]) when isRefX env sigma (pointwise_relation_ref ()) f ->
decomp_pointwise env sigma (pred n) relb
| App (f, [| a; b; arelb |]) when isRefX env sigma (forall_relation_ref ()) f ->
decomp_pointwise env sigma (pred n) (Reductionops.beta_applist sigma (arelb, [mkRel 1]))
| _ -> (* cf #11347: when rewriting a commutative cut, we decomp_pointwise on "c := eq (Prop -> Prop)"
Maybe if funext is available it's possible to do something? *)
None
let refresh_univs env evars ty = let evars', ty = Evarsolve.refresh_universes ~onlyalg:true ~status:(Evd.UnivFlexible false)
(Some false) env (fst evars) ty in
(evars', snd evars), ty
let pointwise_or_dep_relation env evars n t car rel = let evars, car = refresh_univs env evars car in if noccurn (goalevars evars) 1 car && noccurn (goalevars evars) 1 rel then
app_poly env evars pointwise_relation [| t; lift (-1) car; lift (-1) rel |] else
app_poly env evars forall_relation
[| t; mkLambda (make_annot n ERelevance.relevant, t, car);
mkLambda (make_annot n ERelevance.relevant, t, rel) |]
let lift_cstr env evars (args : constr list) c ty cstr = let start evars env car = match cstr with
| None | Some (_, None) -> let evars, rel = mk_relation env evars car in
new_cstr_evar evars env rel
| Some (ty, Some rel) -> evars, rel in let rec aux evars env prod n = if Int.equal n 0 then start evars env prod else let sigma = goalevars evars in match EConstr.kind sigma (Reductionops.whd_all env sigma prod) with
| Prod (na, ty, b) -> if noccurn sigma 1 b then let b' = lift (-1) b in let evars, rb = aux evars env b' (pred n) in
app_poly env evars pointwise_relation [| ty; b'; rb |] else let evars, rb = aux evars (push_rel (LocalAssum (na, ty)) env) b (pred n) in
app_poly env evars forall_relation
[| ty; mkLambda (na, ty, b); mkLambda (na, ty, rb) |]
| _ -> raise Not_found in let rec find env c ty = function
| [] -> None
| arg :: args -> trylet evars, found = aux evars env ty (succ (List.length args)) in
Some (evars, found, c, ty, arg :: args) with Not_found -> let sigma = goalevars evars in let ty = Reductionops.whd_all env sigma ty in find env (mkApp (c, [| arg |])) (prod_applist sigma ty [arg]) args infind env c ty args
let unlift_cstr env sigma = function
| None -> None
| Some codom -> decomp_pointwise env (goalevars sigma) 1 codom
(** Looking up declared rewrite relations (instances of [RewriteRelation]) *) let is_applied_rewrite_relation env sigma rels t = match EConstr.kind sigma t with
| App (c, args) when Array.length args >= 2 -> let head = if isApp sigma c then fst (destApp sigma c) else c in if isRefX env sigma (rocq_eq_ref ()) head then None else
(try let env' = push_rel_context rels env in match decompose_app_rel env' sigma t with
| None -> None
| Some (equiv, ty1, ty2, concl, c1, c2) -> let (evars, evset), inst =
app_poly env' (sigma,Evar.Set.empty)
rewrite_relation_class [| ty1; equiv |] in let sigma, _ = Class_tactics.resolve_one_typeclass env' evars inst in (* We check that the relation is homogeneous *after* launching resolution, as this convertibility test might be expensive in general (e.g. this
slows down mathcomp-odd-order). *) match evd_convertible env sigma ty1 ty2 with
| None -> None
| Some sigma -> Some (it_mkProd_or_LetIn t rels) with e when CErrors.noncritical e -> None)
| _ -> None
end
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
(evd', cstrevars evars), c
module PropGlobal = struct
module Consts = struct let prefix = "rewrite.prop" let app_poly = app_poly_nocheck let arrow = bind_global "core""arrow" let rocq_inverse = bind_global "core""flip" end
module G = GlobalBindings(Consts)
include G
include Consts let inverse env evd car rel =
type_app_poly env env evd rocq_inverse [| car ; car; mkProp; rel |] (* app_poly env evd rocq_inverse [| car ; car; mkProp; rel |] *)
end
module TypeGlobal = struct
module Consts = struct let prefix = "rewrite.type" let app_poly = app_poly_check let arrow = bind_global prefix "arrow" let rocq_inverse = bind_global prefix "flip" end
module G = GlobalBindings(Consts)
include G
include Consts
let inverse env (evd,cstrs) car rel = let evd, car = Evarsolve.refresh_universes ~onlyalg:true (Some false) env evd car in let (evd, sort) = Evarutil.new_Type ~rigid:Evd.univ_flexible evd in
app_poly_check env (evd,cstrs) rocq_inverse [| car ; car; sort; rel |]
end
(* Check that relation constants have been registered *) let init_relation_classes () = if Rocqlib.has_ref "rewrite.prop.relation" || Rocqlib.has_ref "rewrite.type.relation"then () else CErrors.user_err
(Pp.str "No bindings have been registered for relation classes in Prop or Type, maybe you need to require Corelib.Classes.(C)RelationClasses.")
let init_rewrite () = if Rocqlib.has_ref "rewrite.prop.Proper" || Rocqlib.has_ref "rewrite.type.Proper"then() else CErrors.user_err
(Pp.str "No bindings have been registered for morphisms in Prop or Type, maybe you need to require Corelib.Classes.(C)Morphisms.")
let get_type_of_refresh env evars t = let evars', tty = Evarsolve.get_type_of_refresh env (fst evars) t in
(evars', snd evars), tty
(* Flags used for the setoid variant of "rewrite" and for the strategies "hints"/"old_hints"/"terms" of "rewrite_strat", and for solving pre-existing
evars in "rewrite" (see unify_abs) *) let rewrite_unif_flags = let flags = rewrite_core_unif_flags in {
Unification.core_unify_flags = flags;
Unification.merge_unify_flags = flags;
Unification.subterm_unify_flags = flags;
Unification.allow_K_in_toplevel_higher_order_unification = true;
Unification.resolve_evars = true
}
let rewrite_core_conv_unif_flags = {
rewrite_core_unif_flags with
Unification.modulo_conv_on_closed_terms = Some conv_transparent_state;
Unification.modulo_delta_types = conv_transparent_state;
Unification.modulo_betaiota = true
}
(* Fallback flags for the setoid variant of "rewrite" *) let rewrite_conv_unif_flags = let flags = rewrite_core_conv_unif_flags in {
Unification.core_unify_flags = flags;
Unification.merge_unify_flags = flags;
Unification.subterm_unify_flags = flags;
Unification.allow_K_in_toplevel_higher_order_unification = true;
Unification.resolve_evars = true
}
(* Flags for "setoid_rewrite c"/"rewrite_strat -> c" *) let general_rewrite_unif_flags () = let ts = rewrite_transparent_state () in let core_flags =
{ rewrite_core_unif_flags with
Unification.modulo_conv_on_closed_terms = Some ts;
Unification.use_evars_eagerly_in_conv_on_closed_terms = true;
Unification.modulo_delta = ts;
Unification.modulo_delta_types = TransparentState.full;
Unification.modulo_betaiota = true } in {
Unification.core_unify_flags = core_flags;
Unification.merge_unify_flags = core_flags;
Unification.subterm_unify_flags = { core_flags with Unification.modulo_delta = TransparentState.empty };
Unification.allow_K_in_toplevel_higher_order_unification = true;
Unification.resolve_evars = true
}
(** FIXME: write this in the new monad interface *) let solve_remaining_by env sigma holes by = match by with
| None -> sigma
| Some tac -> letmap h = if h.EClause.hole_deps then None elsematch EConstr.kind sigma h.EClause.hole_evar with
| Evar (evk, _) ->
Some evk
| _ -> None in (* Only solve independent holes *) let indep = List.map_filter map holes in let solve_tac = tclCOMPLETE (Gentactic.interp tac) in let solve sigma evk = let evi = try Some (Evd.find_undefined sigma evk) with Not_found -> None in match evi with
| None -> sigma (* Evar should not be defined, but just in case *)
| Some evi -> let env = Evd.evar_env env evi in let ty = Evd.evar_concl evi in let name, poly = Id.of_string "rewrite", falsein let c, sigma = Proof.refine_by_tactic ~name ~poly env sigma ty solve_tac in
Evd.define evk c sigma in List.fold_left solve sigma indep
let no_constraints cstrs = fun ev _ -> not (Evar.Set.mem ev cstrs)
let poly_inverse sort = if sort then PropGlobal.inverse else TypeGlobal.inverse
type rewrite_proof =
| RewPrf of constr * constr (** A Relation (R : rew_car -> rew_car -> Prop) and a proof of R rew_from rew_to *)
| RewCast of cast_kind (** A proof of convertibility (with casts) *)
type rewrite_result_info = {
rew_car : constr ; (** A type *)
rew_from : constr ; (** A term of type rew_car *)
rew_to : constr ; (** A term of type rew_car *)
rew_prf : rewrite_proof ; (** A proof of rew_from == rew_to *)
rew_evars : evars;
}
type rewrite_result =
| Fail
| Identity
| Success of rewrite_result_info
type'a strategy_input = { state : 'a ; (* a parameter: for instance, a state *)
env : Environ.env ;
unfresh : Id.Set.t; (* Unfresh names *)
term1 : constr ;
ty1 : types ; (* first term and its type (convertible to rew_from) *)
cstr : (bool(* prop *) * constr option) ;
evars : evars }
type'a pure_strategy = { strategy : 'a strategy_input -> 'a * rewrite_result (* the updated state and the "result" *) }
type strategy = unit pure_strategy
let symmetry env sort rew = let { rew_evars = evars; rew_car = car; } = rew in let (rew_evars, rew_prf) = match rew.rew_prf with
| RewCast _ -> (rew.rew_evars, rew.rew_prf)
| RewPrf (rel, prf) -> try let evars, symprf = get_symmetric_proof sort env evars car rel in let prf = mkApp (symprf, [| rew.rew_from ; rew.rew_to ; prf |]) in
(evars, RewPrf (rel, prf)) with Not_found -> let evars, rel = poly_inverse sort env evars car rel in
(evars, RewPrf (rel, prf)) in
{ rew with rew_from = rew.rew_to; rew_to = rew.rew_from; rew_prf; rew_evars; }
(* Matching/unifying the rewriting rule against [t] *) let unify_eqn { car; rel; prf; c1; c2; holes; sort } l2r flags env (sigma, cstrs) by t = try let left = if l2r then c1 else c2 in let _, sigma = Unification.w_unify ~flags env sigma CONV left t in let sigma = TC.resolve_typeclasses ~filter:(no_constraints cstrs)
~fail:true env sigma in let sigma = solve_remaining_by env sigma holes by in let nf c = Reductionops.nf_evar sigma c in let c1 = nf c1 and c2 = nf c2 and rew_car = nf car and rel = nf rel and prf = nf prf in let ty1 = Retyping.get_type_of env sigma c1 in let ty2 = Retyping.get_type_of env sigma c2 in beginmatch Reductionops.infer_conv ~pb:CUMUL env sigma ty2 ty1 with
| None -> None
| Some sigma -> let rew_evars = sigma, cstrs in let rew_prf = RewPrf (rel, prf) in let rew = { rew_evars; rew_prf; rew_car; rew_from = c1; rew_to = c2; } in let rew = if l2r then rew else symmetry env sort rew in
Some rew end with
| e when noncritical e -> None
let unify_abs (car, rel, prf, c1, c2) l2r sort env (sigma, cstrs) t = try let left = if l2r then c1 else c2 in (* The pattern is already instantiated, so the next w_unify is basically an eq_constr, except when preexisting evars occur in either the lemma or the goal, in which case the eq_constr also
solved this evars *) let _, sigma = Unification.w_unify ~flags:rewrite_unif_flags env sigma CONV left t in let rew_evars = sigma, cstrs in let rew_prf = RewPrf (rel, prf) in let rew = { rew_car = car; rew_from = c1; rew_to = c2; rew_prf; rew_evars; } in let rew = if l2r then rew else symmetry env sort rew in
Some rew with
| e when noncritical e -> None
let get_opt_rew_rel = function RewPrf (rel, prf) -> Some rel | _ -> None
let new_global env (evars, cstrs) gr = let (sigma,c) = Evd.fresh_global env evars gr in
(sigma, cstrs), c
let make_eq env sigma =
new_global env sigma Rocqlib.(lib_ref "core.eq.type") let make_eq_refl env sigma =
new_global env sigma Rocqlib.(lib_ref "core.eq.refl")
let get_rew_prf env evars r = match r.rew_prf with
| RewPrf (rel, prf) -> evars, (rel, prf)
| RewCast c -> let evars, eq = make_eq env evars in let evars, eq_refl = make_eq_refl env evars in let rel = mkApp (eq, [| r.rew_car |]) in
evars, (rel, mkCast (mkApp (eq_refl, [| r.rew_car; r.rew_from |]),
c, mkApp (rel, [| r.rew_from; r.rew_to |])))
let poly_subrelation sort = if sort then PropGlobal.subrelation else TypeGlobal.subrelation
let resolve_subrelation env car rel sort prf rel' res = if Termops.eq_constr env (fst res.rew_evars) rel rel' then res else let evars, app = app_poly_check env res.rew_evars (poly_subrelation sort) [|car; rel; rel'|] in let evars, subrel = new_cstr_evar evars env appin let appsub = mkApp (subrel, [| res.rew_from ; res.rew_to ; prf |]) in
{ res with
rew_prf = RewPrf (rel', appsub);
rew_evars = evars }
let resolve_morphism env m args args' (b,cstr) evars = let evars, proj, sigargs, m', args, args' = let first = match (Array.findi (fun _ b -> not (Option.is_empty b)) args') with
| Some i -> i
| None -> invalid_arg "resolve_morphism"in let morphargs, morphobjs = Array.chop first args in let morphargs', morphobjs' = Array.chop first args' in let appm = mkApp(m, morphargs) in let evd, appmtype = Typing.type_of env (goalevars evars) appm in let evars = evd, snd evars in let cstrs = List.map
(Option.map (fun r -> r.rew_car, get_opt_rew_rel r.rew_prf))
(Array.to_list morphobjs') in (* Desired signature *) let evars, appmtype', signature, sigargs = if b then PropGlobal.build_signature evars env appmtype cstrs cstr else TypeGlobal.build_signature evars env appmtype cstrs cstr in (* Actual signature found *) let evars', appmtype' = Evarsolve.refresh_universes ~status:(Evd.UnivFlexible false) ~onlyalg:true
(Some false) env (fst evars) appmtype' in let cl_args = [| appmtype' ; signature ; appm |] in let evars, app = app_poly_sort b env (evars', snd evars) (if b then PropGlobal.proper_type else TypeGlobal.proper_type)
cl_args in let dosub, appsub = if b then PropGlobal.do_subrelation, PropGlobal.apply_subrelation else TypeGlobal.do_subrelation, TypeGlobal.apply_subrelation in let _, dosub = app_poly_sort b env evars dosub [||] in let _, appsub = app_poly_nocheck env evars appsub [||] in let dosub_id = Id.of_string "do_subrelation"in let env' = EConstr.push_named (LocalDef (make_annot dosub_id ERelevance.relevant, dosub, appsub)) env in let evars, morph = new_cstr_evar evars env' app in (* Replace the free [dosub_id] in the evar by the global reference *) let morph = Vars.replace_vars (fst evars) [dosub_id , dosub] morph in
evars, morph, sigargs, appm, morphobjs, morphobjs' in let projargs, subst, evars, respars, typeargs =
Array.fold_left2
(fun (acc, subst, evars, sigargs, typeargs') x y -> let (carrier, relation), sigargs = split_head sigargs in match relation with
| Some relation -> let carrier = substl subst carrier and relation = substl subst relation in
(match y with
| None -> let evars, proof =
(if b then PropGlobal.proper_proof else TypeGlobal.proper_proof)
env evars carrier relation x in
[ proof ; x ; x ] @ acc, subst, evars, sigargs, x :: typeargs'
| Some r -> let evars, proof = get_rew_prf env evars r in
[ snd proof; r.rew_to; x ] @ acc, subst, evars,
sigargs, r.rew_to :: typeargs')
| None -> ifnot (Option.is_empty y) then
user_err Pp.(str "Cannot rewrite inside dependent arguments of a function");
x :: acc, x :: subst, evars, sigargs, x :: typeargs')
([], [], evars, sigargs, []) args args' in let proof = applist (proj, List.rev projargs) in let newt = applist (m', List.rev typeargs) in match respars with
[ a, Some r ] -> evars, proof, substl subst a, substl subst r, newt
| _ -> assert(false)
let apply_constraint env car rel prf cstr res = match snd cstr with
| None -> res
| Some r -> resolve_subrelation env car rel (fst cstr) prf r res
let coerce env cstr res = let evars, (rel, prf) = get_rew_prf env res.rew_evars res in let res = { res with rew_evars = evars } in
apply_constraint env res.rew_car rel prf cstr res
let apply_rule unify : occurrences_count pure_strategy =
{ strategy = fun { state = occs ; env ;
term1 = t ; ty1 = ty ; cstr ; evars } -> let unif = if isEvar (goalevars evars) t then None else unify env evars t in match unif with
| None -> (occs, Fail)
| Some rew -> let b, occs = update_occurrence_counter occs in ifnot b then (occs, Fail) elseif Termops.eq_constr env (fst rew.rew_evars) t rew.rew_to then (occs, Identity) else let res = { rew with rew_car = ty } in let res = Success (coerce env cstr res) in
(occs, res)
}
let with_no_bindings (c : delayed_open_constr) : delayed_open_constr_with_bindings =
(); fun env sigma -> let (sigma, c) = c env sigma in
(sigma, (c, NoBindings))
let apply_lemma l2r flags oc by loccs : strategy = let oc = with_no_bindings oc in let strategy ({ state = () ; env ; term1 = t ; evars = (sigma, cstrs) } as input) = let sigma, c = oc env sigma in let sigma, rew = decompose_applied_relation env sigma c in let evars = (sigma, cstrs) in let unify env evars t = let rew = unify_eqn rew l2r flags env evars by t in match rew with
| None -> None
| Some rew -> Some rew in let loccs, res = (apply_rule unify).strategy {
input with
state = initialize_occurrence_counter loccs ;
evars
} in
check_used_occurrences loccs;
(), res
in {strategy}
let e_app_poly env evars f args = let evars', c = app_poly_nocheck env !evars f args in
evars := evars';
c
let make_leibniz_proof env c ty r = let evars = ref r.rew_evars in let prf = match r.rew_prf with
| RewPrf (rel, prf) -> let rel = e_app_poly env evars rocq_eq [| ty |] in let prf =
e_app_poly env evars rocq_f_equal
[| r.rew_car; ty;
mkLambda (make_annot Anonymous ERelevance.relevant, r.rew_car, c);
r.rew_from; r.rew_to; prf |] in RewPrf (rel, prf)
| RewCast k -> r.rew_prf in
{ rew_car = ty; rew_evars = !evars;
rew_from = subst1 r.rew_from c; rew_to = subst1 r.rew_to c; rew_prf = prf }
let fold_match ?(force=false) env sigma c = letcase = destCase sigma c in let (ci, (p,_), iv, c, brs) = EConstr.expand_case env sigma casein let cty = Retyping.get_type_of env sigma c in let dep, pred, sk = let env', ctx, body = let ctx, pred = decompose_lambda_decls sigma p in let env' = push_rel_context ctx env in
env', ctx, pred in let sortp = Retyping.get_sort_quality_of env' sigma body in let sortc = Retyping.get_sort_quality_of env sigma cty in let dep = not (noccurn sigma 1 body) in let pred = if dep then p else
it_mkProd_or_LetIn (subst1 mkProp body) (List.tl ctx) in let sk = (* not sure how correct this is *) if UnivGen.QualityOrSet.is_prop sortp then if UnivGen.QualityOrSet.is_prop sortc then if dep then case_dep else case_nodep else ( if dep then casep_dep else case_nodep (* should this be casep_nodep? *)) else ((* sortc <> InProp by typing *) if dep then case_dep else case_nodep) in match Ind_tables.lookup_scheme sk ci.ci_ind with
| Some cst ->
dep, pred, cst
| None -> raise Not_found in letapp = let sk = if Global.is_polymorphic (ConstRef sk) then CErrors.anomaly Pp.(str "Unexpected univ poly in Rewrite.fold_match") else UnsafeMonomorphic.mkConst sk in let ind, args = Inductiveops.find_mrectype env sigma cty in let pars, args = List.chop ci.ci_npar args in let meths = Array.to_list brs in
applist (sk, pars @ [pred] @ meths @ args @ [c]) in
sk, app
let unfold_match env sigma sk app = match EConstr.kind sigma appwith
| App (f', args) when QConstant.equal env (fst (destConst sigma f')) sk -> let v = Environ.constant_value_in env (sk,UVars.Instance.empty)(*FIXME*) in let v = EConstr.of_constr v in
Reductionops.whd_beta env sigma (mkApp (v, args))
| _ -> app
let is_rew_cast = function RewCast _ -> true | _ -> false
let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = let aux { state ; env ; unfresh ;
term1 = t ; ty1 = ty ; cstr = (prop, cstr) ; evars } = let cstr' = Option.map (fun c -> (ty, Some c)) cstr in match EConstr.kind (goalevars evars) t with
| App (m, args) -> let rewrite_args state success = let state, (args', evars', progress) =
Array.fold_left
(fun (state, (acc, evars, progress)) arg -> ifnot (Option.is_empty progress) && notallthen
state, (None :: acc, evars, progress) else let evars, argty = get_type_of_refresh env evars arg in let state, res = s.strategy { state ; env ;
unfresh ;
term1 = arg ; ty1 = argty ;
cstr = (prop,None) ;
evars } in let res' = match res with
| Identity -> let progress = ifOption.is_empty progress then Some falseelse progress in
(None :: acc, evars, progress)
| Success r ->
(Some r :: acc, r.rew_evars, Some true)
| Fail -> (None :: acc, evars, progress) in state, res')
(state, ([], evars, success)) args in let res = match progress with
| None -> Fail
| Some false -> Identity
| Some true -> let args' = Array.of_list (List.rev args') in if Array.exists
(function
| None -> false
| Some r -> not (is_rew_cast r.rew_prf)) args' then let evars', prf, car, rel, c2 =
resolve_morphism env m args args' (prop, cstr') evars' in let res = { rew_car = ty; rew_from = t;
rew_to = c2; rew_prf = RewPrf (rel, prf);
rew_evars = evars' } in Success res else let args' = Array.map2
(fun aorig anew -> match anew with None -> aorig
| Some r -> r.rew_to) args args' in let res = { rew_car = ty; rew_from = t;
rew_to = mkApp (m, args'); rew_prf = RewCast DEFAULTcast;
rew_evars = evars' } in Success res in state, res in if flags.on_morphisms then let evars, mty = get_type_of_refresh env evars m in let evars, cstr', m, mty, argsl, args = let argsl = Array.to_list args in let lift = if prop then PropGlobal.lift_cstr else TypeGlobal.lift_cstr in match lift env evars argsl m mty None with
| Some (evars, cstr', m, mty, args) ->
evars, Some cstr', m, mty, args, Array.of_list args
| None -> evars, None, m, mty, argsl, args in let state, m' = s.strategy { state ; env ; unfresh ;
term1 = m ; ty1 = mty ;
cstr = (prop, cstr') ; evars } in match m' with
| Fail -> rewrite_args state None (* Standard path, try rewrite on arguments *)
| Identity -> rewrite_args state (Some false)
| Success r -> (* We rewrote the function and get a proof of pointwise rel for the arguments.
We just apply it. *) let prf = match r.rew_prf with
| RewPrf (rel, prf) -> letapp = if prop then PropGlobal.apply_pointwise else TypeGlobal.apply_pointwise in
RewPrf (app env (goalevars evars) rel argsl, mkApp (prf, args))
| x -> x in let res =
{ rew_car = Reductionops.hnf_prod_appvect env (goalevars evars) r.rew_car args;
rew_from = mkApp(r.rew_from, args); rew_to = mkApp(r.rew_to, args);
rew_prf = prf; rew_evars = r.rew_evars } in let res = match prf with
| RewPrf (rel, prf) ->
Success (apply_constraint env res.rew_car
rel prf (prop,cstr) res)
| _ -> Success res in state, res else rewrite_args state None
| Proj (p, r, arg) -> let expanded = Retyping.expand_projection env (fst evars) p arg [] in let hd, args = EConstr.destApp (fst evars) expanded in let arg = Array.last args in let evars, argty = get_type_of_refresh env evars arg in let input = {
state; env; unfresh;
term1 = arg; ty1 = argty;
cstr = (prop, None); evars } in let state, res = s.strategy input in let res = match res with
| Fail -> Fail
| Identity -> Identity
| Success res -> let evars = res.rew_evars in if is_rew_cast res.rew_prf then
Success { rew_car = ty; rew_from = t;
rew_to = mkProj (p, r, res.rew_to); rew_prf = RewCast DEFAULTcast;
rew_evars = evars } else let args' = Array.make (Array.length args) None in let () = args'.(Array.length args - 1) <- Some res in let evars, prf, _, rel, c2 =
resolve_morphism env hd args args' (prop, cstr') evars in let (_, args) = EConstr.destApp (goalevars evars) c2 in
Success { rew_car = ty; rew_from = t;
rew_to = mkProj (p, r, Array.last args); rew_prf = RewPrf (rel, prf);
rew_evars = evars } in
state, res
| Prod (n, x, b) when noccurn (goalevars evars) 1 b -> let b = subst1 mkProp b in let evars, tx = get_type_of_refresh env evars x in let evars, tb = get_type_of_refresh env evars b in let arr = if prop then PropGlobal.arrow_morphism else TypeGlobal.arrow_morphism in let (evars', mor), unfold = arr env evars n.binder_name tx tb x b in let state, res = s.strategy { state ; env ; unfresh ;
term1 = mor ; ty1 = ty ;
cstr = (prop,cstr) ; evars = evars' } in let res = match res with
| Success r -> Success { r with rew_to = unfold (goalevars r.rew_evars) r.rew_to }
| Fail | Identity -> res in state, res
| Prod (n, dom, codom) -> let lam = mkLambda (n, dom, codom) in let (evars', app), unfold = if eq_constr (fst evars) ty mkProp then
(app_poly_sort prop env evars rocq_all [| dom; lam |]), TypeGlobal.unfold_all else let forall = if prop then PropGlobal.rocq_forall else TypeGlobal.rocq_forall in
(app_poly_sort prop env evars forall [| dom; lam |]), TypeGlobal.unfold_forall in let state, res = s.strategy { state ; env ; unfresh ;
term1 = app ; ty1 = ty ;
cstr = (prop,cstr) ; evars = evars' } in let res = match res with
| Success r -> Success { r with rew_to = unfold (goalevars r.rew_evars) r.rew_to }
| Fail | Identity -> res in state, res
(* TODO: real rewriting under binders: introduce x x' (H : R x x') and rewrite with H at any occurrence of x. Ask for (R ==> R') for the lambda. Formalize this. B. Barras' idea is to have a context of relations, of length 1, with Σ for gluing dependent relations and using projections to get them out.
*)
| Lambda (n, t, b) when flags.under_lambdas -> let unfresh, n' = let id = match n.binder_name with
| Anonymous -> Namegen.default_dependent_ident
| Name id -> id in let id = Tactics.fresh_id_in_env unfresh id env in
Id.Set.add id unfresh, {n with binder_name = Name id} in let unfresh = match n'.binder_name with
| Anonymous -> unfresh
| Name id -> Id.Set.add id unfresh in letopen Context.Rel.Declaration in let env' = EConstr.push_rel (LocalAssum (n', t)) env in let bty = Retyping.get_type_of env' (goalevars evars) b in let unlift = if prop then PropGlobal.unlift_cstr else TypeGlobal.unlift_cstr in let state, b' = s.strategy { state ; env = env' ; unfresh ;
term1 = b ; ty1 = bty ;
cstr = (prop, unlift env evars cstr) ;
evars } in let res = match b' with
| Success r -> let r = match r.rew_prf with
| RewPrf (rel, prf) -> let point = if prop then PropGlobal.pointwise_or_dep_relation else
TypeGlobal.pointwise_or_dep_relation in let evars, rel = point env r.rew_evars n'.binder_name t r.rew_car rel in let prf = mkLambda (n', t, prf) in
{ r with rew_prf = RewPrf (rel, prf); rew_evars = evars }
| x -> r in
Success { r with
rew_car = mkProd (n, t, r.rew_car);
rew_from = mkLambda(n, t, r.rew_from);
rew_to = mkLambda (n, t, r.rew_to) }
| Fail | Identity -> b' in state, res
| Case (ci, u, pms, p, iv, c, brs) -> let (ci, (p,rp), iv, c, brs) = EConstr.expand_case env (goalevars evars) (ci, u, pms, p, iv, c, brs) in let cty = Retyping.get_type_of env (goalevars evars) c in let evars', eqty = app_poly_sort prop env evars rocq_eq [| cty |] in let cstr' = Some eqty in let state, c' = s.strategy { state ; env ; unfresh ;
term1 = c ; ty1 = cty ;
cstr = (prop, cstr') ; evars = evars' } in let state, res = match c' with
| Success r -> letcase = mkCase (EConstr.contract_case env (goalevars evars) (ci, (lift 1 p,rp), map_invert (lift 1) iv, mkRel 1, Array.map (lift 1) brs)) in let res = make_leibniz_proof env case ty r in
state, Success (coerce env (prop,cstr) res)
| Fail | Identity -> if Array.for_all (Int.equal 0) ci.ci_cstr_ndecls then let evars', eqty = app_poly_sort prop env evars rocq_eq [| ty |] in let cstr = Some eqty in let state, found, brs' = Array.fold_left
(fun (state, found, acc) br -> ifnot (Option.is_empty found) then
(state, found, fun x -> lift 1 br :: acc x) else let state, res = s.strategy { state ; env ; unfresh ;
term1 = br ; ty1 = ty ;
cstr = (prop,cstr) ; evars } in match res with
| Success r -> (state, Some r, fun x -> mkRel 1 :: acc x)
| Fail | Identity -> (state, None, fun x -> lift 1 br :: acc x))
(state, None, fun x -> []) brs in match found with
| Some r -> let ctxc = mkCase (EConstr.contract_case env (goalevars evars) (ci, (lift 1 p, rp), map_invert (lift 1) iv, lift 1 c, Array.of_list (List.rev (brs' c')))) in
state, Success (make_leibniz_proof env ctxc ty r)
| None -> state, c' else matchtry Some (fold_match env (goalevars evars) t) with Not_found -> None with
| None -> state, c'
| Some (cst, t') -> let state, res = s.strategy { state ; env ; unfresh ;
term1 = t' ; ty1 = ty ;
cstr = (prop,cstr) ; evars } in let res = match res with
| Success prf ->
Success { prf with
rew_from = t;
rew_to = unfold_match env (goalevars evars) cst prf.rew_to }
| x' -> c' in state, res in let res = match res with
| Success r -> Success (coerce env (prop,cstr) r)
| Fail | Identity -> res in state, res
| _ -> state, Fail in { strategy = aux }
(** Requires transitivity of the rewrite step, if not a reduction.
Not tail-recursive. *)
let transitivity state env unfresh cstr (res : rewrite_result_info) (next : 'a pure_strategy) : 'a * rewrite_result = let cstr = match cstr with
| _, Some _ -> cstr
| prop, None -> prop, get_opt_rew_rel res.rew_prf in let state, nextres =
next.strategy { state; env; unfresh; cstr;
term1 = res.rew_to;
ty1 = res.rew_car;
evars = res.rew_evars; } in let res = match nextres with
| Fail -> Fail
| Identity -> Success res
| Success res' -> match res.rew_prf with
| RewCast c -> Success { res' with rew_from = res.rew_from }
| RewPrf (rew_rel, rew_prf) -> match res'.rew_prf with
| RewCast _ -> Success { res with rew_to = res'.rew_to }
| RewPrf (res'_rel, res'_prf) -> let trans = if fst cstr then PropGlobal.transitive_type else TypeGlobal.transitive_type in let evars, prfty =
app_poly_sort (fst cstr) env res'.rew_evars trans [| res.rew_car; rew_rel |] in let evars, prf = new_cstr_evar evars env prfty in let prf = mkApp (prf, [|res.rew_from; res'.rew_from; res'.rew_to;
rew_prf; res'_prf |]) in Success { res' with rew_from = res.rew_from;
rew_evars = evars; rew_prf = RewPrf (res'_rel, prf) } in state, res
let fail : 'a pure_strategy =
{ strategy = fun { state } -> state, Fail }
let id : 'a pure_strategy =
{ strategy = fun { state } -> state, Identity }
let refl : 'a pure_strategy =
{ strategy = fun { state ; env ;
term1 = t ; ty1 = ty ;
cstr = (prop,cstr) ; evars } -> let evars, rel = match cstr with
| None -> let mkr = if prop then PropGlobal.mk_relation else TypeGlobal.mk_relation in let evars, rty = mkr env evars ty in
new_cstr_evar evars env rty
| Some r -> evars, r in let evars, proof = let proxy = if prop then PropGlobal.proper_proxy_type else TypeGlobal.proper_proxy_type in let evars, mty = app_poly_sort prop env evars proxy [| ty ; rel; t |] in
new_cstr_evar evars env mty in let res = Success { rew_car = ty; rew_from = t; rew_to = t;
rew_prf = RewPrf (rel, proof); rew_evars = evars } in state, res
}
let progress (s : 'a pure_strategy) : 'a pure_strategy = { strategy = fun input -> let state, res = s.strategy input in match res with
| Fail -> state, Fail
| Identity -> state, Fail
| Success r -> state, Success r
}
let seq first snd : 'a pure_strategy = { strategy = fun ({ env ; unfresh ; cstr } as input) -> let state, res = first.strategy input in match res with
| Fail -> state, Fail
| Identity -> snd.strategy { input with state }
| Success res -> transitivity state env unfresh cstr res snd
}
let seqs strs = List.fold_left seq id strs
let choice fst snd : 'a pure_strategy = { strategy = fun input -> let state, res = fst.strategy input in match res with
| Fail -> snd.strategy { input with state }
| Identity | Success _ -> state, res
}
let choices strs = List.fold_left choice fail strs
let try_ str : 'a pure_strategy = choice str id
let check_interrupt str input =
Control.check_for_interrupt ();
str input
let fix (f : 'a pure_strategy -> 'a pure_strategy) : 'a pure_strategy = let rec aux input = (f { strategy = fun input -> check_interrupt aux input }).strategy input in
{ strategy = aux }
let fix_tac (f : 'a pure_strategy -> 'a pure_strategy Proofview.tactic) : 'a pure_strategy Proofview.tactic = let forward_def = (* The error below happens if you do [rewrite_strat (fix (fun s => rewrite_strat s None; s)) None]
*) let err_msg = Pp.str "Rewrite strategy fixed-point variables cannot be executed by \"rewrite_strat\" inside of fix."in ref (fun _ -> user_err err_msg) in
f {strategy = fun input -> check_interrupt !forward_def input} >>= fun f ->
forward_def := f.strategy;
Proofview.tclUNIT f
let all_subterms (s : 'a pure_strategy) : 'a pure_strategy = subterm true default_flags s
let one_subterm (s : 'a pure_strategy) : 'a pure_strategy = subterm false default_flags s
let any (s : 'a pure_strategy) : 'a pure_strategy =
fix (fun any -> try_ (seq s any))
let repeat (s : 'a pure_strategy) : 'a pure_strategy =
seq s (any s)
let bottomup (s : 'a pure_strategy) : 'a pure_strategy =
fix (fun s' -> seq (choice (progress (all_subterms s')) s) (try_ s'))
let topdown (s : 'a pure_strategy) : 'a pure_strategy =
fix (fun s' -> seq (choice s (progress (all_subterms s'))) (try_ s'))
let innermost (s : 'a pure_strategy) : 'a pure_strategy =
fix (fun ins -> choice (one_subterm ins) s)
let outermost (s : 'a pure_strategy) : 'a pure_strategy =
fix (fun out -> choice s (one_subterm out))
let one_lemma c l2r by occs : strategy =
apply_lemma l2r (general_rewrite_unif_flags ()) c by occs
let lemmas cs : strategy = List.fold_left (fun tac (c, l2r, by) ->
choice tac (apply_lemma l2r rewrite_unif_flags c by AllOccurrences)
) fail cs
let inj_open hint = (); fun _env sigma -> let (ctx, lemma) = Autorewrite.RewRule.rew_lemma hint in let subst, ctx = UnivGen.fresh_universe_context_set_instance ctx in let subst = Sorts.QVar.Map.empty, subst in let lemma = Vars.subst_univs_level_constr subst (EConstr.of_constr lemma) in let sigma = Evd.merge_context_set UnivRigid sigma ctx in
(sigma, lemma)
let old_hints (db : string) : strategy = let rules = Autorewrite.find_rewrites db in
lemmas
(List.map (fun hint -> (inj_open hint,
Autorewrite.RewRule.rew_l2r hint,
Autorewrite.RewRule.rew_tac hint
)
) rules)
let hints (db : string) : strategy = { strategy = fun ({ term1 = t; env } as input) -> let t = EConstr.Unsafe.to_constr t in let rules = Autorewrite.find_matches env db t in let lemma hint = (inj_open hint,
Autorewrite.RewRule.rew_l2r hint,
Autorewrite.RewRule.rew_tac hint
) in let lems = List.map lemma rules in
(lemmas lems).strategy input
}
let reduce (r : Redexpr.red_expr) : 'a pure_strategy = { strategy = fun { state = state ; env = env ; term1 = t ; ty1 = ty ; cstr = cstr ; evars = evars } -> let rfn, ckind = Redexpr.reduction_of_red_expr env r in let sigma = goalevars evars in let (sigma, t') = rfn env sigma t in if Termops.eq_constr env sigma t' t then
state, Identity else
state, Success { rew_car = ty; rew_from = t; rew_to = t';
rew_prf = RewCast ckind;
rew_evars = sigma, cstrevars evars }
}
let run_fold_in env evars c term typ : rewrite_result = let unfolded = match Tacred.red_product env (goalevars evars) c with
| None -> user_err Pp.(str "fold: the term is not unfoldable!")
| Some c -> c intry let _, sigma = Unification.w_unify env (goalevars evars) CONV ~flags:(Unification.elim_flags ()) unfolded term in let c' = Reductionops.nf_evar sigma c in
Success { rew_car = typ; rew_from = term; rew_to = c';
rew_prf = RewCast DEFAULTcast;
rew_evars = (sigma, cstrevars evars) } with e when CErrors.noncritical e -> Fail
let fold (c : Evd.econstr) : 'a pure_strategy =
{ strategy = fun { state ; env ; term1 = t ; ty1 = ty ; cstr ; evars } ->
state, run_fold_in env evars c t ty
}
let fold_glob c : 'a pure_strategy =
{ strategy = fun { state ; env ; term1 = t ; ty1 = ty ; cstr ; evars } -> let sigma, c = Pretyping.understand_tcc env (goalevars evars) c in
state, run_fold_in env (sigma, cstrevars evars) c t ty
} end
(** The strategy for a single rewrite, dealing with occurrences. *)
(** A dummy initial clauseenv to avoid generating initial evars before even finding a first application of the rewriting lemma, in setoid_rewrite
mode *)
let rewrite_with l2r flags c occs : strategy = { strategy = fun ({ state = () } as input) -> let unify env evars t = let (sigma, cstrs) = evars in let sigma, cbl = c env sigma in let sigma, rew = decompose_applied_relation env sigma cbl in
unify_eqn rew l2r flags env (sigma, cstrs) None t in letapp = apply_rule unify in let strat =
Strategies.fix (fun aux ->
Strategies.choice (Strategies.progress app) (subterm true default_flags aux)) in let occs, res = strat.strategy { input with state = initialize_occurrence_counter occs } in
check_used_occurrences occs;
((), res)
}
let apply_strategy (s : strategy) env unfresh concl (prop, cstr) evars = let evars, ty = get_type_of_refresh env evars concl in let _, res = s.strategy { state = () ; env ; unfresh ;
term1 = concl ; ty1 = ty ;
cstr = (prop, Some cstr) ; evars } in
res
let solve_constraints env (evars,cstrs) = let oldtcs = Evd.get_typeclass_evars evars in let evars' = Evd.set_typeclass_evars evars cstrs in let evars' = TC.resolve_typeclasses env ~filter:TC.all_evars ~fail:true evars'in
Evd.set_typeclass_evars evars' oldtcs
let nf_zeta =
Reductionops.clos_norm_flags (RedFlags.mkflags [RedFlags.fZETA])
exception RewriteFailure of Environ.env * Evd.evar_map * pretype_error
type result = (evar_map * constr option * types) optionoption
exception UnsolvedConstraints of Environ.env * evar_map * Evar.t
let () = CErrors.register_handler begin function
| UnsolvedConstraints (env, evars, ev) ->
Some (str "Unsolved constraint remaining: " ++ spc () ++
Termops.pr_evar_info env evars (Evd.find_undefined evars ev) ++ str ".")
| _ -> None end
let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : result = let sigma, sort = Typing.sort_of env sigma concl in let evdref = ref sigma in let evars = (!evdref, Evar.Set.empty) in let evars, cstr = let prop, (evars, arrow) = if ESorts.is_prop sigma sort thentrue, app_poly_sort true env evars impl [||] elsefalse, app_poly_sort false env evars TypeGlobal.arrow [||] in match is_hyp with
| None -> let evars, t = poly_inverse prop env evars (mkSort sort) arrow in
evars, (prop, t)
| Some _ -> evars, (prop, arrow) in let eq = apply_strategy strat env avoid concl cstr evars in match eq with
| Fail -> None
| Identity -> Some None
| Success res -> let (_, cstrs) = res.rew_evars in let evars = solve_constraints env res.rew_evars in let iter ev = ifnot (Evd.is_defined evars ev) thenraise (UnsolvedConstraints (env, evars, ev)) in let () = Evar.Set.iter iter cstrs in let newt = res.rew_to in let res = match res.rew_prf with
| RewCast c -> None
| RewPrf (rel, p) -> let p = nf_zeta env evars p in let term = match abs with
| None -> p
| Some (t, ty) ->
mkApp (mkLambda (make_annot (Name (Id.of_string "lemma")) ERelevance.relevant, ty, p), [| t |]) in let proof = match is_hyp with
| None -> term
| Some id -> mkApp (term, [| mkVar id |]) in
Some proof in
Some (Some (evars, res, newt))
let assert_replacing id newt tac = let prf = Tactics.assert_after_replacing id newt in
Proofview.tclTHEN prf (Proofview.tclFOCUS 2 2 tac)
let newfail n s = let info = Exninfo.reify () in
Proofview.tclZERO ~info (Tacticals.FailError (n, lazy s))
let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = letopen Proofview.Notations in (* For compatibility *) let beta = Tactics.reduct_in_concl ~cast:false ~check:false
(Reductionops.nf_betaiota, DEFAULTcast) in let beta_hyp id = Tactics.reduct_in_hyp ~check:false ~reorder:false Reductionops.nf_betaiota (id, InHyp) in let treat sigma res state = match res with
| None -> newfail 0 (str "Nothing to rewrite")
| Some None -> if progress then newfail 0 (str"Failed to progress") else Proofview.tclUNIT ()
| Some (Some res) -> let (undef, prf, newt) = res in let fold ev _ accu = if Evd.mem sigma ev then accu else ev :: accu in let gls = List.rev (Evd.fold_undefined fold undef []) in let gls = List.map (fun gl -> Proofview.goal_with_state gl state) gls in match clause, prf with
| Some id, Some p -> let tac = tclTHENLIST [
Refine.refine ~typecheck:true (fun h -> (h,p));
Proofview.Unsafe.tclNEWGOALS gls;
] in
Proofview.Unsafe.tclEVARS undef <*>
--> --------------------
--> maximum size reached
--> --------------------
¤ Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.0.42Bemerkung:
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
