From fd8ebe626f092fcd607dc1f8eb51fde9c74df483 Mon Sep 17 00:00:00 2001 From: Jim Fehrle Date: Sat, 7 Nov 2020 17:40:45 -0800 Subject: [PATCH 1/2] Add COPYALL and APPENDALL edit ops, drop unneeded code (cherry picked from commit 250ffd2ac4458f347cc34a9b99298f26f57910a2) --- doc/tools/docgram/README.md | 10 +- doc/tools/docgram/doc_grammar.ml | 210 ++----------------------------- 2 files changed, 14 insertions(+), 206 deletions(-) diff --git a/doc/tools/docgram/README.md b/doc/tools/docgram/README.md index 6c507e1d5754..ba5876ff76a0 100644 --- a/doc/tools/docgram/README.md +++ b/doc/tools/docgram/README.md @@ -181,9 +181,6 @@ as a separate production. (Doesn't work recursively; splicing for both `OPTINREF` - applies the local `OPTINREF` edit to every nonterminal -`EXPAND` - expands LIST0, LIST1, LIST* ... SEP and OPT constructs into -new non-terminals - ### Local edits `DELETE ` - removes the specified production from the grammar @@ -201,6 +198,9 @@ that appear in the specified production: The current version handles a single USE_NT or ADD_OPT per EDIT. These symbols may appear in the middle of the production given in the EDIT. +`APPENDALL ` - inserts at the end of every production in +. + `INSERTALL ` - inserts at the beginning of every production in . @@ -212,10 +212,12 @@ that appear in the specified production: | WITH ``` +`COPYALL ` - creates a new nonterminal `` and copies +all the productions in the nonterminal to ``. + `MOVETO ` - moves the production to `` and, if needed, creates a new production -> \. - `MOVEALLBUT ` - moves all the productions in the nonterminal to `` *except* for the productions following the `MOVEALLBUT` production in the edit script (terminated only by the closing `]`). diff --git a/doc/tools/docgram/doc_grammar.ml b/doc/tools/docgram/doc_grammar.ml index 92a745c86363..ae66520d89f1 100644 --- a/doc/tools/docgram/doc_grammar.ml +++ b/doc/tools/docgram/doc_grammar.ml @@ -1020,7 +1020,7 @@ let rec gen_nt_name sym = good_name name (* create a new nt for LIST* or OPT with the specified name *) -let rec maybe_add_nt g insert_after name sym queue = +let maybe_add_nt g insert_after name sym queue = let empty = [Snterm "empty"] in let maybe_unwrap ?(multi=false) sym = match sym with @@ -1094,65 +1094,6 @@ let rec maybe_add_nt g insert_after name sym queue = end; new_nt -(* expand LIST*, OPT and add "empty" *) -(* todo: doesn't handle recursive expansions well, such as syntax_modifier_opt *) -and expand_rule g edited_nt queue = - let rule = NTMap.find edited_nt !g.map in - let insert_after = ref edited_nt in - let rec expand rule = - let rec aux syms res = - match syms with - | [] -> res - | sym0 :: tl -> - let new_sym = match sym0 with - | Sterm _ - | Snterm _ -> - sym0 - | Slist1 sym - | Slist1sep (sym, _) - | Slist0 sym - | Slist0sep (sym, _) - | Sopt sym -> - let name = gen_nt_name sym in - if name <> "" then begin - let new_nt = maybe_add_nt g insert_after name sym0 queue in - Snterm new_nt - end else sym0 - | Sparen slist -> Sparen (expand slist) - | Sprod slistlist -> - let has_empty = List.length (List.hd (List.rev slistlist)) = 0 in - let name = gen_nt_name sym0 in - if name <> "" then begin - let new_nt = maybe_add_nt g insert_after name - (if has_empty then (Sopt (Sprod (List.rev (List.tl (List.rev slistlist))) )) - else sym0) queue - in - Snterm new_nt - end else - Sprod (List.map expand slistlist) - | Sedit _ - | Sedit2 _ -> - sym0 (* these constructors not used here *) - in - aux tl (new_sym :: res) - in - List.rev (aux rule (if edited_nt <> "empty" && ematch rule [] then [Snterm "empty"] else [])) - in - let rule' = List.map expand rule in - g_update_prods g edited_nt rule' - -let expand_lists g = - (* todo: use Queue.of_seq w OCaml 4.07+ *) - let queue = Queue.create () in - List.iter (fun nt -> Queue.add nt queue) !g.order; - try - while true do - let nt = Queue.pop queue in - expand_rule g nt queue - done - with - | Queue.Empty -> () - let apply_merge g edit_map = List.iter (fun b -> let (from_nt, to_nt) = b in @@ -1213,10 +1154,6 @@ let edit_all_prods g op eprods = global_repl g [(Snterm nt)] [(Sopt (Snterm nt))] end) !g.order; true - | "EXPAND" -> - if List.length eprods > 1 || List.length (List.hd eprods) <> 0 then - error "'EXPAND:' expects a single empty production\n"; - expand_lists g; true | _ -> false let edit_single_prod g edit0 prods nt = @@ -1281,6 +1218,11 @@ let apply_edit_file g edits = with Not_found -> prods in let prods' = moveto nt dest_nt oprod prods in aux tl prods' add_nt + | [Snterm "COPYALL"; Snterm dest_nt] :: tl -> + if NTMap.mem dest_nt !g.map then + error "COPYALL target nonterminal `%s` already exists\n" dest_nt; + g_maybe_add g dest_nt prods; + aux tl prods add_nt | [Snterm "MOVEALLBUT"; Snterm dest_nt] :: tl -> List.iter (fun tlprod -> if not (List.mem tlprod prods) then @@ -1300,6 +1242,8 @@ let apply_edit_file g edits = aux tl (remove_prod [] prods nt) add_nt | (Snterm "INSERTALL" :: syms) :: tl -> aux tl (List.map (fun p -> syms @ p) prods) add_nt + | (Snterm "APPENDALL" :: syms) :: tl -> + aux tl (List.map (fun p -> p @ syms) prods) add_nt | (Snterm "PRINT" :: _) :: tl -> pr_prods nt prods; aux tl prods add_nt @@ -1395,56 +1339,6 @@ let nt_subset_in_orig_order g nts = let subset = StringSet.of_list nts in List.filter (fun nt -> StringSet.mem nt subset) !g.order -let print_chunk out g seen fmt title starts ends = - fprintf out "\n\n%s:\n%s\n" title header; - List.iter (fun start -> - let nts = (nt_closure g start ends) in - print_in_order out g fmt (nt_subset_in_orig_order g nts) !seen; - seen := StringSet.union !seen (StringSet.of_list nts)) - starts - -let print_chunks g out fmt () = - let seen = ref StringSet.empty in - print_chunk out g seen fmt "lconstr" ["lconstr"] ["binder_constr"; "tactic_expr5"]; - print_chunk out g seen fmt "Gallina syntax of terms" ["binder_constr"] ["tactic_expr5"]; - print_chunk out g seen fmt "Gallina The Vernacular" ["gallina"] ["tactic_expr5"]; - print_chunk out g seen fmt "intropattern_list_opt" ["intropattern_list"; "or_and_intropattern_loc"] ["operconstr"; "tactic_expr5"]; - print_chunk out g seen fmt "simple_tactic" ["simple_tactic"] - ["tactic_expr5"; "tactic_expr3"; "tactic_expr2"; "tactic_expr1"; "tactic_expr0"]; - - (*print_chunk out g seen fmt "Ltac" ["tactic_expr5"] [];*) - print_chunk out g seen fmt "Ltac" ["tactic_expr5"] ["tactic_expr4"]; - print_chunk out g seen fmt "Ltac 4" ["tactic_expr4"] ["tactic_expr3"; "tactic_expr2"]; - print_chunk out g seen fmt "Ltac 3" ["tactic_expr3"] ["tactic_expr2"]; - print_chunk out g seen fmt "Ltac 2" ["tactic_expr2"] ["tactic_expr1"]; - print_chunk out g seen fmt "Ltac 1" ["tactic_expr1"] ["tactic_expr0"]; - print_chunk out g seen fmt "Ltac 0" ["tactic_expr0"] []; - - - print_chunk out g seen fmt "command" ["command"] []; - print_chunk out g seen fmt "vernac_toplevel" ["vernac_toplevel"] []; - print_chunk out g seen fmt "vernac_control" ["vernac_control"] [] - - (* - let ssr_tops = ["ssr_dthen"; "ssr_else"; "ssr_mpat"; "ssr_rtype"] in - seen := StringSet.union !seen (StringSet.of_list ssr_tops); - - print_chunk out g seen fmt "ssrindex" ["ssrindex"] []; - print_chunk out g seen fmt "command" ["command"] []; - print_chunk out g seen fmt "binder_constr" ["binder_constr"] []; - (*print_chunk out g seen fmt "closed_binder" ["closed_binder"] [];*) - print_chunk out g seen fmt "gallina_ext" ["gallina_ext"] []; - (*print_chunk out g seen fmt "hloc" ["hloc"] [];*) - (*print_chunk out g seen fmt "hypident" ["hypident"] [];*) - print_chunk out g seen fmt "simple_tactic" ["simple_tactic"] []; - print_chunk out g seen fmt "tactic_expr" ["tactic_expr4"; "tactic_expr1"; "tactic_expr0"] []; - fprintf out "\n\nRemainder:\n"; - print_in_order g (List.filter (fun x -> not (StringSet.mem x !seen)) !g.order) StringSet.empty; - *) - - - (*seen := StringSet.diff !seen (StringSet.of_list ssr_tops);*) - (*print_chunk out g seen fmt "vernac_toplevel" ["vernac_toplevel"] [];*) let index_of str list = let rec index_of_r str list index = match list with @@ -1478,89 +1372,6 @@ let get_range g start end_ = let get_rangeset g start end_ = StringSet.of_list (get_range g start end_) -let print_dominated g = - let info nt rangeset exclude = - let reachable = StringSet.of_list (nt_closure g nt exclude) in - let unreachable = StringSet.of_list (nt_closure g (List.hd start_symbols) (nt::exclude)) in - let dominated = StringSet.diff reachable unreachable in - Printf.printf "For %s, 'attribute' is: reachable = %b, unreachable = %b, dominated = %b\n" nt - (StringSet.mem "attribute" reachable) - (StringSet.mem "attribute" unreachable) - (StringSet.mem "attribute" dominated); - Printf.printf " rangeset = %b excluded = %b\n" - (StringSet.mem "attribute" rangeset) - (List.mem "attribute" exclude); - reachable, dominated - in - let pr3 nt rangeset reachable dominated = - let missing = StringSet.diff dominated rangeset in - if not (StringSet.is_empty missing) then begin - Printf.printf "\nMissing in range for '%s':\n" nt; - StringSet.iter (fun nt -> Printf.printf " %s\n" nt) missing - end; - - let unneeded = StringSet.diff rangeset reachable in - if not (StringSet.is_empty unneeded) then begin - Printf.printf "\nUnneeded in range for '%s':\n" nt; - StringSet.iter (fun nt -> Printf.printf " %s\n" nt) unneeded - end; - in - let pr2 nt rangeset exclude = - let reachable, dominated = info nt rangeset exclude in - pr3 nt rangeset reachable dominated - in - let pr nt end_ = pr2 nt (get_rangeset g nt end_) [] in - - let ssr_ltac = ["ssr_first_else"; "ssrmmod"; "ssrdotac"; "ssrortacarg"; - "ssrparentacarg"] in - let ssr_tac = ["ssrintrosarg"; "ssrhintarg"; "ssrtclarg"; "ssrseqarg"; "ssrmovearg"; - "ssrrpat"; "ssrclauses"; "ssrcasearg"; "ssrarg"; "ssrapplyarg"; "ssrexactarg"; - "ssrcongrarg"; "ssrterm"; "ssrrwargs"; "ssrunlockargs"; "ssrfixfwd"; "ssrcofixfwd"; - "ssrfwdid"; "ssrposefwd"; "ssrsetfwd"; "ssrdgens"; "ssrhavefwdwbinders"; "ssrhpats_nobs"; - "ssrhavefwd"; "ssrsufffwd"; "ssrwlogfwd"; "ssrhint"; "ssrclear"; "ssr_idcomma"; - "ssrrwarg"; "ssrintros_ne"; "ssrhint3arg" ] @ ssr_ltac in - let ssr_cmd = ["ssr_modlocs"; "ssr_search_arg"; "ssrhintref"; "ssrhintref_list"; - "ssrviewpos"; "ssrviewposspc"] in - let ltac = ["ltac_expr"; "ltac_expr0"; "ltac_expr1"; "ltac_expr2"; "ltac_expr3"] in - let term = ["term"; "term0"; "term1"; "term10"; "term100"; "term9"; - "pattern"; "pattern0"; "pattern1"; "pattern10"] in - - pr "term" "constr"; - - let ltac_rangeset = List.fold_left StringSet.union StringSet.empty - [(get_rangeset g "ltac_expr" "tactic_atom"); - (get_rangeset g "toplevel_selector" "range_selector"); - (get_rangeset g "ltac_match_term" "match_pattern"); - (get_rangeset g "ltac_match_goal" "match_pattern_opt")] in - pr2 "ltac_expr" ltac_rangeset ("simple_tactic" :: ssr_tac); - - let dec_vern_rangeset = get_rangeset g "decorated_vernac" "opt_coercion" in - let dev_vern_excl = - ["gallina_ext"; "command"; "tactic_mode"; "syntax"; "command_entry"] @ term @ ltac @ ssr_tac in - pr2 "decorated_vernac" dec_vern_rangeset dev_vern_excl; - - let simp_tac_range = get_rangeset g "simple_tactic" "hypident_occ_list_comma" in - let simp_tac_excl = ltac @ ssr_tac in - pr2 "simple_tactic" simp_tac_range simp_tac_excl; - - let cmd_range = get_rangeset g "command" "int_or_id_list_opt" in - let cmd_excl = ssr_tac @ ssr_cmd in - pr2 "command" cmd_range cmd_excl; - - let syn_range = get_rangeset g "syntax" "constr_as_binder_kind" in - let syn_excl = ssr_tac @ ssr_cmd in - pr2 "syntax" syn_range syn_excl; - - let gext_range = get_rangeset g "gallina_ext" "Structure_opt" in - let gext_excl = ssr_tac @ ssr_cmd in - pr2 "gallina_ext" gext_range gext_excl; - - let qry_range = get_rangeset g "query_command" "searchabout_query_list" in - let qry_excl = ssr_tac @ ssr_cmd in - pr2 "query_command" qry_range qry_excl - - (* todo: tactic_mode *) - let check_range_consistency g start end_ = let defined_list = get_range g start end_ in let defined = StringSet.of_list defined_list in @@ -1913,10 +1724,6 @@ let process_rst g file args seen tac_prods cmd_prods = end in -(* let skip_files = ["doc/sphinx/proof-engine/ltac.rst"; "doc/sphinx/proof-engine/ltac2.rst";*) -(* "doc/sphinx/proof-engine/ssreflect-proof-language.rst"]*) -(* in*) - let cmd_exclude_files = [ "doc/sphinx/proof-engine/ssreflect-proof-language.rst"; "doc/sphinx/proofs/automatic-tactics/auto.rst"; @@ -2101,7 +1908,6 @@ let process_grammar args = close_out out; finish_with_file (dir "orderedGrammar") args; (* check_singletons g*) -(* print_dominated g*) let seen = ref { nts=NTMap.empty; tacs=NTMap.empty; tacvs=NTMap.empty; cmds=NTMap.empty; cmdvs=NTMap.empty } in let args = { args with no_update = false } in (* always update rsts in place for now *) From ed7ecf1fbdc15300f6e9ad5e4d74da41823da6b4 Mon Sep 17 00:00:00 2001 From: Jim Fehrle Date: Sat, 12 Sep 2020 20:54:22 -0700 Subject: [PATCH 2/2] Convert auto chapter to prodn (cherry picked from commit b1846e859091e24db1210be53f9193aa3aedb4d9) --- doc/changelog/04-tactics/13381-bfs_eauto.rst | 6 +- doc/sphinx/addendum/generalized-rewriting.rst | 14 +- doc/sphinx/addendum/type-classes.rst | 10 +- doc/sphinx/addendum/universe-polymorphism.rst | 2 +- doc/sphinx/changes.rst | 12 +- doc/sphinx/conf.py | 4 +- doc/sphinx/language/core/inductive.rst | 5 +- doc/sphinx/language/core/modules.rst | 3 +- doc/sphinx/language/core/sections.rst | 3 +- doc/sphinx/proof-engine/ltac.rst | 5 +- doc/sphinx/proof-engine/ltac2.rst | 2 +- doc/sphinx/proof-engine/tactics.rst | 122 ++-- .../proof-engine/vernacular-commands.rst | 2 +- doc/sphinx/proofs/automatic-tactics/auto.rst | 671 ++++++++---------- .../proofs/writing-proofs/rewriting.rst | 35 +- doc/tools/docgram/common.edit_mlg | 120 +++- doc/tools/docgram/doc_grammar.ml | 25 +- doc/tools/docgram/fullGrammar | 43 +- doc/tools/docgram/orderedGrammar | 235 +++--- theories/Classes/CRelationClasses.v | 2 - theories/Classes/RelationClasses.v | 2 - 21 files changed, 704 insertions(+), 619 deletions(-) diff --git a/doc/changelog/04-tactics/13381-bfs_eauto.rst b/doc/changelog/04-tactics/13381-bfs_eauto.rst index f37fbfe52b1b..e63241e46c09 100644 --- a/doc/changelog/04-tactics/13381-bfs_eauto.rst +++ b/doc/changelog/04-tactics/13381-bfs_eauto.rst @@ -1,6 +1,6 @@ - **Deprecated:** - Undocumented :n:`eauto @int_or_var @int_or_var` syntax in favor of new ``bfs eauto``. - Also deprecated 2-integer syntax for ``debug eauto`` and ``info_eauto``. - (Use ``bfs eauto`` with the :flag:`Info Eauto` or :flag:`Debug Eauto` flags instead.) + Undocumented :n:`eauto @nat_or_var @nat_or_var` syntax in favor of new :tacn:`bfs eauto`. + Also deprecated 2-integer syntax for :tacn:`debug eauto` and :tacn:`info_eauto`. + (Use :tacn:`bfs eauto` with the :flag:`Info Eauto` or :flag:`Debug Eauto` flags instead.) (`#13381 `_, by Jim Fehrle). diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index 27ae7cea3a53..039a23e8c2f8 100644 --- a/doc/sphinx/addendum/generalized-rewriting.rst +++ b/doc/sphinx/addendum/generalized-rewriting.rst @@ -535,11 +535,19 @@ pass additional arguments such as ``using relation``. .. tacn:: setoid_reflexivity setoid_symmetry {? in @ident } setoid_transitivity @one_term - setoid_rewrite {? {| -> | <- } } @one_term {? with @bindings } {? at @occurrences } {? in @ident } - setoid_rewrite {? {| -> | <- } } @one_term {? with @bindings } in @ident at @occurrences + setoid_rewrite {? {| -> | <- } } @one_term {? with @bindings } {? at @rewrite_occs } {? in @ident } + setoid_rewrite {? {| -> | <- } } @one_term {? with @bindings } in @ident at @rewrite_occs setoid_replace @one_term with @one_term {? using relation @one_term } {? in @ident } {? at {+ @int_or_var } } {? by @ltac_expr3 } :name: setoid_reflexivity; setoid_symmetry; setoid_transitivity; setoid_rewrite; _; setoid_replace + .. todo: move rewrite_occs to rewrite chapter when that chapter is revised + + .. insertprodn rewrite_occs rewrite_occs + + .. prodn:: + rewrite_occs ::= {+ @integer } + | @ident + The ``using relation`` arguments cannot be passed to the unprefixed form. The latter argument tells the tactic what parametric relation should be used to replace the first tactic argument with the second one. If @@ -714,6 +722,8 @@ instances are tried at each node of the search tree). To speed it up, declare your constant as rigid for proof search using the command :cmd:`Typeclasses Opaque`. +.. _strategies4rewriting: + Strategies for rewriting ------------------------ diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index 98445fca1a4d..4143d836c471 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -335,12 +335,6 @@ Summary of the commands .. cmd:: Instance {? @ident_decl {* @binder } } : @type {? @hint_info } {? {| := %{ {* @field_def } %} | := @term } } - .. insertprodn hint_info one_pattern - - .. prodn:: - hint_info ::= %| {? @natural } {? @one_pattern } - one_pattern ::= @one_term - Declares a typeclass instance named :token:`ident_decl` of the class :n:`@type` with the specified parameters and with fields defined by :token:`field_def`, where each field must be a declared field of @@ -503,7 +497,7 @@ Typeclasses Transparent, Typeclasses Opaque It is useful when some constants prevent some unifications and make resolution fail. It is also useful to declare constants which - should never be unfolded during proof-search, like fixpoints or + should never be unfolded during proof search, like fixpoints or anything which does not look like an abbreviation. This can additionally speed up proof search as the typeclass map can be indexed by such rigid constants (see @@ -555,7 +549,7 @@ Settings This can be expensive as it requires rebuilding hint clauses dynamically, and does not benefit from the invertibility status of the product introduction rule, resulting in potentially more - expensive proof-search (i.e. more useless backtracking). + expensive proof search (i.e. more useless backtracking). .. flag:: Typeclass Resolution For Conversion diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index 4615a8dfca23..bb78b142caba 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -412,7 +412,7 @@ Explicit Universes | _ | @qualid univ_decl ::= @%{ {* @ident } {? + } {? %| {*, @univ_constraint } {? + } } %} - cumul_univ_decl ::= @%{ {* {? {| = | + | * } } @ident } {? + } {? %| {*, @univ_constraint } {? + } } %} + cumul_univ_decl ::= @%{ {* {? {| + | = | * } } @ident } {? + } {? %| {*, @univ_constraint } {? + } } %} univ_constraint ::= @universe_name {| < | = | <= } @universe_name The syntax has been extended to allow users to explicitly bind names diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 24fa71059c55..249c7794bea5 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -551,7 +551,7 @@ Flags, options and attributes ``Private`` (`#11665 `_, by Théo Zimmermann). - **Added:** - The :cmd:`Hint` commands now accept the :attr:`export` locality as + The :ref:`Hint ` commands now accept the :attr:`export` locality as an attribute, allowing to make import-scoped hints (`#11812 `_, by Pierre-Marie Pédrot). @@ -3170,7 +3170,7 @@ Vernacular Commands `Inductive list (A : Type) := nil : list | cons : A -> list -> list.` - New `Set Hint Variables/Constants Opaque/Transparent` commands for setting globally the opacity flag of variables and constants in hint databases, - overwriting the opacity set of the hint database. + overriding the opacity setting of the hint database. - Added generic syntax for "attributes", as in: `#[local] Lemma foo : bar.` - Added the `Numeral Notation` command for registering decimal numeral @@ -4045,7 +4045,7 @@ constraints can now be left floating around and be seen by the user thanks to a new option. The Keyed Unification mode has been improved by Matthieu Sozeau. -The typeclass resolution engine and associated proof-search tactic have +The typeclass resolution engine and associated proof search tactic have been reimplemented on top of the proof-engine monad, providing better integration in tactics, and new options have been introduced to control it, by Matthieu Sozeau with help from Théo Zimmermann. @@ -5140,7 +5140,7 @@ Program - Hints costs are now correctly taken into account (potential source of incompatibilities). - Documented the Hint Cut command that allows control of the - proof-search during typeclass resolution (see reference manual). + proof search during typeclass resolution (see reference manual). API @@ -5776,7 +5776,7 @@ Libraries comes first. By default, the power function now takes two BigN. - Creation of Vector, an independent library for lists indexed by their length. - Vectors' names overwrite lists' one so you should not "Import" the library. + Vectors' names override lists' one so you should not "Import" the library. All old names changed: function names follow the ocaml ones and, for example, Vcons becomes Vector.cons. You can get [..;..;..]-style notations by importing Vector.VectorNotations. @@ -6830,7 +6830,7 @@ Tactics - Tactic "remember" now supports an "in" clause to remember only selected occurrences of a term. -- Tactic "pose proof" supports name overwriting in case of specialization of an +- Tactic "pose proof" supports name overriding in case of specialization of an hypothesis. - Semi-decision tactic "jp" for first-order intuitionistic logic moved to user diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index af5d1e3a009f..246568d3c1d0 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -188,10 +188,8 @@ def setup(app): 'conversion', 'where', 'oriented_rewriter', - 'hintbases', 'bindings_with_parameters', - 'destruction_arg', - 'clause_dft_concl' + 'destruction_arg' ]] # -- Options for HTML output ---------------------------------------------- diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst index 251b5e495556..9fda2ab1fa84 100644 --- a/doc/sphinx/language/core/inductive.rst +++ b/doc/sphinx/language/core/inductive.rst @@ -8,14 +8,13 @@ Inductive types .. cmd:: Inductive @inductive_definition {* with @inductive_definition } - .. insertprodn inductive_definition cumul_ident_decl + .. insertprodn inductive_definition constructor .. prodn:: - inductive_definition ::= {? > } @cumul_ident_decl {* @binder } {? %| {* @binder } } {? : @type } {? := {? @constructors_or_record } } {? @decl_notations } + inductive_definition ::= {? > } @ident {? @cumul_univ_decl } {* @binder } {? %| {* @binder } } {? : @type } {? := {? @constructors_or_record } } {? @decl_notations } constructors_or_record ::= {? %| } {+| @constructor } | {? @ident } %{ {*; @record_field } {? ; } %} constructor ::= @ident {* @binder } {? @of_type } - cumul_ident_decl ::= @ident {? @cumul_univ_decl } This command defines one or more inductive types and its constructors. Coq generates destructors diff --git a/doc/sphinx/language/core/modules.rst b/doc/sphinx/language/core/modules.rst index 54252689e13f..6d96e152023a 100644 --- a/doc/sphinx/language/core/modules.rst +++ b/doc/sphinx/language/core/modules.rst @@ -155,7 +155,8 @@ are now available through the dot notation. #. Interactive modules and module types can be nested. #. Interactive modules and module types can't be defined inside of :ref:`sections`. Sections can be defined inside of interactive modules and module types. - #. Hints and notations (:cmd:`Hint` and :cmd:`Notation` commands) can also appear inside interactive + #. Hints and notations (the :ref:`Hint ` and :cmd:`Notation` + commands) can also appear inside interactive modules and module types. Note that with module definitions like: :n:`Module @ident__1 : @module_type := @ident__2.` diff --git a/doc/sphinx/language/core/sections.rst b/doc/sphinx/language/core/sections.rst index df50dbafe3d3..75389bb25972 100644 --- a/doc/sphinx/language/core/sections.rst +++ b/doc/sphinx/language/core/sections.rst @@ -69,7 +69,8 @@ Sections create local contexts which can be shared across multiple definitions. :undocumented: .. note:: - Most commands, like :cmd:`Hint`, :cmd:`Notation`, option management, … which + Most commands, such as the :ref:`Hint ` commands, + :cmd:`Notation` and option management commands that appear inside a section are canceled when the section is closed. .. cmd:: Let @ident_decl @def_body diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 2fc3c9f74808..87a367fc937b 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -1637,9 +1637,10 @@ Testing boolean expressions: guard .. tacn:: guard @int_or_var @comparison @int_or_var :name: guard - .. insertprodn comparison comparison + .. insertprodn int_or_var comparison .. prodn:: + int_or_var ::= {| @integer | @ident } comparison ::= = | < | <= @@ -1761,7 +1762,7 @@ Defining |Ltac| symbols "Ltac intros := idtac" seems like it redefines/hides an existing tactic, but in fact it creates a tactic which can only be called by its qualified name. This is true in - general of tactic notations. The only way to overwrite most + general of tactic notations. The only way to override most primitive tactics, and any user-defined tactic notation, is with another tactic notation. diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index a46f4fb894bb..375129c02de0 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -1475,7 +1475,7 @@ Other nonterminals that have syntactic classes are listed here. * - :n:`clause` - :token:`ltac2_clause` - - :token:`clause_dft_concl` + - :token:`occurrences` * - :n:`occurrences` - :token:`q_occurrences` diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 4f01559cad4f..8f5c04592988 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -466,52 +466,82 @@ Examples: .. _occurrencessets: -Occurrence sets and occurrence clauses -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -An occurrence clause is a modifier to some tactics that obeys the -following syntax: - - .. prodn:: - occurrence_clause ::= in @goal_occurrences - goal_occurrences ::= {*, @ident {? @at_occurrences } } {? |- {? * {? @at_occurrences } } } - | * |- {? * {? @at_occurrences } } - | * - at_occurrences ::= at @occurrences - occurrences ::= {? - } {* @natural } - -The role of an occurrence clause is to select a set of occurrences of a term -in a goal. In the first case, the :n:`@ident {? at {* num}}` parts indicate -that occurrences have to be selected in the hypotheses named :token:`ident`. -If no numbers are given for hypothesis :token:`ident`, then all the -occurrences of :token:`term` in the hypothesis are selected. If numbers are -given, they refer to occurrences of :token:`term` when the term is printed -using the :flag:`Printing All` flag, counting from left to right. In particular, -occurrences of :token:`term` in implicit arguments -(see :ref:`ImplicitArguments`) or coercions (see :ref:`Coercions`) are -counted. - -If a minus sign is given between ``at`` and the list of occurrences, it -negates the condition so that the clause denotes all the occurrences -except the ones explicitly mentioned after the minus sign. - -As an exception to the left-to-right order, the occurrences in -the return subexpression of a match are considered *before* the -occurrences in the matched term. - -In the second case, the ``*`` on the left of ``|-`` means that all occurrences -of term are selected in every hypothesis. - -In the first and second case, if ``*`` is mentioned on the right of ``|-``, the -occurrences of the conclusion of the goal have to be selected. If some numbers -are given, then only the occurrences denoted by these numbers are selected. If -no numbers are given, all occurrences of :token:`term` in the goal are selected. - -Finally, the last notation is an abbreviation for ``* |- *``. Note also -that ``|-`` is optional in the first case when no ``*`` is given. - -Here are some tactics that understand occurrence clauses: :tacn:`set`, -:tacn:`remember`, :tacn:`induction`, :tacn:`destruct`. +Occurrence clauses +~~~~~~~~~~~~~~~~~~ + +An :gdef:`occurrence` is a subterm of a goal or hypothesis that +matches a pattern provided by a tactic. Occurrence clauses +select a subset of the ocurrences in a goal and/or in +one or more of its hypotheses. + + .. insertprodn occurrences concl_occs + + .. prodn:: + occurrences ::= at @occs_nums + | in @goal_occurrences + occs_nums ::= {? - } {+ @nat_or_var } + nat_or_var ::= {| @natural | @ident } + goal_occurrences ::= {+, @hyp_occs } {? %|- {? @concl_occs } } + | * %|- {? @concl_occs } + | %|- {? @concl_occs } + | {? @concl_occs } + hyp_occs ::= @hypident {? at @occs_nums } + hypident ::= @ident + | ( type of @ident ) + | ( value of @ident ) + concl_occs ::= * {? at @occs_nums } + + :n:`@occurrences` + The first form of :token:`occurrences` selects occurrences in + the conclusion of the goal. The second form can select occurrences + in the goal conclusion and in one or more hypotheses. + + :n:`{? - } {+ @nat_or_var }` + Selects the specified occurrences within a single goal or hypothesis. + Occurrences are numbered from left to right starting with 1 when the + goal is printed with the :flag:`Printing All` flag. (In particular, occurrences + in :ref:`implicit arguments ` and + :ref:`coercions ` are counted but not shown by default.) + + Specifying `-` includes all occurrences *except* the ones listed. + + :n:`{*, @hyp_occs } {? %|- {? @concl_occs } }` + Selects occurrences in the specified hypotheses and the + specified occurrences in the conclusion. + + :n:`* %|- {? @concl_occs }` + Selects all occurrences in all hypotheses and the + specified occurrences in the conclusion. + + :n:`%|- {? @concl_occs }` + Selects the specified occurrences in the conclusion. + + :n:`@goal_occurrences ::= {? @concl_occs }` + Selects all occurrences in all hypotheses and in the specified occurrences + in the conclusion. + + :n:`@hypident {? at @occs_nums }` + Omiting :token:`occs_nums` selects all occurrences within the hypothesis. + + :n:`@hypident ::= @ident` + Selects the hypothesis named :token:`ident`. + + :n:`( type of @ident )` + Selects the type part of the named hypothesis (e.g. `: nat`). + + :n:`( value of @ident )` + Selects the value part of the named hypothesis (e.g. `:= 1`). + + :n:`@concl_occs ::= * {? at @occs_nums }` + Selects occurrences in the conclusion. '*' by itself selects all occurrences. + :n:`@occs_nums` selects the specified occurrences. + + Use `in *` to select all occurrences in all hypotheses and the conclusion, + which is equivalent to `in * |- *`. Use `* |-` to select all occurrences + in all hypotheses. + +Tactics that use occurrence clauses include :tacn:`set`, +:tacn:`remember`, :tacn:`induction` and :tacn:`destruct`. .. seealso:: diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 86d1d25745ca..e7db9cfacab7 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -1136,7 +1136,7 @@ Controlling the locality of commands Some commands support an :attr:`export` attribute. The effect of the attribute is to make the effect of the command available when the module containing it is imported. It is supported in - particular by the :cmd:`Hint`, :cmd:`Set` and :cmd:`Unset` + particular by the :ref:`Hint `, :cmd:`Set` and :cmd:`Unset` commands. .. _controlling-typing-flags: diff --git a/doc/sphinx/proofs/automatic-tactics/auto.rst b/doc/sphinx/proofs/automatic-tactics/auto.rst index cc4ab765023d..472df2bd91a6 100644 --- a/doc/sphinx/proofs/automatic-tactics/auto.rst +++ b/doc/sphinx/proofs/automatic-tactics/auto.rst @@ -4,104 +4,87 @@ Programmable proof search ========================= -.. tacn:: auto - :name: auto +.. tacn:: auto {? @nat_or_var } {? @auto_using } {? @hintbases } - This tactic implements a Prolog-like resolution procedure to solve the + .. insertprodn auto_using hintbases + + .. prodn:: + auto_using ::= using {+, @one_term } + hintbases ::= with * + | with {+ @ident } + + Implements a Prolog-like resolution procedure to solve the current goal. It first tries to solve the goal using the :tacn:`assumption` tactic, then it reduces the goal to an atomic one using :tacn:`intros` and introduces the newly generated hypotheses as hints. Then it looks at - the list of tactics associated to the head symbol of the goal and - tries to apply one of them (starting from the tactics with lower - cost). This process is recursively applied to the generated subgoals. + the list of tactics associated with the head symbol of the goal and + tries to apply one of them. Lower cost tactics are tried before higher-cost + tactics. This process is recursively applied to the generated subgoals. - By default, :tacn:`auto` only uses the hypotheses of the current goal and - the hints of the database named ``core``. + :n:`@nat_or_var` + Specifies the maximum search depth. The default is 5. - .. warning:: + :n:`using {+, @one_term }` - :tacn:`auto` uses a weaker version of :tacn:`apply` that is closer to - :tacn:`simple apply` so it is expected that sometimes :tacn:`auto` will - fail even if applying manually one of the hints would succeed. + Uses lemmas :n:`{+, @one_term }` in addition to hints. If :n:`@one_term` is an + inductive type, the collection of its constructors are added as hints. - .. tacv:: auto @natural + Note that hints passed through the `using` clause are used in the same + way as if they were passed through a hint database. Consequently, + they use a weaker version of :tacn:`apply` and :n:`auto using @one_term` + may fail where :n:`apply @one_term` succeeds. - Forces the search depth to be :token:`natural`. The maximal search depth - is 5 by default. + .. todo + Given that this can be seen as counter-intuitive, it could be useful + to have an option to use full-blown :tacn:`apply` for lemmas passed + through the `using` clause. Contributions welcome! - .. tacv:: auto with {+ @ident} + :n:`with *` + Use all existing hint databases. Using this variant is highly discouraged + in finished scripts since it is both slower and less robust than explicitly + selecting the required databases. - Uses the hint databases :n:`{+ @ident}` in addition to the database ``core``. + :n:`with {+ @ident }` + Use the hint databases :n:`{+ @ident}` in addition to the database ``core``. + Use the fake database `nocore` to omit `core`. - .. note:: + If no `with` clause is given, :tacn:`auto` only uses the hypotheses of the + current goal and the hints of the database named ``core``. - Use the fake database `nocore` if you want to *not* use the `core` - database. + :tacn:`auto` generally either completely solves the goal or + leaves it unchanged. Use :tacn:`solve` `[ auto ]` if you want a failure + when they don't solve the goal. :tacn:`auto` will fail if :tacn:`fail` + or :tacn:`gfail` are invoked directly or indirectly, in which case setting + the :flag:`Ltac Debug` may help you debug the failure. - .. tacv:: auto with * + .. warning:: - Uses all existing hint databases. Using this variant is highly discouraged - in finished scripts since it is both slower and less robust than the variant - where the required databases are explicitly listed. + :tacn:`auto` uses a weaker version of :tacn:`apply` that is closer to + :tacn:`simple apply` so it is expected that sometimes :tacn:`auto` will + fail even if applying manually one of the hints would succeed. .. seealso:: - :ref:`The Hints Databases for auto and eauto ` for the list of + :ref:`thehintsdatabasesforautoandeauto` for the list of pre-defined databases and the way to create or extend a database. - .. tacv:: auto using {+ @qualid__i} {? with {+ @ident } } - - Uses lemmas :n:`@qualid__i` in addition to hints. If :n:`@qualid` is an - inductive type, it is the collection of its constructors which are added - as hints. - - .. note:: - - The hints passed through the `using` clause are used in the same - way as if they were passed through a hint database. Consequently, - they use a weaker version of :tacn:`apply` and :n:`auto using @qualid` - may fail where :n:`apply @qualid` succeeds. - - Given that this can be seen as counter-intuitive, it could be useful - to have an option to use full-blown :tacn:`apply` for lemmas passed - through the `using` clause. Contributions welcome! - - .. tacv:: info_auto + .. tacn:: info_auto {? @nat_or_var } {? @auto_using } {? @hintbases } Behaves like :tacn:`auto` but shows the tactics it uses to solve the goal. This variant is very useful for getting a better understanding of automation, or to know what lemmas/assumptions were used. - .. tacv:: debug auto - :name: debug auto + .. tacn:: debug auto {? @nat_or_var } {? @auto_using } {? @hintbases } Behaves like :tacn:`auto` but shows the tactics it tries to solve the goal, including failing paths. - .. tacv:: {? info_}auto {? @natural} {? using {+ @qualid}} {? with {+ @ident}} - - This is the most general form, combining the various options. - -.. tacv:: trivial - :name: trivial - - This tactic is a restriction of :tacn:`auto` that is not recursive - and tries only hints that cost `0`. Typically it solves trivial - equalities like :g:`X=X`. - - .. tacv:: trivial with {+ @ident} - trivial with * - trivial using {+ @qualid} - debug trivial - info_trivial - {? info_}trivial {? using {+ @qualid}} {? with {+ @ident}} - :name: _; _; _; debug trivial; info_trivial; _ - :undocumented: +.. tacn:: trivial {? @auto_using } {? @hintbases } + debug trivial {? @auto_using } {? @hintbases } + info_trivial {? @auto_using } {? @hintbases } -.. note:: - :tacn:`auto` and :tacn:`trivial` either solve completely the goal or - else succeed without changing the goal. Use :g:`solve [ auto ]` and - :g:`solve [ trivial ]` if you would prefer these tactics to fail when - they do not manage to solve the goal. + Like :tacn:`auto`, but is not recursive + and only tries hints with zero cost. Typically used to solve goals + for which a lemma is already available in the specified :n:`hintbases`. .. flag:: Info Auto Debug Auto @@ -111,10 +94,9 @@ Programmable proof search These flags enable printing of informative or debug information for the :tacn:`auto` and :tacn:`trivial` tactics. -.. tacn:: eauto - :name: eauto +.. tacn:: eauto {? @nat_or_var } {? @auto_using } {? @hintbases } - This tactic generalizes :tacn:`auto`. While :tacn:`auto` does not try + Generalizes :tacn:`auto`. While :tacn:`auto` does not try resolution hints which would leave existential variables in the goal, :tacn:`eauto` does try them (informally speaking, it internally uses a tactic close to :tacn:`simple eapply` instead of a tactic close to :tacn:`simple apply` @@ -133,12 +115,13 @@ Programmable proof search Goal forall P:nat -> Prop, P 0 -> exists n, P n. eauto. - Note that ``ex_intro`` should be declared as a hint. + `ex_intro` is declared as a hint so the proof succeeds. + .. seealso:: :ref:`thehintsdatabasesforautoandeauto` - .. tacv:: {? info_}eauto {? @natural} {? using {+ @qualid}} {? with {+ @ident}} + .. tacn:: info_eauto {? @nat_or_var } {? @auto_using } {? @hintbases } - The various options for :tacn:`eauto` are the same as for :tacn:`auto`. + The various options for :tacn:`info_eauto` are the same as for :tacn:`info_auto`. :tacn:`eauto` also obeys the following flags: @@ -146,34 +129,55 @@ Programmable proof search Debug Eauto :undocumented: - .. seealso:: :ref:`The Hints Databases for auto and eauto ` + .. tacn:: debug eauto {? @nat_or_var } {? @auto_using } {? @hintbases } + Behaves like :tacn:`eauto` but shows the tactics it tries to solve the goal, + including failing paths. + + .. tacn:: bfs eauto {? @nat_or_var } {? @auto_using } {? @hintbases } + + Like :tacn:`eauto`, but uses a + `breadth-first search `_. -.. tacn:: autounfold with {+ @ident} - :name: autounfold +.. tacn:: autounfold {? @hintbases } {? @occurrences } - This tactic unfolds constants that were declared through a :cmd:`Hint Unfold` + Unfolds constants that were declared through a :cmd:`Hint Unfold` in the given databases. -.. tacv:: autounfold with {+ @ident} in @goal_occurrences + :n:`@occurrences` + Performs the unfolding in the specified occurrences. The :n:`at @occs_nums` + clause of :n:`@occurrences` is not supported. + +.. tacn:: autorewrite {? * } with {+ @ident } {? @occurrences } {? using @ltac_expr } + + `*` + If present, rewrite all occurrences whose side conditions are solved. - Performs the unfolding in the given clause (:token:`goal_occurrences`). + .. todo: This may not always work as described, see #4976 #7672 and + https://github.com/coq/coq/issues/1933#issuecomment-337497938 as + mentioned here: https://github.com/coq/coq/pull/13343#discussion_r527801604 -.. tacv:: autounfold with * + :n:`with {+ @ident }` + Specifies the rewriting rule bases to use. - Uses the unfold hints declared in all the hint databases. + :n:`@occurrences` + Performs rewriting in the specified occurrences. Note: the `at` clause + is currently not supported. -.. tacn:: autorewrite with {+ @ident} - :name: autorewrite + .. exn:: The "at" syntax isn't available yet for the autorewrite tactic. - This tactic carries out rewritings according to the rewriting rule - bases :n:`{+ @ident}`. + Appears when there is an `at` clause on the conclusion. - Each rewriting rule from the base :n:`@ident` is applied to the main subgoal until + :n:`using @ltac_expr` + :token:`ltac_expr` is applied to the main subgoal after each rewriting step. + + Applies rewritings according to the rewriting rule bases :n:`{+ @ident }`. + + For each rule base, applies each rewriting to the main subgoal until it fails. Once all the rules have been processed, if the main subgoal has - progressed (e.g., if it is distinct from the initial main goal) then the rules - of this base are processed again. If the main subgoal has not progressed then - the next base is processed. For the bases, the behavior is exactly similar to + changed then the rules + of this base are processed again. If the main subgoal has not changed then + the next base is processed. For the bases, the behavior is very similar to the processing of the rewriting rules. The rewriting rule bases are built with the :cmd:`Hint Rewrite` @@ -183,31 +187,13 @@ Programmable proof search This tactic may loop if you build non terminating rewriting systems. -.. tacv:: autorewrite with {+ @ident} using @tactic - - Performs, in the same way, all the rewritings of the bases :n:`{+ @ident}` - applying tactic to the main subgoal after each rewriting step. - -.. tacv:: autorewrite with {+ @ident} in @qualid - - Performs all the rewritings in hypothesis :n:`@qualid`. - -.. tacv:: autorewrite with {+ @ident} in @qualid using @tactic - - Performs all the rewritings in hypothesis :n:`@qualid` applying :n:`@tactic` - to the main subgoal after each rewriting step. - -.. tacv:: autorewrite with {+ @ident} in @goal_occurrences - - Performs all the rewriting in the clause :n:`@goal_occurrences`. - .. seealso:: - :ref:`Hint-Rewrite ` for feeding the database of lemmas used by + :cmd:`Hint Rewrite` for feeding the database of lemmas used by :tacn:`autorewrite` and :tacn:`autorewrite` for examples showing the use of this tactic. + Also see :ref:`strategies4rewriting`. .. tacn:: easy - :name: easy This tactic tries to solve the current goal by a number of standard closing steps. In particular, it tries to close the current goal using the closing tactics @@ -220,45 +206,43 @@ Programmable proof search This tactic solves goals that belong to many common classes; in particular, many cases of unsatisfiable hypotheses, and simple equality goals are usually solved by this tactic. -.. tacv:: now @tactic - :name: now +.. tacn:: now @ltac_expr Run :n:`@tactic` followed by :tacn:`easy`. This is a notation for :n:`@tactic; easy`. -Controlling automation --------------------------- - .. _thehintsdatabasesforautoandeauto: The hints databases for auto and eauto -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +-------------------------------------- The hints for :tacn:`auto` and :tacn:`eauto` are stored in databases. Each database -maps head symbols to a list of hints. - -.. cmd:: Print Hint @ident +maps head symbols to a list of hints. Use the :cmd:`Print Hint` command to view +the database. - Use this command - to display the hints associated to the head symbol :n:`@ident` - (see :ref:`Print Hint `). Each hint has a cost that is a nonnegative - integer, and an optional pattern. The hints with lower cost are tried first. A - hint is tried by :tacn:`auto` when the conclusion of the current goal matches its - pattern or when it has no pattern. +Each hint has a cost that is a nonnegative +integer and an optional pattern. Hints with lower costs are tried first. +:tacn:`auto` tries a hint when the conclusion of the current goal matches its +pattern or when the hint has no pattern. Creating Hint databases -``````````````````````` +----------------------- -One can optionally declare a hint database using the command -:cmd:`Create HintDb`. If a hint is added to an unknown database, it will be -automatically created. +Hint databases can be created with the :cmd:`Create HintDb` command or implicitly +by adding a hint to an unknown database. We recommend you always use :cmd:`Create HintDb` +and then imediately use :cmd:`Hint Constants` and :cmd:`Hint Variables` to make +those settings explicit. -.. cmd:: Create HintDb @ident {? discriminated} +Note that the default transparency +settings differ between these two methods of creation. Databases created with +:cmd:`Create HintDb` have the default setting `Transparent` for both `Variables` +and `Constants`, while implicitly created databases have the `Opaque` setting. - This command creates a new database named :n:`@ident`. The database is +.. cmd:: Create HintDb @ident {? discriminated } + + Creates a new hint database named :n:`@ident`. The database is implemented by a Discrimination Tree (DT) that serves as an index of all the lemmas. The DT can use transparency information to decide if a constant should be indexed or not - (c.f. :ref:`The hints databases for auto and eauto `), making the retrieval more efficient. The legacy implementation (the default one for new databases) uses the DT only on goals without existentials (i.e., :tacn:`auto` goals), for non-Immediate hints and does not make use of transparency @@ -270,149 +254,144 @@ automatically created. from the order in which they were inserted, making this implementation observationally different from the legacy one. -.. cmd:: Hint @hint_definition : {+ @ident} +.. _creating_hints: + +Creating Hints +-------------- - The general command to add a hint to some databases :n:`{+ @ident}`. + The various `Hint` commands share these elements: - This command supports the :attr:`local`, :attr:`global` and :attr:`export` - locality attributes. When no locality is explictly given, the - command is :attr:`local` inside a section and :attr:`global` otherwise. + :n:`{? : {+ @ident } }` specifies the hint database(s) to add to. + *(Deprecated since version 8.10:* If no :token:`ident`\s + are given, the hint is added to the `core` database.) + + Outside of sections, these commands support the :attr:`local`, :attr:`export` + and :attr:`global` attributes. :attr:`global` is the default. Inside sections, + only the :attr:`local` attribute is supported because hints are local to sections. + :attr:`local` hints are never visible from other modules, even if they - require or import the current module. Inside a section, the :attr:`local` - attribute is useless since hints do not survive anyway to the closure of - sections. + :cmd:`Import` or :cmd:`Require` the current module. - + :attr:`export` are visible from other modules when they import the current - module. Requiring it is not enough. + + :attr:`export` hints are visible from other modules when they :cmd:`Import` the current + module, but not when they only :cmd:`Require` it. This attribute is supported by + all `Hint` commands except for :cmd:`Hint Rewrite`. - + :attr:`global` hints are made available by merely requiring the current - module. + + :attr:`global` hints are visible from other modules when they :cmd:`Import` or + :cmd:`Require` the current module. .. deprecated:: 8.13 - The default value for hint locality is scheduled to change in a future + The default value for hint locality will change in a future release. For the time being, adding hints outside of sections without - specifying an explicit locality is therefore triggering a deprecation - warning. It is recommended to use :attr:`export` whenever possible - - The various possible :production:`hint_definition`\s are given below. - - .. cmdv:: Hint @hint_definition + specifying an explicit locality will trigger a deprecation + warning. We recommend you use :attr:`export` whenever possible. - No database name is given: the hint is registered in the ``core`` database. + The `Hint` commands are: - .. deprecated:: 8.10 + .. cmd:: Hint Resolve {+ {| @qualid | @one_term } } {? @hint_info } {? : {+ @ident } } + Hint Resolve {| -> | <- } {+ @qualid } {? @natural } {? : {+ @ident } } + :name: Hint Resolve; _ - .. cmdv:: Hint Resolve @qualid {? | {? @natural} {? @pattern}} : @ident - :name: Hint Resolve + .. insertprodn hint_info one_pattern - This command adds :n:`simple apply @qualid` to the hint list with the head - symbol of the type of :n:`@qualid`. The cost of that hint is the number of - subgoals generated by :n:`simple apply @qualid` or :n:`@natural` if specified. The - associated :n:`@pattern` is inferred from the conclusion of the type of - :n:`@qualid` or the given :n:`@pattern` if specified. In case the inferred type - of :n:`@qualid` does not start with a product the tactic added in the hint list - is :n:`exact @qualid`. In case this type can however be reduced to a type - starting with a product, the tactic :n:`simple apply @qualid` is also stored in - the hints list. If the inferred type of :n:`@qualid` contains a dependent - quantification on a variable which occurs only in the premisses of the type + .. prodn:: + hint_info ::= %| {? @natural } {? @one_pattern } + one_pattern ::= @one_term + + The first form adds each :n:`@qualid` as a hint with the head symbol of the type of + :n:`@qualid` to the specified hint databases (:n:`@ident`\s). The cost of the hint is the number of + subgoals generated by :tacn:`simple apply` :n:`@qualid` or, if specified, :n:`@natural`. The + associated pattern is inferred from the conclusion of the type of + :n:`@qualid` or, if specified, the given :n:`@one_pattern`. + + If the inferred type + of :n:`@qualid` does not start with a product, :tacn:`exact` :n:`@qualid` is added + to the hint list. If the type can be reduced to a type starting with a product, + :tacn:`simple apply` :n:`@qualid` is also added to the hints list. + + If the inferred type of :n:`@qualid` contains a dependent + quantification on a variable which occurs only in the premises of the type and not in its conclusion, no instance could be inferred for the variable by - unification with the goal. In this case, the hint is added to the hint list - of :tacn:`eauto` instead of the hint list of auto and a warning is printed. A - typical example of a hint that is used only by :tacn:`eauto` is a transitivity + unification with the goal. In this case, the hint is only used by + :tacn:`eauto` / :tacn:`typeclasses eauto`, but not by :tacn:`auto`. A + typical hint that would only be used by :tacn:`eauto` is a transitivity lemma. - .. exn:: @qualid cannot be used as a hint - - The head symbol of the type of :n:`@qualid` is a bound variable - such that this tactic cannot be associated to a constant. - - .. cmdv:: Hint Resolve {+ @qualid} : @ident + :n:`{| -> | <- }` + The second form adds the left-to-right (`->`) or right-ot-left implication (`<-`) + of an equivalence as a hint (informally + the hint will be used as, respectively, :tacn:`apply` :n:`-> @qualid` or + :tacn:`apply` :n:`<- @qualid`, + although as mentioned before, the tactic actually used is a restricted version of + :tacn:`apply`). - Adds each :n:`Hint Resolve @qualid`. + :n:`@one_term` + Permits declaring a hint without declaring a new + constant first, but this is not recommended. - .. cmdv:: Hint Resolve -> @qualid : @ident + .. warn:: Declaring arbitrary terms as hints is fragile; it is recommended to declare a toplevel constant instead + :undocumented: - Adds the left-to-right implication of an equivalence as a hint (informally - the hint will be used as :n:`apply <- @qualid`, although as mentioned - before, the tactic actually used is a restricted version of - :tacn:`apply`). - - .. cmdv:: Hint Resolve <- @qualid + .. exn:: @qualid cannot be used as a hint - Adds the right-to-left implication of an equivalence as a hint. + The head symbol of the type of :n:`@qualid` is a bound variable + such that this tactic cannot be associated to a constant. - .. cmdv:: Hint Immediate @qualid : @ident - :name: Hint Immediate + .. cmd:: Hint Immediate {+ {| @qualid | @one_term } } {? : {+ @ident } } - This command adds :n:`simple apply @qualid; trivial` to the hint list associated - with the head symbol of the type of :n:`@ident` in the given database. This - tactic will fail if all the subgoals generated by :n:`simple apply @qualid` are + Adds :tacn:`simple apply` :n:`@qualid;` :tacn:`trivial` to the hint list for each :n:`@qualid` associated + with the head symbol of the type of :n:`@ident`. This + tactic will fail if all the subgoals generated by :tacn:`simple apply` :n:`@qualid` are not solved immediately by the :tacn:`trivial` tactic (which only tries tactics - with cost 0).This command is useful for theorems such as the symmetry of - equality or :g:`n+1=m+1 -> n=m` that we may like to introduce with a limited - use in order to avoid useless proof-search. The cost of this tactic (which + with cost 0). This command is useful for theorems such as the symmetry of + equality or :g:`n+1=m+1 -> n=m` that we may want to introduce with limited + use in order to avoid useless proof search. The cost of this tactic (which never generates subgoals) is always 1, so that it is not used by :tacn:`trivial` itself. - .. exn:: @qualid cannot be used as a hint - :undocumented: + .. cmd:: Hint Constructors {+ @qualid } {? : {+ @ident } } - .. cmdv:: Hint Immediate {+ @qualid} : @ident - - Adds each :n:`Hint Immediate @qualid`. - - .. cmdv:: Hint Constructors @qualid : @ident - :name: Hint Constructors - - If :token:`qualid` is an inductive type, this command adds all its constructors as + For each :n:`@qualid` that is an inductive type, adds all its constructors as hints of type ``Resolve``. Then, when the conclusion of current goal has the form :n:`(@qualid ...)`, :tacn:`auto` will try to apply each constructor. .. exn:: @qualid is not an inductive type :undocumented: - .. cmdv:: Hint Constructors {+ @qualid} : @ident - - Extends the previous command for several inductive types. + .. cmd:: Hint Unfold {+ @qualid } {? : {+ @ident } } - .. cmdv:: Hint Unfold @qualid : @ident - :name: Hint Unfold - - This adds the tactic :n:`unfold @qualid` to the hint list that will only be - used when the head constant of the goal is :token:`qualid`. + For each :n:`@qualid`, adds the tactic :tacn:`unfold` :n:`@qualid` to the + hint list that will only be used when the head constant of the goal is :token:`qualid`. Its cost is 4. - .. cmdv:: Hint Unfold {+ @qualid} - - Extends the previous command for several defined constants. - - .. cmdv:: Hint Transparent {+ @qualid} : @ident - Hint Opaque {+ @qualid} : @ident + .. cmd:: Hint {| Transparent | Opaque } {+ @qualid } {? : {+ @ident } } :name: Hint Transparent; Hint Opaque - This adds transparency hints to the database, making :n:`@qualid` - transparent or opaque constants during resolution. This information is used + Adds transparency hints to the database, making each :n:`@qualid` + a transparent or opaque constant during resolution. This information is used during unification of the goal with any lemma in the database and inside the discrimination network to relax or constrain it in the case of discriminated databases. - .. cmdv:: Hint Variables {| Transparent | Opaque } : @ident - Hint Constants {| Transparent | Opaque } : @ident - :name: Hint Variables; Hint Constants + .. cmd:: Hint {| Constants | Variables } {| Transparent | Opaque } {? : {+ @ident } } + :name: Hint Constants; Hint Variables - This sets the transparency flag used during unification of - hints in the database for all constants or all variables, - overwriting the existing settings of opacity. It is advised - to use this just after a :cmd:`Create HintDb` command. + Sets the transparency flag for constants or variables for the specified hint + databases. + These flags affect the unification of hints in the database. + We advise using this just after a :cmd:`Create HintDb` command. - .. cmdv:: Hint Extern @natural {? @pattern} => @tactic : @ident - :name: Hint Extern + .. cmd:: Hint Extern @natural {? @one_pattern } => @ltac_expr {? : {+ @ident } } - This hint type is to extend :tacn:`auto` with tactics other than :tacn:`apply` and - :tacn:`unfold`. For that, we must specify a cost, an optional :n:`@pattern` and a - :n:`@tactic` to execute. + Extends :tacn:`auto` with tactics other than :tacn:`apply` and + :tacn:`unfold`. :n:`@natural` is the cost, :n:`@one_term` is the pattern + to match and :n:`@ltac_expr` is the action to apply. + + .. note:: + + Use a :cmd:`Hint Extern` with no pattern to do + pattern matching on hypotheses using ``match goal with`` + inside the tactic. .. example:: @@ -441,80 +420,131 @@ automatically created. .. coqtop:: all Require Import List. - Hint Extern 5 ({?X1 = ?X2} + {?X1 <> ?X2}) => generalize X1, X2; decide equality : eqdec. + Hint Extern 5 ({?X1 = ?X2} + {?X1 <> ?X2}) => + generalize X1, X2; decide equality : eqdec. Goal forall a b:list (nat * nat), {a = b} + {a <> b}. - Info 1 auto with eqdec. + info_auto. - .. cmdv:: Hint Cut @regexp : @ident - :name: Hint Cut + .. cmd:: Hint Cut [ @hints_regexp ] {? : {+ @ident } } - .. warning:: - - These hints currently only apply to typeclass proof search and the - :tacn:`typeclasses eauto` tactic. - - This command can be used to cut the proof-search tree according to a regular - expression matching paths to be cut. The grammar for regular expressions is - the following. Beware, there is no operator precedence during parsing, one can - check with :cmd:`Print HintDb` to verify the current cut expression: + .. DISABLED insertprodn hints_regexp hints_regexp .. prodn:: - regexp ::= @ident (hint or instance identifier) + hints_regexp ::= {+ @qualid } (hint or instance identifier) | _ (any hint) - | @regexp | @regexp (disjunction) - | @regexp @regexp (sequence) - | @regexp * (Kleene star) + | @hints_regexp | @hints_regexp (disjunction) + | @hints_regexp @hints_regexp (sequence) + | @hints_regexp * (Kleene star) | emp (empty) | eps (epsilon) - | ( @regexp ) + | ( @hints_regexp ) + + Used to cut the proof search tree according to a regular + expression that matches the paths to be cut. + - The `emp` regexp does not match any search path while `eps` - matches the empty path. During proof search, the path of - successive successful hints on a search branch is recorded, as a - list of identifiers for the hints (note that :cmd:`Hint Extern`\’s do not have + During proof search, the path of + successive successful hints on a search branch is recorded as a + list of identifiers for the hints (note that :cmd:`Hint Extern`\s do not have an associated identifier). - Before applying any hint :n:`@ident` the current path `p` extended with - :n:`@ident` is matched against the current cut expression `c` associated to - the hint database. If matching succeeds, the hint is *not* applied. The - semantics of :n:`Hint Cut @regexp` is to set the cut expression - to :n:`c | regexp`, the initial cut expression being `emp`. - - .. cmdv:: Hint Mode @qualid {* {| + | ! | - } } : @ident - :name: Hint Mode - - This sets an optional mode of use of the identifier :n:`@qualid`. When - proof-search faces a goal that ends in an application of :n:`@qualid` to - arguments :n:`@term ... @term`, the mode tells if the hints associated to - :n:`@qualid` can be applied or not. A mode specification is a list of n ``+``, + For each hint :n:`@qualid` in the hint database, the current path `p` + extended with :n:`@qualid` + is matched against the current cut expression `c` associated with the + hint database. If the match succeeds the hint is *not* applied. + + :n:`Hint Cut @hints_regexp` sets the cut expression + to :n:`c | @hints_regexp`. The initial cut expression is `emp`. + + The output of :cmd:`Print HintDb` shows the cut expression. + + .. warning:: + + There is no operator precedence during parsing, one can + check with :cmd:`Print HintDb` to verify the current cut expression. + + .. warning:: + + These hints currently only apply to typeclass proof search and the + :tacn:`typeclasses eauto` tactic. + + .. cmd:: Hint Mode @qualid {+ {| + | ! | - } } {? : {+ @ident } } + + Sets an optional mode of use for the identifier :n:`@qualid`. When + proof search has a goal that ends in an application of :n:`@qualid` to + arguments :n:`@arg ... @arg`, the mode tells if the hints associated with + :n:`@qualid` can be applied or not. A mode specification is a list of ``+``, ``!`` or ``-`` items that specify if an argument of the identifier is to be treated as an input (``+``), if its head only is an input (``!``) or an output (``-``) of the identifier. For a mode to match a list of arguments, input terms and input heads *must not* contain existential variables or be - existential variables respectively, while outputs can be any term. Multiple - modes can be declared for a single identifier, in that case only one mode - needs to match the arguments for the hints to be applied. The head of a term + existential variables respectively, while outputs can be any term. + + The head of a term is understood here as the applicative head, or the match or projection scrutinee’s head, recursively, casts being ignored. :cmd:`Hint Mode` is especially useful for typeclasses, when one does not want to support default instances and avoid ambiguity in general. Setting a parameter of a class as an - input forces proof-search to be driven by that index of the class, with ``!`` - giving more flexibility by allowing existentials to still appear deeper in the - index but not at its head. + input forces proof search to be driven by that index of the class, with ``!`` + allowing existentials to appear in the index but not at its head. .. note:: - + One can use a :cmd:`Hint Extern` with no pattern to do - pattern matching on hypotheses using ``match goal with`` - inside the tactic. + + Multiple modes can be declared for a single identifier. In that + case only one mode needs to match the arguments for the hints to be applied. + If you want to add hints such as :cmd:`Hint Transparent`, :cmd:`Hint Cut`, or :cmd:`Hint Mode`, for typeclass resolution, do not forget to put them in the ``typeclass_instances`` hint database. +.. cmd:: Hint Rewrite {? {| -> | <- } } {+ @one_term } {? using @ltac_expr } {? : {* @ident } } + + :n:`{? using @ltac_expr }` + If specified, :n:`@ltac_expr` is applied to the generated subgoals, except for the + main subgoal. + + :n:`{| -> | <- }` + Arrows specify the orientation; left to right (:n:`->`) or right to left (:n:`<-`). + If no arrow is given, the default orientation is left to right (:n:`->`). + + Adds the terms :n:`{+ @one_term }` (their types must be + equalities) to the rewriting bases :n:`{* @ident }`. + Note that the rewriting bases are distinct from the :tacn:`auto` + hint bases and that :tacn:`auto` does not take them into account. + + .. cmd:: Print Rewrite HintDb @ident + + This command displays all rewrite hints contained in :n:`@ident`. + +.. cmd:: Remove Hints {+ @qualid } {? : {+ @ident } } + + Removes the hints associated with the :n:`{+ @qualid }` in databases + :n:`{+ @ident}`. Note: hints created with :cmd:`Hint Extern` currently + can't be removed. The best workaround for this is to make the hints + non global and carefully select which modules you import. + +.. cmd:: Print Hint {? {| * | @reference } } + + :n:`*` + Display all declared hints. + + :n:`@reference` + Display all hints associated with the head symbol :n:`@reference`. + + Displays tactics from the hints list. The default is to show hints that + apply to the conclusion of the current goal. The other forms with :n:`*` + and :n:`@reference` can be used even if no proof is open. + + Each hint has a cost that is a nonnegative + integer and an optional pattern. The hints with lower cost are tried first. + +.. cmd:: Print HintDb @ident + + This command displays all hints from database :n:`@ident`. + Hint databases defined in the Coq standard library -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +-------------------------------------------------- Several hint databases are defined in the Coq standard library. The actual content of a database is the collection of hints declared @@ -555,76 +585,8 @@ At Coq startup, only the core database is nonempty and can be used. You are advised not to put your own hints in the core database, but use one or several databases specific to your development. -.. _removehints: - -.. cmd:: Remove Hints {+ @term} : {+ @ident} - - This command removes the hints associated to terms :n:`{+ @term}` in databases - :n:`{+ @ident}`. - -.. _printhint: - -.. cmd:: Print Hint - - This command displays all hints that apply to the current goal. It - fails if no proof is being edited, while the two variants can be used - at every moment. - -**Variants:** - - -.. cmd:: Print Hint @ident - - This command displays only tactics associated with :n:`@ident` in the hints - list. This is independent of the goal being edited, so this command will not - fail if no goal is being edited. - -.. cmd:: Print Hint * - - This command displays all declared hints. - -.. cmd:: Print HintDb @ident - - This command displays all hints from database :n:`@ident`. - -.. _hintrewrite: - -.. cmd:: Hint Rewrite {+ @term} : {+ @ident} - - This vernacular command adds the terms :n:`{+ @term}` (their types must be - equalities) in the rewriting bases :n:`{+ @ident}` with the default orientation - (left to right). Notice that the rewriting bases are distinct from the :tacn:`auto` - hint bases and that :tacn:`auto` does not take them into account. - - This command is synchronous with the section mechanism (see :ref:`section-mechanism`): - when closing a section, all aliases created by ``Hint Rewrite`` in that - section are lost. Conversely, when loading a module, all ``Hint Rewrite`` - declarations at the global level of that module are loaded. - -**Variants:** - -.. cmd:: Hint Rewrite -> {+ @term} : {+ @ident} - - This is strictly equivalent to the command above (we only make explicit the - orientation which otherwise defaults to ->). - -.. cmd:: Hint Rewrite <- {+ @term} : {+ @ident} - - Adds the rewriting rules :n:`{+ @term}` with a right-to-left orientation in - the bases :n:`{+ @ident}`. - -.. cmd:: Hint Rewrite {? {| -> | <- } } {+ @one_term } {? using @ltac_expr } {? : {* @ident } } - - When the rewriting rules :n:`{+ @term}` in :n:`{+ @ident}` will be used, the - tactic ``tactic`` will be applied to the generated subgoals, the main subgoal - excluded. - -.. cmd:: Print Rewrite HintDb @ident - - This command displays all rewrite hints contained in :n:`@ident`. - Hint locality -~~~~~~~~~~~~~ +------------- Hints provided by the ``Hint`` commands are erased when closing a section. Conversely, all hints of a module ``A`` that are not defined inside a @@ -649,7 +611,6 @@ option which accepts three flags allowing for a fine-grained handling of non-imported hints. .. opt:: Loose Hint Behavior {| "Lax" | "Warn" | "Strict" } - :name: Loose Hint Behavior This option accepts three values, which control the behavior of hints w.r.t. :cmd:`Import`: @@ -668,22 +629,12 @@ non-imported hints. .. _tactics-implicit-automation: Setting implicit automation tactics -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +----------------------------------- -.. cmd:: Proof with @tactic +.. cmd:: Proof with @ltac_expr {? using @section_var_expr } - This command may be used to start a proof. It defines a default tactic - to be used each time a tactic command ``tactic``:sub:`1` is ended by ``...``. - In this case the tactic command typed by the user is equivalent to - ``tactic``:sub:`1` ``;tactic``. + Starts a proof in which :token:`ltac_expr` is applied to the active goals + after each tactic that ends with `...` instead of the usual single period. + ":n:`@tactic...`" is equivalent to ":n:`@tactic; @ltac_expr.`". .. seealso:: :cmd:`Proof` in :ref:`proof-editing-mode`. - - - .. cmdv:: Proof with @tactic using {+ @ident} - - Combines in a single line ``Proof with`` and ``Proof using``, see :ref:`proof-editing-mode` - - .. cmdv:: Proof using {+ @ident} with @tactic - - Combines in a single line ``Proof with`` and ``Proof using``, see :ref:`proof-editing-mode` diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst index 9ec568c2c7a9..2de6b2a18cdc 100644 --- a/doc/sphinx/proofs/writing-proofs/rewriting.rst +++ b/doc/sphinx/proofs/writing-proofs/rewriting.rst @@ -295,21 +295,21 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. Performing computations --------------------------- -.. insertprodn red_expr pattern_occ +.. insertprodn red_expr pattern_occs .. prodn:: red_expr ::= red | hnf - | simpl {? @delta_flag } {? @ref_or_pattern_occ } + | simpl {? @delta_flag } {? {| @reference_occs | @pattern_occs } } | cbv {? @strategy_flag } | cbn {? @strategy_flag } | lazy {? @strategy_flag } | compute {? @delta_flag } - | vm_compute {? @ref_or_pattern_occ } - | native_compute {? @ref_or_pattern_occ } - | unfold {+, @unfold_occ } + | vm_compute {? {| @reference_occs | @pattern_occs } } + | native_compute {? {| @reference_occs | @pattern_occs } } + | unfold {+, @reference_occs } | fold {+ @one_term } - | pattern {+, @pattern_occ } + | pattern {+, @pattern_occs } | @ident delta_flag ::= {? - } [ {+ @reference } ] strategy_flag ::= {+ @red_flag } @@ -321,16 +321,8 @@ Performing computations | cofix | zeta | delta {? @delta_flag } - ref_or_pattern_occ ::= @reference {? at @occs_nums } - | @one_term {? at @occs_nums } - occs_nums ::= {+ @nat_or_var } - | - {+ @nat_or_var } - int_or_var ::= @integer - | @ident - nat_or_var ::= @natural - | @ident - unfold_occ ::= @reference {? at @occs_nums } - pattern_occ ::= @one_term {? at @occs_nums } + reference_occs ::= @reference {? at @occs_nums } + pattern_occs ::= @one_term {? at @occs_nums } This set of tactics implements different specialized usages of the tactic :tacn:`change`. @@ -348,17 +340,6 @@ clauses) and are introduced by the keyword `in`. If no goal clause is provided, the default is to perform the conversion only in the conclusion. -The syntax and description of the various goal clauses is the -following: - -+ :n:`in {+ @ident} |-` only in hypotheses :n:`{+ @ident}` -+ :n:`in {+ @ident} |- *` in hypotheses :n:`{+ @ident}` and in the - conclusion -+ :n:`in * |-` in every hypothesis -+ :n:`in *` (equivalent to in :n:`* |- *`) everywhere -+ :n:`in (type of @ident) (value of @ident) ... |-` in type part of - :n:`@ident`, in the value part of :n:`@ident`, etc. - For backward compatibility, the notation :n:`in {+ @ident}` performs the conversion in hypotheses :n:`{+ @ident}`. diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index 4080eaae08a1..8efda825de5a 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -19,8 +19,22 @@ lglob: [ ] hint: [ +| REPLACE "Resolve" "->" LIST1 global OPT natural +| WITH "Resolve" [ "->" | "<-" ] LIST1 global OPT natural +| DELETE "Resolve" "<-" LIST1 global OPT natural +| REPLACE "Variables" "Transparent" +| WITH [ "Constants" | "Variables" ] [ "Transparent" | "Opaque" ] +| DELETE "Variables" "Opaque" +| DELETE "Constants" "Transparent" +| DELETE "Constants" "Opaque" +| REPLACE "Transparent" LIST1 global +| WITH [ "Transparent" | "Opaque" ] LIST1 global +| DELETE "Opaque" LIST1 global + | REPLACE "Extern" natural OPT Constr.constr_pattern "=>" Pltac.tactic | WITH "Extern" natural OPT constr_pattern "=>" tactic +| INSERTALL "Hint" +| APPENDALL opt_hintbases ] (* todo: does ARGUMENT EXTEND make the symbol global? It is in both extraargs and extratactics *) @@ -149,6 +163,7 @@ DELETE: [ | ensure_fixannot | test_array_opening | test_array_closing +| test_variance_ident (* SSR *) | ssr_null_entry @@ -267,7 +282,7 @@ binder_constr: [ | REPLACE "if" term200 "is" ssr_dthen ssr_else | WITH "if" term200 [ "is" | "isn't" ] ssr_dthen ssr_else TAG SSR | DELETE "if" term200 "isn't" ssr_dthen ssr_else -| DELETE "if" term200 [ "is" | "isn't" ] ssr_dthen ssr_else TAG SSR (* todo: restore for SSR *) +| DELETE "if" term200 [ "is" | "isn't" ] ssr_dthen ssr_else TAG SSR (* todo: restore as "MOVETO term_if" for SSR *) | MOVETO term_fix "let" "fix" fix_decl "in" term200 | MOVETO term_cofix "let" "cofix" cofix_body "in" term200 | MOVETO term_let "let" [ "(" LIST0 name SEP "," ")" | "()" ] as_return_type ":=" term200 "in" term200 @@ -597,6 +612,11 @@ univ_decl: [ | WITH "@{" LIST0 identref OPT "+" OPT [ "|" LIST0 univ_constraint SEP "," OPT "+" ] "}" ] +cumul_univ_decl: [ +| REPLACE "@{" LIST0 variance_identref [ "+" | ] [ "|" LIST0 univ_constraint SEP "," [ "+" | ] "}" | [ "}" | bar_cbrace ] ] +| WITH "@{" LIST0 variance_identref OPT "+" OPT [ "|" LIST0 univ_constraint SEP "," OPT "+" ] "}" +] + of_type: [ | DELETENT ] @@ -905,12 +925,13 @@ where: [ ] simple_tactic: [ -| DELETE "intros" -| REPLACE "intros" ne_intropatterns -| WITH "intros" intropatterns -| DELETE "eintros" -| REPLACE "eintros" ne_intropatterns -| WITH "eintros" intropatterns +| REPLACE "eauto" OPT nat_or_var OPT nat_or_var auto_using hintbases +| WITH "eauto" OPT nat_or_var auto_using hintbases +| REPLACE "debug" "eauto" OPT nat_or_var OPT nat_or_var auto_using hintbases +| WITH "debug" "eauto" OPT nat_or_var auto_using hintbases +| REPLACE "info_eauto" OPT nat_or_var OPT nat_or_var auto_using hintbases +| WITH "info_eauto" OPT nat_or_var auto_using hintbases + | DELETE "autorewrite" "with" LIST1 preident clause | DELETE "autorewrite" "with" LIST1 preident clause "using" tactic | DELETE "autorewrite" "*" "with" LIST1 preident clause @@ -966,6 +987,12 @@ simple_tactic: [ | DELETE "intro" "after" hyp | DELETE "intro" "before" hyp | "intro" OPT ident OPT where +| DELETE "intros" +| REPLACE "intros" ne_intropatterns +| WITH "intros" intropatterns +| DELETE "eintros" +| REPLACE "eintros" ne_intropatterns +| WITH "eintros" intropatterns | DELETE "move" hyp "at" "top" | DELETE "move" hyp "at" "bottom" | DELETE "move" hyp "after" hyp @@ -1139,6 +1166,10 @@ printable: [ | REPLACE [ "Sorted" | ] "Universes" OPT printunivs_subgraph OPT ne_string | WITH OPT "Sorted" "Universes" OPT printunivs_subgraph OPT ne_string | DELETE "Term" smart_global OPT univ_name_list (* readded in commands *) +| REPLACE "Hint" +| WITH "Hint" OPT [ "*" | smart_global ] +| DELETE "Hint" smart_global +| DELETE "Hint" "*" | INSERTALL "Print" ] @@ -1163,6 +1194,8 @@ scheme_kind: [ command: [ | REPLACE "Print" printable | WITH printable +| REPLACE "Hint" hint opt_hintbases +| WITH hint | "SubClass" ident_decl def_body | REPLACE "Ltac" LIST1 ltac_tacdef_body SEP "with" | WITH "Ltac" ltac_tacdef_body LIST0 ( "with" ltac_tacdef_body ) @@ -1242,6 +1275,9 @@ command: [ | REPLACE "Preterm" "of" ident | WITH "Preterm" OPT ( "of" ident ) | DELETE "Preterm" +| REPLACE "Proof" "using" section_var_expr "with" Pltac.tactic +| WITH "Proof" "using" section_subset_expr OPT [ "with" ltac_expr5 ] +| DELETE "Proof" "using" section_var_expr (* hide the fact that table names are limited to 2 IDENTs *) | REPLACE "Remove" IDENT IDENT LIST1 table_value @@ -1441,8 +1477,8 @@ type_cstr: [ ] inductive_definition: [ -| REPLACE opt_coercion ident_decl binders OPT [ "|" binders ] OPT [ ":" lconstr ] opt_constructors_or_fields decl_notations -| WITH opt_coercion ident_decl binders OPT [ "|" binders ] OPT [ ":" type ] opt_constructors_or_fields decl_notations +| REPLACE opt_coercion cumul_ident_decl binders OPT [ "|" binders ] OPT [ ":" lconstr ] opt_constructors_or_fields decl_notations +| WITH opt_coercion cumul_ident_decl binders OPT [ "|" binders ] OPT [ ":" type ] opt_constructors_or_fields decl_notations ] (* note that constructor -> identref constructor_type *) @@ -1578,9 +1614,12 @@ simple_reserv: [ in_clause: [ | DELETE in_clause' -| REPLACE LIST0 hypident_occ SEP "," "|-" concl_occ -| WITH LIST0 hypident_occ SEP "," OPT ( "|-" concl_occ ) -| DELETE LIST0 hypident_occ SEP "," +| REPLACE LIST1 hypident_occ SEP "," "|-" concl_occ +| WITH LIST1 hypident_occ SEP "," OPT ( "|-" concl_occ ) +| DELETE LIST1 hypident_occ SEP "," +| REPLACE "*" occs +| WITH concl_occ +(* todo: perhaps concl_occ should be "*" | "at" occs_nums *) ] ltac2_in_clause: [ @@ -1791,6 +1830,7 @@ tactic_notation_tactics: [ | "field_simplify" OPT ( "[" LIST1 constr "]" ) LIST1 constr OPT ( "in" ident ) | "field_simplify_eq" OPT ( "[" LIST1 constr "]" ) OPT ( "in" ident ) | "intuition" OPT ltac_expr5 (* todo: Not too keen on things like "with_power_flags" in tauto.ml, not easy to follow *) +| "now" ltac_expr5 | "nsatz" OPT ( "with" "radicalmax" ":=" constr "strategy" ":=" constr "parameters" ":=" constr "variables" ":=" constr ) | "psatz" constr OPT nat_or_var | "ring" OPT ( "[" LIST1 constr "]" ) @@ -1942,6 +1982,18 @@ tac2rec_fields: [ | LIST1 tac2rec_field SEP ";" OPT ";" TAG Ltac2 ] +int_or_var: [ +| REPLACE integer +| WITH [ integer | identref ] +| DELETE identref +] + +nat_or_var: [ +| REPLACE natural +| WITH [ natural | identref ] +| DELETE identref +] + ltac2_occs_nums: [ | DELETE LIST1 nat_or_anti (* Ltac2 plugin *) | REPLACE "-" nat_or_anti LIST0 nat_or_anti (* Ltac2 plugin *) @@ -2387,6 +2439,33 @@ attribute: [ | DELETE "using" OPT attr_value ] +hypident: [ +(* todo: restore for SSR *) +| DELETE "(" "type" "of" ident ")" (* SSR plugin *) +| DELETE "(" "value" "of" ident ")" (* SSR plugin *) +] + +ref_or_pattern_occ: [ +| DELETE smart_global OPT occs +| DELETE constr OPT occs +| unfold_occ +| pattern_occ +] + +clause_dft_concl: [ +(* omit an OPT since clause_dft_concl is always OPT *) +| REPLACE OPT occs +| WITH occs +] + +occs_nums: [ +| EDIT ADD_OPT "-" LIST1 nat_or_var +] + +variance_identref: [ +| EDIT ADD_OPT variance identref +] + SPLICE: [ | clause | noedit_mode @@ -2526,6 +2605,7 @@ SPLICE: [ | eliminator (* todo: splice or not? *) | quoted_attributes (* todo: splice or not? *) | printable +| hint | only_parsing | record_fields | constructor_type @@ -2606,8 +2686,17 @@ SPLICE: [ | syn_level | firstorder_rhs | firstorder_using +| hints_path_atom +| ref_or_pattern_occ +| cumul_ident_decl +| variance +| variance_identref ] (* end SPLICE *) +RENAME: [ +| occurrences rewrite_occs +] + RENAME: [ | tactic3 ltac_expr3 (* todo: can't figure out how this gets mapped by coqpp *) | tactic1 ltac_expr1 (* todo: can't figure out how this gets mapped by coqpp *) @@ -2652,6 +2741,13 @@ RENAME: [ | ssrclauses ssr_in | ssrcpat ssrblockpat | constr_pattern one_pattern +| hints_path hints_regexp +| clause_dft_concl occurrences +| in_clause goal_occurrences +| unfold_occ reference_occs +| pattern_occ pattern_occs +| hypident_occ hyp_occs +| concl_occ concl_occs ] simple_tactic: [ diff --git a/doc/tools/docgram/doc_grammar.ml b/doc/tools/docgram/doc_grammar.ml index ae66520d89f1..dd7990368ee2 100644 --- a/doc/tools/docgram/doc_grammar.ml +++ b/doc/tools/docgram/doc_grammar.ml @@ -527,28 +527,28 @@ let rec edit_SELF nt cur_level next_level right_assoc inner prod = prod -let autoloaded_mlgs = [ (* in the order they are loaded by Coq *) +let autoloaded_mlgs = [ (* productions from other mlgs are marked with TAGs *) "parsing/g_constr.mlg"; "parsing/g_prim.mlg"; - "vernac/g_vernac.mlg"; - "vernac/g_proofs.mlg"; - "toplevel/g_toplevel.mlg"; - "plugins/ltac/extraargs.mlg"; - "plugins/ltac/g_obligations.mlg"; + "plugins/btauto/g_btauto.mlg"; + "plugins/cc/g_congruence.mlg"; + "plugins/firstorder/g_ground.mlg"; "plugins/ltac/coretactics.mlg"; + "plugins/ltac/extraargs.mlg"; "plugins/ltac/extratactics.mlg"; - "plugins/ltac/profile_ltac_tactics.mlg"; "plugins/ltac/g_auto.mlg"; "plugins/ltac/g_class.mlg"; - "plugins/ltac/g_rewrite.mlg"; "plugins/ltac/g_eqdecide.mlg"; - "plugins/ltac/g_tactic.mlg"; "plugins/ltac/g_ltac.mlg"; - "plugins/btauto/g_btauto.mlg"; + "plugins/ltac/g_obligations.mlg"; + "plugins/ltac/g_rewrite.mlg"; + "plugins/ltac/g_tactic.mlg"; + "plugins/ltac/profile_ltac_tactics.mlg"; "plugins/rtauto/g_rtauto.mlg"; - "plugins/cc/g_congruence.mlg"; - "plugins/firstorder/g_ground.mlg"; "plugins/syntax/g_number_string.mlg"; + "toplevel/g_toplevel.mlg"; + "vernac/g_proofs.mlg"; + "vernac/g_vernac.mlg"; ] @@ -1726,7 +1726,6 @@ let process_rst g file args seen tac_prods cmd_prods = let cmd_exclude_files = [ "doc/sphinx/proof-engine/ssreflect-proof-language.rst"; - "doc/sphinx/proofs/automatic-tactics/auto.rst"; "doc/sphinx/proofs/writing-proofs/rewriting.rst"; "doc/sphinx/proofs/writing-proofs/proof-mode.rst"; "doc/sphinx/proof-engine/tactics.rst"; diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index d01f66c6d7d0..cf90eea5a19d 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -342,6 +342,21 @@ closed_binder: [ | [ "of" | "&" ] term99 (* SSR plugin *) ] +one_open_binder: [ +| name +| name ":" lconstr +| one_closed_binder +] + +one_closed_binder: [ +| "(" name ":" lconstr ")" +| "{" name "}" +| "{" name ":" lconstr "}" +| "[" name "]" +| "[" name ":" lconstr "]" +| "'" pattern0 +] + typeclass_constraint: [ | "!" term200 | "{" name "}" ":" [ "!" | ] term200 @@ -875,10 +890,29 @@ univ_decl: [ | "@{" LIST0 identref [ "+" | ] [ "|" LIST0 univ_constraint SEP "," [ "+" | ] "}" | [ "}" | bar_cbrace ] ] ] +variance: [ +| "+" +| "=" +| "*" +] + +variance_identref: [ +| identref +| test_variance_ident variance identref +] + +cumul_univ_decl: [ +| "@{" LIST0 variance_identref [ "+" | ] [ "|" LIST0 univ_constraint SEP "," [ "+" | ] "}" | [ "}" | bar_cbrace ] ] +] + ident_decl: [ | identref OPT univ_decl ] +cumul_ident_decl: [ +| identref OPT cumul_univ_decl +] + finite_token: [ | "Inductive" | "CoInductive" @@ -918,7 +952,7 @@ opt_constructors_or_fields: [ ] inductive_definition: [ -| opt_coercion ident_decl binders OPT [ "|" binders ] OPT [ ":" lconstr ] opt_constructors_or_fields decl_notations +| opt_coercion cumul_ident_decl binders OPT [ "|" binders ] OPT [ ":" lconstr ] opt_constructors_or_fields decl_notations ] constructors_or_record: [ @@ -1914,8 +1948,9 @@ in_clause: [ | in_clause' | "*" occs | "*" "|-" concl_occ -| LIST0 hypident_occ SEP "," "|-" concl_occ -| LIST0 hypident_occ SEP "," +| "|-" concl_occ +| LIST1 hypident_occ SEP "," "|-" concl_occ +| LIST1 hypident_occ SEP "," ] test_lpar_id_colon: [ @@ -2493,7 +2528,7 @@ in_hyp_list: [ ] in_hyp_as: [ -| "in" id_or_meta as_ipat +| "in" LIST1 [ id_or_meta as_ipat ] SEP "," | ] diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index f62dd8f731eb..7c709baa4805 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -436,7 +436,7 @@ univ_decl: [ ] cumul_univ_decl: [ -| "@{" LIST0 ( OPT [ "=" | "+" | "*" ] ident ) OPT "+" OPT [ "|" LIST0 univ_constraint SEP "," OPT "+" ] "}" +| "@{" LIST0 ( OPT [ "+" | "=" | "*" ] ident ) OPT "+" OPT [ "|" LIST0 univ_constraint SEP "," OPT "+" ] "}" ] univ_constraint: [ @@ -512,6 +512,21 @@ binder: [ | "'" pattern0 ] +one_open_binder: [ +| name +| name ":" term +| one_closed_binder +] + +one_closed_binder: [ +| "(" name ":" term ")" +| "{" name "}" +| "{" name ":" term "}" +| "[" name "]" +| "[" name ":" term "]" +| "'" pattern0 +] + implicit_binders: [ | "{" LIST1 name OPT ( ":" type ) "}" | "[" LIST1 name OPT ( ":" type ) "]" @@ -614,16 +629,16 @@ reduce: [ red_expr: [ | "red" | "hnf" -| "simpl" OPT delta_flag OPT ref_or_pattern_occ +| "simpl" OPT delta_flag OPT [ reference_occs | pattern_occs ] | "cbv" OPT strategy_flag | "cbn" OPT strategy_flag | "lazy" OPT strategy_flag | "compute" OPT delta_flag -| "vm_compute" OPT ref_or_pattern_occ -| "native_compute" OPT ref_or_pattern_occ -| "unfold" LIST1 unfold_occ SEP "," +| "vm_compute" OPT [ reference_occs | pattern_occs ] +| "native_compute" OPT [ reference_occs | pattern_occs ] +| "unfold" LIST1 reference_occs SEP "," | "fold" LIST1 one_term -| "pattern" LIST1 pattern_occ SEP "," +| "pattern" LIST1 pattern_occs SEP "," | ident ] @@ -646,31 +661,11 @@ red_flag: [ | "delta" OPT delta_flag ] -ref_or_pattern_occ: [ +reference_occs: [ | reference OPT ( "at" occs_nums ) -| one_term OPT ( "at" occs_nums ) -] - -occs_nums: [ -| LIST1 nat_or_var -| "-" LIST1 nat_or_var -] - -int_or_var: [ -| integer -| ident ] -nat_or_var: [ -| natural -| ident -] - -unfold_occ: [ -| reference OPT ( "at" occs_nums ) -] - -pattern_occ: [ +pattern_occs: [ | one_term OPT ( "at" occs_nums ) ] @@ -705,7 +700,7 @@ field_def: [ ] inductive_definition: [ -| OPT ">" cumul_ident_decl LIST0 binder OPT [ "|" LIST0 binder ] OPT [ ":" type ] OPT ( ":=" OPT constructors_or_record ) OPT decl_notations +| OPT ">" ident OPT cumul_univ_decl LIST0 binder OPT [ "|" LIST0 binder ] OPT [ ":" type ] OPT ( ":=" OPT constructors_or_record ) OPT decl_notations ] constructors_or_record: [ @@ -717,10 +712,6 @@ constructor: [ | ident LIST0 binder OPT of_type ] -cumul_ident_decl: [ -| ident OPT cumul_univ_decl -] - filtered_import: [ | qualid OPT [ "(" LIST1 ( qualid OPT [ "(" ".." ")" ] ) SEP "," ")" ] ] @@ -901,9 +892,7 @@ command: [ | "Print" "Typing" "Flags" | "Print" "Tables" | "Print" "Options" -| "Print" "Hint" -| "Print" "Hint" reference -| "Print" "Hint" "*" +| "Print" "Hint" OPT [ "*" | reference ] | "Print" "HintDb" ident | "Print" "Scopes" | "Print" "Scope" scope_name @@ -958,7 +947,6 @@ command: [ | "Extract" "Inductive" qualid "=>" [ ident | string ] "[" LIST0 [ ident | string ] "]" OPT string (* extraction plugin *) | "Show" "Extraction" (* extraction plugin *) | "Proof" -| "Proof" "using" section_var_expr | "Proof" "Mode" string | "Proof" term | "Abort" OPT [ "All" | ident ] @@ -983,7 +971,6 @@ command: [ | "Guarded" | "Create" "HintDb" ident OPT "discriminated" | "Remove" "Hints" LIST1 qualid OPT ( ":" LIST1 ident ) -| "Hint" hint OPT ( ":" LIST1 ident ) | "Comments" LIST0 [ one_term | string | natural ] | "Declare" "Instance" ident_decl LIST0 binder ":" term OPT hint_info | "Declare" "Scope" scope_name @@ -1030,7 +1017,7 @@ command: [ | "Print" "Rings" (* ring plugin *) | "Add" "Field" ident ":" one_term OPT ( "(" LIST1 field_mod SEP "," ")" ) (* ring plugin *) | "Print" "Fields" (* ring plugin *) -| "Hint" "Cut" "[" hints_path "]" OPT ( ":" LIST1 ident ) +| "Hint" "Cut" "[" hints_regexp "]" OPT ( ":" LIST1 ident ) | "Prenex" "Implicits" LIST1 qualid (* SSR plugin *) | "Print" "Hint" "View" OPT ssrviewpos (* SSR plugin *) | "Hint" "View" OPT ssrviewpos LIST1 ( one_term OPT ( "|" natural ) ) (* SSR plugin *) @@ -1039,7 +1026,7 @@ command: [ | "Typeclasses" "Opaque" LIST1 qualid | "Typeclasses" "eauto" ":=" OPT "debug" OPT ( "(" [ "bfs" | "dfs" ] ")" ) OPT natural | "Proof" "with" ltac_expr OPT [ "using" section_var_expr ] -| "Proof" "using" section_var_expr "with" ltac_expr +| "Proof" "using" section_var_expr OPT [ "with" ltac_expr ] | "Tactic" "Notation" OPT ( "(" "at" "level" natural ")" ) LIST1 ltac_production_item ":=" ltac_expr | "Print" "Rewrite" "HintDb" ident | "Print" "Ltac" qualid @@ -1142,6 +1129,15 @@ command: [ | "Ltac2" "Notation" [ string | lident ] ":=" ltac2_expr (* Ltac2 plugin *) | "Ltac2" "Eval" ltac2_expr (* Ltac2 plugin *) | "Print" "Ltac2" qualid (* Ltac2 plugin *) +| "Hint" "Resolve" LIST1 [ qualid | one_term ] OPT hint_info OPT ( ":" LIST1 ident ) +| "Hint" "Resolve" [ "->" | "<-" ] LIST1 qualid OPT natural OPT ( ":" LIST1 ident ) +| "Hint" "Immediate" LIST1 [ qualid | one_term ] OPT ( ":" LIST1 ident ) +| "Hint" [ "Constants" | "Variables" ] [ "Transparent" | "Opaque" ] OPT ( ":" LIST1 ident ) +| "Hint" [ "Transparent" | "Opaque" ] LIST1 qualid OPT ( ":" LIST1 ident ) +| "Hint" "Mode" qualid LIST1 [ "+" | "!" | "-" ] OPT ( ":" LIST1 ident ) +| "Hint" "Unfold" LIST1 qualid OPT ( ":" LIST1 ident ) +| "Hint" "Constructors" LIST1 qualid OPT ( ":" LIST1 ident ) +| "Hint" "Extern" natural OPT one_pattern "=>" ltac_expr OPT ( ":" LIST1 ident ) | "Time" sentence | "Redirect" string sentence | "Timeout" natural sentence @@ -1205,23 +1201,6 @@ univ_name_list: [ | "@{" LIST0 name "}" ] -hint: [ -| "Resolve" LIST1 [ qualid | one_term ] OPT hint_info -| "Resolve" "->" LIST1 qualid OPT natural -| "Resolve" "<-" LIST1 qualid OPT natural -| "Immediate" LIST1 [ qualid | one_term ] -| "Variables" "Transparent" -| "Variables" "Opaque" -| "Constants" "Transparent" -| "Constants" "Opaque" -| "Transparent" LIST1 qualid -| "Opaque" LIST1 qualid -| "Mode" qualid LIST1 [ "+" | "!" | "-" ] -| "Unfold" LIST1 qualid -| "Constructors" LIST1 qualid -| "Extern" natural OPT one_pattern "=>" ltac_expr -] - tacdef_body: [ | qualid LIST0 name [ ":=" | "::=" ] ltac_expr ] @@ -1275,28 +1254,37 @@ constr_with_bindings_arg: [ | OPT ">" one_term OPT ( "with" bindings ) (* SSR plugin *) ] -clause_dft_concl: [ -| "in" in_clause -| OPT ( "at" occs_nums ) +occurrences: [ +| "at" occs_nums +| "in" goal_occurrences ] -in_clause: [ -| "*" OPT ( "at" occs_nums ) -| "*" "|-" OPT concl_occ -| LIST0 hypident_occ SEP "," OPT ( "|-" OPT concl_occ ) +occs_nums: [ +| OPT "-" LIST1 nat_or_var ] -hypident_occ: [ +nat_or_var: [ +| [ natural | ident ] +] + +goal_occurrences: [ +| LIST1 hyp_occs SEP "," OPT ( "|-" OPT concl_occs ) +| "*" "|-" OPT concl_occs +| "|-" OPT concl_occs +| OPT concl_occs +] + +hyp_occs: [ | hypident OPT ( "at" occs_nums ) ] hypident: [ | ident -| "(" "type" "of" ident ")" (* SSR plugin *) -| "(" "value" "of" ident ")" (* SSR plugin *) +| "(" "type" "of" ident ")" +| "(" "value" "of" ident ")" ] -concl_occ: [ +concl_occs: [ | "*" OPT ( "at" occs_nums ) ] @@ -1545,15 +1533,15 @@ number_string_via: [ | "via" qualid "mapping" "[" LIST1 [ qualid "=>" qualid | "[" qualid "]" "=>" qualid ] SEP "," "]" ] -hints_path: [ -| "(" hints_path ")" -| hints_path "*" -| "emp" -| "eps" -| hints_path "|" hints_path +hints_regexp: [ | LIST1 qualid | "_" -| hints_path hints_path +| hints_regexp "|" hints_regexp +| hints_regexp hints_regexp +| hints_regexp "*" +| "emp" +| "eps" +| "(" hints_regexp ")" ] class: [ @@ -1630,7 +1618,7 @@ simple_tactic: [ | "constructor" OPT nat_or_var OPT ( "with" bindings ) | "econstructor" OPT ( nat_or_var OPT ( "with" bindings ) ) | "specialize" one_term OPT ( "with" bindings ) OPT ( "as" simple_intropattern ) -| "symmetry" OPT ( "in" in_clause ) +| "symmetry" OPT ( "in" goal_occurrences ) | "split" OPT ( "with" bindings ) | "esplit" OPT ( "with" bindings ) | "exists" OPT ( LIST1 bindings SEP "," ) @@ -1648,8 +1636,8 @@ simple_tactic: [ | "clear" "-" LIST1 ident | "clearbody" LIST1 ident | "generalize" "dependent" one_term -| "replace" one_term "with" one_term OPT clause_dft_concl OPT ( "by" ltac_expr3 ) -| "replace" OPT [ "->" | "<-" ] one_term OPT clause_dft_concl +| "replace" one_term "with" one_term OPT occurrences OPT ( "by" ltac_expr3 ) +| "replace" OPT [ "->" | "<-" ] one_term OPT occurrences | "setoid_replace" one_term "with" one_term OPT ( "using" "relation" one_term ) OPT ( "in" ident ) OPT ( "at" LIST1 int_or_var ) OPT ( "by" ltac_expr3 ) | OPT ( [ natural | "[" ident "]" ] ":" ) "{" | bullet @@ -1701,9 +1689,9 @@ simple_tactic: [ | "decompose" "record" one_term | "absurd" one_term | "contradiction" OPT ( one_term OPT ( "with" bindings ) ) -| "autorewrite" OPT "*" "with" LIST1 ident OPT clause_dft_concl OPT ( "using" ltac_expr ) -| "rewrite" "*" OPT [ "->" | "<-" ] one_term OPT ( "in" ident ) OPT ( "at" occurrences OPT ( "by" ltac_expr3 ) ) -| "rewrite" "*" OPT [ "->" | "<-" ] one_term "at" occurrences "in" ident OPT ( "by" ltac_expr3 ) +| "autorewrite" OPT "*" "with" LIST1 ident OPT occurrences OPT ( "using" ltac_expr ) +| "rewrite" "*" OPT [ "->" | "<-" ] one_term OPT ( "in" ident ) OPT ( "at" rewrite_occs OPT ( "by" ltac_expr3 ) ) +| "rewrite" "*" OPT [ "->" | "<-" ] one_term "at" rewrite_occs "in" ident OPT ( "by" ltac_expr3 ) | "refine" one_term | "simple" "refine" one_term | "notypeclasses" "refine" one_term @@ -1764,13 +1752,13 @@ simple_tactic: [ | "auto" OPT nat_or_var OPT auto_using OPT hintbases | "info_auto" OPT nat_or_var OPT auto_using OPT hintbases | "debug" "auto" OPT nat_or_var OPT auto_using OPT hintbases -| "eauto" OPT nat_or_var OPT nat_or_var OPT auto_using OPT hintbases +| "eauto" OPT nat_or_var OPT auto_using OPT hintbases | "new" "auto" OPT nat_or_var OPT auto_using OPT hintbases -| "debug" "eauto" OPT nat_or_var OPT nat_or_var OPT auto_using OPT hintbases -| "info_eauto" OPT nat_or_var OPT nat_or_var OPT auto_using OPT hintbases +| "debug" "eauto" OPT nat_or_var OPT auto_using OPT hintbases +| "info_eauto" OPT nat_or_var OPT auto_using OPT hintbases | "dfs" "eauto" OPT nat_or_var OPT auto_using OPT hintbases | "bfs" "eauto" OPT nat_or_var OPT auto_using OPT hintbases -| "autounfold" OPT hintbases OPT clause_dft_concl +| "autounfold" OPT hintbases OPT occurrences | "autounfold_one" OPT hintbases OPT ( "in" ident ) | "unify" one_term one_term OPT ( "with" ident ) | "convert_concl_no_check" one_term @@ -1784,8 +1772,8 @@ simple_tactic: [ | "rewrite_strat" rewstrategy OPT ( "in" ident ) | "rewrite_db" ident OPT ( "in" ident ) | "substitute" OPT [ "->" | "<-" ] one_term OPT ( "with" bindings ) -| "setoid_rewrite" OPT [ "->" | "<-" ] one_term OPT ( "with" bindings ) OPT ( "at" occurrences ) OPT ( "in" ident ) -| "setoid_rewrite" OPT [ "->" | "<-" ] one_term OPT ( "with" bindings ) "in" ident "at" occurrences +| "setoid_rewrite" OPT [ "->" | "<-" ] one_term OPT ( "with" bindings ) OPT ( "at" rewrite_occs ) OPT ( "in" ident ) +| "setoid_rewrite" OPT [ "->" | "<-" ] one_term OPT ( "with" bindings ) "in" ident "at" rewrite_occs | "setoid_symmetry" OPT ( "in" ident ) | "setoid_reflexivity" | "setoid_transitivity" one_term @@ -1808,10 +1796,10 @@ simple_tactic: [ | "pose" one_term OPT as_name | "epose" bindings_with_parameters | "epose" one_term OPT as_name -| "set" bindings_with_parameters OPT clause_dft_concl -| "set" one_term OPT as_name OPT clause_dft_concl -| "eset" bindings_with_parameters OPT clause_dft_concl -| "eset" one_term OPT as_name OPT clause_dft_concl +| "set" bindings_with_parameters OPT occurrences +| "set" one_term OPT as_name OPT occurrences +| "eset" bindings_with_parameters OPT occurrences +| "eset" one_term OPT as_name OPT occurrences | "remember" one_term OPT as_name OPT eqn_ipat OPT clause_dft_all | "eremember" one_term OPT as_name OPT eqn_ipat OPT clause_dft_all | "assert" "(" ident ":=" term ")" @@ -1829,32 +1817,32 @@ simple_tactic: [ | "enough" one_term OPT as_ipat OPT ( "by" ltac_expr3 ) | "eenough" one_term OPT as_ipat OPT ( "by" ltac_expr3 ) | "generalize" one_term OPT ( LIST1 one_term ) -| "generalize" one_term OPT ( "at" occs_nums ) OPT as_name LIST0 [ "," pattern_occ OPT as_name ] +| "generalize" one_term OPT ( "at" occs_nums ) OPT as_name LIST0 [ "," pattern_occs OPT as_name ] | "induction" induction_clause_list | "einduction" induction_clause_list | "destruct" induction_clause_list | "edestruct" induction_clause_list -| "rewrite" LIST1 oriented_rewriter SEP "," OPT clause_dft_concl OPT ( "by" ltac_expr3 ) -| "erewrite" LIST1 oriented_rewriter SEP "," OPT clause_dft_concl OPT ( "by" ltac_expr3 ) +| "rewrite" LIST1 oriented_rewriter SEP "," OPT occurrences OPT ( "by" ltac_expr3 ) +| "erewrite" LIST1 oriented_rewriter SEP "," OPT occurrences OPT ( "by" ltac_expr3 ) | "dependent" [ "simple" "inversion" | "inversion" | "inversion_clear" ] [ ident | natural ] OPT as_or_and_ipat OPT [ "with" one_term ] | "simple" "inversion" [ ident | natural ] OPT as_or_and_ipat OPT ( "in" LIST1 ident ) | "inversion" [ ident | natural ] OPT as_or_and_ipat OPT ( "in" LIST1 ident ) | "inversion_clear" [ ident | natural ] OPT as_or_and_ipat OPT ( "in" LIST1 ident ) | "inversion" [ ident | natural ] "using" one_term OPT ( "in" LIST1 ident ) -| "red" OPT clause_dft_concl -| "hnf" OPT clause_dft_concl -| "simpl" OPT delta_flag OPT ref_or_pattern_occ OPT clause_dft_concl -| "cbv" OPT strategy_flag OPT clause_dft_concl -| "cbn" OPT strategy_flag OPT clause_dft_concl -| "lazy" OPT strategy_flag OPT clause_dft_concl -| "compute" OPT delta_flag OPT clause_dft_concl -| "vm_compute" OPT ref_or_pattern_occ OPT clause_dft_concl -| "native_compute" OPT ref_or_pattern_occ OPT clause_dft_concl -| "unfold" LIST1 unfold_occ SEP "," OPT clause_dft_concl -| "fold" LIST1 one_term OPT clause_dft_concl -| "pattern" LIST1 pattern_occ SEP "," OPT clause_dft_concl -| "change" conversion OPT clause_dft_concl -| "change_no_check" conversion OPT clause_dft_concl +| "red" OPT occurrences +| "hnf" OPT occurrences +| "simpl" OPT delta_flag OPT [ reference_occs | pattern_occs ] OPT occurrences +| "cbv" OPT strategy_flag OPT occurrences +| "cbn" OPT strategy_flag OPT occurrences +| "lazy" OPT strategy_flag OPT occurrences +| "compute" OPT delta_flag OPT occurrences +| "vm_compute" OPT [ reference_occs | pattern_occs ] OPT occurrences +| "native_compute" OPT [ reference_occs | pattern_occs ] OPT occurrences +| "unfold" LIST1 reference_occs SEP "," OPT occurrences +| "fold" LIST1 one_term OPT occurrences +| "pattern" LIST1 pattern_occs SEP "," OPT occurrences +| "change" conversion OPT occurrences +| "change_no_check" conversion OPT occurrences | "btauto" | "rtauto" | "congruence" OPT natural OPT ( "with" LIST1 one_term ) @@ -1946,6 +1934,7 @@ simple_tactic: [ | "field_simplify" OPT ( "[" LIST1 one_term "]" ) LIST1 one_term OPT ( "in" ident ) | "field_simplify_eq" OPT ( "[" LIST1 one_term "]" ) OPT ( "in" ident ) | "intuition" OPT ltac_expr +| "now" ltac_expr | "nsatz" OPT ( "with" "radicalmax" ":=" one_term "strategy" ":=" one_term "parameters" ":=" one_term "variables" ":=" one_term ) | "psatz" one_term OPT nat_or_var | "ring" OPT ( "[" LIST1 one_term "]" ) @@ -1998,19 +1987,24 @@ induction_clause_list: [ | LIST1 induction_clause SEP "," OPT ( "using" one_term OPT ( "with" bindings ) ) OPT opt_clause ] -induction_clause: [ -| destruction_arg OPT as_or_and_ipat OPT eqn_ipat OPT opt_clause -] - opt_clause: [ -| "in" in_clause +| "in" goal_occurrences | "at" occs_nums ] +induction_clause: [ +| destruction_arg OPT as_or_and_ipat OPT eqn_ipat OPT opt_clause +] + auto_using: [ | "using" LIST1 one_term SEP "," ] +hintbases: [ +| "with" "*" +| "with" LIST1 ident +] + or_and_intropattern: [ | "[" intropattern_or_list_or "]" | "(" LIST0 simple_intropattern SEP "," ")" @@ -2055,6 +2049,10 @@ bindings: [ | LIST1 one_term ] +int_or_var: [ +| [ integer | ident ] +] + comparison: [ | "=" | "<" @@ -2063,11 +2061,6 @@ comparison: [ | ">=" ] -hintbases: [ -| "with" "*" -| "with" LIST1 ident -] - bindings_with_parameters: [ | "(" ident LIST0 simple_binder ":=" term ")" ] @@ -2436,11 +2429,11 @@ tac2mode: [ ] clause_dft_all: [ -| "in" in_clause +| "in" goal_occurrences ] in_hyp_as: [ -| "in" ident OPT as_ipat +| "in" LIST1 [ ident OPT as_ipat ] SEP "," ] simple_binder: [ @@ -2470,7 +2463,7 @@ func_scheme_def: [ | ident ":=" "Induction" "for" qualid "Sort" sort_family (* funind plugin *) ] -occurrences: [ +rewrite_occs: [ | LIST1 integer | ident ] diff --git a/theories/Classes/CRelationClasses.v b/theories/Classes/CRelationClasses.v index 236d35b68e18..c489d82d0b63 100644 --- a/theories/Classes/CRelationClasses.v +++ b/theories/Classes/CRelationClasses.v @@ -236,8 +236,6 @@ Hint Resolve irreflexivity : ord. Unset Implicit Arguments. -(** A HintDb for crelations. *) - Ltac solve_crelation := match goal with | [ |- ?R ?x ?x ] => reflexivity diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index 54ee06343a04..353496dfbae2 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -235,8 +235,6 @@ Hint Resolve irreflexivity : ord. Unset Implicit Arguments. -(** A HintDb for relations. *) - Ltac solve_relation := match goal with | [ |- ?R ?x ?x ] => reflexivity