diff options
| author | Théo Zimmermann | 2020-11-05 11:44:02 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2020-11-05 11:44:02 +0100 |
| commit | 643f13e31c34c5bf736a521fb44a4328953af0c5 (patch) | |
| tree | 156f1973bf0feee55020b189fe181cee843745dd | |
| parent | fdb8ef82a127629313539a78190a89d901090e2f (diff) | |
Remove everything after term rewriting and simplification.
| -rw-r--r-- | doc/sphinx/proofs/writing-proofs/rewriting.rst | 1456 |
1 files changed, 0 insertions, 1456 deletions
diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst index fe9a31e220..79b86af958 100644 --- a/doc/sphinx/proofs/writing-proofs/rewriting.rst +++ b/doc/sphinx/proofs/writing-proofs/rewriting.rst @@ -3519,1459 +3519,3 @@ Conversion tactics applied to hypotheses .. exn:: No such hypothesis: @ident. :undocumented: - - -.. _automation: - -Automation ----------- - -.. tacn:: auto - :name: auto - - This tactic 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. - - By default, :tacn:`auto` only uses the hypotheses of the current goal and - the hints of the database named ``core``. - - .. warning:: - - :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. - - .. tacv:: auto @natural - - Forces the search depth to be :token:`natural`. The maximal search depth - is 5 by default. - - .. tacv:: auto with {+ @ident} - - Uses the hint databases :n:`{+ @ident}` in addition to the database ``core``. - - .. note:: - - Use the fake database `nocore` if you want to *not* use the `core` - database. - - .. tacv:: auto with * - - 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. - - .. seealso:: - :ref:`The Hints Databases for auto and eauto <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 - - 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 - - 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: - -.. 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. - -.. flag:: Info Auto - Debug Auto - Info Trivial - Debug Trivial - - These flags enable printing of informative or debug information for - the :tacn:`auto` and :tacn:`trivial` tactics. - -.. tacn:: eauto - :name: eauto - - This tactic 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` - in the case of :tacn:`auto`). As a consequence, :tacn:`eauto` - can solve such a goal: - - .. example:: - - .. coqtop:: all - - Hint Resolve ex_intro : core. - Goal forall P:nat -> Prop, P 0 -> exists n, P n. - eauto. - - Note that ``ex_intro`` should be declared as a hint. - - - .. tacv:: {? info_}eauto {? @natural} {? using {+ @qualid}} {? with {+ @ident}} - - The various options for :tacn:`eauto` are the same as for :tacn:`auto`. - - :tacn:`eauto` also obeys the following flags: - - .. flag:: Info Eauto - Debug Eauto - :undocumented: - - .. seealso:: :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>` - - -.. tacn:: autounfold with {+ @ident} - :name: autounfold - - This tactic unfolds constants that were declared through a :cmd:`Hint Unfold` - in the given databases. - -.. tacv:: autounfold with {+ @ident} in @goal_occurrences - - Performs the unfolding in the given clause (:token:`goal_occurrences`). - -.. tacv:: autounfold with * - - Uses the unfold hints declared in all the hint databases. - -.. tacn:: autorewrite with {+ @ident} - :name: autorewrite - - This tactic carries out rewritings according to the rewriting rule - bases :n:`{+ @ident}`. - - Each rewriting rule from the base :n:`@ident` is applied 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 - the processing of the rewriting rules. - - The rewriting rule bases are built with the :cmd:`Hint Rewrite` - command. - -.. warning:: - - 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 <hintrewrite>` for feeding the database of lemmas used by - :tacn:`autorewrite` and :tacn:`autorewrite` for examples showing the use of this tactic. - -.. 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 - :tacn:`trivial`, :tacn:`reflexivity`, :tacn:`symmetry`, :tacn:`contradiction` - and :tacn:`inversion` of hypothesis. - If this fails, it tries introducing variables and splitting and-hypotheses, - using the closing tactics afterwards, and splitting the goal using - :tacn:`split` and recursing. - - 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 - - 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 - - Use this command - to display the hints associated to the head symbol :n:`@ident` - (see :ref:`Print Hint <printhint>`). 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. - -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. - -.. cmd:: Create HintDb @ident {? discriminated} - - This command creates a new 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 <thehintsdatabasesforautoandeauto>`), - 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 - hints, putting more work on the unification that is run after - retrieval (it keeps a list of the lemmas in case the DT is not used). - The new implementation enabled by the discriminated option makes use - of DTs in all cases and takes transparency information into account. - However, the order in which hints are retrieved from the DT may differ - from the order in which they were inserted, making this implementation - observationally different from the legacy one. - -.. cmd:: Hint @hint_definition : {+ @ident} - - The general command to add a hint to some databases :n:`{+ @ident}`. - - 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. - - + :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. - - + :attr:`export` are visible from other modules when they import the current - module. Requiring it is not enough. This attribute is only effective for - the :cmd:`Hint Resolve`, :cmd:`Hint Immediate`, :cmd:`Hint Unfold` and - :cmd:`Hint Extern` variants of the command. - - + :attr:`global` hints are made available by merely requiring the current - module. - - The various possible :production:`hint_definition`\s are given below. - - .. cmdv:: Hint @hint_definition - - No database name is given: the hint is registered in the ``core`` database. - - .. deprecated:: 8.10 - - .. cmdv:: Hint Resolve @qualid {? | {? @natural} {? @pattern}} : @ident - :name: Hint Resolve - - 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 - 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 - 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 - - Adds each :n:`Hint Resolve @qualid`. - - .. cmdv:: Hint Resolve -> @qualid : @ident - - 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 - - Adds the right-to-left implication of an equivalence as a hint. - - .. cmdv:: Hint Immediate @qualid : @ident - :name: Hint Immediate - - 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 - 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 - 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: - - .. 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 - 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. - - .. 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`. - 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 - :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 - 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 - - 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. - - .. cmdv:: Hint Extern @natural {? @pattern} => @tactic : @ident - :name: Hint Extern - - 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. - - .. example:: - - .. coqtop:: in - - Hint Extern 4 (~(_ = _)) => discriminate : core. - - Now, when the head of the goal is a disequality, ``auto`` will try - discriminate if it does not manage to solve the goal with hints with a - cost less than 4. - - One can even use some sub-patterns of the pattern in - the tactic script. A sub-pattern is a question mark followed by an - identifier, like ``?X1`` or ``?X2``. Here is an example: - - .. example:: - - .. coqtop:: reset all - - Require Import List. - 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. - - .. cmdv:: Hint Cut @regexp : @ident - :name: Hint Cut - - .. 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: - - .. prodn:: - regexp ::= @ident (hint or instance identifier) - | _ (any hint) - | @regexp | @regexp (disjunction) - | @regexp @regexp (sequence) - | @regexp * (Kleene star) - | emp (empty) - | eps (epsilon) - | ( @regexp ) - - 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 - 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 ``+``, - ``!`` 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 - 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. - - .. note:: - - + One can use a :cmd:`Hint Extern` with no pattern to do - pattern matching on hypotheses using ``match goal with`` - inside the tactic. - - + 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. - - -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 -to belong to this database in each of the various modules currently -loaded. Especially, requiring new modules may extend the database. -At |Coq| startup, only the core database is nonempty and can be used. - -:core: This special database is automatically used by ``auto``, except when - pseudo-database ``nocore`` is given to ``auto``. The core database - contains only basic lemmas about negation, conjunction, and so on. - Most of the hints in this database come from the Init and Logic directories. - -:arith: This database contains all lemmas about Peano’s arithmetic proved in the - directories Init and Arith. - -:zarith: contains lemmas about binary signed integers from the - directories theories/ZArith. The database also contains - high-cost hints that call :tacn:`lia` on equations and - inequalities in ``nat`` or ``Z``. - -:bool: contains lemmas about booleans, mostly from directory theories/Bool. - -:datatypes: is for lemmas about lists, streams and so on that are mainly proved - in the Lists subdirectory. - -:sets: contains lemmas about sets and relations from the directories Sets and - Relations. - -:typeclass_instances: contains all the typeclass instances declared in the - environment, including those used for ``setoid_rewrite``, - from the Classes directory. - -:fset: internal database for the implementation of the ``FSets`` library. - -:ordered_type: lemmas about ordered types (as defined in the legacy ``OrderedType`` module), - mainly used in the ``FSets`` and ``FMaps`` libraries. - -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 -section (and not defined with option ``Local``) become available when the -module ``A`` is required (using e.g. ``Require A.``). - -As of today, hints only have a binary behavior regarding locality, as -described above: either they disappear at the end of a section scope, -or they remain global forever. This causes a scalability issue, -because hints coming from an unrelated part of the code may badly -influence another development. It can be mitigated to some extent -thanks to the :cmd:`Remove Hints` command, -but this is a mere workaround and has some limitations (for instance, external -hints cannot be removed). - -A proper way to fix this issue is to bind the hints to their module scope, as -for most of the other objects |Coq| uses. Hints should only be made available when -the module they are defined in is imported, not just required. It is very -difficult to change the historical behavior, as it would break a lot of scripts. -We propose a smooth transitional path by providing the :opt:`Loose Hint Behavior` -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`: - - - "Lax": this is the default, and corresponds to the historical behavior, - that is, hints defined outside of a section have a global scope. - - - "Warn": outputs a warning when a non-imported hint is used. Note that this - is an over-approximation, because a hint may be triggered by a run that - will eventually fail and backtrack, resulting in the hint not being - actually useful for the proof. - - - "Strict": changes the behavior of an unloaded hint to a immediate fail - tactic, allowing to emulate an import-scoped hint mechanism. - -.. _tactics-implicit-automation: - -Setting implicit automation tactics -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -.. cmd:: Proof with @tactic - - 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``. - - .. 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` - -.. _decisionprocedures: - -Decision procedures -------------------- - -.. tacn:: tauto - :name: tauto - - This tactic implements a decision procedure for intuitionistic propositional - calculus based on the contraction-free sequent calculi LJT* of Roy Dyckhoff - :cite:`Dyc92`. Note that :tacn:`tauto` succeeds on any instance of an - intuitionistic tautological proposition. :tacn:`tauto` unfolds negations and - logical equivalence but does not unfold any other definition. - -.. example:: - - The following goal can be proved by :tacn:`tauto` whereas :tacn:`auto` would - fail: - - .. coqtop:: reset all - - Goal forall (x:nat) (P:nat -> Prop), x = 0 \/ P x -> x <> 0 -> P x. - intros. - tauto. - -Moreover, if it has nothing else to do, :tacn:`tauto` performs introductions. -Therefore, the use of :tacn:`intros` in the previous proof is unnecessary. -:tacn:`tauto` can for instance for: - -.. example:: - - .. coqtop:: reset all - - Goal forall (A:Prop) (P:nat -> Prop), A \/ (forall x:nat, ~ A -> P x) -> forall x:nat, ~ A -> P x. - tauto. - -.. note:: - In contrast, :tacn:`tauto` cannot solve the following goal - :g:`Goal forall (A:Prop) (P:nat -> Prop), A \/ (forall x:nat, ~ A -> P x) ->` - :g:`forall x:nat, ~ ~ (A \/ P x).` - because :g:`(forall x:nat, ~ A -> P x)` cannot be treated as atomic and - an instantiation of `x` is necessary. - -.. tacv:: dtauto - :name: dtauto - - While :tacn:`tauto` recognizes inductively defined connectives isomorphic to - the standard connectives ``and``, ``prod``, ``or``, ``sum``, ``False``, - ``Empty_set``, ``unit``, ``True``, :tacn:`dtauto` also recognizes all inductive - types with one constructor and no indices, i.e. record-style connectives. - -.. tacn:: intuition @tactic - :name: intuition - - The tactic :tacn:`intuition` takes advantage of the search-tree built by the - decision procedure involved in the tactic :tacn:`tauto`. It uses this - information to generate a set of subgoals equivalent to the original one (but - simpler than it) and applies the tactic :n:`@tactic` to them :cite:`Mun94`. If - this tactic fails on some goals then :tacn:`intuition` fails. In fact, - :tacn:`tauto` is simply :g:`intuition fail`. - - .. example:: - - For instance, the tactic :g:`intuition auto` applied to the goal:: - - (forall (x:nat), P x) /\ B -> (forall (y:nat), P y) /\ P O \/ B /\ P O - - internally replaces it by the equivalent one:: - - (forall (x:nat), P x), B |- P O - - and then uses :tacn:`auto` which completes the proof. - -Originally due to César Muñoz, these tactics (:tacn:`tauto` and -:tacn:`intuition`) have been completely re-engineered by David Delahaye using -mainly the tactic language (see :ref:`ltac`). The code is -now much shorter and a significant increase in performance has been noticed. -The general behavior with respect to dependent types, unfolding and -introductions has slightly changed to get clearer semantics. This may lead to -some incompatibilities. - -.. tacv:: intuition - - Is equivalent to :g:`intuition auto with *`. - -.. tacv:: dintuition - :name: dintuition - - While :tacn:`intuition` recognizes inductively defined connectives - isomorphic to the standard connectives ``and``, ``prod``, ``or``, ``sum``, ``False``, - ``Empty_set``, ``unit``, ``True``, :tacn:`dintuition` also recognizes all inductive - types with one constructor and no indices, i.e. record-style connectives. - -.. flag:: Intuition Negation Unfolding - - Controls whether :tacn:`intuition` unfolds inner negations which do not need - to be unfolded. This flag is on by default. - -.. tacn:: rtauto - :name: rtauto - - The :tacn:`rtauto` tactic solves propositional tautologies similarly to what - :tacn:`tauto` does. The main difference is that the proof term is built using a - reflection scheme applied to a sequent calculus proof of the goal. The search - procedure is also implemented using a different technique. - - Users should be aware that this difference may result in faster proof-search - but slower proof-checking, and :tacn:`rtauto` might not solve goals that - :tacn:`tauto` would be able to solve (e.g. goals involving universal - quantifiers). - - Note that this tactic is only available after a ``Require Import Rtauto``. - -.. tacn:: firstorder - :name: firstorder - - The tactic :tacn:`firstorder` is an experimental extension of :tacn:`tauto` to - first- order reasoning, written by Pierre Corbineau. It is not restricted to - usual logical connectives but instead may reason about any first-order class - inductive definition. - -.. opt:: Firstorder Solver @tactic - :name: Firstorder Solver - - The default tactic used by :tacn:`firstorder` when no rule applies is - :g:`auto with core`, it can be reset locally or globally using this option. - - .. cmd:: Print Firstorder Solver - - Prints the default tactic used by :tacn:`firstorder` when no rule applies. - -.. tacv:: firstorder @tactic - - Tries to solve the goal with :n:`@tactic` when no logical rule may apply. - -.. tacv:: firstorder using {+ @qualid} - - .. deprecated:: 8.3 - - Use the syntax below instead (with commas). - -.. tacv:: firstorder using {+, @qualid} - - Adds lemmas :n:`{+, @qualid}` to the proof-search environment. If :n:`@qualid` - refers to an inductive type, it is the collection of its constructors which are - added to the proof-search environment. - -.. tacv:: firstorder with {+ @ident} - - Adds lemmas from :tacn:`auto` hint bases :n:`{+ @ident}` to the proof-search - environment. - -.. tacv:: firstorder @tactic using {+, @qualid} with {+ @ident} - - This combines the effects of the different variants of :tacn:`firstorder`. - -.. opt:: Firstorder Depth @natural - :name: Firstorder Depth - - This option controls the proof-search depth bound. - -.. tacn:: congruence - :name: congruence - - The tactic :tacn:`congruence`, by Pierre Corbineau, implements the standard - Nelson and Oppen congruence closure algorithm, which is a decision procedure - for ground equalities with uninterpreted symbols. It also includes - constructor theory (see :tacn:`injection` and :tacn:`discriminate`). If the goal - is a non-quantified equality, congruence tries to prove it with non-quantified - equalities in the context. Otherwise it tries to infer a discriminable equality - from those in the context. Alternatively, congruence tries to prove that a - hypothesis is equal to the goal or to the negation of another hypothesis. - - :tacn:`congruence` is also able to take advantage of hypotheses stating - quantified equalities, but you have to provide a bound for the number of extra - equalities generated that way. Please note that one of the sides of the - equality must contain all the quantified variables in order for congruence to - match against it. - -.. example:: - - .. coqtop:: reset all - - Theorem T (A:Type) (f:A -> A) (g: A -> A -> A) a b: a=(f a) -> (g b (f a))=(f (f a)) -> (g a b)=(f (g b a)) -> (g a b)=a. - intros. - congruence. - Qed. - - Theorem inj (A:Type) (f:A -> A * A) (a c d: A) : f = pair a -> Some (f c) = Some (f d) -> c=d. - intros. - congruence. - Qed. - -.. tacv:: congruence @natural - - Tries to add at most :token:`natural` instances of hypotheses stating quantified equalities - to the problem in order to solve it. A bigger value of :token:`natural` does not make - success slower, only failure. You might consider adding some lemmas as - hypotheses using assert in order for :tacn:`congruence` to use them. - -.. tacv:: congruence with {+ @term} - :name: congruence with - - Adds :n:`{+ @term}` to the pool of terms used by :tacn:`congruence`. This helps - in case you have partially applied constructors in your goal. - -.. exn:: I don’t know how to handle dependent equality. - - The decision procedure managed to find a proof of the goal or of a - discriminable equality but this proof could not be built in |Coq| because of - dependently-typed functions. - -.. exn:: Goal is solvable by congruence but some arguments are missing. Try congruence with {+ @term}, replacing metavariables by arbitrary terms. - - The decision procedure could solve the goal with the provision that additional - arguments are supplied for some partially applied constructors. Any term of an - appropriate type will allow the tactic to successfully solve the goal. Those - additional arguments can be given to congruence by filling in the holes in the - terms given in the error message, using the :tacn:`congruence with` variant described above. - -.. flag:: Congruence Verbose - - This flag makes :tacn:`congruence` print debug information. - - -Checking properties of terms ----------------------------- - -Each of the following tactics acts as the identity if the check -succeeds, and results in an error otherwise. - -.. tacn:: constr_eq @term @term - :name: constr_eq - - This tactic checks whether its arguments are equal modulo alpha - conversion, casts and universe constraints. It may unify universes. - -.. exn:: Not equal. - :undocumented: - -.. exn:: Not equal (due to universes). - :undocumented: - -.. tacn:: constr_eq_strict @term @term - :name: constr_eq_strict - - This tactic checks whether its arguments are equal modulo alpha - conversion, casts and universe constraints. It does not add new - constraints. - -.. exn:: Not equal. - :undocumented: - -.. exn:: Not equal (due to universes). - :undocumented: - -.. tacn:: unify @term @term - :name: unify - - This tactic checks whether its arguments are unifiable, potentially - instantiating existential variables. - -.. exn:: Unable to unify @term with @term. - :undocumented: - -.. tacv:: unify @term @term with @ident - - Unification takes the transparency information defined in the hint database - :n:`@ident` into account (see :ref:`the hints databases for auto and eauto <thehintsdatabasesforautoandeauto>`). - -.. tacn:: is_evar @term - :name: is_evar - - This tactic checks whether its argument is a current existential - variable. Existential variables are uninstantiated variables generated - by :tacn:`eapply` and some other tactics. - -.. exn:: Not an evar. - :undocumented: - -.. tacn:: has_evar @term - :name: has_evar - - This tactic checks whether its argument has an existential variable as - a subterm. Unlike context patterns combined with ``is_evar``, this tactic - scans all subterms, including those under binders. - -.. exn:: No evars. - :undocumented: - -.. tacn:: is_var @term - :name: is_var - - This tactic checks whether its argument is a variable or hypothesis in - the current goal context or in the opened sections. - -.. exn:: Not a variable or hypothesis. - :undocumented: - - -.. _equality: - -Equality --------- - - -.. tacn:: f_equal - :name: f_equal - - This tactic applies to a goal of the form :g:`f a`:sub:`1` :g:`... a`:sub:`n` - :g:`= f′a′`:sub:`1` :g:`... a′`:sub:`n`. Using :tacn:`f_equal` on such a goal - leads to subgoals :g:`f=f′` and :g:`a`:sub:`1` = :g:`a′`:sub:`1` and so on up - to :g:`a`:sub:`n` :g:`= a′`:sub:`n`. Amongst these subgoals, the simple ones - (e.g. provable by :tacn:`reflexivity` or :tacn:`congruence`) are automatically - solved by :tacn:`f_equal`. - - -.. tacn:: reflexivity - :name: reflexivity - - This tactic applies to a goal that has the form :g:`t=u`. It checks that `t` - and `u` are convertible and then solves the goal. It is equivalent to - ``apply refl_equal``. - - .. exn:: The conclusion is not a substitutive equation. - :undocumented: - - .. exn:: Unable to unify ... with ... - :undocumented: - - -.. tacn:: symmetry - :name: symmetry - - This tactic applies to a goal that has the form :g:`t=u` and changes it into - :g:`u=t`. - - -.. tacv:: symmetry in @ident - - If the statement of the hypothesis ident has the form :g:`t=u`, the tactic - changes it to :g:`u=t`. - - -.. tacn:: transitivity @term - :name: transitivity - - This tactic applies to a goal that has the form :g:`t=u` and transforms it - into the two subgoals :n:`t=@term` and :n:`@term=u`. - - .. tacv:: etransitivity - - This tactic behaves like :tacn:`transitivity`, using a fresh evar instead of - a concrete :token:`term`. - - -Equality and inductive sets ---------------------------- - -We describe in this section some special purpose tactics dealing with -equality and inductive sets or types. These tactics use the -equality :g:`eq:forall (A:Type), A->A->Prop`, simply written with the infix -symbol :g:`=`. - -.. tacn:: decide equality - :name: decide equality - - This tactic solves a goal of the form :g:`forall x y : R, {x = y} + {~ x = y}`, - where :g:`R` is an inductive type such that its constructors do not take - proofs or functions as arguments, nor objects in dependent types. It - solves goals of the form :g:`{x = y} + {~ x = y}` as well. - -.. tacn:: compare @term @term - :name: compare - - This tactic compares two given objects :n:`@term` and :n:`@term` of an - inductive datatype. If :g:`G` is the current goal, it leaves the sub- - goals :n:`@term =@term -> G` and :n:`~ @term = @term -> G`. The type of - :n:`@term` and :n:`@term` must satisfy the same restrictions as in the - tactic ``decide equality``. - -.. tacn:: simplify_eq @term - :name: simplify_eq - - Let :n:`@term` be the proof of a statement of conclusion :n:`@term = @term`. - If :n:`@term` and :n:`@term` are structurally different (in the sense - described for the tactic :tacn:`discriminate`), then the tactic - ``simplify_eq`` behaves as :n:`discriminate @term`, otherwise it behaves as - :n:`injection @term`. - -.. note:: - If some quantified hypothesis of the goal is named :n:`@ident`, - then :n:`simplify_eq @ident` first introduces the hypothesis in the local - context using :n:`intros until @ident`. - -.. tacv:: simplify_eq @natural - - This does the same thing as :n:`intros until @natural` then - :n:`simplify_eq @ident` where :n:`@ident` is the identifier for the last - introduced hypothesis. - -.. tacv:: simplify_eq @term with @bindings - - This does the same as :n:`simplify_eq @term` but using the given bindings to - instantiate parameters or hypotheses of :n:`@term`. - -.. tacv:: esimplify_eq @natural - esimplify_eq @term {? with @bindings} - :name: esimplify_eq; _ - - This works the same as :tacn:`simplify_eq` but if the type of :n:`@term`, or the - type of the hypothesis referred to by :n:`@natural`, has uninstantiated - parameters, these parameters are left as existential variables. - -.. tacv:: simplify_eq - - If the current goal has form :g:`t1 <> t2`, it behaves as - :n:`intro @ident; simplify_eq @ident`. - -.. tacn:: dependent rewrite -> @ident - :name: dependent rewrite -> - - This tactic applies to any goal. If :n:`@ident` has type - :g:`(existT B a b)=(existT B a' b')` in the local context (i.e. each - :n:`@term` of the equality has a sigma type :g:`{ a:A & (B a)}`) this tactic - rewrites :g:`a` into :g:`a'` and :g:`b` into :g:`b'` in the current goal. - This tactic works even if :g:`B` is also a sigma type. This kind of - equalities between dependent pairs may be derived by the - :tacn:`injection` and :tacn:`inversion` tactics. - -.. tacv:: dependent rewrite <- @ident - :name: dependent rewrite <- - - Analogous to :tacn:`dependent rewrite ->` but uses the equality from right to - left. - -Classical tactics ------------------ - -In order to ease the proving process, when the ``Classical`` module is -loaded, a few more tactics are available. Make sure to load the module -using the ``Require Import`` command. - -.. tacn:: classical_left - classical_right - :name: classical_left; classical_right - - These tactics are the analog of :tacn:`left` and :tacn:`right` - but using classical logic. They can only be used for - disjunctions. Use :tacn:`classical_left` to prove the left part of the - disjunction with the assumption that the negation of right part holds. - Use :tacn:`classical_right` to prove the right part of the disjunction with - the assumption that the negation of left part holds. - -.. _tactics-automating: - -Automating ------------- - - -.. tacn:: btauto - :name: btauto - - The tactic :tacn:`btauto` implements a reflexive solver for boolean - tautologies. It solves goals of the form :g:`t = u` where `t` and `u` are - constructed over the following grammar: - - .. prodn:: - btauto_term ::= @ident - | true - | false - | orb @btauto_term @btauto_term - | andb @btauto_term @btauto_term - | xorb @btauto_term @btauto_term - | negb @btauto_term - | if @btauto_term then @btauto_term else @btauto_term - - Whenever the formula supplied is not a tautology, it also provides a - counter-example. - - Internally, it uses a system very similar to the one of the ring - tactic. - - Note that this tactic is only available after a ``Require Import Btauto``. - - .. exn:: Cannot recognize a boolean equality. - - The goal is not of the form :g:`t = u`. Especially note that :tacn:`btauto` - doesn't introduce variables into the context on its own. - -.. tacv:: field - field_simplify {* @term} - field_simplify_eq - - The field tactic is built on the same ideas as ring: this is a - reflexive tactic that solves or simplifies equations in a field - structure. The main idea is to reduce a field expression (which is an - extension of ring expressions with the inverse and division - operations) to a fraction made of two polynomial expressions. - - Tactic :n:`field` is used to solve subgoals, whereas :n:`field_simplify {+ @term}` - replaces the provided terms by their reduced fraction. - :n:`field_simplify_eq` applies when the conclusion is an equation: it - simplifies both hand sides and multiplies so as to cancel - denominators. So it produces an equation without division nor inverse. - - All of these 3 tactics may generate a subgoal in order to prove that - denominators are different from zero. - - See :ref:`Theringandfieldtacticfamilies` for more information on the tactic and how to - declare new field structures. All declared field structures can be - printed with the Print Fields command. - -.. example:: - - .. coqtop:: reset all - - Require Import Reals. - Goal forall x y:R, - (x * y > 0)%R -> - (x * (1 / x + x / (x + y)))%R = - ((- 1 / y) * y * (- x * (x / (x + y)) - 1))%R. - - intros; field. - -.. seealso:: - - File plugins/ring/RealField.v for an example of instantiation, - theory theories/Reals for many examples of use of field. - -Non-logical tactics ------------------------- - - -.. tacn:: cycle @integer - :name: cycle - - Reorders the selected goals so that the first :n:`@integer` goals appear after the - other selected goals. - If :n:`@integer` is negative, it puts the last :n:`@integer` goals at the - beginning of the list. - The tactic is only useful with a goal selector, most commonly `all:`. - Note that other selectors reorder goals; `1,3: cycle 1` is not equivalent - to `all: cycle 1`. See :tacn:`… : … (goal selector)`. - -.. example:: - - .. coqtop:: none reset - - Parameter P : nat -> Prop. - - .. coqtop:: all abort - - Goal P 1 /\ P 2 /\ P 3 /\ P 4 /\ P 5. - repeat split. - all: cycle 2. - all: cycle -3. - -.. tacn:: swap @integer @integer - :name: swap - - Exchanges the position of the specified goals. - Negative values for :n:`@integer` indicate counting goals - backward from the end of the list of selected goals. Goals are indexed from 1. - The tactic is only useful with a goal selector, most commonly `all:`. - Note that other selectors reorder goals; `1,3: swap 1 3` is not equivalent - to `all: swap 1 3`. See :tacn:`… : … (goal selector)`. - -.. example:: - - .. coqtop:: all abort - - Goal P 1 /\ P 2 /\ P 3 /\ P 4 /\ P 5. - repeat split. - all: swap 1 3. - all: swap 1 -1. - -.. tacn:: revgoals - :name: revgoals - - Reverses the order of the selected goals. The tactic is only useful with a goal - selector, most commonly `all :`. Note that other selectors reorder goals; - `1,3: revgoals` is not equivalent to `all: revgoals`. See :tacn:`… : … (goal selector)`. - - .. example:: - - .. coqtop:: all abort - - Goal P 1 /\ P 2 /\ P 3 /\ P 4 /\ P 5. - repeat split. - all: revgoals. - -.. tacn:: shelve - :name: shelve - - This tactic moves all goals under focus to a shelf. While on the - shelf, goals will not be focused on. They can be solved by - unification, or they can be called back into focus with the command - :cmd:`Unshelve`. - - .. tacv:: shelve_unifiable - :name: shelve_unifiable - - Shelves only the goals under focus that are mentioned in other goals. - Goals that appear in the type of other goals can be solved by unification. - - .. example:: - - .. coqtop:: all abort - - Goal exists n, n=0. - refine (ex_intro _ _ _). - all: shelve_unifiable. - reflexivity. - -.. cmd:: Unshelve - - This command moves all the goals on the shelf (see :tacn:`shelve`) - from the shelf into focus, by appending them to the end of the current - list of focused goals. - -.. tacn:: unshelve @tactic - :name: unshelve - - Performs :n:`@tactic`, then unshelves existential variables added to the - shelf by the execution of :n:`@tactic`, prepending them to the current goal. - -.. tacn:: give_up - :name: give_up - - This tactic removes the focused goals from the proof. They are not - solved, and cannot be solved later in the proof. As the goals are not - solved, the proof cannot be closed. - - The ``give_up`` tactic can be used while editing a proof, to choose to - write the proof script in a non-sequential order. - -Delaying solving unification constraints ----------------------------------------- - -.. tacn:: solve_constraints - :name: solve_constraints - :undocumented: - -.. flag:: Solve Unification Constraints - - By default, after each tactic application, postponed typechecking unification - problems are resolved using heuristics. Unsetting this flag disables this - behavior, allowing tactics to leave unification constraints unsolved. Use the - :tacn:`solve_constraints` tactic at any point to solve the constraints. - -Proof maintenance ------------------ - -*Experimental.* Many tactics, such as :tacn:`intros`, can automatically generate names, such -as "H0" or "H1" for a new hypothesis introduced from a goal. Subsequent proof steps -may explicitly refer to these names. However, future versions of |Coq| may not assign -names exactly the same way, which could cause the proof to fail because the -new names don't match the explicit references in the proof. - -The following "Mangle Names" settings let users find all the -places where proofs rely on automatically generated names, which can -then be named explicitly to avoid any incompatibility. These -settings cause |Coq| to generate different names, producing errors for -references to automatically generated names. - -.. flag:: Mangle Names - - When set, generated names use the prefix specified in the following - option instead of the default prefix. - -.. opt:: Mangle Names Prefix @string - :name: Mangle Names Prefix - - Specifies the prefix to use when generating names. - -Performance-oriented tactic variants ------------------------------------- - -.. tacn:: change_no_check @term - :name: change_no_check - - For advanced usage. Similar to :tacn:`change` :n:`@term`, but as an optimization, - it skips checking that :n:`@term` is convertible to the goal. - - Recall that the |Coq| kernel typechecks proofs again when they are concluded to - ensure safety. Hence, using :tacn:`change` checks convertibility twice - overall, while :tacn:`change_no_check` can produce ill-typed terms, - but checks convertibility only once. - Hence, :tacn:`change_no_check` can be useful to speed up certain proof - scripts, especially if one knows by construction that the argument is - indeed convertible to the goal. - - In the following example, :tacn:`change_no_check` replaces :g:`False` by - :g:`True`, but :cmd:`Qed` then rejects the proof, ensuring consistency. - - .. example:: - - .. coqtop:: all abort - - Goal False. - change_no_check True. - exact I. - Fail Qed. - - :tacn:`change_no_check` supports all of :tacn:`change`'s variants. - - .. tacv:: change_no_check @term with @term’ - :undocumented: - - .. tacv:: change_no_check @term at {+ @natural} with @term’ - :undocumented: - - .. tacv:: change_no_check @term {? {? at {+ @natural}} with @term} in @ident - - .. example:: - - .. coqtop:: all abort - - Goal True -> False. - intro H. - change_no_check False in H. - exact H. - Fail Qed. - - .. tacv:: convert_concl_no_check @term - :name: convert_concl_no_check - - .. deprecated:: 8.11 - - Deprecated old name for :tacn:`change_no_check`. Does not support any of its - variants. - -.. tacn:: exact_no_check @term - :name: exact_no_check - - For advanced usage. Similar to :tacn:`exact` :n:`@term`, but as an optimization, - it skips checking that :n:`@term` has the goal's type, relying on the kernel - check instead. See :tacn:`change_no_check` for more explanation. - - .. example:: - - .. coqtop:: all abort - - Goal False. - exact_no_check I. - Fail Qed. - - .. tacv:: vm_cast_no_check @term - :name: vm_cast_no_check - - For advanced usage. Similar to :tacn:`exact_no_check` :n:`@term`, but additionally - instructs the kernel to use :tacn:`vm_compute` to compare the - goal's type with the :n:`@term`'s type. - - .. example:: - - .. coqtop:: all abort - - Goal False. - vm_cast_no_check I. - Fail Qed. - - .. tacv:: native_cast_no_check @term - :name: native_cast_no_check - - for advanced usage. similar to :tacn:`exact_no_check` :n:`@term`, but additionally - instructs the kernel to use :tacn:`native_compute` to compare the goal's - type with the :n:`@term`'s type. - - .. example:: - - .. coqtop:: all abort - - Goal False. - native_cast_no_check I. - Fail Qed. - -.. [1] Actually, only the second subgoal will be generated since the - other one can be automatically checked. -.. [2] This corresponds to the cut rule of sequent calculus. -.. [3] Reminder: opaque constants will not be expanded by δ reductions. |