diff options
Diffstat (limited to 'plugins')
34 files changed, 990 insertions, 692 deletions
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index 4425e41652..4769c2dc53 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -102,6 +102,7 @@ let start_deriving f suchthat lemma = let terminator = Proof_global.make_terminator terminator in let pstate = Proof_global.start_dependent_proof ~ontop:None lemma kind goals terminator in - fst @@ Proof_global.with_current_proof begin fun _ p -> - Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p + Proof_global.simple_with_current_proof begin fun _ p -> + let p,_,() = Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p in + p end pstate diff --git a/plugins/extraction/extraction.mli b/plugins/extraction/extraction.mli index d27c79cb62..bf98f8cd70 100644 --- a/plugins/extraction/extraction.mli +++ b/plugins/extraction/extraction.mli @@ -16,9 +16,9 @@ open Environ open Evd open Miniml -val extract_constant : env -> Constant.t -> constant_body -> ml_decl +val extract_constant : env -> Constant.t -> Opaqueproof.opaque constant_body -> ml_decl -val extract_constant_spec : env -> Constant.t -> constant_body -> ml_spec +val extract_constant_spec : env -> Constant.t -> 'a constant_body -> ml_spec (** For extracting "module ... with ..." declaration *) diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 399a77c596..4e229a94b6 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -109,7 +109,7 @@ let labels_of_ref r = (*s Constants tables. *) -let typedefs = ref (Cmap_env.empty : (constant_body * ml_type) Cmap_env.t) +let typedefs = ref (Cmap_env.empty : (Opaqueproof.opaque constant_body * ml_type) Cmap_env.t) let init_typedefs () = typedefs := Cmap_env.empty let add_typedef kn cb t = typedefs := Cmap_env.add kn (cb,t) !typedefs @@ -120,7 +120,7 @@ let lookup_typedef kn cb = with Not_found -> None let cst_types = - ref (Cmap_env.empty : (constant_body * ml_schema) Cmap_env.t) + ref (Cmap_env.empty : (Opaqueproof.opaque constant_body * ml_schema) Cmap_env.t) let init_cst_types () = cst_types := Cmap_env.empty let add_cst_type kn cb s = cst_types := Cmap_env.add kn (cb,s) !cst_types let lookup_cst_type kn cb = diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index acc1bfee8a..7e53964642 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -72,11 +72,11 @@ val labels_of_ref : GlobRef.t -> ModPath.t * Label.t list [mutual_inductive_body] as checksum. In both case, we should ideally also check the env *) -val add_typedef : Constant.t -> constant_body -> ml_type -> unit -val lookup_typedef : Constant.t -> constant_body -> ml_type option +val add_typedef : Constant.t -> Opaqueproof.opaque constant_body -> ml_type -> unit +val lookup_typedef : Constant.t -> Opaqueproof.opaque constant_body -> ml_type option -val add_cst_type : Constant.t -> constant_body -> ml_schema -> unit -val lookup_cst_type : Constant.t -> constant_body -> ml_schema option +val add_cst_type : Constant.t -> Opaqueproof.opaque constant_body -> ml_schema -> unit +val lookup_cst_type : Constant.t -> Opaqueproof.opaque constant_body -> ml_schema option val add_ind : MutInd.t -> mutual_inductive_body -> ml_ind -> unit val lookup_ind : MutInd.t -> mutual_inductive_body -> ml_ind option diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg index a3973732ad..dbfc0fc91d 100644 --- a/plugins/funind/g_indfun.mlg +++ b/plugins/funind/g_indfun.mlg @@ -185,7 +185,7 @@ VERNAC COMMAND EXTEND Function | _,((_,None,_,_,_),_) -> false) recsl in match Vernac_classifier.classify_vernac - (Vernacexpr.(VernacExpr([], VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl)))) + (Vernacexpr.(CAst.make @@ VernacExpr([], VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl)))) with | Vernacextend.VtSideff ids, _ when hard -> Vernacextend.(VtStartProof (GuaranteesOpacity, ids), VtLater) diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 45a4e61846..e15e167ff3 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1518,7 +1518,7 @@ let do_build_inductive in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac Vernacexpr.(VernacExpr([], VernacInductive(None,false,Declarations.Finite,repacked_rel_inds))) + Ppvernac.pr_vernac Vernacexpr.(CAst.make @@ VernacExpr([], VernacInductive(None,false,Declarations.Finite,repacked_rel_inds))) ++ fnl () ++ msg in @@ -1533,7 +1533,7 @@ let do_build_inductive in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac Vernacexpr.(VernacExpr([], VernacInductive(None,false,Declarations.Finite,repacked_rel_inds))) + Ppvernac.pr_vernac Vernacexpr.(CAst.make @@ VernacExpr([], VernacInductive(None,false,Declarations.Finite,repacked_rel_inds))) ++ fnl () ++ CErrors.print reraise in diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 6494e90a03..ce7d149ae1 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -414,7 +414,7 @@ let register_struct ~pstate is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * V match fixpoint_exprl with | [(({CAst.v=fname},pl),_,bl,ret_type,body),_] when not is_rec -> let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in - ComDefinition.do_definition ~ontop:pstate + ComDefinition.do_definition ~program_mode:false fname (Decl_kinds.Global,false,Decl_kinds.Definition) pl diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 3c2b03dfe0..1fca132655 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -132,7 +132,7 @@ let nat = function () -> (coq_init_constant "nat") let iter_ref () = try find_reference ["Recdef"] "iter" with Not_found -> user_err Pp.(str "module Recdef not loaded") -let iter_rd = function () -> (constr_of_global (delayed_force iter_ref)) +let iter_rd = function () -> (constr_of_monomorphic_global (delayed_force iter_ref)) let eq = function () -> (coq_init_constant "eq") let le_lt_SS = function () -> (constant ["Recdef"] "le_lt_SS") let le_lt_n_Sm = function () -> (coq_constant arith_Lt "le_lt_n_Sm") @@ -145,7 +145,7 @@ let coq_O = function () -> (coq_init_constant "O") let coq_S = function () -> (coq_init_constant "S") let lt_n_O = function () -> (coq_constant arith_Nat "nlt_0_r") let max_ref = function () -> (find_reference ["Recdef"] "max") -let max_constr = function () -> EConstr.of_constr (constr_of_global (delayed_force max_ref)) +let max_constr = function () -> EConstr.of_constr (constr_of_monomorphic_global (delayed_force max_ref)) let f_S t = mkApp(delayed_force coq_S, [|t|]);; @@ -701,7 +701,7 @@ let mkDestructEq : let changefun patvars env sigma = pattern_occs [Locus.AllOccurrencesBut [1], expr] (pf_env g2) sigma (pf_concl g2) in - Proofview.V82.of_tactic (change_in_concl None changefun) g2); + Proofview.V82.of_tactic (change_in_concl ~check:true None changefun) g2); Proofview.V82.of_tactic (simplest_case expr)]), to_revert @@ -1041,13 +1041,13 @@ let compute_terminate_type nb_args func = let open Term in let open Constr in let open CVars in - let _,a_arrow_b,_ = destLambda(def_of_const (constr_of_global func)) in + let _,a_arrow_b,_ = destLambda(def_of_const (constr_of_monomorphic_global func)) in let rev_args,b = decompose_prod_n nb_args a_arrow_b in let left = mkApp(delayed_force iter_rd, Array.of_list (lift 5 a_arrow_b:: mkRel 3:: - constr_of_global func::mkRel 1:: + constr_of_monomorphic_global func::mkRel 1:: List.rev (List.map_i (fun i _ -> mkRel (6+i)) 0 rev_args) ) ) @@ -1065,7 +1065,7 @@ let compute_terminate_type nb_args func = delayed_force nat, (mkProd (make_annot (Name k_id) Sorts.Relevant, delayed_force nat, mkArrow cond Sorts.Relevant result))))|])in - let value = mkApp(constr_of_global (Util.delayed_force coq_sig_ref), + let value = mkApp(constr_of_monomorphic_global (Util.delayed_force coq_sig_ref), [|b; (mkLambda (make_annot (Name v_id) Sorts.Relevant, b, nb_iter))|]) in compose_prod rev_args value @@ -1161,7 +1161,7 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a fun g -> let sigma = project g in let ids = Termops.ids_of_named_context (pf_hyps g) in - let func_body = (def_of_const (constr_of_global func)) in + let func_body = (def_of_const (constr_of_monomorphic_global func)) in let func_body = EConstr.of_constr func_body in let (f_name, _, body1) = destLambda sigma func_body in let f_id = @@ -1222,7 +1222,7 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a let get_current_subgoals_types pstate = let p = Proof_global.give_me_the_proof pstate in - let sgs,_,_,_,sigma = Proof.proof p in + let Proof.{ goals=sgs; sigma; _ } = Proof.data p in sigma, List.map (Goal.V82.abstract_type sigma) sgs exception EmptySubgoals @@ -1253,7 +1253,7 @@ let build_and_l sigma l = let c,tac,nb = f pl in mk_and p1 c, tclTHENS - (Proofview.V82.of_tactic (apply (EConstr.of_constr (constr_of_global conj_constr)))) + (Proofview.V82.of_tactic (apply (EConstr.of_constr (constr_of_monomorphic_global conj_constr)))) [tclIDTAC; tac ],nb+1 @@ -1437,7 +1437,7 @@ let start_equation (f:GlobRef.t) (term_f:GlobRef.t) (cont_tactic:Id.t list -> tactic) g = let sigma = project g in let ids = pf_ids_of_hyps g in - let terminate_constr = constr_of_global term_f in + let terminate_constr = constr_of_monomorphic_global term_f in let terminate_constr = EConstr.of_constr terminate_constr in let nargs = nb_prod (project g) (EConstr.of_constr (type_of_const sigma terminate_constr)) in let x = n_x_id ids nargs in @@ -1457,7 +1457,7 @@ let com_eqn sign uctx nb_arg eq_name functional_ref f_ref terminate_ref equation | _ -> anomaly ~label:"terminate_lemma" (Pp.str "not a constant.") in let evd = Evd.from_ctx uctx in - let f_constr = constr_of_global f_ref in + let f_constr = constr_of_monomorphic_global f_ref in let equation_lemma_type = subst1 f_constr equation_lemma_type in let pstate = Lemmas.start_proof ~ontop:None eq_name (Global, false, Proof Lemma) ~sign evd (EConstr.of_constr equation_lemma_type) in @@ -1466,12 +1466,12 @@ let com_eqn sign uctx nb_arg eq_name functional_ref f_ref terminate_ref equation (fun x -> prove_eq (fun _ -> tclIDTAC) {nb_arg=nb_arg; - f_terminate = EConstr.of_constr (constr_of_global terminate_ref); + f_terminate = EConstr.of_constr (constr_of_monomorphic_global terminate_ref); f_constr = EConstr.of_constr f_constr; concl_tac = tclIDTAC; func=functional_ref; info=(instantiate_lambda Evd.empty - (EConstr.of_constr (def_of_const (constr_of_global functional_ref))) + (EConstr.of_constr (def_of_const (constr_of_monomorphic_global functional_ref))) (EConstr.of_constr f_constr::List.map mkVar x) ); is_main_branch = true; @@ -1570,9 +1570,9 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num if not stop then let eq_ref = Nametab.locate (qualid_of_ident equation_id ) in - let f_ref = destConst (constr_of_global f_ref) - and functional_ref = destConst (constr_of_global functional_ref) - and eq_ref = destConst (constr_of_global eq_ref) in + let f_ref = destConst (constr_of_monomorphic_global f_ref) + and functional_ref = destConst (constr_of_monomorphic_global functional_ref) + and eq_ref = destConst (constr_of_monomorphic_global eq_ref) in generate_induction_principle f_ref tcc_lemma_constr functional_ref eq_ref rec_arg_num (EConstr.of_constr rec_arg_type) diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg index 523c7c8305..e59076bd63 100644 --- a/plugins/ltac/g_auto.mlg +++ b/plugins/ltac/g_auto.mlg @@ -182,9 +182,18 @@ TACTIC EXTEND unify } END +{ +let deprecated_convert_concl_no_check = + CWarnings.create + ~name:"convert_concl_no_check" ~category:"deprecated" + (fun () -> Pp.str "The syntax [convert_concl_no_check] is deprecated. Use [change_no_check] instead.") +} TACTIC EXTEND convert_concl_no_check -| ["convert_concl_no_check" constr(x) ] -> { Tactics.convert_concl_no_check x DEFAULTcast } +| ["convert_concl_no_check" constr(x) ] -> { + deprecated_convert_concl_no_check (); + Tactics.convert_concl ~check:false x DEFAULTcast + } END { diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg index 469551809c..12b12bc7b0 100644 --- a/plugins/ltac/g_rewrite.mlg +++ b/plugins/ltac/g_rewrite.mlg @@ -278,7 +278,7 @@ VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF } | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Morphism" constr(m) ":" ident(n) ] (* This command may or may not open a goal *) - => { VtUnknown, VtNow } + => { (if Lib.is_modtype() then VtSideff([n]) else VtStartProof(GuaranteesOpacity, [n])), VtLater } -> { add_morphism_infer atts m n } diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg index a2dd51643b..c23240b782 100644 --- a/plugins/ltac/g_tactic.mlg +++ b/plugins/ltac/g_tactic.mlg @@ -703,7 +703,11 @@ GRAMMAR EXTEND Gram | IDENT "change"; c = conversion; cl = clause_dft_concl -> { let (oc, c) = c in let p,cl = merge_occurrences loc cl oc in - TacAtom (CAst.make ~loc @@ TacChange (p,c,cl)) } + TacAtom (CAst.make ~loc @@ TacChange (true,p,c,cl)) } + | IDENT "change_no_check"; c = conversion; cl = clause_dft_concl -> + { let (oc, c) = c in + let p,cl = merge_occurrences loc cl oc in + TacAtom (CAst.make ~loc @@ TacChange (false,p,c,cl)) } ] ] ; END diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 80070a7493..79f0f521cc 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -833,9 +833,10 @@ let pr_goal_selector ~toplevel s = pr_red_expr r ++ pr_non_empty_arg (pr_clauses (Some true) pr.pr_name) h ) - | TacChange (op,c,h) -> + | TacChange (check,op,c,h) -> + let name = if check then "change_no_check" else "change" in hov 1 ( - primitive "change" ++ brk (1,1) + primitive name ++ brk (1,1) ++ ( match op with None -> diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 2d40ba6562..963b7189f9 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1574,8 +1574,8 @@ let newfail n s = let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = let open Proofview.Notations in (* For compatibility *) - let beta = Tactics.reduct_in_concl (Reductionops.nf_betaiota, DEFAULTcast) in - let beta_hyp id = Tactics.reduct_in_hyp Reductionops.nf_betaiota (id, InHyp) in + let beta = Tactics.reduct_in_concl ~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 = match res with | None -> newfail 0 (str "Nothing to rewrite") @@ -1596,7 +1596,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = tclTHENFIRST (assert_replacing id newt tac) (beta_hyp id) | Some id, None -> Proofview.Unsafe.tclEVARS undef <*> - convert_hyp_no_check (LocalAssum (make_annot id Sorts.Relevant, newt)) <*> + convert_hyp ~check:false ~reorder:false (LocalAssum (make_annot id Sorts.Relevant, newt)) <*> beta_hyp id | None, Some p -> Proofview.Unsafe.tclEVARS undef <*> @@ -1610,7 +1610,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = end | None, None -> Proofview.Unsafe.tclEVARS undef <*> - convert_concl_no_check newt DEFAULTcast + convert_concl ~check:false newt DEFAULTcast in Proofview.Goal.enter begin fun gl -> let concl = Proofview.Goal.concl gl in @@ -1800,7 +1800,7 @@ let anew_instance ~pstate atts binders instance fields = let program_mode = atts.program in new_instance ~pstate ~program_mode atts.polymorphic binders instance (Some (true, CAst.make @@ CRecord (fields))) - ~global:atts.global ~generalize:false ~refine:false Hints.empty_hint_info + ~global:atts.global ~generalize:false Hints.empty_hint_info let declare_instance_refl ~pstate atts binders a aeq n lemma = let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive" diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml index 30e316b36d..0eb7726a18 100644 --- a/plugins/ltac/tacexpr.ml +++ b/plugins/ltac/tacexpr.ml @@ -34,6 +34,7 @@ type rec_flag = bool (* true = recursive false = not recursive *) type advanced_flag = bool (* true = advanced false = basic *) type letin_flag = bool (* true = use local def false = use Leibniz *) type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *) +type check_flag = bool (* true = check false = do not check *) type ('c,'d,'id) inversion_strength = | NonDepInversion of @@ -125,7 +126,7 @@ type 'a gen_atomic_tactic_expr = (* Conversion *) | TacReduce of ('trm,'cst,'pat) red_expr_gen * 'nam clause_expr - | TacChange of 'pat option * 'dtrm * 'nam clause_expr + | TacChange of check_flag * 'pat option * 'dtrm * 'nam clause_expr (* Equality and inversion *) | TacRewrite of evars_flag * diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index 8b6b14322b..fd303f5d94 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -34,6 +34,7 @@ type rec_flag = bool (* true = recursive false = not recursive *) type advanced_flag = bool (* true = advanced false = basic *) type letin_flag = bool (* true = use local def false = use Leibniz *) type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *) +type check_flag = bool (* true = check false = do not check *) type ('c,'d,'id) inversion_strength = | NonDepInversion of @@ -124,7 +125,7 @@ type 'a gen_atomic_tactic_expr = (* Conversion *) | TacReduce of ('trm,'cst,'pat) red_expr_gen * 'nam clause_expr - | TacChange of 'pat option * 'dtrm * 'nam clause_expr + | TacChange of check_flag * 'pat option * 'dtrm * 'nam clause_expr (* Equality and inversion *) | TacRewrite of evars_flag * diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 543d4de0fe..c1f7fab123 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -551,7 +551,7 @@ let rec intern_atomic lf ist x = | TacReduce (r,cl) -> dump_glob_red_expr r; TacReduce (intern_red_expr ist r, clause_app (intern_hyp_location ist) cl) - | TacChange (None,c,cl) -> + | TacChange (check,None,c,cl) -> let is_onhyps = match cl.onhyps with | None | Some [] -> true | _ -> false @@ -560,17 +560,17 @@ let rec intern_atomic lf ist x = | AtLeastOneOccurrence | AllOccurrences | NoOccurrences -> true | _ -> false in - TacChange (None, + TacChange (check,None, (if is_onhyps && is_onconcl then intern_type ist c else intern_constr ist c), clause_app (intern_hyp_location ist) cl) - | TacChange (Some p,c,cl) -> + | TacChange (check,Some p,c,cl) -> let { ltacvars } = ist in let metas,pat = intern_typed_pattern ist ~as_type:false ~ltacvars p in let fold accu x = Id.Set.add x accu in let ltacvars = List.fold_left fold ltacvars metas in let ist' = { ist with ltacvars } in - TacChange (Some pat,intern_constr ist' c, + TacChange (check,Some pat,intern_constr ist' c, clause_app (intern_hyp_location ist) cl) (* Equality and inversion *) diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 4398fb14ab..800be2565d 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -1770,7 +1770,7 @@ and interp_atomic ist tac : unit Proofview.tactic = Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (Tactics.reduce r_interp (interp_clause ist (pf_env gl) (project gl) cl)) end - | TacChange (None,c,cl) -> + | TacChange (check,None,c,cl) -> (* spiwack: until the tactic is in the monad *) Proofview.Trace.name_tactic (fun _ _ -> Pp.str"<change>") begin Proofview.Goal.enter begin fun gl -> @@ -1792,10 +1792,10 @@ and interp_atomic ist tac : unit Proofview.tactic = then interp_type ist env sigma c else interp_constr ist env sigma c in - Tactics.change None c_interp (interp_clause ist (pf_env gl) (project gl) cl) + Tactics.change ~check None c_interp (interp_clause ist (pf_env gl) (project gl) cl) end end - | TacChange (Some op,c,cl) -> + | TacChange (check,Some op,c,cl) -> (* spiwack: until the tactic is in the monad *) Proofview.Trace.name_tactic (fun _ _ -> Pp.str"<change>") begin Proofview.Goal.enter begin fun gl -> @@ -1815,7 +1815,7 @@ and interp_atomic ist tac : unit Proofview.tactic = with e when to_catch e (* Hack *) -> user_err (strbrk "Failed to get enough information from the left-hand side to type the right-hand side.") in - Tactics.change (Some op) c_interp (interp_clause ist env sigma cl) + Tactics.change ~check (Some op) c_interp (interp_clause ist env sigma cl) end end diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index e617f3d45e..a3eeca2267 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -158,8 +158,8 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with (* Conversion *) | TacReduce (r,cl) -> TacReduce (subst_redexp subst r, cl) - | TacChange (op,c,cl) -> - TacChange (Option.map (subst_glob_constr_or_pattern subst) op, + | TacChange (check,op,c,cl) -> + TacChange (check,Option.map (subst_glob_constr_or_pattern subst) op, subst_glob_constr subst c, cl) (* Equality and inversion *) diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index ef6af16036..de9dec0f74 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -207,7 +207,7 @@ struct * ZMicromega.v *) - let gen_constant_in_modules s m n = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.gen_reference_in_modules s m n) + let gen_constant_in_modules s m n = EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.gen_reference_in_modules s m n) let init_constant = gen_constant_in_modules "ZMicromega" Coqlib.init_modules [@@@ocaml.warning "+3"] diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 4802608fda..ffc3506a1f 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -535,7 +535,7 @@ 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_no_check newc DEFAULTcast + convert_concl ~check:false newc DEFAULTcast end let focused_simpl path = focused_simpl path @@ -687,7 +687,7 @@ let simpl_coeffs path_init path_k = let n = Pervasives.(-) (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_no_check newc DEFAULTcast + convert_concl ~check:false newc DEFAULTcast end let rec shuffle p (t1,t2) = @@ -1849,12 +1849,12 @@ let destructure_hyps = match destructurate_type env sigma typ with | Kapp(Nat,_) -> (tclTHEN - (convert_hyp_no_check (NamedDecl.set_type (mkApp (Lazy.force coq_neq, [| t1;t2|])) + (Tactics.convert_hyp ~check:false ~reorder:false (NamedDecl.set_type (mkApp (Lazy.force coq_neq, [| t1;t2|])) decl)) (loop lit)) | Kapp(Z,_) -> (tclTHEN - (convert_hyp_no_check (NamedDecl.set_type (mkApp (Lazy.force coq_Zne, [| t1;t2|])) + (Tactics.convert_hyp ~check:false ~reorder:false (NamedDecl.set_type (mkApp (Lazy.force coq_Zne, [| t1;t2|])) decl)) (loop lit)) | _ -> loop lit diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v index 813c521ab0..ad2ee821b3 100644 --- a/plugins/setoid_ring/Field_theory.v +++ b/plugins/setoid_ring/Field_theory.v @@ -1235,12 +1235,19 @@ Notation ring_correct := (ring_correct Rsth Reqe ARth CRmorph pow_th cdiv_th). (* simplify a field expression into a fraction *) -(* TODO: simplify when den is constant... *) Definition display_linear l num den := - NPphi_dev l num / NPphi_dev l den. + let lnum := NPphi_dev l num in + match den with + | Pc c => if ceqb c cI then lnum else lnum / NPphi_dev l den + | _ => lnum / NPphi_dev l den + end. Definition display_pow_linear l num den := - NPphi_pow l num / NPphi_pow l den. + let lnum := NPphi_pow l num in + match den with + | Pc c => if ceqb c cI then lnum else lnum / NPphi_pow l den + | _ => lnum / NPphi_pow l den + end. Theorem Field_rw_correct n lpe l : Ninterp_PElist l lpe -> @@ -1252,7 +1259,18 @@ Theorem Field_rw_correct n lpe l : Proof. intros Hlpe lmp lmp_eq fe nfe eq_nfe H; subst nfe lmp. rewrite (Fnorm_FEeval_PEeval _ _ H). - unfold display_linear; apply rdiv_ext; + unfold display_linear. + destruct (Nnorm _ _ _) as [c | | ] eqn: HN; + try ( apply rdiv_ext; + eapply ring_rw_correct; eauto). + destruct (ceqb_spec c cI). + set (nnum := NPphi_dev _ _). + apply eq_trans with (nnum / NPphi_dev l (Pc c)). + apply rdiv_ext; + eapply ring_rw_correct; eauto. + rewrite Pphi_dev_ok; try eassumption. + now simpl; rewrite H0, phi_1, <- rdiv1. + apply rdiv_ext; eapply ring_rw_correct; eauto. Qed. @@ -1266,8 +1284,19 @@ Theorem Field_rw_pow_correct n lpe l : Proof. intros Hlpe lmp lmp_eq fe nfe eq_nfe H; subst nfe lmp. rewrite (Fnorm_FEeval_PEeval _ _ H). - unfold display_pow_linear; apply rdiv_ext; - eapply ring_rw_pow_correct;eauto. + unfold display_pow_linear. + destruct (Nnorm _ _ _) as [c | | ] eqn: HN; + try ( apply rdiv_ext; + eapply ring_rw_pow_correct; eauto). + destruct (ceqb_spec c cI). + set (nnum := NPphi_pow _ _). + apply eq_trans with (nnum / NPphi_pow l (Pc c)). + apply rdiv_ext; + eapply ring_rw_pow_correct; eauto. + rewrite Pphi_pow_ok; try eassumption. + now simpl; rewrite H0, phi_1, <- rdiv1. + apply rdiv_ext; + eapply ring_rw_pow_correct; eauto. Qed. Theorem Field_correct n l lpe fe1 fe2 : diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 3f69701bd3..b02b97f656 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -89,10 +89,10 @@ let protect_red map env sigma c0 = EConstr.of_constr (eval 0 c) let protect_tac map = - Tactics.reduct_option (protect_red map,DEFAULTcast) None + Tactics.reduct_option ~check:false (protect_red map,DEFAULTcast) None let protect_tac_in map id = - Tactics.reduct_option (protect_red map,DEFAULTcast) (Some(id, Locus.InHyp)) + Tactics.reduct_option ~check:false (protect_red map,DEFAULTcast) (Some(id, Locus.InHyp)) (****************************************************************************) diff --git a/plugins/ssr/ssrbool.v b/plugins/ssr/ssrbool.v index d6b7371647..49d729bd6c 100644 --- a/plugins/ssr/ssrbool.v +++ b/plugins/ssr/ssrbool.v @@ -94,20 +94,31 @@ Require Import ssreflect ssrfun. like terms from boolean equalities (can fail). This file provides a theory of boolean predicates and relations: pred T == the type of bool predicates (:= T -> bool). - simpl_pred T == the type of simplifying bool predicates, using - the simpl_fun from ssrfun.v. + simpl_pred T == the type of simplifying bool predicates, based on + the simpl_fun type from ssrfun.v. + mem_pred T == a specialized form of simpl_pred for "collective" + predicates (see below). rel T == the type of bool relations. := T -> pred T or T -> T -> bool. simpl_rel T == type of simplifying relations. + := T -> simpl_pred T predType == the generic predicate interface, supported for for lists and sets. - pred_class == a coercion class for the predType projection to - pred; declaring a coercion to pred_class is an - alternative way of equipping a type with a - predType structure, which interoperates better - with coercion subtyping. This is used, e.g., - for finite sets, so that finite groups inherit - the membership operation by coercing to sets. + pred_sort == the predType >-> Type projection; pred_sort is + itself a Coercion target class. Declaring a + coercion to pred_sort is an alternative way of + equiping a type with a predType structure, which + interoperates better with coercion subtyping. + This is used, e.g., for finite sets, so that finite + groups inherit the membership operation by + coercing to sets. + {pred T} == a type convertible to pred T, but whose head + constant is pred_sort. This type should be used + for parameters that can be used as collective + predicates (see below), as this will allow passing + in directly collections that implement predType + by coercion as described above, e.g., finite sets. + := pred_sort (predPredType T) If P is a predicate the proposition "x satisfies P" can be written applicatively as (P x), or using an explicit connective as (x \in P); in the latter case we say that P is a "collective" predicate. We use A, B @@ -119,8 +130,14 @@ Require Import ssreflect ssrfun. pred T value of one type needs to be passed as the other the following conversions should be used explicitly: SimplPred P == a (simplifying) applicative equivalent of P. - mem A == an applicative equivalent of A: - mem A x simplifies to x \in A. + mem A == an applicative equivalent of collective predicate A: + mem A x simplifies to x \in A, as mem A has in + fact type mem_pred T. + --> In user notation collective predicates _only_ occur as arguments to mem: + A only appears as (mem A). This is hidden by notation, e.g., + x \in A := in_mem x (mem A) here, enum A := enum_mem (mem A) in fintype. + This makes it possible to unify the various ways in which A can be + interpreted as a predicate, for both pattern matching and display. Alternatively one can use the syntax for explicit simplifying predicates and relations (in the following x is bound in E): #[#pred x | E#]# == simplifying (see ssrfun) predicate x => E. @@ -135,11 +152,11 @@ Require Import ssreflect ssrfun. #[#predD A & B#]# == difference of collective predicates A and B. #[#predC A#]# == complement of the collective predicate A. #[#preim f of A#]# == preimage under f of the collective predicate A. - predU P Q, ... == union, etc of applicative predicates. - pred0 == the empty predicate. - predT == the total (always true) predicate. - if T : predArgType, then T coerces to predT. - {: T} == T cast to predArgType (e.g., {: bool * nat}) + predU P Q, ..., preim f P == union, etc of applicative predicates. + pred0 == the empty predicate. + predT == the total (always true) predicate. + if T : predArgType, then T coerces to predT. + {: T} == T cast to predArgType (e.g., {: bool * nat}). In the following, x and y are bound in E: #[#rel x y | E#]# == simplifying relation x, y => E. #[#rel x y : T | E#]# == simplifying relation with arguments cast. @@ -147,7 +164,9 @@ Require Import ssreflect ssrfun. #[#rel x y in A & B#]# == #[#rel x y | (x \in A) && (y \in B) #]#. #[#rel x y in A | E#]# == #[#rel x y in A & A | E#]#. #[#rel x y in A#]# == #[#rel x y in A & A#]#. - relU R S == union of relations R and S. + relU R S == union of relations R and S. + relpre f R == preimage of relation R under f. + xpredU, ..., xrelpre == lambda terms implementing predU, ..., etc. Explicit values of type pred T (i.e., lamdba terms) should always be used applicatively, while values of collection types implementing the predType interface, such as sequences or sets should always be used as collective @@ -177,7 +196,7 @@ Require Import ssreflect ssrfun. applicative and collective styles. Purely for aesthetics, we provide a subtype of collective predicates: qualifier q T == a pred T pretty-printing wrapper. An A : qualifier q T - coerces to pred_class and thus behaves as a collective + coerces to pred_sort and thus behaves as a collective predicate, but x \in A and x \notin A are displayed as: x \is A and x \isn't A when q = 0, x \is a A and x \isn't a A when q = 1, @@ -189,11 +208,11 @@ Require Import ssreflect ssrfun. We provide an internal interface to support attaching properties (such as being multiplicative) to predicates: pred_key p == phantom type that will serve as a support for properties - to be attached to p : pred_class; instances should be + to be attached to p : {pred _}; instances should be created with Fact/Qed so as to be opaque. KeyedPred k_p == an instance of the interface structure that attaches (k_p : pred_key P) to P; the structure projection is a - coercion to pred_class. + coercion to pred_sort. KeyedQualifier k_q == an instance of the interface structure that attaches (k_q : pred_key q) to (q : qualifier n T). DefaultPredKey p == a default value for pred_key p; the vernacular command @@ -235,17 +254,20 @@ Require Import ssreflect ssrfun. {in A &, P2} <-> forall x y, x \in A -> y \in A -> Qxy. {in A1 & A2 & A3, Q3} <-> forall x y z, x \in A1 -> y \in A2 -> z \in A3 -> Qxyz. - {in A1 & A2 &, Q3} == {in A1 & A2 & A2, Q3}. - {in A1 && A3, Q3} == {in A1 & A1 & A3, Q3}. - {in A &&, Q3} == {in A & A & A, Q3}. - {in A, bijective f} == f has a right inverse in A. - {on C, P1} == forall x, (f x) \in C -> Qx - when P1 is also convertible to Pf f. + {in A1 & A2 &, Q3} := {in A1 & A2 & A2, Q3}. + {in A1 && A3, Q3} := {in A1 & A1 & A3, Q3}. + {in A &&, Q3} := {in A & A & A, Q3}. + {in A, bijective f} <-> f has a right inverse in A. + {on C, P1} <-> forall x, (f x) \in C -> Qx + when P1 is also convertible to Pf f, e.g., + {on C, involutive f}. {on C &, P2} == forall x y, f x \in C -> f y \in C -> Qxy - when P2 is also convertible to Pf f. + when P2 is also convertible to Pf f, e.g., + {on C &, injective f}. {on C, P1' & g} == forall x, (f x) \in cd -> Qx when P1' is convertible to Pf f - and P1' g is convertible to forall x, Qx. + and P1' g is convertible to forall x, Qx, e.g., + {on C, cancel f & g}. {on C, bijective f} == f has a right inverse on C. This file extends the lemma name suffix conventions of ssrfun as follows: A -- associativity, as in andbA : associative andb. @@ -282,13 +304,119 @@ Notation ReflectF := Bool.ReflectF. Reserved Notation "~~ b" (at level 35, right associativity). Reserved Notation "b ==> c" (at level 55, right associativity). -Reserved Notation "b1 (+) b2" (at level 50, left associativity). -Reserved Notation "x \in A" - (at level 70, format "'[hv' x '/ ' \in A ']'", no associativity). -Reserved Notation "x \notin A" - (at level 70, format "'[hv' x '/ ' \notin A ']'", no associativity). -Reserved Notation "p1 =i p2" - (at level 70, format "'[hv' p1 '/ ' =i p2 ']'", no associativity). +Reserved Notation "b1 (+) b2" (at level 50, left associativity). + +Reserved Notation "x \in A" (at level 70, no associativity, + format "'[hv' x '/ ' \in A ']'"). +Reserved Notation "x \notin A" (at level 70, no associativity, + format "'[hv' x '/ ' \notin A ']'"). +Reserved Notation "x \is A" (at level 70, no associativity, + format "'[hv' x '/ ' \is A ']'"). +Reserved Notation "x \isn't A" (at level 70, no associativity, + format "'[hv' x '/ ' \isn't A ']'"). +Reserved Notation "x \is 'a' A" (at level 70, no associativity, + format "'[hv' x '/ ' \is 'a' A ']'"). +Reserved Notation "x \isn't 'a' A" (at level 70, no associativity, + format "'[hv' x '/ ' \isn't 'a' A ']'"). +Reserved Notation "x \is 'an' A" (at level 70, no associativity, + format "'[hv' x '/ ' \is 'an' A ']'"). +Reserved Notation "x \isn't 'an' A" (at level 70, no associativity, + format "'[hv' x '/ ' \isn't 'an' A ']'"). +Reserved Notation "p1 =i p2" (at level 70, no associativity, + format "'[hv' p1 '/ ' =i p2 ']'"). +Reserved Notation "{ 'subset' A <= B }" (at level 0, A, B at level 69, + format "'[hv' { 'subset' A '/ ' <= B } ']'"). + +Reserved Notation "{ : T }" (at level 0, format "{ : T }"). +Reserved Notation "{ 'pred' T }" (at level 0, format "{ 'pred' T }"). +Reserved Notation "[ 'predType' 'of' T ]" (at level 0, + format "[ 'predType' 'of' T ]"). + +Reserved Notation "[ 'pred' : T | E ]" (at level 0, + format "'[hv' [ 'pred' : T | '/ ' E ] ']'"). +Reserved Notation "[ 'pred' x | E ]" (at level 0, x ident, + format "'[hv' [ 'pred' x | '/ ' E ] ']'"). +Reserved Notation "[ 'pred' x : T | E ]" (at level 0, x ident, + format "'[hv' [ 'pred' x : T | '/ ' E ] ']'"). +Reserved Notation "[ 'pred' x | E1 & E2 ]" (at level 0, x ident, + format "'[hv' [ 'pred' x | '/ ' E1 & '/ ' E2 ] ']'"). +Reserved Notation "[ 'pred' x : T | E1 & E2 ]" (at level 0, x ident, + format "'[hv' [ 'pred' x : T | '/ ' E1 & E2 ] ']'"). +Reserved Notation "[ 'pred' x 'in' A ]" (at level 0, x ident, + format "'[hv' [ 'pred' x 'in' A ] ']'"). +Reserved Notation "[ 'pred' x 'in' A | E ]" (at level 0, x ident, + format "'[hv' [ 'pred' x 'in' A | '/ ' E ] ']'"). +Reserved Notation "[ 'pred' x 'in' A | E1 & E2 ]" (at level 0, x ident, + format "'[hv' [ 'pred' x 'in' A | '/ ' E1 & '/ ' E2 ] ']'"). + +Reserved Notation "[ 'qualify' x | P ]" (at level 0, x at level 99, + format "'[hv' [ 'qualify' x | '/ ' P ] ']'"). +Reserved Notation "[ 'qualify' x : T | P ]" (at level 0, x at level 99, + format "'[hv' [ 'qualify' x : T | '/ ' P ] ']'"). +Reserved Notation "[ 'qualify' 'a' x | P ]" (at level 0, x at level 99, + format "'[hv' [ 'qualify' 'a' x | '/ ' P ] ']'"). +Reserved Notation "[ 'qualify' 'a' x : T | P ]" (at level 0, x at level 99, + format "'[hv' [ 'qualify' 'a' x : T | '/ ' P ] ']'"). +Reserved Notation "[ 'qualify' 'an' x | P ]" (at level 0, x at level 99, + format "'[hv' [ 'qualify' 'an' x | '/ ' P ] ']'"). +Reserved Notation "[ 'qualify' 'an' x : T | P ]" (at level 0, x at level 99, + format "'[hv' [ 'qualify' 'an' x : T | '/ ' P ] ']'"). + +Reserved Notation "[ 'rel' x y | E ]" (at level 0, x ident, y ident, + format "'[hv' [ 'rel' x y | '/ ' E ] ']'"). +Reserved Notation "[ 'rel' x y : T | E ]" (at level 0, x ident, y ident, + format "'[hv' [ 'rel' x y : T | '/ ' E ] ']'"). +Reserved Notation "[ 'rel' x y 'in' A & B | E ]" (at level 0, x ident, y ident, + format "'[hv' [ 'rel' x y 'in' A & B | '/ ' E ] ']'"). +Reserved Notation "[ 'rel' x y 'in' A & B ]" (at level 0, x ident, y ident, + format "'[hv' [ 'rel' x y 'in' A & B ] ']'"). +Reserved Notation "[ 'rel' x y 'in' A | E ]" (at level 0, x ident, y ident, + format "'[hv' [ 'rel' x y 'in' A | '/ ' E ] ']'"). +Reserved Notation "[ 'rel' x y 'in' A ]" (at level 0, x ident, y ident, + format "'[hv' [ 'rel' x y 'in' A ] ']'"). + +Reserved Notation "[ 'mem' A ]" (at level 0, format "[ 'mem' A ]"). +Reserved Notation "[ 'predI' A & B ]" (at level 0, + format "[ 'predI' A & B ]"). +Reserved Notation "[ 'predU' A & B ]" (at level 0, + format "[ 'predU' A & B ]"). +Reserved Notation "[ 'predD' A & B ]" (at level 0, + format "[ 'predD' A & B ]"). +Reserved Notation "[ 'predC' A ]" (at level 0, + format "[ 'predC' A ]"). +Reserved Notation "[ 'preim' f 'of' A ]" (at level 0, + format "[ 'preim' f 'of' A ]"). + +Reserved Notation "\unless C , P" (at level 200, C at level 100, + format "'[hv' \unless C , '/ ' P ']'"). + +Reserved Notation "{ 'for' x , P }" (at level 0, + format "'[hv' { 'for' x , '/ ' P } ']'"). +Reserved Notation "{ 'in' d , P }" (at level 0, + format "'[hv' { 'in' d , '/ ' P } ']'"). +Reserved Notation "{ 'in' d1 & d2 , P }" (at level 0, + format "'[hv' { 'in' d1 & d2 , '/ ' P } ']'"). +Reserved Notation "{ 'in' d & , P }" (at level 0, + format "'[hv' { 'in' d & , '/ ' P } ']'"). +Reserved Notation "{ 'in' d1 & d2 & d3 , P }" (at level 0, + format "'[hv' { 'in' d1 & d2 & d3 , '/ ' P } ']'"). +Reserved Notation "{ 'in' d1 & & d3 , P }" (at level 0, + format "'[hv' { 'in' d1 & & d3 , '/ ' P } ']'"). +Reserved Notation "{ 'in' d1 & d2 & , P }" (at level 0, + format "'[hv' { 'in' d1 & d2 & , '/ ' P } ']'"). +Reserved Notation "{ 'in' d & & , P }" (at level 0, + format "'[hv' { 'in' d & & , '/ ' P } ']'"). +Reserved Notation "{ 'on' cd , P }" (at level 0, + format "'[hv' { 'on' cd , '/ ' P } ']'"). +Reserved Notation "{ 'on' cd & , P }" (at level 0, + format "'[hv' { 'on' cd & , '/ ' P } ']'"). +Reserved Notation "{ 'on' cd , P & g }" (at level 0, g at level 8, + format "'[hv' { 'on' cd , '/ ' P & g } ']'"). +Reserved Notation "{ 'in' d , 'bijective' f }" (at level 0, f at level 8, + format "'[hv' { 'in' d , '/ ' 'bijective' f } ']'"). +Reserved Notation "{ 'on' cd , 'bijective' f }" (at level 0, f at level 8, + format "'[hv' { 'on' cd , '/ ' 'bijective' f } ']'"). + (** We introduce a number of n-ary "list-style" notations that share a common @@ -335,18 +463,6 @@ Reserved Notation "[ ==> b1 => c ]" (at level 0, only parsing). Reserved Notation "[ ==> b1 , b2 , .. , bn => c ]" (at level 0, format "'[hv' [ ==> '[' b1 , '/' b2 , '/' .. , '/' bn ']' '/' => c ] ']'"). -Reserved Notation "[ 'pred' : T => E ]" (at level 0, format - "'[hv' [ 'pred' : T => '/ ' E ] ']'"). -Reserved Notation "[ 'pred' x => E ]" (at level 0, x at level 8, format - "'[hv' [ 'pred' x => '/ ' E ] ']'"). -Reserved Notation "[ 'pred' x : T => E ]" (at level 0, x at level 8, format - "'[hv' [ 'pred' x : T => '/ ' E ] ']'"). - -Reserved Notation "[ 'rel' x y => E ]" (at level 0, x, y at level 8, format - "'[hv' [ 'rel' x y => '/ ' E ] ']'"). -Reserved Notation "[ 'rel' x y : T => E ]" (at level 0, x, y at level 8, format - "'[hv' [ 'rel' x y : T => '/ ' E ] ']'"). - (** Shorter delimiter **) Delimit Scope bool_scope with B. Open Scope bool_scope. @@ -622,9 +738,7 @@ Hint View for apply/ impliesPn|2 impliesP|2. Definition unless condition property : Prop := forall goal : Prop, (condition -> goal) -> (property -> goal) -> goal. -Notation "\unless C , P" := (unless C P) - (at level 200, C at level 100, - format "'[' \unless C , '/ ' P ']'") : type_scope. +Notation "\unless C , P" := (unless C P) : type_scope. Lemma unlessL C P : implies C (\unless C, P). Proof. by split=> hC G /(_ hC). Qed. @@ -1002,8 +1116,7 @@ Ltac bool_congr := Moreover these infix forms are convertible to their prefix counterpart (e.g., predI P Q x which in turn simplifies to P x && Q x). The converse is not true, however; collective predicate types cannot, in general, be - general, be used applicatively, because of the "uniform inheritance" - restriction on implicit coercions. + used applicatively, because of restrictions on implicit coercions. However, we do define an explicit generic coercion - mem : forall (pT : predType), pT -> mem_pred T where mem_pred T is a variant of simpl_pred T that preserves the infix @@ -1019,319 +1132,391 @@ Ltac bool_congr := not to use it applicatively; this avoids the burden of having to declare a different predicate type for each predicate parameter of each section or lemma. - This trick is made possible by the fact that the constructor of the - mem_pred T type aligns the unification process, forcing a generic - "collective" predicate A : pred T to unify with the actual collective B, - which mem has coerced to pred T via an internal, hidden implicit coercion, - supplied by the predType structure for B. Users should take care not to - inadvertently "strip" (mem B) down to the coerced B, since this will - expose the internal coercion: Coq will display a term B x that cannot be - typed as such. The topredE lemma can be used to restore the x \in B - syntax in this case. While -topredE can conversely be used to change - x \in P into P x, it is safer to use the inE and memE lemmas instead, as - they do not run the risk of exposing internal coercions. As a consequence - it is better to explicitly cast a generic applicative pred T to simpl_pred - using the SimplPred constructor, when it is used as a collective predicate - (see, e.g., Lemma eq_big in bigop). + In detail, we ensure that the head normal form of mem A is always of the + eta-long MemPred (fun x => pA x) form, where pA is the pred interpretation of + A following its predType pT, i.e., the _expansion_ of topred A. For a pred T + evar ?P, (mem ?P) converts MemPred (fun x => ?P x), whose argument is a Miller + pattern and therefore always unify: unifying (mem A) with (mem ?P) always + yields ?P = pA, because the rigid constant MemPred aligns the unification. + Furthermore, we ensure pA is always either A or toP .... A where toP ... is + the expansion of @topred T pT, and toP is declared as a Coercion, so pA will + _display_ as A in either case, and the instances of @mem T (predPredType T) pA + appearing in the premises or right-hand side of a generic lemma parametrized + by ?P will be indistinguishable from @mem T pT A. + Users should take care not to inadvertently "strip" (mem A) down to the + coerced A, since this will expose the internal toP coercion: Coq could then + display terms A x that cannot be typed as such. The topredE lemma can be used + to restore the x \in A syntax in this case. While -topredE can conversely be + used to change x \in P into P x for an applicative P, it is safer to use the + inE, unfold_in or and memE lemmas instead, as they do not run the risk of + exposing internal coercions. As a consequence it is better to explicitly + cast a generic applicative predicate to simpl_pred using the SimplPred + constructor when it is used as a collective predicate (see, e.g., + Lemma eq_big in bigop). We also sometimes "instantiate" the predType structure by defining a - coercion to the sort of the predPredType structure. This works better for - types such as {set T} that have subtypes that coerce to them, since the - same coercion will be inserted by the application of mem. It also lets us - turn any Type aT : predArgType into the total predicate over that type, - i.e., fun _: aT => true. This allows us to write, e.g., ##|'I_n| for the - cardinal of the (finite) type of integers less than n. - Collective predicates have a specific extensional equality, - - A =i B, - while applicative predicates use the extensional equality of functions, - - P =1 Q - The two forms are convertible, however. - We lift boolean operations to predicates, defining: - - predU (union), predI (intersection), predC (complement), - predD (difference), and preim (preimage, i.e., composition) - For each operation we define three forms, typically: - - predU : pred T -> pred T -> simpl_pred T - - #[#predU A & B#]#, a Notation for predU (mem A) (mem B) - - xpredU, a Notation for the lambda-expression inside predU, - which is mostly useful as an argument of =1, since it exposes the head - head constant of the expression to the ssreflect matching algorithm. - The syntax for the preimage of a collective predicate A is - - #[#preim f of A#]# - Finally, the generic syntax for defining a simpl_pred T is - - #[#pred x : T | P(x) #]#, #[#pred x | P(x) #]#, #[#pred x in A | P(x) #]#, etc. - We also support boolean relations, but only the applicative form, with - types - - rel T, an alias for T -> pred T - - simpl_rel T, an auto-simplifying version, and syntax - #[#rel x y | P(x,y) #]#, #[#rel x y in A & B | P(x,y) #]#, etc. - The notation #[#rel of fA#]# can be used to coerce a function returning a - collective predicate to one returning pred T. - Finally, note that there is specific support for ambivalent predicates - that can work in either style, as per this file's head descriptor. **) - + coercion to the sort of the predPredType structure, conveniently denoted + {pred T}. This works better for types such as {set T} that have subtypes that + coerce to them, since the same coercion will be inserted by the application + of mem, or of any lemma that expects a generic collective predicates with + type {pred T} := pred_sort (predPredType T) = pred T; thus {pred T} should be + the preferred type for generic collective predicate parameters. + This device also lets us turn any Type aT : predArgType into the total + predicate over that type, i.e., fun _: aT => true. This allows us to write, + e.g., ##|'I_n| for the cardinal of the (finite) type of integers less than n. + **) + +(** Boolean predicates. *) Definition pred T := T -> bool. - Identity Coercion fun_of_pred : pred >-> Funclass. -Definition rel T := T -> pred T. +Definition subpred T (p1 p2 : pred T) := forall x : T, p1 x -> p2 x. -Identity Coercion fun_of_rel : rel >-> Funclass. +(* Notation for some manifest predicates. *) -Notation xpred0 := (fun _ => false). -Notation xpredT := (fun _ => true). +Notation xpred0 := (fun=> false). +Notation xpredT := (fun=> true). Notation xpredI := (fun (p1 p2 : pred _) x => p1 x && p2 x). Notation xpredU := (fun (p1 p2 : pred _) x => p1 x || p2 x). Notation xpredC := (fun (p : pred _) x => ~~ p x). Notation xpredD := (fun (p1 p2 : pred _) x => ~~ p2 x && p1 x). Notation xpreim := (fun f (p : pred _) x => p (f x)). -Notation xrelU := (fun (r1 r2 : rel _) x y => r1 x y || r2 x y). -Section Predicates. +(** The packed class interface for pred-like types. **) -Variables T : Type. - -Definition subpred (p1 p2 : pred T) := forall x, p1 x -> p2 x. - -Definition subrel (r1 r2 : rel T) := forall x y, r1 x y -> r2 x y. - -Definition simpl_pred := simpl_fun T bool. -Definition applicative_pred := pred T. -Definition collective_pred := pred T. +#[universes(template)] +Structure predType T := + PredType {pred_sort :> Type; topred : pred_sort -> pred T}. + +Definition clone_pred T U := + fun pT & @pred_sort T pT -> U => + fun toP (pT' := @PredType T U toP) & phant_id pT' pT => pT'. +Notation "[ 'predType' 'of' T ]" := (@clone_pred _ T _ id _ id) : form_scope. + +Canonical predPredType T := PredType (@id (pred T)). +Canonical boolfunPredType T := PredType (@id (T -> bool)). + +(** The type of abstract collective predicates. + While {pred T} is contertible to pred T, it presents the pred_sort coercion + class, which crucially does _not_ coerce to Funclass. Term whose type P coerces + to {pred T} cannot be applied to arguments, but they _can_ be used as if P + had a canonical predType instance, as the coercion will be inserted if the + unification P =~= pred_sort ?pT fails, changing the problem into the trivial + {pred T} =~= pred_sort ?pT (solution ?pT := predPredType P). + Additional benefits of this approach are that any type coercing to P will + also inherit this behaviour, and that the coercion will be apparent in the + elaborated expression. The latter may be important if the coercion is also + a canonical structure projector - see mathcomp/fingroup/fingroup.v. The + main drawback of implementing predType by coercion in this way is that the + type of the value must be known when the unification constraint is imposed: + if we only register the constraint and then later discover later that the + expression had type P it will be too late of insert a coercion, whereas a + canonical instance of predType fo P would have solved the deferred constraint. + Finally, definitions, lemmas and sections should use type {pred T} for + their generic collective type parameters, as this will make it possible to + apply such definitions and lemmas directly to values of types that implement + predType by coercion to {pred T} (values of types that implement predType + without coercing to {pred T} will have to be coerced explicitly using topred). +**) +Notation "{ 'pred' T }" := (pred_sort (predPredType T)) : type_scope. + +(** The type of self-simplifying collective predicates. **) +Definition simpl_pred T := simpl_fun T bool. +Definition SimplPred {T} (p : pred T) : simpl_pred T := SimplFun p. + +(** Some simpl_pred constructors. **) + +Definition pred0 {T} := @SimplPred T xpred0. +Definition predT {T} := @SimplPred T xpredT. +Definition predI {T} (p1 p2 : pred T) := SimplPred (xpredI p1 p2). +Definition predU {T} (p1 p2 : pred T) := SimplPred (xpredU p1 p2). +Definition predC {T} (p : pred T) := SimplPred (xpredC p). +Definition predD {T} (p1 p2 : pred T) := SimplPred (xpredD p1 p2). +Definition preim {aT rT} (f : aT -> rT) (d : pred rT) := SimplPred (xpreim f d). + +Notation "[ 'pred' : T | E ]" := (SimplPred (fun _ : T => E%B)) : fun_scope. +Notation "[ 'pred' x | E ]" := (SimplPred (fun x => E%B)) : fun_scope. +Notation "[ 'pred' x | E1 & E2 ]" := [pred x | E1 && E2 ] : fun_scope. +Notation "[ 'pred' x : T | E ]" := + (SimplPred (fun x : T => E%B)) (only parsing) : fun_scope. +Notation "[ 'pred' x : T | E1 & E2 ]" := + [pred x : T | E1 && E2 ] (only parsing) : fun_scope. + +(** Coercions for simpl_pred. + As simpl_pred T values are used both applicatively and collectively we + need simpl_pred to coerce to both pred T _and_ {pred T}. However it is + undesireable to have two distinct constants for what are essentially identical + coercion functions, as this confuses the SSReflect keyed matching algorithm. + While the Coq Coercion declarations appear to disallow such Coercion aliasing, + it is possible to work around this limitation with a combination of modules + and functors, which we do below. + In addition we also give a predType instance for simpl_pred, which will + be preferred to the {pred T} coercion to solve simpl_pred T =~= pred_sort ?pT + constraints; not however that the pred_of_simpl coercion _will_ be used + when a simpl_pred T is passed as a {pred T}, since the simplPredType T + structure for simpl_pred T is _not_ convertible to predPredType T. **) + +Module PredOfSimpl. +Definition coerce T (sp : simpl_pred T) : pred T := fun_of_simpl sp. +End PredOfSimpl. +Notation pred_of_simpl := PredOfSimpl.coerce. +Coercion pred_of_simpl : simpl_pred >-> pred. +Canonical simplPredType T := PredType (@pred_of_simpl T). + +Module Type PredSortOfSimplSignature. +Parameter coerce : forall T, simpl_pred T -> {pred T}. +End PredSortOfSimplSignature. +Module DeclarePredSortOfSimpl (PredSortOfSimpl : PredSortOfSimplSignature). +Coercion PredSortOfSimpl.coerce : simpl_pred >-> pred_sort. +End DeclarePredSortOfSimpl. +Module Export PredSortOfSimplCoercion := DeclarePredSortOfSimpl PredOfSimpl. + +(** Type to pred coercion. + This lets us use types of sort predArgType as a synonym for their universal + predicate. We define this predicate as a simpl_pred T rather than a pred T or + a {pred T} so that /= and inE reduce (T x) and x \in T to true, respectively. + Unfortunately, this can't be used for existing types like bool whose sort + is already fixed (at least, not without redefining bool, true, false and + all bool operations and lemmas); we provide syntax to recast a given type + in predArgType as a workaround. **) +Definition predArgType := Type. +Bind Scope type_scope with predArgType. +Identity Coercion sort_of_predArgType : predArgType >-> Sortclass. +Coercion pred_of_argType (T : predArgType) : simpl_pred T := predT. +Notation "{ : T }" := (T%type : predArgType) : type_scope. -Definition SimplPred (p : pred T) : simpl_pred := SimplFun p. +(** Boolean relations. + Simplifying relations follow the coding pattern of 2-argument simplifying + functions: the simplifying type constructor is applied to the _last_ + argument. This design choice will let the in_simpl componenent of inE expand + membership in simpl_rel as well. We provide an explicit coercion to rel T + to avoid eta-expansion during coercion; this coercion self-simplifies so it + should be invisible. + **) -Coercion pred_of_simpl (p : simpl_pred) : pred T := fun_of_simpl p. -Coercion applicative_pred_of_simpl (p : simpl_pred) : applicative_pred := - fun_of_simpl p. -Coercion collective_pred_of_simpl (p : simpl_pred) : collective_pred := - fun x => (let: SimplFun f := p in fun _ => f x) x. -(** - Note: applicative_of_simpl is convertible to pred_of_simpl, while - collective_of_simpl is not. **) +Definition rel T := T -> pred T. +Identity Coercion fun_of_rel : rel >-> Funclass. -Definition pred0 := SimplPred xpred0. -Definition predT := SimplPred xpredT. -Definition predI p1 p2 := SimplPred (xpredI p1 p2). -Definition predU p1 p2 := SimplPred (xpredU p1 p2). -Definition predC p := SimplPred (xpredC p). -Definition predD p1 p2 := SimplPred (xpredD p1 p2). -Definition preim rT f (d : pred rT) := SimplPred (xpreim f d). +Definition subrel T (r1 r2 : rel T) := forall x y : T, r1 x y -> r2 x y. -Definition simpl_rel := simpl_fun T (pred T). +Definition simpl_rel T := T -> simpl_pred T. -Definition SimplRel (r : rel T) : simpl_rel := [fun x => r x]. +Coercion rel_of_simpl T (sr : simpl_rel T) : rel T := fun x : T => sr x. +Arguments rel_of_simpl {T} sr x /. -Coercion rel_of_simpl_rel (r : simpl_rel) : rel T := fun x y => r x y. +Notation xrelU := (fun (r1 r2 : rel _) x y => r1 x y || r2 x y). +Notation xrelpre := (fun f (r : rel _) x y => r (f x) (f y)). -Definition relU r1 r2 := SimplRel (xrelU r1 r2). +Definition SimplRel {T} (r : rel T) : simpl_rel T := fun x => SimplPred (r x). +Definition relU {T} (r1 r2 : rel T) := SimplRel (xrelU r1 r2). +Definition relpre {aT rT} (f : aT -> rT) (r : rel rT) := SimplRel (xrelpre f r). -Lemma subrelUl r1 r2 : subrel r1 (relU r1 r2). -Proof. by move=> *; apply/orP; left. Qed. +Notation "[ 'rel' x y | E ]" := (SimplRel (fun x y => E%B)) : fun_scope. +Notation "[ 'rel' x y : T | E ]" := + (SimplRel (fun x y : T => E%B)) (only parsing) : fun_scope. -Lemma subrelUr r1 r2 : subrel r2 (relU r1 r2). -Proof. by move=> *; apply/orP; right. Qed. +Lemma subrelUl T (r1 r2 : rel T) : subrel r1 (relU r1 r2). +Proof. by move=> x y r1xy; apply/orP; left. Qed. -#[universes(template)] -Variant mem_pred := Mem of pred T. +Lemma subrelUr T (r1 r2 : rel T) : subrel r2 (relU r1 r2). +Proof. by move=> x y r2xy; apply/orP; right. Qed. -Definition isMem pT topred mem := mem = (fun p : pT => Mem [eta topred p]). +(** Variant of simpl_pred specialised to the membership operator. **) #[universes(template)] -Structure predType := PredType { - pred_sort :> Type; - topred : pred_sort -> pred T; - _ : {mem | isMem topred mem} -}. - -Definition mkPredType pT toP := PredType (exist (@isMem pT toP) _ (erefl _)). - -Canonical predPredType := Eval hnf in @mkPredType (pred T) id. -Canonical simplPredType := Eval hnf in mkPredType pred_of_simpl. -Canonical boolfunPredType := Eval hnf in @mkPredType (T -> bool) id. - -Coercion pred_of_mem mp : pred_sort predPredType := let: Mem p := mp in [eta p]. -Canonical memPredType := Eval hnf in mkPredType pred_of_mem. - -Definition clone_pred U := - fun pT & pred_sort pT -> U => - fun a mP (pT' := @PredType U a mP) & phant_id pT' pT => pT'. - -End Predicates. - -Arguments pred0 {T}. -Arguments predT {T}. -Prenex Implicits pred0 predT predI predU predC predD preim relU. - -Notation "[ 'pred' : T | E ]" := (SimplPred (fun _ : T => E%B)) - (at level 0, format "[ 'pred' : T | E ]") : fun_scope. -Notation "[ 'pred' x | E ]" := (SimplPred (fun x => E%B)) - (at level 0, x ident, format "[ 'pred' x | E ]") : fun_scope. -Notation "[ 'pred' x | E1 & E2 ]" := [pred x | E1 && E2 ] - (at level 0, x ident, format "[ 'pred' x | E1 & E2 ]") : fun_scope. -Notation "[ 'pred' x : T | E ]" := (SimplPred (fun x : T => E%B)) - (at level 0, x ident, only parsing) : fun_scope. -Notation "[ 'pred' x : T | E1 & E2 ]" := [pred x : T | E1 && E2 ] - (at level 0, x ident, only parsing) : fun_scope. -Notation "[ 'rel' x y | E ]" := (SimplRel (fun x y => E%B)) - (at level 0, x ident, y ident, format "[ 'rel' x y | E ]") : fun_scope. -Notation "[ 'rel' x y : T | E ]" := (SimplRel (fun x y : T => E%B)) - (at level 0, x ident, y ident, only parsing) : fun_scope. - -Notation "[ 'predType' 'of' T ]" := (@clone_pred _ T _ id _ _ id) - (at level 0, format "[ 'predType' 'of' T ]") : form_scope. +Variant mem_pred T := Mem of pred T. (** - This redundant coercion lets us "inherit" the simpl_predType canonical - instance by declaring a coercion to simpl_pred. This hack is the only way - to put a predType structure on a predArgType. We use simpl_pred rather - than pred to ensure that /= removes the identity coercion. Note that the - coercion will never be used directly for simpl_pred, since the canonical - instance should always be resolved. **) - -Notation pred_class := (pred_sort (predPredType _)). -Coercion sort_of_simpl_pred T (p : simpl_pred T) : pred_class := p : pred T. + We mainly declare pred_of_mem as a coercion so that it is not displayed. + Similarly to pred_of_simpl, it will usually not be inserted by type + inference, as all mem_pred mp =~= pred_sort ?pT unification problems will + be solve by the memPredType instance below; pred_of_mem will however + be used if a mem_pred T is used as a {pred T}, which is desireable as it + will avoid a redundant mem in a collective, e.g., passing (mem A) to a lemma + expection a generic collective predicate p : {pred T} and premise x \in P + will display a subgoal x \in A rathere than x \in mem A. + Conversely, pred_of_mem will _not_ if it is used id (mem A) is used + applicatively or as a pred T; there the simpl_of_mem coercion defined below + will be used, resulting in a subgoal that displays as mem A x by simplifies + to x \in A. + **) +Coercion pred_of_mem {T} mp : {pred T} := let: Mem p := mp in [eta p]. +Canonical memPredType T := PredType (@pred_of_mem T). + +Definition in_mem {T} (x : T) mp := pred_of_mem mp x. +Definition eq_mem {T} mp1 mp2 := forall x : T, in_mem x mp1 = in_mem x mp2. +Definition sub_mem {T} mp1 mp2 := forall x : T, in_mem x mp1 -> in_mem x mp2. + +Arguments in_mem {T} x mp : simpl never. +Typeclasses Opaque eq_mem. +Typeclasses Opaque sub_mem. -(** - This lets us use some types as a synonym for their universal predicate. - Unfortunately, this won't work for existing types like bool, unless we - redefine bool, true, false and all bool ops. **) -Definition predArgType := Type. -Bind Scope type_scope with predArgType. -Identity Coercion sort_of_predArgType : predArgType >-> Sortclass. -Coercion pred_of_argType (T : predArgType) : simpl_pred T := predT. +(** The [simpl_of_mem; pred_of_simpl] path provides a new mem_pred >-> pred + coercion, but does _not_ override the pred_of_mem : mem_pred >-> pred_sort + explicit coercion declaration above. + **) +Coercion simpl_of_mem {T} mp := SimplPred (fun x : T => in_mem x mp). -Notation "{ : T }" := (T%type : predArgType) - (at level 0, format "{ : T }") : type_scope. +Lemma sub_refl T (mp : mem_pred T) : sub_mem mp mp. Proof. by []. Qed. +Arguments sub_refl {T mp} [x] mp_x. (** - These must be defined outside a Section because "cooking" kills the - nosimpl tag. **) - + It is essential to interlock the production of the Mem constructor inside + the branch of the predType match, to ensure that unifying mem A with + Mem [eta ?p] sets ?p := toP A (or ?p := P if toP = id and A = [eta P]), + rather than topred pT A, had we put mem A := Mem (topred A). +**) Definition mem T (pT : predType T) : pT -> mem_pred T := - nosimpl (let: @PredType _ _ _ (exist _ mem _) := pT return pT -> _ in mem). -Definition in_mem T x mp := nosimpl pred_of_mem T mp x. - -Prenex Implicits mem. - -Coercion pred_of_mem_pred T mp := [pred x : T | in_mem x mp]. - -Definition eq_mem T p1 p2 := forall x : T, in_mem x p1 = in_mem x p2. -Definition sub_mem T p1 p2 := forall x : T, in_mem x p1 -> in_mem x p2. - -Typeclasses Opaque eq_mem. - -Lemma sub_refl T (p : mem_pred T) : sub_mem p p. Proof. by []. Qed. -Arguments sub_refl {T p}. + let: PredType toP := pT in fun A => Mem [eta toP A]. +Arguments mem {T pT} A : rename, simpl never. Notation "x \in A" := (in_mem x (mem A)) : bool_scope. Notation "x \in A" := (in_mem x (mem A)) : bool_scope. Notation "x \notin A" := (~~ (x \in A)) : bool_scope. Notation "A =i B" := (eq_mem (mem A) (mem B)) : type_scope. -Notation "{ 'subset' A <= B }" := (sub_mem (mem A) (mem B)) - (at level 0, A, B at level 69, - format "{ '[hv' 'subset' A '/ ' <= B ']' }") : type_scope. -Notation "[ 'mem' A ]" := (pred_of_simpl (pred_of_mem_pred (mem A))) - (at level 0, only parsing) : fun_scope. -Notation "[ 'rel' 'of' fA ]" := (fun x => [mem (fA x)]) - (at level 0, format "[ 'rel' 'of' fA ]") : fun_scope. -Notation "[ 'predI' A & B ]" := (predI [mem A] [mem B]) - (at level 0, format "[ 'predI' A & B ]") : fun_scope. -Notation "[ 'predU' A & B ]" := (predU [mem A] [mem B]) - (at level 0, format "[ 'predU' A & B ]") : fun_scope. -Notation "[ 'predD' A & B ]" := (predD [mem A] [mem B]) - (at level 0, format "[ 'predD' A & B ]") : fun_scope. -Notation "[ 'predC' A ]" := (predC [mem A]) - (at level 0, format "[ 'predC' A ]") : fun_scope. -Notation "[ 'preim' f 'of' A ]" := (preim f [mem A]) - (at level 0, format "[ 'preim' f 'of' A ]") : fun_scope. - -Notation "[ 'pred' x 'in' A ]" := [pred x | x \in A] - (at level 0, x ident, format "[ 'pred' x 'in' A ]") : fun_scope. -Notation "[ 'pred' x 'in' A | E ]" := [pred x | x \in A & E] - (at level 0, x ident, format "[ 'pred' x 'in' A | E ]") : fun_scope. -Notation "[ 'pred' x 'in' A | E1 & E2 ]" := [pred x | x \in A & E1 && E2 ] - (at level 0, x ident, - format "[ 'pred' x 'in' A | E1 & E2 ]") : fun_scope. +Notation "{ 'subset' A <= B }" := (sub_mem (mem A) (mem B)) : type_scope. + +Notation "[ 'mem' A ]" := + (pred_of_simpl (simpl_of_mem (mem A))) (only parsing) : fun_scope. + +Notation "[ 'predI' A & B ]" := (predI [mem A] [mem B]) : fun_scope. +Notation "[ 'predU' A & B ]" := (predU [mem A] [mem B]) : fun_scope. +Notation "[ 'predD' A & B ]" := (predD [mem A] [mem B]) : fun_scope. +Notation "[ 'predC' A ]" := (predC [mem A]) : fun_scope. +Notation "[ 'preim' f 'of' A ]" := (preim f [mem A]) : fun_scope. +Notation "[ 'pred' x 'in' A ]" := [pred x | x \in A] : fun_scope. +Notation "[ 'pred' x 'in' A | E ]" := [pred x | x \in A & E] : fun_scope. +Notation "[ 'pred' x 'in' A | E1 & E2 ]" := + [pred x | x \in A & E1 && E2 ] : fun_scope. + Notation "[ 'rel' x y 'in' A & B | E ]" := - [rel x y | (x \in A) && (y \in B) && E] - (at level 0, x ident, y ident, - format "[ 'rel' x y 'in' A & B | E ]") : fun_scope. -Notation "[ 'rel' x y 'in' A & B ]" := [rel x y | (x \in A) && (y \in B)] - (at level 0, x ident, y ident, - format "[ 'rel' x y 'in' A & B ]") : fun_scope. -Notation "[ 'rel' x y 'in' A | E ]" := [rel x y in A & A | E] - (at level 0, x ident, y ident, - format "[ 'rel' x y 'in' A | E ]") : fun_scope. -Notation "[ 'rel' x y 'in' A ]" := [rel x y in A & A] - (at level 0, x ident, y ident, - format "[ 'rel' x y 'in' A ]") : fun_scope. - -Section simpl_mem. - -Variables (T : Type) (pT : predType T). -Implicit Types (x : T) (p : pred T) (sp : simpl_pred T) (pp : pT). + [rel x y | (x \in A) && (y \in B) && E] : fun_scope. +Notation "[ 'rel' x y 'in' A & B ]" := + [rel x y | (x \in A) && (y \in B)] : fun_scope. +Notation "[ 'rel' x y 'in' A | E ]" := [rel x y in A & A | E] : fun_scope. +Notation "[ 'rel' x y 'in' A ]" := [rel x y in A & A] : fun_scope. + +(** Aliases of pred T that let us tag intances of simpl_pred as applicative + or collective, via bespoke coercions. This tagging will give control over + the simplification behaviour of inE and othe rewriting lemmas below. + For this control to work it is crucial that collective_of_simpl _not_ + be convertible to either applicative_of_simpl or pred_of_simpl. Indeed + they differ here by a commutattive conversion (of the match and lambda). + **) +Definition applicative_pred T := pred T. +Definition collective_pred T := pred T. +Coercion applicative_pred_of_simpl T (sp : simpl_pred T) : applicative_pred T := + fun_of_simpl sp. +Coercion collective_pred_of_simpl T (sp : simpl_pred T) : collective_pred T := + let: SimplFun p := sp in p. + +(** Explicit simplification rules for predicate application and membership. **) +Section PredicateSimplification. + +Variables T : Type. + +Implicit Types (p : pred T) (pT : predType T) (sp : simpl_pred T). +Implicit Types (mp : mem_pred T). (** - Bespoke structures that provide fine-grained control over matching the - various forms of the \in predicate; note in particular the different forms - of hoisting that are used. We had to work around several bugs in the - implementation of unification, notably improper expansion of telescope - projections and overwriting of a variable assignment by a later - unification (probably due to conversion cache cross-talk). **) + The following four bespoke structures provide fine-grained control over + matching the various predicate forms. While all four follow a common pattern + of using a canonical projection to match a particular form of predicate + (in pred T, simpl_pred, mem_pred and mem_pred, respectively), and display + the matched predicate in the structure type, each is in fact used for a + different, specific purpose: + - registered_applicative_pred: this user-facing structure is used to + declare values of type pred T meant to be used applicatively. The + structure parameter merely displays this same value, and is used to avoid + undesireable, visible occurrence of the structure in the right hand side + of rewrite rules such as app_predE. + There is a canonical instance of registered_applicative_pred for values + of the applicative_of_simpl coercion, which handles the + Definition Apred : applicative_pred T := [pred x | ...] idiom. + This instance is mainly intended for the in_applicative component of inE, + in conjunction with manifest_mem_pred and applicative_mem_pred. + - manifest_simpl_pred: the only instance of this structure matches manifest + simpl_pred values of the form SimplPred p, displaying p in the structure + type. This structure is used in in_simpl to detect and selectively expand + collective predicates of this form. An explicit SimplPred p pattern would + _NOT_ work for this purpose, as then the left-hand side of in_simpl would + reduce to in_mem ?x (Mem [eta ?p]) and would thus match _any_ instance + of \in, not just those arising from a manifest simpl_pred. + - manifest_mem_pred: similar to manifest_simpl_pred, the one instance of this + structure matches manifest mem_pred values of the form Mem [eta ?p]. The + purpose is different however: to match and display in ?p the actual + predicate appearing in an ... \in ... expression matched by the left hand + side of the in_applicative component of inE; then + - applicative_mem_pred is a telescope refinement of manifest_mem_pred p with + a default constructor that checks that the predicate p is the value of a + registered_applicative_pred; any unfolding occurring during this check + does _not_ affect the value of p passed to in_applicative, since that + has been fixed earlier by the manifest_mem_pred match. In particular the + definition of a predicate using the applicative_pred_of_simpl idiom above + will not be expanded - this very case is the reason in_applicative uses + a mem_pred telescope in its left hand side. The more straighforward + ?x \in applicative_pred_value ?ap (equivalent to in_mem ?x (Mem ?ap)) + with ?ap : registered_applicative_pred ?p would set ?p := [pred x | ...] + rather than ?p := Apred in the example above. + Also note that the in_applicative component of inE must be come before the + in_simpl one, as the latter also matches terms of the form x \in Apred. + Finally, no component of inE matches x \in Acoll, when + Definition Acoll : collective_pred T := [pred x | ...]. + as the collective_pred_of_simpl is _not_ convertible to pred_of_simpl. **) + #[universes(template)] -Structure manifest_applicative_pred p := ManifestApplicativePred { - manifest_applicative_pred_value :> pred T; - _ : manifest_applicative_pred_value = p +Structure registered_applicative_pred p := RegisteredApplicativePred { + applicative_pred_value :> pred T; + _ : applicative_pred_value = p }. -Definition ApplicativePred p := ManifestApplicativePred (erefl p). +Definition ApplicativePred p := RegisteredApplicativePred (erefl p). Canonical applicative_pred_applicative sp := ApplicativePred (applicative_pred_of_simpl sp). #[universes(template)] Structure manifest_simpl_pred p := ManifestSimplPred { - manifest_simpl_pred_value :> simpl_pred T; - _ : manifest_simpl_pred_value = SimplPred p + simpl_pred_value :> simpl_pred T; + _ : simpl_pred_value = SimplPred p }. Canonical expose_simpl_pred p := ManifestSimplPred (erefl (SimplPred p)). #[universes(template)] Structure manifest_mem_pred p := ManifestMemPred { - manifest_mem_pred_value :> mem_pred T; - _ : manifest_mem_pred_value= Mem [eta p] + mem_pred_value :> mem_pred T; + _ : mem_pred_value = Mem [eta p] }. -Canonical expose_mem_pred p := @ManifestMemPred p _ (erefl _). +Canonical expose_mem_pred p := ManifestMemPred (erefl (Mem [eta p])). #[universes(template)] Structure applicative_mem_pred p := ApplicativeMemPred {applicative_mem_pred_value :> manifest_mem_pred p}. -Canonical check_applicative_mem_pred p (ap : manifest_applicative_pred p) mp := - @ApplicativeMemPred ap mp. +Canonical check_applicative_mem_pred p (ap : registered_applicative_pred p) := + [eta @ApplicativeMemPred ap]. -Lemma mem_topred (pp : pT) : mem (topred pp) = mem pp. -Proof. by rewrite /mem; case: pT pp => T1 app1 [mem1 /= ->]. Qed. +Lemma mem_topred pT (pp : pT) : mem (topred pp) = mem pp. +Proof. by case: pT pp. Qed. -Lemma topredE x (pp : pT) : topred pp x = (x \in pp). +Lemma topredE pT x (pp : pT) : topred pp x = (x \in pp). Proof. by rewrite -mem_topred. Qed. -Lemma app_predE x p (ap : manifest_applicative_pred p) : ap x = (x \in p). +Lemma app_predE x p (ap : registered_applicative_pred p) : ap x = (x \in p). Proof. by case: ap => _ /= ->. Qed. Lemma in_applicative x p (amp : applicative_mem_pred p) : in_mem x amp = p x. -Proof. by case: amp => [[_ /= ->]]. Qed. +Proof. by case: amp => -[_ /= ->]. Qed. Lemma in_collective x p (msp : manifest_simpl_pred p) : (x \in collective_pred_of_simpl msp) = p x. Proof. by case: msp => _ /= ->. Qed. Lemma in_simpl x p (msp : manifest_simpl_pred p) : - in_mem x (Mem [eta fun_of_simpl (msp : simpl_pred T)]) = p x. + in_mem x (Mem [eta pred_of_simpl msp]) = p x. Proof. by case: msp => _ /= ->. Qed. (** Because of the explicit eta expansion in the left-hand side, this lemma - should only be used in a right-to-left direction. The 8.3 hack allowing - partial right-to-left use does not work with the improved expansion - heuristics in 8.4. **) + should only be used in the left-to-right direction. + **) Lemma unfold_in x p : (x \in ([eta p] : pred T)) = p x. Proof. by []. Qed. @@ -1345,55 +1530,39 @@ Proof. by []. Qed. Definition memE := mem_simpl. (* could be extended *) -Lemma mem_mem (pp : pT) : (mem (mem pp) = mem pp) * (mem [mem pp] = mem pp). -Proof. by rewrite -mem_topred. Qed. +Lemma mem_mem mp : + (mem mp = mp) * (mem (mp : simpl_pred T) = mp) * (mem (mp : pred T) = mp). +Proof. by case: mp. Qed. -End simpl_mem. +End PredicateSimplification. (** Qualifiers and keyed predicates. **) #[universes(template)] -Variant qualifier (q : nat) T := Qualifier of predPredType T. +Variant qualifier (q : nat) T := Qualifier of {pred T}. -Coercion has_quality n T (q : qualifier n T) : pred_class := +Coercion has_quality n T (q : qualifier n T) : {pred T} := fun x => let: Qualifier _ p := q in p x. Arguments has_quality n {T}. Lemma qualifE n T p x : (x \in @Qualifier n T p) = p x. Proof. by []. Qed. -Notation "x \is A" := (x \in has_quality 0 A) - (at level 70, no associativity, - format "'[hv' x '/ ' \is A ']'") : bool_scope. -Notation "x \is 'a' A" := (x \in has_quality 1 A) - (at level 70, no associativity, - format "'[hv' x '/ ' \is 'a' A ']'") : bool_scope. -Notation "x \is 'an' A" := (x \in has_quality 2 A) - (at level 70, no associativity, - format "'[hv' x '/ ' \is 'an' A ']'") : bool_scope. -Notation "x \isn't A" := (x \notin has_quality 0 A) - (at level 70, no associativity, - format "'[hv' x '/ ' \isn't A ']'") : bool_scope. -Notation "x \isn't 'a' A" := (x \notin has_quality 1 A) - (at level 70, no associativity, - format "'[hv' x '/ ' \isn't 'a' A ']'") : bool_scope. -Notation "x \isn't 'an' A" := (x \notin has_quality 2 A) - (at level 70, no associativity, - format "'[hv' x '/ ' \isn't 'an' A ']'") : bool_scope. -Notation "[ 'qualify' x | P ]" := (Qualifier 0 (fun x => P%B)) - (at level 0, x at level 99, - format "'[hv' [ 'qualify' x | '/ ' P ] ']'") : form_scope. -Notation "[ 'qualify' x : T | P ]" := (Qualifier 0 (fun x : T => P%B)) - (at level 0, x at level 99, only parsing) : form_scope. -Notation "[ 'qualify' 'a' x | P ]" := (Qualifier 1 (fun x => P%B)) - (at level 0, x at level 99, - format "'[hv' [ 'qualify' 'a' x | '/ ' P ] ']'") : form_scope. -Notation "[ 'qualify' 'a' x : T | P ]" := (Qualifier 1 (fun x : T => P%B)) - (at level 0, x at level 99, only parsing) : form_scope. -Notation "[ 'qualify' 'an' x | P ]" := (Qualifier 2 (fun x => P%B)) - (at level 0, x at level 99, - format "'[hv' [ 'qualify' 'an' x | '/ ' P ] ']'") : form_scope. -Notation "[ 'qualify' 'an' x : T | P ]" := (Qualifier 2 (fun x : T => P%B)) - (at level 0, x at level 99, only parsing) : form_scope. +Notation "x \is A" := (x \in has_quality 0 A) : bool_scope. +Notation "x \is 'a' A" := (x \in has_quality 1 A) : bool_scope. +Notation "x \is 'an' A" := (x \in has_quality 2 A) : bool_scope. +Notation "x \isn't A" := (x \notin has_quality 0 A) : bool_scope. +Notation "x \isn't 'a' A" := (x \notin has_quality 1 A) : bool_scope. +Notation "x \isn't 'an' A" := (x \notin has_quality 2 A) : bool_scope. +Notation "[ 'qualify' x | P ]" := (Qualifier 0 (fun x => P%B)) : form_scope. +Notation "[ 'qualify' x : T | P ]" := + (Qualifier 0 (fun x : T => P%B)) (only parsing) : form_scope. +Notation "[ 'qualify' 'a' x | P ]" := (Qualifier 1 (fun x => P%B)) : form_scope. +Notation "[ 'qualify' 'a' x : T | P ]" := + (Qualifier 1 (fun x : T => P%B)) (only parsing) : form_scope. +Notation "[ 'qualify' 'an' x | P ]" := + (Qualifier 2 (fun x => P%B)) : form_scope. +Notation "[ 'qualify' 'an' x : T | P ]" := + (Qualifier 2 (fun x : T => P%B)) (only parsing) : form_scope. (** Keyed predicates: support for property-bearing predicate interfaces. **) @@ -1401,12 +1570,12 @@ Section KeyPred. Variable T : Type. #[universes(template)] -Variant pred_key (p : predPredType T) := DefaultPredKey. +Variant pred_key (p : {pred T}) := DefaultPredKey. -Variable p : predPredType T. +Variable p : {pred T}. #[universes(template)] Structure keyed_pred (k : pred_key p) := - PackKeyedPred {unkey_pred :> pred_class; _ : unkey_pred =i p}. + PackKeyedPred {unkey_pred :> {pred T}; _ : unkey_pred =i p}. Variable k : pred_key p. Definition KeyedPred := @PackKeyedPred k p (frefl _). @@ -1418,10 +1587,10 @@ Lemma keyed_predE : k_p =i p. Proof. by case: k_p. Qed. Instances that strip the mem cast; the first one has "pred_of_mem" as its projection head value, while the second has "pred_of_simpl". The latter has the side benefit of preempting accidental misdeclarations. - Note: pred_of_mem is the registered mem >-> pred_class coercion, while - simpl_of_mem; pred_of_simpl is the mem >-> pred >=> Funclass coercion. We + Note: pred_of_mem is the registered mem >-> pred_sort coercion, while + [simpl_of_mem; pred_of_simpl] is the mem >-> pred >=> Funclass coercion. We must write down the coercions explicitly as the Canonical head constant - computation does not strip casts !! **) + computation does not strip casts. **) Canonical keyed_mem := @PackKeyedPred k (pred_of_mem (mem k_p)) keyed_predE. Canonical keyed_mem_simpl := @@ -1429,8 +1598,8 @@ Canonical keyed_mem_simpl := End KeyPred. -Notation "x \i 'n' S" := (x \in @unkey_pred _ S _ _) - (at level 70, format "'[hv' x '/ ' \i 'n' S ']'") : bool_scope. +Local Notation in_unkey x S := (x \in @unkey_pred _ S _ _) (only parsing). +Notation "x \in S" := (in_unkey x S) (only printing) : bool_scope. Section KeyedQualifier. @@ -1447,12 +1616,12 @@ Canonical keyed_qualifier_keyed := PackKeyedPred k keyed_qualifier_suproof. End KeyedQualifier. -Notation "x \i 's' A" := (x \i n has_quality 0 A) - (at level 70, format "'[hv' x '/ ' \i 's' A ']'") : bool_scope. -Notation "x \i 's' 'a' A" := (x \i n has_quality 1 A) - (at level 70, format "'[hv' x '/ ' \i 's' 'a' A ']'") : bool_scope. -Notation "x \i 's' 'an' A" := (x \i n has_quality 2 A) - (at level 70, format "'[hv' x '/ ' \i 's' 'an' A ']'") : bool_scope. +Notation "x \is A" := + (in_unkey x (has_quality 0 A)) (only printing) : bool_scope. +Notation "x \is 'a' A" := + (in_unkey x (has_quality 1 A)) (only printing) : bool_scope. +Notation "x \is 'an' A" := + (in_unkey x (has_quality 2 A)) (only printing) : bool_scope. Module DefaultKeying. @@ -1592,7 +1761,7 @@ Definition prop_on2 Pf P & phantom T3 (Pf f) & ph {all2 P} := End LocalProperties. Definition inPhantom := Phantom Prop. -Definition onPhantom T P (x : T) := Phantom Prop (P x). +Definition onPhantom {T} P (x : T) := Phantom Prop (P x). Definition bijective_in aT rT (d : mem_pred aT) (f : aT -> rT) := exists2 g, prop_in1 d (inPhantom (cancel f g)) @@ -1602,59 +1771,30 @@ Definition bijective_on aT rT (cd : mem_pred rT) (f : aT -> rT) := exists2 g, prop_on1 cd (Phantom _ (cancel f)) (onPhantom (cancel f) g) & prop_in1 cd (inPhantom (cancel g f)). -Notation "{ 'for' x , P }" := - (prop_for x (inPhantom P)) - (at level 0, format "{ 'for' x , P }") : type_scope. - -Notation "{ 'in' d , P }" := - (prop_in1 (mem d) (inPhantom P)) - (at level 0, format "{ 'in' d , P }") : type_scope. - +Notation "{ 'for' x , P }" := (prop_for x (inPhantom P)) : type_scope. +Notation "{ 'in' d , P }" := (prop_in1 (mem d) (inPhantom P)) : type_scope. Notation "{ 'in' d1 & d2 , P }" := - (prop_in11 (mem d1) (mem d2) (inPhantom P)) - (at level 0, format "{ 'in' d1 & d2 , P }") : type_scope. - -Notation "{ 'in' d & , P }" := - (prop_in2 (mem d) (inPhantom P)) - (at level 0, format "{ 'in' d & , P }") : type_scope. - + (prop_in11 (mem d1) (mem d2) (inPhantom P)) : type_scope. +Notation "{ 'in' d & , P }" := (prop_in2 (mem d) (inPhantom P)) : type_scope. Notation "{ 'in' d1 & d2 & d3 , P }" := - (prop_in111 (mem d1) (mem d2) (mem d3) (inPhantom P)) - (at level 0, format "{ 'in' d1 & d2 & d3 , P }") : type_scope. - + (prop_in111 (mem d1) (mem d2) (mem d3) (inPhantom P)) : type_scope. Notation "{ 'in' d1 & & d3 , P }" := - (prop_in21 (mem d1) (mem d3) (inPhantom P)) - (at level 0, format "{ 'in' d1 & & d3 , P }") : type_scope. - + (prop_in21 (mem d1) (mem d3) (inPhantom P)) : type_scope. Notation "{ 'in' d1 & d2 & , P }" := - (prop_in12 (mem d1) (mem d2) (inPhantom P)) - (at level 0, format "{ 'in' d1 & d2 & , P }") : type_scope. - -Notation "{ 'in' d & & , P }" := - (prop_in3 (mem d) (inPhantom P)) - (at level 0, format "{ 'in' d & & , P }") : type_scope. - + (prop_in12 (mem d1) (mem d2) (inPhantom P)) : type_scope. +Notation "{ 'in' d & & , P }" := (prop_in3 (mem d) (inPhantom P)) : type_scope. Notation "{ 'on' cd , P }" := - (prop_on1 (mem cd) (inPhantom P) (inPhantom P)) - (at level 0, format "{ 'on' cd , P }") : type_scope. + (prop_on1 (mem cd) (inPhantom P) (inPhantom P)) : type_scope. Notation "{ 'on' cd & , P }" := - (prop_on2 (mem cd) (inPhantom P) (inPhantom P)) - (at level 0, format "{ 'on' cd & , P }") : type_scope. - -Local Arguments onPhantom {_%type_scope} _ _. + (prop_on2 (mem cd) (inPhantom P) (inPhantom P)) : type_scope. +Local Arguments onPhantom : clear scopes. Notation "{ 'on' cd , P & g }" := - (prop_on1 (mem cd) (Phantom (_ -> Prop) P) (onPhantom P g)) - (at level 0, format "{ 'on' cd , P & g }") : type_scope. - -Notation "{ 'in' d , 'bijective' f }" := (bijective_in (mem d) f) - (at level 0, f at level 8, - format "{ 'in' d , 'bijective' f }") : type_scope. - -Notation "{ 'on' cd , 'bijective' f }" := (bijective_on (mem cd) f) - (at level 0, f at level 8, - format "{ 'on' cd , 'bijective' f }") : type_scope. + (prop_on1 (mem cd) (Phantom (_ -> Prop) P) (onPhantom P g)) : type_scope. +Notation "{ 'in' d , 'bijective' f }" := (bijective_in (mem d) f) : type_scope. +Notation "{ 'on' cd , 'bijective' f }" := + (bijective_on (mem cd) f) : type_scope. (** Weakening and monotonicity lemmas for localized predicates. @@ -1666,7 +1806,7 @@ Notation "{ 'on' cd , 'bijective' f }" := (bijective_on (mem cd) f) Section LocalGlobal. Variables T1 T2 T3 : predArgType. -Variables (D1 : pred T1) (D2 : pred T2) (D3 : pred T3). +Variables (D1 : {pred T1}) (D2 : {pred T2}) (D3 : {pred T3}). Variables (d1 d1' : mem_pred T1) (d2 d2' : mem_pred T2) (d3 d3' : mem_pred T3). Variables (f f' : T1 -> T2) (g : T2 -> T1) (h : T3). Variables (P1 : T1 -> Prop) (P2 : T1 -> T2 -> Prop). @@ -1850,7 +1990,7 @@ End MonoHomoMorphismTheory. Section MonoHomoMorphismTheory_in. Variables (aT rT sT : predArgType) (f : aT -> rT) (g : rT -> aT). -Variable (aD : pred aT). +Variable (aD : {pred aT}). Variable (aP : pred aT) (rP : pred rT) (aR : rel aT) (rR : rel rT). Notation rD := [pred x | g x \in aD]. diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index a05b1e3d81..56f17703ff 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -426,8 +426,8 @@ let mk_anon_id t gl_ids = (set s i (Char.chr (Char.code (get s i) + 1)); s) in Id.of_string_soft (Bytes.to_string (loop (n - 1))) -let convert_concl_no_check t = Tactics.convert_concl_no_check t DEFAULTcast -let convert_concl t = Tactics.convert_concl t DEFAULTcast +let convert_concl_no_check t = Tactics.convert_concl ~check:false t DEFAULTcast +let convert_concl ~check t = Tactics.convert_concl ~check t DEFAULTcast let rename_hd_prod orig_name_ref gl = match EConstr.kind (project gl) (pf_concl gl) with @@ -799,7 +799,7 @@ let discharge_hyp (id', (id, mode)) gl = | NamedDecl.LocalDef (_, v, t), _ -> let id' = {(NamedDecl.get_annot decl) with binder_name = Name id'} in Proofview.V82.of_tactic - (convert_concl (EConstr.of_constr (mkLetIn (id', v, t, cl')))) gl + (convert_concl ~check:true (EConstr.of_constr (mkLetIn (id', v, t, cl')))) gl (* wildcard names *) let clear_wilds wilds gl = @@ -1170,7 +1170,7 @@ let gentac gen gl = ppdebug(lazy(str"c@gentac=" ++ pr_econstr_env (pf_env gl) (project gl) c)); let gl = pf_merge_uc ucst gl in if conv - then tclTHEN (Proofview.V82.of_tactic (convert_concl cl)) (old_cleartac clr) gl + then tclTHEN (Proofview.V82.of_tactic (convert_concl ~check:true cl)) (old_cleartac clr) gl else genclrtac cl [c] clr gl let genstac (gens, clr) = @@ -1215,7 +1215,7 @@ let unprotecttac gl = let prot, _ = EConstr.destConst (project gl) c in Tacticals.onClause (fun idopt -> let hyploc = Option.map (fun id -> id, InHyp) idopt in - Proofview.V82.of_tactic (Tactics.reduct_option + Proofview.V82.of_tactic (Tactics.reduct_option ~check:false (Reductionops.clos_norm_flags (CClosure.RedFlags.mkflags [CClosure.RedFlags.fBETA; @@ -1282,10 +1282,10 @@ let clr_of_wgen gen clrs = match gen with | clr, _ -> old_cleartac clr :: clrs -let reduct_in_concl t = Tactics.reduct_in_concl (t, DEFAULTcast) +let reduct_in_concl ~check t = Tactics.reduct_in_concl ~check (t, DEFAULTcast) let unfold cl = let module R = Reductionops in let module F = CClosure.RedFlags in - reduct_in_concl (R.clos_norm_flags (F.mkflags + reduct_in_concl ~check:false (R.clos_norm_flags (F.mkflags (List.map (fun c -> F.fCONST (fst (destConst (EConstr.Unsafe.to_constr c)))) cl @ [F.fBETA; F.fMATCH; F.fFIX; F.fCOFIX]))) @@ -1409,8 +1409,6 @@ let tclINTRO_ANON ?seed () = | Some seed -> tclINTRO ~id:(Seed seed) ~conclusion:return let tclRENAME_HD_PROD name = Goal.enter begin fun gl -> - let convert_concl_no_check t = - Tactics.convert_concl_no_check t DEFAULTcast in let concl = Goal.concl gl in let sigma = Goal.sigma gl in match EConstr.kind sigma concl with diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli index 58ce84ecb3..575f016014 100644 --- a/plugins/ssr/ssrcommon.mli +++ b/plugins/ssr/ssrcommon.mli @@ -252,7 +252,7 @@ val ssrevaltac : Tacinterp.interp_sign -> Tacinterp.Value.t -> unit Proofview.tactic val convert_concl_no_check : EConstr.t -> unit Proofview.tactic -val convert_concl : EConstr.t -> unit Proofview.tactic +val convert_concl : check:bool -> EConstr.t -> unit Proofview.tactic val red_safe : Reductionops.reduction_function -> diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v index 6c74ac1960..5e3e8ce5fb 100644 --- a/plugins/ssr/ssreflect.v +++ b/plugins/ssr/ssreflect.v @@ -28,6 +28,11 @@ Declare ML Module "ssreflect_plugin". argumentType c == the T such that c : forall x : T, P x. returnType c == the R such that c : T -> R. {type of c for s} == P s where c : forall x : T, P x. + nonPropType == an interface for non-Prop Types: a nonPropType coerces + to a Type, and only types that do _not_ have sort + Prop are canonical nonPropType instances. This is + useful for applied views (see mid-file comment). + notProp T == the nonPropType instance for type T. phantom T v == singleton type with inhabitant Phantom T v. phant T == singleton type with inhabitant Phant v. =^~ r == the converse of rewriting rule r (e.g., in a @@ -57,8 +62,6 @@ Declare ML Module "ssreflect_plugin". More information about these definitions and their use can be found in the ssreflect manual, and in specific comments below. **) - - Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -77,7 +80,8 @@ Reserved Notation "(* 69 *)" (at level 69). (** Non ambiguous keyword to check if the SsrSyntax module is imported **) Reserved Notation "(* Use to test if 'SsrSyntax_is_Imported' *)" (at level 8). -Reserved Notation "<hidden n >" (at level 200). +Reserved Notation "<hidden n >" (at level 0, n at level 0, + format "<hidden n >"). Reserved Notation "T (* n *)" (at level 200, format "T (* n *)"). End SsrSyntax. @@ -85,6 +89,39 @@ End SsrSyntax. Export SsrMatchingSyntax. Export SsrSyntax. +(** Save primitive notation that will be overloaded. **) +Local Notation CoqGenericIf c vT vF := (if c then vT else vF) (only parsing). +Local Notation CoqGenericDependentIf c x R vT vF := + (if c as x return R then vT else vF) (only parsing). +Local Notation CoqCast x T := (x : T) (only parsing). + +(** Reserve notation that introduced in this file. **) +Reserved Notation "'if' c 'then' vT 'else' vF" (at level 200, + c, vT, vF at level 200, only parsing). +Reserved Notation "'if' c 'return' R 'then' vT 'else' vF" (at level 200, + c, R, vT, vF at level 200, only parsing). +Reserved Notation "'if' c 'as' x 'return' R 'then' vT 'else' vF" (at level 200, + c, R, vT, vF at level 200, x ident, only parsing). + +Reserved Notation "x : T" (at level 100, right associativity, + format "'[hv' x '/ ' : T ']'"). +Reserved Notation "T : 'Type'" (at level 100, format "T : 'Type'"). +Reserved Notation "P : 'Prop'" (at level 100, format "P : 'Prop'"). + +Reserved Notation "[ 'the' sT 'of' v 'by' f ]" (at level 0, + format "[ 'the' sT 'of' v 'by' f ]"). +Reserved Notation "[ 'the' sT 'of' v ]" (at level 0, + format "[ 'the' sT 'of' v ]"). +Reserved Notation "{ 'type' 'of' c 'for' s }" (at level 0, + format "{ 'type' 'of' c 'for' s }"). + +Reserved Notation "=^~ r" (at level 100, format "=^~ r"). + +Reserved Notation "[ 'unlockable' 'of' C ]" (at level 0, + format "[ 'unlockable' 'of' C ]"). +Reserved Notation "[ 'unlockable' 'fun' C ]" (at level 0, + format "[ 'unlockable' 'fun' C ]"). + (** To define notations for tactic in intro patterns. When "=> /t" is parsed, "t:%ssripat" is actually interpreted. **) @@ -100,32 +137,28 @@ Delimit Scope ssripat_scope with ssripat. Declare Scope general_if_scope. Delimit Scope general_if_scope with GEN_IF. -Notation "'if' c 'then' v1 'else' v2" := - (if c then v1 else v2) - (at level 200, c, v1, v2 at level 200, only parsing) : general_if_scope. +Notation "'if' c 'then' vT 'else' vF" := + (CoqGenericIf c vT vF) (only parsing) : general_if_scope. -Notation "'if' c 'return' t 'then' v1 'else' v2" := - (if c return t then v1 else v2) - (at level 200, c, t, v1, v2 at level 200, only parsing) : general_if_scope. +Notation "'if' c 'return' R 'then' vT 'else' vF" := + (CoqGenericDependentIf c c R vT vF) (only parsing) : general_if_scope. -Notation "'if' c 'as' x 'return' t 'then' v1 'else' v2" := - (if c as x return t then v1 else v2) - (at level 200, c, t, v1, v2 at level 200, x ident, only parsing) - : general_if_scope. +Notation "'if' c 'as' x 'return' R 'then' vT 'else' vF" := + (CoqGenericDependentIf c x R vT vF) (only parsing) : general_if_scope. (** Force boolean interpretation of simple if expressions. **) Declare Scope boolean_if_scope. Delimit Scope boolean_if_scope with BOOL_IF. -Notation "'if' c 'return' t 'then' v1 'else' v2" := - (if c%bool is true in bool return t then v1 else v2) : boolean_if_scope. +Notation "'if' c 'return' R 'then' vT 'else' vF" := + (if c is true as c in bool return R then vT else vF) : boolean_if_scope. -Notation "'if' c 'then' v1 'else' v2" := - (if c%bool is true in bool return _ then v1 else v2) : boolean_if_scope. +Notation "'if' c 'then' vT 'else' vF" := + (if c%bool is true as _ in bool return _ then vT else vF) : boolean_if_scope. -Notation "'if' c 'as' x 'return' t 'then' v1 'else' v2" := - (if c%bool is true as x in bool return t then v1 else v2) : boolean_if_scope. +Notation "'if' c 'as' x 'return' R 'then' vT 'else' vF" := + (if c%bool is true as x in bool return R then vT else vF) : boolean_if_scope. Open Scope boolean_if_scope. @@ -149,19 +182,15 @@ Open Scope form_scope. precedence of the notation, which binds less tightly than application), and put printing boxes that print the type of a long definition on a separate line rather than force-fit it at the right margin. **) -Notation "x : T" := (x : T) - (at level 100, right associativity, - format "'[hv' x '/ ' : T ']'") : core_scope. +Notation "x : T" := (CoqCast x T) : core_scope. (** Allow the casual use of notations like nat * nat for explicit Type declarations. Note that (nat * nat : Type) is NOT equivalent to (nat * nat)%%type, whose inferred type is legacy type "Set". **) -Notation "T : 'Type'" := (T%type : Type) - (at level 100, only parsing) : core_scope. +Notation "T : 'Type'" := (CoqCast T%type Type) (only parsing) : core_scope. (** Allow similarly Prop annotation for, e.g., rewrite multirules. **) -Notation "P : 'Prop'" := (P%type : Prop) - (at level 100, only parsing) : core_scope. +Notation "P : 'Prop'" := (CoqCast P%type Prop) (only parsing) : core_scope. (** Constants for abstract: and #[#: name #]# intro pattern **) Definition abstract_lock := unit. @@ -170,8 +199,10 @@ Definition abstract_key := tt. Definition abstract (statement : Type) (id : nat) (lock : abstract_lock) := let: tt := lock in statement. -Notation "<hidden n >" := (abstract _ n _). -Notation "T (* n *)" := (abstract T n abstract_key). +Declare Scope ssr_scope. +Notation "<hidden n >" := (abstract _ n _) : ssr_scope. +Notation "T (* n *)" := (abstract T n abstract_key) : ssr_scope. +Open Scope ssr_scope. Register abstract_lock as plugins.ssreflect.abstract_lock. Register abstract_key as plugins.ssreflect.abstract_key. @@ -222,28 +253,27 @@ Local Arguments get_by _%type_scope _%type_scope _ _ _ _. Notation "[ 'the' sT 'of' v 'by' f ]" := (@get_by _ sT f _ _ ((fun v' (s : sT) => Put v' (f s) s) v _)) - (at level 0, only parsing) : form_scope. + (only parsing) : form_scope. -Notation "[ 'the' sT 'of' v ]" := (get ((fun s : sT => Put v (*coerce*)s s) _)) - (at level 0, only parsing) : form_scope. +Notation "[ 'the' sT 'of' v ]" := (get ((fun s : sT => Put v (*coerce*) s s) _)) + (only parsing) : form_scope. (** - The following are "format only" versions of the above notations. Since Coq - doesn't provide this facility, we fake it by splitting the "the" keyword. + The following are "format only" versions of the above notations. We need to do this to prevent the formatter from being be thrown off by application collapsing, coercion insertion and beta reduction in the right hand side of the notations above. **) -Notation "[ 'th' 'e' sT 'of' v 'by' f ]" := (@get_by _ sT f v _ _) - (at level 0, format "[ 'th' 'e' sT 'of' v 'by' f ]") : form_scope. +Notation "[ 'the' sT 'of' v 'by' f ]" := (@get_by _ sT f v _ _) + (only printing) : form_scope. -Notation "[ 'th' 'e' sT 'of' v ]" := (@get _ sT v _ _) - (at level 0, format "[ 'th' 'e' sT 'of' v ]") : form_scope. +Notation "[ 'the' sT 'of' v ]" := (@get _ sT v _ _) + (only printing) : form_scope. (** We would like to recognize -Notation " #[# 'th' 'e' sT 'of' v : 'Type' #]#" := (@get Type sT v _ _) - (at level 0, format " #[# 'th' 'e' sT 'of' v : 'Type' #]#") : form_scope. +Notation " #[# 'the' sT 'of' v : 'Type' #]#" := (@get Type sT v _ _) + (at level 0, format " #[# 'the' sT 'of' v : 'Type' #]#") : form_scope. **) (** @@ -278,8 +308,7 @@ Definition argumentType T P & forall x : T, P x := T. Definition dependentReturnType T P & forall x : T, P x := P. Definition returnType aT rT & aT -> rT := rT. -Notation "{ 'type' 'of' c 'for' s }" := (dependentReturnType c s) - (at level 0, format "{ 'type' 'of' c 'for' s }") : type_scope. +Notation "{ 'type' 'of' c 'for' s }" := (dependentReturnType c s) : type_scope. (** A generic "phantom" type (actually, a unit type with a phantom parameter). @@ -330,7 +359,7 @@ Notation unkeyed x := (let flex := x in flex). (** Ssreflect converse rewrite rule rule idiom. **) Definition ssr_converse R (r : R) := (Logic.I, r). -Notation "=^~ r" := (ssr_converse r) (at level 100) : form_scope. +Notation "=^~ r" := (ssr_converse r) : form_scope. (** Term tagging (user-level). @@ -397,11 +426,11 @@ Ltac ssrdone0 := Structure unlockable T v := Unlockable {unlocked : T; _ : unlocked = v}. Lemma unlock T x C : @unlocked T x C = x. Proof. by case: C. Qed. -Notation "[ 'unlockable' 'of' C ]" := (@Unlockable _ _ C (unlock _)) - (at level 0, format "[ 'unlockable' 'of' C ]") : form_scope. +Notation "[ 'unlockable' 'of' C ]" := + (@Unlockable _ _ C (unlock _)) : form_scope. -Notation "[ 'unlockable' 'fun' C ]" := (@Unlockable _ (fun _ => _) C (unlock _)) - (at level 0, format "[ 'unlockable' 'fun' C ]") : form_scope. +Notation "[ 'unlockable' 'fun' C ]" := + (@Unlockable _ (fun _ => _) C (unlock _)) : form_scope. (** Generic keyed constant locking. **) @@ -418,7 +447,7 @@ Proof. by case: k. Qed. Canonical locked_with_unlockable T k x := @Unlockable T x (locked_with k x) (locked_withE k x). -(** More accurate variant of unlock, and safer alternative to locked_withE. **) +(** More accurate variant of unlock, and safer alternative to locked_withE. **) Lemma unlock_with T k x : unlocked (locked_with_unlockable k x) = x :> T. Proof. exact: unlock. Qed. @@ -597,3 +626,102 @@ Ltac over := | apply: Under_iff.under_iff_done | rewrite over ]. + +(** An interface for non-Prop types; used to avoid improper instantiation + of polymorphic lemmas with on-demand implicits when they are used as views. + For example: Some_inj {T} : forall x y : T, Some x = Some y -> x = y. + Using move/Some_inj on a goal of the form Some n = Some 0 will fail: + SSReflect will interpret the view as @Some_inj ?T _top_assumption_ + since this is the well-typed application of the view with the minimal + number of inserted evars (taking ?T := Some n = Some 0), and then will + later complain that it cannot erase _top_assumption_ after having + abstracted the viewed assumption. Making x and y maximal implicits + would avoid this and force the intended @Some_inj nat x y _top_assumption_ + interpretation, but is undesireable as it makes it harder to use Some_inj + with the many SSReflect and MathComp lemmas that have an injectivity + premise. Specifying {T : nonPropType} solves this more elegantly, as then + (?T : Type) no longer unifies with (Some n = Some 0), which has sort Prop. + **) + +Module NonPropType. + +(** Implementation notes: + We rely on three interface Structures: + - test_of r, the middle structure, performs the actual check: it has two + canonical instances whose 'condition' projection are maybeProj (?P : Prop) + and tt, and which set r := true and r := false, respectively. Unifying + condition (?t : test_of ?r) with maybeProj T will thus set ?r to true if + T is in Prop as the test_Prop T instance will apply, and otherwise simplify + maybeProp T to tt and use the test_negative instance and set ?r to false. + - call_of c r sets up a call to test_of on condition c with expected result r. + It has a default instance for its 'callee' projection to Type, which + sets c := maybeProj T and r := false whe unifying with a type T. + - type is a telescope on call_of c r, which checks that unifying test_of ?r1 + with c indeed sets ?r1 := r; the type structure bundles the 'test' instance + and its 'result' value along with its call_of c r projection. The default + instance essentially provides eta-expansion for 'type'. This is only + essential for the first 'result' projection to bool; using the instance + for other projection merely avoids spurrious delta expansions that would + spoil the notProp T notation. + In detail, unifying T =~= ?S with ?S : nonPropType, i.e., + (1) T =~= @callee (@condition (result ?S) (test ?S)) (result ?S) (frame ?S) + first uses the default call instance with ?T := T to reduce (1) to + (2a) @condition (result ?S) (test ?S) =~= maybeProp T + (3) result ?S =~= false + (4) frame ?S =~= call T + along with some trivial universe-related checks which are irrelevant here. + Then the unification tries to use the test_Prop instance to reduce (2a) to + (6a) result ?S =~= true + (7a) ?P =~= T with ?P : Prop + (8a) test ?S =~= test_Prop ?P + Now the default 'check' instance with ?result := true resolves (6a) as + (9a) ?S := @check true ?test ?frame + Then (7a) can be solved precisely if T has sort at most (hence exactly) Prop, + and then (8a) is solved by the check instance, yielding ?test := test_Prop T, + and completing the solution of (2a), and _committing_ to it. But now (3) is + inconsistent with (9a), and this makes the entire problem (1) fails. + If on the othe hand T does not have sort Prop then (7a) fails and the + unification resorts to delta expanding (2a), which gives + (2b) @condition (result ?S) (test ?S) =~= tt + which is then reduced, using the test_negative instance, to + (6b) result ?S =~= false + (8b) test ?S =~= test_negative + Both are solved using the check default instance, as in the (2a) branch, giving + (9b) ?S := @check false test_negative ?frame + Then (3) and (4) are similarly soved using check, giving the final assignment + (9) ?S := notProp T + Observe that we _must_ perform the actual test unification on the arguments + of the initial canonical instance, and not on the instance itself as we do + in mathcomp/matrix and mathcomp/vector, because we want the unification to + fail when T has sort Prop. If both the test_of _and_ the result check + unifications were done as part of the structure telescope then the latter + would be a sub-problem of the former, and thus failing the check would merely + make the test_of unification backtrack and delta-expand and we would not get + failure. + **) + +Structure call_of (condition : unit) (result : bool) := Call {callee : Type}. +Definition maybeProp (T : Type) := tt. +Definition call T := Call (maybeProp T) false T. + +Structure test_of (result : bool) := Test {condition :> unit}. +Definition test_Prop (P : Prop) := Test true (maybeProp P). +Definition test_negative := Test false tt. + +Structure type := + Check {result : bool; test : test_of result; frame : call_of test result}. +Definition check result test frame := @Check result test frame. + +Module Exports. +Canonical call. +Canonical test_Prop. +Canonical test_negative. +Canonical check. +Notation nonPropType := type. +Coercion callee : call_of >-> Sortclass. +Coercion frame : type >-> call_of. +Notation notProp T := (@check false test_negative (call T)). +End Exports. + +End NonPropType. +Export NonPropType.Exports. diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index ad20113320..93c0d5c236 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -118,7 +118,7 @@ let newssrcongrtac arg ist gl = match try Some (pf_unify_HO gl_c (pf_concl gl) c) with exn when CErrors.noncritical exn -> None with | Some gl_c -> - tclTHEN (Proofview.V82.of_tactic (convert_concl (fs gl_c c))) + tclTHEN (Proofview.V82.of_tactic (convert_concl ~check:true (fs gl_c c))) (t_ok (proj gl_c)) gl | None -> t_fail () gl in let mk_evar gl ty = @@ -276,7 +276,7 @@ let unfoldintac occ rdx t (kt,_) gl = try beta env0 (EConstr.of_constr (eval_pattern env0 sigma0 concl0 rdx occ unfold)) with Option.IsNone -> errorstrm Pp.(str"Failed to unfold " ++ pr_econstr_pat env0 sigma t) in let _ = conclude () in - Proofview.V82.of_tactic (convert_concl concl) gl + Proofview.V82.of_tactic (convert_concl ~check:true concl) gl ;; let foldtac occ rdx ft gl = @@ -303,7 +303,7 @@ let foldtac occ rdx ft gl = let concl0 = EConstr.Unsafe.to_constr concl0 in let concl = eval_pattern env0 sigma0 concl0 rdx occ fold in let _ = conclude () in - Proofview.V82.of_tactic (convert_concl (EConstr.of_constr concl)) gl + Proofview.V82.of_tactic (convert_concl ~check:true (EConstr.of_constr concl)) gl ;; let converse_dir = function L2R -> R2L | R2L -> L2R @@ -406,7 +406,7 @@ let rwcltac ?under ?map_redex cl rdx dir sr gl = let cl' = EConstr.mkApp (EConstr.mkNamedLambda (make_annot pattern_id Sorts.Relevant) rdxt cl, [|rdx|]) in let sigma, _ = Typing.type_of env sigma cl' in let gl = pf_merge_uc_of sigma gl in - Proofview.V82.of_tactic (convert_concl cl'), rewritetac ?under dir r', gl + Proofview.V82.of_tactic (convert_concl ~check:true cl'), rewritetac ?under dir r', gl else let dc, r2 = EConstr.decompose_lam_n_assum (project gl) n r' in let r3, _, r3t = @@ -446,7 +446,7 @@ let lz_setoid_relation = | Some (env', srel) when env' == env -> srel | _ -> let srel = - try Some (UnivGen.constr_of_global @@ + try Some (UnivGen.constr_of_monomorphic_global @@ Coqlib.find_reference "Class_setoid" ("Coq"::sdir) "RewriteRelation" [@ocaml.warning "-3"]) with _ -> None in last_srel := Some (env, srel); srel @@ -491,7 +491,7 @@ let rwprocess_rule dir rule gl = | _ -> let sigma, pi2 = Evd.fresh_global env sigma coq_prod.Coqlib.proj2 in EConstr.mkApp (pi2, ra), sigma in - if EConstr.eq_constr sigma a.(0) (EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.(lib_ref "core.True.type"))) then + if EConstr.eq_constr sigma a.(0) (EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.(lib_ref "core.True.type"))) then let s, sigma = sr sigma 2 in loop (converse_dir d) sigma s a.(1) rs 0 else @@ -644,7 +644,7 @@ let unfoldtac occ ko t kt gl = let cl' = EConstr.Vars.subst1 (pf_unfoldn [OnlyOccurrences [1], get_evalref env (project gl) c] gl c) cl in let f = if ko = None then CClosure.betaiotazeta else CClosure.betaiota in Proofview.V82.of_tactic - (convert_concl (pf_reduce (Reductionops.clos_norm_flags f) gl cl')) gl + (convert_concl ~check:true (pf_reduce (Reductionops.clos_norm_flags f) gl cl')) gl let unlocktac ist args gl = let utac (occ, gt) gl = diff --git a/plugins/ssr/ssrfun.v b/plugins/ssr/ssrfun.v index b51ffada0c..46af775296 100644 --- a/plugins/ssr/ssrfun.v +++ b/plugins/ssr/ssrfun.v @@ -219,25 +219,113 @@ Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. -Declare Scope fun_scope. -Delimit Scope fun_scope with FUN. -Open Scope fun_scope. +(** Parsing / printing declarations. *) +Reserved Notation "p .1" (at level 2, left associativity, format "p .1"). +Reserved Notation "p .2" (at level 2, left associativity, format "p .2"). +Reserved Notation "f ^~ y" (at level 10, y at level 8, no associativity, + format "f ^~ y"). +Reserved Notation "@^~ x" (at level 10, x at level 8, no associativity, + format "@^~ x"). +Reserved Notation "[ 'eta' f ]" (at level 0, format "[ 'eta' f ]"). +Reserved Notation "'fun' => E" (at level 200, format "'fun' => E"). + +Reserved Notation "[ 'fun' : T => E ]" (at level 0, + format "'[hv' [ 'fun' : T => '/ ' E ] ']'"). +Reserved Notation "[ 'fun' x => E ]" (at level 0, + x ident, format "'[hv' [ 'fun' x => '/ ' E ] ']'"). +Reserved Notation "[ 'fun' x : T => E ]" (at level 0, + x ident, format "'[hv' [ 'fun' x : T => '/ ' E ] ']'"). +Reserved Notation "[ 'fun' x y => E ]" (at level 0, + x ident, y ident, format "'[hv' [ 'fun' x y => '/ ' E ] ']'"). +Reserved Notation "[ 'fun' x y : T => E ]" (at level 0, + x ident, y ident, format "'[hv' [ 'fun' x y : T => '/ ' E ] ']'"). +Reserved Notation "[ 'fun' ( x : T ) y => E ]" (at level 0, + x ident, y ident, format "'[hv' [ 'fun' ( x : T ) y => '/ ' E ] ']'"). +Reserved Notation "[ 'fun' x ( y : T ) => E ]" (at level 0, + x ident, y ident, format "'[hv' [ 'fun' x ( y : T ) => '/ ' E ] ']'"). +Reserved Notation "[ 'fun' ( x : T ) ( y : U ) => E ]" (at level 0, + x ident, y ident, format "[ 'fun' ( x : T ) ( y : U ) => E ]" ). + +Reserved Notation "f =1 g" (at level 70, no associativity). +Reserved Notation "f =1 g :> A" (at level 70, g at next level, A at level 90). +Reserved Notation "f =2 g" (at level 70, no associativity). +Reserved Notation "f =2 g :> A" (at level 70, g at next level, A at level 90). +Reserved Notation "f \o g" (at level 50, format "f \o '/ ' g"). +Reserved Notation "f \; g" (at level 60, right associativity, + format "f \; '/ ' g"). + +Reserved Notation "{ 'morph' f : x / a >-> r }" (at level 0, f at level 99, + x ident, format "{ 'morph' f : x / a >-> r }"). +Reserved Notation "{ 'morph' f : x / a }" (at level 0, f at level 99, + x ident, format "{ 'morph' f : x / a }"). +Reserved Notation "{ 'morph' f : x y / a >-> r }" (at level 0, f at level 99, + x ident, y ident, format "{ 'morph' f : x y / a >-> r }"). +Reserved Notation "{ 'morph' f : x y / a }" (at level 0, f at level 99, + x ident, y ident, format "{ 'morph' f : x y / a }"). +Reserved Notation "{ 'homo' f : x / a >-> r }" (at level 0, f at level 99, + x ident, format "{ 'homo' f : x / a >-> r }"). +Reserved Notation "{ 'homo' f : x / a }" (at level 0, f at level 99, + x ident, format "{ 'homo' f : x / a }"). +Reserved Notation "{ 'homo' f : x y / a >-> r }" (at level 0, f at level 99, + x ident, y ident, format "{ 'homo' f : x y / a >-> r }"). +Reserved Notation "{ 'homo' f : x y / a }" (at level 0, f at level 99, + x ident, y ident, format "{ 'homo' f : x y / a }"). +Reserved Notation "{ 'homo' f : x y /~ a }" (at level 0, f at level 99, + x ident, y ident, format "{ 'homo' f : x y /~ a }"). +Reserved Notation "{ 'mono' f : x / a >-> r }" (at level 0, f at level 99, + x ident, format "{ 'mono' f : x / a >-> r }"). +Reserved Notation "{ 'mono' f : x / a }" (at level 0, f at level 99, + x ident, format "{ 'mono' f : x / a }"). +Reserved Notation "{ 'mono' f : x y / a >-> r }" (at level 0, f at level 99, + x ident, y ident, format "{ 'mono' f : x y / a >-> r }"). +Reserved Notation "{ 'mono' f : x y / a }" (at level 0, f at level 99, + x ident, y ident, format "{ 'mono' f : x y / a }"). +Reserved Notation "{ 'mono' f : x y /~ a }" (at level 0, f at level 99, + x ident, y ident, format "{ 'mono' f : x y /~ a }"). + +Reserved Notation "@ 'id' T" (at level 10, T at level 8, format "@ 'id' T"). +Reserved Notation "@ 'sval'" (at level 10, format "@ 'sval'"). -(** Notations for argument transpose **) -Notation "f ^~ y" := (fun x => f x y) - (at level 10, y at level 8, no associativity, format "f ^~ y") : fun_scope. -Notation "@^~ x" := (fun f => f x) - (at level 10, x at level 8, no associativity, format "@^~ x") : fun_scope. +(** + Syntax for defining auxiliary recursive function. + Usage: + Section FooDefinition. + Variables (g1 : T1) (g2 : T2). (globals) + Fixoint foo_auxiliary (a3 : T3) ... := + body, using #[#rec e3, ... #]# for recursive calls + where " #[# 'rec' a3 , a4 , ... #]#" := foo_auxiliary. + Definition foo x y .. := #[#rec e1, ... #]#. + + proofs about foo + End FooDefinition. **) + +Reserved Notation "[ 'rec' a ]" (at level 0, + format "[ 'rec' a ]"). +Reserved Notation "[ 'rec' a , b ]" (at level 0, + format "[ 'rec' a , b ]"). +Reserved Notation "[ 'rec' a , b , c ]" (at level 0, + format "[ 'rec' a , b , c ]"). +Reserved Notation "[ 'rec' a , b , c , d ]" (at level 0, + format "[ 'rec' a , b , c , d ]"). +Reserved Notation "[ 'rec' a , b , c , d , e ]" (at level 0, + format "[ 'rec' a , b , c , d , e ]"). +Reserved Notation "[ 'rec' a , b , c , d , e , f ]" (at level 0, + format "[ 'rec' a , b , c , d , e , f ]"). +Reserved Notation "[ 'rec' a , b , c , d , e , f , g ]" (at level 0, + format "[ 'rec' a , b , c , d , e , f , g ]"). +Reserved Notation "[ 'rec' a , b , c , d , e , f , g , h ]" (at level 0, + format "[ 'rec' a , b , c , d , e , f , g , h ]"). +Reserved Notation "[ 'rec' a , b , c , d , e , f , g , h , i ]" (at level 0, + format "[ 'rec' a , b , c , d , e , f , g , h , i ]"). +Reserved Notation "[ 'rec' a , b , c , d , e , f , g , h , i , j ]" (at level 0, + format "[ 'rec' a , b , c , d , e , f , g , h , i , j ]"). Declare Scope pair_scope. Delimit Scope pair_scope with PAIR. Open Scope pair_scope. (** Notations for pair/conjunction projections **) -Notation "p .1" := (fst p) - (at level 2, left associativity, format "p .1") : pair_scope. -Notation "p .2" := (snd p) - (at level 2, left associativity, format "p .2") : pair_scope. +Notation "p .1" := (fst p) : pair_scope. +Notation "p .2" := (snd p) : pair_scope. Coercion pair_of_and P Q (PandQ : P /\ Q) := (proj1 PandQ, proj2 PandQ). @@ -291,41 +379,13 @@ Canonical wrap T x := @Wrap T x. Prenex Implicits unwrap wrap Wrap. -(** - Syntax for defining auxiliary recursive function. - Usage: - Section FooDefinition. - Variables (g1 : T1) (g2 : T2). (globals) - Fixoint foo_auxiliary (a3 : T3) ... := - body, using #[#rec e3, ... #]# for recursive calls - where " #[# 'rec' a3 , a4 , ... #]#" := foo_auxiliary. - Definition foo x y .. := #[#rec e1, ... #]#. - + proofs about foo - End FooDefinition. **) +Declare Scope fun_scope. +Delimit Scope fun_scope with FUN. +Open Scope fun_scope. -Reserved Notation "[ 'rec' a0 ]" - (at level 0, format "[ 'rec' a0 ]"). -Reserved Notation "[ 'rec' a0 , a1 ]" - (at level 0, format "[ 'rec' a0 , a1 ]"). -Reserved Notation "[ 'rec' a0 , a1 , a2 ]" - (at level 0, format "[ 'rec' a0 , a1 , a2 ]"). -Reserved Notation "[ 'rec' a0 , a1 , a2 , a3 ]" - (at level 0, format "[ 'rec' a0 , a1 , a2 , a3 ]"). -Reserved Notation "[ 'rec' a0 , a1 , a2 , a3 , a4 ]" - (at level 0, format "[ 'rec' a0 , a1 , a2 , a3 , a4 ]"). -Reserved Notation "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 ]" - (at level 0, format "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 ]"). -Reserved Notation "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 , a6 ]" - (at level 0, format "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 , a6 ]"). -Reserved Notation "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 , a6 , a7 ]" - (at level 0, - format "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 , a6 , a7 ]"). -Reserved Notation "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 , a6 , a7 , a8 ]" - (at level 0, - format "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 , a6 , a7 , a8 ]"). -Reserved Notation "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 , a6 , a7 , a8 , a9 ]" - (at level 0, - format "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 , a6 , a7 , a8 , a9 ]"). +(** Notations for argument transpose **) +Notation "f ^~ y" := (fun x => f x y) : fun_scope. +Notation "@^~ x" := (fun f => f x) : fun_scope. (** Definitions and notation for explicit functions with simplification, @@ -344,33 +404,19 @@ Coercion fun_of_simpl : simpl_fun >-> Funclass. End SimplFun. -Notation "[ 'fun' : T => E ]" := (SimplFun (fun _ : T => E)) - (at level 0, - format "'[hv' [ 'fun' : T => '/ ' E ] ']'") : fun_scope. - -Notation "[ 'fun' x => E ]" := (SimplFun (fun x => E)) - (at level 0, x ident, - format "'[hv' [ 'fun' x => '/ ' E ] ']'") : fun_scope. - +Notation "[ 'fun' : T => E ]" := (SimplFun (fun _ : T => E)) : fun_scope. +Notation "[ 'fun' x => E ]" := (SimplFun (fun x => E)) : fun_scope. +Notation "[ 'fun' x y => E ]" := (fun x => [fun y => E]) : fun_scope. Notation "[ 'fun' x : T => E ]" := (SimplFun (fun x : T => E)) - (at level 0, x ident, only parsing) : fun_scope. - -Notation "[ 'fun' x y => E ]" := (fun x => [fun y => E]) - (at level 0, x ident, y ident, - format "'[hv' [ 'fun' x y => '/ ' E ] ']'") : fun_scope. - + (only parsing) : fun_scope. Notation "[ 'fun' x y : T => E ]" := (fun x : T => [fun y : T => E]) - (at level 0, x ident, y ident, only parsing) : fun_scope. - + (only parsing) : fun_scope. Notation "[ 'fun' ( x : T ) y => E ]" := (fun x : T => [fun y => E]) - (at level 0, x ident, y ident, only parsing) : fun_scope. - + (only parsing) : fun_scope. Notation "[ 'fun' x ( y : T ) => E ]" := (fun x => [fun y : T => E]) - (at level 0, x ident, y ident, only parsing) : fun_scope. - -Notation "[ 'fun' ( x : xT ) ( y : yT ) => E ]" := - (fun x : xT => [fun y : yT => E]) - (at level 0, x ident, y ident, only parsing) : fun_scope. + (only parsing) : fun_scope. +Notation "[ 'fun' ( x : T ) ( y : U ) => E ]" := (fun x : T => [fun y : U => E]) + (only parsing) : fun_scope. (** For delta functions in eqtype.v. **) Definition SimplFunDelta aT rT (f : aT -> aT -> rT) := [fun z => f z z]. @@ -402,51 +448,38 @@ Typeclasses Opaque eqrel. Hint Resolve frefl rrefl : core. -Notation "f1 =1 f2" := (eqfun f1 f2) - (at level 70, no associativity) : fun_scope. -Notation "f1 =1 f2 :> A" := (f1 =1 (f2 : A)) - (at level 70, f2 at next level, A at level 90) : fun_scope. -Notation "f1 =2 f2" := (eqrel f1 f2) - (at level 70, no associativity) : fun_scope. -Notation "f1 =2 f2 :> A" := (f1 =2 (f2 : A)) - (at level 70, f2 at next level, A at level 90) : fun_scope. +Notation "f1 =1 f2" := (eqfun f1 f2) : fun_scope. +Notation "f1 =1 f2 :> A" := (f1 =1 (f2 : A)) : fun_scope. +Notation "f1 =2 f2" := (eqrel f1 f2) : fun_scope. +Notation "f1 =2 f2 :> A" := (f1 =2 (f2 : A)) : fun_scope. Section Composition. Variables A B C : Type. -Definition funcomp u (f : B -> A) (g : C -> B) x := let: tt := u in f (g x). -Definition catcomp u g f := funcomp u f g. -Local Notation comp := (funcomp tt). - +Definition comp (f : B -> A) (g : C -> B) x := f (g x). +Definition catcomp g f := comp f g. Definition pcomp (f : B -> option A) (g : C -> option B) x := obind f (g x). Lemma eq_comp f f' g g' : f =1 f' -> g =1 g' -> comp f g =1 comp f' g'. -Proof. by move=> eq_ff' eq_gg' x; rewrite /= eq_gg' eq_ff'. Qed. +Proof. by move=> eq_ff' eq_gg' x; rewrite /comp eq_gg' eq_ff'. Qed. End Composition. -Notation comp := (funcomp tt). -Notation "@ 'comp'" := (fun A B C => @funcomp A B C tt). -Notation "f1 \o f2" := (comp f1 f2) - (at level 50, format "f1 \o '/ ' f2") : fun_scope. -Notation "f1 \; f2" := (catcomp tt f1 f2) - (at level 60, right associativity, format "f1 \; '/ ' f2") : fun_scope. +Arguments comp {A B C} f g x /. +Arguments catcomp {A B C} g f x /. +Notation "f1 \o f2" := (comp f1 f2) : fun_scope. +Notation "f1 \; f2" := (catcomp f1 f2) : fun_scope. -Notation "[ 'eta' f ]" := (fun x => f x) - (at level 0, format "[ 'eta' f ]") : fun_scope. +Notation "[ 'eta' f ]" := (fun x => f x) : fun_scope. -Notation "'fun' => E" := (fun _ => E) (at level 200, only parsing) : fun_scope. +Notation "'fun' => E" := (fun _ => E) : fun_scope. Notation id := (fun x => x). -Notation "@ 'id' T" := (fun x : T => x) - (at level 10, T at level 8, only parsing) : fun_scope. +Notation "@ 'id' T" := (fun x : T => x) (only parsing) : fun_scope. -Definition id_head T u x : T := let: tt := u in x. -Definition explicit_id_key := tt. -Notation idfun := (id_head tt). -Notation "@ 'idfun' T " := (@id_head T explicit_id_key) - (at level 10, T at level 8, format "@ 'idfun' T") : fun_scope. +Definition idfun T x : T := x. +Arguments idfun {T} x /. Definition phant_id T1 T2 v1 v2 := phantom T1 v1 -> phantom T2 v2. @@ -542,74 +575,33 @@ Definition monomorphism_2 (aR rR : _ -> _ -> sT) := End Morphism. Notation "{ 'morph' f : x / a >-> r }" := - (morphism_1 f (fun x => a) (fun x => r)) - (at level 0, f at level 99, x ident, - format "{ 'morph' f : x / a >-> r }") : type_scope. - + (morphism_1 f (fun x => a) (fun x => r)) : type_scope. Notation "{ 'morph' f : x / a }" := - (morphism_1 f (fun x => a) (fun x => a)) - (at level 0, f at level 99, x ident, - format "{ 'morph' f : x / a }") : type_scope. - + (morphism_1 f (fun x => a) (fun x => a)) : type_scope. Notation "{ 'morph' f : x y / a >-> r }" := - (morphism_2 f (fun x y => a) (fun x y => r)) - (at level 0, f at level 99, x ident, y ident, - format "{ 'morph' f : x y / a >-> r }") : type_scope. - + (morphism_2 f (fun x y => a) (fun x y => r)) : type_scope. Notation "{ 'morph' f : x y / a }" := - (morphism_2 f (fun x y => a) (fun x y => a)) - (at level 0, f at level 99, x ident, y ident, - format "{ 'morph' f : x y / a }") : type_scope. - + (morphism_2 f (fun x y => a) (fun x y => a)) : type_scope. Notation "{ 'homo' f : x / a >-> r }" := - (homomorphism_1 f (fun x => a) (fun x => r)) - (at level 0, f at level 99, x ident, - format "{ 'homo' f : x / a >-> r }") : type_scope. - + (homomorphism_1 f (fun x => a) (fun x => r)) : type_scope. Notation "{ 'homo' f : x / a }" := - (homomorphism_1 f (fun x => a) (fun x => a)) - (at level 0, f at level 99, x ident, - format "{ 'homo' f : x / a }") : type_scope. - + (homomorphism_1 f (fun x => a) (fun x => a)) : type_scope. Notation "{ 'homo' f : x y / a >-> r }" := - (homomorphism_2 f (fun x y => a) (fun x y => r)) - (at level 0, f at level 99, x ident, y ident, - format "{ 'homo' f : x y / a >-> r }") : type_scope. - + (homomorphism_2 f (fun x y => a) (fun x y => r)) : type_scope. Notation "{ 'homo' f : x y / a }" := - (homomorphism_2 f (fun x y => a) (fun x y => a)) - (at level 0, f at level 99, x ident, y ident, - format "{ 'homo' f : x y / a }") : type_scope. - + (homomorphism_2 f (fun x y => a) (fun x y => a)) : type_scope. Notation "{ 'homo' f : x y /~ a }" := - (homomorphism_2 f (fun y x => a) (fun x y => a)) - (at level 0, f at level 99, x ident, y ident, - format "{ 'homo' f : x y /~ a }") : type_scope. - + (homomorphism_2 f (fun y x => a) (fun x y => a)) : type_scope. Notation "{ 'mono' f : x / a >-> r }" := - (monomorphism_1 f (fun x => a) (fun x => r)) - (at level 0, f at level 99, x ident, - format "{ 'mono' f : x / a >-> r }") : type_scope. - + (monomorphism_1 f (fun x => a) (fun x => r)) : type_scope. Notation "{ 'mono' f : x / a }" := - (monomorphism_1 f (fun x => a) (fun x => a)) - (at level 0, f at level 99, x ident, - format "{ 'mono' f : x / a }") : type_scope. - + (monomorphism_1 f (fun x => a) (fun x => a)) : type_scope. Notation "{ 'mono' f : x y / a >-> r }" := - (monomorphism_2 f (fun x y => a) (fun x y => r)) - (at level 0, f at level 99, x ident, y ident, - format "{ 'mono' f : x y / a >-> r }") : type_scope. - + (monomorphism_2 f (fun x y => a) (fun x y => r)) : type_scope. Notation "{ 'mono' f : x y / a }" := - (monomorphism_2 f (fun x y => a) (fun x y => a)) - (at level 0, f at level 99, x ident, y ident, - format "{ 'mono' f : x y / a }") : type_scope. - + (monomorphism_2 f (fun x y => a) (fun x y => a)) : type_scope. Notation "{ 'mono' f : x y /~ a }" := - (monomorphism_2 f (fun y x => a) (fun x y => a)) - (at level 0, f at level 99, x ident, y ident, - format "{ 'mono' f : x y /~ a }") : type_scope. + (monomorphism_2 f (fun y x => a) (fun x y => a)) : type_scope. (** In an intuitionistic setting, we have two degrees of injectivity. The @@ -620,9 +612,6 @@ Notation "{ 'mono' f : x y /~ a }" := Section Injections. -(** - rT must come first so we can use @ to mitigate the Coq 1st order - unification bug (e..g., Coq can't infer rT from a "cancel" lemma). **) Variables (rT aT : Type) (f : aT -> rT). Definition injective := forall x1 x2, f x1 = f x2 -> x1 = x2. @@ -650,10 +639,8 @@ Proof. by move=> fK <-. Qed. End Injections. -Lemma Some_inj {T} : injective (@Some T). Proof. by move=> x y []. Qed. - -(** Force implicits to use as a view. **) -Prenex Implicits Some_inj. +Lemma Some_inj {T : nonPropType} : injective (@Some T). +Proof. by move=> x y []. Qed. (** cancellation lemmas for dependent type casts. **) Lemma esymK T x y : cancel (@esym T x y) (@esym T y x). diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index 01d71aa96a..4d4400a0f8 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -56,7 +56,7 @@ let ssrsettac id ((_, (pat, pty)), (_, occ)) gl = | Cast(t, DEFAULTcast, ty) -> t, (gl, ty) | _ -> c, pfe_type_of gl c in let cl' = EConstr.mkLetIn (make_annot (Name id) Sorts.Relevant, c, cty, cl) in - Tacticals.tclTHEN (Proofview.V82.of_tactic (convert_concl cl')) (introid id) gl + Tacticals.tclTHEN (Proofview.V82.of_tactic (convert_concl ~check:true cl')) (introid id) gl open Util @@ -161,7 +161,7 @@ let havetac ist let gl, ty = pfe_type_of gl t in let ctx, _ = EConstr.decompose_prod_n_assum (project gl) 1 ty in let assert_is_conv gl = - try Proofview.V82.of_tactic (convert_concl (EConstr.it_mkProd_or_LetIn concl ctx)) gl + try Proofview.V82.of_tactic (convert_concl ~check:true (EConstr.it_mkProd_or_LetIn concl ctx)) gl with _ -> errorstrm (str "Given proof term is not of type " ++ pr_econstr_env (pf_env gl) (project gl) (EConstr.mkArrow (EConstr.mkVar (Id.of_string "_")) Sorts.Relevant concl)) in gl, ty, Tacticals.tclTHEN assert_is_conv (Proofview.V82.of_tactic (Tactics.apply t)), id, itac_c @@ -471,7 +471,7 @@ let undertac ?(pad_intro = false) ist ipats ((dir,_),_ as rule) hint = if hint = nohint then Proofview.tclUNIT () else - let betaiota = Tactics.reduct_in_concl (Reductionops.nf_betaiota, DEFAULTcast) in + let betaiota = Tactics.reduct_in_concl ~check:false (Reductionops.nf_betaiota, DEFAULTcast) in (* Usefulness of check_numgoals: tclDISPATCH would be enough, except for the error message w.r.t. the number of provided/expected tactics, as the last one is implied *) diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml index bbe7bde78b..91ff432364 100644 --- a/plugins/ssr/ssrtacticals.ml +++ b/plugins/ssr/ssrtacticals.ml @@ -110,7 +110,7 @@ let endclausestac id_map clseq gl_id cl0 gl = | _ -> EConstr.map (project gl) unmark c in let utac hyp = Proofview.V82.of_tactic - (Tactics.convert_hyp_no_check (NamedDecl.map_constr unmark hyp)) in + (Tactics.convert_hyp ~check:false ~reorder:false (NamedDecl.map_constr unmark hyp)) in let utacs = List.map utac (pf_hyps gl) in let ugtac gl' = Proofview.V82.of_tactic diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml index 075ebf006a..0a5c85f4ab 100644 --- a/plugins/ssr/ssrview.ml +++ b/plugins/ssr/ssrview.ml @@ -290,7 +290,7 @@ let finalize_view s0 ?(simple_types=true) p = Goal.enter_one ~__LOC__ begin fun g -> let env = Goal.env g in let sigma = Goal.sigma g in - let evars_of_p = Evd.evars_of_term (EConstr.to_constr ~abort_on_undefined_evars:false sigma p) in + let evars_of_p = Evd.evars_of_term sigma p in let filter x _ = Evar.Set.mem x evars_of_p in let sigma = Typeclasses.resolve_typeclasses ~fail:false ~filter env sigma in let p = Reductionops.nf_evar sigma p in @@ -307,7 +307,7 @@ Goal.enter_one ~__LOC__ begin fun g -> let und0 = (* Unassigned evars in the initial goal *) let sigma0 = Tacmach.project s0 in let g0info = Evd.find sigma0 (Tacmach.sig_it s0) in - let g0 = Evd.evars_of_filtered_evar_info g0info in + let g0 = Evd.evars_of_filtered_evar_info sigma0 g0info in List.filter (fun k -> Evar.Set.mem k g0) (List.map fst (Evar.Map.bindings (Evd.undefined_map sigma0))) in let rigid = rigid_of und0 in diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index 1deb935d5c..adbcfb8f3b 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -529,8 +529,8 @@ exception FoundUnif of (evar_map * UState.t * tpattern) (* Note: we don't update env as we descend into the term, as the primitive *) (* unification procedure always rejects subterms with bound variables. *) -let dont_impact_evars_in cl = - let evs_in_cl = Evd.evars_of_term cl in +let dont_impact_evars_in sigma0 cl = + let evs_in_cl = Evd.evars_of_term sigma0 cl in fun sigma -> Evar.Set.for_all (fun k -> try let _ = Evd.find_undefined sigma k in true with Not_found -> false) evs_in_cl @@ -544,7 +544,7 @@ let dont_impact_evars_in cl = (* - w_unify expands let-in (zeta conversion) eagerly, whereas we want to *) (* match a head let rigidly. *) let match_upats_FO upats env sigma0 ise orig_c = - let dont_impact_evars = dont_impact_evars_in orig_c in + let dont_impact_evars = dont_impact_evars_in sigma0 (EConstr.of_constr orig_c) in let rec loop c = let f, a = splay_app ise c in let i0 = ref (-1) in let fpats = @@ -586,7 +586,7 @@ let match_upats_FO upats env sigma0 ise orig_c = let match_upats_HO ~on_instance upats env sigma0 ise c = - let dont_impact_evars = dont_impact_evars_in c in + let dont_impact_evars = dont_impact_evars_in sigma0 (EConstr.of_constr c) in let it_did_match = ref false in let failed_because_of_TC = ref false in let rec aux upats env sigma0 ise c = @@ -1299,7 +1299,7 @@ let ssrpatterntac _ist arg gl = let concl_x = EConstr.of_constr concl_x in let gl, tty = pf_type_of gl t in let concl = EConstr.mkLetIn (make_annot (Name (Id.of_string "selected")) Sorts.Relevant, t, tty, concl_x) in - Proofview.V82.of_tactic (convert_concl concl DEFAULTcast) gl + Proofview.V82.of_tactic (convert_concl ~check:true concl DEFAULTcast) gl (* Register "ssrpattern" tactic *) let () = diff --git a/plugins/syntax/g_numeral.mlg b/plugins/syntax/g_numeral.mlg index baa4ae0306..0f0f3953da 100644 --- a/plugins/syntax/g_numeral.mlg +++ b/plugins/syntax/g_numeral.mlg @@ -16,18 +16,17 @@ open Notation open Numeral open Pp open Names -open Ltac_plugin open Stdarg open Pcoq.Prim -let pr_numnot_option _ _ _ = function +let pr_numnot_option = function | Nop -> mt () | Warning n -> str "(warning after " ++ str n ++ str ")" | Abstract n -> str "(abstract after " ++ str n ++ str ")" } -ARGUMENT EXTEND numnotoption +VERNAC ARGUMENT EXTEND numnotoption PRINTED BY { pr_numnot_option } | [ ] -> { Nop } | [ "(" "warning" "after" bigint(waft) ")" ] -> { Warning waft } diff --git a/plugins/syntax/plugin_base.dune b/plugins/syntax/plugin_base.dune index aac46338ea..7a23581768 100644 --- a/plugins/syntax/plugin_base.dune +++ b/plugins/syntax/plugin_base.dune @@ -3,7 +3,7 @@ (public_name coq.plugins.numeral_notation) (synopsis "Coq numeral notation plugin") (modules g_numeral numeral) - (libraries coq.plugins.ltac)) + (libraries coq.vernac)) (library (name string_notation_plugin) |