From 2df15a2c6e77d4afab8bf4d8387b7294db3d6d01 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Tue, 17 Mar 2026 08:19:32 +0100 Subject: [PATCH 01/11] Update comment --- lib/deprecation.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/deprecation.ml b/lib/deprecation.ml index 41ed5fd5cf78..ad1c81abc2b7 100644 --- a/lib/deprecation.ml +++ b/lib/deprecation.ml @@ -102,6 +102,6 @@ module Version = struct let v9_3 = get_generic_cat "9.3" (* When adding a new version here, please also add #[export] Set Warnings "-deprecated-since-X.Y". - in theories/Compat/RocqX{Y-1}.v *) + in theories/Corelib/Compat/RocqX{Y-1}.v *) end From 32259453768fa542fa40286996a4c741fc4da4ff Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Wed, 7 Jan 2026 10:28:42 +0100 Subject: [PATCH 02/11] [ssreflect] Cleanup old vim vars --- plugins/ssr/ssrparser.mlg | 2 -- plugins/ssr/ssrtacs.mlg | 2 -- plugins/ssr/ssrvernac.mlg | 2 -- 3 files changed, 6 deletions(-) diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index 57ccbf298144..7578b83eb112 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -1752,5 +1752,3 @@ module Internal = struct end } - -(* vim: set filetype=ocaml foldmethod=marker: *) diff --git a/plugins/ssr/ssrtacs.mlg b/plugins/ssr/ssrtacs.mlg index eb63b42f655b..ef00626ee8f0 100644 --- a/plugins/ssr/ssrtacs.mlg +++ b/plugins/ssr/ssrtacs.mlg @@ -1050,5 +1050,3 @@ TACTIC EXTEND under Ssrfwd.undertac ~pad_intro:true ist (Some [IPatAnon All]) arg h } END - -(* vim: set filetype=ocaml foldmethod=marker: *) diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg index d7995bd31af5..b3d1f80a7f2e 100644 --- a/plugins/ssr/ssrvernac.mlg +++ b/plugins/ssr/ssrvernac.mlg @@ -345,5 +345,3 @@ GRAMMAR EXTEND Gram [ IDENT "type"; "of"; c = Constr.constr -> { Tacexpr.ConstrTypeOf c }] ]; END - -(* vim: set filetype=ocaml foldmethod=marker: *) From 8a048a15b837b51e770245187a1ea5e5e24cfa66 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 19 Mar 2026 09:43:15 +0100 Subject: [PATCH 03/11] [ssreflect] Cleanup old compat code --- plugins/ssr/ssrvernac.mlg | 55 --------------------------------------- 1 file changed, 55 deletions(-) diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg index b3d1f80a7f2e..128dc66c199d 100644 --- a/plugins/ssr/ssrvernac.mlg +++ b/plugins/ssr/ssrvernac.mlg @@ -17,7 +17,6 @@ module CoqConstr = Constr open CoqConstr open Constrexpr open Constrexpr_ops -open Procq open Procq.Prim open Procq.Constr open Pvernac.Vernac_ @@ -291,57 +290,3 @@ VERNAC COMMAND EXTEND HintView CLASSIFIED AS SIDEFF | Some k -> Ssrview.AdaptorDb.declare k hints } END - -(** Search compatibility *) - -{ - -open G_vernac -} - -GRAMMAR EXTEND Gram - GLOBAL: query_command; - - query_command: TOP - [ [ IDENT "Search"; s = search_query; l = search_queries; "." -> - { let (sl,m) = l in - fun g -> - Vernacexpr.VernacSearch (Vernacexpr.Search (s::sl),g, m) } - ] ] -; -END - -(** Keyword compatibility fixes. *) - -(* Coq v8.1 notation uses "by" and "of" quasi-keywords, i.e., reserved *) -(* identifiers used as keywords. This is incompatible with ssreflect.v *) -(* which makes "by" and "of" true keywords, because of technicalities *) -(* in the internal lexer-parser API of Rocq. We patch this here by *) -(* adding new parsing rules that recognize the new keywords. *) -(* To make matters worse, the Rocq grammar for tactics fails to *) -(* export the non-terminals we need to patch. Fortunately, the CamlP5 *) -(* API provides a backdoor access (with loads of Obj.magic trickery). *) - -(* Coq v8.3 defines "by" as a keyword, some hacks are not needed any *) -(* longer and thus comment out. Such comments are marked with v8.3 *) - -{ - -open Pltac - -} - -GRAMMAR EXTEND Gram - GLOBAL: hypident; - hypident: TOP [ - [ "("; IDENT "type"; "of"; id = Prim.identref; ")" -> { id, Locus.InHypTypeOnly } - | "("; IDENT "value"; "of"; id = Prim.identref; ")" -> { id, Locus.InHypValueOnly } - ] ]; -END - -GRAMMAR EXTEND Gram - GLOBAL: constr_eval; - constr_eval: TOP [ - [ IDENT "type"; "of"; c = Constr.constr -> { Tacexpr.ConstrTypeOf c }] - ]; -END From db2107cbb5d586999fbd323465c148dfd5f1d742 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 19 Mar 2026 10:13:30 +0100 Subject: [PATCH 04/11] [ssreflect] Update outdated comment --- plugins/ssr/ssrparser.mlg | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index 7578b83eb112..a23cfbe34fee 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -43,14 +43,11 @@ open Libobject (** Ssreflect load check. *) -(* To allow ssrcoq to be fully compatible with the "plain" Rocq, we only *) +(* To allow ssrcoq to be fully compatible with the "plain" Rocq, we only*) (* turn on its incompatible features (the new rewrite syntax, and the *) (* reserved identifiers) when the theory library (ssreflect.v) has *) -(* has actually been required, or is being defined. Because this check *) -(* needs to be done often (for each identifier lookup), we implement *) -(* some caching, repeating the test only when the environment changes. *) -(* We check for protect_term because it is the first constant loaded; *) -(* ssr_have would ultimately be a better choice. *) +(* has actually been imported. This is done thanks to the "SSR Loaded" *) +(* option. *) let is_ssr_loaded = Pptactic.ssr_loaded From 139adb2321bf9f07be8c409b57bd7cbf60688b23 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 19 Mar 2026 09:39:23 +0100 Subject: [PATCH 05/11] =?UTF-8?q?[ssreflect]=20Use=20=E2=80=97=20instead?= =?UTF-8?q?=20of=20=5F=20for=20reserved=20identifiers?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Using double-low-line rather than underscore, i.e., `‗foo‗` instead of `_foo_`, will cause less conflicts and is not an issue since, by definition, we never type these identifiers by hand. --- clib/unicode.ml | 1 + .../proof-engine/ssreflect-proof-language.rst | 13 ------ plugins/ssr/ssrcommon.ml | 45 ++++++++++--------- plugins/ssr/ssrcommon.mli | 3 ++ plugins/ssr/ssrparser.mlg | 36 +++++---------- 5 files changed, 41 insertions(+), 57 deletions(-) diff --git a/clib/unicode.ml b/clib/unicode.ml index 266059bd5e7a..6465e399de2d 100644 --- a/clib/unicode.ml +++ b/clib/unicode.ml @@ -122,6 +122,7 @@ let classify = mk_lookup_table_from_unicode_tables_for IdentSep [ single 0x005F; (* Underscore. *) + single 0x2017; (* Double low line. *) single 0x00A0; (* Non breaking space, overrides Sep *) ]; mk_lookup_table_from_unicode_tables_for IdentPart diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index f947b7a21f29..084877a27cf3 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -121,8 +121,6 @@ compatible with the rest of Rocq, up to a few discrepancies. + New tactic(al)s names (:tacn:`last`, :tacn:`done`, :tacn:`have`, :tacn:`suffices`, :tacn:`suff`, :tacn:`without loss`, :tacn:`wlog`, :tacn:`congr`, :tacn:`unlock`) might clash with user tactic names. -+ Identifiers with both leading and trailing ``_``, such as ``_x_``, are - reserved by |SSR| and cannot appear in scripts. + The extensions to the :tacn:`rewrite` tactic are partly incompatible with those available in current versions of Rocq; in particular, ``rewrite .. in (type of k)`` or ``rewrite .. in *`` or any other variant of :tacn:`rewrite` @@ -165,17 +163,6 @@ compatible with the rest of Rocq, up to a few discrepancies. Controls whether the incompatible rewrite syntax is enabled (the default). Disabling the :term:`flag` makes the syntax compatible with other parts of Rocq. -.. flag:: SsrIdents - - Controls whether tactics can refer to |SSR|-generated variables that are - in the form _xxx_. Scripts with explicit references to such variables - are fragile; they are prone to failure if the proof is later modified or - if the details of variable name generation change in future releases of Rocq. - - The default is on, which gives an error message when the user tries to - create such identifiers. Disabling the :term:`flag` generates a warning instead, - increasing compatibility with other parts of Rocq. - Gallina extensions -------------------- diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index b8f390ca7e57..bfbad25e5cc8 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -251,7 +251,7 @@ let add_internal_name pt = internal_names := pt :: !internal_names let is_internal_name s = List.exists (fun p -> p s) !internal_names let mk_internal_id s = - let s' = Printf.sprintf "_%s_" s in + let s' = Printf.sprintf "‗%s‗" s in let s' = String.map (fun c -> if c = ' ' then '_' else c) s' in add_internal_name ((=) s'); Id.of_string s' @@ -262,19 +262,22 @@ let skip_digits s = 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) +let mk_tagged_id t i = Id.of_string (Printf.sprintf "%s%d‗" t i) +(* [is_dll s n] test if character at pos [n] of [s] is UTF8 double low line '‗'. + Assumes [n] <= [String.length n - 3]. *) +let is_dll s n = s.[n] = '\226' && s.[n+1] = '\128' && s.[n+2] = '\151' let is_tagged t s = - let n = String.length s - 1 and m = String.length t in - m < n && s.[n] = '_' && same_prefix s t m && skip_digits s m = n + let n = String.length s and m = String.length t in + m < n - 3 && is_dll s (n - 3) && same_prefix s t m && skip_digits s m = n - 3 -let evar_tag = "_evar_" +let evar_tag = "‗evar_" let _ = add_internal_name (is_tagged evar_tag) let mk_evar_name n = Name (mk_tagged_id evar_tag n) let ssr_anon_hyp = "Hyp" -let wildcard_tag = "_the_" -let wildcard_post = "_wildcard_" +let wildcard_tag = "‗the_" +let wildcard_post = "_wildcard‗" 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 @@ -283,19 +286,19 @@ let has_wildcard_tag s = skip_digits s m = n - m' - 2 let _ = add_internal_name has_wildcard_tag -let discharged_tag = "_discharged_" +let discharged_tag = "‗discharged_" let mk_discharged_id id = - Id.of_string (Printf.sprintf "%s%s_" discharged_tag (Id.to_string id)) + Id.of_string (Printf.sprintf "%s%s‗" discharged_tag (Id.to_string id)) let has_discharged_tag s = - let m = String.length discharged_tag and n = String.length s - 1 in - m < n && s.[n] = '_' && same_prefix s discharged_tag m + let m = String.length discharged_tag and n = String.length s in + m < n - 3 && is_dll s (n - 3) && same_prefix s discharged_tag m let _ = add_internal_name has_discharged_tag let is_discharged_id id = has_discharged_tag (Id.to_string id) let max_suffix m (t, j0 as tj0) id = - let s = Id.to_string id in let n = String.length s - 1 in - let dn = String.length t - 1 - n in let i0 = j0 - dn in - if not (i0 >= m && s.[n] = '_' && same_prefix s t m) then tj0 else + let s = Id.to_string id in let n = String.length s - 3 in + let dn = String.length t - 3 - n in let i0 = j0 - dn in + if not (i0 >= m && is_dll s n && same_prefix s t m) then tj0 else let rec loop i = if i < i0 && s.[i] = '0' then loop (i + 1) else if (if i < i0 then skip_digits s i = n else le_s_t i) then s, i else tj0 @@ -309,9 +312,9 @@ let max_suffix m (t, j0 as tj0) id = let mk_anon_id t gl_ids = let gl_ids = List.map NamedDecl.get_id (EConstr.named_context_of_val gl_ids) in let m, si0, id0 = - let s = ref (Printf.sprintf "_%s_" t) in - if is_internal_name !s then s := "_" ^ !s; - let n = String.length !s - 1 in + let s = ref (Printf.sprintf "‗%s‗" t) in + if is_internal_name !s then s := "‗" ^ !s; + let n = String.length !s - 3 in let rec loop i j = let d = !s.[i] in if not (is_digit d) then i + 1, j else loop (i - 1) (if d = '0' then j else i) in @@ -320,10 +323,12 @@ let mk_anon_id t gl_ids = let s, i = List.fold_left (max_suffix m) si0 gl_ids in let open Bytes in let s = of_string s in - let n = length s - 1 in + let n = length s - 3 in + let cat_dll s = + set s (n + 1) '\226'; set s (n + 2) '\128'; cat s (of_string "\151") in let rec loop i = if get s i = '9' then (set s i '0'; loop (i - 1)) else - if i < m then (set s n '0'; set s m '1'; cat s (of_string "_")) else + if i < m then (set s n '0'; set s m '1'; cat_dll s) else (set s i (Char.chr (Char.code (get s i) + 1)); s) in Id.of_string_soft (Bytes.to_string (loop (n - 1))) @@ -551,7 +556,7 @@ let nb_evar_deps = function let s = Id.to_string id in if not (is_tagged evar_tag s) then 0 else let m = String.length evar_tag in - (try int_of_string (String.sub s m (String.length s - 1 - m)) with e when CErrors.noncritical e -> 0) + (try int_of_string (String.sub s m (String.length s - 3 - m)) with e when CErrors.noncritical e -> 0) | _ -> 0 let type_id env sigma t = Id.of_string (Namegen.hdchar env sigma t) diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli index eb0de8cda3d8..309fd844cd7f 100644 --- a/plugins/ssr/ssrcommon.mli +++ b/plugins/ssr/ssrcommon.mli @@ -149,6 +149,9 @@ val mkSsrConst : Environ.env -> Evd.evar_map -> string -> Evd.evar_map * EConstr val is_discharged_id : Id.t -> bool val mk_discharged_id : Id.t -> Id.t +(* [is_dll s n] test if character at pos [n] of [s] is UTF8 double low line '‗'. + Assumes [n] < [String.length n - 3]. *) +val is_dll : string -> int -> bool val is_tagged : string -> string -> bool val has_discharged_tag : string -> bool val ssrqid : string -> Libnames.qualid diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index a23cfbe34fee..d414a5faa150 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -44,10 +44,9 @@ open Libobject (** Ssreflect load check. *) (* To allow ssrcoq to be fully compatible with the "plain" Rocq, we only*) -(* turn on its incompatible features (the new rewrite syntax, and the *) -(* reserved identifiers) when the theory library (ssreflect.v) has *) -(* has actually been imported. This is done thanks to the "SSR Loaded" *) -(* option. *) +(* turn on its incompatible features (the new rewrite syntax) when the *) +(* theory library (ssreflect.v) has actually been imported. *) +(* This is done thanks to the "SSR Loaded" option. *) let is_ssr_loaded = Pptactic.ssr_loaded @@ -1623,31 +1622,20 @@ let ltac_expr = Pltac.ltac_expr (* Since Rocq now does repeated internal checks of its external lexical *) (* rules, we now need to carve ssreflect reserved identifiers out of *) -(* out of the user namespace. We use identifiers of the form _id_ for *) -(* this purpose, e.g., we "anonymize" an identifier id as _id_, adding *) -(* an extra leading _ if this might clash with an internal identifier. *) -(* We check for ssreflect identifiers in the ident grammar rule; *) -(* when the ssreflect Module is present this is normally an error, *) -(* but we provide a compatibility flag to reduce this to a warning. *) +(* the user namespace. We use identifiers of the form ‗id‗ for *) +(* this purpose, e.g., we "anonymize" an identifier id as ‗id‗, adding *) +(* an extra leading ‗ if this might clash with an internal identifier. *) +(* We check for ssreflect identifiers in the ident grammar rule. *) { -let { Goptions.get = ssr_reserved_ids } = - Goptions.declare_bool_option_and_ref ~stage:Synterp ~key:["SsrIdents"] ~value:true () - let is_ssr_reserved s = - let n = String.length s in n > 2 && s.[0] = '_' && s.[n - 1] = '_' + let n = String.length s in n > 6 && is_dll s 0 && is_dll s (n - 3) let ssr_id_of_string loc s = - if is_ssr_reserved s && is_ssr_loaded () then begin - if ssr_reserved_ids() then - CErrors.user_err ~loc (str ("The identifier " ^ s ^ " is reserved.")) - else if is_internal_name s then - Feedback.msg_warning (str ("Conflict between " ^ s ^ " and ssreflect internal names.")) - else Feedback.msg_warning (str ( - "The name " ^ s ^ " fits the _xxx_ format used for anonymous variables.\n" - ^ "Scripts with explicit references to anonymous variables are fragile.")) - end; Id.of_string s + if is_ssr_reserved s then begin + CErrors.user_err ~loc (str ("The identifier " ^ s ^ " is reserved.")) + end; Id.of_string s let ssr_null_entry = Procq.Entry.(of_parser "ssr_null" { parser_fun = fun _ _ -> Ok () }) @@ -1660,7 +1648,7 @@ END { -let perm_tag = "_perm_Hyp_" +let perm_tag = "‗perm_Hyp_" let _ = add_internal_name (is_tagged perm_tag) } From 3d594176ef918d8bfbc48ad870448ba17adeeb8a Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 19 Mar 2026 10:25:58 +0100 Subject: [PATCH 06/11] [ssreflect] Rename SSR Loaded to SSRRewriteLoaded --- plugins/ltac/pptactic.ml | 6 +++--- plugins/ltac/pptactic.mli | 2 +- plugins/ssr/ssrparser.mlg | 6 +++--- plugins/ssr/ssrparser.mli | 2 +- plugins/ssr/ssrtacs.mlg | 2 +- theories/Corelib/ssr/ssreflect.v | 4 ++-- 6 files changed, 11 insertions(+), 11 deletions(-) diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 46a68fa762e7..b3575c44833c 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -500,10 +500,10 @@ let string_of_genarg_arg (ArgumentType arg) = (* When the [ssreflect.SsrSynax] module is imported, ssreflect operates in reduced compatibility mode. During printing, we try to account for this when this module is imported. *) -let { Goptions.get = ssr_loaded } = - Goptions.declare_bool_option_and_ref ~stage:Synterp ~key:["SSR";"Loaded"] ~value:false () +let { Goptions.get = ssr_rewrite_loaded } = + Goptions.declare_bool_option_and_ref ~stage:Synterp ~key:["SSRRewriteLoaded"] ~value:false () - let pr_orient b = if b then if ssr_loaded () then str "-> " else mt () else str "<- " + let pr_orient b = if b then if ssr_rewrite_loaded () then str "-> " else mt () else str "<- " let pr_multi = let open Equality in function | Precisely 1 -> mt () diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index 0f7602d255bb..5dfe18498fb7 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -164,7 +164,7 @@ val ltop : entry_relative_level val make_constr_printer : (env -> Evd.evar_map -> entry_relative_level -> 'a -> Pp.t) -> 'a Genprint.top_printer -val ssr_loaded : unit -> bool +val ssr_rewrite_loaded : unit -> bool module Internal : sig val pr_tacvalue_ref : (env -> Tacarg.tacvalue -> Pp.t) ref diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index d414a5faa150..4cf14fa7fd5d 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -46,9 +46,9 @@ open Libobject (* To allow ssrcoq to be fully compatible with the "plain" Rocq, we only*) (* turn on its incompatible features (the new rewrite syntax) when the *) (* theory library (ssreflect.v) has actually been imported. *) -(* This is done thanks to the "SSR Loaded" option. *) +(* This is done thanks to the "SSRRewriteLoaded" option. *) -let is_ssr_loaded = Pptactic.ssr_loaded +let is_ssr_rewrite_loaded = Pptactic.ssr_rewrite_loaded } @@ -1725,7 +1725,7 @@ module Internal = struct let pr_intros = pr_intros let pr_view = pr_view let pr_mult = pr_mult - let is_ssr_loaded = is_ssr_loaded + let is_ssr_rewrite_loaded = is_ssr_rewrite_loaded let pr_hpats = pr_hpats let pr_fwd = pr_fwd let pr_hint = pr_hint diff --git a/plugins/ssr/ssrparser.mli b/plugins/ssr/ssrparser.mli index a1d177156e4a..6ae33a82c73d 100644 --- a/plugins/ssr/ssrparser.mli +++ b/plugins/ssr/ssrparser.mli @@ -188,7 +188,7 @@ module Internal : sig val pr_mult : ssrmult -> Pp.t - val is_ssr_loaded : unit -> bool + val is_ssr_rewrite_loaded : unit -> bool val pr_hpats : ssrhpats -> Pp.t diff --git a/plugins/ssr/ssrtacs.mlg b/plugins/ssr/ssrtacs.mlg index ef00626ee8f0..5f7e899f857d 100644 --- a/plugins/ssr/ssrtacs.mlg +++ b/plugins/ssr/ssrtacs.mlg @@ -758,7 +758,7 @@ let lbrace = Char.chr 123 let test_ssr_rw_syntax = let test kwstate strm = if not !ssr_rw_syntax then Error () else - if is_ssr_loaded () then Ok () else + if is_ssr_rewrite_loaded () then Ok () else match LStream.peek_nth kwstate 0 strm with | Some (Tok.KEYWORD key) when List.mem key.[0] [lbrace; '['; '/'] -> Ok () | _ -> Error () in diff --git a/theories/Corelib/ssr/ssreflect.v b/theories/Corelib/ssr/ssreflect.v index 0b36894e488d..4770682bd3e1 100644 --- a/theories/Corelib/ssr/ssreflect.v +++ b/theories/Corelib/ssr/ssreflect.v @@ -86,8 +86,8 @@ Module SsrSyntax. Reserved Notation "(* x 'is' y 'of' z 'isn't' // /= //= *)". -(** Enable SSR features **) -#[export] Set SSR Loaded. +(** Enable SSR rewrite compat **) +#[export] Set SSRRewriteLoaded. Reserved Notation "" (at level 0, n at level 0, format ""). From 3d24d7ada30c608bc0626c3d592e312502eda49f Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 20 Mar 2026 08:07:58 +0100 Subject: [PATCH 07/11] [ssreflect] Use tactic name 'rw' instead of 'rewrite' Since this was the major cause of conflict with legacy tactics, ssreflect can now be loaded in the Prelude. For backward compatibility From Corelib Require Import ssreflect. still loads a 'rewrite' wrapper to 'rw'. This compatibility layer also includes the `if _ is _ then _ else _` and the `if _ isn't _ then _ else _` notations. --- doc/Makefile.docgram | 2 +- doc/corelib/index-list.html.template | 1 + plugins/ssr/ssrparser.mlg | 12 +- plugins/ssr/ssrparser.mli | 2 - plugins/ssr/ssrtacs.mlg | 34 +- plugins/ssr/ssrtacs.mli | 2 + plugins/ssr/ssrvernac.mlg | 22 +- plugins/ssrrewrite/dune | 11 + plugins/ssrrewrite/ssrrewrite.mlg | 130 ++++++ plugins/ssrrewrite/ssrrewrite.mli | 0 test-suite/bugs/bug_4966.v | 2 +- theories/Corelib/ssr/ssreflect.v | 643 +-------------------------- theories/Corelib/ssr/ssreflect_rw.v | 643 +++++++++++++++++++++++++++ 13 files changed, 812 insertions(+), 692 deletions(-) create mode 100644 plugins/ssrrewrite/dune create mode 100644 plugins/ssrrewrite/ssrrewrite.mlg create mode 100644 plugins/ssrrewrite/ssrrewrite.mli create mode 100644 theories/Corelib/ssr/ssreflect_rw.v diff --git a/doc/Makefile.docgram b/doc/Makefile.docgram index e78384058722..5f158279158a 100644 --- a/doc/Makefile.docgram +++ b/doc/Makefile.docgram @@ -38,7 +38,7 @@ REAL_DOC_MLGS := $(wildcard */*.mlg plugins/*/*.mlg) # omit SSR MLGS and chapter for now SSR_MLGS := \ plugins/ssr/ssrparser.mlg plugins/ssr/ssrtacs.mlg plugins/ssr/ssrvernac.mlg \ - plugins/ssrmatching/g_ssrmatching.mlg + plugins/ssrmatching/g_ssrmatching.mlg plugins/ssrrewrite/ssrrewrite.mlg REAL_DOC_MLGS := $(filter-out $(SSR_MLGS),$(REAL_DOC_MLGS)) SSR_RSTS := doc/sphinx/proof-engine/ssreflect-proof-language.rst DOC_RSTS := $(filter-out $(SSR_RSTS),$(DOC_RSTS)) diff --git a/doc/corelib/index-list.html.template b/doc/corelib/index-list.html.template index 6923703a666c..43b5d3498687 100644 --- a/doc/corelib/index-list.html.template +++ b/doc/corelib/index-list.html.template @@ -113,6 +113,7 @@ through the Require Import command.

theories/Corelib/ssrmatching/ssrmatching.v theories/Corelib/ssr/ssrclasses.v + theories/Corelib/ssr/ssreflect_rw.v theories/Corelib/ssr/ssreflect.v theories/Corelib/ssr/ssrbool.v theories/Corelib/ssr/ssrfun.v diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index 4cf14fa7fd5d..3ab565e3dd48 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -41,15 +41,6 @@ open Ssrequality open Ssripats open Libobject -(** Ssreflect load check. *) - -(* To allow ssrcoq to be fully compatible with the "plain" Rocq, we only*) -(* turn on its incompatible features (the new rewrite syntax) when the *) -(* theory library (ssreflect.v) has actually been imported. *) -(* This is done thanks to the "SSRRewriteLoaded" option. *) - -let is_ssr_rewrite_loaded = Pptactic.ssr_rewrite_loaded - } DECLARE PLUGIN "rocq-runtime.plugins.ssreflect" @@ -1579,7 +1570,7 @@ END { let sq_brace_tacnames = - ["first"; "solve"; "do"; "rewrite"; "have"; "suffices"; "wlog"] + ["first"; "solve"; "do"; "rewrite"; "rw"; "have"; "suffices"; "wlog"] (* "by" is a keyword *) let test_ssrseqvar = @@ -1725,7 +1716,6 @@ module Internal = struct let pr_intros = pr_intros let pr_view = pr_view let pr_mult = pr_mult - let is_ssr_rewrite_loaded = is_ssr_rewrite_loaded let pr_hpats = pr_hpats let pr_fwd = pr_fwd let pr_hint = pr_hint diff --git a/plugins/ssr/ssrparser.mli b/plugins/ssr/ssrparser.mli index 6ae33a82c73d..04d1096784b5 100644 --- a/plugins/ssr/ssrparser.mli +++ b/plugins/ssr/ssrparser.mli @@ -188,8 +188,6 @@ module Internal : sig val pr_mult : ssrmult -> Pp.t - val is_ssr_rewrite_loaded : unit -> bool - val pr_hpats : ssrhpats -> Pp.t val pr_fwd : (Ssrast.ssrfwdkind * Ssrast.ssrbindfmt list) * Ssrast.ast_closure_term -> Pp.t diff --git a/plugins/ssr/ssrtacs.mlg b/plugins/ssr/ssrtacs.mlg index 5f7e899f857d..64e86faad268 100644 --- a/plugins/ssr/ssrtacs.mlg +++ b/plugins/ssr/ssrtacs.mlg @@ -740,41 +740,15 @@ let pr_ssrrwargs _ _ _ rwargs = pr_list spc pr_rwarg rwargs ARGUMENT EXTEND ssrrwargs TYPED AS ssrrwarg list PRINTED BY { pr_ssrrwargs } END -{ - -let ssr_rw_syntax = Summary.ref ~name:"SSR:rewrite" true - -let () = - Goptions.(declare_bool_option - { optstage = Summary.Stage.Synterp; - optkey = ["SsrRewrite"]; - optread = (fun _ -> !ssr_rw_syntax); - optdepr = None; - optwrite = (fun b -> ssr_rw_syntax := b) }) - -let lbrace = Char.chr 123 -(** Workaround to a limitation of coqpp *) - -let test_ssr_rw_syntax = - let test kwstate strm = - if not !ssr_rw_syntax then Error () else - if is_ssr_rewrite_loaded () then Ok () else - match LStream.peek_nth kwstate 0 strm with - | Some (Tok.KEYWORD key) when List.mem key.[0] [lbrace; '['; '/'] -> Ok () - | _ -> Error () in - Procq.Entry.(of_parser "test_ssr_rw_syntax" { parser_fun = test }) - -} - GRAMMAR EXTEND Gram GLOBAL: ssrrwargs; - ssrrwargs: TOP [[ test_ssr_rw_syntax; a = LIST1 ssrrwarg -> { a } ]]; + ssrrwargs: TOP [[ a = LIST1 ssrrwarg -> { a } ]]; END -(** The "rewrite" tactic *) +(** The "rw" tactic *) -TACTIC EXTEND ssrrewrite - | [ "rewrite" ssrrwargs(args) ssrclauses(clauses) ] -> +TACTIC EXTEND ssrrw + | [ "rw" ssrrwargs(args) ssrclauses(clauses) ] -> { tclCLAUSES (ssrrewritetac ist args) clauses } END diff --git a/plugins/ssr/ssrtacs.mli b/plugins/ssr/ssrtacs.mli index 4069c40ae277..062f2c1c2d43 100644 --- a/plugins/ssr/ssrtacs.mli +++ b/plugins/ssr/ssrtacs.mli @@ -10,6 +10,8 @@ open Ssrparser val wit_ssrarg : ssrarg Genarg.uniform_genarg_type val wit_ssrrwarg : ssrrwarg Genarg.uniform_genarg_type +val ssrrwargs : ssrrwarg list Procq.Entry.t +val pr_ssrrwargs : 'a -> 'b -> 'c -> ssrrwarg list -> Pp.t val wit_ssrrwargs : ssrrwarg list Genarg.uniform_genarg_type val wit_ssrseqdir : ssrdir Genarg.uniform_genarg_type diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg index 128dc66c199d..ccd46159c1d5 100644 --- a/plugins/ssr/ssrvernac.mlg +++ b/plugins/ssr/ssrvernac.mlg @@ -46,8 +46,6 @@ IGNORE KEYWORDS (** Alternative notations for "match" and anonymous arguments. *)(* ************) (* Syntax: *) -(* if is then ... else ... *) -(* if is [in ..] return ... then ... else ... *) (* let: := in ... *) (* let: [in ...] := return ... in ... *) (* The scope of a top-level 'as' in the pattern extends over the *) @@ -75,7 +73,6 @@ let aliasvar = function let mk_cnotype mp = aliasvar mp, None let mk_ctype mp t = aliasvar mp, Some t let mk_rtype t = Some t -let mk_dthen ?loc (mp, ct, rt) c = (CAst.make ?loc (mp, c)), ct, rt let mk_let ?loc rt ct mp c1 = CAst.make ?loc @@ CCases (LetPatternStyle, rt, ct, [CAst.make ?loc (mp, c1)]) let mk_pat c (na, t) = (c, na, t) @@ -86,25 +83,8 @@ GRAMMAR EXTEND Gram GLOBAL: term; ssr_rtype: [[ "return"; t = term LEVEL "100" -> { mk_rtype t } ]]; ssr_mpat: [[ p = pattern -> { [[p]] } ]]; - ssr_dpat: [ - [ mp = ssr_mpat; "in"; t = pattern; rt = ssr_rtype -> { mp, mk_ctype mp t, rt } - | mp = ssr_mpat; rt = ssr_rtype -> { mp, mk_cnotype mp, rt } - | mp = ssr_mpat -> { mp, no_ct, no_rt } - ] ]; - ssr_dthen: [[ dp = ssr_dpat; "then"; c = lconstr -> { mk_dthen ~loc dp c } ]]; - ssr_elsepat: [[ "else" -> { [[CAst.make ~loc @@ CPatAtom None]] } ]]; - ssr_else: [[ mp = ssr_elsepat; c = lconstr -> { CAst.make ~loc (mp, c) } ]]; term: LEVEL "10" [ - [ "if"; c = term 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 = term LEVEL "200";"isn't";db1 = ssr_dthen; b2 = ssr_else -> - { 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)) - in - CAst.make ~loc @@ CCases (MatchStyle, rt, [mk_pat c ct], [b1; b2]) } - | "let"; ":"; mp = ssr_mpat; ":="; c = lconstr; "in"; c1 = lconstr -> + [ "let"; ":"; mp = ssr_mpat; ":="; c = lconstr; "in"; c1 = lconstr -> { mk_let ~loc no_rt [mk_pat c no_ct] mp c1 } | "let"; ":"; mp = ssr_mpat; ":="; c = lconstr; rt = ssr_rtype; "in"; c1 = lconstr -> diff --git a/plugins/ssrrewrite/dune b/plugins/ssrrewrite/dune new file mode 100644 index 000000000000..55f94c46ba44 --- /dev/null +++ b/plugins/ssrrewrite/dune @@ -0,0 +1,11 @@ +(library + (name ssreflect_rewrite_plugin) + (public_name rocq-runtime.plugins.ssreflect_rewrite) + (synopsis "Rocq's ssreflect plugin for rewrite compatibility") + (flags :standard -open Gramlib) + (libraries rocq-runtime.plugins.ssrmatching rocq-runtime.plugins.ssreflect)) + +(rule + (targets ssrrewrite.ml) + (deps (:mlg ssrrewrite.mlg)) + (action (chdir %{project_root} (run rocq pp-mlg %{deps})))) diff --git a/plugins/ssrrewrite/ssrrewrite.mlg b/plugins/ssrrewrite/ssrrewrite.mlg new file mode 100644 index 000000000000..c6d7feb5423a --- /dev/null +++ b/plugins/ssrrewrite/ssrrewrite.mlg @@ -0,0 +1,130 @@ +(************************************************************************) +(* * The Rocq Prover / The Rocq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* !ssr_rewrite_syntax); + optdepr = None; + optwrite = (fun b -> ssr_rewrite_syntax := b) }) + +let lbrace = Char.chr 123 +(** Workaround to a limitation of coqpp *) + +let test_ssr_rewrite_syntax = + let test kwstate strm = + if not !ssr_rewrite_syntax then Error () else + if Pptactic.ssr_rewrite_loaded () then Ok () else + match LStream.peek_nth kwstate 0 strm with + | Some (Tok.KEYWORD key) when List.mem key.[0] [lbrace; '['; '/'] -> Ok () + | _ -> Error () in + Procq.Entry.(of_parser "test_ssr_rewrite_syntax" { parser_fun = test }) + +} + +GRAMMAR EXTEND Gram + GLOBAL: ssrrewriteargs; + ssrrewriteargs: TOP [[ test_ssr_rewrite_syntax; a = ssrrwargs -> { a } ]]; +END + +(** The "rewrite" tactic *) + +TACTIC EXTEND ssrrewrite + | [ "rewrite" ssrrewriteargs(args) ssrclauses(clauses) ] -> + { tclCLAUSES (ssrrewritetac ist args) clauses } +END + +{ + +(* global syntactic changes and vernacular commands *) + +(** Alternative notations for "match" and anonymous arguments. *)(* ************) + +(* Syntax: *) +(* if is then ... else ... *) +(* if is [in ..] return ... then ... else ... *) +(* The scope of a top-level 'as' in the pattern extends over the *) +(* 'return' type (dependent if/let). *) +(* in b (*^--ALTERNATIVE INNER LET--------^ *) *) + +(* Caveat : There is no pretty-printing support, since this would *) +(* require a modification to the Rocq kernel (adding a new match *) +(* display style -- why aren't these strings?); also, the v8.1 *) +(* pretty-printer only allows extension hooks for printing *) +(* integer or string literals. *) +(* Also note that in the v8 grammar "is" needs to be a keyword; *) +(* as this can't be done from an ML extension file, the new *) +(* syntax will only work when ssreflect.v is imported. *) + +let no_ct = None, None and no_rt = None +let aliasvar = function + | [[{ CAst.v = CPatAlias (_, na); loc }]] -> Some na + | _ -> None +let mk_cnotype mp = aliasvar mp, None +let mk_ctype mp t = aliasvar mp, Some t +let mk_rtype t = Some t +let mk_dthen ?loc (mp, ct, rt) c = (CAst.make ?loc (mp, c)), ct, rt +let mk_pat c (na, t) = (c, na, t) + +} + +GRAMMAR EXTEND Gram + GLOBAL: term; + ssr_rtype: [[ "return"; t = term LEVEL "100" -> { mk_rtype t } ]]; + ssr_mpat: [[ p = pattern -> { [[p]] } ]]; + ssr_dpat: [ + [ mp = ssr_mpat; "in"; t = pattern; rt = ssr_rtype -> { mp, mk_ctype mp t, rt } + | mp = ssr_mpat; rt = ssr_rtype -> { mp, mk_cnotype mp, rt } + | mp = ssr_mpat -> { mp, no_ct, no_rt } + ] ]; + ssr_dthen: [[ dp = ssr_dpat; "then"; c = lconstr -> { mk_dthen ~loc dp c } ]]; + ssr_elsepat: [[ "else" -> { [[CAst.make ~loc @@ CPatAtom None]] } ]]; + ssr_else: [[ mp = ssr_elsepat; c = lconstr -> { CAst.make ~loc (mp, c) } ]]; + term: LEVEL "10" [ + [ "if"; c = term 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 = term LEVEL "200";"isn't";db1 = ssr_dthen; b2 = ssr_else -> + { 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)) + in + CAst.make ~loc @@ CCases (MatchStyle, rt, [mk_pat c ct], [b1; b2]) } + ] ]; +END diff --git a/plugins/ssrrewrite/ssrrewrite.mli b/plugins/ssrrewrite/ssrrewrite.mli new file mode 100644 index 000000000000..e69de29bb2d1 diff --git a/test-suite/bugs/bug_4966.v b/test-suite/bugs/bug_4966.v index 16dc0d113efc..05e93431c59b 100644 --- a/test-suite/bugs/bug_4966.v +++ b/test-suite/bugs/bug_4966.v @@ -1,7 +1,7 @@ (* Interpretation of auto as an argument of an ltac function (i.e. as an ident) was wrongly "auto with *" *) Axiom proof_admitted : False. -#[export] Hint Extern 0 => case proof_admitted : unused. +#[export] Hint Extern 0 => (case proof_admitted) : unused. Ltac do_tac tac := tac. Goal False. diff --git a/theories/Corelib/ssr/ssreflect.v b/theories/Corelib/ssr/ssreflect.v index 4770682bd3e1..284e34b14631 100644 --- a/theories/Corelib/ssr/ssreflect.v +++ b/theories/Corelib/ssr/ssreflect.v @@ -8,103 +8,29 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) +Require Export ssreflect_rw. +Declare ML Module "rocq-runtime.plugins.ssreflect_rewrite". -(** ## **) +Module SsrIsSyntax. -Require Import ssrmatching. -Declare ML Module "rocq-runtime.plugins.ssreflect". +(** Declare Ssr keywords: "is" "isn't". **) +Reserved Notation "(******* x 'is' y 'isn't' *******)". -(** - This file is the Gallina part of the ssreflect plugin implementation. - Files that use the ssreflect plugin should always Require ssreflect and - either Import ssreflect or Import ssreflect.SsrSyntax. - Part of the contents of this file is technical and will only interest - advanced developers; in addition the following are defined: - #[#the str of v by f#]# == the Canonical s : str such that f s = v. - #[#the str of v#]# == the Canonical s : str that coerces to v. - 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 - rewrite multirule). - unkeyed t == t, but treated as an unkeyed matching pattern by - the ssreflect matching algorithm. - nosimpl t == t, but on the right-hand side of Definition C := - nosimpl disables expansion of C by /=. - locked t == t, but locked t is not convertible to t. - locked_with k t == t, but not convertible to t or locked_with k' t - unless k = k' (with k : unit). Rocq type-checking - will be much more efficient if locked_with with a - bespoke k is used for sealed definitions. - unlockable v == interface for sealed constant definitions of v. - Unlockable def == the unlockable that registers def : C = v. - #[#unlockable of C#]# == a clone for C of the canonical unlockable for the - definition of C (e.g., if it uses locked_with). - #[#unlockable fun C#]# == #[#unlockable of C#]# with the expansion forced to be - an explicit lambda expression. - -> The usage pattern for ADT operations is: - Definition foo_def x1 .. xn := big_foo_expression. - Fact foo_key : unit. Proof. by #[# #]#. Qed. - Definition foo := locked_with foo_key foo_def. - Canonical foo_unlockable := #[#unlockable fun foo#]#. - This minimizes the comparison overhead for foo, while still allowing - rewrite unlock to expose big_foo_expression. - - #[#elaborate x#]# == triggers Rocq elaboration to fill the holes of the term x - The main use case is to trigger typeclass inference in - the body of a ssreflect have := #[#elaborate body#]#. - - Additionally we provide default intro pattern ltac views: - - top of the stack actions: - => /#[#apply#]# := => hyp {}/hyp - => /#[#swap#]# := => x y; move: y x - (also swap and preserves let bindings) - => /#[#dup#]# := => x; have copy := x; move: copy x - (also copies and preserves let bindings) - - calling rewrite from an intro pattern, use with parsimony: - => /#[#1! rules#]# := rewrite rules - => /#[#! rules#]# := rewrite !rules - - More information about these definitions and their use can be found in the - ssreflect manual, and in specific comments below. **) +End SsrIsSyntax. -Set Implicit Arguments. -Unset Strict Implicit. -Unset Printing Implicit Defensive. +Export SsrIsSyntax. -Module SsrSyntax. - -(** Declare Ssr keywords: "is" "isn't" "of" "//" "/=" and "//=". **) - -Reserved Notation "(* x 'is' y 'of' z 'isn't' // /= //= *)". - -(** Enable SSR rewrite compat **) +(** Signal that we have ssreflect version of rewrite (meaning + "rewrite a" must be printed "rewrite -> a" for compatibility). **) #[export] Set SSRRewriteLoaded. -Reserved Notation "" (at level 0, n at level 0, - format ""). -#[warning="-postfix-notation-not-level-1"] -Reserved Notation "T (* n *)" (at level 200, format "T (* n *)"). - -End SsrSyntax. - -Export SsrMatchingSyntax. -Export SsrSyntax. - (** Save primitive notation that will be overloaded. **) -Local Abbreviation RocqGenericIf c vT vF := (if c then vT else vF) (only parsing). +Local Abbreviation RocqGenericIf c vT vF := + (if c then vT else vF) (only parsing). Local Abbreviation RocqGenericDependentIf c x R vT vF := (if c as x return R then vT else vF) (only parsing). -(** Reserve notation that introduced in this file. **) +(** Reserve notations that are introduced in this file. **) Reserved Notation "'if' c 'then' vT 'else' vF" (at level 10, c, vT, vF at level 200). Reserved Notation "'if' c 'return' R 'then' vT 'else' vF" (at level 10, @@ -112,28 +38,6 @@ Reserved Notation "'if' c 'return' R 'then' vT 'else' vF" (at level 10, Reserved Notation "'if' c 'as' x 'return' R 'then' vT 'else' vF" (at level 10, c, R, vT, vF at level 200, x name). -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 ]"). - -Reserved Notation "[ 'elaborate' x ]" (at level 0). - -(** - To define notations for tactic in intro patterns. - When "=> /t" is parsed, "t:%ssripat" is actually interpreted. **) -Declare Scope ssripat_scope. -Delimit Scope ssripat_scope with ssripat. - (** Make the general "if" into a notation, so that we can override it below. The notations are "only parsing" because the Rocq decompiler will not @@ -168,523 +72,10 @@ Notation "'if' c 'as' x 'return' R 'then' vT 'else' vF" := Open Scope boolean_if_scope. -(** - To allow a wider variety of notations without reserving a large number of - of identifiers, the ssreflect library systematically uses "forms" to - enclose complex mixfix syntax. A "form" is simply a mixfix expression - enclosed in square brackets and introduced by a keyword: - #[#keyword ... #]# - Because the keyword follows a bracket it does not need to be reserved. - Non-ssreflect libraries that do not respect the form syntax (e.g., the Rocq - Lists library) should be loaded before ssreflect so that their notations - do not mask all ssreflect forms. **) -Declare Scope form_scope. -Delimit Scope form_scope with FORM. -Open Scope form_scope. - -(** Constants for abstract: and #[#: name #]# intro pattern **) -Definition abstract_lock := unit. -Definition abstract_key := tt. - -Definition abstract (statement : Type) (id : nat) (lock : abstract_lock) := - let: tt := lock in statement. - -Declare Scope ssr_scope. -Notation "" := (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. -Register abstract as plugins.ssreflect.abstract. - -(** Constants for tactic-views **) -Inductive external_view : Type := tactic_view of Type. - -(** - Syntax for referring to canonical structures: - #[#the struct_type of proj_val by proj_fun#]# - This form denotes the Canonical instance s of the Structure type - struct_type whose proj_fun projection is proj_val, i.e., such that - proj_fun s = proj_val. - Typically proj_fun will be A record field accessors of struct_type, but - this need not be the case; it can be, for instance, a field of a record - type to which struct_type coerces; proj_val will likewise be coerced to - the return type of proj_fun. In all but the simplest cases, proj_fun - should be eta-expanded to allow for the insertion of implicit arguments. - In the common case where proj_fun itself is a coercion, the "by" part - can be omitted entirely; in this case it is inferred by casting s to the - inferred type of proj_val. Obviously the latter can be fixed by using an - explicit cast on proj_val, and it is highly recommended to do so when the - return type intended for proj_fun is "Type", as the type inferred for - proj_val may vary because of sort polymorphism (it could be Set or Prop). - Note when using the #[#the _ of _ #]# form to generate a substructure from a - telescopes-style canonical hierarchy (implementing inheritance with - coercions), one should always project or coerce the value to the BASE - structure, because Rocq will only find a Canonical derived structure for - the Canonical base structure -- not for a base structure that is specific - to proj_value. **) - -Module TheCanonical. - -Variant put vT sT (v1 v2 : vT) (s : sT) : Prop := Put. - -Definition get vT sT v s (p : @put vT sT v v s) := let: Put _ _ _ := p in s. - -Definition get_by vT sT & sT -> vT := @get vT sT. - -End TheCanonical. - -Import TheCanonical. (* Note: no export. *) - -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 _)) - (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. - 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 "[ 'the' sT 'of' v 'by' f ]" := (@get_by _ sT f v _ _) - (only printing) : form_scope. - -Notation "[ 'the' sT 'of' v ]" := (@get _ sT v _ _) - (only printing) : form_scope. - -(** - We would like to recognize -Notation " #[# 'the' sT 'of' v : 'Type' #]#" := (@get Type sT v _ _) - (at level 0, format " #[# 'the' sT 'of' v : 'Type' #]#") : form_scope. - **) - -(** - Helper notation for canonical structure inheritance support. - This is a workaround for the poor interaction between delta reduction and - canonical projections in Rocq's unification algorithm, by which transparent - definitions hide canonical instances, i.e., in - Canonical a_type_struct := @Struct a_type ... - Definition my_type := a_type. - my_type doesn't effectively inherit the struct structure from a_type. Our - solution is to redeclare the instance as follows - Canonical my_type_struct := Eval hnf in #[#struct of my_type#]#. - The special notation #[#str of _ #]# must be defined for each Structure "str" - with constructor "Str", typically as follows - Definition clone_str s := - let: Str _ x y ... z := s return {type of Str for s} -> str in - fun k => k _ x y ... z. - Notation " #[# 'str' 'of' T 'for' s #]#" := (@clone_str s (@Str T)) - (at level 0, format " #[# 'str' 'of' T 'for' s #]#") : form_scope. - Notation " #[# 'str' 'of' T #]#" := (repack_str (fun x => @Str T x)) - (at level 0, format " #[# 'str' 'of' T #]#") : form_scope. - The notation for the match return predicate is defined below; the eta - expansion in the second form serves both to distinguish it from the first - and to avoid the delta reduction problem. - There are several variations on the notation and the definition of the - the "clone" function, for telescopes, mixin classes, and join (multiple - inheritance) classes. We describe a different idiom for clones in ssrfun; - it uses phantom types (see below) and static unification; see fintype and - ssralg for examples. **) - -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) : type_scope. - -(** - A generic "phantom" type (actually, a unit type with a phantom parameter). - This type can be used for type definitions that require some Structure - on one of their parameters, to allow Rocq to infer said structure so it - does not have to be supplied explicitly or via the " #[#the _ of _ #]#" notation - (the latter interacts poorly with other Notation). - The definition of a (co)inductive type with a parameter p : p_type, that - needs to use the operations of a structure - Structure p_str : Type := p_Str {p_repr :> p_type; p_op : p_repr -> ...} - should be given as - Inductive indt_type (p : p_str) := Indt ... . - Definition indt_of (p : p_str) & phantom p_type p := indt_type p. - Notation "{ 'indt' p }" := (indt_of (Phantom p)). - Definition indt p x y ... z : {indt p} := @Indt p x y ... z. - Notation " #[# 'indt' x y ... z #]#" := (indt x y ... z). - That is, the concrete type and its constructor should be shadowed by - definitions that use a phantom argument to infer and display the true - value of p (in practice, the "indt" constructor often performs additional - functions, like "locking" the representation -- see below). - We also define a simpler version ("phant" / "Phant") of phantom for the - common case where p_type is Type. **) - -Variant phantom T (p : T) : Prop := Phantom. -Arguments phantom : clear implicits. -Arguments Phantom : clear implicits. -Variant phant (p : Type) : Prop := Phant. - -(** Internal tagging used by the implementation of the ssreflect elim. **) - -Definition protect_term (A : Type) (x : A) : A := x. - -Register protect_term as plugins.ssreflect.protect_term. - -(** - The ssreflect idiom for a non-keyed pattern: - - unkeyed t will match any subterm that unifies with t, regardless of - whether it displays the same head symbol as t. - - unkeyed t a b will match any application of a term f unifying with t, - to two arguments unifying with a and b, respectively, regardless of - apparent head symbols. - - unkeyed x where x is a variable will match any subterm with the same - type as x (when x would raise the 'indeterminate pattern' error). **) - +(* This abbreviation is only parsing in Prelude *) Abbreviation 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) : form_scope. - -(** - Term tagging (user-level). - The ssreflect library uses four strengths of term tagging to restrict - convertibility during type checking: - nosimpl t simplifies to t EXCEPT in a definition; more precisely, given - Definition foo := nosimpl bar, foo (or foo t') will NOT be expanded by - the /= and //= switches unless it is in a forcing context (e.g., in - match foo t' with ... end, foo t' will be reduced if this allows the - match to be reduced). Note that nosimpl bar is simply notation for a - a term that beta-iota reduces to bar; hence rewrite /foo will replace - foo by bar, and rewrite -/foo will replace bar by foo. - CAVEAT: nosimpl should not be used inside a Section, because the end of - section "cooking" removes the iota redex. - locked t is provably equal to t, but is not convertible to t; 'locked' - provides support for selective rewriting, via the lock t : t = locked t - Lemma, and the ssreflect unlock tactic. - locked_with k t is equal but not convertible to t, much like locked t, - but supports explicit tagging with a value k : unit. This is used to - mitigate a flaw in the term comparison heuristic of the Rocq kernel, - which treats all terms of the form locked t as equal and compares their - arguments recursively, leading to an exponential blowup of comparison. - For this reason locked_with should be used rather than locked when - defining ADT operations. The unlock tactic does not support locked_with - but the unlock rewrite rule does, via the unlockable interface. - we also use Module Type ascription to create truly opaque constants, - because simple expansion of constants to reveal an unreducible term - doubles the time complexity of a negative comparison. Such opaque - constants can be expanded generically with the unlock rewrite rule. - See the definition of card and subset in fintype for examples of this. **) - -Abbreviation nosimpl t := (let: tt := tt in t). - -Lemma master_key : unit. Proof. exact tt. Qed. -Definition locked A := let: tt := master_key in fun x : A => x. - -Register master_key as plugins.ssreflect.master_key. -Register locked as plugins.ssreflect.locked. - -Lemma lock A x : x = locked x :> A. Proof. unlock; reflexivity. Qed. - -(** The basic closing tactic "done". **) -Ltac done := - trivial; hnf; intros; solve - [ do ![solve [trivial | simple refine (@sym_equal _ _ _ _); trivial] - | discriminate | contradiction | split] - | match goal with H : ~ _ |- _ => solve [case H; trivial] end ]. - -(** Quicker done tactic not including split, syntax: /0/ **) -Ltac ssrdone0 := - trivial; hnf; intros; solve - [ do ![solve [trivial | apply: sym_equal; trivial] - | discriminate | contradiction ] - | match goal with H : ~ _ |- _ => solve [case H; trivial] end ]. - -(** To unlock opaque constants. **) -#[universes(template)] -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 _)) : form_scope. - -Notation "[ 'unlockable' 'fun' C ]" := - (@Unlockable _ (fun _ => _) C (unlock _)) : form_scope. - -(** Generic keyed constant locking. **) - -(** The argument order ensures that k is always compared before T. **) -Definition locked_with k := let: tt := k in fun T x => x : T. - -(** - This can be used as a cheap alternative to cloning the unlockable instance - below, but with caution as unkeyed matching can be expensive. **) -Lemma locked_withE T k x : unkeyed (locked_with k x) = x :> T. -Proof. by case: k. Qed. - -(** Intensionaly, this instance will not apply to locked u. **) -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. **) -Lemma unlock_with T k x : unlocked (locked_with_unlockable k x) = x :> T. -Proof. exact: unlock. Qed. - -(** Abbreviation to trigger Rocq elaboration to fill the holes **) -Notation "[ 'elaborate' x ]" := (ltac:(refine x)) (only parsing). - -(** The internal lemmas for the have tactics. **) - -Lemma ssr_have - (Plemma : Prop) (Pgoal : Prop) - (step : Plemma) (rest : Plemma -> Pgoal) : Pgoal. -Proof. exact: rest step. Qed. - -Register ssr_have as plugins.ssreflect.ssr_have. - -Polymorphic Lemma ssr_have_upoly@{s1 s2;u1 u2} - (Plemma : Type@{s1;u1}) (Pgoal : Type@{s2;u2}) - (step : Plemma) (rest : Plemma -> Pgoal) : Pgoal. -Proof. exact: rest step. Qed. - -Register ssr_have_upoly as plugins.ssreflect.ssr_have_upoly. - -(** Internal N-ary congruence lemmas for the congr tactic. **) - -Fixpoint nary_congruence_statement (n : nat) - : (forall B, (B -> B -> Prop) -> Prop) -> Prop := - match n with - | O => fun k => forall B, k B (fun x1 x2 : B => x1 = x2) - | S n' => - let k' A B e (f1 f2 : A -> B) := - forall x1 x2, x1 = x2 -> (e (f1 x1) (f2 x2) : Prop) in - fun k => forall A, nary_congruence_statement n' (fun B e => k _ (k' A B e)) - end. - -Lemma nary_congruence n (k := fun B e => forall y : B, (e y y : Prop)) : - nary_congruence_statement n k. -Proof. -have: k _ _ := _; rewrite {1}/k. -elim: n k => [|n IHn] k k_P /= A; first exact: k_P. -by apply: IHn => B e He; apply: k_P => f x1 x2 <-. -Qed. - -Lemma ssr_congr_arrow Plemma Pgoal : Plemma = Pgoal -> Plemma -> Pgoal. -Proof. by move->. Qed. -Arguments ssr_congr_arrow : clear implicits. - -Register nary_congruence as plugins.ssreflect.nary_congruence. -Register ssr_congr_arrow as plugins.ssreflect.ssr_congr_arrow. - -(** View lemmas that don't use reflection. **) - -Section ApplyIff. - -Variables P Q : Prop. -Hypothesis eqPQ : P <-> Q. - -Lemma iffLR : P -> Q. Proof. by case: eqPQ. Qed. -Lemma iffRL : Q -> P. Proof. by case: eqPQ. Qed. - -Lemma iffLRn : ~P -> ~Q. Proof. by move=> nP tQ; case: nP; case: eqPQ tQ. Qed. -Lemma iffRLn : ~Q -> ~P. Proof. by move=> nQ tP; case: nQ; case: eqPQ tP. Qed. - -End ApplyIff. - -Hint View for move/ iffLRn|2 iffRLn|2 iffLR|2 iffRL|2. -Hint View for apply/ iffRLn|2 iffLRn|2 iffRL|2 iffLR|2. - -(** - To focus non-ssreflect tactics on a subterm, eg vm_compute. - Usage: - elim/abstract_context: (pattern) => G defG. - vm_compute; rewrite {}defG {G}. - Note that vm_cast are not stored in the proof term - for reductions occurring in the context, hence - set here := pattern; vm_compute in (value of here) - blows up at Qed time. **) -Lemma abstract_context T (P : T -> Type) x : - (forall Q, Q = P -> Q x) -> P x. -Proof. by move=> /(_ P); apply. Qed. - -(*****************************************************************************) -(* Material for under/over (to rewrite under binders using "context lemmas") *) - -Require Export ssrunder. - -#[global] -Hint Extern 0 (@Under_rel.Over_rel _ _ _ _) => - solve [ apply: Under_rel.over_rel_done ] : core. -#[global] -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_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. - 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 undesirable 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 when 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 spurious 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 other 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 solved 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. -Abbreviation nonPropType := type. -Coercion callee : call_of >-> Sortclass. -Coercion frame : type >-> call_of. -Abbreviation notProp T := (@check false test_negative (call T)). -End Exports. - -End NonPropType. -Export NonPropType.Exports. - -Module Export ipat. - -Notation "'[' 'apply' ']'" := (ltac:(let f := fresh "_top_" in move=> f {}/f)) - (at level 0, only parsing) : ssripat_scope. - -(* we try to preserve the naming by matching the names from the goal *) -(* we do move to perform a hnf before trying to match *) -Notation "'[' 'swap' ']'" := (ltac:(move; - let x := lazymatch goal with - | |- forall (x : _), _ => fresh x | |- let x := _ in _ => fresh x | _ => fresh "_top_" - end in intro x; move; - let y := lazymatch goal with - | |- forall (y : _), _ => fresh y | |- let y := _ in _ => fresh y | _ => fresh "_top_" - end in intro y; revert x; revert y)) - (at level 0, only parsing) : ssripat_scope. - - -(* we try to preserve the naming by matching the names from the goal *) -(* we do move to perform a hnf before trying to match *) -Notation "'[' 'dup' ']'" := (ltac:(move; - lazymatch goal with - | |- forall (x : _), _ => - let x := fresh x in intro x; - let copy := fresh x in have copy := x; revert x; revert copy - | |- let x := _ in _ => - let x := fresh x in intro x; - let copy := fresh x in pose copy := x; - do [unfold x in (value of copy)]; revert x; revert copy - | |- _ => - let x := fresh "_top_" in move=> x; - let copy := fresh "_top" in have copy := x; revert x; revert copy - end)) - (at level 0, only parsing) : ssripat_scope. - -Notation "'[' '1' '!' rules ']'" := (ltac:(rewrite rules)) - (at level 0, rules at level 200, only parsing) : ssripat_scope. -Notation "'[' '!' rules ']'" := (ltac:(rewrite !rules)) - (at level 0, rules at level 200, only parsing) : ssripat_scope. - -End ipat. - -(* A class to trigger reduction by rewriting. *) -(* Usage: rewrite [pattern]vm_compute. *) -(* Alternatively one may redefine a lemma as in algebra/rat.v : *) -(* Lemma rat_vm_compute n (x : rat) : vm_compute_eq n%:Q x -> n%:Q = x. *) -(* Proof. exact. Qed. *) - -Class vm_compute_eq {T : Type} (x y : T) := vm_compute : x = y. - -#[global] -Hint Extern 0 (@vm_compute_eq _ _ _) => - vm_compute; reflexivity : typeclass_instances. +Abbreviation phant := ssreflect_rw.phant. +Abbreviation Phant := ssreflect_rw.Phant. +Abbreviation phantom := ssreflect_rw.phantom. +Abbreviation Phantom := ssreflect_rw.Phantom. diff --git a/theories/Corelib/ssr/ssreflect_rw.v b/theories/Corelib/ssr/ssreflect_rw.v new file mode 100644 index 000000000000..810e127f30ce --- /dev/null +++ b/theories/Corelib/ssr/ssreflect_rw.v @@ -0,0 +1,643 @@ +(************************************************************************) +(* * The Rocq Prover / The Rocq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* .doc { font-family: monospace; white-space: pre; } # **) + +Require Import ssrmatching. +Declare ML Module "rocq-runtime.plugins.ssreflect". + +(** + This file is the Gallina part of the ssreflect plugin implementation. + Files that use the ssreflect plugin should always Require ssreflect and + either Import ssreflect or Import ssreflect.SsrSyntax. + Part of the contents of this file is technical and will only interest + advanced developers; in addition the following are defined: + #[#the str of v by f#]# == the Canonical s : str such that f s = v. + #[#the str of v#]# == the Canonical s : str that coerces to v. + 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 + rewrite multirule). + unkeyed t == t, but treated as an unkeyed matching pattern by + the ssreflect matching algorithm. + nosimpl t == t, but on the right-hand side of Definition C := + nosimpl disables expansion of C by /=. + locked t == t, but locked t is not convertible to t. + locked_with k t == t, but not convertible to t or locked_with k' t + unless k = k' (with k : unit). Rocq type-checking + will be much more efficient if locked_with with a + bespoke k is used for sealed definitions. + unlockable v == interface for sealed constant definitions of v. + Unlockable def == the unlockable that registers def : C = v. + #[#unlockable of C#]# == a clone for C of the canonical unlockable for the + definition of C (e.g., if it uses locked_with). + #[#unlockable fun C#]# == #[#unlockable of C#]# with the expansion forced to be + an explicit lambda expression. + -> The usage pattern for ADT operations is: + Definition foo_def x1 .. xn := big_foo_expression. + Fact foo_key : unit. Proof. by #[# #]#. Qed. + Definition foo := locked_with foo_key foo_def. + Canonical foo_unlockable := #[#unlockable fun foo#]#. + This minimizes the comparison overhead for foo, while still allowing + rw unlock to expose big_foo_expression. + + #[#elaborate x#]# == triggers Rocq elaboration to fill the holes of the term x + The main use case is to trigger typeclass inference in + the body of a ssreflect have := #[#elaborate body#]#. + + Additionally we provide default intro pattern ltac views: + - top of the stack actions: + => /#[#apply#]# := => hyp {}/hyp + => /#[#swap#]# := => x y; move: y x + (also swap and preserves let bindings) + => /#[#dup#]# := => x; have copy := x; move: copy x + (also copies and preserves let bindings) + - calling rw from an intro pattern, use with parsimony: + => /#[#1! rules#]# := rw rules + => /#[#! rules#]# := rw !rules + + 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. + +Module SsrSyntax. + +(** Declare Ssr keywords: "//" "/=" and "//=". **) +Reserved Notation "(******* // /= //= *******)". + +Reserved Notation "" (at level 0, n at level 0, only printing, + format ""). +#[warning="-postfix-notation-not-level-1"] +Reserved Notation "T (* n *)" + (at level 200, only printing, format "T (* n *)"). + +End SsrSyntax. + +Export SsrMatchingSyntax. +Export SsrSyntax. + +(** Reserve notations that are introduced in this file. **) +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 "[ 'unlockable' 'of' C ]" (at level 0, + format "[ 'unlockable' 'of' C ]"). + +Reserved Notation "=^~ r" (at level 100, format "=^~ r"). + +Reserved Notation "[ 'unlockable' 'fun' C ]" (at level 0, + format "[ 'unlockable' 'fun' C ]"). + +Reserved Notation "[ 'elaborate' x ]" (at level 0). + +(** + To define notations for tactic in intro patterns. + When "=> /t" is parsed, "t:%ssripat" is actually interpreted. **) +Declare Scope ssripat_scope. +Delimit Scope ssripat_scope with ssripat. + +(** + To allow a wider variety of notations without reserving a large number + of identifiers, the ssreflect library systematically uses "forms" to + enclose complex mixfix syntax. A "form" is simply a mixfix expression + enclosed in square brackets and introduced by a keyword: + #[#keyword ... #]# + Because the keyword follows a bracket it does not need to be reserved. + Non-ssreflect libraries that do not respect the form syntax (e.g., the Rocq + Lists library) should be loaded before ssreflect so that their notations + do not mask all ssreflect forms. **) +Declare Scope form_scope. +Delimit Scope form_scope with FORM. +Open Scope form_scope. + +(** Constants for abstract: and #[#: name #]# intro pattern **) +Definition abstract_lock := unit. +Definition abstract_key := tt. + +Definition abstract (statement : Type) (id : nat) (lock : abstract_lock) := + let: tt := lock in statement. + +Declare Scope ssr_scope. +Notation "" := (abstract _ n _) (only printing) : ssr_scope. +Notation "T (* n *)" := (abstract T n abstract_key) (only printing) : ssr_scope. +Open Scope ssr_scope. + +Register abstract_lock as plugins.ssreflect.abstract_lock. +Register abstract_key as plugins.ssreflect.abstract_key. +Register abstract as plugins.ssreflect.abstract. + +(** Constants for tactic-views **) +Inductive external_view : Type := tactic_view of Type. + +(** + Syntax for referring to canonical structures: + #[#the struct_type of proj_val by proj_fun#]# + This form denotes the Canonical instance s of the Structure type + struct_type whose proj_fun projection is proj_val, i.e., such that + proj_fun s = proj_val. + Typically proj_fun will be A record field accessors of struct_type, but + this need not be the case; it can be, for instance, a field of a record + type to which struct_type coerces; proj_val will likewise be coerced to + the return type of proj_fun. In all but the simplest cases, proj_fun + should be eta-expanded to allow for the insertion of implicit arguments. + In the common case where proj_fun itself is a coercion, the "by" part + can be omitted entirely; in this case it is inferred by casting s to the + inferred type of proj_val. Obviously the latter can be fixed by using an + explicit cast on proj_val, and it is highly recommended to do so when the + return type intended for proj_fun is "Type", as the type inferred for + proj_val may vary because of sort polymorphism (it could be Set or Prop). + Note when using the #[#the _ of _ #]# form to generate a substructure from a + telescopes-style canonical hierarchy (implementing inheritance with + coercions), one should always project or coerce the value to the BASE + structure, because Rocq will only find a Canonical derived structure for + the Canonical base structure -- not for a base structure that is specific + to proj_value. **) + +Module TheCanonical. + +Variant put vT sT (v1 v2 : vT) (s : sT) : Prop := Put. + +Definition get vT sT v s (p : @put vT sT v v s) := let: Put _ _ _ := p in s. + +Definition get_by vT sT & sT -> vT := @get vT sT. + +End TheCanonical. + +Import TheCanonical. (* Note: no export. *) + +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 _)) + (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. + 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 "[ 'the' sT 'of' v 'by' f ]" := (@get_by _ sT f v _ _) + (only printing) : form_scope. + +Notation "[ 'the' sT 'of' v ]" := (@get _ sT v _ _) + (only printing) : form_scope. + +(** + We would like to recognize +Notation " #[# 'the' sT 'of' v : 'Type' #]#" := (@get Type sT v _ _) + (at level 0, format " #[# 'the' sT 'of' v : 'Type' #]#") : form_scope. + **) + +(** + Helper notation for canonical structure inheritance support. + This is a workaround for the poor interaction between delta reduction and + canonical projections in Rocq's unification algorithm, by which transparent + definitions hide canonical instances, i.e., in + Canonical a_type_struct := @Struct a_type ... + Definition my_type := a_type. + my_type doesn't effectively inherit the struct structure from a_type. Our + solution is to redeclare the instance as follows + Canonical my_type_struct := Eval hnf in #[#struct of my_type#]#. + The special notation #[#str of _ #]# must be defined for each Structure "str" + with constructor "Str", typically as follows + Definition clone_str s := + let: Str _ x y ... z := s return {type of Str for s} -> str in + fun k => k _ x y ... z. + Notation " #[# 'str' 'of' T 'for' s #]#" := (@clone_str s (@Str T)) + (at level 0, format " #[# 'str' 'of' T 'for' s #]#") : form_scope. + Notation " #[# 'str' 'of' T #]#" := (repack_str (fun x => @Str T x)) + (at level 0, format " #[# 'str' 'of' T #]#") : form_scope. + The notation for the match return predicate is defined below; the eta + expansion in the second form serves both to distinguish it from the first + and to avoid the delta reduction problem. + There are several variations on the notation and the definition of the + the "clone" function, for telescopes, mixin classes, and join (multiple + inheritance) classes. We describe a different idiom for clones in ssrfun; + it uses phantom types (see below) and static unification; see fintype and + ssralg for examples. **) + +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) : type_scope. + +(** + A generic "phantom" type (actually, a unit type with a phantom parameter). + This type can be used for type definitions that require some Structure + on one of their parameters, to allow Rocq to infer said structure so it + does not have to be supplied explicitly or via the " #[#the _ of _ #]#" notation + (the latter interacts poorly with other Notation). + The definition of a (co)inductive type with a parameter p : p_type, that + needs to use the operations of a structure + Structure p_str : Type := p_Str {p_repr :> p_type; p_op : p_repr -> ...} + should be given as + Inductive indt_type (p : p_str) := Indt ... . + Definition indt_of (p : p_str) & phantom p_type p := indt_type p. + Notation "{ 'indt' p }" := (indt_of (Phantom p)). + Definition indt p x y ... z : {indt p} := @Indt p x y ... z. + Notation " #[# 'indt' x y ... z #]#" := (indt x y ... z). + That is, the concrete type and its constructor should be shadowed by + definitions that use a phantom argument to infer and display the true + value of p (in practice, the "indt" constructor often performs additional + functions, like "locking" the representation -- see below). + We also define a simpler version ("phant" / "Phant") of phantom for the + common case where p_type is Type. **) + +Variant phantom T (p : T) : Prop := Phantom. +Arguments phantom : clear implicits. +Arguments Phantom : clear implicits. +Variant phant (p : Type) : Prop := Phant. + +(** Internal tagging used by the implementation of the ssreflect elim. **) + +Definition protect_term (A : Type) (x : A) : A := x. + +Register protect_term as plugins.ssreflect.protect_term. + +(** + The ssreflect idiom for a non-keyed pattern: + - unkeyed t will match any subterm that unifies with t, regardless of + whether it displays the same head symbol as t. + - unkeyed t a b will match any application of a term f unifying with t, + to two arguments unifying with a and b, respectively, regardless of + apparent head symbols. + - unkeyed x where x is a variable will match any subterm with the same + type as x (when x would raise the 'indeterminate pattern' error). **) + +Abbreviation unkeyed x := (let flex := x in flex) (only parsing). + +(** Ssreflect converse rewrite rule rule idiom. **) +Definition ssr_converse R (r : R) := (Logic.I, r). +Notation "=^~ r" := (ssr_converse r) : form_scope. + +(** + Term tagging (user-level). + The ssreflect library uses four strengths of term tagging to restrict + convertibility during type checking: + nosimpl t simplifies to t EXCEPT in a definition; more precisely, given + Definition foo := nosimpl bar, foo (or foo t') will NOT be expanded by + the /= and //= switches unless it is in a forcing context (e.g., in + match foo t' with ... end, foo t' will be reduced if this allows the + match to be reduced). Note that nosimpl bar is simply notation for a + a term that beta-iota reduces to bar; hence rw /foo will replace + foo by bar, and rw -/foo will replace bar by foo. + CAVEAT: nosimpl should not be used inside a Section, because the end of + section "cooking" removes the iota redex. + locked t is provably equal to t, but is not convertible to t; 'locked' + provides support for selective rewriting, via the lock t : t = locked t + Lemma, and the ssreflect unlock tactic. + locked_with k t is equal but not convertible to t, much like locked t, + but supports explicit tagging with a value k : unit. This is used to + mitigate a flaw in the term comparison heuristic of the Rocq kernel, + which treats all terms of the form locked t as equal and compares their + arguments recursively, leading to an exponential blowup of comparison. + For this reason locked_with should be used rather than locked when + defining ADT operations. The unlock tactic does not support locked_with + but the unlock rewrite rule does, via the unlockable interface. + we also use Module Type ascription to create truly opaque constants, + because simple expansion of constants to reveal an unreducible term + doubles the time complexity of a negative comparison. Such opaque + constants can be expanded generically with the unlock rewrite rule. + See the definition of card and subset in fintype for examples of this. **) + +Abbreviation nosimpl t := (let: tt := tt in t). + +Lemma master_key : unit. Proof. exact tt. Qed. +Definition locked A := let: tt := master_key in fun x : A => x. + +Register master_key as plugins.ssreflect.master_key. +Register locked as plugins.ssreflect.locked. + +Lemma lock A x : x = locked x :> A. Proof. unlock; reflexivity. Qed. + +(** The basic closing tactic "done". **) +Ltac done := + trivial; hnf; intros; solve + [ do ![solve [trivial | simple refine (@sym_equal _ _ _ _); trivial] + | discriminate | contradiction | split] + | match goal with H : ~ _ |- _ => solve [case H; trivial] end ]. + +(** Quicker done tactic not including split, syntax: /0/ **) +Ltac ssrdone0 := + trivial; hnf; intros; solve + [ do ![solve [trivial | apply: sym_equal; trivial] + | discriminate | contradiction ] + | match goal with H : ~ _ |- _ => solve [case H; trivial] end ]. + +(** To unlock opaque constants. **) +#[universes(template)] +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 _)) : form_scope. + +Notation "[ 'unlockable' 'fun' C ]" := + (@Unlockable _ (fun _ => _) C (unlock _)) : form_scope. + +(** Generic keyed constant locking. **) + +(** The argument order ensures that k is always compared before T. **) +Definition locked_with k := let: tt := k in fun T x => x : T. + +(** + This can be used as a cheap alternative to cloning the unlockable instance + below, but with caution as unkeyed matching can be expensive. **) +Lemma locked_withE T k x : unkeyed (locked_with k x) = x :> T. +Proof. by case: k. Qed. + +(** Intensionaly, this instance will not apply to locked u. **) +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. **) +Lemma unlock_with T k x : unlocked (locked_with_unlockable k x) = x :> T. +Proof. exact: unlock. Qed. + +(** Abbreviation to trigger Rocq elaboration to fill the holes **) +Notation "[ 'elaborate' x ]" := (ltac:(refine x)) (only parsing). + +(** The internal lemmas for the have tactics. **) + +Lemma ssr_have + (Plemma : Prop) (Pgoal : Prop) + (step : Plemma) (rest : Plemma -> Pgoal) : Pgoal. +Proof. exact: rest step. Qed. + +Register ssr_have as plugins.ssreflect.ssr_have. + +Polymorphic Lemma ssr_have_upoly@{s1 s2;u1 u2} + (Plemma : Type@{s1;u1}) (Pgoal : Type@{s2;u2}) + (step : Plemma) (rest : Plemma -> Pgoal) : Pgoal. +Proof. exact: rest step. Qed. + +Register ssr_have_upoly as plugins.ssreflect.ssr_have_upoly. + +(** Internal N-ary congruence lemmas for the congr tactic. **) + +Fixpoint nary_congruence_statement (n : nat) + : (forall B, (B -> B -> Prop) -> Prop) -> Prop := + match n with + | O => fun k => forall B, k B (fun x1 x2 : B => x1 = x2) + | S n' => + let k' A B e (f1 f2 : A -> B) := + forall x1 x2, x1 = x2 -> (e (f1 x1) (f2 x2) : Prop) in + fun k => forall A, nary_congruence_statement n' (fun B e => k _ (k' A B e)) + end. + +Lemma nary_congruence n (k := fun B e => forall y : B, (e y y : Prop)) : + nary_congruence_statement n k. +Proof. +have: k _ _ := _; rw {1}/k. +elim: n k => [|n IHn] k k_P /= A; first exact: k_P. +by apply: IHn => B e He; apply: k_P => f x1 x2 <-. +Qed. + +Lemma ssr_congr_arrow Plemma Pgoal : Plemma = Pgoal -> Plemma -> Pgoal. +Proof. by move->. Qed. +Arguments ssr_congr_arrow : clear implicits. + +Register nary_congruence as plugins.ssreflect.nary_congruence. +Register ssr_congr_arrow as plugins.ssreflect.ssr_congr_arrow. + +(** View lemmas that don't use reflection. **) + +Section ApplyIff. + +Variables P Q : Prop. +Hypothesis eqPQ : P <-> Q. + +Lemma iffLR : P -> Q. Proof. by case: eqPQ. Qed. +Lemma iffRL : Q -> P. Proof. by case: eqPQ. Qed. + +Lemma iffLRn : ~P -> ~Q. Proof. by move=> nP tQ; case: nP; case: eqPQ tQ. Qed. +Lemma iffRLn : ~Q -> ~P. Proof. by move=> nQ tP; case: nQ; case: eqPQ tP. Qed. + +End ApplyIff. + +Hint View for move/ iffLRn|2 iffRLn|2 iffLR|2 iffRL|2. +Hint View for apply/ iffRLn|2 iffLRn|2 iffRL|2 iffLR|2. + +(** + To focus non-ssreflect tactics on a subterm, eg vm_compute. + Usage: + elim/abstract_context: (pattern) => G defG. + vm_compute; rw {}defG {G}. + Note that vm_cast are not stored in the proof term + for reductions occurring in the context, hence + set here := pattern; vm_compute in (value of here) + blows up at Qed time. **) +Lemma abstract_context T (P : T -> Type) x : + (forall Q, Q = P -> Q x) -> P x. +Proof. by move=> /(_ P); apply. Qed. + +(*****************************************************************************) +(* Material for under/over (to rewrite under binders using "context lemmas") *) + +Require Export ssrunder. + +#[global] +Hint Extern 0 (@Under_rel.Over_rel _ _ _ _) => + solve [ apply: Under_rel.over_rel_done ] : core. +#[global] +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_rel.under_rel_done + | rw 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. + 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 undesirable 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 when 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 spurious 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 other 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 solved 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. +Abbreviation nonPropType := type. +Coercion callee : call_of >-> Sortclass. +Coercion frame : type >-> call_of. +Abbreviation notProp T := (@check false test_negative (call T)). +End Exports. + +End NonPropType. +Export NonPropType.Exports. + +Module Export ipat. + +Notation "'[' 'apply' ']'" := (ltac:(let f := fresh "_top_" in move=> f {}/f)) + (at level 0, only parsing) : ssripat_scope. + +(* we try to preserve the naming by matching the names from the goal *) +(* we do move to perform a hnf before trying to match *) +Notation "'[' 'swap' ']'" := (ltac:(move; + let x := lazymatch goal with + | |- forall (x : _), _ => fresh x | |- let x := _ in _ => fresh x | _ => fresh "_top_" + end in intro x; move; + let y := lazymatch goal with + | |- forall (y : _), _ => fresh y | |- let y := _ in _ => fresh y | _ => fresh "_top_" + end in intro y; revert x; revert y)) + (at level 0, only parsing) : ssripat_scope. + + +(* we try to preserve the naming by matching the names from the goal *) +(* we do move to perform a hnf before trying to match *) +Notation "'[' 'dup' ']'" := (ltac:(move; + lazymatch goal with + | |- forall (x : _), _ => + let x := fresh x in intro x; + let copy := fresh x in have copy := x; revert x; revert copy + | |- let x := _ in _ => + let x := fresh x in intro x; + let copy := fresh x in pose copy := x; + do [unfold x in (value of copy)]; revert x; revert copy + | |- _ => + let x := fresh "_top_" in move=> x; + let copy := fresh "_top" in have copy := x; revert x; revert copy + end)) + (at level 0, only parsing) : ssripat_scope. + +Notation "'[' '1' '!' rules ']'" := (ltac:(rw rules)) + (at level 0, rules at level 200, only parsing) : ssripat_scope. +Notation "'[' '!' rules ']'" := (ltac:(rw !rules)) + (at level 0, rules at level 200, only parsing) : ssripat_scope. + +End ipat. + +(* A class to trigger reduction by rewriting. *) +(* Usage: rw [pattern]vm_compute. *) +(* Alternatively one may redefine a lemma as in algebra/rat.v : *) +(* Lemma rat_vm_compute n (x : rat) : vm_compute_eq n%:Q x -> n%:Q = x. *) +(* Proof. exact. Qed. *) + +Class vm_compute_eq {T : Type} (x y : T) := vm_compute : x = y. + +#[global] +Hint Extern 0 (@vm_compute_eq _ _ _) => + vm_compute; reflexivity : typeclass_instances. From 9e9afe18beff2b86d769c109c6530c7965f295e2 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 20 Mar 2026 08:09:39 +0100 Subject: [PATCH 08/11] [ssreflect] Renaming rewrite -> rw --- test-suite/output/ssr_under.v | 2 +- theories/Corelib/ssr/ssrbool.v | 98 +++++++++++++++++----------------- theories/Corelib/ssr/ssrfun.v | 26 ++++----- 3 files changed, 63 insertions(+), 63 deletions(-) diff --git a/test-suite/output/ssr_under.v b/test-suite/output/ssr_under.v index 5328f35d70fc..d100488d0abb 100644 --- a/test-suite/output/ssr_under.v +++ b/test-suite/output/ssr_under.v @@ -10,7 +10,7 @@ Axiom eq_G : Ltac show := match goal with [|-?g] => idtac g end. Lemma example_G (n : nat) : G (fun n => n - n) n >= 0. -under eq_G => m do [show; rewrite subnn]. +under eq_G => m do [show; rw subnn]. show. Abort. diff --git a/theories/Corelib/ssr/ssrbool.v b/theories/Corelib/ssr/ssrbool.v index 514a9b427541..a1d23ba841a8 100644 --- a/theories/Corelib/ssr/ssrbool.v +++ b/theories/Corelib/ssr/ssrbool.v @@ -557,7 +557,7 @@ Lemma contraTnot (b : bool) (P : Prop) : (P -> ~~ b) -> (b -> ~ P). Proof. by case: b; auto. Qed. Lemma contraNnot (P : Prop) (b : bool) : (P -> b) -> (~~ b -> ~ P). -Proof. rewrite -{1}[b]negbK; exact: contraTnot. Qed. +Proof. rw -{1}[b]negbK; exact: contraTnot. Qed. Lemma contraPT (P : Prop) (b : bool) : (~~ b -> ~ P) -> P -> b. Proof. by case: b => //= /(_ isT) nP /nP. Qed. @@ -566,7 +566,7 @@ Lemma contra_notT (P : Prop) (b : bool) : (~~ b -> P) -> ~ P -> b. Proof. by case: b => //= /(_ isT) HP /(_ HP). Qed. Lemma contra_notN (P : Prop) (b : bool) : (b -> P) -> ~ P -> ~~ b. -Proof. rewrite -{1}[b]negbK; exact: contra_notT. Qed. +Proof. rw -{1}[b]negbK; exact: contra_notT. Qed. Lemma contraPN (P : Prop) (b : bool) : (b -> ~ P) -> (P -> ~~ b). Proof. by case: b => //=; move/(_ isT) => HP /HP. Qed. @@ -620,7 +620,7 @@ Lemma ifP : if_spec (b = false) b (if b then vT else vF). Proof. by case def_b: b; constructor. Qed. Lemma ifPn : if_spec (~~ b) b (if b then vT else vF). -Proof. by case def_b: b; constructor; rewrite ?def_b. Qed. +Proof. by case def_b: b; constructor; rw ?def_b. Qed. Lemma ifT : b -> (if b then vT else vF) = vT. Proof. by move->. Qed. Lemma ifF : b = false -> (if b then vT else vF) = vF. Proof. by move->. Qed. @@ -686,10 +686,10 @@ Lemma elimTFn : b = c -> if c then ~ P else P. Proof. by move <-; apply: (elimNTF Hb); case b. Qed. Lemma equivPifn : (Q -> P) -> (P -> Q) -> if b then ~ Q else Q. -Proof. by rewrite -if_neg; apply: equivPif. Qed. +Proof. by rw -if_neg; apply: equivPif. Qed. Lemma xorPifn : Q \/ P -> ~ (Q /\ P) -> if b then Q else ~ Q. -Proof. by rewrite -if_neg; apply: xorPif. Qed. +Proof. by rw -if_neg; apply: xorPif. Qed. End ReflectNegCore. @@ -746,7 +746,7 @@ Variant alt_spec : bool -> Type := | AltFalse of ~~ b : alt_spec false. Lemma altP : alt_spec b. -Proof. by case def_b: b / Pb; constructor; rewrite ?def_b. Qed. +Proof. by case def_b: b / Pb; constructor; rw ?def_b. Qed. Lemma eqbLR (b1 b2 : bool) : b1 = b2 -> b1 -> b2. Proof. by move->. Qed. @@ -1159,13 +1159,13 @@ Arguments addbP {a b}. Ltac bool_congr := match goal with | |- (?X1 && ?X2 = ?X3) => first - [ symmetry; rewrite -1?(andbC X1) -?(andbCA X1); congr 1 (andb X1); symmetry - | case: (X1); [ rewrite ?andTb ?andbT // | by rewrite ?andbF /= ] ] + [ symmetry; rw -1?(andbC X1) -?(andbCA X1); congr 1 (andb X1); symmetry + | case: (X1); [ rw ?andTb ?andbT // | by rw ?andbF /= ] ] | |- (?X1 || ?X2 = ?X3) => first - [ symmetry; rewrite -1?(orbC X1) -?(orbCA X1); congr 1 (orb X1); symmetry - | case: (X1); [ by rewrite ?orbT //= | rewrite ?orFb ?orbF ] ] + [ symmetry; rw -1?(orbC X1) -?(orbCA X1); congr 1 (orb X1); symmetry + | case: (X1); [ by rw ?orbT //= | rw ?orFb ?orbF ] ] | |- (?X1 (+) ?X2 = ?X3) => - symmetry; rewrite -1?(addbC X1) -?(addbCA X1); congr 1 (addb X1); symmetry + symmetry; rw -1?(addbC X1) -?(addbCA X1); congr 1 (addb X1); symmetry | |- (~~ ?X1 = ?X2) => congr 1 negb end. @@ -1580,7 +1580,7 @@ Lemma mem_topred pT (pp : pT) : mem (topred pp) = mem pp. Proof. by case: pT pp. Qed. Lemma topredE pT x (pp : pT) : topred pp x = (x \in pp). -Proof. by rewrite -mem_topred. Qed. +Proof. by rw -mem_topred. Qed. Lemma app_predE x p (ap : registered_applicative_pred p) : ap x = (x \in p). Proof. by case: ap => _ /= ->. Qed. @@ -1776,10 +1776,10 @@ Section PER. Hypotheses (symR : symmetric) (trR : transitive). Lemma sym_left_transitive : left_transitive. -Proof. by move=> x y Rxy z; apply/idP/idP; apply: trR; rewrite // symR. Qed. +Proof. by move=> x y Rxy z; apply/idP/idP; apply: trR; rw // symR. Qed. Lemma sym_right_transitive : right_transitive. -Proof. by move=> x y /sym_left_transitive Rxy z; rewrite !(symR z) Rxy. Qed. +Proof. by move=> x y /sym_left_transitive Rxy z; rw !(symR z) Rxy. Qed. End PER. @@ -1792,7 +1792,7 @@ Definition equivalence_rel := forall x y z, R z z * (R x y -> R x z = R y z). Lemma equivalence_relP : equivalence_rel <-> reflexive /\ left_transitive. Proof. split=> [eqiR | [Rxx trR] x y z]; last by split=> [|/trR->]. -by split=> [x | x y Rxy z]; [rewrite (eqiR x x x) | rewrite (eqiR x y z)]. +by split=> [x | x y Rxy z]; [rw (eqiR x x x) | rw (eqiR x y z)]. Qed. End RelationProperties. @@ -1966,19 +1966,19 @@ Lemma can_in_inj : {in D1, cancel f g} -> {in D1 &, injective f}. Proof. by move=> fK x y /fK{2}<- /fK{2}<- ->. Qed. Lemma canLR_in x y : {in D1, cancel f g} -> y \in D1 -> x = f y -> g x = y. -Proof. by move=> fK D1y ->; rewrite fK. Qed. +Proof. by move=> fK D1y ->; rw fK. Qed. Lemma canRL_in x y : {in D1, cancel f g} -> x \in D1 -> f x = y -> x = g y. -Proof. by move=> fK D1x <-; rewrite fK. Qed. +Proof. by move=> fK D1x <-; rw fK. Qed. Lemma on_can_inj : {on D2, cancel f & g} -> {on D2 &, injective f}. Proof. by move=> fK x y /fK{2}<- /fK{2}<- ->. Qed. Lemma canLR_on x y : {on D2, cancel f & g} -> f y \in D2 -> x = f y -> g x = y. -Proof. by move=> fK D2fy ->; rewrite fK. Qed. +Proof. by move=> fK D2fy ->; rw fK. Qed. Lemma canRL_on x y : {on D2, cancel f & g} -> f x \in D2 -> f x = y -> x = g y. -Proof. by move=> fK D2fx <-; rewrite fK. Qed. +Proof. by move=> fK D2fx <-; rw fK. Qed. Lemma inW_bij : bijective f -> {in D1, bijective f}. Proof. by case=> g' fK g'K; exists g' => * ? *; auto. Qed. @@ -2007,21 +2007,21 @@ Qed. Lemma in_on1P : {in D1, {on D2, allQ1 f}} <-> {in [pred x in D1 | f x \in D2], allQ1 f}. Proof. -split => allf x; have := allf x; rewrite inE => Q1f; first by case/andP. +split => allf x; have := allf x; rw inE => Q1f; first by case/andP. by move=> ? ?; apply: Q1f; apply/andP. Qed. Lemma in_on1lP : {in D1, {on D2, allQ1l f & h}} <-> {in [pred x in D1 | f x \in D2], allQ1l f h}. Proof. -split => allf x; have := allf x; rewrite inE => Q1f; first by case/andP. +split => allf x; have := allf x; rw inE => Q1f; first by case/andP. by move=> ? ?; apply: Q1f; apply/andP. Qed. Lemma in_on2P : {in D1 &, {on D2 &, allQ2 f}} <-> {in [pred x in D1 | f x \in D2] &, allQ2 f}. Proof. -split => allf x y; have := allf x y; rewrite !inE => Q2f. +split => allf x y; have := allf x y; rw !inE => Q2f. by move=> /andP[? ?] /andP[? ?]; apply: Q2f. by move=> ? ? ? ?; apply: Q2f; apply/andP. Qed. @@ -2098,12 +2098,12 @@ Arguments in_on2S {T1 T2} D2 {f Q2}. Lemma can_in_pcan [rT aT : Type] (A : {pred aT}) [f : aT -> rT] [g : rT -> aT] : {in A, cancel f g} -> {in A, pcancel f (fun y : rT => Some (g y))}. -Proof. by move=> fK x Ax; rewrite fK. Qed. +Proof. by move=> fK x Ax; rw fK. Qed. Lemma pcan_in_inj [rT aT : Type] [A : {pred aT}] [f : aT -> rT] [g : rT -> option aT] : {in A, pcancel f g} -> {in A &, injective f}. -Proof. by move=> fK x y Ax Ay /(congr1 g); rewrite !fK// => -[]. Qed. +Proof. by move=> fK x y Ax Ay /(congr1 g); rw !fK// => -[]. Qed. Lemma in_inj_comp A B C (f : B -> A) (h : C -> B) (P : pred B) (Q : pred C) : {in P &, injective f} -> {in Q &, injective h} -> {homo h : x / Q x >-> P x} -> @@ -2117,14 +2117,14 @@ Lemma can_in_comp [A B C : Type] (D : {pred B}) (D' : {pred C}) {homo h : x / x \in D' >-> x \in D} -> {in D, cancel f f'} -> {in D', cancel h h'} -> {in D', cancel (f \o h) (h' \o f')}. -Proof. by move=> hD fK hK c cD /=; rewrite fK ?hK ?hD. Qed. +Proof. by move=> hD fK hK c cD /=; rw fK ?hK ?hD. Qed. Lemma pcan_in_comp [A B C : Type] (D : {pred B}) (D' : {pred C}) [f : B -> A] [h : C -> B] [f' : A -> option B] [h' : B -> option C] : {homo h : x / x \in D' >-> x \in D} -> {in D, pcancel f f'} -> {in D', pcancel h h'} -> {in D', pcancel (f \o h) (obind h' \o f')}. -Proof. by move=> hD fK hK c cD /=; rewrite fK/= ?hK ?hD. Qed. +Proof. by move=> hD fK hK c cD /=; rw fK/= ?hK ?hD. Qed. Definition pred_oapp T (D : {pred T}) : pred (option T) := [pred x | oapp (mem D) false x]. @@ -2135,9 +2135,9 @@ Lemma ocan_in_comp [A B C : Type] (D : {pred B}) (D' : {pred C}) {in D, ocancel f f'} -> {in D', ocancel h h'} -> {in D', ocancel (obind f \o h) (h' \o f')}. Proof. -move=> hD fK hK c cD /=; rewrite -[RHS]hK/=; case hcE : (h c) => [b|]//=. -have bD : b \in D by have := hD _ cD; rewrite hcE inE. -by rewrite -[b in RHS]fK; case: (f b) => //=; have /hK := cD; rewrite hcE. +move=> hD fK hK c cD /=; rw -[RHS]hK/=; case hcE : (h c) => [b|]//=. +have bD : b \in D by have := hD _ cD; rw hcE inE. +by rw -[b in RHS]fK; case: (f b) => //=; have /hK := cD; rw hcE. Qed. Section in_sig. @@ -2187,7 +2187,7 @@ Lemma equivalence_relP_in T (R : rel T) (A : pred T) : <-> {in A, reflexive R} /\ {in A &, forall x y, R x y -> {in A, R x =1 R y}}. Proof. split=> [eqiR | [Rxx trR] x y z *]; last by split=> [|/trR-> //]; apply: Rxx. -by split=> [x Ax|x y Ax Ay Rxy z Az]; [rewrite (eqiR x x) | rewrite (eqiR x y)]. +by split=> [x Ax|x y Ax Ay Rxy z Az]; [rw (eqiR x x) | rw (eqiR x y)]. Qed. Section MonoHomoMorphismTheory. @@ -2196,41 +2196,41 @@ Variables (aT rT sT : Type) (f : aT -> rT) (g : rT -> aT). Variables (aP : pred aT) (rP : pred rT) (aR : rel aT) (rR : rel rT). Lemma monoW : {mono f : x / aP x >-> rP x} -> {homo f : x / aP x >-> rP x}. -Proof. by move=> hf x ax; rewrite hf. Qed. +Proof. by move=> hf x ax; rw hf. Qed. Lemma mono2W : {mono f : x y / aR x y >-> rR x y} -> {homo f : x y / aR x y >-> rR x y}. -Proof. by move=> hf x y axy; rewrite hf. Qed. +Proof. by move=> hf x y axy; rw hf. Qed. Hypothesis fgK : cancel g f. Lemma homoRL : {homo f : x y / aR x y >-> rR x y} -> forall x y, aR (g x) y -> rR x (f y). -Proof. by move=> Hf x y /Hf; rewrite fgK. Qed. +Proof. by move=> Hf x y /Hf; rw fgK. Qed. Lemma homoLR : {homo f : x y / aR x y >-> rR x y} -> forall x y, aR x (g y) -> rR (f x) y. -Proof. by move=> Hf x y /Hf; rewrite fgK. Qed. +Proof. by move=> Hf x y /Hf; rw fgK. Qed. Lemma homo_mono : {homo f : x y / aR x y >-> rR x y} -> {homo g : x y / rR x y >-> aR x y} -> {mono g : x y / rR x y >-> aR x y}. Proof. move=> mf mg x y; case: (boolP (rR _ _))=> [/mg //|]. -by apply: contraNF=> /mf; rewrite !fgK. +by apply: contraNF=> /mf; rw !fgK. Qed. Lemma monoLR : {mono f : x y / aR x y >-> rR x y} -> forall x y, rR (f x) y = aR x (g y). -Proof. by move=> mf x y; rewrite -{1}[y]fgK mf. Qed. +Proof. by move=> mf x y; rw -{1}[y]fgK mf. Qed. Lemma monoRL : {mono f : x y / aR x y >-> rR x y} -> forall x y, rR x (f y) = aR (g x) y. -Proof. by move=> mf x y; rewrite -{1}[x]fgK mf. Qed. +Proof. by move=> mf x y; rw -{1}[x]fgK mf. Qed. Lemma can_mono : {mono f : x y / aR x y >-> rR x y} -> {mono g : x y / rR x y >-> aR x y}. -Proof. by move=> mf x y /=; rewrite -mf !fgK. Qed. +Proof. by move=> mf x y /=; rw -mf !fgK. Qed. End MonoHomoMorphismTheory. @@ -2243,14 +2243,14 @@ Variable (aP : pred aT) (rP : pred rT) (aR : rel aT) (rR : rel rT). Lemma mono1W_in : {in aD, {mono f : x / aP x >-> rP x}} -> {in aD, {homo f : x / aP x >-> rP x}}. -Proof. by move=> hf x hx ax; rewrite hf. Qed. +Proof. by move=> hf x hx ax; rw hf. Qed. #[deprecated(since="Coq 8.16", note="Use mono1W_in instead.")] Abbreviation mono2W_in := mono1W_in. Lemma monoW_in : {in aD &, {mono f : x y / aR x y >-> rR x y}} -> {in aD &, {homo f : x y / aR x y >-> rR x y}}. -Proof. by move=> hf x y hx hy axy; rewrite hf. Qed. +Proof. by move=> hf x y hx hy axy; rw hf. Qed. Hypothesis fgK : {in rD, {on aD, cancel g & f}}. Hypothesis mem_g : {homo g : x / x \in rD >-> x \in aD}. @@ -2258,12 +2258,12 @@ Hypothesis mem_g : {homo g : x / x \in rD >-> x \in aD}. Lemma homoRL_in : {in aD &, {homo f : x y / aR x y >-> rR x y}} -> {in rD & aD, forall x y, aR (g x) y -> rR x (f y)}. -Proof. by move=> Hf x y hx hy /Hf; rewrite fgK ?mem_g// ?inE; apply. Qed. +Proof. by move=> Hf x y hx hy /Hf; rw fgK ?mem_g// ?inE; apply. Qed. Lemma homoLR_in : {in aD &, {homo f : x y / aR x y >-> rR x y}} -> {in aD & rD, forall x y, aR x (g y) -> rR (f x) y}. -Proof. by move=> Hf x y hx hy /Hf; rewrite fgK ?mem_g// ?inE; apply. Qed. +Proof. by move=> Hf x y hx hy /Hf; rw fgK ?mem_g// ?inE; apply. Qed. Lemma homo_mono_in : {in aD &, {homo f : x y / aR x y >-> rR x y}} -> @@ -2271,23 +2271,23 @@ Lemma homo_mono_in : {in rD &, {mono g : x y / rR x y >-> aR x y}}. Proof. move=> mf mg x y hx hy; case: (boolP (rR _ _))=> [/mg //|]; first exact. -by apply: contraNF=> /mf; rewrite !fgK ?mem_g//; apply. +by apply: contraNF=> /mf; rw !fgK ?mem_g//; apply. Qed. Lemma monoLR_in : {in aD &, {mono f : x y / aR x y >-> rR x y}} -> {in aD & rD, forall x y, rR (f x) y = aR x (g y)}. -Proof. by move=> mf x y hx hy; rewrite -{1}[y]fgK ?mem_g// mf ?mem_g. Qed. +Proof. by move=> mf x y hx hy; rw -{1}[y]fgK ?mem_g// mf ?mem_g. Qed. Lemma monoRL_in : {in aD &, {mono f : x y / aR x y >-> rR x y}} -> {in rD & aD, forall x y, rR x (f y) = aR (g x) y}. -Proof. by move=> mf x y hx hy; rewrite -{1}[x]fgK ?mem_g// mf ?mem_g. Qed. +Proof. by move=> mf x y hx hy; rw -{1}[x]fgK ?mem_g// mf ?mem_g. Qed. Lemma can_mono_in : {in aD &, {mono f : x y / aR x y >-> rR x y}} -> {in rD &, {mono g : x y / rR x y >-> aR x y}}. -Proof. by move=> mf x y hx hy; rewrite -mf ?mem_g// !fgK ?mem_g. Qed. +Proof. by move=> mf x y hx hy; rw -mf ?mem_g// !fgK ?mem_g. Qed. End MonoHomoMorphismTheory_in. Arguments homoRL_in {aT rT f g aD rD aR rR}. @@ -2373,15 +2373,15 @@ Variables (f : aT -> rT) (g : rT -> aT). Lemma inj_can_sym_in_on : {homo f : x / x \in aD >-> x \in rD} -> {in aD, {on rD, cancel f & g}} -> {in rD &, {on aD &, injective g}} -> {in rD, {on aD, cancel g & f}}. -Proof. by move=> fD fK gI x x_rD gx_aD; apply: gI; rewrite ?inE ?fK ?fD. Qed. +Proof. by move=> fD fK gI x x_rD gx_aD; apply: gI; rw ?inE ?fK ?fD. Qed. Lemma inj_can_sym_on : {in aD, cancel f g} -> {on aD &, injective g} -> {on aD, cancel g & f}. -Proof. by move=> fK gI x gx_aD; apply: gI; rewrite ?inE ?fK. Qed. +Proof. by move=> fK gI x gx_aD; apply: gI; rw ?inE ?fK. Qed. Lemma inj_can_sym_in : {homo f \o g : x / x \in rD} -> {on rD, cancel f & g} -> {in rD &, injective g} -> {in rD, cancel g f}. -Proof. by move=> fgD fK gI x x_rD; apply: gI; rewrite ?fK ?fgD. Qed. +Proof. by move=> fgD fK gI x x_rD; apply: gI; rw ?fK ?fgD. Qed. End inj_can_sym_in_on. Arguments inj_can_sym_in_on {aT rT aD rD f g}. diff --git a/theories/Corelib/ssr/ssrfun.v b/theories/Corelib/ssr/ssrfun.v index e5e5d1376680..fa714ce2f55c 100644 --- a/theories/Corelib/ssr/ssrfun.v +++ b/theories/Corelib/ssr/ssrfun.v @@ -445,7 +445,7 @@ Lemma frefl f : eqfun f f. Proof. by []. Qed. Lemma fsym f g : eqfun f g -> eqfun g f. Proof. by move=> eq_fg x. Qed. Lemma ftrans f g h : eqfun f g -> eqfun g h -> eqfun f h. -Proof. by move=> eq_fg eq_gh x; rewrite eq_fg. Qed. +Proof. by move=> eq_fg eq_gh x; rw eq_fg. Qed. Lemma rrefl r : eqrel r r. Proof. by []. Qed. @@ -470,7 +470,7 @@ 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 /comp eq_gg' eq_ff'. Qed. +Proof. by move=> eq_ff' eq_gg' x; rw /comp eq_gg' eq_ff'. Qed. End Composition. @@ -509,7 +509,7 @@ Proof. by []. Qed. Lemma omap_id (x : option rT) : omap id x = x. Proof. by case: x. Qed. Lemma eq_omap (h : aT -> rT) : f =1 h -> omap f =1 omap h. -Proof. by move=> Ef [?|] //=; rewrite Ef. Qed. +Proof. by move=> Ef [?|] //=; rw Ef. Qed. Lemma omapEapp : omap f = oapp (olift f) None. Proof. by []. Qed. @@ -680,7 +680,7 @@ Lemma can_pcan g : cancel g -> pcancel (fun y => Some (g y)). Proof. by move=> fK x; congr (Some _). Qed. Lemma pcan_inj g : pcancel g -> injective. -Proof. by move=> fK x y /(congr1 g); rewrite !fK => [[]]. Qed. +Proof. by move=> fK x y /(congr1 g); rw !fK => [[]]. Qed. Lemma can_inj g : cancel g -> injective. Proof. by move/can_pcan; apply: pcan_inj. Qed. @@ -707,7 +707,7 @@ Proof. by move=> injf [?|] [?|] //= [/injf->]. Qed. Lemma omapK {aT rT : Type} (f : aT -> rT) (g : rT -> aT) : cancel f g -> cancel (omap f) (omap g). -Proof. by move=> fK [?|] //=; rewrite fK. Qed. +Proof. by move=> fK [?|] //=; rw fK. Qed. Lemma of_voidK T : pcancel (of_void T) [fun _ => None]. Proof. by case. Qed. @@ -736,28 +736,28 @@ Lemma inj_compr : injective (f \o h) -> injective h. Proof. by move=> injfh x y /(congr1 f) /injfh. Qed. Lemma can_comp f' h' : cancel f f' -> cancel h h' -> cancel (f \o h) (h' \o f'). -Proof. by move=> fK hK x; rewrite /= fK hK. Qed. +Proof. by move=> fK hK x; rw /= fK hK. Qed. Lemma pcan_pcomp f' h' : pcancel f f' -> pcancel h h' -> pcancel (f \o h) (pcomp h' f'). -Proof. by move=> fK hK x; rewrite /pcomp fK /= hK. Qed. +Proof. by move=> fK hK x; rw /pcomp fK /= hK. Qed. Lemma ocan_comp [fo : B -> option A] [ho : C -> option B] [f' : A -> B] [h' : B -> C] : ocancel fo f' -> ocancel ho h' -> ocancel (obind fo \o ho) (h' \o f'). Proof. -move=> fK hK c /=; rewrite -[RHS]hK/=; case hcE : (ho c) => [b|]//=. -by rewrite -[b in RHS]fK; case: (fo b) => //=; have := hK c; rewrite hcE. +move=> fK hK c /=; rw -[RHS]hK/=; case hcE : (ho c) => [b|]//=. +by rw -[b in RHS]fK; case: (fo b) => //=; have := hK c; rw hcE. Qed. Lemma eq_inj : injective f -> f =1 g -> injective g. -Proof. by move=> injf eqfg x y; rewrite -2!eqfg; apply: injf. Qed. +Proof. by move=> injf eqfg x y; rw -2!eqfg; apply: injf. Qed. Lemma eq_can f' g' : cancel f f' -> f =1 g -> f' =1 g' -> cancel g g'. -Proof. by move=> fK eqfg eqfg' x; rewrite -eqfg -eqfg'. Qed. +Proof. by move=> fK eqfg eqfg' x; rw -eqfg -eqfg'. Qed. Lemma inj_can_eq f' : cancel f f' -> injective f' -> cancel g f' -> f =1 g. -Proof. by move=> fK injf' gK x; apply: injf'; rewrite fK. Qed. +Proof. by move=> fK injf' gK x; apply: injf'; rw fK. Qed. End InjectionsTheory. @@ -775,7 +775,7 @@ Proof. by case: bijf => g fK _; apply: can_inj fK. Qed. Lemma bij_can_sym f' : cancel f' f <-> cancel f f'. Proof. split=> fK; first exact: inj_can_sym fK bij_inj. -by case: bijf => h _ hK x; rewrite -[x]hK fK. +by case: bijf => h _ hK x; rw -[x]hK fK. Qed. Lemma bij_can_eq f' f'' : cancel f f' -> cancel f f'' -> f' =1 f''. From c4a7ced9d945fadcf8e2a1db048d8ef6581c800c Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 20 Mar 2026 08:13:20 +0100 Subject: [PATCH 09/11] [ssreflect] Deprecate rewrite --- plugins/ltac/tacinterp.mli | 1 + plugins/ssrrewrite/ssrrewrite.mlg | 10 +++++++++- 2 files changed, 10 insertions(+), 1 deletion(-) diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli index ff39394f29c8..d9394b101ccb 100644 --- a/plugins/ltac/tacinterp.mli +++ b/plugins/ltac/tacinterp.mli @@ -48,6 +48,7 @@ open Genintern val f_avoid_ids : Id.Set.t TacStore.field val f_debug : debug_info TacStore.field +val extract_loc : interp_sign -> Loc.t option val extract_ltac_constr_values : interp_sign -> Environ.env -> Ltac_pretype.constr_under_binders Id.Map.t diff --git a/plugins/ssrrewrite/ssrrewrite.mlg b/plugins/ssrrewrite/ssrrewrite.mlg index c6d7feb5423a..cf1667041ffa 100644 --- a/plugins/ssrrewrite/ssrrewrite.mlg +++ b/plugins/ssrrewrite/ssrrewrite.mlg @@ -18,6 +18,11 @@ open Ssreflect_plugin.Ssrequality open Ssreflect_plugin.Ssrparser open Ssreflect_plugin.Ssrtacs +let warn_deprecated_rewrite = + CWarnings.create ~name:"rewrite-rw" ~category:Deprecation.Version.v9_3 + ~quickfix:(fun ~loc () -> [Quickfix.make ~loc (Pp.str "rw")]) + (fun () -> Pp.str "The 'rewrite' tactic has been renamed 'rw'.") + } DECLARE PLUGIN "rocq-runtime.plugins.ssreflect_rewrite" @@ -67,7 +72,10 @@ END TACTIC EXTEND ssrrewrite | [ "rewrite" ssrrewriteargs(args) ssrclauses(clauses) ] -> - { tclCLAUSES (ssrrewritetac ist args) clauses } + { let loc = Tacinterp.extract_loc ist + |> Option.map (fun l -> Loc.sub l 0 7) in + warn_deprecated_rewrite ?loc (); + tclCLAUSES (ssrrewritetac ist args) clauses } END { From 90ad5409bc7adf3bae5ae0a49e0b803ce97a801d Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 20 Mar 2026 07:56:45 +0100 Subject: [PATCH 10/11] Update doc --- doc/sphinx/addendum/generalized-rewriting.rst | 2 +- doc/sphinx/changes.rst | 4 +- .../proof-engine/ssreflect-proof-language.rst | 573 +++++++++--------- 3 files changed, 295 insertions(+), 284 deletions(-) diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index 5bb8b9770bdf..0c6366c5dd7d 100644 --- a/doc/sphinx/addendum/generalized-rewriting.rst +++ b/doc/sphinx/addendum/generalized-rewriting.rst @@ -484,7 +484,7 @@ It is used in two cases: constraint can be automatically discharged. + Compatibility with ssreflect's rewrite: - The :tacn:`rewrite (ssreflect)` tactic uses generalized rewriting when possible, by + The :tacn:`rw` tactic uses generalized rewriting when possible, by checking that a ``RewriteRelation R`` instance exists when rewriting with a term of type ``R t u``. diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 6450a6b721e3..73e7fab18dea 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -10079,7 +10079,7 @@ Changes in 8.11+beta1 relation. More precisely, assume the given context lemma has type `forall f1 f2, .. -> (forall i, R1 (f1 i) (f2 i)) -> R2 f1 f2`. The first step performed by :tacn:`under` (since Coq 8.10) amounts to - calling the tactic :tacn:`rewrite `, which + calling the tactic :tacn:`rw`, which itself relies on :tacn:`setoid_rewrite` if need be. So this step was already compatible with a double implication or setoid equality for the conclusion head symbol `R2`. But a further step consists in @@ -11109,7 +11109,7 @@ Many bug fixes and documentation improvements, in particular: by Andreas Lynge, review by Enrico Tassi) - Make the ``rewrite /t`` tactic work together with :flag:`Universe Polymorphism`. - This makes :tacn:`rewrite ` compatible with the HoTT + This makes :tacn:`rw` compatible with the HoTT library https://github.com/HoTT/HoTT (`#10305 `_, fixes `#9336 `_, diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 084877a27cf3..a94a6d1cdd2d 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -55,11 +55,11 @@ such as tactics to mix forward steps and generalizations as |SSR| adopts the point of view that rewriting, definition expansion and partial evaluation participate all to a same concept of rewriting a goal in a larger sense. As such, all these functionalities -are provided by the :tacn:`rewrite ` tactic. +are provided by the :tacn:`rw` tactic. |SSR| includes a little language of patterns to select subterms in tactics or tacticals where it matters. Its most notable application is -in the :tacn:`rewrite ` tactic, where patterns are +in the :tacn:`rw` tactic, where patterns are used to specify where the rewriting step has to take place. Finally, |SSR| supports so-called reflection steps, typically @@ -68,8 +68,7 @@ logical view of a concept. To conclude, it is worth mentioning that |SSR| tactics can be mixed with non-|SSR| tactics in the same proof, or in the same Ltac -expression. The few exceptions to this statement are described in -section :ref:`compatibility_issues_ssr`. +expression. Acknowledgments @@ -86,9 +85,15 @@ Usage Getting started ~~~~~~~~~~~~~~~ -To be available, the tactics presented in this manual need the -following minimal set of libraries to be loaded: ``ssreflect.v``, -``ssrfun.v`` and ``ssrbool.v``. +To be available, the tactics presented in this manual need +``ssreflect_rw.v`` to be loaded. + +.. note:: + One can also load ``ssreflect.v`` to get the deprecated ``rewrite`` + tactic alias for :tacn:`rw` as well as the ``if is isn't then _ else _`` syntax specialised to booleans. + Moreover, these tactics come with a methodology specific to the authors of |SSR| and which requires a few options to be set in a different way than in their default way. All in all, @@ -96,7 +101,7 @@ this corresponds to working in the following context: .. rocqtop:: in - From Corelib Require Import ssreflect ssrfun ssrbool. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -105,64 +110,6 @@ this corresponds to working in the following context: :flag:`Implicit Arguments`, :flag:`Strict Implicit`, :flag:`Printing Implicit Defensive` -.. _compatibility_issues_ssr: - - -Compatibility issues -~~~~~~~~~~~~~~~~~~~~ - -Requiring the above modules creates an environment that is mostly -compatible with the rest of Rocq, up to a few discrepancies. - - -+ New keywords (``is``) might clash with variable, constant, tactic or - tactical names, or with quasi-keywords in tactic or - notation commands. -+ New tactic(al)s names (:tacn:`last`, :tacn:`done`, :tacn:`have`, :tacn:`suffices`, - :tacn:`suff`, :tacn:`without loss`, :tacn:`wlog`, :tacn:`congr`, :tacn:`unlock`) - might clash with user tactic names. -+ The extensions to the :tacn:`rewrite` tactic are partly incompatible with those - available in current versions of Rocq; in particular, ``rewrite .. in - (type of k)`` or ``rewrite .. in *`` or any other variant of :tacn:`rewrite` - will not work, and the |SSR| syntax and semantics for occurrence selection - and rule chaining are different. Use an explicit rewrite direction - (``rewrite <- …`` or ``rewrite -> …``) to access the Rocq rewrite tactic. -+ New symbols (``//``, ``/=``, ``//=``) might clash with adjacent - existing symbols. - This can be avoided by inserting white spaces. -+ New constant and theorem names might clash with the user theory. - This can be avoided by not importing all of |SSR|: - - .. rocqtop:: in - - From Corelib Require ssreflect. - Import ssreflect.SsrSyntax. - - Note that the full - syntax of |SSR|’s rewrite and reserved identifiers are enabled - only if the ssreflect module has been required and if ``SsrSyntax`` has - been imported. Thus a file that requires (without importing) ``ssreflect`` - and imports ``SsrSyntax`` can be required and imported without - automatically enabling |SSR|’s extended rewrite syntax and - reserved identifiers. -+ Some user notations (in particular, defining an infix ``;``) might - interfere with the "open term", parenthesis-free syntax of tactics - such as :tacn:`have`, :tacn:`set (ssreflect)` and :tacn:`pose (ssreflect)`. -+ The generalization of ``if`` statements to non-Boolean conditions is turned off - by |SSR|, because it is mostly subsumed by Coercion to ``bool`` of the - ``sumXXX`` types (declared in ``ssrfun.v``) and the - :n:`if @term is @pattern then @term else @term` construct - (see :ref:`pattern_conditional_ssr`). To use the - generalized form, turn off the |SSR| Boolean ``if`` notation using the command: - ``Close Scope boolean_if_scope``. -+ The following flags can be unset to make |SSR| more compatible with - parts of Rocq. - -.. flag:: SsrRewrite - - Controls whether the incompatible rewrite syntax is enabled (the default). - Disabling the :term:`flag` makes the syntax compatible with other parts of Rocq. - Gallina extensions -------------------- @@ -204,7 +151,7 @@ construct differs from the latter as follows. .. rocqtop:: reset none - From Corelib Require Import ssreflect. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -244,7 +191,8 @@ dependent pattern matching and for aliasing the pattern (see Pattern conditional ~~~~~~~~~~~~~~~~~~~ -The following construct can be used for a refutable pattern matching, +When doing ``From Corelib Require Import ssreflect`` (not ``ssreflect_rw``), +the following construct can be used for a refutable pattern matching, that is, pattern testing: .. prodn:: @@ -262,15 +210,16 @@ example, the null and all list function(al)s can be defined as follows: .. rocqtop:: reset none - From Corelib Require Import ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. - Section Test. .. rocqtop:: all - Variable d: Set. + From Corelib Require Import ssreflect. + + Section Test. + Variable d : Set. Definition null (s : list d) := if s is nil then true else false. Variable a : d -> bool. @@ -298,13 +247,15 @@ The latter appears to be marginally shorter, but it is quite ambiguous, and indeed often requires an explicit annotation ``(term : {_} + {_})`` to type check, which evens the character count. -Therefore, |SSR| restricts by default the condition of a plain ``if`` +Therefore, ``From Corelib Require Import ssreflect`` restricts by default the condition of a plain ``if`` construct to the standard ``bool`` type; this avoids spurious type annotations. .. example:: - .. rocqtop:: all + .. rocqtop:: reset all + + From Corelib Require Import ssreflect. Definition orb b1 b2 := if b1 then true else b2. @@ -363,7 +314,7 @@ expressions such as .. rocqtop:: reset none - From Corelib Require Import ssreflect. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -388,7 +339,7 @@ each point of use; e.g., the above definition can be written: .. rocqtop:: reset none - From Corelib Require Import ssreflect. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -433,16 +384,12 @@ Anonymous arguments When in a definition, the type of a certain argument is mandatory, but not its name, one usually uses “arrow” abstractions for prenex -arguments, or the ``(_ : term)`` syntax for inner arguments. In |SSR|, -the latter can be replaced by the open syntax ``of term`` or -(equivalently) ``& term``, which are both syntactically equivalent to a -``(_ : term)`` expression. This feature almost behaves as the -following extension of the binder syntax: +arguments, or the ``(_ : term)`` syntax for inner arguments. +The latter can be replaced by the open syntax ``& term``, +which is syntactically equivalent to a +``(_ : term)`` expression. -.. prodn:: - binder += {| & @term | of @term } - -Caveat: ``& T`` and ``of T`` abbreviations have to appear at the end +Caveat: ``& T`` abbreviations have to appear at the end of a binder list. For instance, the usual two-constructor polymorphic type list, i.e., the one of the standard ``List`` library, can be defined by the following declaration: @@ -451,14 +398,13 @@ defined by the following declaration: .. rocqtop:: reset none - From Corelib Require Import ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. .. rocqtop:: all - Inductive list (A : Type) : Type := nil | cons of A & list A. + Inductive list (A : Type) : Type := nil | cons & A & list A. Wildcards @@ -505,7 +451,7 @@ For example, the tactic :tacn:`pose (ssreflect)` supports parameters: .. rocqtop:: reset none - From Corelib Require Import ssreflect. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -620,7 +566,7 @@ where: .. rocqtop:: reset none - From Corelib Require Import ssreflect. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -668,7 +614,7 @@ conditions. .. rocqtop:: reset none - From Corelib Require Import ssreflect. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -689,7 +635,7 @@ conditions. .. rocqtop:: reset none - From Corelib Require Import ssreflect. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -710,7 +656,7 @@ Moreover: .. rocqtop:: reset none - From Corelib Require Import ssreflect. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -730,7 +676,7 @@ Moreover: .. rocqtop:: reset none - From Corelib Require Import ssreflect. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -763,7 +709,7 @@ An *occurrence switch* can be: .. rocqtop:: reset none - From Corelib Require Import ssreflect. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -785,7 +731,7 @@ An *occurrence switch* can be: .. rocqtop:: reset none - From Corelib Require Import ssreflect. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -806,7 +752,7 @@ An *occurrence switch* can be: .. rocqtop:: reset none - From Corelib Require Import ssreflect. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -837,7 +783,7 @@ selection. .. rocqtop:: reset none - From Corelib Require Import ssreflect. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -854,7 +800,7 @@ only one occurrence of the selected term. .. rocqtop:: reset none - From Corelib Require Import ssreflect. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -885,7 +831,7 @@ context of a goal thanks to the ``in`` tactical. .. rocqtop:: reset none - From Corelib Require Import ssreflect. + From Corelib Require Import ssreflect_rw. .. rocqtop:: all @@ -901,7 +847,7 @@ context of a goal thanks to the ``in`` tactical. .. rocqtop:: reset none - From Corelib Require Import ssreflect. + From Corelib Require Import ssreflect_rw. .. rocqtop:: all @@ -1017,7 +963,7 @@ constants to the goal. .. rocqtop:: reset none - From Corelib Require Import ssreflect. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -1078,7 +1024,7 @@ The ``:`` tactical is used to operate on an element in the context. .. rocqtop:: reset none - From Corelib Require Import ssreflect. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -1173,7 +1119,7 @@ The move tactic. .. rocqtop:: reset all - Require Import ssreflect. + From Corelib Require Import ssreflect_rw. Goal not False. move. @@ -1243,7 +1189,7 @@ The elim tactic .. rocqtop:: reset none - From Corelib Require Import ssreflect. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -1283,7 +1229,7 @@ existential metavariables of sort :g:`Prop`. .. rocqtop:: reset none - From Corelib Require Import ssreflect. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -1430,7 +1376,7 @@ If the tactic is ``move`` or ``case`` and an equation :token:`ident` is given, t (step 3) for :token:`d_item` is suppressed (see Section :ref:`generation_of_equations_ssr`). Intro patterns (see Section :ref:`introduction_ssr`) -and the ``rewrite`` tactic (see Section :ref:`rewriting_ssr`) +and the ``rw`` tactic (see Section :ref:`rewriting_ssr`) let one place a :token:`clear_switch` in the middle of other items (namely identifiers, views and rewrite rules). This can trigger the addition of proof context items to the ones being explicitly @@ -1463,7 +1409,7 @@ context to interpret wildcards; in particular, it can accommodate the .. rocqtop:: reset none - From Corelib Require Import ssreflect. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -1701,7 +1647,7 @@ Intro patterns (resp. :token:`occ_switch` ``<-``) pops the top assumption (which should be a rewritable proposition) into an anonymous fact, rewrites (resp. rewrites right to left) the goal with this - fact (using the |SSR| ``rewrite`` tactic described in Section + fact (using the |SSR| ``rw`` tactic described in Section :ref:`rewriting_ssr`, and honoring the optional occurrence selector), and finally deletes the anonymous fact from the context. ``[`` :token:`i_item` * ``| … |`` :token:`i_item` * ``]`` @@ -1755,13 +1701,15 @@ Clears are deferred until the end of the intro pattern. .. rocqtop:: reset none - From Corelib Require Import ssreflect ssrbool. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. .. rocqtop:: all + From Corelib Require Import ssrbool. + Lemma test x y : Nat.leb 0 x = true -> (Nat.leb 0 x) && (Nat.leb y 2) = true. move=> {x} ->. @@ -1816,7 +1764,7 @@ Block introduction .. rocqtop:: reset none - From Corelib Require Import ssreflect. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -1869,7 +1817,7 @@ deal with the possible parameters of the constants introduced. .. rocqtop:: reset none - From Corelib Require Import ssreflect. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -1888,7 +1836,7 @@ under fresh |SSR| names. .. rocqtop:: reset none - From Corelib Require Import ssreflect. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -1955,7 +1903,7 @@ be substituted. .. rocqtop:: reset none - From Corelib Require Import ssreflect. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -2061,20 +2009,20 @@ of the time more than two levels of indentation. Here is a fragment of such a structured script:: case E1: (abezoutn _ _) => [[| k1] [| k2]]. - - rewrite !muln0 !gexpn0 mulg1 => H1. - move/eqP: (sym_equal F0); rewrite -H1 orderg1 eqn_mul1. + - rw !muln0 !gexpn0 mulg1 => H1. + move/eqP: (sym_equal F0); rw -H1 orderg1 eqn_mul1. by case/andP; move/eqP. - - rewrite muln0 gexpn0 mulg1 => H1. + - rw muln0 gexpn0 mulg1 => H1. have F1: t %| t * S k2.+1 - 1. - apply: (@dvdn_trans (orderg x)); first by rewrite F0; exact: dvdn_mull. - rewrite orderg_dvd; apply/eqP; apply: (mulgI x). - rewrite -{1}(gexpn1 x) mulg1 gexpn_add leq_add_sub //. + apply: (@dvdn_trans (orderg x)); first by rw F0; exact: dvdn_mull. + rw orderg_dvd; apply/eqP; apply: (mulgI x). + rw -{1}(gexpn1 x) mulg1 gexpn_add leq_add_sub //. by move: P1; case t. - rewrite dvdn_subr in F1; last by exact: dvdn_mulr. - + rewrite H1 F0 -{2}(muln1 (p ^ l)); congr (_ * _). - by apply/eqP; rewrite -dvdn1. + rw dvdn_subr in F1; last by exact: dvdn_mulr. + + rw H1 F0 -{2}(muln1 (p ^ l)); congr (_ * _). + by apply/eqP; rw -dvdn1. + by move: P1; case: (t) => [| [| s1]]. - - rewrite muln0 gexpn0 mul1g => H1. + - rw muln0 gexpn0 mul1g => H1. ... @@ -2109,7 +2057,7 @@ with a ``by``, like in: .. rocqdoc:: - by apply/eqP; rewrite -dvdn1. + by apply/eqP; rw -dvdn1. .. tacn:: done :name: done @@ -2128,7 +2076,7 @@ with a ``by``, like in: Ltac done := trivial; hnf; intros; solve - [ do ![solve [trivial | apply: sym_equal; trivial] + [ do ![solve [trivial | simple refine (@sym_equal _ _ _ _); trivial] | discriminate | contradiction | split] | match goal with H : ~ _ |- _ => solve [case H; trivial] end ]. @@ -2174,19 +2122,19 @@ is equivalent to: .. rocqdoc:: - by rewrite my_lemma1. + by rw my_lemma1. succeeds, then the tactic: .. rocqdoc:: - by rewrite my_lemma1; apply my_lemma2. + by rw my_lemma1; apply my_lemma2. usually fails since it is equivalent to: .. rocqdoc:: - by (rewrite my_lemma1; apply my_lemma2). + by (rw my_lemma1; apply my_lemma2). .. _selectors_ssr: @@ -2256,7 +2204,7 @@ to the others. .. rocqtop:: reset none - From Corelib Require Import ssreflect. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -2322,14 +2270,14 @@ For instance, the tactic: .. rocqdoc:: - tactic; do 1? rewrite mult_comm. + tactic; do 1? rw mult_comm. rewrites at most one time the lemma ``mult_comm`` in all the subgoals generated by tactic, whereas the tactic: .. rocqdoc:: - tactic; do 2! rewrite mult_comm. + tactic; do 2! rw mult_comm. rewrites exactly two times the lemma ``mult_comm`` in all the subgoals generated by ``tactic``, and fails if this rewrite is not possible in some @@ -2354,7 +2302,7 @@ already presented the *localization* tactical ``in``, whose general syntax is: where :token:`ident` is a name in the context. On the left side of ``in``, -:token:`tactic` can be ``move``, ``case``, ``elim``, ``rewrite``, ``set``, +:token:`tactic` can be ``move``, ``case``, ``elim``, ``rw``, ``set``, or any tactic formed with the general iteration tactical ``do`` (see Section :ref:`iteration_ssr`). @@ -2375,14 +2323,14 @@ between standard Ltac ``in`` and the |SSR| tactical in. .. rocqtop:: reset none - From Corelib Require Import ssreflect. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. .. rocqtop:: all - Ltac mytac H := rewrite H. + Ltac mytac H := rw H. Lemma test x y (H1 : x = y) (H2 : y = 3) : x + y = 6. do [mytac H2] in H1 *. @@ -2393,7 +2341,7 @@ between standard Ltac ``in`` and the |SSR| tactical in. By default, ``in`` keeps the body of local definitions. To erase the body of a local definition during the generalization phase, the name of the local definition must be written between parentheses, like in -``rewrite H in H1 (def_n) H2.`` +``rw H in H1 (def_n) H2.`` .. tacv:: @tactic in {+ {| @clear_switch | {? @}@ident | ( @ident ) | ( {? @}@ident := @c_pattern ) } } {? * } @@ -2450,7 +2398,7 @@ the holes are abstracted in term. .. rocqtop:: reset none - From Corelib Require Import ssreflect. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -2464,7 +2412,7 @@ the holes are abstracted in term. .. rocqtop:: reset none - From Corelib Require Import ssreflect. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -2482,7 +2430,7 @@ tactic: .. rocqtop:: reset none - From Corelib Require Import ssreflect. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -2526,7 +2474,7 @@ statement is very short, basically when it fits in one line like in: .. rocqdoc:: - have H23 : 3 + 2 = 2 + 3 by rewrite addnC. + have H23 : 3 + 2 = 2 + 3 by rw addnC. The possibility of using :token:`i_item` supplies a very concise syntax for the further use of the intermediate step. For instance, @@ -2535,7 +2483,7 @@ the further use of the intermediate step. For instance, .. rocqtop:: reset none - From Corelib Require Import ssreflect. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -2563,7 +2511,7 @@ destruction of existential assumptions like in the tactic: .. rocqtop:: reset none - From Corelib Require Import ssreflect. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -2590,7 +2538,7 @@ term for the intermediate lemma, using tactics of the form: .. rocqtop:: reset none - From Corelib Require Import ssreflect. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -2610,16 +2558,18 @@ The following example requires the mathcomp and mczify libraries. .. example:: - .. rocqtop:: reset none warn extra-mathcomp extra-mczify - - From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat zify. + .. rocqtop:: reset none Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. + Set Warnings "-notation-overridden". .. rocqtop:: all extra-mathcomp extra-mczify + From Corelib Require Import ssreflect_rw. + From mathcomp Require Import ssrfun ssrbool ssrnat zify. + Lemma test : True. have H x (y : nat) : 2 * x + y = x + x + y by lia. @@ -2732,7 +2682,7 @@ typeclass inference. .. rocqtop:: reset none - From Corelib Require Import ssreflect. + From Corelib Require Import ssreflect_rw. Axiom ty : Type. Axiom t : ty. @@ -2877,16 +2827,19 @@ simplifies a proof. Here is an example showing the beginning of the proof that quotient and reminder of natural number euclidean division are unique. -The following example requires the mathcomp and mczify libraries. +The following example requires the mathcomp library. .. example:: - .. rocqtop:: reset none warn extra-mathcomp + .. rocqtop:: reset none - From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat. + Set Warnings "-notation-overridden". .. rocqtop:: all extra-mathcomp + From Corelib Require Import ssreflect_rw. + From mathcomp Require Import ssrfun ssrbool ssrnat. + Lemma quo_rem_unicity d q1 q2 r1 r2 : q1*d + r1 = q2*d + r2 -> r1 < d -> r2 < d -> (q1, r1) = (q2, r2). wlog: q1 q2 r1 r2 / q1 <= q2. @@ -2908,7 +2861,7 @@ pattern will be used to process its instance. .. rocqtop:: reset none - From Corelib Require Import ssreflect ssrfun ssrbool. + From Corelib Require Import ssreflect_rw ssrfun ssrbool. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -2958,7 +2911,7 @@ illustrated in the following example. .. rocqtop:: reset none - From Corelib Require Import ssreflect. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -2977,7 +2930,7 @@ illustrated in the following example. .. rocqtop:: reset none - From Corelib Require Import ssreflect. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -3002,7 +2955,7 @@ intermediate results handled are properties of effectively computable functions. The most efficient means of establishing such results are computation and simplification of expressions involving such functions, i.e., rewriting. |SSR| therefore includes an -extended ``rewrite`` tactic that unifies and combines most of the +extended ``rw`` tactic that unifies and combines most of the rewriting functionalities. @@ -3021,8 +2974,7 @@ The main features of the rewrite tactic are: The general form of an |SSR| rewrite tactic is: -.. tacn:: rewrite {+ @rstep } - :name: rewrite (ssreflect) +.. tacn:: rw {+ @rstep } :undocumented: The combination of a rewrite tactic with the ``in`` tactical (see Section @@ -3072,7 +3024,7 @@ operation should be performed. :token:`r_item` is actually processed and is complemented with the name of the rewrite rule if and only if it is a simple proof context entry [#10]_. As a consequence, one can - write ``rewrite {}H`` to rewrite with ``H`` and dispose ``H`` immediately + write ``rw {}H`` to rewrite with ``H`` and dispose ``H`` immediately afterwards. This behavior can be avoided by putting parentheses around the rewrite rule. @@ -3084,16 +3036,16 @@ A :token:`r_item` can be one of the following. :ref:`introduction_ssr`). Simplification operations are intertwined with the possible other rewrite operations specified by the list of :token:`r_item`. + A *folding/unfolding* :token:`r_item`. The tactic - ``rewrite /term`` unfolds the + ``rw /term`` unfolds the :term:`head constant` of ``term`` in every occurrence of the first matching of ``term`` in the goal. In particular, if ``my_def`` is a (local or global) - defined constant, the tactic ``rewrite /my_def.`` is analogous to: + defined constant, the tactic ``rw /my_def.`` is analogous to: ``unfold my_def``. - Conversely, ``rewrite -/my_def.`` is equivalent to ``fold my_def``. + Conversely, ``rw -/my_def.`` is equivalent to ``fold my_def``. When an unfold :token:`r_item` is combined with a redex pattern, a conversion operation is performed. A tactic of the form - ``rewrite -[term1]/term2.`` + ``rw -[term1]/term2.`` is equivalent to ``change term1 with term2.`` If ``term2`` is a single constant and ``term1`` head symbol is not ``term2``, then the head symbol of ``term1`` is repeatedly unfolded until ``term2`` appears. @@ -3103,15 +3055,15 @@ A :token:`r_item` can be one of the following. ``eq`` is the Leibniz equality or a registered setoid equality; + a list of terms ``(t1 ,…,tn)``, each ``ti`` having a type as above, and - the tactic ``rewrite r_prefix (t1 ,…,tn ).`` - is equivalent to ``do [rewrite r_prefix t1 | … | rewrite r_prefix tn ].``; + the tactic ``rw r_prefix (t1 ,…,tn ).`` + is equivalent to ``do [rw r_prefix t1 | … | rw r_prefix tn ].``; + an anonymous rewrite lemma ``(_ : term)``, where ``term`` has a type as above. .. example:: .. rocqtop:: reset none - From Corelib Require Import ssreflect. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -3121,7 +3073,7 @@ A :token:`r_item` can be one of the following. Definition double x := x + x. Definition ddouble x := double (double x). Lemma test x : ddouble x = 4 * x. - rewrite [ddouble _]/double. + rw [ddouble _]/double. .. warning:: @@ -3135,13 +3087,13 @@ A :token:`r_item` can be one of the following. .. rocqtop:: all fail - rewrite -[f y]/(y + _). + rw -[f y]/(y + _). but the following script succeeds .. rocqtop:: all - rewrite -[f y x]/(y + _). + rw -[f y x]/(y + _). .. flag:: SsrOldRewriteGoalsOrder @@ -3172,7 +3124,7 @@ In a rewrite tactic of the form: .. rocqdoc:: - rewrite occ_switch [term1]term2. + rw occ_switch [term1]term2. ``term1`` is the explicit rewrite redex and ``term2`` is the rewrite rule. This execution of this tactic unfolds as follows. @@ -3215,7 +3167,7 @@ tactic: .. rocqdoc:: - rewrite /my_def {2}[f _]/= my_eq //=. + rw /my_def {2}[f _]/= my_eq //=. unfolds ``my_def`` in the goal, simplifies the second occurrence of the @@ -3230,7 +3182,7 @@ proof of basic results on natural numbers arithmetic. .. rocqtop:: reset none - From Corelib Require Import ssreflect. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -3242,11 +3194,11 @@ proof of basic results on natural numbers arithmetic. Axiom addSnnS : forall m n, S m + n = m + S n. Lemma addnCA m n p : m + (n + p) = n + (m + p). - by elim: m p => [ | m Hrec] p; rewrite ?addSnnS -?addnS. + by elim: m p => [ | m Hrec] p; rw ?addSnnS -?addnS. Qed. Lemma addnC n m : m + n = n + m. - by rewrite -{1}[n]addn0 addnCA addn0. + by rw -{1}[n]addn0 addnCA addn0. Qed. Note the use of the ``?`` switch for parallel rewrite operations in the @@ -3266,7 +3218,7 @@ side of the equality the user wants to rewrite. .. rocqtop:: reset none - From Corelib Require Import ssreflect. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -3274,7 +3226,7 @@ side of the equality the user wants to rewrite. .. rocqtop:: all Lemma test (H : forall t u, t + u = u + t) x y : x + y = y + x. - rewrite [y + _]H. + rw [y + _]H. Note that if this first pattern matching is not compatible with the :token:`r_item`, the rewrite fails, even if the goal contains a @@ -3286,7 +3238,7 @@ the equality. .. rocqtop:: reset none - From Corelib Require Import ssreflect. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -3294,7 +3246,7 @@ the equality. .. rocqtop:: all Lemma test (H : forall t u, t + u * 0 = t) x y : x + y * 4 + 2 * 0 = x + 2 * 0. - Fail rewrite [x + _]H. + Fail rw [x + _]H. Indeed, the left-hand side of ``H`` does not match the redex identified by the pattern ``x + y * 4``. @@ -3309,7 +3261,7 @@ Occurrence switches and redex switches .. rocqtop:: reset none - From Corelib Require Import ssreflect. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -3317,7 +3269,7 @@ Occurrence switches and redex switches .. rocqtop:: all Lemma test x y : x + y + 0 = x + y + y + 0 + 0 + (x + y + 0). - rewrite {2}[_ + y + 0](_: forall z, z + 0 = z). + rw {2}[_ + y + 0](_: forall z, z + 0 = z). The second subgoal is generated by the use of an anonymous lemma in the rewrite tactic. The effect of the tactic on the initial goal is to @@ -3338,7 +3290,7 @@ repetition. .. rocqtop:: reset none - From Corelib Require Import ssreflect. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -3346,7 +3298,7 @@ repetition. .. rocqtop:: all Lemma test x y (z : nat) : x + 1 = x + y + 1. - rewrite 2!(_ : _ + 1 = z). + rw 2!(_ : _ + 1 = z). This last tactic generates *three* subgoals because the second rewrite operation specified with the ``2!`` multiplier @@ -3368,7 +3320,7 @@ rewrite operations prescribed by the rules on the current goal. .. rocqtop:: reset none - From Corelib Require Import ssreflect. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -3382,7 +3334,7 @@ rewrite operations prescribed by the rules on the current goal. Hypothesis eqac : a = c. Lemma test : a = a. - rewrite (eqab, eqac). + rw (eqab, eqac). Indeed, rule ``eqab`` is the first to apply among the ones gathered in the tuple passed to the rewrite tactic. This multirule @@ -3393,8 +3345,8 @@ rewrite operations prescribed by the rules on the current goal. Definition multi1 := (eqab, eqac). - In this case, the tactic ``rewrite multi1`` is a synonym for - ``rewrite (eqab, eqac)``. + In this case, the tactic ``rw multi1`` is a synonym for + ``rw (eqab, eqac)``. More precisely, a multirule rewrites the first subterm to which one of the rules applies in a left-to-right traversal of the goal, with the @@ -3412,7 +3364,7 @@ literal matches have priority. Definition multi2 := (eqab, eqd0). Lemma test : d = b. - rewrite multi2. + rw multi2. Indeed, rule ``eqd0`` applies without unfolding the definition of ``d``. @@ -3430,7 +3382,7 @@ repeated anew. Definition multi3 := (eq_adda_b, eq_adda_c, eqb0). Lemma test : 1 + a = 12 + a. - rewrite 2!multi3. + rw 2!multi3. It uses ``eq_adda_b`` then ``eqb0`` on the left-hand side only. Without the bound ``2``, one would obtain ``0 = 0``. @@ -3441,7 +3393,7 @@ to (universally) quantify over the parameters of a subset of rules (as there is special code that will omit unnecessary quantifiers for rules that can be syntactically extracted). It is also possible to reverse the direction of a rule subset, using a special dedicated syntax: the -tactic rewrite ``(=^~ multi1)`` is equivalent to ``rewrite multi1_rev``. +tactic rewrite ``(=^~ multi1)`` is equivalent to ``rw multi1_rev``. .. example:: @@ -3484,7 +3436,7 @@ the efficient operations, we gather all these rules in the definition Definition trecE := (addE, (doubleE, oddE), (mulE, add_mulE, (expE, mul_expE))). -The tactic ``rewrite !trecE.`` +The tactic ``rw !trecE.`` restores the naive version of each operation in a goal involving the efficient ones, e.g., for the purpose of a correctness proof. @@ -3493,16 +3445,16 @@ Wildcards vs abstractions ````````````````````````` The rewrite tactic supports :token:`r_item`\s containing holes. For example, in -the tactic ``rewrite (_ : _ * 0 = 0).``, +the tactic ``rw (_ : _ * 0 = 0).``, the term ``_ * 0 = 0`` is interpreted as ``forall n : nat, n * 0 = 0.`` Anyway this tactic is *not* equivalent to -``rewrite (_ : forall x, x * 0 = 0).``. +``rw (_ : forall x, x * 0 = 0).``. .. example:: .. rocqtop:: reset none - From Corelib Require Import ssreflect. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -3512,13 +3464,13 @@ Anyway this tactic is *not* equivalent to .. rocqtop:: all Lemma test y z : y * 0 + y * (z * 0) = 0. - rewrite (_ : _ * 0 = 0). + rw (_ : _ * 0 = 0). while the other tactic results in .. rocqtop:: all restart abort - rewrite (_ : forall x, x * 0 = 0). + rw (_ : forall x, x * 0 = 0). The first tactic requires you to prove the instance of the (missing) lemma that was used, while the latter requires you prove the quantified @@ -3552,7 +3504,7 @@ cases. .. rocqtop:: reset none - From Corelib Require Import ssreflect. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -3567,7 +3519,7 @@ cases. Lemma test : f 3 + f 3 = f 6. (* we call the standard rewrite tactic here *) - rewrite -> H. + rewrite H. This rewriting is not possible in |SSR|, because there is no occurrence of the head symbol ``f`` of the rewrite rule in the @@ -3575,23 +3527,23 @@ cases. .. rocqtop:: all restart fail - rewrite H. + rw H. Rewriting with ``H`` first requires unfolding the occurrences of ``f`` where the substitution is to be performed (here there is a single such - occurrence), using tactic ``rewrite /f`` (for a global replacement of - ``f`` by ``g``) or ``rewrite pattern/f``, for a finer selection. + occurrence), using tactic ``rw /f`` (for a global replacement of + ``f`` by ``g``) or ``rw pattern/f``, for a finer selection. .. rocqtop:: all restart - rewrite /f H. + rw /f H. Alternatively, one can override the pattern inferred from ``H`` .. rocqtop:: all restart - rewrite [f _]H. + rw [f _]H. Existential metavariables and rewriting @@ -3610,7 +3562,6 @@ corresponding new goals will be generated. .. rocqtop:: reset none - From Corelib Require Import ssreflect ssrfun ssrbool. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -3618,6 +3569,8 @@ corresponding new goals will be generated. .. rocqtop:: all abort + From Corelib Require Import ssreflect ssrfun ssrbool. + Axiom leq : nat -> nat -> bool. Notation "m <= n" := (leq m n) : nat_scope. Notation "m < n" := (S m <= n) : nat_scope. @@ -3630,11 +3583,11 @@ corresponding new goals will be generated. Axiom insubT : forall n x Px, insub n x = Some (Sub x Px). Lemma test (x : 'I_2) y : Some x = insub 2 y. - rewrite insubT. + rw insubT. Since the argument corresponding to ``Px`` is not supplied by the user, the resulting goal should be ``Some x = Some (Sub y ?Goal).`` - Instead, |SSR| ``rewrite`` tactic hides the existential variable. + Instead, |SSR| ``rw`` tactic hides the existential variable. As in :ref:`apply_ssr`, the ``ssrautoprop`` tactic is used to try to solve the existential variable. @@ -3642,7 +3595,7 @@ corresponding new goals will be generated. .. rocqtop:: all abort Lemma test (x : 'I_2) y (H : y < 2) : Some x = insub 2 y. - rewrite insubT. + rw insubT. As a temporary limitation, this behavior is available only if the @@ -3667,7 +3620,7 @@ complete terms, as shown by the simple example below. .. rocqtop:: reset none - From Corelib Require Import ssreflect. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -3690,7 +3643,7 @@ complete terms, as shown by the simple example below. .. rocqtop:: all fail - rewrite eq_map. + rw eq_map. as we need to explicitly provide the non-inferable argument ``F2``, which corresponds here to the term we want to obtain *after* the @@ -3699,8 +3652,8 @@ complete terms, as shown by the simple example below. .. rocqtop:: all abort - rewrite (@eq_map _ (fun _ : nat => 0)). - by move=> m; rewrite subnn. + rw (@eq_map _ (fun _ : nat => 0)). + by move=> m; rw subnn. The :tacn:`under` tactic lets one perform the same operation in a more convenient way: @@ -3708,7 +3661,7 @@ complete terms, as shown by the simple example below. .. rocqtop:: all abort Lemma example_map l : sumlist (map (fun m => m - m) l) = 0. - under eq_map => m do rewrite subnn. + under eq_map => m do rw subnn. The under tactic @@ -3746,7 +3699,7 @@ Let us redo the running example in interactive mode. Lemma example_map l : sumlist (map (fun m => m - m) l) = 0. under eq_map => m. - rewrite subnn. + rw subnn. over. The execution of the Ltac expression: @@ -3755,8 +3708,8 @@ The execution of the Ltac expression: involves the following steps. -1. It performs a :n:`rewrite @term` - without failing like in the first example with ``rewrite eq_map.``, +1. It performs a :n:`rw @term` + without failing like in the first example with ``rw eq_map.``, but creating evars (see :tacn:`evar`). If :n:`term` is prefixed by a pattern or an occurrence selector, then the modifiers are honoured. @@ -3774,7 +3727,8 @@ involves the following steps. registered relations (w.r.t. Class ``RewriteRelation``) between a term and an evar, e.g., ``m - m = ?F2 m`` in the running example. (This support for setoid-like relations is enabled as soon as one does - both ``Require Import ssreflect.`` and ``Require Setoid.``) + both ``From Corelib Require Import ssreflect_rw.`` + and ``From Corelib Require Setoid.``) 5. If so :tacn:`under` protects these n goals against an accidental instantiation of the evar. @@ -3858,7 +3812,7 @@ Notes: .. rocqtop:: reset none - From Corelib Require Import ssreflect. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -3922,7 +3876,7 @@ Notes: \sum_(0 <= i < m | prime i) \sum_(0 <= j < n | odd j) (j + i). under eq_bigr => i prime_i do under eq_big => [ j | j odd_j ] do - [ rewrite (muln1 j) | rewrite (addnC i j) ]. + [ rw (muln1 j) | rw (addnC i j) ]. Remark how the final goal uses the name ``i`` (the name given in the intro pattern) rather than ``a`` in the binder of the first summation. @@ -3965,21 +3919,22 @@ selective rewriting, blocking on the fly the reduction in the term ``t``. .. rocqtop:: reset none - From Corelib Require Import ssreflect ssrfun ssrbool. - From Corelib Require Import ListDef. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. - Section Test. .. rocqtop:: all + From Corelib Require Import ssreflect ssrfun ssrbool. + From Corelib Require Import ListDef. + Section Test. + Variable A : Type. Fixpoint has (p : A -> bool) (l : list A) : bool := if l is cons x l then p x || (has p l) else false. Lemma test p x y l (H : p x = true) : has p ( x :: y :: l) = true. - rewrite {2}[cons]lock /= -lock. + rw {2}[cons]lock /= -lock. It is sometimes desirable to globally prevent a definition from being expanded by simplification; this is done by adding ``locked`` in the @@ -3989,7 +3944,7 @@ definition. .. rocqtop:: reset none - From Corelib Require Import ssreflect. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -4000,7 +3955,7 @@ definition. Definition lid := locked (fun x : nat => x). Lemma test : lid 3 = 3. - rewrite /=. + rw /=. unlock lid. .. tacn:: unlock {? @occ_switch } @ident @@ -4060,7 +4015,7 @@ arithmetic operations. We define for instance: The operation ``addn`` behaves exactly like ``plus``, except that ``(addn (S n) m)`` will not simplify spontaneously to ``(S (addn n m))`` (the two terms, however, are convertible). -In addition, the unfolding step ``rewrite /addn`` +In addition, the unfolding step ``rw /addn`` will replace ``addn`` directly with ``plus``, so the ``nosimpl`` form is essentially invisible. @@ -4102,11 +4057,10 @@ which the function is supplied: .. rocqtop:: reset none - From Corelib Require Import ssreflect. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. - Section Test. .. rocqtop:: all @@ -4129,14 +4083,14 @@ which the function is supplied: .. rocqtop:: reset none - From Corelib Require Import ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. - Section Test. .. rocqtop:: all + From Corelib Require Import ssreflect. + Definition f n := if n is 0 then plus else mult. Definition g (n m : nat) := plus. @@ -4152,18 +4106,17 @@ which the function is supplied: .. rocqtop:: reset none - From Corelib Require Import ssreflect. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. - Section Test. .. rocqtop:: all Lemma test n m (Hnm : m <= n) : S m + (S n - S m) = S n. - congr S; rewrite -/plus. + congr S; rw -/plus. - The tactic ``rewrite -/plus`` folds back the expansion of ``plus``, + The tactic ``rw -/plus`` folds back the expansion of ``plus``, which was necessary for matching both sides of the equality with an application of ``S``. @@ -4173,11 +4126,10 @@ which the function is supplied: .. rocqtop:: reset none - From Corelib Require Import ssreflect. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. - Section Test. .. rocqtop:: all @@ -4240,7 +4192,7 @@ in the second column. The rewrite tactic supports two more patterns obtained prefixing the first two with ``in``. The intended meaning is that the pattern identifies -all subterms of the specified context. The ``rewrite`` tactic will infer a +all subterms of the specified context. The ``rw`` tactic will infer a pattern for the redex looking at the rule used for rewriting. .. list-table:: @@ -4274,11 +4226,11 @@ consider the goal ``a = b`` and the tactic .. rocqdoc:: - rewrite [in X in _ = X]rule. + rw [in X in _ = X]rule. It rewrites all occurrences of the left hand side of ``rule`` inside ``b`` only (``a``, and the hidden type of the equality, are ignored). Note that the -variant ``rewrite [X in _ = X]rule`` would have rewritten ``b`` +variant ``rw [X in _ = X]rule`` would have rewritten ``b`` exactly (i.e., it would only work if ``b`` and the left-hand side of rule can be unified). @@ -4353,17 +4305,16 @@ parentheses are required around more complex patterns. .. rocqtop:: reset none - From Corelib Require Import ssreflect. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. - Section Test. .. rocqtop:: all Lemma test a b : a + b + 1 = b + (a + 1). set t := (X in _ = X). - rewrite {}/t. + rw {}/t. set t := (a + _ in X in _ = X). @@ -4392,11 +4343,10 @@ Contextual patterns in rewrite .. rocqtop:: reset none - From Corelib Require Import ssreflect. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. - Section Test. .. rocqtop:: all @@ -4408,7 +4358,7 @@ Contextual patterns in rewrite Axiom addnC : forall m n, m + n = n + m. Lemma test x y z f : (x.+1 + y) + f (x.+1 + y) (z + (x + y).+1) = 0. - rewrite [in f _ _]addSn. + rw [in f _ _]addSn. Note: the simplification rule ``addSn`` is applied only under the ``f`` symbol. @@ -4416,7 +4366,7 @@ Contextual patterns in rewrite .. rocqtop:: all - rewrite addSn -[X in _ = X]addn0. + rw addSn -[X in _ = X]addn0. Note that the right-hand side of ``addn0`` is undetermined, but the rewrite pattern specifies the redex explicitly. The right-hand side @@ -4429,13 +4379,13 @@ Contextual patterns in rewrite .. rocqtop:: all - rewrite -{2}[in X in _ = X](addn0 0). + rw -{2}[in X in _ = X](addn0 0). The following tactic is quite tricky: .. rocqtop:: all - rewrite [_.+1 in X in f _ X](addnC x.+1). + rw [_.+1 in X in f _ X](addnC x.+1). The explicit redex ``_.+1`` is important, since its :term:`head constant` ``S`` differs from the head constant inferred from @@ -4455,7 +4405,7 @@ Contextual patterns in rewrite .. rocqtop:: all - rewrite [x.+1 + y as X in f X _]addnC. + rw [x.+1 + y as X in f X _]addnC. Patterns for recurrent contexts @@ -4482,7 +4432,7 @@ Shortcuts defined this way can be freely used in place of the trailing .. rocqdoc:: set rhs := RHS. - rewrite [in RHS]rule. + rw [in RHS]rule. case: (a + _ in RHS). @@ -4556,14 +4506,15 @@ generation (see Section :ref:`generation_of_equations_ssr`). .. rocqtop:: reset none - From Corelib Require Import ssreflect ListDef. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. - Section Test. .. rocqtop:: all + From Corelib Require Import ssreflect ListDef. + Section Test. + Variable d : Type. Fixpoint add_last (s : list d) (z : d) {struct s} : list d := if s is cons x s' then cons x (add_last s' z) else z :: nil. @@ -4631,7 +4582,7 @@ Here is an example of a regular, but nontrivial, eliminator. .. rocqtop:: reset none - From Corelib Require Import ssreflect. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -4645,10 +4596,10 @@ Here is an example of a regular, but nontrivial, eliminator. end -> P _x m) -> forall n : nat, P n (plus m n). Admitted. - Section Test. - .. rocqtop:: all + From Corelib Require Import ssreflect. + Fixpoint plus (m n : nat) {struct n} : nat := if n is S p then S (plus m p) else m. @@ -4669,10 +4620,10 @@ Here is an example of a regular, but nontrivial, eliminator. .. rocqtop:: reset none From Corelib Require Import ssreflect. + Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. - Section Test. Fixpoint plus (m n : nat) {struct n} : nat := if n is S p then S (plus m p) else m. @@ -4700,6 +4651,7 @@ Here is an example of a regular, but nontrivial, eliminator. .. rocqtop:: reset none From Corelib Require Import ssreflect. + Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -4735,11 +4687,10 @@ Here is an example of a truncated eliminator: .. rocqtop:: reset none - From Corelib Require Import ssreflect. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. - Section Test. .. rocqdoc:: @@ -4799,7 +4750,7 @@ disjunction. .. rocqtop:: reset none - From Corelib Require Import ssreflect. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -4820,7 +4771,7 @@ disjunction. .. rocqtop:: reset none - From Corelib Require Import ssreflect. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -4855,7 +4806,7 @@ equation-name generation mechanism (see Section :ref:`generation_of_equations_ss .. rocqtop:: reset none - From Corelib Require Import ssreflect. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -4888,7 +4839,7 @@ relevant for the current goal. .. rocqtop:: reset none - From Corelib Require Import ssreflect. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -4932,11 +4883,10 @@ assumption to some given arguments. .. rocqtop:: reset none - From Corelib Require Import ssreflect. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. - Section Test. .. rocqtop:: all @@ -4961,14 +4911,16 @@ bookkeeping steps. .. rocqtop:: reset none - From Corelib Require Import ssreflect ssrbool. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. - Section Test. .. rocqtop:: all + From Corelib Require Import ssrbool. + Section Test. + Variables P Q: bool -> Prop. Hypothesis PQequiv : forall a b, P (a || b) <-> Q a. @@ -5017,7 +4969,7 @@ analysis: .. rocqtop:: reset none - From Corelib Require Import ssreflect. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -5034,14 +4986,15 @@ analysis .. rocqtop:: reset none - From Corelib Require Import ssreflect ssrbool. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. - Section Test. .. rocqtop:: all + From Corelib Require Import ssrbool. + Lemma test b : b || ~~ b = true. by case: b. @@ -5124,7 +5077,7 @@ Let us compare the respective behaviors of ``andE`` and ``andP``. .. rocqtop:: reset none - From Corelib Require Import ssreflect ssrbool. + From Corelib Require Import ssreflect_rw ssrbool. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -5165,14 +5118,15 @@ The view mechanism is compatible with reflect predicates. .. rocqtop:: reset none - From Corelib Require Import ssreflect ssrbool. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. - Section Test. .. rocqtop:: all abort + From Corelib Require Import ssrbool. + Lemma test (a b : bool) (Ha : a) (Hb : b) : a /\ b. apply/andP. @@ -5283,14 +5237,15 @@ but they also allow complex transformation, involving negations. .. rocqtop:: reset none - From Corelib Require Import ssreflect ssrbool. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. - Section Test. .. rocqtop:: all + From Corelib Require Import ssrbool. + Check introN. .. rocqtop:: all @@ -5316,16 +5271,17 @@ actually uses its propositional interpretation. .. rocqtop:: reset none - From Corelib Require Import ssreflect ssrbool. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. - Section Test. .. rocqtop:: all + From Corelib Require Import ssrbool. + Lemma test (a b : bool) (pab : b && a) : b. - have /andP [pa ->] : (a && b) by rewrite andbC. + have /andP [pa ->] : (a && b) by rw andbC. Interpreting goals `````````````````` @@ -5379,14 +5335,15 @@ In this context, the identity view can be used when no view has to be applied: .. rocqtop:: reset none - From Corelib Require Import ssreflect ssrbool. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. - Section Test. .. rocqtop:: all + From Corelib Require Import ssrbool. + Lemma test (b1 b2 b3 : bool) : ~~ (b1 || b2) = b3. apply/idP/idP. @@ -5395,14 +5352,15 @@ In this context, the identity view can be used when no view has to be applied: .. rocqtop:: reset none - From Corelib Require Import ssreflect ssrbool. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. - Section Test. .. rocqtop:: all + From Corelib Require Import ssrbool. + Lemma test (b1 b2 b3 : bool) : ~~ (b1 || b2) = b3. apply/norP/idP. @@ -5471,15 +5429,17 @@ pass a given hypothesis to a lemma. .. rocqtop:: reset none - From Corelib Require Import ssreflect ssrbool. + From Corelib Require Import ssreflect_rw. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. - Section Test. - Variables P Q R : Prop. .. rocqtop:: all + From Corelib Require Import ssrbool. + Section Test. + Variables P Q R : Prop. + Variable P2Q : P -> Q. Variable Q2R : Q -> R. @@ -5504,8 +5464,8 @@ The following intro pattern ltac views are provided: One can call rewrite from an intro pattern, use with parsimony: -+ ``/[1! rules]`` shortcut for ``rewrite rules`` -+ ``/[! rules]`` shortcut for ``rewrite !rules`` ++ ``/[1! rules]`` shortcut for ``rw rules`` ++ ``/[! rules]`` shortcut for ``rw !rules`` Synopsis and Index @@ -5641,7 +5601,7 @@ respectively. case analysis (see :ref:`the_defective_tactics_ssr`) -.. tacv:: rewrite {+ @r_step } +.. tacv:: rw {+ @r_step } rewrite (see :ref:`rewriting_ssr`) @@ -5774,3 +5734,54 @@ Commands Proof`` command of Rocq proof mode. .. [#10] A simple proof context entry is a naked identifier (i.e., not between parentheses) designating a context entry that is not a section variable. + +.. _compatibility_issues_ssr: + + +Compatibility issues +~~~~~~~~~~~~~~~~~~~~ + +Requiring the module `ssreflect_rw` from `Corelib` +creates an environment that is mostly +compatible with the rest of Rocq, up to a few discrepancies. + ++ New tactic(al)s names (:tacn:`last`, :tacn:`done`, :tacn:`have`, :tacn:`suffices`, + :tacn:`suff`, :tacn:`without loss`, :tacn:`wlog`, :tacn:`congr`, :tacn:`unlock`) + might clash with user tactic names. ++ New symbols (``//``, ``/=``, ``//=``) might clash with adjacent + existing symbols. + This can be avoided by inserting white spaces. ++ Some user notations (in particular, defining an infix ``;``) might + interfere with the "open term", parenthesis-free syntax of tactics + such as :tacn:`have`, :tacn:`set (ssreflect)` and :tacn:`pose (ssreflect)`. + +In addition, requiring the backward compatibility module `ssreflect` from `Corelib` +creates an environment that is mostly +compatible with the rest of Rocq, up to a few discrepancies. + ++ New keywords (``is``) might clash with variable, constant, tactic or + tactical names, or with quasi-keywords in tactic or + notation commands. ++ The extensions to the :tacn:`rewrite` tactic are partly incompatible with those + available in current versions of Rocq; in particular, ``rewrite .. in + (type of k)`` or ``rewrite .. in *`` or any other variant of :tacn:`rewrite` + will not work, and the |SSR| syntax and semantics for occurrence selection + and rule chaining are different. Use an explicit rewrite direction + (``rewrite <- …`` or ``rewrite -> …``) to access the Rocq rewrite tactic. ++ The generalization of ``if`` statements to non-Boolean conditions is turned off + by |SSR|, because it is mostly subsumed by Coercion to ``bool`` of the + ``sumXXX`` types (declared in ``ssrfun.v``) and the + :n:`if @term is @pattern then @term else @term` construct + (see :ref:`pattern_conditional_ssr`). To use the + generalized form, turn off the |SSR| Boolean ``if`` notation using the command: + ``Close Scope boolean_if_scope``. ++ The following flag can be unset to make |SSR| more compatible with + parts of Rocq. + +.. flag:: SsrRewrite + + Controls whether the incompatible rewrite syntax is enabled (the default). + Disabling the :term:`flag` makes the syntax compatible with other parts of Rocq. + Note that this ``rewrite`` syntax, now superseded by ``rw``, is + only activated when explicitly requiring the backward compatibility + module ``From Corelib Require Import ssreflect.``. From 72cca582742d19a10856d94ce091c5ce28271b35 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 20 Mar 2026 07:56:02 +0100 Subject: [PATCH 11/11] Add changelog --- .../07-ssreflect/21478-ssreflect-rw-Changed.rst | 12 ++++++++++++ 1 file changed, 12 insertions(+) create mode 100644 doc/changelog/07-ssreflect/21478-ssreflect-rw-Changed.rst diff --git a/doc/changelog/07-ssreflect/21478-ssreflect-rw-Changed.rst b/doc/changelog/07-ssreflect/21478-ssreflect-rw-Changed.rst new file mode 100644 index 000000000000..82bf5fe59af0 --- /dev/null +++ b/doc/changelog/07-ssreflect/21478-ssreflect-rw-Changed.rst @@ -0,0 +1,12 @@ +- **Changed:** + ``rewrite`` tactic for ``rw``. Since this was the major cause of + conflict with legacy tactics, ssreflect can now be loaded with less + conflicts through ``From Corelib Require Import ssreflect_rw.``. + For backward compatibility + ``From Corelib Require Import ssreflect.`` + still loads a ``rewrite`` wrapper to ``rw`` as well as the + ``if is then else `` + and ``if isn't then else `` + syntactic sugars for match + (`#21478 `_, + by Pierre Roux).