diff options
Diffstat (limited to 'plugins/ssr')
| -rw-r--r-- | plugins/ssr/ssrbool.v | 8 | ||||
| -rw-r--r-- | plugins/ssr/ssrclasses.v | 32 | ||||
| -rw-r--r-- | plugins/ssr/ssrcommon.ml | 91 | ||||
| -rw-r--r-- | plugins/ssr/ssrcommon.mli | 13 | ||||
| -rw-r--r-- | plugins/ssr/ssreflect.v | 113 | ||||
| -rw-r--r-- | plugins/ssr/ssreflect_plugin.mlpack | 1 | ||||
| -rw-r--r-- | plugins/ssr/ssrelim.ml | 48 | ||||
| -rw-r--r-- | plugins/ssr/ssrequality.ml | 98 | ||||
| -rw-r--r-- | plugins/ssr/ssrequality.mli | 3 | ||||
| -rw-r--r-- | plugins/ssr/ssrfun.v | 25 | ||||
| -rw-r--r-- | plugins/ssr/ssrfwd.ml | 54 | ||||
| -rw-r--r-- | plugins/ssr/ssrparser.mlg | 116 | ||||
| -rw-r--r-- | plugins/ssr/ssrprinters.mli | 2 | ||||
| -rw-r--r-- | plugins/ssr/ssrsetoid.v | 122 | ||||
| -rw-r--r-- | plugins/ssr/ssrtacticals.ml | 2 | ||||
| -rw-r--r-- | plugins/ssr/ssrunder.v | 75 | ||||
| -rw-r--r-- | plugins/ssr/ssrvernac.mlg | 19 |
17 files changed, 498 insertions, 324 deletions
diff --git a/plugins/ssr/ssrbool.v b/plugins/ssr/ssrbool.v index bf0761d3ae..376410658a 100644 --- a/plugins/ssr/ssrbool.v +++ b/plugins/ssr/ssrbool.v @@ -1323,7 +1323,6 @@ Proof. by move=> x y r2xy; apply/orP; right. Qed. (** Variant of simpl_pred specialised to the membership operator. **) -#[universes(template)] Variant mem_pred T := Mem of pred T. (** @@ -1464,7 +1463,6 @@ Implicit Types (mp : mem_pred T). Definition Acoll : collective_pred T := [pred x | ...]. as the collective_pred_of_simpl is _not_ convertible to pred_of_simpl. **) -#[universes(template)] Structure registered_applicative_pred p := RegisteredApplicativePred { applicative_pred_value :> pred T; _ : applicative_pred_value = p @@ -1473,21 +1471,18 @@ 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 { 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 { mem_pred_value :> mem_pred T; _ : mem_pred_value = Mem [eta p] }. 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 : registered_applicative_pred p) := @@ -1538,7 +1533,6 @@ End PredicateSimplification. (** Qualifiers and keyed predicates. **) -#[universes(template)] Variant qualifier (q : nat) T := Qualifier of {pred T}. Coercion has_quality n T (q : qualifier n T) : {pred T} := @@ -1573,7 +1567,6 @@ Variable T : Type. Variant pred_key (p : {pred T}) := DefaultPredKey. Variable p : {pred T}. -#[universes(template)] Structure keyed_pred (k : pred_key p) := PackKeyedPred {unkey_pred :> {pred T}; _ : unkey_pred =i p}. @@ -1605,7 +1598,6 @@ Section KeyedQualifier. Variables (T : Type) (n : nat) (q : qualifier n T). -#[universes(template)] Structure keyed_qualifier (k : pred_key q) := PackKeyedQualifier {unkey_qualifier; _ : unkey_qualifier = q}. Definition KeyedQualifier k := PackKeyedQualifier k (erefl q). diff --git a/plugins/ssr/ssrclasses.v b/plugins/ssr/ssrclasses.v new file mode 100644 index 0000000000..0ae3f8c6a5 --- /dev/null +++ b/plugins/ssr/ssrclasses.v @@ -0,0 +1,32 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** #<style> .doc { font-family: monospace; white-space: pre; } </style># **) + +(** Compatibility layer for [under] and [setoid_rewrite]. + + Note: this file does not require [ssreflect]; it is both required by + [ssrsetoid] and required by [ssrunder]. + + Redefine [Coq.Classes.RelationClasses.Reflexive] here, so that doing + [Require Import ssreflect] does not [Require Import RelationClasses], + and conversely. **) + +Section Defs. + Context {A : Type}. + Class Reflexive (R : A -> A -> Prop) := + reflexivity : forall x : A, R x x. +End Defs. + +Register Reflexive as plugins.ssreflect.reflexive_type. +Register reflexivity as plugins.ssreflect.reflexive_proof. + +Instance eq_Reflexive {A : Type} : Reflexive (@eq A) := @eq_refl A. +Instance iff_Reflexive : Reflexive iff := iff_refl. diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 33e9f871fd..de3c660938 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -181,7 +181,6 @@ let option_assert_get o msg = (** Constructors for rawconstr *) open Glob_term -open Decl_kinds let mkRHole = DAst.make @@ GHole (Evar_kinds.InternalHole, Namegen.IntroAnonymous, None) @@ -271,7 +270,7 @@ let of_ftactic ftac gl = in (sigma, ans) -let interp_wit wit ist gl x = +let interp_wit wit ist gl x = let globarg = in_gen (glbwit wit) x in let arg = Tacinterp.interp_genarg ist globarg in let (sigma, arg) = of_ftactic arg gl in @@ -351,7 +350,7 @@ let same_prefix s t n = let rec loop i = i = n || s.[i] = t.[i] && loop (i + 1) in loop 0 let skip_digits s = - let n = String.length s in + let n = String.length s in let rec loop i = if i < n && is_digit s.[i] then loop (i + 1) else i in loop let mk_tagged_id t i = Id.of_string (Printf.sprintf "%s%d_" t i) @@ -369,7 +368,7 @@ let wildcard_tag = "_the_" let wildcard_post = "_wildcard_" let mk_wildcard_id i = Id.of_string (Printf.sprintf "%s%s%s" wildcard_tag (CString.ordinal i) wildcard_post) -let has_wildcard_tag s = +let has_wildcard_tag s = let n = String.length s in let m = String.length wildcard_tag in let m' = String.length wildcard_post in n < m + m' + 2 && same_prefix s wildcard_tag m && @@ -441,7 +440,7 @@ let inc_safe n = if n = 0 then n else n + 1 let rec safe_depth s c = match EConstr.kind s c with | LetIn ({binder_name=Name x}, _, _, c') when is_discharged_id x -> safe_depth s c' + 1 | LetIn (_, _, _, c') | Prod (_, _, c') -> inc_safe (safe_depth s c') -| _ -> 0 +| _ -> 0 let red_safe (r : Reductionops.reduction_function) e s c0 = let rec red_to e c n = match EConstr.kind s c with @@ -519,7 +518,7 @@ let resolve_typeclasses ~where ~fail env sigma = sigma -let nf_evar sigma t = +let nf_evar sigma t = EConstr.Unsafe.to_constr (Evarutil.nf_evar sigma (EConstr.of_constr t)) let pf_abs_evars2 gl rigid (sigma, c0) = @@ -536,7 +535,7 @@ let pf_abs_evars2 gl rigid (sigma, c0) = let t = Context.Named.fold_inside abs_dc ~init:concl dc in nf_evar sigma t in let rec put evlist c = match Constr.kind c with - | Evar (k, a) -> + | Evar (k, a) -> if List.mem_assoc k evlist || Evd.mem sigma0 k || List.mem k rigid then evlist else let n = max 0 (Array.length a - nenv) in let t = abs_evar n k in (k, (n, t)) :: put evlist t @@ -562,11 +561,11 @@ let pf_abs_evars gl t = pf_abs_evars2 gl [] t (* As before but if (?i : T(?j)) and (?j : P : Prop), then the lambda for i - * looks like (fun evar_i : (forall pi : P. T(pi))) thanks to "loopP" and all + * looks like (fun evar_i : (forall pi : P. T(pi))) thanks to "loopP" and all * occurrences of evar_i are replaced by (evar_i evar_j) thanks to "app". * * If P can be solved by ssrautoprop (that defaults to trivial), then - * the corresponding lambda looks like (fun evar_i : T(c)) where c is + * the corresponding lambda looks like (fun evar_i : T(c)) where c is * the solution found by ssrautoprop. *) let ssrautoprop_tac = ref (fun gl -> assert false) @@ -597,11 +596,11 @@ let pf_abs_evars_pirrel gl (sigma, c0) = let t = Context.Named.fold_inside abs_dc ~init:concl dc in nf_evar sigma0 (nf_evar sigma t) in let rec put evlist c = match Constr.kind c with - | Evar (k, a) -> + | Evar (k, a) -> if List.mem_assoc k evlist || Evd.mem sigma0 k then evlist else let n = max 0 (Array.length a - nenv) in - let k_ty = - Retyping.get_sort_family_of + let k_ty = + Retyping.get_sort_family_of (pf_env gl) sigma (Evd.evar_concl (Evd.find sigma k)) in let is_prop = k_ty = InProp in let t = abs_evar n k in (k, (n, t, is_prop)) :: put evlist t @@ -611,23 +610,23 @@ let pf_abs_evars_pirrel gl (sigma, c0) = let pr_constr t = Printer.pr_econstr_env (pf_env gl) sigma (Reductionops.nf_beta (pf_env gl) (project gl) (EConstr.of_constr t)) in pp(lazy(str"evlist=" ++ pr_list (fun () -> str";") (fun (k,_) -> Evar.print k) evlist)); - let evplist = - let depev = List.fold_left (fun evs (_,(_,t,_)) -> + let evplist = + let depev = List.fold_left (fun evs (_,(_,t,_)) -> let t = EConstr.of_constr t in Intset.union evs (Evarutil.undefined_evars_of_term sigma t)) Intset.empty evlist in List.filter (fun (i,(_,_,b)) -> b && Intset.mem i depev) evlist in - let evlist, evplist, sigma = + let evlist, evplist, sigma = if evplist = [] then evlist, [], sigma else List.fold_left (fun (ev, evp, sigma) (i, (_,t,_) as p) -> - try + try let ng, sigma = call_on_evar !ssrautoprop_tac i sigma in if (ng <> []) then errorstrm (str "Should we tell the user?"); List.filter (fun (j,_) -> j <> i) ev, evp, sigma with _ -> ev, p::evp, sigma) (evlist, [], sigma) (List.rev evplist) in let c0 = nf_evar sigma c0 in - let evlist = + let evlist = List.map (fun (x,(y,t,z)) -> x,(y,nf_evar sigma t,z)) evlist in - let evplist = + let evplist = List.map (fun (x,(y,t,z)) -> x,(y,nf_evar sigma t,z)) evplist in pp(lazy(str"c0= " ++ pr_constr c0)); let rec lookup k i = function @@ -647,7 +646,7 @@ let pf_abs_evars_pirrel gl (sigma, c0) = let rec loopP evlist c i = function | (_, (n, t, _)) :: evl -> let t = get evlist (i - 1) t in - let n = Name (Id.of_string (ssr_anon_hyp ^ string_of_int n)) in + let n = Name (Id.of_string (ssr_anon_hyp ^ string_of_int n)) in loopP evlist (mkProd (make_annot n Sorts.Relevant, t, c)) (i - 1) evl | [] -> c in let rec loop c i = function @@ -656,8 +655,8 @@ let pf_abs_evars_pirrel gl (sigma, c0) = let t_evplist = List.filter (fun (k,_) -> Intset.mem k evs) evplist in let t = loopP t_evplist (get t_evplist 1 t) 1 t_evplist in let t = get evlist (i - 1) t in - let extra_args = - List.map (fun (k,_) -> mkRel (fst (lookup k i evlist))) + let extra_args = + List.map (fun (k,_) -> mkRel (fst (lookup k i evlist))) (List.rev t_evplist) in let c = if extra_args = [] then c else app extra_args 1 c in loop (mkLambda (make_annot (mk_evar_name n) Sorts.Relevant, t, c)) (i - 1) evl @@ -681,6 +680,10 @@ let pf_type_id gl t = Id.of_string (Namegen.hdchar (pf_env gl) (project gl) t) let pfe_type_of gl t = let sigma, ty = pf_type_of gl t in re_sig (sig_it gl) sigma, ty +let pfe_new_type gl = + let sigma, env, it = project gl, pf_env gl, sig_it gl in + let sigma,t = Evarutil.new_Type sigma in + re_sig it sigma, t let pfe_type_relevance_of gl t = let gl, ty = pfe_type_of gl t in gl, ty, pf_apply Retyping.relevance_of_term gl t @@ -752,7 +755,7 @@ let pf_abs_prod name gl c cl = pf_mkprod gl c ~name (Termops.subst_term (project (** look up a name in the ssreflect internals module *) let ssrdirpath = DirPath.make [Id.of_string "ssreflect"] -let ssrqid name = Libnames.make_qualid ssrdirpath (Id.of_string name) +let ssrqid name = Libnames.make_qualid ssrdirpath (Id.of_string name) let mkSsrRef name = let qn = Format.sprintf "plugins.ssreflect.%s" name in if Coqlib.has_ref qn then Coqlib.lib_ref qn else @@ -855,7 +858,7 @@ let top_id = mk_internal_id "top assumption" let ssr_n_tac seed n gl = let name = if n = -1 then seed else ("ssr" ^ seed ^ string_of_int n) in let fail msg = CErrors.user_err (Pp.str msg) in - let tacname = + let tacname = try Tacenv.locate_tactic (Libnames.qualid_of_ident (Id.of_string name)) with Not_found -> try Tacenv.locate_tactic (ssrqid name) with Not_found -> @@ -924,13 +927,13 @@ let pf_interp_ty ?(resolve_typeclasses=false) ist gl ty = (* TASSI: given (c : ty), generates (c ??? : ty[???/...]) with m evars *) exception NotEnoughProducts -let saturate ?(beta=false) ?(bi_types=false) env sigma c ?(ty=Retyping.get_type_of env sigma c) m +let saturate ?(beta=false) ?(bi_types=false) env sigma c ?(ty=Retyping.get_type_of env sigma c) m = - let rec loop ty args sigma n = - if n = 0 then + let rec loop ty args sigma n = + if n = 0 then let args = List.rev args in (if beta then Reductionops.whd_beta sigma else fun x -> x) - (EConstr.mkApp (c, Array.of_list (List.map snd args))), ty, args, sigma + (EConstr.mkApp (c, Array.of_list (List.map snd args))), ty, args, sigma else match EConstr.kind_of_type sigma ty with | ProdType (_, src, tgt) -> let sigma = create_evar_defs sigma in @@ -938,7 +941,7 @@ let saturate ?(beta=false) ?(bi_types=false) env sigma c ?(ty=Retyping.get_type_ Evarutil.new_evar env sigma (if bi_types then Reductionops.nf_betaiota env sigma src else src) in loop (EConstr.Vars.subst1 x tgt) ((m - n,x) :: args) sigma (n-1) - | CastType (t, _) -> loop t args sigma n + | CastType (t, _) -> loop t args sigma n | LetInType (_, v, _, t) -> loop (EConstr.Vars.subst1 v t) args sigma n | SortType _ -> assert false | AtomicType _ -> @@ -950,10 +953,10 @@ let saturate ?(beta=false) ?(bi_types=false) env sigma c ?(ty=Retyping.get_type_ in loop ty [] sigma m -let pf_saturate ?beta ?bi_types gl c ?ty m = +let pf_saturate ?beta ?bi_types gl c ?ty m = let env, sigma, si = pf_env gl, project gl, sig_it gl in let t, ty, args, sigma = saturate ?beta ?bi_types env sigma c ?ty m in - t, ty, args, re_sig si sigma + t, ty, args, re_sig si sigma let pf_partial_solution gl t evl = let sigma, g = project gl, sig_it gl in @@ -970,7 +973,7 @@ let dependent_apply_error = * is just like apply, but with a user-provided number n of implicits. * * Refine.refine function that handles type classes and evars but fails to - * handle "dependently typed higher order evars". + * handle "dependently typed higher order evars". * * Refiner.refiner that does not handle metas with a non ground type but works * with dependently typed higher order metas. *) @@ -995,7 +998,7 @@ let applyn ~with_evars ?beta ?(with_shelve=false) ?(first_goes_last=false) n t g let t, gl = if n = 0 then t, gl else let sigma, si = project gl, sig_it gl in let rec loop sigma bo args = function (* saturate with metas *) - | 0 -> EConstr.mkApp (t, Array.of_list (List.rev args)), re_sig si sigma + | 0 -> EConstr.mkApp (t, Array.of_list (List.rev args)), re_sig si sigma | n -> match EConstr.kind sigma bo with | Lambda (_, ty, bo) -> if not (EConstr.Vars.closed0 sigma ty) then @@ -1038,7 +1041,7 @@ let introid ?(orig=ref Anonymous) name = tclTHEN (fun gl -> let g, env = Tacmach.pf_concl gl, pf_env gl in let sigma = project gl in match EConstr.kind sigma g with - | App (hd, _) when EConstr.isLambda sigma hd -> + | App (hd, _) when EConstr.isLambda sigma hd -> Proofview.V82.of_tactic (convert_concl_no_check (Reductionops.whd_beta sigma g)) gl | _ -> tclIDTAC gl) (Proofview.V82.of_tactic @@ -1063,9 +1066,9 @@ let is_pf_var sigma c = let hyp_of_var sigma v = SsrHyp (Loc.tag @@ EConstr.destVar sigma v) let interp_clr sigma = function -| Some clr, (k, c) +| Some clr, (k, c) when (k = xNoFlag || k = xWithAt) && is_pf_var sigma c -> - hyp_of_var sigma c :: clr + hyp_of_var sigma c :: clr | Some clr, _ -> clr | None, _ -> [] @@ -1088,7 +1091,7 @@ let tclDO n tac = let prefix i = str"At iteration " ++ int i ++ str": " in let tac_err_at i gl = try tac gl - with + with | CErrors.UserError (l, s) as e -> let _, info = CErrors.push e in let e' = CErrors.UserError (l, prefix i ++ s) in @@ -1120,7 +1123,7 @@ let pf_interp_gen_aux gl to_ind ((oclr, occ), t) = let pat = interp_cpattern gl t None in (* UGLY API *) let gl = pf_merge_uc_of (fst pat) gl in let cl, env, sigma = Tacmach.pf_concl gl, pf_env gl, project gl in - let (c, ucst), cl = + let (c, ucst), cl = try fill_occ_pattern ~raise_NoMatch:true env sigma (EConstr.Unsafe.to_constr cl) pat occ 1 with NoMatch -> redex_of_pattern env pat, (EConstr.Unsafe.to_constr cl) in let gl = pf_merge_uc ucst gl in @@ -1128,9 +1131,9 @@ let pf_interp_gen_aux gl to_ind ((oclr, occ), t) = let cl = EConstr.of_constr cl in let clr = interp_clr sigma (oclr, (tag_of_cpattern t, c)) in if not(occur_existential sigma c) then - if tag_of_cpattern t = xWithAt then + if tag_of_cpattern t = xWithAt then if not (EConstr.isVar sigma c) then - errorstrm (str "@ can be used with variables only") + errorstrm (str "@ can be used with variables only") else match Tacmach.pf_get_hyp gl (EConstr.destVar sigma c) with | NamedDecl.LocalAssum _ -> errorstrm (str "@ can be used with let-ins only") | NamedDecl.LocalDef (name, b, ty) -> true, pat, EConstr.mkLetIn (map_annot Name.mk_name name,b,ty,cl),c,clr,ucst,gl @@ -1183,7 +1186,7 @@ let gen_tmp_ids push_ctxs ctx (tclTHENLIST (List.map (fun (id,orig_ref) -> - tclTHEN + tclTHEN (gentac ((None,Some(false,[])),cpattern_of_id id)) (rename_hd_prod orig_ref)) ctx.tmp_ids) gl) @@ -1207,7 +1210,7 @@ let pfLIFT f = Proofview.tclUNIT x ;; -(* TASSI: This version of unprotects inlines the unfold tactic definition, +(* TASSI: This version of unprotects inlines the unfold tactic definition, * since we don't want to wipe out let-ins, and it seems there is no flag * to change that behaviour in the standard unfold code *) let unprotecttac gl = @@ -1216,8 +1219,8 @@ let unprotecttac gl = Tacticals.onClause (fun idopt -> let hyploc = Option.map (fun id -> id, InHyp) idopt in Proofview.V82.of_tactic (Tactics.reduct_option ~check:false - (Reductionops.clos_norm_flags - (CClosure.RedFlags.mkflags + (Reductionops.clos_norm_flags + (CClosure.RedFlags.mkflags [CClosure.RedFlags.fBETA; CClosure.RedFlags.fCONST prot; CClosure.RedFlags.fMATCH; @@ -1250,7 +1253,7 @@ let abs_wgen keep_let f gen (gl,args,c) = let x' = make_annot (Name (f x)) (NamedDecl.get_relevance hyp) in let prod = EConstr.mkProd (x', NamedDecl.get_type hyp, EConstr.Vars.subst_var x c) in gl, EConstr.mkVar x :: args, prod - | _, Some ((x, "@"), Some p) -> + | _, Some ((x, "@"), Some p) -> let x = hoi_id x in let cp = interp_cpattern gl p None in let gl = pf_merge_uc_of (fst cp) gl in diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli index e920bc318a..741db9a6c2 100644 --- a/plugins/ssr/ssrcommon.mli +++ b/plugins/ssr/ssrcommon.mli @@ -38,7 +38,7 @@ val hoi_id : ssrhyp_or_id -> Id.t (******************************* hints ***********************************) -val mk_hint : 'a -> 'a ssrhint +val mk_hint : 'a -> 'a ssrhint val mk_orhint : 'a -> bool * 'a val nullhint : bool * 'a list val nohint : 'a ssrhint @@ -122,7 +122,7 @@ val mkCLambda : ?loc:Loc.t -> Name.t -> constr_expr -> constr_expr -> constr_e val isCHoles : constr_expr list -> bool val isCxHoles : (constr_expr * 'a option) list -> bool -val intern_term : +val intern_term : Tacinterp.interp_sign -> env -> ssrterm -> Glob_term.glob_constr @@ -152,7 +152,7 @@ val pf_e_type_of : Goal.goal Evd.sigma -> EConstr.constr -> Goal.goal Evd.sigma * EConstr.types -val splay_open_constr : +val splay_open_constr : Goal.goal Evd.sigma -> evar_map * EConstr.t -> (Names.Name.t Context.binder_annot * EConstr.t) list * EConstr.t @@ -181,7 +181,7 @@ val mk_evar_name : int -> Name.t val ssr_anon_hyp : string val pf_type_id : Goal.goal Evd.sigma -> EConstr.types -> Id.t -val pf_abs_evars : +val pf_abs_evars : Goal.goal Evd.sigma -> evar_map * EConstr.t -> int * EConstr.t * Evar.t list * @@ -205,6 +205,7 @@ val pf_type_of : val pfe_type_of : Goal.goal Evd.sigma -> EConstr.t -> Goal.goal Evd.sigma * EConstr.types +val pfe_new_type : Goal.goal Evd.sigma -> Goal.goal Evd.sigma * EConstr.types val pfe_type_relevance_of : Goal.goal Evd.sigma -> EConstr.t -> Goal.goal Evd.sigma * EConstr.types * Sorts.relevance @@ -234,7 +235,7 @@ val is_discharged_id : Id.t -> bool val mk_discharged_id : Id.t -> Id.t val is_tagged : string -> string -> bool val has_discharged_tag : string -> bool -val ssrqid : string -> Libnames.qualid +val ssrqid : string -> Libnames.qualid val new_tmp_id : tac_ctx -> (Names.Id.t * Name.t ref) * tac_ctx val mk_anon_id : string -> Id.t list -> Id.t @@ -243,7 +244,7 @@ val pf_abs_evars_pirrel : evar_map * Constr.constr -> int * Constr.constr val nbargs_open_constr : Goal.goal Evd.sigma -> Evd.evar_map * EConstr.t -> int val pf_nbargs : Goal.goal Evd.sigma -> EConstr.t -> int -val gen_tmp_ids : +val gen_tmp_ids : ?ist:Geninterp.interp_sign -> (Goal.goal * tac_ctx) Evd.sigma -> (Goal.goal * tac_ctx) list Evd.sigma diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v index 71abafc22f..bc4a57dedd 100644 --- a/plugins/ssr/ssreflect.v +++ b/plugins/ssr/ssreflect.v @@ -209,7 +209,6 @@ Register abstract_key as plugins.ssreflect.abstract_key. Register abstract as plugins.ssreflect.abstract. (** Constants for tactic-views **) -#[universes(template)] Inductive external_view : Type := tactic_view of Type. (** @@ -531,102 +530,32 @@ Lemma abstract_context T (P : T -> Type) x : Proof. by move=> /(_ P); apply. Qed. (*****************************************************************************) -(* Constants for under, to rewrite under binders using "Leibniz eta lemmas". *) - -Module Type UNDER_EQ. -Parameter Under_eq : - forall (R : Type), R -> R -> Prop. -Parameter Under_eq_from_eq : - forall (T : Type) (x y : T), @Under_eq T x y -> x = y. - -(** [Over_eq, over_eq, over_eq_done]: for "by rewrite over_eq" *) -Parameter Over_eq : - forall (R : Type), R -> R -> Prop. -Parameter over_eq : - forall (T : Type) (x : T) (y : T), @Under_eq T x y = @Over_eq T x y. -Parameter over_eq_done : - forall (T : Type) (x : T), @Over_eq T x x. -(* We need both hints below, otherwise the test-suite does not pass *) -Hint Extern 0 (@Over_eq _ _ _) => solve [ apply over_eq_done ] : core. -(* => for [test-suite/ssr/under.v:test_big_patt1] *) -Hint Resolve over_eq_done : core. -(* => for [test-suite/ssr/over.v:test_over_1_1] *) - -(** [under_eq_done]: for Ltac-style over *) -Parameter under_eq_done : - forall (T : Type) (x : T), @Under_eq T x x. -Notation "''Under[' x ]" := (@Under_eq _ x _) - (at level 8, format "''Under[' x ]", only printing). -End UNDER_EQ. - -Module Export Under_eq : UNDER_EQ. -Definition Under_eq := @eq. -Lemma Under_eq_from_eq (T : Type) (x y : T) : - @Under_eq T x y -> x = y. -Proof. by []. Qed. -Definition Over_eq := Under_eq. -Lemma over_eq : - forall (T : Type) (x : T) (y : T), @Under_eq T x y = @Over_eq T x y. -Proof. by []. Qed. -Lemma over_eq_done : - forall (T : Type) (x : T), @Over_eq T x x. -Proof. by []. Qed. -Lemma under_eq_done : - forall (T : Type) (x : T), @Under_eq T x x. -Proof. by []. Qed. -End Under_eq. - -Register Under_eq as plugins.ssreflect.Under_eq. -Register Under_eq_from_eq as plugins.ssreflect.Under_eq_from_eq. - -Module Type UNDER_IFF. -Parameter Under_iff : Prop -> Prop -> Prop. -Parameter Under_iff_from_iff : forall x y : Prop, @Under_iff x y -> x <-> y. - -(** [Over_iff, over_iff, over_iff_done]: for "by rewrite over_iff" *) -Parameter Over_iff : Prop -> Prop -> Prop. -Parameter over_iff : - forall (x : Prop) (y : Prop), @Under_iff x y = @Over_iff x y. -Parameter over_iff_done : - forall (x : Prop), @Over_iff x x. -Hint Extern 0 (@Over_iff _ _) => solve [ apply over_iff_done ] : core. -Hint Resolve over_iff_done : core. - -(** [under_iff_done]: for Ltac-style over *) -Parameter under_iff_done : - forall (x : Prop), @Under_iff x x. -Notation "''Under[' x ]" := (@Under_iff x _) - (at level 8, format "''Under[' x ]", only printing). -End UNDER_IFF. - -Module Export Under_iff : UNDER_IFF. -Definition Under_iff := iff. -Lemma Under_iff_from_iff (x y : Prop) : - @Under_iff x y -> x <-> y. -Proof. by []. Qed. -Definition Over_iff := Under_iff. -Lemma over_iff : - forall (x : Prop) (y : Prop), @Under_iff x y = @Over_iff x y. -Proof. by []. Qed. -Lemma over_iff_done : - forall (x : Prop), @Over_iff x x. -Proof. by []. Qed. -Lemma under_iff_done : - forall (x : Prop), @Under_iff x x. -Proof. by []. Qed. -End Under_iff. - -Register Under_iff as plugins.ssreflect.Under_iff. -Register Under_iff_from_iff as plugins.ssreflect.Under_iff_from_iff. - -Definition over := (over_eq, over_iff). +(* Material for under/over (to rewrite under binders using "context lemmas") *) + +Require Export ssrunder. + +Hint Extern 0 (@Under_rel.Over_rel _ _ _ _) => + solve [ apply: Under_rel.over_rel_done ] : core. +Hint Resolve Under_rel.over_rel_done : core. + +Register Under_rel.Under_rel as plugins.ssreflect.Under_rel. +Register Under_rel.Under_rel_from_rel as plugins.ssreflect.Under_rel_from_rel. +(** Closing rewrite rule *) +Definition over := over_rel. + +(** Closing tactic *) Ltac over := - by [ apply: Under_eq.under_eq_done - | apply: Under_iff.under_iff_done + by [ apply: Under_rel.under_rel_done | rewrite over ]. +(** Convenience rewrite rule to unprotect evars, e.g., to instantiate + them in another way than with reflexivity. *) +Definition UnderE := Under_relE. + +(*****************************************************************************) + (** 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. diff --git a/plugins/ssr/ssreflect_plugin.mlpack b/plugins/ssr/ssreflect_plugin.mlpack index 824348fee7..46669998b9 100644 --- a/plugins/ssr/ssreflect_plugin.mlpack +++ b/plugins/ssr/ssreflect_plugin.mlpack @@ -10,4 +10,3 @@ Ssripats Ssrfwd Ssrparser Ssrvernac - diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index d0426c86b9..26962ee87b 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -36,7 +36,7 @@ module RelDecl = Context.Rel.Declaration * checks if the eliminator is recursive or not *) let analyze_eliminator elimty env sigma = let rec loop ctx t = match EConstr.kind_of_type sigma t with - | AtomicType (hd, args) when EConstr.isRel sigma hd -> + | AtomicType (hd, args) when EConstr.isRel sigma hd -> ctx, EConstr.destRel sigma hd, not (EConstr.Vars.noccurn sigma 1 t), Array.length args, t | CastType (t, _) -> loop ctx t | ProdType (x, ty, t) -> loop (RelDecl.LocalAssum (x, ty) :: ctx) t @@ -50,7 +50,7 @@ let analyze_eliminator elimty env sigma = str"the eliminator's"++Pp.cut()++str"type:"++spc()++pr_econstr_env env' sigma elimty) in let ctx, pred_id, elim_is_dep, n_pred_args,concl = loop [] elimty in let n_elim_args = Context.Rel.nhyps ctx in - let is_rec_elim = + let is_rec_elim = let count_occurn n term = let count = ref 0 in let rec occur_rec n c = match EConstr.kind sigma c with @@ -59,7 +59,7 @@ let analyze_eliminator elimty env sigma = in occur_rec n term; !count in let occurr2 n t = count_occurn n t > 1 in - not (List.for_all_i + not (List.for_all_i (fun i (_,rd) -> pred_id <= i || not (occurr2 (pred_id - i) rd)) 1 (assums_of_rel_context ctx)) in @@ -68,7 +68,7 @@ let analyze_eliminator elimty env sigma = let subgoals_tys sigma (relctx, concl) = let rec aux cur_depth acc = function - | hd :: rest -> + | hd :: rest -> let ty = Context.Rel.Declaration.get_type hd in if EConstr.Vars.noccurn sigma cur_depth concl && List.for_all_i (fun i -> function @@ -94,7 +94,7 @@ let subgoals_tys sigma (relctx, concl) = * 1. find the eliminator if not given as ~elim and analyze it * 2. build the patterns to be matched against the conclusion, looking at * (occ, c), deps and the pattern inferred from the type of the eliminator - * 3. build the new predicate matching the patterns, and the tactic to + * 3. build the new predicate matching the patterns, and the tactic to * generalize the equality in case eqid is not None * 4. build the tactic handle instructions and clears as required in ipats and * by eqid *) @@ -131,7 +131,7 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = let is_undef_pat = function | sigma, T t -> EConstr.isEvar sigma (EConstr.of_constr t) | _ -> false in - let match_pat env p occ h cl = + let match_pat env p occ h cl = let sigma0 = project orig_gl in ppdebug(lazy Pp.(str"matching: " ++ pr_occ occ ++ pp_pattern env p)); let (c,ucst), cl = @@ -139,11 +139,11 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = ppdebug(lazy Pp.(str" got: " ++ pr_constr_env env sigma0 c)); c, EConstr.of_constr cl, ucst in let mkTpat gl t = (* takes a term, refreshes it and makes a T pattern *) - let n, t, _, ucst = pf_abs_evars orig_gl (project gl, fire_subst gl t) in + let n, t, _, ucst = pf_abs_evars orig_gl (project gl, fire_subst gl t) in let t, _, _, sigma = saturate ~beta:true env (project gl) t n in Evd.merge_universe_context sigma ucst, T (EConstr.Unsafe.to_constr t) in let unif_redex gl (sigma, r as p) t = (* t is a hint for the redex of p *) - let n, t, _, ucst = pf_abs_evars orig_gl (project gl, fire_subst gl t) in + let n, t, _, ucst = pf_abs_evars orig_gl (project gl, fire_subst gl t) in let t, _, _, sigma = saturate ~beta:true env sigma t n in let sigma = Evd.merge_universe_context sigma ucst in match r with @@ -317,11 +317,11 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = (* if we are the index for the equation we do not clear *) let clr_t = if deps = [] && eqid <> None then [] else clr_t in let p = if is_undef_pat p then mkTpat gl inf_t else p in - loop (patterns @ [i, p, inf_t, occ]) + loop (patterns @ [i, p, inf_t, occ]) (clr_t @ clr) (i+1) (deps, inf_deps) - | [], c :: inf_deps -> + | [], c :: inf_deps -> ppdebug(lazy Pp.(str"adding inf pattern " ++ pr_econstr_pat env (project gl) c)); - loop (patterns @ [i, mkTpat gl c, c, allocc]) + loop (patterns @ [i, mkTpat gl c, c, allocc]) clr (i+1) ([], inf_deps) | _::_, [] -> errorstrm Pp.(str "Too many dependent abstractions") in let deps, head_p, inf_deps_r = match what, c_is_head_p, cty with @@ -332,7 +332,7 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = let occ = if occ = None then allocc else occ in let inf_p, inf_deps_r = List.hd inf_deps_r, List.tl inf_deps_r in deps, [1, pc, inf_p, occ], inf_deps_r in - let patterns, clr, gl = + let patterns, clr, gl = loop [] orig_clr (List.length head_p+1) (List.rev deps, inf_deps_r) in head_p @ patterns, Util.List.uniquize clr, gl in @@ -340,7 +340,7 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = ppdebug(lazy Pp.(pp_concat (str"inf. patterns=") (List.map (pp_inf_pat gl) patterns))); (* Predicate generation, and (if necessary) tactic to generalize the * equation asked by the user *) - let elim_pred, gen_eq_tac, clr, gl = + let elim_pred, gen_eq_tac, clr, gl = let error gl t inf_t = errorstrm Pp.(str"The given pattern matches the term"++ spc()++pp_term gl t++spc()++str"while the inferred pattern"++ spc()++pr_econstr_pat env (project gl) (fire_subst gl inf_t)++spc()++ str"doesn't") in @@ -356,19 +356,19 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = let gl = try pf_unify_HO gl inf_t c with exn when CErrors.noncritical exn -> error gl c inf_t in cl, gl, post - with + with | NoMatch | NoProgress -> let e, ucst = redex_of_pattern env p in let gl = pf_merge_uc ucst gl in let e = EConstr.of_constr e in let n, e, _, _ucst = pf_abs_evars gl (fst p, e) in - let e, _, _, gl = pf_saturate ~beta:true gl e n in + let e, _, _, gl = pf_saturate ~beta:true gl e n in let gl = try pf_unify_HO gl inf_t e with exn when CErrors.noncritical exn -> error gl e inf_t in cl, gl, post - in + in let rec match_all concl gl patterns = - let concl, gl, postponed = + let concl, gl, postponed = List.fold_left match_or_postpone (concl, gl, []) patterns in if postponed = [] then concl, gl else if List.length postponed = List.length patterns then @@ -377,8 +377,8 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = else match_all concl gl postponed in let concl, gl = match_all concl gl patterns in let pred_rctx, _ = EConstr.decompose_prod_assum (project gl) (fire_subst gl predty) in - let concl, gen_eq_tac, clr, gl = match eqid with - | Some (IPatId _) when not is_rec -> + let concl, gen_eq_tac, clr, gl = match eqid with + | Some (IPatId _) when not is_rec -> let k = List.length deps in let c = fire_subst gl (List.assoc (n_elim_args - k - 1) elim_args) in let gl, t = pfe_type_of gl c in @@ -405,7 +405,7 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = | _ -> concl, Tacticals.tclIDTAC, clr, gl in let mk_lam t r = EConstr.mkLambda_or_LetIn r t in let concl = List.fold_left mk_lam concl pred_rctx in - let gl, concl = + let gl, concl = if eqid <> None && is_rec then let gl, concls = pfe_type_of gl concl in let concl, gl = mkProt concls concl gl in @@ -421,10 +421,10 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = let gl = pf_resolve_typeclasses ~where:elim ~fail:false gl in let gl, _ = pf_e_type_of gl elim in (* check that the patterns do not contain non instantiated dependent metas *) - let () = + let () = let evars_of_term = Evarutil.undefined_evars_of_term (project gl) in let patterns = List.map (fun (_,_,t,_) -> fire_subst gl t) patterns in - let patterns_ev = List.map evars_of_term patterns in + let patterns_ev = List.map evars_of_term patterns in let ev = List.fold_left Evar.Set.union Evar.Set.empty patterns_ev in let ty_ev = Evar.Set.fold (fun i e -> let ex = i in @@ -441,7 +441,7 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = end in (* the elim tactic, with the eliminator and the predicated we computed *) - let elim = project gl, elim in + let elim = project gl, elim in let seed = Array.map (fun ty -> let ctx,_ = EConstr.decompose_prod_assum (project gl) ty in @@ -517,7 +517,7 @@ let perform_injection c gl = let cl1 = EConstr.mkLambda EConstr.(make_annot Anonymous Sorts.Relevant, mkArrow eqt Sorts.Relevant cl, mkApp (mkRel 1, [|c_eq|])) in let id = injecteq_id in let id_with_ebind = (EConstr.mkVar id, NoBindings) in - let injtac = Tacticals.tclTHEN (introid id) (injectidl2rtac id id_with_ebind) in + let injtac = Tacticals.tclTHEN (introid id) (injectidl2rtac id id_with_ebind) in Tacticals.tclTHENLAST (Proofview.V82.of_tactic (Tactics.apply (EConstr.compose_lam dc cl1))) injtac gl let ssrscase_or_inj_tac c = Proofview.V82.tactic ~nf_evars:false (fun gl -> diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index aa1316f15e..cdda84a18d 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -109,6 +109,11 @@ let congrtac ((n, t), ty) ist gl = loop 1 in tclTHEN (refine_with cf) (tclTRY (Proofview.V82.of_tactic Tactics.reflexivity)) gl +let pf_typecheck t gl = + let it = sig_it gl in + let sigma,_ = pf_type_of gl t in + re_sig [it] sigma + let newssrcongrtac arg ist gl = ppdebug(lazy Pp.(str"===newcongr===")); ppdebug(lazy Pp.(str"concl=" ++ Printer.pr_econstr_env (pf_env gl) (project gl) (pf_concl gl))); @@ -120,25 +125,31 @@ let newssrcongrtac arg ist gl = | Some gl_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 = + | None -> t_fail () gl in + let mk_evar gl ty = let env, sigma, si = pf_env gl, project gl, sig_it gl in let sigma = Evd.create_evar_defs sigma in let (sigma, x) = Evarutil.new_evar env sigma ty in x, re_sig si sigma in let arr, gl = pf_mkSsrConst "ssr_congr_arrow" gl in let ssr_congr lr = EConstr.mkApp (arr, lr) in + let eq, gl = pf_fresh_global Coqlib.(lib_ref "core.eq.type") gl in (* here the two cases: simple equality or arrow *) - let equality, _, eq_args, gl' = - let eq, gl = pf_fresh_global Coqlib.(lib_ref "core.eq.type") gl in - pf_saturate gl (EConstr.of_constr eq) 3 in + let equality, _, eq_args, gl' = pf_saturate gl (EConstr.of_constr eq) 3 in tclMATCH_GOAL (equality, gl') (fun gl' -> fs gl' (List.assoc 0 eq_args)) (fun ty -> congrtac (arg, Detyping.detype Detyping.Now false Id.Set.empty (pf_env gl) (project gl) ty) ist) (fun () -> - let lhs, gl' = mk_evar gl EConstr.mkProp in let rhs, gl' = mk_evar gl' EConstr.mkProp in + let gl', t_lhs = pfe_new_type gl in + let gl', t_rhs = pfe_new_type gl' in + let lhs, gl' = mk_evar gl' t_lhs in + let rhs, gl' = mk_evar gl' t_rhs in let arrow = EConstr.mkArrow lhs Sorts.Relevant (EConstr.Vars.lift 1 rhs) in tclMATCH_GOAL (arrow, gl') (fun gl' -> [|fs gl' lhs;fs gl' rhs|]) - (fun lr -> tclTHEN (Proofview.V82.of_tactic (Tactics.apply (ssr_congr lr))) (congrtac (arg, mkRType) ist)) + (fun lr -> + let a = ssr_congr lr in + tclTHENLIST [ pf_typecheck a + ; Proofview.V82.of_tactic (Tactics.apply a) + ; congrtac (arg, mkRType) ist ]) (fun _ _ -> errorstrm Pp.(str"Conclusion is not an equality nor an arrow"))) gl @@ -163,7 +174,7 @@ let nodocc = mkclr [] let is_rw_cut = function RWred (Cut _) -> true | _ -> false -let mk_rwarg (d, (n, _ as m)) ((clr, occ as docc), rx) (rt, _ as r) : ssrrwarg = +let mk_rwarg (d, (n, _ as m)) ((clr, occ as docc), rx) (rt, _ as r) : ssrrwarg = if rt <> RWeq then begin if rt = RWred Nop && not (m = nomult && occ = None && rx = None) && (clr = None || clr = Some []) then @@ -179,7 +190,7 @@ let mk_rwarg (d, (n, _ as m)) ((clr, occ as docc), rx) (rt, _ as r) : ssrrwarg = let norwmult = L2R, nomult let norwocc = noclr, None -let simplintac occ rdx sim gl = +let simplintac occ rdx sim gl = let simptac m gl = if m <> ~-1 then begin if rdx <> None then @@ -208,7 +219,7 @@ let rec get_evalref env sigma c = match EConstr.kind sigma c with (* Strip a pattern generated by a prenex implicit to its constant. *) let strip_unfold_term _ ((sigma, t) as p) kt = match EConstr.kind sigma t with - | App (f, a) when kt = xNoFlag && Array.for_all (EConstr.isEvar sigma) a && EConstr.isConst sigma f -> + | App (f, a) when kt = xNoFlag && Array.for_all (EConstr.isEvar sigma) a && EConstr.isConst sigma f -> (sigma, f), true | Const _ | Var _ -> p, true | Proj _ -> p, true @@ -224,7 +235,7 @@ let all_ok _ _ = true let fake_pmatcher_end () = mkProp, L2R, (Evd.empty, UState.empty, mkProp) -let unfoldintac occ rdx t (kt,_) gl = +let unfoldintac occ rdx t (kt,_) gl = let fs sigma x = Reductionops.nf_evar sigma x in let sigma0, concl0, env0 = project gl, pf_concl gl, pf_env gl in let (sigma, t), const = strip_unfold_term env0 t kt in @@ -239,18 +250,18 @@ let unfoldintac occ rdx t (kt,_) gl = let ise, u = mk_tpattern env0 sigma0 (ise,EConstr.Unsafe.to_constr t) all_ok L2R (EConstr.Unsafe.to_constr t) in let find_T, end_T = mk_tpattern_matcher ~raise_NoMatch:true sigma0 occ (ise,[u]) in - (fun env c _ h -> + (fun env c _ h -> try find_T env c h ~k:(fun env c _ _ -> EConstr.Unsafe.to_constr (body env t (EConstr.of_constr c))) with NoMatch when easy -> c | NoMatch | NoProgress -> errorstrm Pp.(str"No occurrence of " ++ pr_econstr_pat env sigma0 t ++ spc() ++ str "in " ++ Printer.pr_constr_env env sigma c)), - (fun () -> try end_T () with - | NoMatch when easy -> fake_pmatcher_end () + (fun () -> try end_T () with + | NoMatch when easy -> fake_pmatcher_end () | NoMatch -> anomaly "unfoldintac") - | _ -> + | _ -> (fun env (c as orig_c) _ h -> if const then - let rec aux c = + let rec aux c = match EConstr.kind sigma0 c with | Const _ when EConstr.eq_constr sigma0 c t -> body env t t | App (f,a) when EConstr.eq_constr sigma0 f t -> EConstr.mkApp (body env f f,a) @@ -271,15 +282,15 @@ let unfoldintac occ rdx t (kt,_) gl = with _ -> errorstrm Pp.(str "The term " ++ pr_constr_env env sigma c ++spc()++ str "does not unify with " ++ pr_econstr_pat env sigma t)), fake_pmatcher_end in - let concl = + let concl = let concl0 = EConstr.Unsafe.to_constr concl0 in - try beta env0 (EConstr.of_constr (eval_pattern env0 sigma0 concl0 rdx occ unfold)) + 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 ~check:true concl) gl ;; -let foldtac occ rdx ft gl = +let foldtac occ rdx ft gl = let sigma0, concl0, env0 = project gl, pf_concl gl, pf_env gl in let sigma, t = ft in let t = EConstr.to_constr ~abort_on_undefined_evars:false sigma t in @@ -292,7 +303,7 @@ let foldtac occ rdx ft gl = mk_tpattern_matcher ~raise_NoMatch:true sigma0 occ (ise,[ut]) in (fun env c _ h -> try find_T env c h ~k:(fun env t _ _ -> t) with NoMatch ->c), (fun () -> try end_T () with NoMatch -> fake_pmatcher_end ()) - | _ -> + | _ -> (fun env c _ h -> try let sigma = unify_HO env sigma (EConstr.of_constr c) (EConstr.of_constr t) in @@ -336,17 +347,21 @@ let pirrel_rewrite ?(under=false) ?(map_redex=id_map_redex) pred rdx rdx_ty new_ let sigma, p = (* The resulting goal *) Evarutil.new_evar env sigma (beta (EConstr.Vars.subst1 new_rdx pred)) in let pred = EConstr.mkNamedLambda (make_annot pattern_id Sorts.Relevant) rdx_ty pred in - let elim, gl = - let ((kn, i) as ind, _), unfolded_c_ty = pf_reduce_to_quantified_ind gl c_ty in + let sigma, elim = let sort = elimination_sort_of_goal gl in - let elim, gl = pf_fresh_global (Indrec.lookup_eliminator env ind sort) gl in - if dir = R2L then elim, gl else (* taken from Coq's rewrite *) - let elim, _ = destConst elim in - let mp,l = Constant.repr2 (Constant.make1 (Constant.canonical elim)) in - let l' = Label.of_id (Nameops.add_suffix (Label.to_id l) "_r") in - let c1' = Global.constant_of_delta_kn (Constant.canonical (Constant.make2 mp l')) in - mkConst c1', gl in - let elim = EConstr.of_constr elim in + match Equality.eq_elimination_ref (dir = L2R) sort with + | Some r -> Evd.fresh_global env sigma r + | None -> + let ((kn, i) as ind, _), unfolded_c_ty = Tacred.reduce_to_quantified_ind env sigma c_ty in + let sort = elimination_sort_of_goal gl in + let sigma, elim = Evd.fresh_global env sigma (Indrec.lookup_eliminator env ind sort) in + if dir = R2L then sigma, elim else + let elim, _ = EConstr.destConst sigma elim in + let mp,l = Constant.repr2 (Constant.make1 (Constant.canonical elim)) in + let l' = Label.of_id (Nameops.add_suffix (Label.to_id l) "_r") in + let c1' = Global.constant_of_delta_kn (Constant.canonical (Constant.make2 mp l')) in + sigma, EConstr.of_constr (mkConst c1') + in let proof = EConstr.mkApp (elim, [| rdx_ty; new_rdx; pred; p; rdx; c |]) in (* We check the proof is well typed *) let sigma, proof_ty = @@ -356,12 +371,12 @@ let pirrel_rewrite ?(under=false) ?(map_redex=id_map_redex) pred rdx rdx_ty new_ in ppdebug(lazy Pp.(str"pirrel_rewrite: proof term: " ++ pr_econstr_env env sigma proof)); ppdebug(lazy Pp.(str"pirrel_rewrite of type: " ++ pr_econstr_env env sigma proof_ty)); - try refine_with + try refine_with ~first_goes_last:(not !ssroldreworder || under) ~with_evars:under (sigma, proof) gl - with _ -> + with _ -> (* we generate a msg like: "Unable to find an instance for the variable" *) let hd_ty, miss = match EConstr.kind sigma c with - | App (hd, args) -> + | App (hd, args) -> let hd_ty = Retyping.get_type_of env sigma hd in let names = let rec aux t = function 0 -> [] | n -> let t = Reductionops.whd_all env sigma t in @@ -394,7 +409,7 @@ let rwcltac ?under ?map_redex cl rdx dir sr gl = (* ppdebug(lazy(str"sigma@rwcltac=" ++ pr_evar_map None (fst sr))); *) ppdebug(lazy Pp.(str"r@rwcltac=" ++ pr_econstr_env (pf_env gl) (project gl) (snd sr))); let cvtac, rwtac, gl = - if EConstr.Vars.closed0 (project gl) r' then + if EConstr.Vars.closed0 (project gl) r' then let env, sigma, c, c_eq = pf_env gl, fst sr, snd sr, Coqlib.(lib_ref "core.eq.type") in let sigma, c_ty = Typing.type_of env sigma c in ppdebug(lazy Pp.(str"c_ty@rwcltac=" ++ pr_econstr_env env sigma c_ty)); @@ -402,14 +417,14 @@ let rwcltac ?under ?map_redex cl rdx dir sr gl = | AtomicType(e, a) when Ssrcommon.is_ind_ref sigma e c_eq -> let new_rdx = if dir = L2R then a.(2) else a.(1) in pirrel_rewrite ?under ?map_redex cl rdx rdxt new_rdx dir (sigma,c) c_ty, tclIDTAC, 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 ~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 = + let r3, _, r3t = try EConstr.destCast (project gl) r2 with _ -> errorstrm Pp.(str "no cast from " ++ pr_econstr_pat (pf_env gl) (project gl) (snd sr) ++ str " to " ++ pr_econstr_env (pf_env gl) (project gl) r2) in @@ -456,7 +471,7 @@ let ssr_is_setoid env = | None -> fun _ _ _ -> false | Some srel -> fun sigma r args -> - Rewrite.is_applied_rewrite_relation env + Rewrite.is_applied_rewrite_relation env sigma [] (EConstr.mkApp (r, args)) <> None let closed0_check cl p gl = @@ -491,7 +506,8 @@ 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_monomorphic_global @@ Coqlib.(lib_ref "core.True.type"))) then + let sigma,trty = Evd.fresh_global env sigma Coqlib.(lib_ref "core.True.type") in + if EConstr.eq_constr sigma a.(0) trty then let s, sigma = sr sigma 2 in loop (converse_dir d) sigma s a.(1) rs 0 else @@ -569,7 +585,7 @@ let rwrxtac ?under ?map_redex occ rdx_pat dir rule gl = sigma, pats @ [pat] in let rpats = List.fold_left (rpat env0 sigma0) (r_sigma,[]) rules in let find_R, end_R = mk_tpattern_matcher sigma0 occ ~upats_origin rpats in - (fun e c _ i -> find_R ~k:(fun _ _ _ h -> mkRel h) e c i), + (fun e c _ i -> find_R ~k:(fun _ _ _ h -> mkRel h) e c i), fun cl -> let rdx,d,r = end_R () in closed0_check cl rdx gl; (d,r),rdx | Some(_, (T e | X_In_T (_,e) | E_As_X_In_T (e,_,_) | E_In_X_In_T (e,_,_))) -> let r = ref None in @@ -617,7 +633,7 @@ let rwargtac ?under ?map_redex ist ((dir, mult), (((oclr, occ), grx), (kind, gt) let interp gc gl = try interp_term ist gl gc with _ when snd mult = May -> fail := true; (project gl, EConstr.mkProp) in - let rwtac gl = + let rwtac gl = let rx = Option.map (interp_rpattern gl) grx in let gl = match rx with | None -> gl @@ -656,6 +672,6 @@ let unlocktac ist args gl = let locked, gl = pf_mkSsrConst "locked" gl in let key, gl = pf_mkSsrConst "master_key" gl in let ktacs = [ - (fun gl -> unfoldtac None None (project gl,locked) xInParens gl); + (fun gl -> unfoldtac None None (project gl,locked) xInParens gl); Proofview.V82.of_tactic (Ssrelim.casetac key (fun ?seed:_ k -> k)) ] in tclTHENLIST (List.map utac args @ ktacs) gl diff --git a/plugins/ssr/ssrequality.mli b/plugins/ssr/ssrequality.mli index 43aeeb2dae..baf5288725 100644 --- a/plugins/ssr/ssrequality.mli +++ b/plugins/ssr/ssrequality.mli @@ -42,6 +42,9 @@ val mk_rwarg : val norwmult : ssrdir * ssrmult val norwocc : (Ssrast.ssrclear option * Ssrast.ssrocc) * Ssrmatching.rpattern option +val ssr_is_setoid : + Environ.env -> Evd.evar_map -> EConstr.t -> EConstr.t array -> bool + val ssrinstancesofrule : Ltac_plugin.Tacinterp.interp_sign -> Ssrast.ssrdir -> diff --git a/plugins/ssr/ssrfun.v b/plugins/ssr/ssrfun.v index 5e600362b4..b8affba541 100644 --- a/plugins/ssr/ssrfun.v +++ b/plugins/ssr/ssrfun.v @@ -56,6 +56,10 @@ Require Import ssreflect. Structure inference, as in the implementation of the mxdirect predicate in matrix.v. + - The empty type: + void == a notation for the Empty_set type of the standard library. + of_void T == the canonical injection void -> T. + - Sigma types: tag w == the i of w : {i : I & T i}. tagged w == the T i component of w : {i : I & T i}. @@ -166,7 +170,7 @@ Require Import ssreflect. right_loop inv op <-> op, inv obey the inverse loop right axiom: (x op y) op (inv y) = x for all x, y. rev_right_loop inv op <-> op, inv obey the inverse loop reverse right - axiom: (x op y) op (inv y) = x for all x, y. + axiom: (x op (inv y)) op y = x for all x, y. Note that familiar "cancellation" identities like x + y - y = x or x - y + y = x are respectively instances of right_loop and rev_right_loop The corresponding lemmas will use the K and NK/VK suffixes, respectively. @@ -391,19 +395,19 @@ Notation "@^~ x" := (fun f => f x) : fun_scope. Definitions and notation for explicit functions with simplification, i.e., which simpl and /= beta expand (this is complementary to nosimpl). **) +#[universes(template)] +Variant simpl_fun (aT rT : Type) := SimplFun of aT -> rT. + Section SimplFun. Variables aT rT : Type. -#[universes(template)] -Variant simpl_fun := SimplFun of aT -> rT. +Definition fun_of_simpl (f : simpl_fun aT rT) := fun x => let: SimplFun lam := f in lam x. -Definition fun_of_simpl f := fun x => let: SimplFun lam := f in lam x. +End SimplFun. Coercion fun_of_simpl : simpl_fun >-> Funclass. -End SimplFun. - 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. @@ -483,6 +487,12 @@ Arguments idfun {T} x /. Definition phant_id T1 T2 v1 v2 := phantom T1 v1 -> phantom T2 v2. +(** The empty type. **) + +Notation void := Empty_set. + +Definition of_void T (x : void) : T := match x with end. + (** Strong sigma types. **) Section Tag. @@ -642,6 +652,9 @@ End Injections. Lemma Some_inj {T : nonPropType} : injective (@Some T). Proof. by move=> x y []. Qed. +Lemma of_voidK T : pcancel (of_void T) [fun _ => None]. +Proof. by case. Qed. + (** cancellation lemmas for dependent type casts. **) Lemma esymK T x y : cancel (@esym T x y) (@esym T y x). Proof. by case: y /. Qed. diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index cca94c8c9b..f486d1e457 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -42,7 +42,7 @@ let ssrsettac id ((_, (pat, pty)), (_, occ)) gl = (mkRHole, Some body), ist) pty in let pat = interp_cpattern gl pat pty in let cl, sigma, env = pf_concl gl, project gl, pf_env gl in - let (c, ucst), cl = + let (c, ucst), cl = let cl = EConstr.Unsafe.to_constr cl in try fill_occ_pattern ~raise_NoMatch:true env sigma cl pat occ 1 with NoMatch -> redex_of_pattern ~resolve_typeclasses:true env pat, cl in @@ -77,8 +77,8 @@ let () = }) -open Constrexpr -open Glob_term +open Constrexpr +open Glob_term let combineCG t1 t2 f g = match t1, t2 with | (x, (t1, None)), (_, (t2, None)) -> x, (g t1 t2, None) @@ -96,7 +96,7 @@ let introstac ipats = Proofview.V82.of_tactic (tclIPAT ipats) let havetac ist (transp,((((clr, orig_pats), binders), simpl), (((fk, _), t), hint))) - suff namefst gl + suff namefst gl = let concl = pf_concl gl in let pats = tclCompileIPats orig_pats in @@ -195,7 +195,7 @@ let havetac ist | _,false,true -> let _, ty, uc = interp_ty gl fixtc cty in let gl = pf_merge_uc uc gl in gl, EConstr.mkArrow ty Sorts.Relevant concl, hint, id, itac_c - | _, false, false -> + | _, false, false -> let n, cty, uc = interp_ty gl fixtc cty in let gl = pf_merge_uc uc gl in gl, cty, Tacticals.tclTHEN (binderstac n) hint, id, Tacticals.tclTHEN itac_c simpltac | _, true, false -> assert false in @@ -260,7 +260,7 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl = | _ -> CErrors.anomaly(str"SSR: wlog: pired: " ++ pr_econstr_env env sigma c) in c, args, pired c args, pf_merge_uc uc gl in let tacipat pats = introstac pats in - let tacigens = + let tacigens = Tacticals.tclTHEN (Tacticals.tclTHENLIST(List.rev(List.fold_right mkclr gens [old_cleartac clr0]))) (introstac (List.fold_right mkpats gens [])) in @@ -340,6 +340,21 @@ let intro_lock ipats = let hnf' = Proofview.numgoals >>= fun ng -> Proofview.tclDISPATCH (ncons (ng - 1) ssrsmovetac @ [Proofview.tclUNIT ()]) in + let protect_subgoal env sigma hd args = + Tactics.New.refine ~typecheck:true (fun sigma -> + let lm2 = Array.length args - 2 in + let sigma, carrier = + Typing.type_of env sigma args.(lm2) in + let rel = EConstr.mkApp (hd, Array.sub args 0 lm2) in + let rel_args = Array.sub args lm2 2 in + let sigma, under_rel = + Ssrcommon.mkSsrConst "Under_rel" env sigma in + let sigma, under_from_rel = + Ssrcommon.mkSsrConst "Under_rel_from_rel" env sigma in + let under_rel_args = Array.append [|carrier; rel|] rel_args in + let ty = EConstr.mkApp (under_rel, under_rel_args) in + let sigma, t = Evarutil.new_evar env sigma ty in + sigma, EConstr.mkApp(under_from_rel,Array.append under_rel_args [|t|])) in let rec lock_eq () : unit Proofview.tactic = Proofview.Goal.enter begin fun _ -> Proofview.tclORELSE (Ssripats.tclIPAT [Ssripats.IOpTemporay; Ssripats.IOpEqGen (lock_eq ())]) @@ -349,30 +364,23 @@ let intro_lock ipats = let env = Proofview.Goal.env gl in match EConstr.kind_of_type sigma c with | Term.AtomicType(hd, args) when + Array.length args >= 2 && is_app_evar sigma (Array.last args) && + Ssrequality.ssr_is_setoid env sigma hd args + (* if the last condition above [ssr_is_setoid ...] holds + then [Coq.Classes.RelationClasses] has been required *) + || + (* if this is not the case, the tactic can still succeed + when the considered relation is [Coq.Init.Logic.iff] *) Ssrcommon.is_const_ref sigma hd (Coqlib.lib_ref "core.iff.type") && - Array.length args = 2 && is_app_evar sigma args.(1) -> - Tactics.New.refine ~typecheck:true (fun sigma -> - let sigma, under_iff = - Ssrcommon.mkSsrConst "Under_iff" env sigma in - let sigma, under_from_iff = - Ssrcommon.mkSsrConst "Under_iff_from_iff" env sigma in - let ty = EConstr.mkApp (under_iff,args) in - let sigma, t = Evarutil.new_evar env sigma ty in - sigma, EConstr.mkApp(under_from_iff,Array.append args [|t|])) + Array.length args = 2 && is_app_evar sigma args.(1) -> + protect_subgoal env sigma hd args | _ -> let t = Reductionops.whd_all env sigma c in match EConstr.kind_of_type sigma t with | Term.AtomicType(hd, args) when Ssrcommon.is_ind_ref sigma hd (Coqlib.lib_ref "core.eq.type") && Array.length args = 3 && is_app_evar sigma args.(2) -> - Tactics.New.refine ~typecheck:true (fun sigma -> - let sigma, under = - Ssrcommon.mkSsrConst "Under_eq" env sigma in - let sigma, under_from_eq = - Ssrcommon.mkSsrConst "Under_eq_from_eq" env sigma in - let ty = EConstr.mkApp (under,args) in - let sigma, t = Evarutil.new_evar env sigma ty in - sigma, EConstr.mkApp(under_from_eq,Array.append args [|t|])) + protect_subgoal env sigma hd args | _ -> ppdebug(lazy Pp.(str"under: stop:" ++ pr_econstr_env env sigma t)); diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index c09250ade5..22325f3fc3 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -32,7 +32,6 @@ open Ppconstr open Namegen open Tactypes -open Decl_kinds open Constrexpr open Constrexpr_ops @@ -168,7 +167,7 @@ let pr_name = function Name id -> pr_id id | Anonymous -> str "_" let pr_spc () = str " " let pr_list = prlist_with_sep -(**************************** ssrhyp **************************************) +(**************************** ssrhyp **************************************) let pr_ssrhyp _ _ _ = pr_hyp @@ -235,7 +234,7 @@ let pr_ssrsimpl _ _ _ = pr_simpl let wit_ssrsimplrep = add_genarg "ssrsimplrep" (fun env sigma -> pr_simpl) -let test_ssrslashnum b1 b2 strm = +let test_ssrslashnum b1 b2 _ strm = match Util.stream_nth 0 strm with | Tok.KEYWORD "/" -> (match Util.stream_nth 1 strm with @@ -276,11 +275,11 @@ let test_ssrslashnum11 = test_ssrslashnum true true let test_ssrslashnum01 = test_ssrslashnum false true let test_ssrslashnum00 = test_ssrslashnum false false -let negate_parser f x = - let rc = try Some (f x) with Stream.Failure -> None in +let negate_parser f tok x = + let rc = try Some (f tok x) with Stream.Failure -> None in match rc with | None -> () - | Some _ -> raise Stream.Failure + | Some _ -> raise Stream.Failure let test_not_ssrslashnum = Pcoq.Entry.of_parser @@ -385,7 +384,6 @@ open Pltac ARGUMENT EXTEND ssrindex PRINTED BY { pr_ssrindex } INTERPRETED BY { interp_index } -| [ int_or_var(i) ] -> { mk_index ~loc i } END @@ -475,7 +473,7 @@ END (* Old kinds of terms *) -let input_ssrtermkind strm = match Util.stream_nth 0 strm with +let input_ssrtermkind _ strm = match Util.stream_nth 0 strm with | Tok.KEYWORD "(" -> xInParens | Tok.KEYWORD "@" -> xWithAt | _ -> xNoFlag @@ -484,7 +482,7 @@ let ssrtermkind = Pcoq.Entry.of_parser "ssrtermkind" input_ssrtermkind (* New kinds of terms *) -let input_term_annotation strm = +let input_term_annotation _ strm = match Stream.npeek 2 strm with | Tok.KEYWORD "(" :: Tok.KEYWORD "(" :: _ -> `DoubleParens | Tok.KEYWORD "(" :: _ -> `Parens @@ -523,7 +521,6 @@ ARGUMENT EXTEND ssrterm GLOBALIZED BY { glob_ssrterm } SUBSTITUTED BY { subst_ssrterm } RAW_PRINTED BY { pr_ssrterm } GLOB_PRINTED BY { pr_ssrterm } -| [ "YouShouldNotTypeThis" constr(c) ] -> { mk_lterm c } END GRAMMAR EXTEND Gram @@ -570,7 +567,6 @@ let pr_ssrbwdview _ _ _ = pr_view ARGUMENT EXTEND ssrbwdview TYPED AS ssrterm list PRINTED BY { pr_ssrbwdview } -| [ "YouShouldNotTypeThis" ] -> { [] } END (* Pcoq *) @@ -594,7 +590,6 @@ let pr_ssrfwdview _ _ _ = pr_view2 ARGUMENT EXTEND ssrfwdview TYPED AS ast_closure_term list PRINTED BY { pr_ssrfwdview } -| [ "YouShouldNotTypeThis" ] -> { [] } END (* Pcoq *) @@ -617,10 +612,10 @@ let ipat_of_intro_pattern p = Tactypes.( | IntroAction IntroWildcard -> IPatAnon Drop | IntroAction (IntroOrAndPattern (IntroOrPattern iorpat)) -> IPatCase (Regular( - List.map (List.map ipat_of_intro_pattern) - (List.map (List.map remove_loc) iorpat))) + List.map (List.map ipat_of_intro_pattern) + (List.map (List.map remove_loc) iorpat))) | IntroAction (IntroOrAndPattern (IntroAndPattern iandpat)) -> - IPatCase + IPatCase (Regular [List.map ipat_of_intro_pattern (List.map remove_loc iandpat)]) | IntroNaming IntroAnonymous -> IPatAnon (One None) | IntroAction (IntroRewrite b) -> IPatRewrite (allocc, if b then L2R else R2L) @@ -693,7 +688,7 @@ let rec add_intro_pattern_hyps ipat hyps = | IntroAction (IntroRewrite _) -> hyps | IntroAction (IntroInjection ips) -> List.fold_right add_intro_pattern_hyps ips hyps | IntroAction (IntroApplyOn (c,pat)) -> add_intro_pattern_hyps pat hyps - | IntroForthcoming _ -> + | IntroForthcoming _ -> (* As in ipat_of_intro_pattern, was unable to determine which kind of ipat interp_introid could return [HH] *) assert false @@ -751,7 +746,7 @@ let pushIPatNoop = function | pats :: orpat -> (IPatNoop :: pats) :: orpat | [] -> [] -let test_ident_no_do strm = +let test_ident_no_do _ strm = match Util.stream_nth 0 strm with | Tok.IDENT s when s <> "do" -> () | _ -> raise Stream.Failure @@ -762,7 +757,6 @@ let test_ident_no_do = } ARGUMENT EXTEND ident_no_do PRINTED BY { fun _ _ _ -> Names.Id.print } -| [ "YouShouldNotTypeThis" ident(id) ] -> { id } END @@ -830,7 +824,7 @@ END { -let reject_ssrhid strm = +let reject_ssrhid _ strm = match Util.stream_nth 0 strm with | Tok.KEYWORD "[" -> (match Util.stream_nth 1 strm with @@ -840,13 +834,13 @@ let reject_ssrhid strm = let test_nohidden = Pcoq.Entry.of_parser "test_ssrhid" reject_ssrhid -let rec reject_binder crossed_paren k s = +let rec reject_binder crossed_paren k tok s = match try Some (Util.stream_nth k s) with Stream.Failure -> None with - | Some (Tok.KEYWORD "(") when not crossed_paren -> reject_binder true (k+1) s - | Some (Tok.IDENT _) when crossed_paren -> reject_binder true (k+1) s + | Some (Tok.KEYWORD "(") when not crossed_paren -> reject_binder true (k+1) tok s + | Some (Tok.IDENT _) when crossed_paren -> reject_binder true (k+1) tok s | Some (Tok.KEYWORD ":" | Tok.KEYWORD ":=") when crossed_paren -> raise Stream.Failure | Some (Tok.KEYWORD ")") when crossed_paren -> raise Stream.Failure @@ -857,7 +851,6 @@ let _test_nobinder = Pcoq.Entry.of_parser "test_nobinder" (reject_binder false 0 } ARGUMENT EXTEND ssrcpat TYPED AS ssripatrep PRINTED BY { pr_ssripat } - | [ "YouShouldNotTypeThis" ssriorpat(x) ] -> { IPatCase(Regular x) } END (* Pcoq *) @@ -897,12 +890,12 @@ let check_ssrhpats loc w_binders ipats = let err_loc s = CErrors.user_err ~loc ~hdr:"ssreflect" s in let clr, ipats = let opt_app = function None -> fun l -> Some l - | Some l1 -> fun l2 -> Some (l1 @ l2) in + | Some l1 -> fun l2 -> Some (l1 @ l2) in let rec aux clr = function | IPatClear cl :: tl -> aux (opt_app clr cl) tl | tl -> clr, tl in aux None ipats in - let simpl, ipats = + let simpl, ipats = match List.rev ipats with | IPatSimpl _ as s :: tl -> [s], List.rev tl | _ -> [], ipats in @@ -913,7 +906,7 @@ let check_ssrhpats loc w_binders ipats = | [] -> ipat, [] | ( IPatId _| IPatAnon _| IPatCase _ | IPatDispatch _ | IPatRewrite _ as i) :: tl -> if w_binders then - if simpl <> [] && tl <> [] then + if simpl <> [] && tl <> [] then err_loc(str"binders XOR s-item allowed here: "++pr_ipats(tl@simpl)) else if not (List.for_all (function IPatId _ -> true | _ -> false) tl) then err_loc (str "Only binders allowed here: " ++ pr_ipats tl) @@ -946,7 +939,7 @@ ARGUMENT EXTEND ssrhpats_wtransp | [ ssripats(i) "@" ssripats(j) ] -> { true,check_ssrhpats loc true (i @ j) } END -ARGUMENT EXTEND ssrhpats_nobs +ARGUMENT EXTEND ssrhpats_nobs TYPED AS (((ssrclear option * ssripats) * ssripats) * ssripats) PRINTED BY { pr_ssrhpats } | [ ssripats(i) ] -> { check_ssrhpats loc false i } END @@ -985,7 +978,6 @@ let pr_ssrintrosarg env sigma _ _ prt (tac, ipats) = ARGUMENT EXTEND ssrintrosarg TYPED AS (tactic * ssrintros) PRINTED BY { pr_ssrintrosarg env sigma } -| [ "YouShouldNotTypeThis" ssrtacarg(arg) ssrintros_ne(ipats) ] -> { arg, ipats } END { @@ -1013,7 +1005,7 @@ END { -let accept_ssrfwdid strm = +let accept_ssrfwdid _ strm = match stream_nth 0 strm with | Tok.IDENT id -> accept_before_syms_or_any_id [":"; ":="; "("] strm | _ -> raise Stream.Failure @@ -1027,7 +1019,7 @@ GRAMMAR EXTEND Gram ssrfwdid: [[ test_ssrfwdid; id = Prim.ident -> { id } ]]; END - + (* by *) (** Tactical arguments. *) @@ -1117,7 +1109,7 @@ END open Ssrmatching_plugin.Ssrmatching open Ssrmatching_plugin.G_ssrmatching -let pr_wgen = function +let pr_wgen = function | (clr, Some((id,k),None)) -> spc() ++ pr_clear mt clr ++ str k ++ pr_hoi id | (clr, Some((id,k),Some p)) -> spc() ++ pr_clear mt clr ++ str"(" ++ str k ++ pr_hoi id ++ str ":=" ++ @@ -1160,7 +1152,7 @@ let pr_ssrclausehyps _ _ _ = pr_clausehyps } -ARGUMENT EXTEND ssrclausehyps +ARGUMENT EXTEND ssrclausehyps TYPED AS ssrwgen list PRINTED BY { pr_ssrclausehyps } | [ ssrwgen(hyp) "," ssrclausehyps(hyps) ] -> { hyp :: hyps } | [ ssrwgen(hyp) ssrclausehyps(hyps) ] -> { hyp :: hyps } @@ -1171,7 +1163,7 @@ END (* type ssrclauses = ssrahyps * ssrclseq *) -let pr_clauses (hyps, clseq) = +let pr_clauses (hyps, clseq) = if clseq = InGoal then mt () else str "in " ++ pr_clausehyps hyps ++ pr_clseq clseq let pr_ssrclauses _ _ _ = pr_clauses @@ -1223,7 +1215,7 @@ let rec format_local_binders h0 bl0 = match h0, bl0 with | BFdef :: h, CLocalDef ({CAst.v=x}, v, oty) :: bl -> Bdef (x, oty, v) :: format_local_binders h bl | _ -> [] - + let rec format_constr_expr h0 c0 = let open CAst in match h0, c0 with | BFvar :: h, { v = CLambdaN ([CLocalAssum([{CAst.v=x}], _, _)], c) } -> let bs, c' = format_constr_expr h c in @@ -1236,11 +1228,11 @@ let rec format_constr_expr h0 c0 = let open CAst in match h0, c0 with Bdef (x, oty, v) :: bs, c' | [BFcast], { v = CCast (c, Glob_term.CastConv t) } -> [Bcast t], c - | BFrec (has_str, has_cast) :: h, + | BFrec (has_str, has_cast) :: h, { v = CFix ( _, [_, Some {CAst.v = CStructRec locn}, bl, t, c]) } -> let bs = format_local_binders h bl in let bstr = if has_str then [Bstruct (Name locn.CAst.v)] else [] in - bs @ bstr @ (if has_cast then [Bcast t] else []), c + bs @ bstr @ (if has_cast then [Bcast t] else []), c | BFrec (_, has_cast) :: h, { v = CCoFix ( _, [_, bl, t, c]) } -> format_local_binders h bl @ (if has_cast then [Bcast t] else []), c | _, c -> @@ -1344,20 +1336,20 @@ ARGUMENT EXTEND ssrbinder TYPED AS (ssrfwdfmt * constr) PRINTED BY { pr_ssrbinde | [ ssrbvar(bv) ] -> { let { CAst.loc=xloc } as x = bvar_lname bv in (FwdPose, [BFvar]), - CAst.make ~loc @@ CLambdaN ([CLocalAssum([x],Default Explicit,mkCHole xloc)],mkCHole (Some loc)) } + CAst.make ~loc @@ CLambdaN ([CLocalAssum([x],Default Glob_term.Explicit,mkCHole xloc)],mkCHole (Some loc)) } | [ "(" ssrbvar(bv) ")" ] -> { let { CAst.loc=xloc } as x = bvar_lname bv in (FwdPose, [BFvar]), - CAst.make ~loc @@ CLambdaN ([CLocalAssum([x],Default Explicit,mkCHole xloc)],mkCHole (Some loc)) } + CAst.make ~loc @@ CLambdaN ([CLocalAssum([x],Default Glob_term.Explicit,mkCHole xloc)],mkCHole (Some loc)) } | [ "(" ssrbvar(bv) ":" lconstr(t) ")" ] -> { let x = bvar_lname bv in (FwdPose, [BFdecl 1]), - CAst.make ~loc @@ CLambdaN ([CLocalAssum([x], Default Explicit, t)], mkCHole (Some loc)) } + CAst.make ~loc @@ CLambdaN ([CLocalAssum([x], Default Glob_term.Explicit, t)], mkCHole (Some loc)) } | [ "(" ssrbvar(bv) ne_ssrbvar_list(bvs) ":" lconstr(t) ")" ] -> { let xs = List.map bvar_lname (bv :: bvs) in let n = List.length xs in (FwdPose, [BFdecl n]), - CAst.make ~loc @@ CLambdaN ([CLocalAssum (xs, Default Explicit, t)], mkCHole (Some loc)) } + CAst.make ~loc @@ CLambdaN ([CLocalAssum (xs, Default Glob_term.Explicit, t)], mkCHole (Some loc)) } | [ "(" ssrbvar(id) ":" lconstr(t) ":=" lconstr(v) ")" ] -> { (FwdPose,[BFdef]), CAst.make ~loc @@ CLetIn (bvar_lname id, v, Some t, mkCHole (Some loc)) } | [ "(" ssrbvar(id) ":=" lconstr(v) ")" ] -> @@ -1369,7 +1361,7 @@ GRAMMAR EXTEND Gram ssrbinder: [ [ ["of" -> { () } | "&" -> { () } ]; c = operconstr LEVEL "99" -> { (FwdPose, [BFvar]), - CAst.make ~loc @@ CLambdaN ([CLocalAssum ([CAst.make ~loc Anonymous],Default Explicit,c)],mkCHole (Some loc)) } ] + CAst.make ~loc @@ CLambdaN ([CLocalAssum ([CAst.make ~loc Anonymous],Default Glob_term.Explicit,c)],mkCHole (Some loc)) } ] ]; END @@ -1398,7 +1390,7 @@ let push_binders c2 bs = let rec fix_binders = let open CAst in function | (_, { v = CLambdaN ([CLocalAssum(xs, _, t)], _) } ) :: bs -> - CLocalAssum (xs, Default Explicit, t) :: fix_binders bs + CLocalAssum (xs, Default Glob_term.Explicit, t) :: fix_binders bs | (_, { v = CLetIn (x, v, oty, _) } ) :: bs -> CLocalDef (x, v, oty) :: fix_binders bs | _ -> [] @@ -1524,11 +1516,11 @@ END { -let intro_id_to_binder = List.map (function +let intro_id_to_binder = List.map (function | IPatId id -> let { CAst.loc=xloc } as x = bvar_lname (mkCVar id) in (FwdPose, [BFvar]), - CAst.make @@ CLambdaN ([CLocalAssum([x], Default Explicit, mkCHole xloc)], + CAst.make @@ CLambdaN ([CLocalAssum([x], Default Glob_term.Explicit, mkCHole xloc)], mkCHole None) | _ -> anomaly "non-id accepted as binder") @@ -1597,7 +1589,7 @@ END let sq_brace_tacnames = ["first"; "solve"; "do"; "rewrite"; "have"; "suffices"; "wlog"] (* "by" is a keyword *) -let accept_ssrseqvar strm = +let accept_ssrseqvar _ strm = match stream_nth 0 strm with | Tok.IDENT id when not (List.mem id sq_brace_tacnames) -> accept_before_syms_or_ids ["["] ["first";"last"] strm @@ -1691,11 +1683,11 @@ let ssr_id_of_string loc s = ^ "Scripts with explicit references to anonymous variables are fragile.")) end; Id.of_string s -let ssr_null_entry = Pcoq.Entry.of_parser "ssr_null" (fun _ -> ()) +let ssr_null_entry = Pcoq.Entry.of_parser "ssr_null" (fun _ _ -> ()) } -GRAMMAR EXTEND Gram +GRAMMAR EXTEND Gram GLOBAL: Prim.ident; Prim.ident: [[ s = IDENT; ssr_null_entry -> { ssr_id_of_string loc s } ]]; END @@ -1711,14 +1703,6 @@ let _ = add_internal_name (is_tagged perm_tag) (** Tactical extensions. *) -(* The TACTIC EXTEND facility can't be used for defining new user *) -(* tacticals, because: *) -(* - the concrete syntax must start with a fixed string *) -(* We use the following workaround: *) -(* - We use the (unparsable) "YouShouldNotTypeThis" token for tacticals that *) -(* don't start with a token, then redefine the grammar and *) -(* printer using GEXTEND and set_pr_ssrtac, respectively. *) - { type ssrargfmt = ArgSsr of string | ArgSep of string @@ -1772,8 +1756,8 @@ END { let ssrautoprop gl = - try - let tacname = + try + let tacname = try Tacenv.locate_tactic (qualid_of_ident (Id.of_string "ssrautoprop")) with Not_found -> Tacenv.locate_tactic (ssrqid "ssrautoprop") in let tacexpr = CAst.make @@ Tacexpr.Reference (ArgArg (Loc.tag @@ tacname)) in @@ -2002,7 +1986,7 @@ END { -let accept_ssreqid strm = +let accept_ssreqid _ strm = match Util.stream_nth 0 strm with | Tok.IDENT _ -> accept_before_syms [":"] strm | Tok.KEYWORD ":" -> () @@ -2184,7 +2168,7 @@ let pr_ssraarg _ _ _ (view, (dgens, ipats)) = } -ARGUMENT EXTEND ssrapplyarg +ARGUMENT EXTEND ssrapplyarg TYPED AS (ssrbwdview * (ssragens * ssrintros)) PRINTED BY { pr_ssraarg } | [ ":" ssragen(gen) ssragens(dgens) ssrintros(intros) ] -> @@ -2243,8 +2227,6 @@ END (** The "congr" tactic *) -(* type ssrcongrarg = open_constr * (int * constr) *) - { let pr_ssrcongrarg _ _ _ ((n, f), dgens) = @@ -2423,7 +2405,7 @@ let lbrace = Char.chr 123 (** Workaround to a limitation of coqpp *) let test_ssr_rw_syntax = - let test strm = + let test _ strm = if not !ssr_rw_syntax then raise Stream.Failure else if is_ssr_loaded () then () else match Util.stream_nth 0 strm with @@ -2585,7 +2567,7 @@ ARGUMENT EXTEND ssrwlogfwd TYPED AS (ssrwgen list * ssrfwd) | [ ":" ssrwgen_list(gens) "/" ast_closure_lterm(t) ] -> { gens, mkFwdHint "/" t} END - + TACTIC EXTEND ssrwlog | [ "wlog" ssrhpats_nobs(pats) ssrwlogfwd(fwd) ssrhint(hint) ] -> { V82.tactic (wlogtac ist pats fwd hint false `NoGen) } @@ -2607,13 +2589,13 @@ TACTIC EXTEND ssrwithoutloss END TACTIC EXTEND ssrwithoutlosss -| [ "without" "loss" "suff" +| [ "without" "loss" "suff" ssrhpats_nobs(pats) ssrwlogfwd(fwd) ssrhint(hint) ] -> { V82.tactic (wlogtac ist pats fwd hint true `NoGen) } END TACTIC EXTEND ssrwithoutlossss -| [ "without" "loss" "suffices" +| [ "without" "loss" "suffices" ssrhpats_nobs(pats) ssrwlogfwd(fwd) ssrhint(hint) ]-> { V82.tactic (wlogtac ist pats fwd hint true `NoGen) } END @@ -2634,7 +2616,7 @@ END { -let accept_idcomma strm = +let accept_idcomma _ strm = match stream_nth 0 strm with | Tok.IDENT _ | Tok.KEYWORD "_" -> accept_before_syms [","] strm | _ -> raise Stream.Failure @@ -2645,7 +2627,7 @@ let test_idcomma = Pcoq.Entry.of_parser "test_idcomma" accept_idcomma GRAMMAR EXTEND Gram GLOBAL: ssr_idcomma; - ssr_idcomma: [ [ test_idcomma; + ssr_idcomma: [ [ test_idcomma; ip = [ id = IDENT -> { Some (Id.of_string id) } | "_" -> { None } ]; "," -> { Some ip } ] ]; diff --git a/plugins/ssr/ssrprinters.mli b/plugins/ssr/ssrprinters.mli index e4df7399e1..240b1a5476 100644 --- a/plugins/ssr/ssrprinters.mli +++ b/plugins/ssr/ssrprinters.mli @@ -17,7 +17,7 @@ val pp_term : val pr_spc : unit -> Pp.t val pr_bar : unit -> Pp.t -val pr_list : +val pr_list : (unit -> Pp.t) -> ('a -> Pp.t) -> 'a list -> Pp.t val pp_concat : diff --git a/plugins/ssr/ssrsetoid.v b/plugins/ssr/ssrsetoid.v new file mode 100644 index 0000000000..609c9d5ab8 --- /dev/null +++ b/plugins/ssr/ssrsetoid.v @@ -0,0 +1,122 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** #<style> .doc { font-family: monospace; white-space: pre; } </style># **) + +(** Compatibility layer for [under] and [setoid_rewrite]. + + This file is intended to be required by [Require Import Setoid]. + + In particular, we can use the [under] tactic with other relations + than [eq] or [iff], e.g. a [RewriteRelation], by doing: + [Require Import ssreflect. Require Setoid.] + + This file's instances have priority 12 > other stdlib instances + and each [Under_rel] instance comes with a [Hint Cut] directive + (otherwise Ring_polynom.v won't compile because of unbounded search). + + (Note: this file could be skipped when porting [under] to stdlib2.) + *) + +Require Import ssrclasses. +Require Import ssrunder. +Require Import RelationClasses. +Require Import Relation_Definitions. + +(** Reconcile [Coq.Classes.RelationClasses.Reflexive] with + [Coq.ssr.ssrclasses.Reflexive] *) + +Instance compat_Reflexive : + forall {A} {R : relation A}, + RelationClasses.Reflexive R -> + ssrclasses.Reflexive R | 12. +Proof. now trivial. Qed. + +(** Add instances so that ['Under[ F i ]] terms, + that is, [Under_rel T R (F i) (?G i)] terms, + can be manipulated with rewrite/setoid_rewrite with lemmas on [R]. + Note that this requires that [R] is a [Prop] relation, otherwise + a [bool] relation may need to be "lifted": see the [TestPreOrder] + section in test-suite/ssr/under.v *) + +Instance Under_subrelation {A} (R : relation A) : subrelation R (Under_rel _ R) | 12. +Proof. now rewrite Under_relE. Qed. + +(* see also Morphisms.trans_co_eq_inv_impl_morphism *) + +Instance Under_Reflexive {A} (R : relation A) : + RelationClasses.Reflexive R -> + RelationClasses.Reflexive (Under_rel.Under_rel A R) | 12. +Proof. now rewrite Under_rel.Under_relE. Qed. + +Hint Cut [_* Under_Reflexive Under_Reflexive] : typeclass_instances. + +(* These instances are a bit off-topic given that (Under_rel A R) will + typically be reflexive, to be able to trigger the [over] terminator + +Instance under_Irreflexive {A} (R : relation A) : + RelationClasses.Irreflexive R -> + RelationClasses.Irreflexive (Under_rel.Under_rel A R) | 12. +Proof. now rewrite Under_rel.Under_relE. Qed. + +Hint Cut [_* Under_Irreflexive Under_Irreflexive] : typeclass_instances. + +Instance under_Asymmetric {A} (R : relation A) : + RelationClasses.Asymmetric R -> + RelationClasses.Asymmetric (Under_rel.Under_rel A R) | 12. +Proof. now rewrite Under_rel.Under_relE. Qed. + +Hint Cut [_* Under_Asymmetric Under_Asymmetric] : typeclass_instances. + +Instance under_StrictOrder {A} (R : relation A) : + RelationClasses.StrictOrder R -> + RelationClasses.StrictOrder (Under_rel.Under_rel A R) | 12. +Proof. now rewrite Under_rel.Under_relE. Qed. + +Hint Cut [_* Under_Strictorder Under_Strictorder] : typeclass_instances. + *) + +Instance Under_Symmetric {A} (R : relation A) : + RelationClasses.Symmetric R -> + RelationClasses.Symmetric (Under_rel.Under_rel A R) | 12. +Proof. now rewrite Under_rel.Under_relE. Qed. + +Hint Cut [_* Under_Symmetric Under_Symmetric] : typeclass_instances. + +Instance Under_Transitive {A} (R : relation A) : + RelationClasses.Transitive R -> + RelationClasses.Transitive (Under_rel.Under_rel A R) | 12. +Proof. now rewrite Under_rel.Under_relE. Qed. + +Hint Cut [_* Under_Transitive Under_Transitive] : typeclass_instances. + +Instance Under_PreOrder {A} (R : relation A) : + RelationClasses.PreOrder R -> + RelationClasses.PreOrder (Under_rel.Under_rel A R) | 12. +Proof. now rewrite Under_rel.Under_relE. Qed. + +Hint Cut [_* Under_PreOrder Under_PreOrder] : typeclass_instances. + +Instance Under_PER {A} (R : relation A) : + RelationClasses.PER R -> + RelationClasses.PER (Under_rel.Under_rel A R) | 12. +Proof. now rewrite Under_rel.Under_relE. Qed. + +Hint Cut [_* Under_PER Under_PER] : typeclass_instances. + +Instance Under_Equivalence {A} (R : relation A) : + RelationClasses.Equivalence R -> + RelationClasses.Equivalence (Under_rel.Under_rel A R) | 12. +Proof. now rewrite Under_rel.Under_relE. Qed. + +Hint Cut [_* Under_Equivalence Under_Equivalence] : typeclass_instances. + +(* Don't handle Antisymmetric and PartialOrder classes for now, + as these classes depend on two relation symbols... *) diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml index cd2448d764..0fc05f58d3 100644 --- a/plugins/ssr/ssrtacticals.ml +++ b/plugins/ssr/ssrtacticals.ml @@ -109,7 +109,7 @@ let endclausestac id_map clseq gl_id cl0 gl = EConstr.mkLetIn ({na with binder_name=Name (orig_id id)}, unmark v, unmark t, unmark c') | _ -> EConstr.map (project gl) unmark c in let utac hyp = - Proofview.V82.of_tactic + Proofview.V82.of_tactic (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' = diff --git a/plugins/ssr/ssrunder.v b/plugins/ssr/ssrunder.v new file mode 100644 index 0000000000..7c529a6133 --- /dev/null +++ b/plugins/ssr/ssrunder.v @@ -0,0 +1,75 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** #<style> .doc { font-family: monospace; white-space: pre; } </style># **) + +(** Constants for under/over, to rewrite under binders using "context lemmas" + + Note: this file does not require [ssreflect]; it is both required by + [ssrsetoid] and *exported* by [ssrunder]. + + This preserves the following feature: we can use [Setoid] without + requiring [ssreflect] and use [ssreflect] without requiring [Setoid]. +*) + +Require Import ssrclasses. + +Module Type UNDER_REL. +Parameter Under_rel : + forall (A : Type) (eqA : A -> A -> Prop), A -> A -> Prop. +Parameter Under_rel_from_rel : + forall (A : Type) (eqA : A -> A -> Prop) (x y : A), + @Under_rel A eqA x y -> eqA x y. +Parameter Under_relE : + forall (A : Type) (eqA : A -> A -> Prop), + @Under_rel A eqA = eqA. + +(** [Over_rel, over_rel, over_rel_done]: for "by rewrite over_rel" *) +Parameter Over_rel : + forall (A : Type) (eqA : A -> A -> Prop), A -> A -> Prop. +Parameter over_rel : + forall (A : Type) (eqA : A -> A -> Prop) (x y : A), + @Under_rel A eqA x y = @Over_rel A eqA x y. +Parameter over_rel_done : + forall (A : Type) (eqA : A -> A -> Prop) (EeqA : Reflexive eqA) (x : A), + @Over_rel A eqA x x. + +(** [under_rel_done]: for Ltac-style over *) +Parameter under_rel_done : + forall (A : Type) (eqA : A -> A -> Prop) (EeqA : Reflexive eqA) (x : A), + @Under_rel A eqA x x. +Notation "''Under[' x ]" := (@Under_rel _ _ x _) + (at level 8, format "''Under[' x ]", only printing). +End UNDER_REL. + +Module Export Under_rel : UNDER_REL. +Definition Under_rel (A : Type) (eqA : A -> A -> Prop) := + eqA. +Lemma Under_rel_from_rel : + forall (A : Type) (eqA : A -> A -> Prop) (x y : A), + @Under_rel A eqA x y -> eqA x y. +Proof. now trivial. Qed. +Lemma Under_relE (A : Type) (eqA : A -> A -> Prop) : + @Under_rel A eqA = eqA. +Proof. now trivial. Qed. +Definition Over_rel := Under_rel. +Lemma over_rel : + forall (A : Type) (eqA : A -> A -> Prop) (x y : A), + @Under_rel A eqA x y = @Over_rel A eqA x y. +Proof. now trivial. Qed. +Lemma over_rel_done : + forall (A : Type) (eqA : A -> A -> Prop) (EeqA : Reflexive eqA) (x : A), + @Over_rel A eqA x x. +Proof. now unfold Over_rel. Qed. +Lemma under_rel_done : + forall (A : Type) (eqA : A -> A -> Prop) (EeqA : Reflexive eqA) (x : A), + @Under_rel A eqA x x. +Proof. now trivial. Qed. +End Under_rel. diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg index 0adabb0673..9f6fe0e651 100644 --- a/plugins/ssr/ssrvernac.mlg +++ b/plugins/ssr/ssrvernac.mlg @@ -27,7 +27,6 @@ open Notation_ops open Notation_term open Glob_term open Stdarg -open Decl_kinds open Pp open Ppconstr open Printer @@ -105,7 +104,7 @@ GRAMMAR EXTEND Gram [ "if"; c = operconstr LEVEL "200"; "is"; db1 = ssr_dthen; b2 = ssr_else -> { let b1, ct, rt = db1 in CAst.make ~loc @@ CCases (MatchStyle, rt, [mk_pat c ct], [b1; b2]) } | "if"; c = operconstr LEVEL "200";"isn't";db1 = ssr_dthen; b2 = ssr_else -> - { let b1, ct, rt = db1 in + { let b1, ct, rt = db1 in let b1, b2 = let open CAst in let {loc=l1; v=(p1, r1)}, {loc=l2; v=(p2, r2)} = b1, b2 in (make ?loc:l1 (p1, r2), make ?loc:l2 (p2, r1)) @@ -148,7 +147,7 @@ END let declare_one_prenex_implicit locality f = let fref = - try Smartlocate.global_with_alias f + try Smartlocate.global_with_alias f with _ -> errorstrm (pr_qualid f ++ str " is not declared") in let rec loop = function | a :: args' when Impargs.is_status_implicit a -> @@ -280,7 +279,7 @@ let interp_search_notation ?loc tag okey = Feedback.msg_warning (hov 4 (qtag "In" ++ str "also occurs in " ++ pr_ntns')) end; ntn | [ntn] -> - Feedback.msg_info (hov 4 (qtag "In" ++ str "is part of notation " ++ pr_ntn ntn)); ntn + Feedback.msg_notice (hov 4 (qtag "In" ++ str "is part of notation " ++ pr_ntn ntn)); ntn | ntns' -> let e = str "occurs in" ++ spc() ++ pr_and_list pr_ntn ntns' in err (hov 4 (str "ambiguous: " ++ qtag "in" ++ e)) in @@ -298,7 +297,7 @@ let interp_search_notation ?loc tag okey = let rbody = glob_constr_of_notation_constr ?loc body in let m_body = hov 0 (Constrextern.without_symbols prl_glob_constr rbody) in let m = m_sc ++ pr_ntn ntn_pat ++ spc () ++ str "denotes " ++ m_body in - Feedback.msg_info (hov 0 m) in + Feedback.msg_notice (hov 0 m) in if List.length !scs > 1 then let scs' = List.remove (=) sc !scs in let w = pr_ntn ntn ++ str " is also defined " ++ pr_scs scs' in @@ -341,7 +340,7 @@ END (* Main type conclusion pattern filter *) -let rec splay_search_pattern na = function +let rec splay_search_pattern na = function | Pattern.PApp (fp, args) -> splay_search_pattern (na + Array.length args) fp | Pattern.PLetIn (_, _, _, bp) -> splay_search_pattern na bp | Pattern.PRef hr -> hr, na @@ -365,11 +364,11 @@ let coerce_search_pattern_to_sort hpat = if np < na then CErrors.user_err (Pp.str "too many arguments in head search pattern") else let hpat' = if np = na then hpat else mkPApp hpat (np - na) [||] in let warn () = - Feedback.msg_warning (str "Listing only lemmas with conclusion matching " ++ + Feedback.msg_warning (str "Listing only lemmas with conclusion matching " ++ pr_constr_pattern_env env sigma hpat') in if EConstr.isSort sigma ht then begin warn (); true, hpat' end else let filter_head, coe_path = - try + try let _, cp = Classops.lookup_path_to_sort_from (push_rels_assum dc env) sigma ht in warn (); @@ -465,7 +464,7 @@ let interp_modloc mr = let ssrdisplaysearch gr env t = let pr_res = pr_global gr ++ str ":" ++ spc () ++ pr_lconstr_env env Evd.empty t in - Feedback.msg_info (hov 2 pr_res ++ fnl ()) + Feedback.msg_notice (hov 2 pr_res ++ fnl ()) } @@ -560,7 +559,7 @@ END let print_view_hints env sigma kind l = let pp_viewname = str "Hint View" ++ pr_viewpos (Some kind) ++ str " " in let pp_hints = pr_list spc (pr_rawhintref env sigma) l in - Feedback.msg_info (pp_viewname ++ hov 0 pp_hints ++ Pp.cut ()) + Feedback.msg_notice (pp_viewname ++ hov 0 pp_hints ++ Pp.cut ()) } |