From 4c21d78932066765a75c7d25aab8bdf72ca6ab10 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Fri, 3 Apr 2020 15:42:47 +0200 Subject: Extract section on funind from Gallina extensions. --- doc/sphinx/language/gallina-extensions.rst | 2431 +--------------------------- 1 file changed, 2 insertions(+), 2429 deletions(-) (limited to 'doc') diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 18b05e47d3..6d5791bc19 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -1,594 +1,5 @@ -.. _extensionsofgallina: - -Extensions of |Gallina| -======================= - -|Gallina| is the kernel language of |Coq|. We describe here extensions of -|Gallina|’s syntax. - -.. _record-types: - -Record types ----------------- - -The :cmd:`Record` construction is a macro allowing the definition of -records as is done in many programming languages. Its syntax is -described in the grammar below. In fact, the :cmd:`Record` macro is more general -than the usual record types, since it allows also for “manifest” -expressions. In this sense, the :cmd:`Record` construction allows defining -“signatures”. - -.. _record_grammar: - -.. cmd:: {| Record | Structure } @record_definition {* with @record_definition } - :name: Record; Structure - - .. insertprodn record_definition field_body - - .. prodn:: - record_definition ::= {? > } @ident_decl {* @binder } {? : @type } {? @ident } %{ {*; @record_field } %} {? @decl_notations } - record_field ::= {* #[ {*, @attr } ] } @name {? @field_body } {? %| @num } {? @decl_notations } - field_body ::= {* @binder } @of_type - | {* @binder } @of_type := @term - | {* @binder } := @term - - Each :n:`@record_definition` defines a record named by :n:`@ident_decl`. - The constructor name is given by :n:`@ident`. - If the constructor name is not specified, then the default name :n:`Build_@ident` is used, - where :n:`@ident` is the record name. - - If :n:`@type` is - omitted, the default type is :math:`\Type`. The identifiers inside the brackets are the field names. - The type of each field :n:`@ident` is :n:`forall {* @binder }, @type`. - Notice that the type of an identifier can depend on a previously-given identifier. Thus the - order of the fields is important. :n:`@binder` parameters may be applied to the record as a whole - or to individual fields. - - Notations can be attached to fields using the :n:`@decl_notations` annotation. - - :cmd:`Record` and :cmd:`Structure` are synonyms. - - This command supports the :attr:`universes(polymorphic)`, - :attr:`universes(monomorphic)`, :attr:`universes(template)`, - :attr:`universes(notemplate)`, :attr:`universes(cumulative)`, - :attr:`universes(noncumulative)` and :attr:`private(matching)` - attributes. - -More generally, a record may have explicitly defined (a.k.a. manifest) -fields. For instance, we might have: -:n:`Record @ident {* @binder } : @sort := { @ident__1 : @type__1 ; @ident__2 := @term__2 ; @ident__3 : @type__3 }`. -in which case the correctness of :n:`@type__3` may rely on the instance :n:`@term__2` of :n:`@ident__2` and :n:`@term__2` may in turn depend on :n:`@ident__1`. - -.. example:: - - The set of rational numbers may be defined as: - - .. coqtop:: reset all - - Record Rat : Set := mkRat - { sign : bool - ; top : nat - ; bottom : nat - ; Rat_bottom_cond : 0 <> bottom - ; Rat_irred_cond : - forall x y z:nat, (x * y) = top /\ (x * z) = bottom -> x = 1 - }. - - Note here that the fields ``Rat_bottom_cond`` depends on the field ``bottom`` - and ``Rat_irred_cond`` depends on both ``top`` and ``bottom``. - -Let us now see the work done by the ``Record`` macro. First the macro -generates a variant type definition with just one constructor: -:n:`Variant @ident {* @binder } : @sort := @ident__0 {* @binder }`. - -To build an object of type :token:`ident`, one should provide the constructor -:n:`@ident__0` with the appropriate number of terms filling the fields of the record. - -.. example:: - - Let us define the rational :math:`1/2`: - - .. coqtop:: in - - Theorem one_two_irred : forall x y z:nat, x * y = 1 /\ x * z = 2 -> x = 1. - Admitted. - - Definition half := mkRat true 1 2 (O_S 1) one_two_irred. - Check half. - -Alternatively, the following syntax allows creating objects by using named fields, as -shown in this grammar. The fields do not have to be in any particular order, nor do they have -to be all present if the missing ones can be inferred or prompted for -(see :ref:`programs`). - -.. coqtop:: all - - Definition half' := - {| sign := true; - Rat_bottom_cond := O_S 1; - Rat_irred_cond := one_two_irred |}. - -The following settings let you control the display format for types: - -.. flag:: Printing Records - - If set, use the record syntax (shown above) as the default display format. - -You can override the display format for specified types by adding entries to these tables: - -.. table:: Printing Record @qualid - :name: Printing Record - - Specifies a set of qualids which are displayed as records. Use the - :cmd:`Add @table` and :cmd:`Remove @table` commands to update the set of qualids. - -.. table:: Printing Constructor @qualid - :name: Printing Constructor - - Specifies a set of qualids which are displayed as constructors. Use the - :cmd:`Add @table` and :cmd:`Remove @table` commands to update the set of qualids. - -This syntax can also be used for pattern matching. - -.. coqtop:: all - - Eval compute in ( - match half with - | {| sign := true; top := n |} => n - | _ => 0 - end). - -The macro generates also, when it is possible, the projection -functions for destructuring an object of type :token:`ident`. These -projection functions are given the names of the corresponding -fields. If a field is named `_` then no projection is built -for it. In our example: - -.. coqtop:: all - - Eval compute in top half. - Eval compute in bottom half. - Eval compute in Rat_bottom_cond half. - -An alternative syntax for projections based on a dot notation is -available: - -.. coqtop:: all - - Eval compute in half.(top). - -.. flag:: Printing Projections - - This flag activates the dot notation for printing. - - .. example:: - - .. coqtop:: all - - Set Printing Projections. - Check top half. - -.. FIXME: move this to the main grammar in the spec chapter - -.. _record_projections_grammar: - - .. insertprodn term_projection term_projection - - .. prodn:: - term_projection ::= @term0 .( @qualid {* @arg } ) - | @term0 .( @ @qualid {* @term1 } ) - - Syntax of Record projections - -The corresponding grammar rules are given in the preceding grammar. When :token:`qualid` -denotes a projection, the syntax :n:`@term0.(@qualid)` is equivalent to :n:`@qualid @term0`, -the syntax :n:`@term0.(@qualid {+ @arg })` to :n:`@qualid {+ @arg } @term0`. -and the syntax :n:`@term0.(@@qualid {+ @term0 })` to :n:`@@qualid {+ @term0 } @term0`. -In each case, :token:`term0` is the object projected and the -other arguments are the parameters of the inductive type. - - -.. note:: Records defined with the ``Record`` keyword are not allowed to be - recursive (references to the record's name in the type of its field - raises an error). To define recursive records, one can use the ``Inductive`` - and ``CoInductive`` keywords, resulting in an inductive or co-inductive record. - Definition of mutually inductive or co-inductive records are also allowed, as long - as all of the types in the block are records. - -.. note:: Induction schemes are automatically generated for inductive records. - Automatic generation of induction schemes for non-recursive records - defined with the ``Record`` keyword can be activated with the - :flag:`Nonrecursive Elimination Schemes` flag (see :ref:`proofschemes-induction-principles`). - -.. warn:: @ident cannot be defined. - - It can happen that the definition of a projection is impossible. - This message is followed by an explanation of this impossibility. - There may be three reasons: - - #. The name :token:`ident` already exists in the environment (see :cmd:`Axiom`). - #. The body of :token:`ident` uses an incorrect elimination for - :token:`ident` (see :cmd:`Fixpoint` and :ref:`Destructors`). - #. The type of the projections :token:`ident` depends on previous - projections which themselves could not be defined. - -.. exn:: Records declared with the keyword Record or Structure cannot be recursive. - - The record name :token:`ident` appears in the type of its fields, but uses - the keyword ``Record``. Use the keyword ``Inductive`` or ``CoInductive`` instead. - -.. exn:: Cannot handle mutually (co)inductive records. - - Records cannot be defined as part of mutually inductive (or - co-inductive) definitions, whether with records only or mixed with - standard definitions. - -During the definition of the one-constructor inductive definition, all -the errors of inductive definitions, as described in Section -:ref:`gallina-inductive-definitions`, may also occur. - -.. seealso:: Coercions and records in section :ref:`coercions-classes-as-records` of the chapter devoted to coercions. - -.. _primitive_projections: - -Primitive Projections -~~~~~~~~~~~~~~~~~~~~~ - -.. flag:: Primitive Projections - - Turns on the use of primitive - projections when defining subsequent records (even through the ``Inductive`` - and ``CoInductive`` commands). Primitive projections - extended the Calculus of Inductive Constructions with a new binary - term constructor `r.(p)` representing a primitive projection `p` applied - to a record object `r` (i.e., primitive projections are always applied). - Even if the record type has parameters, these do not appear - in the internal representation of - applications of the projection, considerably reducing the sizes of - terms when manipulating parameterized records and type checking time. - On the user level, primitive projections can be used as a replacement - for the usual defined ones, although there are a few notable differences. - -.. flag:: Printing Primitive Projection Parameters - - This compatibility flag reconstructs internally omitted parameters at - printing time (even though they are absent in the actual AST manipulated - by the kernel). - -Primitive Record Types -++++++++++++++++++++++ - -When the :flag:`Primitive Projections` flag is on, definitions of -record types change meaning. When a type is declared with primitive -projections, its :g:`match` construct is disabled (see :ref:`primitive_projections` though). -To eliminate the (co-)inductive type, one must use its defined primitive projections. - -.. The following paragraph is quite redundant with what is above - -For compatibility, the parameters still appear to the user when -printing terms even though they are absent in the actual AST -manipulated by the kernel. This can be changed by unsetting the -:flag:`Printing Primitive Projection Parameters` flag. - -There are currently two ways to introduce primitive records types: - -#. Through the ``Record`` command, in which case the type has to be - non-recursive. The defined type enjoys eta-conversion definitionally, - that is the generalized form of surjective pairing for records: - `r` ``= Build_``\ `R` ``(``\ `r`\ ``.(``\ |p_1|\ ``) …`` `r`\ ``.(``\ |p_n|\ ``))``. - Eta-conversion allows to define dependent elimination for these types as well. -#. Through the ``Inductive`` and ``CoInductive`` commands, when - the body of the definition is a record declaration of the form - ``Build_``\ `R` ``{`` |p_1| ``:`` |t_1|\ ``; … ;`` |p_n| ``:`` |t_n| ``}``. - In this case the types can be recursive and eta-conversion is disallowed. These kind of record types - differ from their traditional versions in the sense that dependent - elimination is not available for them and only non-dependent case analysis - can be defined. - -Reduction -+++++++++ - -The basic reduction rule of a primitive projection is -|p_i| ``(Build_``\ `R` |t_1| … |t_n|\ ``)`` :math:`{\rightarrow_{\iota}}` |t_i|. -However, to take the :math:`{\delta}` flag into -account, projections can be in two states: folded or unfolded. An -unfolded primitive projection application obeys the rule above, while -the folded version delta-reduces to the unfolded version. This allows to -precisely mimic the usual unfolding rules of constants. Projections -obey the usual ``simpl`` flags of the ``Arguments`` command in particular. -There is currently no way to input unfolded primitive projections at the -user-level, and there is no way to display unfolded projections differently -from folded ones. - - -Compatibility Projections and :g:`match` -++++++++++++++++++++++++++++++++++++++++ - -To ease compatibility with ordinary record types, each primitive -projection is also defined as a ordinary constant taking parameters and -an object of the record type as arguments, and whose body is an -application of the unfolded primitive projection of the same name. These -constants are used when elaborating partial applications of the -projection. One can distinguish them from applications of the primitive -projection if the :flag:`Printing Primitive Projection Parameters` flag -is off: For a primitive projection application, parameters are printed -as underscores while for the compatibility projections they are printed -as usual. - -Additionally, user-written :g:`match` constructs on primitive records -are desugared into substitution of the projections, they cannot be -printed back as :g:`match` constructs. - -Variants and extensions of :g:`match` -------------------------------------- - -.. _mult-match: - -Multiple and nested pattern matching -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -The basic version of :g:`match` allows pattern matching on simple -patterns. As an extension, multiple nested patterns or disjunction of -patterns are allowed, as in ML-like languages. - -The extension just acts as a macro that is expanded during parsing -into a sequence of match on simple patterns. Especially, a -construction defined using the extended match is generally printed -under its expanded form (see :flag:`Printing Matching`). - -.. seealso:: :ref:`extendedpatternmatching`. - -.. _if-then-else: - -Pattern-matching on boolean values: the if expression -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -For inductive types with exactly two constructors and for pattern matching -expressions that do not depend on the arguments of the constructors, it is possible -to use a ``if … then … else`` notation. For instance, the definition - -.. coqtop:: all - - Definition not (b:bool) := - match b with - | true => false - | false => true - end. - -can be alternatively written - -.. coqtop:: reset all - - Definition not (b:bool) := if b then false else true. - -More generally, for an inductive type with constructors :n:`@ident__1` -and :n:`@ident__2`, the following terms are equal: - -:n:`if @term__0 {? {? as @name } return @term } then @term__1 else @term__2` - -:n:`match @term__0 {? {? as @name } return @term } with | @ident__1 {* _ } => @term__1 | @ident__2 {* _ } => @term__2 end` - -.. example:: - - .. coqtop:: all - - Check (fun x (H:{x=0}+{x<>0}) => - match H with - | left _ => true - | right _ => false - end). - -Notice that the printing uses the :g:`if` syntax because :g:`sumbool` is -declared as such (see :ref:`controlling-match-pp`). - -.. _irrefutable-patterns: - -Irrefutable patterns: the destructuring let variants -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -Pattern-matching on terms inhabiting inductive type having only one -constructor can be alternatively written using :g:`let … in …` -constructions. There are two variants of them. - - -First destructuring let syntax -++++++++++++++++++++++++++++++ - -The expression :n:`let ( {*, @ident__i } ) := @term__0 in @term__1` -performs case analysis on :n:`@term__0` whose type must be an -inductive type with exactly one constructor. The number of variables -:n:`@ident__i` must correspond to the number of arguments of this -contrustor. Then, in :n:`@term__1`, these variables are bound to the -arguments of the constructor in :n:`@term__0`. For instance, the -definition - -.. coqtop:: reset all - - Definition fst (A B:Set) (H:A * B) := match H with - | pair x y => x - end. - -can be alternatively written - -.. coqtop:: reset all - - Definition fst (A B:Set) (p:A * B) := let (x, _) := p in x. - -Notice that reduction is different from regular :g:`let … in …` -construction since it happens only if :n:`@term__0` is in constructor form. -Otherwise, the reduction is blocked. - -The pretty-printing of a definition by matching on a irrefutable -pattern can either be done using :g:`match` or the :g:`let` construction -(see Section :ref:`controlling-match-pp`). - -If term inhabits an inductive type with one constructor `C`, we have an -equivalence between - -:: - - let (ident₁, …, identₙ) [dep_ret_type] := term in term' - -and - -:: - - match term [dep_ret_type] with - C ident₁ … identₙ => term' - end - - -Second destructuring let syntax -+++++++++++++++++++++++++++++++ - -Another destructuring let syntax is available for inductive types with -one constructor by giving an arbitrary pattern instead of just a tuple -for all the arguments. For example, the preceding example can be -written: - -.. coqtop:: reset all - - Definition fst (A B:Set) (p:A*B) := let 'pair x _ := p in x. - -This is useful to match deeper inside tuples and also to use notations -for the pattern, as the syntax :g:`let ’p := t in b` allows arbitrary -patterns to do the deconstruction. For example: - -.. coqtop:: all - - Definition deep_tuple (A:Set) (x:(A*A)*(A*A)) : A*A*A*A := - let '((a,b), (c, d)) := x in (a,b,c,d). - - Notation " x 'With' p " := (exist _ x p) (at level 20). - - Definition proj1_sig' (A:Set) (P:A->Prop) (t:{ x:A | P x }) : A := - let 'x With p := t in x. - -When printing definitions which are written using this construct it -takes precedence over let printing directives for the datatype under -consideration (see Section :ref:`controlling-match-pp`). - - -.. _controlling-match-pp: - -Controlling pretty-printing of match expressions -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -The following commands give some control over the pretty-printing -of :g:`match` expressions. - -Printing nested patterns -+++++++++++++++++++++++++ - -.. flag:: Printing Matching - - The Calculus of Inductive Constructions knows pattern matching only - over simple patterns. It is however convenient to re-factorize nested - pattern matching into a single pattern matching over a nested - pattern. - - When this flag is on (default), |Coq|’s printer tries to do such - limited re-factorization. - Turning it off tells |Coq| to print only simple pattern matching problems - in the same way as the |Coq| kernel handles them. - - -Factorization of clauses with same right-hand side -++++++++++++++++++++++++++++++++++++++++++++++++++ - -.. flag:: Printing Factorizable Match Patterns - - When several patterns share the same right-hand side, it is additionally - possible to share the clauses using disjunctive patterns. Assuming that the - printing matching mode is on, this flag (on by default) tells |Coq|'s - printer to try to do this kind of factorization. - -Use of a default clause -+++++++++++++++++++++++ - -.. flag:: Printing Allow Match Default Clause - - When several patterns share the same right-hand side which do not depend on the - arguments of the patterns, yet an extra factorization is possible: the - disjunction of patterns can be replaced with a `_` default clause. Assuming that - the printing matching mode and the factorization mode are on, this flag (on by - default) tells |Coq|'s printer to use a default clause when relevant. - -Printing of wildcard patterns -++++++++++++++++++++++++++++++ - -.. flag:: Printing Wildcard - - Some variables in a pattern may not occur in the right-hand side of - the pattern matching clause. When this flag is on (default), the - variables having no occurrences in the right-hand side of the - pattern matching clause are just printed using the wildcard symbol - “_”. - - -Printing of the elimination predicate -+++++++++++++++++++++++++++++++++++++ - -.. flag:: Printing Synth - - In most of the cases, the type of the result of a matched term is - mechanically synthesizable. Especially, if the result type does not - depend of the matched term. When this flag is on (default), - the result type is not printed when |Coq| knows that it can re- - synthesize it. - - -Printing matching on irrefutable patterns -++++++++++++++++++++++++++++++++++++++++++ - -If an inductive type has just one constructor, pattern matching can be -written using the first destructuring let syntax. - -.. table:: Printing Let @qualid - :name: Printing Let - - Specifies a set of qualids for which pattern matching is displayed using a let expression. - Note that this only applies to pattern matching instances entered with :g:`match`. - It doesn't affect pattern matching explicitly entered with a destructuring - :g:`let`. - Use the :cmd:`Add @table` and :cmd:`Remove @table` commands to update this set. - - -Printing matching on booleans -+++++++++++++++++++++++++++++ - -If an inductive type is isomorphic to the boolean type, pattern matching -can be written using ``if`` … ``then`` … ``else`` …. This table controls -which types are written this way: - -.. table:: Printing If @qualid - :name: Printing If - - Specifies a set of qualids for which pattern matching is displayed using - ``if`` … ``then`` … ``else`` …. Use the :cmd:`Add @table` and :cmd:`Remove @table` - commands to update this set. - -This example emphasizes what the printing settings offer. - -.. example:: - - .. coqtop:: all - - Definition snd (A B:Set) (H:A * B) := match H with - | pair x y => y - end. - - Test Printing Let for prod. - - Print snd. - - Remove Printing Let prod. - - Unset Printing Synth. - - Unset Printing Wildcard. - - Print snd. +Functional induction +==================== .. _advanced-recursive-functions: @@ -756,1841 +167,3 @@ terminating functions. :tacn:`functional inversion` will not be available for the function. .. seealso:: :ref:`functional-scheme` and :tacn:`function induction` - -.. _section-mechanism: - -Section mechanism ------------------ - -Sections create local contexts which can be shared across multiple definitions. - -.. example:: - - Sections are opened by the :cmd:`Section` command, and closed by :cmd:`End`. - - .. coqtop:: all - - Section s1. - - Inside a section, local parameters can be introduced using :cmd:`Variable`, - :cmd:`Hypothesis`, or :cmd:`Context` (there are also plural variants for - the first two). - - .. coqtop:: all - - Variables x y : nat. - - The command :cmd:`Let` introduces section-wide :ref:`let-in`. These definitions - won't persist when the section is closed, and all persistent definitions which - depend on `y'` will be prefixed with `let y' := y in`. - - .. coqtop:: in - - Let y' := y. - Definition x' := S x. - Definition x'' := x' + y'. - - .. coqtop:: all - - Print x'. - Print x''. - - End s1. - - Print x'. - Print x''. - - Notice the difference between the value of :g:`x'` and :g:`x''` inside section - :g:`s1` and outside. - -.. cmd:: Section @ident - - This command is used to open a section named :token:`ident`. - Section names do not need to be unique. - - -.. cmd:: End @ident - - This command closes the section or module named :token:`ident`. - See :ref:`Terminating an interactive module or module type definition` - for a description of its use with modules. - - After closing the - section, the local declarations (variables and local definitions, see :cmd:`Variable`) are - *discharged*, meaning that they stop being visible and that all global - objects defined in the section are generalized with respect to the - variables and local definitions they each depended on in the section. - - .. exn:: There is nothing to end. - :undocumented: - - .. exn:: Last block to end has name @ident. - :undocumented: - -.. note:: - Most commands, like :cmd:`Hint`, :cmd:`Notation`, option management, … which - appear inside a section are canceled when the section is closed. - -.. cmd:: Let @ident @def_body - Let Fixpoint @fix_definition {* with @fix_definition } - Let CoFixpoint @cofix_definition {* with @cofix_definition } - :name: Let; Let Fixpoint; Let CoFixpoint - - These commands behave like :cmd:`Definition`, :cmd:`Fixpoint` and :cmd:`CoFixpoint`, except that - the declared constant is local to the current section. - When the section is closed, all persistent - definitions and theorems within it that depend on the constant - will be wrapped with a :n:`@term_let` with the same declaration. - - As for :cmd:`Definition`, :cmd:`Fixpoint` and :cmd:`CoFixpoint`, - if :n:`@term` is omitted, :n:`@type` is required and Coq enters proof editing mode. - This can be used to define a term incrementally, in particular by relying on the :tacn:`refine` tactic. - In this case, the proof should be terminated with :cmd:`Defined` in order to define a constant - for which the computational behavior is relevant. See :ref:`proof-editing-mode`. - -.. cmd:: Context {+ @binder } - - Declare variables in the context of the current section, like :cmd:`Variable`, - but also allowing implicit variables, :ref:`implicit-generalization`, and - let-binders. - - .. coqdoc:: - - Context {A : Type} (a b : A). - Context `{EqDec A}. - Context (b' := b). - -.. seealso:: Section :ref:`binders`. Section :ref:`contexts` in chapter :ref:`typeclasses`. - -Module system -------------- - -The module system provides a way of packaging related elements -together, as well as a means of massive abstraction. - - -.. cmd:: Module {? {| Import | Export } } @ident {* @module_binder } {? @of_module_type } {? := {+<+ @module_expr_inl } } - - .. insertprodn module_binder module_expr_inl - - .. prodn:: - module_binder ::= ( {? {| Import | Export } } {+ @ident } : @module_type_inl ) - module_type_inl ::= ! @module_type - | @module_type {? @functor_app_annot } - functor_app_annot ::= [ inline at level @num ] - | [ no inline ] - module_type ::= @qualid - | ( @module_type ) - | @module_type @module_expr_atom - | @module_type with @with_declaration - with_declaration ::= Definition @qualid {? @univ_decl } := @term - | Module @qualid := @qualid - module_expr_atom ::= @qualid - | ( {+ @module_expr_atom } ) - of_module_type ::= : @module_type_inl - | {* <: @module_type_inl } - module_expr_inl ::= ! {+ @module_expr_atom } - | {+ @module_expr_atom } {? @functor_app_annot } - - Defines a module named :token:`ident`. See the examples :ref:`here`. - - The :n:`Import` and :n:`Export` flags specify whether the module should be automatically - imported or exported. - - Specifying :n:`{* @module_binder }` starts a functor with - parameters given by the :n:`@module_binder`\s. (A *functor* is a function - from modules to modules.) - - .. todo: would like to find a better term than "interactive", not very descriptive - - :n:`@of_module_type` specifies the module type. :n:`{+ <: @module_type_inl }` - starts a module that satisfies each :n:`@module_type_inl`. - - :n:`:= {+<+ @module_expr_inl }` specifies the body of a module or functor - definition. If it's not specified, then the module is defined *interactively*, - meaning that the module is defined as a series of commands terminated with :cmd:`End` - instead of in a single :cmd:`Module` command. - Interactively defining the :n:`@module_expr_inl`\s in a series of - :cmd:`Include` commands is equivalent to giving them all in a single - non-interactive :cmd:`Module` command. - - The ! prefix indicates that any assumption command (such as :cmd:`Axiom`) with an :n:`Inline` clause - in the type of the functor arguments will be ignored. - - .. todo: What is an Inline directive? sb command but still unclear. Maybe referring to the - "inline" in functor_app_annot? or assumption_token Inline assum_list? - -.. cmd:: Module Type @ident {* @module_binder } {* <: @module_type_inl } {? := {+<+ @module_type_inl } } - - Defines a module type named :n:`@ident`. See the example :ref:`here`. - - Specifying :n:`{* @module_binder }` starts a functor type with - parameters given by the :n:`@module_binder`\s. - - :n:`:= {+<+ @module_type_inl }` specifies the body of a module or functor type - definition. If it's not specified, then the module type is defined *interactively*, - meaning that the module type is defined as a series of commands terminated with :cmd:`End` - instead of in a single :cmd:`Module Type` command. - Interactively defining the :n:`@module_type_inl`\s in a series of - :cmd:`Include` commands is equivalent to giving them all in a single - non-interactive :cmd:`Module Type` command. - -.. _terminating_module: - -**Terminating an interactive module or module type definition** - -Interactive modules are terminated with the :cmd:`End` command, which -is also used to terminate :ref:`Sections`. -:n:`End @ident` closes the interactive module or module type :token:`ident`. -If the module type was given, the command verifies that the content of the module -matches the module type. If the module is not a -functor, its components (constants, inductive types, submodules etc.) -are now available through the dot notation. - -.. exn:: No such label @ident. - :undocumented: - -.. exn:: Signature components for label @ident do not match. - :undocumented: - -.. exn:: The field @ident is missing in @qualid. - :undocumented: - -.. |br| raw:: html - -
- -.. note:: - - #. 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 - modules and module types. Note that with module definitions like: - - :n:`Module @ident__1 : @module_type := @ident__2.` - - or - - :n:`Module @ident__1 : @module_type.` |br| - :n:`Include @ident__2.` |br| - :n:`End @ident__1.` - - hints and the like valid for :n:`@ident__1` are the ones defined in :n:`@module_type` - rather then those defined in :n:`@ident__2` (or the module body). - #. Within an interactive module type definition, the :cmd:`Parameter` command declares a - constant instead of definining a new axiom (which it does when not in a module type definition). - #. Assumptions such as :cmd:`Axiom` that include the :n:`Inline` clause will be automatically - expanded when the functor is applied, except when the function application is prefixed by ``!``. - -.. cmd:: Include @module_type_inl {* <+ @module_expr_inl } - - Includes the content of module(s) in the current - interactive module. Here :n:`@module_type_inl` can be a module expression or a module - type expression. If it is a high-order module or module type - expression then the system tries to instantiate :n:`@module_type_inl` with the current - interactive module. - - Including multiple modules is a single :cmd:`Include` is equivalent to including each module - in a separate :cmd:`Include` command. - -.. cmd:: Include Type {+<+ @module_type_inl } - - .. deprecated:: 8.3 - - Use :cmd:`Include` instead. - -.. cmd:: Declare Module {? {| Import | Export } } @ident {* @module_binder } : @module_type_inl - - Declares a module :token:`ident` of type :token:`module_type_inl`. - - If :n:`@module_binder`\s are specified, declares a functor with parameters given by the list of - :token:`module_binder`\s. - -.. cmd:: Import {+ @qualid } - - If :token:`qualid` denotes a valid basic module (i.e. its module type is a - signature), makes its components available by their short names. - - .. example:: - - .. coqtop:: reset in - - Module Mod. - Definition T:=nat. - Check T. - End Mod. - Check Mod.T. - - .. coqtop:: all - - Fail Check T. - Import Mod. - Check T. - - Some features defined in modules are activated only when a module is - imported. This is for instance the case of notations (see :ref:`Notations`). - - Declarations made with the :attr:`local` attribute are never imported by the :cmd:`Import` - command. Such declarations are only accessible through their fully - qualified name. - - .. example:: - - .. coqtop:: in - - Module A. - Module B. - Local Definition T := nat. - End B. - End A. - Import A. - - .. coqtop:: all fail - - Check B.T. - -.. cmd:: Export {+ @qualid } - :name: Export - - Similar to :cmd:`Import`, except that when the module containing this command - is imported, the :n:`{+ @qualid }` are imported as well. - - .. exn:: @qualid is not a module. - :undocumented: - - .. warn:: Trying to mask the absolute name @qualid! - :undocumented: - -.. cmd:: Print Module @qualid - - Prints the module type and (optionally) the body of the module :n:`@qualid`. - -.. cmd:: Print Module Type @qualid - - Prints the module type corresponding to :n:`@qualid`. - -.. flag:: Short Module Printing - - This flag (off by default) disables the printing of the types of fields, - leaving only their names, for the commands :cmd:`Print Module` and - :cmd:`Print Module Type`. - -.. _module_examples: - -Examples -~~~~~~~~ - -.. example:: Defining a simple module interactively - - .. coqtop:: in - - Module M. - Definition T := nat. - Definition x := 0. - - .. coqtop:: all - - Definition y : bool. - exact true. - - .. coqtop:: in - - Defined. - End M. - -Inside a module one can define constants, prove theorems and do anything -else that can be done in the toplevel. Components of a closed -module can be accessed using the dot notation: - -.. coqtop:: all - - Print M.x. - -.. _example_def_simple_module_type: - -.. example:: Defining a simple module type interactively - - .. coqtop:: in - - Module Type SIG. - Parameter T : Set. - Parameter x : T. - End SIG. - -.. _example_filter_module: - -.. example:: Creating a new module that omits some items from an existing module - - Since :n:`SIG`, the type of the new module :n:`N`, doesn't define :n:`y` or - give the body of :n:`x`, which are not included in :n:`N`. - - .. coqtop:: all - - Module N : SIG with Definition T := nat := M. - Print N.T. - Print N.x. - Fail Print N.y. - - .. reset to remove N (undo in last coqtop block doesn't seem to do that), invisibly redefine M, SIG - .. coqtop:: none reset - - Module M. - Definition T := nat. - Definition x := 0. - Definition y : bool. - exact true. - Defined. - End M. - - Module Type SIG. - Parameter T : Set. - Parameter x : T. - End SIG. - -The following definition of :g:`N` using the module type expression :g:`SIG` with -:g:`Definition T := nat` is equivalent to the following one: - -.. todo: what is other definition referred to above? - "Module N' : SIG with Definition T := nat. End N`." is not it. - -.. coqtop:: in - - Module Type SIG'. - Definition T : Set := nat. - Parameter x : T. - End SIG'. - - Module N : SIG' := M. - -If we just want to be sure that our implementation satisfies a -given module type without restricting the interface, we can use a -transparent constraint - -.. coqtop:: in - - Module P <: SIG := M. - -.. coqtop:: all - - Print P.y. - -.. example:: Creating a functor (a module with parameters) - - .. coqtop:: in - - Module Two (X Y: SIG). - Definition T := (X.T * Y.T)%type. - Definition x := (X.x, Y.x). - End Two. - - and apply it to our modules and do some computations: - - .. coqtop:: in - - - Module Q := Two M N. - - .. coqtop:: all - - Eval compute in (fst Q.x + snd Q.x). - -.. example:: A module type with two sub-modules, sharing some fields - - .. coqtop:: in - - Module Type SIG2. - Declare Module M1 : SIG. - Module M2 <: SIG. - Definition T := M1.T. - Parameter x : T. - End M2. - End SIG2. - - .. coqtop:: in - - Module Mod <: SIG2. - Module M1. - Definition T := nat. - Definition x := 1. - End M1. - Module M2 := M. - End Mod. - -Notice that ``M`` is a correct body for the component ``M2`` since its ``T`` -component is ``nat`` as specified for ``M1.T``. - -Libraries and qualified names ---------------------------------- - -.. _names-of-libraries: - -Names of libraries -~~~~~~~~~~~~~~~~~~ - -The theories developed in |Coq| are stored in *library files* which are -hierarchically classified into *libraries* and *sublibraries*. To -express this hierarchy, library names are represented by qualified -identifiers qualid, i.e. as list of identifiers separated by dots (see -:ref:`gallina-identifiers`). For instance, the library file ``Mult`` of the standard -|Coq| library ``Arith`` is named ``Coq.Arith.Mult``. The identifier that starts -the name of a library is called a *library root*. All library files of -the standard library of |Coq| have the reserved root |Coq| but library -filenames based on other roots can be obtained by using |Coq| commands -(coqc, coqtop, coqdep, …) options ``-Q`` or ``-R`` (see :ref:`command-line-options`). -Also, when an interactive |Coq| session starts, a library of root ``Top`` is -started, unless option ``-top`` or ``-notop`` is set (see :ref:`command-line-options`). - -.. _qualified-names: - -Qualified names -~~~~~~~~~~~~~~~ - -Library files are modules which possibly contain submodules which -eventually contain constructions (axioms, parameters, definitions, -lemmas, theorems, remarks or facts). The *absolute name*, or *full -name*, of a construction in some library file is a qualified -identifier starting with the logical name of the library file, -followed by the sequence of submodules names encapsulating the -construction and ended by the proper name of the construction. -Typically, the absolute name ``Coq.Init.Logic.eq`` denotes Leibniz’ -equality defined in the module Logic in the sublibrary ``Init`` of the -standard library of |Coq|. - -The proper name that ends the name of a construction is the short name -(or sometimes base name) of the construction (for instance, the short -name of ``Coq.Init.Logic.eq`` is ``eq``). Any partial suffix of the absolute -name is a *partially qualified name* (e.g. ``Logic.eq`` is a partially -qualified name for ``Coq.Init.Logic.eq``). Especially, the short name of a -construction is its shortest partially qualified name. - -|Coq| does not accept two constructions (definition, theorem, …) with -the same absolute name but different constructions can have the same -short name (or even same partially qualified names as soon as the full -names are different). - -Notice that the notion of absolute, partially qualified and short -names also applies to library filenames. - -**Visibility** - -|Coq| maintains a table called the name table which maps partially qualified -names of constructions to absolute names. This table is updated by the -commands :cmd:`Require`, :cmd:`Import` and :cmd:`Export` and -also each time a new declaration is added to the context. An absolute -name is called visible from a given short or partially qualified name -when this latter name is enough to denote it. This means that the -short or partially qualified name is mapped to the absolute name in -|Coq| name table. Definitions with the :attr:`local` attribute are only accessible with -their fully qualified name (see :ref:`gallina-definitions`). - -It may happen that a visible name is hidden by the short name or a -qualified name of another construction. In this case, the name that -has been hidden must be referred to using one more level of -qualification. To ensure that a construction always remains -accessible, absolute names can never be hidden. - -.. example:: - - .. coqtop:: all - - Check 0. - - Definition nat := bool. - - Check 0. - - Check Datatypes.nat. - - Locate nat. - -.. seealso:: Commands :cmd:`Locate` and :cmd:`Locate Library`. - -.. _libraries-and-filesystem: - -Libraries and filesystem -~~~~~~~~~~~~~~~~~~~~~~~~ - -.. note:: The questions described here have been subject to redesign in |Coq| 8.5. - Former versions of |Coq| use the same terminology to describe slightly different things. - -Compiled files (``.vo`` and ``.vio``) store sub-libraries. In order to refer -to them inside |Coq|, a translation from file-system names to |Coq| names -is needed. In this translation, names in the file system are called -*physical* paths while |Coq| names are contrastingly called *logical* -names. - -A logical prefix Lib can be associated with a physical path using -the command line option ``-Q`` `path` ``Lib``. All subfolders of path are -recursively associated to the logical path ``Lib`` extended with the -corresponding suffix coming from the physical path. For instance, the -folder ``path/fOO/Bar`` maps to ``Lib.fOO.Bar``. Subdirectories corresponding -to invalid |Coq| identifiers are skipped, and, by convention, -subdirectories named ``CVS`` or ``_darcs`` are skipped too. - -Thanks to this mechanism, ``.vo`` files are made available through the -logical name of the folder they are in, extended with their own -basename. For example, the name associated to the file -``path/fOO/Bar/File.vo`` is ``Lib.fOO.Bar.File``. The same caveat applies for -invalid identifiers. When compiling a source file, the ``.vo`` file stores -its logical name, so that an error is issued if it is loaded with the -wrong loadpath afterwards. - -Some folders have a special status and are automatically put in the -path. |Coq| commands associate automatically a logical path to files in -the repository trees rooted at the directory from where the command is -launched, ``coqlib/user-contrib/``, the directories listed in the -``$COQPATH``, ``${XDG_DATA_HOME}/coq/`` and ``${XDG_DATA_DIRS}/coq/`` -environment variables (see `XDG base directory specification -`_) -with the same physical-to-logical translation and with an empty logical prefix. - -The command line option ``-R`` is a variant of ``-Q`` which has the strictly -same behavior regarding loadpaths, but which also makes the -corresponding ``.vo`` files available through their short names in a way -similar to the :cmd:`Import` command. For instance, ``-R path Lib`` -associates to the file ``/path/fOO/Bar/File.vo`` the logical name -``Lib.fOO.Bar.File``, but allows this file to be accessed through the -short names ``fOO.Bar.File,Bar.File`` and ``File``. If several files with -identical base name are present in different subdirectories of a -recursive loadpath, which of these files is found first may be system- -dependent and explicit qualification is recommended. The ``From`` argument -of the ``Require`` command can be used to bypass the implicit shortening -by providing an absolute root to the required file (see :ref:`compiled-files`). - -There also exists another independent loadpath mechanism attached to -OCaml object files (``.cmo`` or ``.cmxs``) rather than |Coq| object -files as described above. The OCaml loadpath is managed using -the option ``-I`` `path` (in the OCaml world, there is neither a -notion of logical name prefix nor a way to access files in -subdirectories of path). See the command :cmd:`Declare ML Module` in -:ref:`compiled-files` to understand the need of the OCaml loadpath. - -See :ref:`command-line-options` for a more general view over the |Coq| command -line options. - -.. _ImplicitArguments: - -Implicit arguments ------------------- - -An implicit argument of a function is an argument which can be -inferred from contextual knowledge. There are different kinds of -implicit arguments that can be considered implicit in different ways. -There are also various commands to control the setting or the -inference of implicit arguments. - - -The different kinds of implicit arguments -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -Implicit arguments inferable from the knowledge of other arguments of a function -++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ - -The first kind of implicit arguments covers the arguments that are -inferable from the knowledge of the type of other arguments of the -function, or of the type of the surrounding context of the -application. Especially, such implicit arguments correspond to -parameters dependent in the type of the function. Typical implicit -arguments are the type arguments in polymorphic functions. There are -several kinds of such implicit arguments. - -**Strict Implicit Arguments** - -An implicit argument can be either strict or non strict. An implicit -argument is said to be *strict* if, whatever the other arguments of the -function are, it is still inferable from the type of some other -argument. Technically, an implicit argument is strict if it -corresponds to a parameter which is not applied to a variable which -itself is another parameter of the function (since this parameter may -erase its arguments), not in the body of a match, and not itself -applied or matched against patterns (since the original form of the -argument can be lost by reduction). - -For instance, the first argument of -:: - - cons: forall A:Set, A -> list A -> list A - -in module ``List.v`` is strict because :g:`list` is an inductive type and :g:`A` -will always be inferable from the type :g:`list A` of the third argument of -:g:`cons`. Also, the first argument of :g:`cons` is strict with respect to the second one, -since the first argument is exactly the type of the second argument. -On the contrary, the second argument of a term of type -:: - - forall P:nat->Prop, forall n:nat, P n -> ex nat P - -is implicit but not strict, since it can only be inferred from the -type :g:`P n` of the third argument and if :g:`P` is, e.g., :g:`fun _ => True`, it -reduces to an expression where ``n`` does not occur any longer. The first -argument :g:`P` is implicit but not strict either because it can only be -inferred from :g:`P n` and :g:`P` is not canonically inferable from an arbitrary -:g:`n` and the normal form of :g:`P n`. Consider, e.g., that :g:`n` is :math:`0` and the third -argument has type :g:`True`, then any :g:`P` of the form -:: - - fun n => match n with 0 => True | _ => anything end - -would be a solution of the inference problem. - -**Contextual Implicit Arguments** - -An implicit argument can be *contextual* or not. An implicit argument -is said *contextual* if it can be inferred only from the knowledge of -the type of the context of the current expression. For instance, the -only argument of:: - - nil : forall A:Set, list A` - -is contextual. Similarly, both arguments of a term of type:: - - forall P:nat->Prop, forall n:nat, P n \/ n = 0 - -are contextual (moreover, :g:`n` is strict and :g:`P` is not). - -**Reversible-Pattern Implicit Arguments** - -There is another class of implicit arguments that can be reinferred -unambiguously if all the types of the remaining arguments are known. -This is the class of implicit arguments occurring in the type of -another argument in position of reversible pattern, which means it is -at the head of an application but applied only to uninstantiated -distinct variables. Such an implicit argument is called *reversible- -pattern implicit argument*. A typical example is the argument :g:`P` of -nat_rec in -:: - - nat_rec : forall P : nat -> Set, P 0 -> - (forall n : nat, P n -> P (S n)) -> forall x : nat, P x - -(:g:`P` is reinferable by abstracting over :g:`n` in the type :g:`P n`). - -See :ref:`controlling-rev-pattern-implicit-args` for the automatic declaration of reversible-pattern -implicit arguments. - -Implicit arguments inferable by resolution -++++++++++++++++++++++++++++++++++++++++++ - -This corresponds to a class of non-dependent implicit arguments that -are solved based on the structure of their type only. - - -Maximal or non maximal insertion of implicit arguments -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -In case a function is partially applied, and the next argument to be -applied is an implicit argument, two disciplines are applicable. In -the first case, the function is considered to have no arguments -furtherly: one says that the implicit argument is not maximally -inserted. In the second case, the function is considered to be -implicitly applied to the implicit arguments it is waiting for: one -says that the implicit argument is maximally inserted. - -Each implicit argument can be declared to be inserted maximally or non -maximally. In Coq, maximally-inserted implicit arguments are written between curly braces -"{ }" and non-maximally-inserted implicit arguments are written in square brackets "[ ]". - -.. seealso:: :flag:`Maximal Implicit Insertion` - -Trailing Implicit Arguments -+++++++++++++++++++++++++++ - -An implicit argument is considered trailing when all following arguments are declared -implicit. Trailing implicit arguments cannot be declared non maximally inserted, -otherwise they would never be inserted. - -.. exn:: Argument @name is a trailing implicit, so it can't be declared non maximal. Please use %{ %} instead of [ ]. - - For instance: - - .. coqtop:: all fail - - Fail Definition double [n] := n + n. - - -Casual use of implicit arguments -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -In a given expression, if it is clear that some argument of a function -can be inferred from the type of the other arguments, the user can -force the given argument to be guessed by replacing it by “_”. If -possible, the correct argument will be automatically generated. - -.. exn:: Cannot infer a term for this placeholder. - :name: Cannot infer a term for this placeholder. (Casual use of implicit arguments) - - |Coq| was not able to deduce an instantiation of a “_”. - -.. _declare-implicit-args: - -Declaration of implicit arguments -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -In case one wants that some arguments of a given object (constant, -inductive types, constructors, assumptions, local or not) are always -inferred by |Coq|, one may declare once and for all which are the -expected implicit arguments of this object. There are two ways to do -this, *a priori* and *a posteriori*. - - -Implicit Argument Binders -+++++++++++++++++++++++++ - -.. insertprodn implicit_binders implicit_binders - -.. prodn:: - implicit_binders ::= %{ {+ @name } {? : @type } %} - | [ {+ @name } {? : @type } ] - -In the first setting, one wants to explicitly give the implicit -arguments of a declared object as part of its definition. To do this, -one has to surround the bindings of implicit arguments by curly -braces or square braces: - -.. coqtop:: all - - Definition id {A : Type} (x : A) : A := x. - -This automatically declares the argument A of id as a maximally -inserted implicit argument. One can then do as-if the argument was -absent in every situation but still be able to specify it if needed: - -.. coqtop:: all - - Definition compose {A B C} (g : B -> C) (f : A -> B) := fun x => g (f x). - - Goal forall A, compose id id = id (A:=A). - -For non maximally inserted implicit arguments, use square brackets: - -.. coqtop:: all - - Fixpoint map [A B : Type] (f : A -> B) (l : list A) : list B := - match l with - | nil => nil - | cons a t => cons (f a) (map f t) - end. - - Print Implicit map. - -The syntax is supported in all top-level definitions: -:cmd:`Definition`, :cmd:`Fixpoint`, :cmd:`Lemma` and so on. For (co-)inductive datatype -declarations, the semantics are the following: an inductive parameter -declared as an implicit argument need not be repeated in the inductive -definition and will become implicit for the inductive type and the constructors. -For example: - -.. coqtop:: all - - Inductive list {A : Type} : Type := - | nil : list - | cons : A -> list -> list. - - Print list. - -One can always specify the parameter if it is not uniform using the -usual implicit arguments disambiguation syntax. - -The syntax is also supported in internal binders. For instance, in the -following kinds of expressions, the type of each declaration present -in :token:`binders` can be bracketed to mark the declaration as -implicit: -:n:`fun (@ident:forall {* @binder }, @type) => @term`, -:n:`forall (@ident:forall {* @binder }, @type), @type`, -:n:`let @ident {* @binder } := @term in @term`, -:n:`fix @ident {* @binder } := @term in @term` and -:n:`cofix @ident {* @binder } := @term in @term`. -Here is an example: - -.. coqtop:: all - - Axiom Ax : - forall (f:forall {A} (a:A), A * A), - let g {A} (x y:A) := (x,y) in - f 0 = g 0 0. - -.. warn:: Ignoring implicit binder declaration in unexpected position - - This is triggered when setting an argument implicit in an - expression which does not correspond to the type of an assumption - or to the body of a definition. Here is an example: - - .. coqtop:: all warn - - Definition f := forall {y}, y = 0. - -.. warn:: Making shadowed name of implicit argument accessible by position - - This is triggered when two variables of same name are set implicit - in the same block of binders, in which case the first occurrence is - considered to be unnamed. Here is an example: - - .. coqtop:: all warn - - Check let g {x:nat} (H:x=x) {x} (H:x=x) := x in 0. - - -Declaring Implicit Arguments -++++++++++++++++++++++++++++ - - - -.. cmd:: Arguments @smart_qualid {* @argument_spec_block } {* , {* @more_implicits_block } } {? : {+, @arguments_modifier } } - :name: Arguments - - .. insertprodn smart_qualid arguments_modifier - - .. prodn:: - smart_qualid ::= @qualid - | @by_notation - by_notation ::= @string {? % @ident } - argument_spec_block ::= @argument_spec - | / - | & - | ( {+ @argument_spec } ) {? % @ident } - | [ {+ @argument_spec } ] {? % @ident } - | %{ {+ @argument_spec } %} {? % @ident } - argument_spec ::= {? ! } @name {? % @ident } - more_implicits_block ::= @name - | [ {+ @name } ] - | %{ {+ @name } %} - arguments_modifier ::= simpl nomatch - | simpl never - | default implicits - | clear bidirectionality hint - | clear implicits - | clear scopes - | clear scopes and implicits - | clear implicits and scopes - | rename - | assert - | extra scopes - - This command sets implicit arguments *a posteriori*, - where the list of :n:`@name`\s is a prefix of the list of - arguments of :n:`@smart_qualid`. Arguments in square - brackets are declared as implicit and arguments in curly brackets are declared as - maximally inserted. - - After the command is issued, implicit arguments can and must be - omitted in any expression that applies :token:`qualid`. - - This command supports the :attr:`local` and :attr:`global` attributes. - Default behavior is to limit the effect to the current section but also to - extend their effect outside the current module or library file. - Applying :attr:`local` limits the effect of the command to the current module if - it's not in a section. Applying :attr:`global` within a section extends the - effect outside the current sections and current module if the command occurs. - - A command containing :n:`@argument_spec_block & @argument_spec_block` - provides :ref:`bidirectionality_hints`. - - Use the :n:`@more_implicits_block` to specify multiple implicit arguments declarations - for names of constants, inductive types, constructors and lemmas that can only be - applied to a fixed number of arguments (excluding, for instance, - constants whose type is polymorphic). - The longest applicable list of implicit arguments will be used to select which - implicit arguments are inserted. - For printing, the omitted arguments are the ones of the longest list of implicit - arguments of the sequence. See the example :ref:`here`. - - The :n:`@arguments_modifier` values have various effects: - - * :n:`clear implicits` - clears implicit arguments - * :n:`default implicits` - automatically determine the implicit arguments of the object. - See :ref:`auto_decl_implicit_args`. - * :n:`rename` - rename implicit arguments for the object - * :n:`assert` - assert that the object has the expected number of arguments with the - expected names. See the example here: :ref:`renaming_implicit_arguments`. - -.. exn:: The / modifier may only occur once. - :undocumented: - -.. exn:: The & modifier may only occur once. - :undocumented: - -.. example:: - - .. coqtop:: reset all - - Inductive list (A : Type) : Type := - | nil : list A - | cons : A -> list A -> list A. - - Check (cons nat 3 (nil nat)). - - Arguments cons [A] _ _. - - Arguments nil {A}. - - Check (cons 3 nil). - - Fixpoint map (A B : Type) (f : A -> B) (l : list A) : list B := - match l with nil => nil | cons a t => cons (f a) (map A B f t) end. - - Fixpoint length (A : Type) (l : list A) : nat := - match l with nil => 0 | cons _ m => S (length A m) end. - - Arguments map [A B] f l. - - Arguments length {A} l. (* A has to be maximally inserted *) - - Check (fun l:list (list nat) => map length l). - -.. _example_more_implicits: - -.. example:: Multiple implicit arguments with :n:`@more_implicits_block` - - .. coqtop:: all - - Arguments map [A B] f l, [A] B f l, A B f l. - - Check (fun l => map length l = map (list nat) nat length l). - -.. note:: - Use the :cmd:`Print Implicit` command to see the implicit arguments - of an object (see :ref:`displaying-implicit-args`). - -.. _auto_decl_implicit_args: - -Automatic declaration of implicit arguments -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - - The :n:`default implicits @arguments_modifier` clause tells |Coq| to automatically determine the - implicit arguments of the object. - - Auto-detection is governed by flags specifying whether strict, - contextual, or reversible-pattern implicit arguments must be - considered or not (see :ref:`controlling-strict-implicit-args`, :ref:`controlling-contextual-implicit-args`, - :ref:`controlling-rev-pattern-implicit-args` and also :ref:`controlling-insertion-implicit-args`). - -.. example:: Default implicits - - .. coqtop:: reset all - - Inductive list (A:Set) : Set := - | nil : list A - | cons : A -> list A -> list A. - - Arguments cons : default implicits. - - Print Implicit cons. - - Arguments nil : default implicits. - - Print Implicit nil. - - Set Contextual Implicit. - - Arguments nil : default implicits. - - Print Implicit nil. - -The computation of implicit arguments takes account of the unfolding -of constants. For instance, the variable ``p`` below has type -``(Transitivity R)`` which is reducible to -``forall x,y:U, R x y -> forall z:U, R y z -> R x z``. As the variables ``x``, ``y`` and ``z`` -appear strictly in the body of the type, they are implicit. - -.. coqtop:: all - - Parameter X : Type. - - Definition Relation := X -> X -> Prop. - - Definition Transitivity (R:Relation) := forall x y:X, R x y -> forall z:X, R y z -> R x z. - - Parameters (R : Relation) (p : Transitivity R). - - Arguments p : default implicits. - - Print p. - - Print Implicit p. - - Parameters (a b c : X) (r1 : R a b) (r2 : R b c). - - Check (p r1 r2). - - -Mode for automatic declaration of implicit arguments -++++++++++++++++++++++++++++++++++++++++++++++++++++ - -.. flag:: Implicit Arguments - - This flag (off by default) allows to systematically declare implicit - the arguments detectable as such. Auto-detection of implicit arguments is - governed by flags controlling whether strict and contextual implicit - arguments have to be considered or not. - -.. _controlling-strict-implicit-args: - -Controlling strict implicit arguments -+++++++++++++++++++++++++++++++++++++ - -.. flag:: Strict Implicit - - When the mode for automatic declaration of implicit arguments is on, - the default is to automatically set implicit only the strict implicit - arguments plus, for historical reasons, a small subset of the non-strict - implicit arguments. To relax this constraint and to set - implicit all non strict implicit arguments by default, you can turn this - flag off. - -.. flag:: Strongly Strict Implicit - - Use this flag (off by default) to capture exactly the strict implicit - arguments and no more than the strict implicit arguments. - -.. _controlling-contextual-implicit-args: - -Controlling contextual implicit arguments -+++++++++++++++++++++++++++++++++++++++++ - -.. flag:: Contextual Implicit - - By default, |Coq| does not automatically set implicit the contextual - implicit arguments. You can turn this flag on to tell |Coq| to also - infer contextual implicit argument. - -.. _controlling-rev-pattern-implicit-args: - -Controlling reversible-pattern implicit arguments -+++++++++++++++++++++++++++++++++++++++++++++++++ - -.. flag:: Reversible Pattern Implicit - - By default, |Coq| does not automatically set implicit the reversible-pattern - implicit arguments. You can turn this flag on to tell |Coq| to also infer - reversible-pattern implicit argument. - -.. _controlling-insertion-implicit-args: - -Controlling the insertion of implicit arguments not followed by explicit arguments -++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ - -.. flag:: Maximal Implicit Insertion - - Assuming the implicit argument mode is on, this flag (off by default) - declares implicit arguments to be automatically inserted when a - function is partially applied and the next argument of the function is - an implicit one. - -Combining manual declaration and automatic declaration -++++++++++++++++++++++++++++++++++++++++++++++++++++++ - -When some arguments are manually specified implicit with binders in a definition -and the automatic declaration mode in on, the manual implicit arguments are added to the -automatically declared ones. - -In that case, and when the flag :flag:`Maximal Implicit Insertion` is set to off, -some trailing implicit arguments can be inferred to be non maximally inserted. In -this case, they are converted to maximally inserted ones. - -.. example:: - - .. coqtop:: all - - Set Implicit Arguments. - Axiom eq0_le0 : forall (n : nat) (x : n = 0), n <= 0. - Print Implicit eq0_le0. - Axiom eq0_le0' : forall (n : nat) {x : n = 0}, n <= 0. - Print Implicit eq0_le0'. - - -.. _explicit-applications: - -Explicit applications -~~~~~~~~~~~~~~~~~~~~~ - -In presence of non-strict or contextual arguments, or in presence of -partial applications, the synthesis of implicit arguments may fail, so -one may have to explicitly give certain implicit arguments of an -application. Use the :n:`(@ident := @term)` form of :token:`arg` to do so, -where :token:`ident` is the name of the implicit argument and :token:`term` -is its corresponding explicit term. Alternatively, one can deactivate -the hiding of implicit arguments for a single function application using the -:n:`@ @qualid {? @univ_annot } {* @term1 }` form of :token:`term10`. - -.. example:: Syntax for explicitly giving implicit arguments (continued) - - .. coqtop:: all - - Check (p r1 (z:=c)). - - Check (p (x:=a) (y:=b) r1 (z:=c) r2). - - -.. _renaming_implicit_arguments: - -Renaming implicit arguments -~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -.. example:: (continued) Renaming implicit arguments - - .. coqtop:: all - - Arguments p [s t] _ [u] _: rename. - - Check (p r1 (u:=c)). - - Check (p (s:=a) (t:=b) r1 (u:=c) r2). - - Fail Arguments p [s t] _ [w] _ : assert. - -.. _displaying-implicit-args: - -Displaying implicit arguments -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -.. cmd:: Print Implicit @smart_qualid - - Displays the implicit arguments associated with an object, - identifying which arguments are applied maximally or not. - - -Displaying implicit arguments when pretty-printing -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -.. flag:: Printing Implicit - - By default, the basic pretty-printing rules hide the inferrable implicit - arguments of an application. Turn this flag on to force printing all - implicit arguments. - -.. flag:: Printing Implicit Defensive - - By default, the basic pretty-printing rules display implicit - arguments that are not detected as strict implicit arguments. This - “defensive” mode can quickly make the display cumbersome so this can - be deactivated by turning this flag off. - -.. seealso:: :flag:`Printing All`. - -Interaction with subtyping -~~~~~~~~~~~~~~~~~~~~~~~~~~ - -When an implicit argument can be inferred from the type of more than -one of the other arguments, then only the type of the first of these -arguments is taken into account, and not an upper type of all of them. -As a consequence, the inference of the implicit argument of “=” fails -in - -.. coqtop:: all - - Fail Check nat = Prop. - -but succeeds in - -.. coqtop:: all - - Check Prop = nat. - - -Deactivation of implicit arguments for parsing -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -.. flag:: Parsing Explicit - - Turning this flag on (it is off by default) deactivates the use of implicit arguments. - - In this case, all arguments of constants, inductive types, - constructors, etc, including the arguments declared as implicit, have - to be given as if no arguments were implicit. By symmetry, this also - affects printing. - -.. _canonical-structure-declaration: - -Canonical structures -~~~~~~~~~~~~~~~~~~~~ - -A canonical structure is an instance of a record/structure type that -can be used to solve unification problems involving a projection -applied to an unknown structure instance (an implicit argument) and a -value. The complete documentation of canonical structures can be found -in :ref:`canonicalstructures`; here only a simple example is given. - -.. cmd:: Canonical {? Structure } @smart_qualid - Canonical {? Structure } @ident_decl @def_body - :name: Canonical Structure; _ - - The first form of this command declares an existing :n:`@smart_qualid` as a - canonical instance of a structure (a record). - - The second form defines a new constant as if the :cmd:`Definition` command - had been used, then declares it as a canonical instance as if the first - form had been used on the defined object. - - This command supports the :attr:`local` attribute. When used, the - structure is canonical only within the :cmd:`Section` containing it. - - Assume that :token:`qualid` denotes an object ``(Build_struct`` |c_1| … |c_n| ``)`` in the - structure :g:`struct` of which the fields are |x_1|, …, |x_n|. - Then, each time an equation of the form ``(``\ |x_i| ``_)`` |eq_beta_delta_iota_zeta| |c_i| has to be - solved during the type checking process, :token:`qualid` is used as a solution. - Otherwise said, :token:`qualid` is canonically used to extend the field |c_i| - into a complete structure built on |c_i|. - - Canonical structures are particularly useful when mixed with coercions - and strict implicit arguments. - - .. example:: - - Here is an example. - - .. coqtop:: all - - Require Import Relations. - - Require Import EqNat. - - Set Implicit Arguments. - - Unset Strict Implicit. - - Structure Setoid : Type := {Carrier :> Set; Equal : relation Carrier; - Prf_equiv : equivalence Carrier Equal}. - - Definition is_law (A B:Setoid) (f:A -> B) := forall x y:A, Equal x y -> Equal (f x) (f y). - - Axiom eq_nat_equiv : equivalence nat eq_nat. - - Definition nat_setoid : Setoid := Build_Setoid eq_nat_equiv. - - Canonical nat_setoid. - - Thanks to :g:`nat_setoid` declared as canonical, the implicit arguments :g:`A` - and :g:`B` can be synthesized in the next statement. - - .. coqtop:: all abort - - Lemma is_law_S : is_law S. - - .. note:: - If a same field occurs in several canonical structures, then - only the structure declared first as canonical is considered. - - .. attr:: canonical(false) - - To prevent a field from being involved in the inference of - canonical instances, its declaration can be annotated with the - :attr:`canonical(false)` attribute (cf. the syntax of - :n:`@record_field`). - - .. example:: - - For instance, when declaring the :g:`Setoid` structure above, the - :g:`Prf_equiv` field declaration could be written as follows. - - .. coqdoc:: - - #[canonical(false)] Prf_equiv : equivalence Carrier Equal - - See :ref:`canonicalstructures` for a more realistic example. - -.. attr:: canonical - - This attribute can decorate a :cmd:`Definition` or :cmd:`Let` command. - It is equivalent to having a :cmd:`Canonical Structure` declaration just - after the command. - -.. cmd:: Print Canonical Projections {* @smart_qualid } - - This displays the list of global names that are components of some - canonical structure. For each of them, the canonical structure of - which it is a projection is indicated. If constants are given as - its arguments, only the unification rules that involve or are - synthesized from simultaneously all given constants will be shown. - - .. example:: - - For instance, the above example gives the following output: - - .. coqtop:: all - - Print Canonical Projections. - - .. coqtop:: all - - Print Canonical Projections nat. - - .. note:: - - The last line in the first example would not show up if the - corresponding projection (namely :g:`Prf_equiv`) were annotated as not - canonical, as described above. - -Implicit types of variables -~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -It is possible to bind variable names to a given type (e.g. in a -development using arithmetic, it may be convenient to bind the names :g:`n` -or :g:`m` to the type :g:`nat` of natural numbers). - -.. cmd:: Implicit {| Type | Types } @reserv_list - :name: Implicit Type; Implicit Types - - .. insertprodn reserv_list simple_reserv - - .. prodn:: - reserv_list ::= {+ ( @simple_reserv ) } - | @simple_reserv - simple_reserv ::= {+ @ident } : @type - - Sets the type of bound - variables starting with :token:`ident` (either :token:`ident` itself or - :token:`ident` followed by one or more single quotes, underscore or - digits) to :token:`type` (unless the bound variable is already declared - with an explicit type, in which case, that type will be used). - -.. example:: - - .. coqtop:: all - - Require Import List. - - Implicit Types m n : nat. - - Lemma cons_inj_nat : forall m n l, n :: l = m :: l -> n = m. - Proof. intros m n. Abort. - - Lemma cons_inj_bool : forall (m n:bool) l, n :: l = m :: l -> n = m. - Abort. - -.. flag:: Printing Use Implicit Types - - By default, the type of bound variables is not printed when - the variable name is associated to an implicit type which matches the - actual type of the variable. This feature can be deactivated by - turning this flag off. - -.. _implicit-generalization: - -Implicit generalization -~~~~~~~~~~~~~~~~~~~~~~~ - -.. index:: `{ } -.. index:: `[ ] -.. index:: `( ) -.. index:: `{! } -.. index:: `[! ] -.. index:: `(! ) - -.. insertprodn generalizing_binder typeclass_constraint - -.. prodn:: - generalizing_binder ::= `( {+, @typeclass_constraint } ) - | `%{ {+, @typeclass_constraint } %} - | `[ {+, @typeclass_constraint } ] - typeclass_constraint ::= {? ! } @term - | %{ @name %} : {? ! } @term - | @name : {? ! } @term - - -Implicit generalization is an automatic elaboration of a statement -with free variables into a closed statement where these variables are -quantified explicitly. Use the :cmd:`Generalizable` command to designate -which variables should be generalized. - -It is activated for a binder by prefixing a \`, and for terms by -surrounding it with \`{ }, or \`[ ] or \`( ). - -Terms surrounded by \`{ } introduce their free variables as maximally -inserted implicit arguments, terms surrounded by \`[ ] introduce them as -non maximally inserted implicit arguments and terms surrounded by \`( ) -introduce them as explicit arguments. - -Generalizing binders always introduce their free variables as -maximally inserted implicit arguments. The binder itself introduces -its argument as usual. - -In the following statement, ``A`` and ``y`` are automatically -generalized, ``A`` is implicit and ``x``, ``y`` and the anonymous -equality argument are explicit. - -.. coqtop:: all reset - - Generalizable All Variables. - - Definition sym `(x:A) : `(x = y -> y = x) := fun _ p => eq_sym p. - - Print sym. - -Dually to normal binders, the name is optional but the type is required: - -.. coqtop:: all - - Check (forall `{x = y :> A}, y = x). - -When generalizing a binder whose type is a typeclass, its own class -arguments are omitted from the syntax and are generalized using -automatic names, without instance search. Other arguments are also -generalized unless provided. This produces a fully general statement. -this behaviour may be disabled by prefixing the type with a ``!`` or -by forcing the typeclass name to be an explicit application using -``@`` (however the later ignores implicit argument information). - -.. coqtop:: all - - Class Op (A:Type) := op : A -> A -> A. - - Class Commutative (A:Type) `(Op A) := commutative : forall x y, op x y = op y x. - Instance nat_op : Op nat := plus. - - Set Printing Implicit. - Check (forall `{Commutative }, True). - Check (forall `{Commutative nat}, True). - Fail Check (forall `{Commutative nat _}, True). - Fail Check (forall `{!Commutative nat}, True). - Arguments Commutative _ {_}. - Check (forall `{!Commutative nat}, True). - Check (forall `{@Commutative nat plus}, True). - -Multiple binders can be merged using ``,`` as a separator: - -.. coqtop:: all - - Check (forall `{Commutative A, Hnat : !Commutative nat}, True). - -.. cmd:: Generalizable {| {| Variable | Variables } {+ @ident } | All Variables | No Variables } - - Controls the set of generalizable identifiers. By default, no variables are - generalizable. - - This command supports the :attr:`global` attribute. - - The :n:`{| Variable | Variables } {+ @ident }` form allows generalization of only the given :n:`@ident`\s. - Using this command multiple times adds to the allowed identifiers. The other forms clear - the list of :n:`@ident`\s. - - The :n:`All Variables` form generalizes all free variables in - the context that appear under a - generalization delimiter. This may result in confusing errors in case - of typos. In such cases, the context will probably contain some - unexpected generalized variables. - - The :n:`No Variables` form disables implicit generalization entirely. This is - the default behavior (before any :cmd:`Generalizable` command has been entered). - - -.. _Coercions: - -Coercions ---------- - -Coercions can be used to implicitly inject terms from one *class* in -which they reside into another one. A *class* is either a sort -(denoted by the keyword ``Sortclass``), a product type (denoted by the -keyword ``Funclass``), or a type constructor (denoted by its name), e.g. -an inductive type or any constant with a type of the form -:n:`forall {+ @binder }, @sort`. - -Then the user is able to apply an object that is not a function, but -can be coerced to a function, and more generally to consider that a -term of type ``A`` is of type ``B`` provided that there is a declared coercion -between ``A`` and ``B``. - -More details and examples, and a description of the commands related -to coercions are provided in :ref:`implicitcoercions`. - -.. _printing_constructions_full: - -Printing constructions in full ------------------------------- - -.. flag:: Printing All - - Coercions, implicit arguments, the type of pattern matching, but also - notations (see :ref:`syntaxextensionsandinterpretationscopes`) can obfuscate the behavior of some - tactics (typically the tactics applying to occurrences of subterms are - sensitive to the implicit arguments). Turning this flag on - deactivates all high-level printing features such as coercions, - implicit arguments, returned type of pattern matching, notations and - various syntactic sugar for pattern matching or record projections. - Otherwise said, :flag:`Printing All` includes the effects of the flags - :flag:`Printing Implicit`, :flag:`Printing Coercions`, :flag:`Printing Synth`, - :flag:`Printing Projections`, and :flag:`Printing Notations`. To reactivate - the high-level printing features, use the command ``Unset Printing All``. - -.. _printing-universes: - -Printing universes ------------------- - -.. flag:: Printing Universes - - Turn this flag on to activate the display of the actual level of each - occurrence of :g:`Type`. See :ref:`Sorts` for details. This wizard flag, in - combination with :flag:`Printing All` can help to diagnose failures to unify - terms apparently identical but internally different in the Calculus of Inductive - Constructions. - -.. cmd:: Print {? Sorted } Universes {? Subgraph ( {* @qualid } ) } {? @string } - :name: Print Universes - - This command can be used to print the constraints on the internal level - of the occurrences of :math:`\Type` (see :ref:`Sorts`). - - The :n:`Subgraph` clause limits the printed graph to the requested names (adjusting - constraints to preserve the implied transitive constraints between - kept universes). - - The :n:`Sorted` clause makes each universe - equivalent to a numbered label reflecting its level (with a linear - ordering) in the universe hierarchy. - - :n:`@string` is an optional output filename. - If :n:`@string` ends in ``.dot`` or ``.gv``, the constraints are printed in the DOT - language, and can be processed by Graphviz tools. The format is - unspecified if `string` doesn’t end in ``.dot`` or ``.gv``. - -.. _existential-variables: - -Existential variables ---------------------- - -.. insertprodn term_evar term_evar - -.. prodn:: - term_evar ::= ?[ @ident ] - | ?[ ?@ident ] - | ?@ident {? @%{ {+; @ident := @term } %} } - -|Coq| terms can include existential variables which represents unknown -subterms to eventually be replaced by actual subterms. - -Existential variables are generated in place of unsolvable implicit -arguments or “_” placeholders when using commands such as ``Check`` (see -Section :ref:`requests-to-the-environment`) or when using tactics such as -:tacn:`refine`, as well as in place of unsolvable instances when using -tactics such that :tacn:`eapply`. An existential -variable is defined in a context, which is the context of variables of -the placeholder which generated the existential variable, and a type, -which is the expected type of the placeholder. - -As a consequence of typing constraints, existential variables can be -duplicated in such a way that they possibly appear in different -contexts than their defining context. Thus, any occurrence of a given -existential variable comes with an instance of its original context. -In the simple case, when an existential variable denotes the -placeholder which generated it, or is used in the same context as the -one in which it was generated, the context is not displayed and the -existential variable is represented by “?” followed by an identifier. - -.. coqtop:: all - - Parameter identity : forall (X:Set), X -> X. - - Check identity _ _. - - Check identity _ (fun x => _). - -In the general case, when an existential variable :n:`?@ident` appears -outside of its context of definition, its instance, written under the -form :n:`{ {*; @ident := @term} }` is appending to its name, indicating -how the variables of its defining context are instantiated. -The variables of the context of the existential variables which are -instantiated by themselves are not written, unless the :flag:`Printing Existential Instances` flag -is on (see Section :ref:`explicit-display-existentials`), and this is why an -existential variable used in the same context as its context of definition is written with no instance. - -.. coqtop:: all - - Check (fun x y => _) 0 1. - - Set Printing Existential Instances. - - Check (fun x y => _) 0 1. - -Existential variables can be named by the user upon creation using -the syntax :n:`?[@ident]`. This is useful when the existential -variable needs to be explicitly handled later in the script (e.g. -with a named-goal selector, see :ref:`goal-selectors`). - -.. _explicit-display-existentials: - -Explicit displaying of existential instances for pretty-printing -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -.. flag:: Printing Existential Instances - - This flag (off by default) activates the full display of how the - context of an existential variable is instantiated at each of the - occurrences of the existential variable. - -.. _tactics-in-terms: - -Solving existential variables using tactics -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -Instead of letting the unification engine try to solve an existential -variable by itself, one can also provide an explicit hole together -with a tactic to solve it. Using the syntax ``ltac:(``\ `tacexpr`\ ``)``, the user -can put a tactic anywhere a term is expected. The order of resolution -is not specified and is implementation-dependent. The inner tactic may -use any variable defined in its scope, including repeated alternations -between variables introduced by term binding as well as those -introduced by tactic binding. The expression `tacexpr` can be any tactic -expression as described in :ref:`ltac`. - -.. coqtop:: all - - Definition foo (x : nat) : nat := ltac:(exact x). - -This construction is useful when one wants to define complicated terms -using highly automated tactics without resorting to writing the proof-term -by means of the interactive proof engine. - -.. _primitive-integers: - -Primitive Integers ------------------- - -The language of terms features 63-bit machine integers as values. The type of -such a value is *axiomatized*; it is declared through the following sentence -(excerpt from the :g:`Int63` module): - -.. coqdoc:: - - Primitive int := #int63_type. - -This type is equipped with a few operators, that must be similarly declared. -For instance, equality of two primitive integers can be decided using the :g:`Int63.eqb` function, -declared and specified as follows: - -.. coqdoc:: - - Primitive eqb := #int63_eq. - Notation "m '==' n" := (eqb m n) (at level 70, no associativity) : int63_scope. - - Axiom eqb_correct : forall i j, (i == j)%int63 = true -> i = j. - -The complete set of such operators can be obtained looking at the :g:`Int63` module. - -These primitive declarations are regular axioms. As such, they must be trusted and are listed by the -:g:`Print Assumptions` command, as in the following example. - -.. coqtop:: in reset - - From Coq Require Import Int63. - Lemma one_minus_one_is_zero : (1 - 1 = 0)%int63. - Proof. apply eqb_correct; vm_compute; reflexivity. Qed. - -.. coqtop:: all - - Print Assumptions one_minus_one_is_zero. - -The reduction machines (:tacn:`vm_compute`, :tacn:`native_compute`) implement -dedicated, efficient, rules to reduce the applications of these primitive -operations. - -The extraction of these primitives can be customized similarly to the extraction -of regular axioms (see :ref:`extraction`). Nonetheless, the :g:`ExtrOCamlInt63` -module can be used when extracting to OCaml: it maps the Coq primitives to types -and functions of a :g:`Uint63` module. Said OCaml module is not produced by -extraction. Instead, it has to be provided by the user (if they want to compile -or execute the extracted code). For instance, an implementation of this module -can be taken from the kernel of Coq. - -Literal values (at type :g:`Int63.int`) are extracted to literal OCaml values -wrapped into the :g:`Uint63.of_int` (resp. :g:`Uint63.of_int64`) constructor on -64-bit (resp. 32-bit) platforms. Currently, this cannot be customized (see the -function :g:`Uint63.compile` from the kernel). - -.. _primitive-floats: - -Primitive Floats ----------------- - -The language of terms features Binary64 floating-point numbers as values. -The type of such a value is *axiomatized*; it is declared through the -following sentence (excerpt from the :g:`PrimFloat` module): - -.. coqdoc:: - - Primitive float := #float64_type. - -This type is equipped with a few operators, that must be similarly declared. -For instance, the product of two primitive floats can be computed using the -:g:`PrimFloat.mul` function, declared and specified as follows: - -.. coqdoc:: - - Primitive mul := #float64_mul. - Notation "x * y" := (mul x y) : float_scope. - - Axiom mul_spec : forall x y, Prim2SF (x * y)%float = SF64mul (Prim2SF x) (Prim2SF y). - -where :g:`Prim2SF` is defined in the :g:`FloatOps` module. - -The set of such operators is described in section :ref:`floats_library`. - -These primitive declarations are regular axioms. As such, they must be trusted, and are listed by the -:g:`Print Assumptions` command. - -The reduction machines (:tacn:`vm_compute`, :tacn:`native_compute`) implement -dedicated, efficient rules to reduce the applications of these primitive -operations, using the floating-point processor operators that are assumed -to comply with the IEEE 754 standard for floating-point arithmetic. - -The extraction of these primitives can be customized similarly to the extraction -of regular axioms (see :ref:`extraction`). Nonetheless, the :g:`ExtrOCamlFloats` -module can be used when extracting to OCaml: it maps the Coq primitives to types -and functions of a :g:`Float64` module. Said OCaml module is not produced by -extraction. Instead, it has to be provided by the user (if they want to compile -or execute the extracted code). For instance, an implementation of this module -can be taken from the kernel of Coq. - -Literal values (of type :g:`Float64.t`) are extracted to literal OCaml -values (of type :g:`float`) written in hexadecimal notation and -wrapped into the :g:`Float64.of_float` constructor, e.g.: -:g:`Float64.of_float (0x1p+0)`. - -.. _bidirectionality_hints: - -Bidirectionality hints ----------------------- - -When type-checking an application, Coq normally does not use information from -the context to infer the types of the arguments. It only checks after the fact -that the type inferred for the application is coherent with the expected type. -Bidirectionality hints make it possible to specify that after type-checking the -first arguments of an application, typing information should be propagated from -the context to help inferring the types of the remaining arguments. - -An :cmd:`Arguments` command containing :n:`@argument_spec_block__1 & @argument_spec_block__2` -provides :ref:`bidirectionality_hints`. -It tells the typechecking algorithm, when type-checking -applications of :n:`@qualid`, to first type-check the arguments in -:n:`@argument_spec_block__1` and then propagate information from the typing context to -type-check the remaining arguments (in :n:`@argument_spec_block__2`). - -.. example:: Bidirectionality hints - - In a context where a coercion was declared from ``bool`` to ``nat``: - - .. coqtop:: in reset - - Definition b2n (b : bool) := if b then 1 else 0. - Coercion b2n : bool >-> nat. - - Coq cannot automatically coerce existential statements over ``bool`` to - statements over ``nat``, because the need for inserting a coercion is known - only from the expected type of a subterm: - - .. coqtop:: all - - Fail Check (ex_intro _ true _ : exists n : nat, n > 0). - - However, a suitable bidirectionality hint makes the example work: - - .. coqtop:: all - - Arguments ex_intro _ _ & _ _. - Check (ex_intro _ true _ : exists n : nat, n > 0). - -Coq will attempt to produce a term which uses the arguments you -provided, but in some cases involving Program mode the arguments after -the bidirectionality starts may be replaced by convertible but -syntactically different terms. -- cgit v1.2.3 From 313d48a0cd8c800e739f6fb1ce4b9d9d086b0cbc Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Fri, 3 Apr 2020 15:46:50 +0200 Subject: Move section on funind in appropriate location (inside libraries). --- doc/sphinx/language/gallina-extensions.rst | 169 ----------------------------- doc/sphinx/using/libraries/funind.rst | 169 +++++++++++++++++++++++++++++ doc/sphinx/using/libraries/index.rst | 1 + 3 files changed, 170 insertions(+), 169 deletions(-) delete mode 100644 doc/sphinx/language/gallina-extensions.rst create mode 100644 doc/sphinx/using/libraries/funind.rst (limited to 'doc') diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst deleted file mode 100644 index 6d5791bc19..0000000000 --- a/doc/sphinx/language/gallina-extensions.rst +++ /dev/null @@ -1,169 +0,0 @@ -Functional induction -==================== - -.. _advanced-recursive-functions: - -Advanced recursive functions ----------------------------- - -The following command is available when the ``FunInd`` library has been loaded via ``Require Import FunInd``: - -.. cmd:: Function @fix_definition {* with @fix_definition } - - This command is a generalization of :cmd:`Fixpoint`. It is a wrapper - for several ways of defining a function *and* other useful related - objects, namely: an induction principle that reflects the recursive - structure of the function (see :tacn:`function induction`) and its fixpoint equality. - This defines a function similar to those defined by :cmd:`Fixpoint`. - As in :cmd:`Fixpoint`, the decreasing argument must - be given (unless the function is not recursive), but it might not - necessarily be *structurally* decreasing. Use the :n:`@fixannot` clause - to name the decreasing argument *and* to describe which kind of - decreasing criteria to use to ensure termination of recursive - calls. - - :cmd:`Function` also supports the :n:`with` clause to create - mutually recursive definitions, however this feature is limited - to structurally recursive functions (i.e. when :n:`@fixannot` is a :n:`struct` - clause). - - See :tacn:`function induction` and :cmd:`Functional Scheme` for how to use - the induction principle to reason easily about the function. - - The form of the :n:`@fixannot` clause determines which definition mechanism :cmd:`Function` uses. - (Note that references to :n:`ident` below refer to the name of the function being defined.): - - * If :n:`@fixannot` is not specified, :cmd:`Function` - defines the nonrecursive function :token:`ident` as if it was declared with - :cmd:`Definition`. In addition, the following are defined: - - + :token:`ident`\ ``_rect``, :token:`ident`\ ``_rec`` and :token:`ident`\ ``_ind``, - which reflect the pattern matching structure of :token:`term` (see :cmd:`Inductive`); - + The inductive :n:`R_@ident` corresponding to the graph of :token:`ident` (silently); - + :token:`ident`\ ``_complete`` and :token:`ident`\ ``_correct`` which - are inversion information linking the function and its graph. - - * If :n:`{ struct ... }` is specified, :cmd:`Function` - defines the structural recursive function :token:`ident` as if it was declared - with :cmd:`Fixpoint`. In addition, the following are defined: - - + The same objects as above; - + The fixpoint equation of :token:`ident`: :n:`@ident`\ ``_equation``. - - * If :n:`{ measure ... }` or :n:`{ wf ... }` are specified, :cmd:`Function` - defines a recursive function by well-founded recursion. The module ``Recdef`` - of the standard library must be loaded for this feature. - - + :n:`{measure @one_term__1 {? @ident } {? @one_term__2 } }`\: where :n:`@ident` is the decreasing argument - and :n:`@one_term__1` is a function from the type of :n:`@ident` to :g:`nat` for which - the decreasing argument decreases (for the :g:`lt` order on :g:`nat`) - for each recursive call of the function. The parameters of the function are - bound in :n:`@one_term__1`. - + :n:`{wf @one_term @ident }`\: where :n:`@ident` is the decreasing argument and - :n:`@one_term` is an ordering relation on the type of :n:`@ident` (i.e. of type - `T`\ :math:`_{\sf ident}` → `T`\ :math:`_{\sf ident}` → ``Prop``) for which the decreasing argument - decreases for each recursive call of the function. The order must be well-founded. - The parameters of the function are bound in :n:`@one_term`. - - If the clause is ``measure`` or ``wf``, the user is left with some proof - obligations that will be used to define the function. These proofs - are: proofs that each recursive call is actually decreasing with - respect to the given criteria, and (if the criteria is `wf`) a proof - that the ordering relation is well-founded. Once proof obligations are - discharged, the following objects are defined: - - + The same objects as with the ``struct`` clause; - + The lemma :n:`@ident`\ ``_tcc`` which collects all proof obligations in one - property; - + The lemmas :n:`@ident`\ ``_terminate`` and :n:`@ident`\ ``_F`` which will be inlined - during extraction of :n:`@ident`. - - The way this recursive function is defined is the subject of several - papers by Yves Bertot and Antonia Balaa on the one hand, and Gilles - Barthe, Julien Forest, David Pichardie, and Vlad Rusu on the other - hand. - -.. note:: - - To obtain the right principle, it is better to put rigid - parameters of the function as first arguments. For example it is - better to define plus like this: - - .. coqtop:: reset none - - Require Import FunInd. - - .. coqtop:: all - - Function plus (m n : nat) {struct n} : nat := - match n with - | 0 => m - | S p => S (plus m p) - end. - - than like this: - - .. coqtop:: reset none - - Require Import FunInd. - - .. coqtop:: all - - Function plus (n m : nat) {struct n} : nat := - match n with - | 0 => m - | S p => S (plus p m) - end. - - -*Limitations* - -:token:`term` must be built as a *pure pattern matching tree* (:g:`match … with`) -with applications only *at the end* of each branch. - -:cmd:`Function` does not support partial application of the function being -defined. Thus, the following example cannot be accepted due to the -presence of partial application of :g:`wrong` in the body of :g:`wrong`: - -.. coqtop:: none - - Require List. - Import List.ListNotations. - -.. coqtop:: all fail - - Function wrong (C:nat) : nat := - List.hd 0 (List.map wrong (C::nil)). - -For now, dependent cases are not treated for non structurally -terminating functions. - -.. exn:: The recursive argument must be specified. - :undocumented: - -.. exn:: No argument name @ident. - :undocumented: - -.. exn:: Cannot use mutual definition with well-founded recursion or measure. - :undocumented: - -.. warn:: Cannot define graph for @ident. - - The generation of the graph relation (:n:`R_@ident`) used to compute the induction scheme of ident - raised a typing error. Only :token:`ident` is defined; the induction scheme - will not be generated. This error happens generally when: - - - the definition uses pattern matching on dependent types, - which :cmd:`Function` cannot deal with yet. - - the definition is not a *pattern matching tree* as explained above. - -.. warn:: Cannot define principle(s) for @ident. - - The generation of the graph relation (:n:`R_@ident`) succeeded but the induction principle - could not be built. Only :token:`ident` is defined. Please report. - -.. warn:: Cannot build functional inversion principle. - - :tacn:`functional inversion` will not be available for the function. - -.. seealso:: :ref:`functional-scheme` and :tacn:`function induction` diff --git a/doc/sphinx/using/libraries/funind.rst b/doc/sphinx/using/libraries/funind.rst new file mode 100644 index 0000000000..ed00f3d455 --- /dev/null +++ b/doc/sphinx/using/libraries/funind.rst @@ -0,0 +1,169 @@ +Functional induction +==================== + +.. _advanced-recursive-functions: + +Advanced recursive functions +---------------------------- + +The following command is available when the ``FunInd`` library has been loaded via ``Require Import FunInd``: + +.. cmd:: Function @fix_definition {* with @fix_definition } + + This command is a generalization of :cmd:`Fixpoint`. It is a wrapper + for several ways of defining a function *and* other useful related + objects, namely: an induction principle that reflects the recursive + structure of the function (see :tacn:`function induction`) and its fixpoint equality. + This defines a function similar to those defined by :cmd:`Fixpoint`. + As in :cmd:`Fixpoint`, the decreasing argument must + be given (unless the function is not recursive), but it might not + necessarily be *structurally* decreasing. Use the :n:`@fixannot` clause + to name the decreasing argument *and* to describe which kind of + decreasing criteria to use to ensure termination of recursive + calls. + + :cmd:`Function` also supports the :n:`with` clause to create + mutually recursive definitions, however this feature is limited + to structurally recursive functions (i.e. when :n:`@fixannot` is a :n:`struct` + clause). + + See :tacn:`function induction` and :cmd:`Functional Scheme` for how to use + the induction principle to reason easily about the function. + + The form of the :n:`@fixannot` clause determines which definition mechanism :cmd:`Function` uses. + (Note that references to :n:`ident` below refer to the name of the function being defined.): + + * If :n:`@fixannot` is not specified, :cmd:`Function` + defines the nonrecursive function :token:`ident` as if it was declared with + :cmd:`Definition`. In addition, the following are defined: + + + :token:`ident`\ ``_rect``, :token:`ident`\ ``_rec`` and :token:`ident`\ ``_ind``, + which reflect the pattern matching structure of :token:`term` (see :cmd:`Inductive`); + + The inductive :n:`R_@ident` corresponding to the graph of :token:`ident` (silently); + + :token:`ident`\ ``_complete`` and :token:`ident`\ ``_correct`` which + are inversion information linking the function and its graph. + + * If :n:`{ struct ... }` is specified, :cmd:`Function` + defines the structural recursive function :token:`ident` as if it was declared + with :cmd:`Fixpoint`. In addition, the following are defined: + + + The same objects as above; + + The fixpoint equation of :token:`ident`: :n:`@ident`\ ``_equation``. + + * If :n:`{ measure ... }` or :n:`{ wf ... }` are specified, :cmd:`Function` + defines a recursive function by well-founded recursion. The module ``Recdef`` + of the standard library must be loaded for this feature. + + + :n:`{measure @one_term__1 {? @ident } {? @one_term__2 } }`\: where :n:`@ident` is the decreasing argument + and :n:`@one_term__1` is a function from the type of :n:`@ident` to :g:`nat` for which + the decreasing argument decreases (for the :g:`lt` order on :g:`nat`) + for each recursive call of the function. The parameters of the function are + bound in :n:`@one_term__1`. + + :n:`{wf @one_term @ident }`\: where :n:`@ident` is the decreasing argument and + :n:`@one_term` is an ordering relation on the type of :n:`@ident` (i.e. of type + `T`\ :math:`_{\sf ident}` → `T`\ :math:`_{\sf ident}` → ``Prop``) for which the decreasing argument + decreases for each recursive call of the function. The order must be well-founded. + The parameters of the function are bound in :n:`@one_term`. + + If the clause is ``measure`` or ``wf``, the user is left with some proof + obligations that will be used to define the function. These proofs + are: proofs that each recursive call is actually decreasing with + respect to the given criteria, and (if the criteria is `wf`) a proof + that the ordering relation is well-founded. Once proof obligations are + discharged, the following objects are defined: + + + The same objects as with the ``struct`` clause; + + The lemma :n:`@ident`\ ``_tcc`` which collects all proof obligations in one + property; + + The lemmas :n:`@ident`\ ``_terminate`` and :n:`@ident`\ ``_F`` which will be inlined + during extraction of :n:`@ident`. + + The way this recursive function is defined is the subject of several + papers by Yves Bertot and Antonia Balaa on the one hand, and Gilles + Barthe, Julien Forest, David Pichardie, and Vlad Rusu on the other + hand. + +.. note:: + + To obtain the right principle, it is better to put rigid + parameters of the function as first arguments. For example it is + better to define plus like this: + + .. coqtop:: reset none + + Require Import FunInd. + + .. coqtop:: all + + Function plus (m n : nat) {struct n} : nat := + match n with + | 0 => m + | S p => S (plus m p) + end. + + than like this: + + .. coqtop:: reset none + + Require Import FunInd. + + .. coqtop:: all + + Function plus (n m : nat) {struct n} : nat := + match n with + | 0 => m + | S p => S (plus p m) + end. + + +*Limitations* + +:token:`term` must be built as a *pure pattern matching tree* (:g:`match … with`) +with applications only *at the end* of each branch. + +:cmd:`Function` does not support partial application of the function being +defined. Thus, the following example cannot be accepted due to the +presence of partial application of :g:`wrong` in the body of :g:`wrong`: + +.. coqtop:: none + + Require List. + Import List.ListNotations. + +.. coqtop:: all fail + + Function wrong (C:nat) : nat := + List.hd 0 (List.map wrong (C::nil)). + +For now, dependent cases are not treated for non structurally +terminating functions. + +.. exn:: The recursive argument must be specified. + :undocumented: + +.. exn:: No argument name @ident. + :undocumented: + +.. exn:: Cannot use mutual definition with well-founded recursion or measure. + :undocumented: + +.. warn:: Cannot define graph for @ident. + + The generation of the graph relation (:n:`R_@ident`) used to compute the induction scheme of ident + raised a typing error. Only :token:`ident` is defined; the induction scheme + will not be generated. This error happens generally when: + + - the definition uses pattern matching on dependent types, + which :cmd:`Function` cannot deal with yet. + - the definition is not a *pattern matching tree* as explained above. + +.. warn:: Cannot define principle(s) for @ident. + + The generation of the graph relation (:n:`R_@ident`) succeeded but the induction principle + could not be built. Only :token:`ident` is defined. Please report. + +.. warn:: Cannot build functional inversion principle. + + :tacn:`functional inversion` will not be available for the function. + +.. seealso:: :ref:`functional-scheme` and :tacn:`function induction` diff --git a/doc/sphinx/using/libraries/index.rst b/doc/sphinx/using/libraries/index.rst index d0848e6c3f..ad10869439 100644 --- a/doc/sphinx/using/libraries/index.rst +++ b/doc/sphinx/using/libraries/index.rst @@ -22,3 +22,4 @@ installed with the `opam package manager ../../language/coq-library ../../addendum/extraction ../../addendum/miscellaneous-extensions + funind -- cgit v1.2.3 From 9c1cf4278ff12c232fbffba33b38395d9959b875 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Mon, 20 Apr 2020 18:05:03 +0200 Subject: Extract Functional Scheme from Scheme chapter. --- doc/sphinx/user-extensions/proof-schemes.rst | 263 --------------------------- 1 file changed, 263 deletions(-) (limited to 'doc') diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst index 34197c4fcf..7917f49ef5 100644 --- a/doc/sphinx/user-extensions/proof-schemes.rst +++ b/doc/sphinx/user-extensions/proof-schemes.rst @@ -1,195 +1,3 @@ -.. _proofschemes: - -Proof schemes -=============== - -.. _proofschemes-induction-principles: - -Generation of induction principles with ``Scheme`` --------------------------------------------------------- - -The ``Scheme`` command is a high-level tool for generating automatically -(possibly mutual) induction principles for given types and sorts. Its -syntax follows the schema: - -.. cmd:: Scheme @ident__1 := Induction for @ident__2 Sort @sort {* with @ident__i := Induction for @ident__j Sort @sort} - - This command is a high-level tool for generating automatically - (possibly mutual) induction principles for given types and sorts. - Each :n:`@ident__j` is a different inductive type identifier belonging to - the same package of mutual inductive definitions. - The command generates the :n:`@ident__i`\s to be mutually recursive - definitions. Each term :n:`@ident__i` proves a general principle of mutual - induction for objects in type :n:`@ident__j`. - -.. cmdv:: Scheme @ident := Minimality for @ident Sort @sort {* with @ident := Minimality for @ident' Sort @sort} - - Same as before but defines a non-dependent elimination principle more - natural in case of inductively defined relations. - -.. cmdv:: Scheme Equality for @ident - :name: Scheme Equality - - Tries to generate a Boolean equality and a proof of the decidability of the usual equality. If `ident` - involves some other inductive types, their equality has to be defined first. - -.. cmdv:: Scheme Induction for @ident Sort @sort {* with Induction for @ident Sort @sort} - - If you do not provide the name of the schemes, they will be automatically computed from the - sorts involved (works also with Minimality). - -.. example:: - - Induction scheme for tree and forest. - - A mutual induction principle for tree and forest in sort ``Set`` can be defined using the command - - .. coqtop:: none - - Axiom A : Set. - Axiom B : Set. - - .. coqtop:: all - - Inductive tree : Set := node : A -> forest -> tree - with forest : Set := - leaf : B -> forest - | cons : tree -> forest -> forest. - - Scheme tree_forest_rec := Induction for tree Sort Set - with forest_tree_rec := Induction for forest Sort Set. - - You may now look at the type of tree_forest_rec: - - .. coqtop:: all - - Check tree_forest_rec. - - This principle involves two different predicates for trees andforests; - it also has three premises each one corresponding to a constructor of - one of the inductive definitions. - - The principle `forest_tree_rec` shares exactly the same premises, only - the conclusion now refers to the property of forests. - -.. example:: - - Predicates odd and even on naturals. - - Let odd and even be inductively defined as: - - .. coqtop:: all - - Inductive odd : nat -> Prop := oddS : forall n:nat, even n -> odd (S n) - with even : nat -> Prop := - | evenO : even 0 - | evenS : forall n:nat, odd n -> even (S n). - - The following command generates a powerful elimination principle: - - .. coqtop:: all - - Scheme odd_even := Minimality for odd Sort Prop - with even_odd := Minimality for even Sort Prop. - - The type of odd_even for instance will be: - - .. coqtop:: all - - Check odd_even. - - The type of `even_odd` shares the same premises but the conclusion is - `(n:nat)(even n)->(P0 n)`. - - -Automatic declaration of schemes -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -.. flag:: Elimination Schemes - - Enables automatic declaration of induction principles when defining a new - inductive type. Defaults to on. - -.. flag:: Nonrecursive Elimination Schemes - - Enables automatic declaration of induction principles for types declared with the :cmd:`Variant` and - :cmd:`Record` commands. Defaults to off. - -.. flag:: Case Analysis Schemes - - This flag governs the generation of case analysis lemmas for inductive types, - i.e. corresponding to the pattern matching term alone and without fixpoint. - -.. flag:: Boolean Equality Schemes - Decidable Equality Schemes - - These flags control the automatic declaration of those Boolean equalities (see - the second variant of ``Scheme``). - -.. warning:: - - You have to be careful with these flags since Coq may now reject well-defined - inductive types because it cannot compute a Boolean equality for them. - -.. flag:: Rewriting Schemes - - This flag governs generation of equality-related schemes such as congruence. - -Combined Scheme -~~~~~~~~~~~~~~~~~~~~~~ - -.. cmd:: Combined Scheme @ident from {+, @ident__i} - - This command is a tool for combining induction principles generated - by the :cmd:`Scheme` command. - Each :n:`@ident__i` is a different inductive principle that must belong - to the same package of mutual inductive principle definitions. - This command generates :n:`@ident` to be the conjunction of the - principles: it is built from the common premises of the principles - and concluded by the conjunction of their conclusions. - In the case where all the inductive principles used are in sort - ``Prop``, the propositional conjunction ``and`` is used, otherwise - the simple product ``prod`` is used instead. - -.. example:: - - We can define the induction principles for trees and forests using: - - .. coqtop:: all - - Scheme tree_forest_ind := Induction for tree Sort Prop - with forest_tree_ind := Induction for forest Sort Prop. - - Then we can build the combined induction principle which gives the - conjunction of the conclusions of each individual principle: - - .. coqtop:: all - - Combined Scheme tree_forest_mutind from tree_forest_ind,forest_tree_ind. - - The type of tree_forest_mutind will be: - - .. coqtop:: all - - Check tree_forest_mutind. - -.. example:: - - We can also combine schemes at sort ``Type``: - - .. coqtop:: all - - Scheme tree_forest_rect := Induction for tree Sort Type - with forest_tree_rect := Induction for forest Sort Type. - - .. coqtop:: all - - Combined Scheme tree_forest_mutrect from tree_forest_rect, forest_tree_rect. - - .. coqtop:: all - - Check tree_forest_mutrect. - .. _functional-scheme: Generation of induction principles with ``Functional`` ``Scheme`` @@ -330,74 +138,3 @@ Generation of induction principles with ``Functional`` ``Scheme`` .. coqtop:: all Check tree_size_ind2. - -.. _derive-inversion: - -Generation of inversion principles with ``Derive`` ``Inversion`` ------------------------------------------------------------------ - -.. cmd:: Derive Inversion @ident with @ident Sort @sort - Derive Inversion @ident with (forall {* @binder }, @ident @term) Sort @sort - - This command generates an inversion principle for the - :tacn:`inversion ... using ...` tactic. The first :token:`ident` is the name - of the generated principle. The second :token:`ident` should be an inductive - predicate, and :token:`binders` the variables occurring in the term - :token:`term`. This command generates the inversion lemma for the sort - :token:`sort` corresponding to the instance :n:`forall {* @binder }, @ident @term`. - When applied, it is equivalent to having inverted the instance with the - tactic :g:`inversion`. - -.. cmdv:: Derive Inversion_clear @ident with @ident Sort @sort - Derive Inversion_clear @ident with (forall {* @binder }, @ident @term) Sort @sort - - When applied, it is equivalent to having inverted the instance with the - tactic inversion replaced by the tactic `inversion_clear`. - -.. cmdv:: Derive Dependent Inversion @ident with @ident Sort @sort - Derive Dependent Inversion @ident with (forall {* @binder }, @ident @term) Sort @sort - - When applied, it is equivalent to having inverted the instance with - the tactic `dependent inversion`. - -.. cmdv:: Derive Dependent Inversion_clear @ident with @ident Sort @sort - Derive Dependent Inversion_clear @ident with (forall {* @binder }, @ident @term) Sort @sort - - When applied, it is equivalent to having inverted the instance - with the tactic `dependent inversion_clear`. - -.. example:: - - Consider the relation `Le` over natural numbers and the following - parameter ``P``: - - .. coqtop:: all - - Inductive Le : nat -> nat -> Set := - | LeO : forall n:nat, Le 0 n - | LeS : forall n m:nat, Le n m -> Le (S n) (S m). - - Parameter P : nat -> nat -> Prop. - - To generate the inversion lemma for the instance :g:`(Le (S n) m)` and the - sort :g:`Prop`, we do: - - .. coqtop:: all - - Derive Inversion_clear leminv with (forall n m:nat, Le (S n) m) Sort Prop. - Check leminv. - - Then we can use the proven inversion lemma: - - .. the original LaTeX did not have any Coq code to setup the goal - - .. coqtop:: none - - Goal forall (n m : nat) (H : Le (S n) m), P n m. - intros. - - .. coqtop:: all - - Show. - - inversion H using leminv. -- cgit v1.2.3 From d1ae08749eb7264b986b62316d9cd1a3b54f0fed Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Mon, 20 Apr 2020 18:07:23 +0200 Subject: Move Functional Scheme to Funind section. --- doc/sphinx/user-extensions/proof-schemes.rst | 140 --------------------------- doc/sphinx/using/libraries/funind.rst | 140 +++++++++++++++++++++++++++ 2 files changed, 140 insertions(+), 140 deletions(-) delete mode 100644 doc/sphinx/user-extensions/proof-schemes.rst create mode 100644 doc/sphinx/using/libraries/funind.rst (limited to 'doc') diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst deleted file mode 100644 index 7917f49ef5..0000000000 --- a/doc/sphinx/user-extensions/proof-schemes.rst +++ /dev/null @@ -1,140 +0,0 @@ -.. _functional-scheme: - -Generation of induction principles with ``Functional`` ``Scheme`` ------------------------------------------------------------------ - - -.. cmd:: Functional Scheme @ident__0 := Induction for @ident' Sort @sort {* with @ident__i := Induction for @ident__i' Sort @sort} - - This command is a high-level experimental tool for - generating automatically induction principles corresponding to - (possibly mutually recursive) functions. First, it must be made - available via ``Require Import FunInd``. - Each :n:`@ident__i` is a different mutually defined function - name (the names must be in the same order as when they were defined). This - command generates the induction principle for each :n:`@ident__i`, following - the recursive structure and case analyses of the corresponding function - :n:`@ident__i'`. - -.. warning:: - - There is a difference between induction schemes generated by the command - :cmd:`Functional Scheme` and these generated by the :cmd:`Function`. Indeed, - :cmd:`Function` generally produces smaller principles that are closer to how - a user would implement them. See :ref:`advanced-recursive-functions` for details. - -.. example:: - - Induction scheme for div2. - - We define the function div2 as follows: - - .. coqtop:: all - - Require Import FunInd. - Require Import Arith. - - Fixpoint div2 (n:nat) : nat := - match n with - | O => 0 - | S O => 0 - | S (S n') => S (div2 n') - end. - - The definition of a principle of induction corresponding to the - recursive structure of `div2` is defined by the command: - - .. coqtop:: all - - Functional Scheme div2_ind := Induction for div2 Sort Prop. - - You may now look at the type of div2_ind: - - .. coqtop:: all - - Check div2_ind. - - We can now prove the following lemma using this principle: - - .. coqtop:: all - - Lemma div2_le' : forall n:nat, div2 n <= n. - intro n. - pattern n, (div2 n). - apply div2_ind; intros. - auto with arith. - auto with arith. - simpl; auto with arith. - Qed. - - We can use directly the functional induction (:tacn:`function induction`) tactic instead - of the pattern/apply trick: - - .. coqtop:: all - - Reset div2_le'. - - Lemma div2_le : forall n:nat, div2 n <= n. - intro n. - functional induction (div2 n). - auto with arith. - auto with arith. - auto with arith. - Qed. - -.. example:: - - Induction scheme for tree_size. - - We define trees by the following mutual inductive type: - - .. original LaTeX had "Variable" instead of "Axiom", which generates an ugly warning - - .. coqtop:: reset all - - Axiom A : Set. - - Inductive tree : Set := - node : A -> forest -> tree - with forest : Set := - | empty : forest - | cons : tree -> forest -> forest. - - We define the function tree_size that computes the size of a tree or a - forest. Note that we use ``Function`` which generally produces better - principles. - - .. coqtop:: all - - Require Import FunInd. - - Function tree_size (t:tree) : nat := - match t with - | node A f => S (forest_size f) - end - with forest_size (f:forest) : nat := - match f with - | empty => 0 - | cons t f' => (tree_size t + forest_size f') - end. - - Notice that the induction principles ``tree_size_ind`` and ``forest_size_ind`` - generated by ``Function`` are not mutual. - - .. coqtop:: all - - Check tree_size_ind. - - Mutual induction principles following the recursive structure of ``tree_size`` - and ``forest_size`` can be generated by the following command: - - .. coqtop:: all - - Functional Scheme tree_size_ind2 := Induction for tree_size Sort Prop - with forest_size_ind2 := Induction for forest_size Sort Prop. - - You may now look at the type of `tree_size_ind2`: - - .. coqtop:: all - - Check tree_size_ind2. diff --git a/doc/sphinx/using/libraries/funind.rst b/doc/sphinx/using/libraries/funind.rst new file mode 100644 index 0000000000..7917f49ef5 --- /dev/null +++ b/doc/sphinx/using/libraries/funind.rst @@ -0,0 +1,140 @@ +.. _functional-scheme: + +Generation of induction principles with ``Functional`` ``Scheme`` +----------------------------------------------------------------- + + +.. cmd:: Functional Scheme @ident__0 := Induction for @ident' Sort @sort {* with @ident__i := Induction for @ident__i' Sort @sort} + + This command is a high-level experimental tool for + generating automatically induction principles corresponding to + (possibly mutually recursive) functions. First, it must be made + available via ``Require Import FunInd``. + Each :n:`@ident__i` is a different mutually defined function + name (the names must be in the same order as when they were defined). This + command generates the induction principle for each :n:`@ident__i`, following + the recursive structure and case analyses of the corresponding function + :n:`@ident__i'`. + +.. warning:: + + There is a difference between induction schemes generated by the command + :cmd:`Functional Scheme` and these generated by the :cmd:`Function`. Indeed, + :cmd:`Function` generally produces smaller principles that are closer to how + a user would implement them. See :ref:`advanced-recursive-functions` for details. + +.. example:: + + Induction scheme for div2. + + We define the function div2 as follows: + + .. coqtop:: all + + Require Import FunInd. + Require Import Arith. + + Fixpoint div2 (n:nat) : nat := + match n with + | O => 0 + | S O => 0 + | S (S n') => S (div2 n') + end. + + The definition of a principle of induction corresponding to the + recursive structure of `div2` is defined by the command: + + .. coqtop:: all + + Functional Scheme div2_ind := Induction for div2 Sort Prop. + + You may now look at the type of div2_ind: + + .. coqtop:: all + + Check div2_ind. + + We can now prove the following lemma using this principle: + + .. coqtop:: all + + Lemma div2_le' : forall n:nat, div2 n <= n. + intro n. + pattern n, (div2 n). + apply div2_ind; intros. + auto with arith. + auto with arith. + simpl; auto with arith. + Qed. + + We can use directly the functional induction (:tacn:`function induction`) tactic instead + of the pattern/apply trick: + + .. coqtop:: all + + Reset div2_le'. + + Lemma div2_le : forall n:nat, div2 n <= n. + intro n. + functional induction (div2 n). + auto with arith. + auto with arith. + auto with arith. + Qed. + +.. example:: + + Induction scheme for tree_size. + + We define trees by the following mutual inductive type: + + .. original LaTeX had "Variable" instead of "Axiom", which generates an ugly warning + + .. coqtop:: reset all + + Axiom A : Set. + + Inductive tree : Set := + node : A -> forest -> tree + with forest : Set := + | empty : forest + | cons : tree -> forest -> forest. + + We define the function tree_size that computes the size of a tree or a + forest. Note that we use ``Function`` which generally produces better + principles. + + .. coqtop:: all + + Require Import FunInd. + + Function tree_size (t:tree) : nat := + match t with + | node A f => S (forest_size f) + end + with forest_size (f:forest) : nat := + match f with + | empty => 0 + | cons t f' => (tree_size t + forest_size f') + end. + + Notice that the induction principles ``tree_size_ind`` and ``forest_size_ind`` + generated by ``Function`` are not mutual. + + .. coqtop:: all + + Check tree_size_ind. + + Mutual induction principles following the recursive structure of ``tree_size`` + and ``forest_size`` can be generated by the following command: + + .. coqtop:: all + + Functional Scheme tree_size_ind2 := Induction for tree_size Sort Prop + with forest_size_ind2 := Induction for forest_size Sort Prop. + + You may now look at the type of `tree_size_ind2`: + + .. coqtop:: all + + Check tree_size_ind2. -- cgit v1.2.3 From 34b5d2cf4383bd0cd89a1f896711dd4ac86decc0 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Mon, 20 Apr 2020 18:11:51 +0200 Subject: Remove Functional Scheme from Scheme chapter. --- doc/sphinx/user-extensions/proof-schemes.rst | 141 +-------------------------- 1 file changed, 1 insertion(+), 140 deletions(-) (limited to 'doc') diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst index 34197c4fcf..e05be7c2c2 100644 --- a/doc/sphinx/user-extensions/proof-schemes.rst +++ b/doc/sphinx/user-extensions/proof-schemes.rst @@ -190,146 +190,7 @@ Combined Scheme Check tree_forest_mutrect. -.. _functional-scheme: - -Generation of induction principles with ``Functional`` ``Scheme`` ------------------------------------------------------------------ - - -.. cmd:: Functional Scheme @ident__0 := Induction for @ident' Sort @sort {* with @ident__i := Induction for @ident__i' Sort @sort} - - This command is a high-level experimental tool for - generating automatically induction principles corresponding to - (possibly mutually recursive) functions. First, it must be made - available via ``Require Import FunInd``. - Each :n:`@ident__i` is a different mutually defined function - name (the names must be in the same order as when they were defined). This - command generates the induction principle for each :n:`@ident__i`, following - the recursive structure and case analyses of the corresponding function - :n:`@ident__i'`. - -.. warning:: - - There is a difference between induction schemes generated by the command - :cmd:`Functional Scheme` and these generated by the :cmd:`Function`. Indeed, - :cmd:`Function` generally produces smaller principles that are closer to how - a user would implement them. See :ref:`advanced-recursive-functions` for details. - -.. example:: - - Induction scheme for div2. - - We define the function div2 as follows: - - .. coqtop:: all - - Require Import FunInd. - Require Import Arith. - - Fixpoint div2 (n:nat) : nat := - match n with - | O => 0 - | S O => 0 - | S (S n') => S (div2 n') - end. - - The definition of a principle of induction corresponding to the - recursive structure of `div2` is defined by the command: - - .. coqtop:: all - - Functional Scheme div2_ind := Induction for div2 Sort Prop. - - You may now look at the type of div2_ind: - - .. coqtop:: all - - Check div2_ind. - - We can now prove the following lemma using this principle: - - .. coqtop:: all - - Lemma div2_le' : forall n:nat, div2 n <= n. - intro n. - pattern n, (div2 n). - apply div2_ind; intros. - auto with arith. - auto with arith. - simpl; auto with arith. - Qed. - - We can use directly the functional induction (:tacn:`function induction`) tactic instead - of the pattern/apply trick: - - .. coqtop:: all - - Reset div2_le'. - - Lemma div2_le : forall n:nat, div2 n <= n. - intro n. - functional induction (div2 n). - auto with arith. - auto with arith. - auto with arith. - Qed. - -.. example:: - - Induction scheme for tree_size. - - We define trees by the following mutual inductive type: - - .. original LaTeX had "Variable" instead of "Axiom", which generates an ugly warning - - .. coqtop:: reset all - - Axiom A : Set. - - Inductive tree : Set := - node : A -> forest -> tree - with forest : Set := - | empty : forest - | cons : tree -> forest -> forest. - - We define the function tree_size that computes the size of a tree or a - forest. Note that we use ``Function`` which generally produces better - principles. - - .. coqtop:: all - - Require Import FunInd. - - Function tree_size (t:tree) : nat := - match t with - | node A f => S (forest_size f) - end - with forest_size (f:forest) : nat := - match f with - | empty => 0 - | cons t f' => (tree_size t + forest_size f') - end. - - Notice that the induction principles ``tree_size_ind`` and ``forest_size_ind`` - generated by ``Function`` are not mutual. - - .. coqtop:: all - - Check tree_size_ind. - - Mutual induction principles following the recursive structure of ``tree_size`` - and ``forest_size`` can be generated by the following command: - - .. coqtop:: all - - Functional Scheme tree_size_ind2 := Induction for tree_size Sort Prop - with forest_size_ind2 := Induction for forest_size Sort Prop. - - You may now look at the type of `tree_size_ind2`: - - .. coqtop:: all - - Check tree_size_ind2. +.. seealso:: :ref:`functional-scheme` .. _derive-inversion: -- cgit v1.2.3 From ff9a3c625766a3069b7ffcbeb5592050838c8222 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Tue, 21 Apr 2020 16:39:15 +0200 Subject: Remove everything in the Tactics chapter up-to function induction and a bit beyond. --- doc/sphinx/proof-engine/tactics.rst | 2664 ----------------------------------- 1 file changed, 2664 deletions(-) (limited to 'doc') diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 19573eee43..f2c662e053 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -1,2104 +1,3 @@ -.. _tactics: - -Tactics -======== - -A deduction rule is a link between some (unique) formula, that we call -the *conclusion* and (several) formulas that we call the *premises*. A -deduction rule can be read in two ways. The first one says: “if I know -this and this then I can deduce this”. For instance, if I have a proof -of A and a proof of B then I have a proof of A ∧ B. This is forward -reasoning from premises to conclusion. The other way says: “to prove -this I have to prove this and this”. For instance, to prove A ∧ B, I -have to prove A and I have to prove B. This is backward reasoning from -conclusion to premises. We say that the conclusion is the *goal* to -prove and premises are the *subgoals*. The tactics implement *backward -reasoning*. When applied to a goal, a tactic replaces this goal with -the subgoals it generates. We say that a tactic reduces a goal to its -subgoal(s). - -Each (sub)goal is denoted with a number. The current goal is numbered -1. By default, a tactic is applied to the current goal, but one can -address a particular goal in the list by writing n:tactic which means -“apply tactic tactic to goal number n”. We can show the list of -subgoals by typing Show (see Section :ref:`requestinginformation`). - -Since not every rule applies to a given statement, not every tactic can -be used to reduce a given goal. In other words, before applying a tactic -to a given goal, the system checks that some *preconditions* are -satisfied. If it is not the case, the tactic raises an error message. - -Tactics are built from atomic tactics and tactic expressions (which -extends the folklore notion of tactical) to combine those atomic -tactics. This chapter is devoted to atomic tactics. The tactic -language will be described in Chapter :ref:`ltac`. - -Common elements of tactics --------------------------- - -.. _invocation-of-tactics: - -Invocation of tactics -~~~~~~~~~~~~~~~~~~~~~ - -A tactic is applied as an ordinary command. It may be preceded by a -goal selector (see Section :ref:`ltac-semantics`). If no selector is -specified, the default selector is used. - -.. _tactic_invocation_grammar: - - .. productionlist:: sentence - tactic_invocation : `toplevel_selector` : `tactic`. - : `tactic`. - -.. opt:: Default Goal Selector "@toplevel_selector" - :name: Default Goal Selector - - This option controls the default selector, used when no selector is - specified when applying a tactic. The initial value is 1, hence the - tactics are, by default, applied to the first goal. - - Using value ``all`` will make it so that tactics are, by default, - applied to every goal simultaneously. Then, to apply a tactic tac - to the first goal only, you can write ``1:tac``. - - Using value ``!`` enforces that all tactics are used either on a - single focused goal or with a local selector (’’strict focusing - mode’’). - - Although more selectors are available, only ``all``, ``!`` or a - single natural number are valid default goal selectors. - -.. _bindingslist: - -Bindings list -~~~~~~~~~~~~~ - -Tactics that take a term as an argument may also support a bindings list -to instantiate some parameters of the term by name or position. -The general form of a term with a bindings list is -:n:`@term with @bindings_list` where :token:`bindings_list` can take two different forms: - -.. _bindings_list_grammar: - - .. productionlist:: bindings_list - ref : `ident` - : `num` - bindings_list : (`ref` := `term`) ... (`ref` := `term`) - : `term` ... `term` - -+ In a bindings list of the form :n:`{+ (@ref:= @term)}`, :n:`@ref` is either an - :n:`@ident` or a :n:`@num`. The references are determined according to the type of - :n:`@term`. If :n:`@ref` is an identifier, this identifier has to be bound in the - type of :n:`@term` and the binding provides the tactic with an instance for the - parameter of this name. If :n:`@ref` is a number ``n``, it refers to - the ``n``-th non dependent premise of the :n:`@term`, as determined by the type - of :n:`@term`. - - .. exn:: No such binder. - :undocumented: - -+ A bindings list can also be a simple list of terms :n:`{* @term}`. - In that case the references to which these terms correspond are - determined by the tactic. In case of :tacn:`induction`, :tacn:`destruct`, :tacn:`elim` - and :tacn:`case`, the terms have to - provide instances for all the dependent products in the type of term while in - the case of :tacn:`apply`, or of :tacn:`constructor` and its variants, only instances - for the dependent products that are not bound in the conclusion of the type - are required. - - .. exn:: Not the right number of missing arguments. - :undocumented: - -.. _intropatterns: - -Intro patterns -~~~~~~~~~~~~~~ - -Intro patterns let you specify the name to assign to variables and hypotheses -introduced by tactics. They also let you split an introduced hypothesis into -multiple hypotheses or subgoals. Common tactics that accept intro patterns -include :tacn:`assert`, :tacn:`intros` and :tacn:`destruct`. - -.. productionlist:: coq - intropattern_list : `intropattern` ... `intropattern` - : `empty` - empty : - intropattern : * - : ** - : `simple_intropattern` - simple_intropattern : `simple_intropattern_closed` [ % `term` ... % `term` ] - simple_intropattern_closed : `naming_intropattern` - : _ - : `or_and_intropattern` - : `rewriting_intropattern` - : `injection_intropattern` - naming_intropattern : `ident` - : ? - : ?`ident` - or_and_intropattern : [ `intropattern_list` | ... | `intropattern_list` ] - : ( `simple_intropattern` , ... , `simple_intropattern` ) - : ( `simple_intropattern` & ... & `simple_intropattern` ) - rewriting_intropattern : -> - : <- - injection_intropattern : [= `intropattern_list` ] - or_and_intropattern_loc : `or_and_intropattern` - : `ident` - -Note that the intro pattern syntax varies between tactics. -Most tactics use :n:`@simple_intropattern` in the grammar. -:tacn:`destruct`, :tacn:`edestruct`, :tacn:`induction`, -:tacn:`einduction`, :tacn:`case`, :tacn:`ecase` and the various -:tacn:`inversion` tactics use :n:`@or_and_intropattern_loc`, while -:tacn:`intros` and :tacn:`eintros` use :n:`@intropattern_list`. -The :n:`eqn:` construct in various tactics uses :n:`@naming_intropattern`. - -**Naming patterns** - -Use these elementary patterns to specify a name: - -* :n:`@ident` — use the specified name -* :n:`?` — let Coq choose a name -* :n:`?@ident` — generate a name that begins with :n:`@ident` -* :n:`_` — discard the matched part (unless it is required for another - hypothesis) -* if a disjunction pattern omits a name, such as :g:`[|H2]`, Coq will choose a name - -**Splitting patterns** - -The most common splitting patterns are: - -* split a hypothesis in the form :n:`A /\ B` into two - hypotheses :g:`H1: A` and :g:`H2: B` using the pattern :g:`(H1 & H2)` or - :g:`(H1, H2)` or :g:`[H1 H2]`. - :ref:`Example `. This also works on :n:`A <-> B`, which - is just a notation representing :n:`(A -> B) /\ (B -> A)`. -* split a hypothesis in the form :g:`A \/ B` into two - subgoals using the pattern :g:`[H1|H2]`. The first subgoal will have the hypothesis - :g:`H1: A` and the second subgoal will have the hypothesis :g:`H2: B`. - :ref:`Example ` -* split a hypothesis in either of the forms :g:`A /\ B` or :g:`A \/ B` using the pattern :g:`[]`. - -Patterns can be nested: :n:`[[Ha|Hb] H]` can be used to split :n:`(A \/ B) /\ C`. - -Note that there is no equivalent to intro patterns for goals. For a goal :g:`A /\ B`, -use the :tacn:`split` tactic to replace the current goal with subgoals :g:`A` and :g:`B`. -For a goal :g:`A \/ B`, use :tacn:`left` to replace the current goal with :g:`A`, or -:tacn:`right` to replace the current goal with :g:`B`. - -* :n:`( {+, @simple_intropattern}` ) — matches - a product over an inductive type with a - :ref:`single constructor `. - If the number of patterns - equals the number of constructor arguments, then it applies the patterns only to - the arguments, and - :n:`( {+, @simple_intropattern} )` is equivalent to :n:`[{+ @simple_intropattern}]`. - If the number of patterns equals the number of constructor arguments plus the number - of :n:`let-ins`, the patterns are applied to the arguments and :n:`let-in` variables. - -* :n:`( {+& @simple_intropattern} )` — matches a right-hand nested term that consists - of one or more nested binary inductive types such as :g:`a1 OP1 a2 OP2 ...` - (where the :g:`OPn` are right-associative). - (If the :g:`OPn` are left-associative, additional parentheses will be needed to make the - term right-hand nested, such as :g:`a1 OP1 (a2 OP2 ...)`.) - The splitting pattern can have more than 2 names, for example :g:`(H1 & H2 & H3)` - matches :g:`A /\ B /\ C`. - The inductive types must have a - :ref:`single constructor with two parameters `. - :ref:`Example ` - -* :n:`[ {+| @intropattern_list} ]` — splits an inductive type that has - :ref:`multiple constructors ` - such as :n:`A \/ B` - into multiple subgoals. The number of :token:`intropattern_list` must be the same as the number of - constructors for the matched part. -* :n:`[ {+ @intropattern} ]` — splits an inductive type that has a - :ref:`single constructor with multiple parameters ` - such as :n:`A /\ B` into multiple hypotheses. Use :n:`[H1 [H2 H3]]` to match :g:`A /\ B /\ C`. -* :n:`[]` — splits an inductive type: If the inductive - type has multiple constructors, such as :n:`A \/ B`, - create one subgoal for each constructor. If the inductive type has a single constructor with - multiple parameters, such as :n:`A /\ B`, split it into multiple hypotheses. - -**Equality patterns** - -These patterns can be used when the hypothesis is an equality: - -* :n:`->` — replaces the right-hand side of the hypothesis with the left-hand - side of the hypothesis in the conclusion of the goal; the hypothesis is - cleared; if the left-hand side of the hypothesis is a variable, it is - substituted everywhere in the context and the variable is removed. - :ref:`Example ` -* :n:`<-` — similar to :n:`->`, but replaces the left-hand side of the hypothesis - with the right-hand side of the hypothesis. -* :n:`[= {*, @intropattern} ]` — If the product is over an equality type, - applies either :tacn:`injection` or :tacn:`discriminate`. - If :tacn:`injection` is applicable, the intropattern - is used on the hypotheses generated by :tacn:`injection`. If the - number of patterns is smaller than the number of hypotheses generated, the - pattern :n:`?` is used to complete the list. - :ref:`Example ` - -**Other patterns** - -* :n:`*` — introduces one or more quantified variables from the result - until there are no more quantified variables. - :ref:`Example ` - -* :n:`**` — introduces one or more quantified variables or hypotheses from the result until there are - no more quantified variables or implications (:g:`->`). :g:`intros **` is equivalent - to :g:`intros`. - :ref:`Example ` - -* :n:`@simple_intropattern_closed {* % @term}` — first applies each of the terms - with the :tacn:`apply ... in` tactic on the hypothesis to be introduced, then it uses - :n:`@simple_intropattern_closed`. - :ref:`Example ` - -.. flag:: Bracketing Last Introduction Pattern - - For :n:`intros @intropattern_list`, controls how to handle a - conjunctive pattern that doesn't give enough simple patterns to match - all the arguments in the constructor. If set (the default), |Coq| generates - additional names to match the number of arguments. - Unsetting the flag will put the additional hypotheses in the goal instead, behavior that is more - similar to |SSR|'s intro patterns. - - .. deprecated:: 8.10 - -.. _intropattern_cons_note: - -.. note:: - - :n:`A \/ B` and :n:`A /\ B` use infix notation to refer to the inductive - types :n:`or` and :n:`and`. - :n:`or` has multiple constructors (:n:`or_introl` and :n:`or_intror`), - while :n:`and` has a single constructor (:n:`conj`) with multiple parameters - (:n:`A` and :n:`B`). - These are defined in ``theories/Init/Logic.v``. The "where" clauses define the - infix notation for "or" and "and". - - .. coqdoc:: - - Inductive or (A B:Prop) : Prop := - | or_introl : A -> A \/ B - | or_intror : B -> A \/ B - where "A \/ B" := (or A B) : type_scope. - - Inductive and (A B:Prop) : Prop := - conj : A -> B -> A /\ B - where "A /\ B" := (and A B) : type_scope. - -.. note:: - - :n:`intros {+ p}` is not always equivalent to :n:`intros p; ... ; intros p` - if some of the :n:`p` are :g:`_`. In the first form, all erasures are done - at once, while they're done sequentially for each tactic in the second form. - If the second matched term depends on the first matched term and the pattern - for both is :g:`_` (i.e., both will be erased), the first :n:`intros` in the second - form will fail because the second matched term still has the dependency on the first. - -Examples: - -.. _intropattern_conj_ex: - - .. example:: intro pattern for /\\ - - .. coqtop:: reset none - - Goal forall (A: Prop) (B: Prop), (A /\ B) -> True. - - .. coqtop:: out - - intros. - - .. coqtop:: all - - destruct H as (HA & HB). - -.. _intropattern_disj_ex: - - .. example:: intro pattern for \\/ - - .. coqtop:: reset none - - Goal forall (A: Prop) (B: Prop), (A \/ B) -> True. - - .. coqtop:: out - - intros. - - .. coqtop:: all - - destruct H as [HA|HB]. all: swap 1 2. - -.. _intropattern_rarrow_ex: - - .. example:: -> intro pattern - - .. coqtop:: reset none - - Goal forall (x:nat) (y:nat) (z:nat), (x = y) -> (y = z) -> (x = z). - - .. coqtop:: out - - intros * H. - - .. coqtop:: all - - intros ->. - -.. _intropattern_inj_discr_ex: - - .. example:: [=] intro pattern - - The first :n:`intros [=]` uses :tacn:`injection` to strip :n:`(S ...)` from - both sides of the matched equality. The second uses :tacn:`discriminate` on - the contradiction :n:`1 = 2` (internally represented as :n:`(S O) = (S (S O))`) - to complete the goal. - - .. coqtop:: reset none - - Goal forall (n m:nat), (S n) = (S m) -> (S O)=(S (S O)) -> False. - - .. coqtop:: out - - intros *. - - .. coqtop:: all - - intros [= H]. - - .. coqtop:: all - - intros [=]. - -.. _intropattern_ampersand_ex: - - .. example:: (A & B & ...) intro pattern - - .. coqtop:: reset none - - Parameters (A : Prop) (B: nat -> Prop) (C: Prop). - - .. coqtop:: out - - Goal A /\ (exists x:nat, B x /\ C) -> True. - - .. coqtop:: all - - intros (a & x & b & c). - -.. _intropattern_star_ex: - - .. example:: * intro pattern - - .. coqtop:: reset out - - Goal forall (A: Prop) (B: Prop), A -> B. - - .. coqtop:: all - - intros *. - -.. _intropattern_2stars_ex: - - .. example:: ** pattern ("intros \**" is equivalent to "intros") - - .. coqtop:: reset out - - Goal forall (A: Prop) (B: Prop), A -> B. - - .. coqtop:: all - - intros **. - - .. example:: compound intro pattern - - .. coqtop:: reset out - - Goal forall A B C:Prop, A \/ B /\ C -> (A -> C) -> C. - - .. coqtop:: all - - intros * [a | (_,c)] f. - all: swap 1 2. - -.. _intropattern_injection_ex: - - .. example:: combined intro pattern using [=] -> and % - - .. coqtop:: reset none - - Require Import Coq.Lists.List. - Section IntroPatterns. - Variables (A : Type) (xs ys : list A). - - .. coqtop:: out - - Example ThreeIntroPatternsCombined : - S (length ys) = 1 -> xs ++ ys = xs. - - .. coqtop:: all - - intros [=->%length_zero_iff_nil]. - - * `intros` would add :g:`H : S (length ys) = 1` - * `intros [=]` would additionally apply :tacn:`injection` to :g:`H` to yield :g:`H0 : length ys = 0` - * `intros [=->%length_zero_iff_nil]` applies the theorem, making H the equality :g:`l=nil`, - which is then applied as for :g:`->`. - - .. coqdoc:: - - Theorem length_zero_iff_nil (l : list A): - length l = 0 <-> l=nil. - - The example is based on `Tej Chajed's coq-tricks `_ - -.. _occurrencessets: - -Occurrence sets and occurrence clauses -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -An occurrence clause is a modifier to some tactics that obeys the -following syntax: - - .. productionlist:: coq - occurrence_clause : in `goal_occurrences` - goal_occurrences : [`ident` [`at_occurrences`], ... , `ident` [`at_occurrences`] [|- [* [`at_occurrences`]]]] - : * |- [* [`at_occurrences`]] - : * - at_occurrences : at `occurrences` - occurrences : [-] `num` ... `num` - -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`. - - -.. seealso:: - - :ref:`Managingthelocalcontext`, :ref:`caseanalysisandinduction`, - :ref:`printing_constructions_full`. - - -.. _applyingtheorems: - -Applying theorems ---------------------- - -.. tacn:: exact @term - :name: exact - - This tactic applies to any goal. It gives directly the exact proof - term of the goal. Let ``T`` be our goal, let ``p`` be a term of type ``U`` then - ``exact p`` succeeds iff ``T`` and ``U`` are convertible (see - :ref:`Conversion-rules`). - - .. exn:: Not an exact proof. - :undocumented: - - .. tacv:: eexact @term. - :name: eexact - - This tactic behaves like :tacn:`exact` but is able to handle terms and - goals with existential variables. - -.. tacn:: assumption - :name: assumption - - This tactic looks in the local context for a hypothesis whose type is - convertible to the goal. If it is the case, the subgoal is proved. - Otherwise, it fails. - - .. exn:: No such assumption. - :undocumented: - - .. tacv:: eassumption - :name: eassumption - - This tactic behaves like :tacn:`assumption` but is able to handle - goals with existential variables. - -.. tacn:: refine @term - :name: refine - - This tactic applies to any goal. It behaves like :tacn:`exact` with a big - difference: the user can leave some holes (denoted by ``_`` - or :n:`(_ : @type)`) in the term. :tacn:`refine` will generate as many - subgoals as there are remaining holes in the elaborated term. The type - of holes must be either synthesized by the system or declared by an explicit cast - like ``(_ : nat -> Prop)``. Any subgoal that - occurs in other subgoals is automatically shelved, as if calling - :tacn:`shelve_unifiable`. The produced subgoals (shelved or not) - are *not* candidates for typeclass resolution, even if they have a type-class - type as conclusion, letting the user control when and how typeclass resolution - is launched on them. This low-level tactic can be useful to advanced users. - - .. example:: - - .. coqtop:: reset all - - Inductive Option : Set := - | Fail : Option - | Ok : bool -> Option. - - Definition get : forall x:Option, x <> Fail -> bool. - refine - (fun x:Option => - match x return x <> Fail -> bool with - | Fail => _ - | Ok b => fun _ => b - end). - intros; absurd (Fail = Fail); trivial. - Defined. - - .. exn:: Invalid argument. - - The tactic :tacn:`refine` does not know what to do with the term you gave. - - .. exn:: Refine passed ill-formed term. - - The term you gave is not a valid proof (not easy to debug in general). This - message may also occur in higher-level tactics that call :tacn:`refine` - internally. - - .. exn:: Cannot infer a term for this placeholder. - :name: Cannot infer a term for this placeholder. (refine) - - There is a hole in the term you gave whose type cannot be inferred. Put a - cast around it. - - .. tacv:: simple refine @term - :name: simple refine - - This tactic behaves like refine, but it does not shelve any subgoal. It does - not perform any beta-reduction either. - - .. tacv:: notypeclasses refine @term - :name: notypeclasses refine - - This tactic behaves like :tacn:`refine` except it performs type checking without - resolution of typeclasses. - - .. tacv:: simple notypeclasses refine @term - :name: simple notypeclasses refine - - This tactic behaves like the combination of :tacn:`simple refine` and - :tacn:`notypeclasses refine`: it performs type checking without resolution of - typeclasses, does not perform beta reductions or shelve the subgoals. - - .. flag:: Debug Unification - - Enables printing traces of unification steps used during - elaboration/typechecking and the :tacn:`refine` tactic. - -.. tacn:: apply @term - :name: apply - - This tactic applies to any goal. The argument term is a term well-formed in - the local context. The tactic :tacn:`apply` tries to match the current goal - against the conclusion of the type of :token:`term`. If it succeeds, then - the tactic returns as many subgoals as the number of non-dependent premises - of the type of term. If the conclusion of the type of :token:`term` does - not match the goal *and* the conclusion is an inductive type isomorphic to - a tuple type, then each component of the tuple is recursively matched to - the goal in the left-to-right order. - - The tactic :tacn:`apply` relies on first-order unification with dependent - types unless the conclusion of the type of :token:`term` is of the form - :n:`P (t__1 ... t__n)` with ``P`` to be instantiated. In the latter case, - the behavior depends on the form of the goal. If the goal is of the form - :n:`(fun x => Q) u__1 ... u__n` and the :n:`t__i` and :n:`u__i` unify, - then :g:`P` is taken to be :g:`(fun x => Q)`. Otherwise, :tacn:`apply` - tries to define :g:`P` by abstracting over :g:`t_1 ... t__n` in the goal. - See :tacn:`pattern` to transform the goal so that it - gets the form :n:`(fun x => Q) u__1 ... u__n`. - - .. exn:: Unable to unify @term with @term. - - The :tacn:`apply` tactic failed to match the conclusion of :token:`term` - and the current goal. You can help the :tacn:`apply` tactic by - transforming your goal with the :tacn:`change` or :tacn:`pattern` - tactics. - - .. exn:: Unable to find an instance for the variables {+ @ident}. - - This occurs when some instantiations of the premises of :token:`term` are not deducible - from the unification. This is the case, for instance, when you want to apply a - transitivity property. In this case, you have to use one of the variants below: - - .. tacv:: apply @term with {+ @term} - - Provides apply with explicit instantiations for all dependent premises of the - type of term that do not occur in the conclusion and consequently cannot be - found by unification. Notice that the collection :n:`{+ @term}` must be given - according to the order of these dependent premises of the type of term. - - .. exn:: Not the right number of missing arguments. - :undocumented: - - .. tacv:: apply @term with @bindings_list - - This also provides apply with values for instantiating premises. Here, variables - are referred by names and non-dependent products by increasing numbers (see - :ref:`bindings list `). - - .. tacv:: apply {+, @term} - - This is a shortcut for :n:`apply @term__1; [.. | ... ; [ .. | apply @term__n] ... ]`, - i.e. for the successive applications of :n:`@term`:sub:`i+1` on the last subgoal - generated by :n:`apply @term__i` , starting from the application of :n:`@term__1`. - - .. tacv:: eapply @term - :name: eapply - - The tactic :tacn:`eapply` behaves like :tacn:`apply` but it does not fail when no - instantiations are deducible for some variables in the premises. Rather, it - turns these variables into existential variables which are variables still to - instantiate (see :ref:`Existential-Variables`). The instantiation is - intended to be found later in the proof. - - .. tacv:: rapply @term - :name: rapply - - The tactic :tacn:`rapply` behaves like :tacn:`eapply` but it - uses the proof engine of :tacn:`refine` for dealing with - existential variables, holes, and conversion problems. This may - result in slightly different behavior regarding which conversion - problems are solvable. However, like :tacn:`apply` but unlike - :tacn:`eapply`, :tacn:`rapply` will fail if there are any holes - which remain in :n:`@term` itself after typechecking and - typeclass resolution but before unification with the goal. More - technically, :n:`@term` is first parsed as a - :production:`constr` rather than as a :production:`uconstr` or - :production:`open_constr` before being applied to the goal. Note - that :tacn:`rapply` prefers to instantiate as many hypotheses of - :n:`@term` as possible. As a result, if it is possible to apply - :n:`@term` to arbitrarily many arguments without getting a type - error, :tacn:`rapply` will loop. - - Note that you need to :n:`Require Import Coq.Program.Tactics` to - make use of :tacn:`rapply`. - - .. tacv:: simple apply @term. - - This behaves like :tacn:`apply` but it reasons modulo conversion only on subterms - that contain no variables to instantiate. For instance, the following example - does not succeed because it would require the conversion of ``id ?foo`` and - :g:`O`. - - .. example:: - - .. coqtop:: all - - Definition id (x : nat) := x. - Parameter H : forall y, id y = y. - Goal O = O. - Fail simple apply H. - - Because it reasons modulo a limited amount of conversion, :tacn:`simple apply` fails - quicker than :tacn:`apply` and it is then well-suited for uses in user-defined - tactics that backtrack often. Moreover, it does not traverse tuples as :tacn:`apply` - does. - - .. tacv:: {? simple} apply {+, @term {? with @bindings_list}} - {? simple} eapply {+, @term {? with @bindings_list}} - :name: simple apply; simple eapply - - This summarizes the different syntaxes for :tacn:`apply` and :tacn:`eapply`. - - .. tacv:: lapply @term - :name: lapply - - This tactic applies to any goal, say :g:`G`. The argument term has to be - well-formed in the current context, its type being reducible to a non-dependent - product :g:`A -> B` with :g:`B` possibly containing products. Then it generates - two subgoals :g:`B->G` and :g:`A`. Applying ``lapply H`` (where :g:`H` has type - :g:`A->B` and :g:`B` does not start with a product) does the same as giving the - sequence ``cut B. 2:apply H.`` where ``cut`` is described below. - - .. warn:: When @term contains more than one non dependent product the tactic lapply only takes into account the first product. - :undocumented: - -.. example:: - - Assume we have a transitive relation ``R`` on ``nat``: - - .. coqtop:: reset in - - Parameter R : nat -> nat -> Prop. - - Axiom Rtrans : forall x y z:nat, R x y -> R y z -> R x z. - - Parameters n m p : nat. - - Axiom Rnm : R n m. - - Axiom Rmp : R m p. - - Consider the goal ``(R n p)`` provable using the transitivity of ``R``: - - .. coqtop:: in - - Goal R n p. - - The direct application of ``Rtrans`` with ``apply`` fails because no value - for ``y`` in ``Rtrans`` is found by ``apply``: - - .. coqtop:: all fail - - apply Rtrans. - - A solution is to ``apply (Rtrans n m p)`` or ``(Rtrans n m)``. - - .. coqtop:: all - - apply (Rtrans n m p). - - Note that ``n`` can be inferred from the goal, so the following would work - too. - - .. coqtop:: in restart - - apply (Rtrans _ m). - - More elegantly, ``apply Rtrans with (y:=m)`` allows only mentioning the - unknown m: - - .. coqtop:: in restart - - apply Rtrans with (y := m). - - Another solution is to mention the proof of ``(R x y)`` in ``Rtrans`` - - .. coqtop:: all restart - - apply Rtrans with (1 := Rnm). - - ... or the proof of ``(R y z)``. - - .. coqtop:: all restart - - apply Rtrans with (2 := Rmp). - - On the opposite, one can use ``eapply`` which postpones the problem of - finding ``m``. Then one can apply the hypotheses ``Rnm`` and ``Rmp``. This - instantiates the existential variable and completes the proof. - - .. coqtop:: all restart abort - - eapply Rtrans. - - apply Rnm. - - apply Rmp. - -.. note:: - When the conclusion of the type of the term to ``apply`` is an inductive - type isomorphic to a tuple type and ``apply`` looks recursively whether a - component of the tuple matches the goal, it excludes components whose - statement would result in applying an universal lemma of the form - ``forall A, ... -> A``. Excluding this kind of lemma can be avoided by - setting the following flag: - -.. flag:: Universal Lemma Under Conjunction - - This flag, which preserves compatibility with versions of Coq prior to - 8.4 is also available for :n:`apply @term in @ident` (see :tacn:`apply ... in`). - -.. tacn:: apply @term in @ident - :name: apply ... in - - This tactic applies to any goal. The argument :token:`term` is a term - well-formed in the local context and the argument :token:`ident` is an - hypothesis of the context. - The tactic :n:`apply @term in @ident` tries to match the conclusion of the - type of :token:`ident` against a non-dependent premise of the type - of :token:`term`, trying them from right to left. If it succeeds, the - statement of hypothesis :token:`ident` is replaced by the conclusion of - the type of :token:`term`. The tactic also returns as many subgoals as the - number of other non-dependent premises in the type of :token:`term` and of - the non-dependent premises of the type of :token:`ident`. If the conclusion - of the type of :token:`term` does not match the goal *and* the conclusion - is an inductive type isomorphic to a tuple type, then - the tuple is (recursively) decomposed and the first component of the tuple - of which a non-dependent premise matches the conclusion of the type of - :token:`ident`. Tuples are decomposed in a width-first left-to-right order - (for instance if the type of :g:`H1` is :g:`A <-> B` and the type of - :g:`H2` is :g:`A` then :g:`apply H1 in H2` transforms the type of :g:`H2` - into :g:`B`). The tactic :tacn:`apply` relies on first-order pattern matching - with dependent types. - - .. exn:: Statement without assumptions. - - This happens if the type of :token:`term` has no non-dependent premise. - - .. exn:: Unable to apply. - - This happens if the conclusion of :token:`ident` does not match any of - the non-dependent premises of the type of :token:`term`. - - .. tacv:: apply {+, @term} in @ident - - This applies each :token:`term` in sequence in :token:`ident`. - - .. tacv:: apply {+, @term with @bindings_list} in @ident - - This does the same but uses the bindings in each :n:`(@ident := @term)` to - instantiate the parameters of the corresponding type of :token:`term` - (see :ref:`bindings list `). - - .. tacv:: eapply {+, @term {? with @bindings_list } } in @ident - - This works as :tacn:`apply ... in` but turns unresolved bindings into - existential variables, if any, instead of failing. - - .. tacv:: apply {+, @term {? with @bindings_list } } in @ident as @simple_intropattern - :name: apply ... in ... as - - This works as :tacn:`apply ... in` then applies the :token:`simple_intropattern` - to the hypothesis :token:`ident`. - - .. tacv:: simple apply @term in @ident - - This behaves like :tacn:`apply ... in` but it reasons modulo conversion - only on subterms that contain no variables to instantiate. For instance, - if :g:`id := fun x:nat => x` and :g:`H: forall y, id y = y -> True` and - :g:`H0 : O = O` then :g:`simple apply H in H0` does not succeed because it - would require the conversion of :g:`id ?x` and :g:`O` where :g:`?x` is - an existential variable to instantiate. - Tactic :n:`simple apply @term in @ident` does not - either traverse tuples as :n:`apply @term in @ident` does. - - .. tacv:: {? simple} apply {+, @term {? with @bindings_list}} in @ident {? as @simple_intropattern} - {? simple} eapply {+, @term {? with @bindings_list}} in @ident {? as @simple_intropattern} - - This summarizes the different syntactic variants of :n:`apply @term in @ident` - and :n:`eapply @term in @ident`. - -.. tacn:: constructor @num - :name: constructor - - This tactic applies to a goal such that its conclusion is an inductive - type (say :g:`I`). The argument :token:`num` must be less or equal to the - numbers of constructor(s) of :g:`I`. Let :n:`c__i` be the i-th - constructor of :g:`I`, then :g:`constructor i` is equivalent to - :n:`intros; apply c__i`. - - .. exn:: Not an inductive product. - :undocumented: - - .. exn:: Not enough constructors. - :undocumented: - - .. tacv:: constructor - - This tries :g:`constructor 1` then :g:`constructor 2`, ..., then - :g:`constructor n` where ``n`` is the number of constructors of the head - of the goal. - - .. tacv:: constructor @num with @bindings_list - - Let ``c`` be the i-th constructor of :g:`I`, then - :n:`constructor i with @bindings_list` is equivalent to - :n:`intros; apply c with @bindings_list`. - - .. warning:: - - The terms in the :token:`bindings_list` are checked in the context - where constructor is executed and not in the context where :tacn:`apply` - is executed (the introductions are not taken into account). - - .. tacv:: split {? with @bindings_list } - :name: split - - This applies only if :g:`I` has a single constructor. It is then - equivalent to :n:`constructor 1 {? with @bindings_list }`. It is - typically used in the case of a conjunction :math:`A \wedge B`. - - .. tacv:: exists @bindings_list - :name: exists - - This applies only if :g:`I` has a single constructor. It is then equivalent - to :n:`intros; constructor 1 with @bindings_list.` It is typically used in - the case of an existential quantification :math:`\exists x, P(x).` - - .. tacv:: exists {+, @bindings_list } - - This iteratively applies :n:`exists @bindings_list`. - - .. exn:: Not an inductive goal with 1 constructor. - :undocumented: - - .. tacv:: left {? with @bindings_list } - right {? with @bindings_list } - :name: left; right - - These tactics apply only if :g:`I` has two constructors, for - instance in the case of a disjunction :math:`A \vee B`. - Then, they are respectively equivalent to - :n:`constructor 1 {? with @bindings_list }` and - :n:`constructor 2 {? with @bindings_list }`. - - .. exn:: Not an inductive goal with 2 constructors. - :undocumented: - - .. tacv:: econstructor - eexists - esplit - eleft - eright - :name: econstructor; eexists; esplit; eleft; eright - - These tactics and their variants behave like :tacn:`constructor`, - :tacn:`exists`, :tacn:`split`, :tacn:`left`, :tacn:`right` and their - variants but they introduce existential variables instead of failing - when the instantiation of a variable cannot be found - (cf. :tacn:`eapply` and :tacn:`apply`). - -.. flag:: Debug Tactic Unification - - Enables printing traces of unification steps in tactic unification. - Tactic unification is used in tactics such as :tacn:`apply` and :tacn:`rewrite`. - -.. _managingthelocalcontext: - -Managing the local context ------------------------------- - -.. tacn:: intro - :name: intro - - This tactic applies to a goal that is either a product or starts with a - let-binder. If the goal is a product, the tactic implements the "Lam" rule - given in :ref:`Typing-rules` [1]_. If the goal starts with a let-binder, - then the tactic implements a mix of the "Let" and "Conv". - - If the current goal is a dependent product :g:`forall x:T, U` - (resp :g:`let x:=t in U`) then :tacn:`intro` puts :g:`x:T` (resp :g:`x:=t`) - in the local context. The new subgoal is :g:`U`. - - If the goal is a non-dependent product :math:`T \rightarrow U`, then it - puts in the local context either :g:`Hn:T` (if :g:`T` is of type :g:`Set` - or :g:`Prop`) or :g:`Xn:T` (if the type of :g:`T` is :g:`Type`). - The optional index ``n`` is such that ``Hn`` or ``Xn`` is a fresh - identifier. In both cases, the new subgoal is :g:`U`. - - If the goal is an existential variable, :tacn:`intro` forces the resolution - of the existential variable into a dependent product :math:`\forall`\ :g:`x:?X, ?Y`, - puts :g:`x:?X` in the local context and leaves :g:`?Y` as a new subgoal - allowed to depend on :g:`x`. - - The tactic :tacn:`intro` applies the tactic :tacn:`hnf` - until :tacn:`intro` can be applied or the goal is not head-reducible. - - .. exn:: No product even after head-reduction. - :undocumented: - - .. tacv:: intro @ident - - This applies :tacn:`intro` but forces :token:`ident` to be the name of - the introduced hypothesis. - - .. exn:: @ident is already used. - :undocumented: - - .. note:: - - If a name used by intro hides the base name of a global constant then - the latter can still be referred to by a qualified name - (see :ref:`Qualified-names`). - - .. tacv:: intros - :name: intros - - This repeats :tacn:`intro` until it meets the head-constant. It never - reduces head-constants and it never fails. - - .. tacv:: intros {+ @ident}. - - This is equivalent to the composed tactic :n:`intro @ident; ... ; intro @ident`. - - .. tacv:: intros until @ident - - This repeats intro until it meets a premise of the goal having the - form :n:`(@ident : @type)` and discharges the variable - named :token:`ident` of the current goal. - - .. exn:: No such hypothesis in current goal. - :undocumented: - - .. tacv:: intros until @num - - This repeats :tacn:`intro` until the :token:`num`\-th non-dependent - product. - - .. example:: - - On the subgoal :g:`forall x y : nat, x = y -> y = x` the - tactic :n:`intros until 1` is equivalent to :n:`intros x y H`, - as :g:`x = y -> y = x` is the first non-dependent product. - - On the subgoal :g:`forall x y z : nat, x = y -> y = x` the - tactic :n:`intros until 1` is equivalent to :n:`intros x y z` - as the product on :g:`z` can be rewritten as a non-dependent - product: :g:`forall x y : nat, nat -> x = y -> y = x`. - - .. exn:: No such hypothesis in current goal. - - This happens when :token:`num` is 0 or is greater than the number of - non-dependent products of the goal. - - .. tacv:: intro {? @ident__1 } after @ident__2 - intro {? @ident__1 } before @ident__2 - intro {? @ident__1 } at top - intro {? @ident__1 } at bottom - - These tactics apply :n:`intro {? @ident__1}` and move the freshly - introduced hypothesis respectively after the hypothesis :n:`@ident__2`, - before the hypothesis :n:`@ident__2`, at the top of the local context, - or at the bottom of the local context. All hypotheses on which the new - hypothesis depends are moved too so as to respect the order of - dependencies between hypotheses. It is equivalent to :n:`intro {? @ident__1 }` - followed by the appropriate call to :tacn:`move ... after ...`, - :tacn:`move ... before ...`, :tacn:`move ... at top`, - or :tacn:`move ... at bottom`. - - .. note:: - - :n:`intro at bottom` is a synonym for :n:`intro` with no argument. - - .. exn:: No such hypothesis: @ident. - :undocumented: - -.. tacn:: intros @intropattern_list - :name: intros ... - - Introduces one or more variables or hypotheses from the goal by matching the - intro patterns. See the description in :ref:`intropatterns`. - -.. tacn:: eintros @intropattern_list - :name: eintros - - Works just like :tacn:`intros ...` except that it creates existential variables - for any unresolved variables rather than failing. - -.. tacn:: clear @ident - :name: clear - - This tactic erases the hypothesis named :n:`@ident` in the local context of - the current goal. As a consequence, :n:`@ident` is no more displayed and no - more usable in the proof development. - - .. exn:: No such hypothesis. - :undocumented: - - .. exn:: @ident is used in the conclusion. - :undocumented: - - .. exn:: @ident is used in the hypothesis @ident. - :undocumented: - - .. tacv:: clear {+ @ident} - - This is equivalent to :n:`clear @ident. ... clear @ident.` - - .. tacv:: clear - {+ @ident} - - This variant clears all the hypotheses except the ones depending in the - hypotheses named :n:`{+ @ident}` and in the goal. - - .. tacv:: clear - - This variants clears all the hypotheses except the ones the goal depends on. - - .. tacv:: clear dependent @ident - - This clears the hypothesis :token:`ident` and all the hypotheses that - depend on it. - - .. tacv:: clearbody {+ @ident} - :name: clearbody - - This tactic expects :n:`{+ @ident}` to be local definitions and clears - their respective bodies. - In other words, it turns the given definitions into assumptions. - - .. exn:: @ident is not a local definition. - :undocumented: - -.. tacn:: revert {+ @ident} - :name: revert - - This applies to any goal with variables :n:`{+ @ident}`. It moves the hypotheses - (possibly defined) to the goal, if this respects dependencies. This tactic is - the inverse of :tacn:`intro`. - - .. exn:: No such hypothesis. - :undocumented: - - .. exn:: @ident__1 is used in the hypothesis @ident__2. - :undocumented: - - .. tacv:: revert dependent @ident - :name: revert dependent - - This moves to the goal the hypothesis :token:`ident` and all the - hypotheses that depend on it. - -.. tacn:: move @ident__1 after @ident__2 - :name: move ... after ... - - This moves the hypothesis named :n:`@ident__1` in the local context after - the hypothesis named :n:`@ident__2`, where “after” is in reference to the - direction of the move. The proof term is not changed. - - If :n:`@ident__1` comes before :n:`@ident__2` in the order of dependencies, - then all the hypotheses between :n:`@ident__1` and :n:`@ident__2` that - (possibly indirectly) depend on :n:`@ident__1` are moved too, and all of - them are thus moved after :n:`@ident__2` in the order of dependencies. - - If :n:`@ident__1` comes after :n:`@ident__2` in the order of dependencies, - then all the hypotheses between :n:`@ident__1` and :n:`@ident__2` that - (possibly indirectly) occur in the type of :n:`@ident__1` are moved too, - and all of them are thus moved before :n:`@ident__2` in the order of - dependencies. - - .. tacv:: move @ident__1 before @ident__2 - :name: move ... before ... - - This moves :n:`@ident__1` towards and just before the hypothesis - named :n:`@ident__2`. As for :tacn:`move ... after ...`, dependencies - over :n:`@ident__1` (when :n:`@ident__1` comes before :n:`@ident__2` in - the order of dependencies) or in the type of :n:`@ident__1` - (when :n:`@ident__1` comes after :n:`@ident__2` in the order of - dependencies) are moved too. - - .. tacv:: move @ident at top - :name: move ... at top - - This moves :token:`ident` at the top of the local context (at the beginning - of the context). - - .. tacv:: move @ident at bottom - :name: move ... at bottom - - This moves :token:`ident` at the bottom of the local context (at the end of - the context). - - .. exn:: No such hypothesis. - :undocumented: - - .. exn:: Cannot move @ident__1 after @ident__2: it occurs in the type of @ident__2. - :undocumented: - - .. exn:: Cannot move @ident__1 after @ident__2: it depends on @ident__2. - :undocumented: - - .. example:: - - .. coqtop:: reset all - - Goal forall x :nat, x = 0 -> forall z y:nat, y=y-> 0=x. - intros x H z y H0. - move x after H0. - Undo. - move x before H0. - Undo. - move H0 after H. - Undo. - move H0 before H. - -.. tacn:: rename @ident__1 into @ident__2 - :name: rename - - This renames hypothesis :n:`@ident__1` into :n:`@ident__2` in the current - context. The name of the hypothesis in the proof-term, however, is left - unchanged. - - .. tacv:: rename {+, @ident__i into @ident__j} - - This renames the variables :n:`@ident__i` into :n:`@ident__j` in parallel. - In particular, the target identifiers may contain identifiers that exist in - the source context, as long as the latter are also renamed by the same - tactic. - - .. exn:: No such hypothesis. - :undocumented: - - .. exn:: @ident is already used. - :undocumented: - -.. tacn:: set (@ident := @term) - :name: set - - This replaces :token:`term` by :token:`ident` in the conclusion of the - current goal and adds the new definition :n:`@ident := @term` to the - local context. - - If :token:`term` has holes (i.e. subexpressions of the form “`_`”), the - tactic first checks that all subterms matching the pattern are compatible - before doing the replacement using the leftmost subterm matching the - pattern. - - .. exn:: The variable @ident is already defined. - :undocumented: - - .. tacv:: set (@ident := @term) in @goal_occurrences - - This notation allows specifying which occurrences of :token:`term` have - to be substituted in the context. The :n:`in @goal_occurrences` clause - is an occurrence clause whose syntax and behavior are described in - :ref:`goal occurrences `. - - .. tacv:: set (@ident {* @binder } := @term) {? in @goal_occurrences } - - This is equivalent to :n:`set (@ident := fun {* @binder } => @term) {? in @goal_occurrences }`. - - .. tacv:: set @term {? in @goal_occurrences } - - This behaves as :n:`set (@ident := @term) {? in @goal_occurrences }` - but :token:`ident` is generated by Coq. - - .. tacv:: eset (@ident {* @binder } := @term) {? in @goal_occurrences } - eset @term {? in @goal_occurrences } - :name: eset; _ - - While the different variants of :tacn:`set` expect that no existential - variables are generated by the tactic, :tacn:`eset` removes this - constraint. In practice, this is relevant only when :tacn:`eset` is - used as a synonym of :tacn:`epose`, i.e. when the :token:`term` does - not occur in the goal. - -.. tacn:: remember @term as @ident__1 {? eqn:@naming_intropattern } - :name: remember - - This behaves as :n:`set (@ident := @term) in *`, using a logical - (Leibniz’s) equality instead of a local definition. - Use :n:`@naming_intropattern` to name or split up the new equation. - - .. tacv:: remember @term as @ident__1 {? eqn:@naming_intropattern } in @goal_occurrences - - This is a more general form of :tacn:`remember` that remembers the - occurrences of :token:`term` specified by an occurrence set. - - .. tacv:: eremember @term as @ident__1 {? eqn:@naming_intropattern } {? in @goal_occurrences } - :name: eremember - - While the different variants of :tacn:`remember` expect that no - existential variables are generated by the tactic, :tacn:`eremember` - removes this constraint. - -.. tacn:: pose (@ident := @term) - :name: pose - - This adds the local definition :n:`@ident := @term` to the current context - without performing any replacement in the goal or in the hypotheses. It is - equivalent to :n:`set (@ident := @term) in |-`. - - .. tacv:: pose (@ident {* @binder } := @term) - - This is equivalent to :n:`pose (@ident := fun {* @binder } => @term)`. - - .. tacv:: pose @term - - This behaves as :n:`pose (@ident := @term)` but :token:`ident` is - generated by Coq. - - .. tacv:: epose (@ident {* @binder } := @term) - epose @term - :name: epose; _ - - While the different variants of :tacn:`pose` expect that no - existential variables are generated by the tactic, :tacn:`epose` - removes this constraint. - -.. tacn:: decompose [{+ @qualid}] @term - :name: decompose - - This tactic recursively decomposes a complex proposition in order to - obtain atomic ones. - - .. example:: - - .. coqtop:: reset all - - Goal forall A B C:Prop, A /\ B /\ C \/ B /\ C \/ C /\ A -> C. - intros A B C H; decompose [and or] H. - all: assumption. - Qed. - - .. note:: - - :tacn:`decompose` does not work on right-hand sides of implications or - products. - - .. tacv:: decompose sum @term - - This decomposes sum types (like :g:`or`). - - .. tacv:: decompose record @term - - This decomposes record types (inductive types with one constructor, - like :g:`and` and :g:`exists` and those defined with the :cmd:`Record` - command. - - -.. _controllingtheproofflow: - -Controlling the proof flow ------------------------------- - -.. tacn:: assert (@ident : @type) - :name: assert - - This tactic applies to any goal. :n:`assert (H : U)` adds a new hypothesis - of name :n:`H` asserting :g:`U` to the current goal and opens a new subgoal - :g:`U` [2]_. The subgoal :g:`U` comes first in the list of subgoals remaining to - prove. - - .. exn:: Not a proposition or a type. - - Arises when the argument :token:`type` is neither of type :g:`Prop`, - :g:`Set` nor :g:`Type`. - - .. tacv:: assert @type - - This behaves as :n:`assert (@ident : @type)` but :n:`@ident` is - generated by Coq. - - .. tacv:: assert @type by @tactic - - This tactic behaves like :tacn:`assert` but applies tactic to solve the - subgoals generated by assert. - - .. exn:: Proof is not complete. - :name: Proof is not complete. (assert) - :undocumented: - - .. tacv:: assert @type as @simple_intropattern - - If :n:`simple_intropattern` is an intro pattern (see :ref:`intropatterns`), - the hypothesis is named after this introduction pattern (in particular, if - :n:`simple_intropattern` is :n:`@ident`, the tactic behaves like - :n:`assert (@ident : @type)`). If :n:`simple_intropattern` is an action - introduction pattern, the tactic behaves like :n:`assert @type` followed by - the action done by this introduction pattern. - - .. tacv:: assert @type as @simple_intropattern by @tactic - - This combines the two previous variants of :tacn:`assert`. - - .. tacv:: assert (@ident := @term) - - This behaves as :n:`assert (@ident : @type) by exact @term` where - :token:`type` is the type of :token:`term`. This is equivalent to using - :tacn:`pose proof`. If the head of term is :token:`ident`, the tactic - behaves as :tacn:`specialize`. - - .. exn:: Variable @ident is already declared. - :undocumented: - -.. tacv:: eassert @type as @simple_intropattern by @tactic - :name: eassert - - While the different variants of :tacn:`assert` expect that no existential - variables are generated by the tactic, :tacn:`eassert` removes this constraint. - This lets you avoid specifying the asserted statement completely before starting - to prove it. - -.. tacv:: pose proof @term {? as @simple_intropattern} - :name: pose proof - - This tactic behaves like :n:`assert @type {? as @simple_intropattern} by exact @term` - where :token:`type` is the type of :token:`term`. In particular, - :n:`pose proof @term as @ident` behaves as :n:`assert (@ident := @term)` - and :n:`pose proof @term as @simple_intropattern` is the same as applying the - :token:`simple_intropattern` to :token:`term`. - -.. tacv:: epose proof @term {? as @simple_intropattern} - :name: epose proof - - While :tacn:`pose proof` expects that no existential variables are generated by - the tactic, :tacn:`epose proof` removes this constraint. - -.. tacv:: pose proof (@ident := @term) - - This is an alternative syntax for :n:`assert (@ident := @term)` and - :n:`pose proof @term as @ident`, following the model of :n:`pose - (@ident := @term)` but dropping the value of :token:`ident`. - -.. tacv:: epose proof (@ident := @term) - - This is an alternative syntax for :n:`eassert (@ident := @term)` - and :n:`epose proof @term as @ident`, following the model of - :n:`epose (@ident := @term)` but dropping the value of - :token:`ident`. - -.. tacv:: enough (@ident : @type) - :name: enough - - This adds a new hypothesis of name :token:`ident` asserting :token:`type` to the - goal the tactic :tacn:`enough` is applied to. A new subgoal stating :token:`type` is - inserted after the initial goal rather than before it as :tacn:`assert` would do. - -.. tacv:: enough @type - - This behaves like :n:`enough (@ident : @type)` with the name :token:`ident` of - the hypothesis generated by Coq. - -.. tacv:: enough @type as @simple_intropattern - - This behaves like :n:`enough @type` using :token:`simple_intropattern` to name or - destruct the new hypothesis. - -.. tacv:: enough (@ident : @type) by @tactic - enough @type {? as @simple_intropattern } by @tactic - - This behaves as above but with :token:`tactic` expected to solve the initial goal - after the extra assumption :token:`type` is added and possibly destructed. If the - :n:`as @simple_intropattern` clause generates more than one subgoal, :token:`tactic` is - applied to all of them. - -.. tacv:: eenough @type {? as @simple_intropattern } {? by @tactic } - eenough (@ident : @type) {? by @tactic } - :name: eenough; _ - - While the different variants of :tacn:`enough` expect that no existential - variables are generated by the tactic, :tacn:`eenough` removes this constraint. - -.. tacv:: cut @type - :name: cut - - This tactic applies to any goal. It implements the non-dependent case of - the “App” rule given in :ref:`typing-rules`. (This is Modus Ponens inference - rule.) :n:`cut U` transforms the current goal :g:`T` into the two following - subgoals: :g:`U -> T` and :g:`U`. The subgoal :g:`U -> T` comes first in the - list of remaining subgoal to prove. - -.. tacv:: specialize (@ident {* @term}) {? as @simple_intropattern} - specialize @ident with @bindings_list {? as @simple_intropattern} - :name: specialize; _ - - This tactic works on local hypothesis :n:`@ident`. The - premises of this hypothesis (either universal quantifications or - non-dependent implications) are instantiated by concrete terms coming either - from arguments :n:`{* @term}` or from a :ref:`bindings list `. - In the first form the application to :n:`{* @term}` can be partial. The - first form is equivalent to :n:`assert (@ident := @ident {* @term})`. In the - second form, instantiation elements can also be partial. In this case the - uninstantiated arguments are inferred by unification if possible or left - quantified in the hypothesis otherwise. With the :n:`as` clause, the local - hypothesis :n:`@ident` is left unchanged and instead, the modified hypothesis - is introduced as specified by the :token:`simple_intropattern`. The name :n:`@ident` - can also refer to a global lemma or hypothesis. In this case, for - compatibility reasons, the behavior of :tacn:`specialize` is close to that of - :tacn:`generalize`: the instantiated statement becomes an additional premise of - the goal. The ``as`` clause is especially useful in this case to immediately - introduce the instantiated statement as a local hypothesis. - - .. exn:: @ident is used in hypothesis @ident. - :undocumented: - - .. exn:: @ident is used in conclusion. - :undocumented: - -.. tacn:: generalize @term - :name: generalize - - This tactic applies to any goal. It generalizes the conclusion with - respect to some term. - -.. example:: - - .. coqtop:: reset none - - Goal forall x y:nat, 0 <= x + y + y. - Proof. intros *. - - .. coqtop:: all - - Show. - generalize (x + y + y). - -If the goal is :g:`G` and :g:`t` is a subterm of type :g:`T` in the goal, -then :n:`generalize t` replaces the goal by :g:`forall (x:T), G′` where :g:`G′` -is obtained from :g:`G` by replacing all occurrences of :g:`t` by :g:`x`. The -name of the variable (here :g:`n`) is chosen based on :g:`T`. - -.. tacv:: generalize {+ @term} - - This is equivalent to :n:`generalize @term; ... ; generalize @term`. - Note that the sequence of term :sub:`i` 's are processed from n to 1. - -.. tacv:: generalize @term at {+ @num} - - This is equivalent to :n:`generalize @term` but it generalizes only over the - specified occurrences of :n:`@term` (counting from left to right on the - expression printed using the :flag:`Printing All` flag). - -.. tacv:: generalize @term as @ident - - This is equivalent to :n:`generalize @term` but it uses :n:`@ident` to name - the generalized hypothesis. - -.. tacv:: generalize {+, @term at {+ @num} as @ident} - - This is the most general form of :n:`generalize` that combines the previous - behaviors. - -.. tacv:: generalize dependent @term - - This generalizes term but also *all* hypotheses that depend on :n:`@term`. It - clears the generalized hypotheses. - -.. tacn:: evar (@ident : @term) - :name: evar - - The :n:`evar` tactic creates a new local definition named :n:`@ident` with type - :n:`@term` in the context. The body of this binding is a fresh existential - variable. - -.. tacn:: instantiate (@ident := @term ) - :name: instantiate - - The instantiate tactic refines (see :tacn:`refine`) an existential variable - :n:`@ident` with the term :n:`@term`. It is equivalent to - :n:`only [ident]: refine @term` (preferred alternative). - - .. note:: To be able to refer to an existential variable by name, the user - must have given the name explicitly (see :ref:`Existential-Variables`). - - .. note:: When you are referring to hypotheses which you did not name - explicitly, be aware that Coq may make a different decision on how to - name the variable in the current goal and in the context of the - existential variable. This can lead to surprising behaviors. - -.. tacv:: instantiate (@num := @term) - - This variant allows to refer to an existential variable which was not named - by the user. The :n:`@num` argument is the position of the existential variable - from right to left in the goal. Because this variant is not robust to slight - changes in the goal, its use is strongly discouraged. - -.. tacv:: instantiate ( @num := @term ) in @ident - instantiate ( @num := @term ) in ( value of @ident ) - instantiate ( @num := @term ) in ( type of @ident ) - - These allow to refer respectively to existential variables occurring in a - hypothesis or in the body or the type of a local definition. - -.. tacv:: instantiate - - Without argument, the instantiate tactic tries to solve as many existential - variables as possible, using information gathered from other tactics in the - same tactical. This is automatically done after each complete tactic (i.e. - after a dot in proof mode), but not, for example, between each tactic when - they are sequenced by semicolons. - -.. tacn:: admit - :name: admit - - This tactic allows temporarily skipping a subgoal so as to - progress further in the rest of the proof. A proof containing admitted - goals cannot be closed with :cmd:`Qed` but only with :cmd:`Admitted`. - -.. tacv:: give_up - - Synonym of :tacn:`admit`. - -.. tacn:: absurd @term - :name: absurd - - This tactic applies to any goal. The argument term is any proposition - :g:`P` of type :g:`Prop`. This tactic applies False elimination, that is it - deduces the current goal from False, and generates as subgoals :g:`∼P` and - :g:`P`. It is very useful in proofs by cases, where some cases are - impossible. In most cases, :g:`P` or :g:`∼P` is one of the hypotheses of the - local context. - -.. tacn:: contradiction - :name: contradiction - - This tactic applies to any goal. The contradiction tactic attempts to - find in the current context (after all intros) a hypothesis that is - equivalent to an empty inductive type (e.g. :g:`False`), to the negation of - a singleton inductive type (e.g. :g:`True` or :g:`x=x`), or two contradictory - hypotheses. - - .. exn:: No such assumption. - :undocumented: - -.. tacv:: contradiction @ident - - The proof of False is searched in the hypothesis named :n:`@ident`. - -.. tacn:: contradict @ident - :name: contradict - - This tactic allows manipulating negated hypothesis and goals. The name - :n:`@ident` should correspond to a hypothesis. With :n:`contradict H`, the - current goal and context is transformed in the following way: - - + H:¬A ⊢ B becomes ⊢ A - + H:¬A ⊢ ¬B becomes H: B ⊢ A - + H: A ⊢ B becomes ⊢ ¬A - + H: A ⊢ ¬B becomes H: B ⊢ ¬A - -.. tacn:: exfalso - :name: exfalso - - This tactic implements the “ex falso quodlibet” logical principle: an - elimination of False is performed on the current goal, and the user is - then required to prove that False is indeed provable in the current - context. This tactic is a macro for :n:`elimtype False`. - -.. _CaseAnalysisAndInduction: - -Case analysis and induction -------------------------------- - -The tactics presented in this section implement induction or case -analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`). - -.. tacn:: destruct @term - :name: destruct - - This tactic applies to any goal. The argument :token:`term` must be of - inductive or co-inductive type and the tactic generates subgoals, one - for each possible form of :token:`term`, i.e. one for each constructor of the - inductive or co-inductive type. Unlike :tacn:`induction`, no induction - hypothesis is generated by :tacn:`destruct`. - - .. tacv:: destruct @ident - - If :token:`ident` denotes a quantified variable of the conclusion - of the goal, then :n:`destruct @ident` behaves - as :n:`intros until @ident; destruct @ident`. If :token:`ident` is not - anymore dependent in the goal after application of :tacn:`destruct`, it - is erased (to avoid erasure, use parentheses, as in :n:`destruct (@ident)`). - - If :token:`ident` is a hypothesis of the context, and :token:`ident` - is not anymore dependent in the goal after application - of :tacn:`destruct`, it is erased (to avoid erasure, use parentheses, as - in :n:`destruct (@ident)`). - - .. tacv:: destruct @num - - :n:`destruct @num` behaves as :n:`intros until @num` - followed by destruct applied to the last introduced hypothesis. - - .. note:: - For destruction of a numeral, use syntax :n:`destruct (@num)` (not - very interesting anyway). - - .. tacv:: destruct @pattern - - The argument of :tacn:`destruct` can also be a pattern of which holes are - denoted by “_”. In this case, the tactic checks that all subterms - matching the pattern in the conclusion and the hypotheses are compatible - and performs case analysis using this subterm. - - .. tacv:: destruct {+, @term} - - This is a shortcut for :n:`destruct @term; ...; destruct @term`. - - .. tacv:: destruct @term as @or_and_intropattern_loc - - This behaves as :n:`destruct @term` but uses the names - in :token:`or_and_intropattern_loc` to name the variables introduced in the - context. The :token:`or_and_intropattern_loc` must have the - form :n:`[p11 ... p1n | ... | pm1 ... pmn ]` with ``m`` being the - number of constructors of the type of :token:`term`. Each variable - introduced by :tacn:`destruct` in the context of the ``i``-th goal - gets its name from the list :n:`pi1 ... pin` in order. If there are not - enough names, :tacn:`destruct` invents names for the remaining variables - to introduce. More generally, the :n:`pij` can be any introduction - pattern (see :tacn:`intros`). This provides a concise notation for - chaining destruction of a hypothesis. - - .. tacv:: destruct @term eqn:@naming_intropattern - :name: destruct ... eqn: - - This behaves as :n:`destruct @term` but adds an equation - between :token:`term` and the value that it takes in each of the - possible cases. The name of the equation is specified - by :token:`naming_intropattern` (see :tacn:`intros`), - in particular ``?`` can be used to let Coq generate a fresh name. - - .. tacv:: destruct @term with @bindings_list - - This behaves like :n:`destruct @term` providing explicit instances for - the dependent premises of the type of :token:`term`. - - .. tacv:: edestruct @term - :name: edestruct - - This tactic behaves like :n:`destruct @term` except that it does not - fail if the instance of a dependent premises of the type - of :token:`term` is not inferable. Instead, the unresolved instances - are left as existential variables to be inferred later, in the same way - as :tacn:`eapply` does. - - .. tacv:: destruct @term using @term {? with @bindings_list } - - This is synonym of :n:`induction @term using @term {? with @bindings_list }`. - - .. tacv:: destruct @term in @goal_occurrences - - This syntax is used for selecting which occurrences of :token:`term` - the case analysis has to be done on. The :n:`in @goal_occurrences` - clause is an occurrence clause whose syntax and behavior is described - in :ref:`occurrences sets `. - - .. tacv:: destruct @term {? with @bindings_list } {? as @or_and_intropattern_loc } {? eqn:@naming_intropattern } {? using @term {? with @bindings_list } } {? in @goal_occurrences } - edestruct @term {? with @bindings_list } {? as @or_and_intropattern_loc } {? eqn:@naming_intropattern } {? using @term {? with @bindings_list } } {? in @goal_occurrences } - - These are the general forms of :tacn:`destruct` and :tacn:`edestruct`. - They combine the effects of the ``with``, ``as``, ``eqn:``, ``using``, - and ``in`` clauses. - -.. tacn:: case @term - :name: case - - The tactic :n:`case` is a more basic tactic to perform case analysis without - recursion. It behaves as :n:`elim @term` but using a case-analysis - elimination principle and not a recursive one. - -.. tacv:: case @term with @bindings_list - - Analogous to :n:`elim @term with @bindings_list` above. - -.. tacv:: ecase @term {? with @bindings_list } - :name: ecase - - In case the type of :n:`@term` has dependent premises, or dependent premises - whose values are not inferable from the :n:`with @bindings_list` clause, - :n:`ecase` turns them into existential variables to be resolved later on. - -.. tacv:: simple destruct @ident - :name: simple destruct - - This tactic behaves as :n:`intros until @ident; case @ident` when :n:`@ident` - is a quantified variable of the goal. - -.. tacv:: simple destruct @num - - This tactic behaves as :n:`intros until @num; case @ident` where :n:`@ident` - is the name given by :n:`intros until @num` to the :n:`@num` -th - non-dependent premise of the goal. - -.. tacv:: case_eq @term - - The tactic :n:`case_eq` is a variant of the :n:`case` tactic that allows to - perform case analysis on a term without completely forgetting its original - form. This is done by generating equalities between the original form of the - term and the outcomes of the case analysis. - -.. tacn:: induction @term - :name: induction - - This tactic applies to any goal. The argument :n:`@term` must be of - inductive type and the tactic :n:`induction` generates subgoals, one for - each possible form of :n:`@term`, i.e. one for each constructor of the - inductive type. - - If the argument is dependent in either the conclusion or some - hypotheses of the goal, the argument is replaced by the appropriate - constructor form in each of the resulting subgoals and induction - hypotheses are added to the local context using names whose prefix - is **IH**. - - There are particular cases: - - + If term is an identifier :n:`@ident` denoting a quantified variable of the - conclusion of the goal, then inductionident behaves as :n:`intros until - @ident; induction @ident`. If :n:`@ident` is not anymore dependent in the - goal after application of :n:`induction`, it is erased (to avoid erasure, - use parentheses, as in :n:`induction (@ident)`). - + If :n:`@term` is a :n:`@num`, then :n:`induction @num` behaves as - :n:`intros until @num` followed by :n:`induction` applied to the last - introduced hypothesis. - - .. note:: - For simple induction on a numeral, use syntax induction (num) - (not very interesting anyway). - - + In case term is a hypothesis :n:`@ident` of the context, and :n:`@ident` - is not anymore dependent in the goal after application of :n:`induction`, - it is erased (to avoid erasure, use parentheses, as in - :n:`induction (@ident)`). - + The argument :n:`@term` can also be a pattern of which holes are denoted - by “_”. In this case, the tactic checks that all subterms matching the - pattern in the conclusion and the hypotheses are compatible and - performs induction using this subterm. - -.. example:: - - .. coqtop:: reset all - - Lemma induction_test : forall n:nat, n = n -> n <= n. - intros n H. - induction n. - -.. exn:: Not an inductive product. - :undocumented: - -.. exn:: Unable to find an instance for the variables @ident ... @ident. - - Use in this case the variant :tacn:`elim ... with` below. - -.. tacv:: induction @term as @or_and_intropattern_loc - - This behaves as :tacn:`induction` but uses the names in - :n:`@or_and_intropattern_loc` to name the variables introduced in the - context. The :n:`@or_and_intropattern_loc` must typically be of the form - :n:`[ p` :sub:`11` :n:`... p` :sub:`1n` :n:`| ... | p`:sub:`m1` :n:`... p`:sub:`mn` :n:`]` - with :n:`m` being the number of constructors of the type of :n:`@term`. Each - variable introduced by induction in the context of the i-th goal gets its - name from the list :n:`p`:sub:`i1` :n:`... p`:sub:`in` in order. If there are - not enough names, induction invents names for the remaining variables to - introduce. More generally, the :n:`p`:sub:`ij` can be any - disjunctive/conjunctive introduction pattern (see :tacn:`intros ...`). For - instance, for an inductive type with one constructor, the pattern notation - :n:`(p`:sub:`1` :n:`, ... , p`:sub:`n` :n:`)` can be used instead of - :n:`[ p`:sub:`1` :n:`... p`:sub:`n` :n:`]`. - -.. tacv:: induction @term with @bindings_list - - This behaves like :tacn:`induction` providing explicit instances for the - premises of the type of :n:`term` (see :ref:`bindings list `). - -.. tacv:: einduction @term - :name: einduction - - This tactic behaves like :tacn:`induction` except that it does not fail if - some dependent premise of the type of :n:`@term` is not inferable. Instead, - the unresolved premises are posed as existential variables to be inferred - later, in the same way as :tacn:`eapply` does. - -.. tacv:: induction @term using @term - :name: induction ... using ... - - This behaves as :tacn:`induction` but using :n:`@term` as induction scheme. - It does not expect the conclusion of the type of the first :n:`@term` to be - inductive. - -.. tacv:: induction @term using @term with @bindings_list - - This behaves as :tacn:`induction ... using ...` but also providing instances - for the premises of the type of the second :n:`@term`. - -.. tacv:: induction {+, @term} using @qualid - - This syntax is used for the case :n:`@qualid` denotes an induction principle - with complex predicates as the induction principles generated by - ``Function`` or ``Functional Scheme`` may be. - -.. tacv:: induction @term in @goal_occurrences - - This syntax is used for selecting which occurrences of :n:`@term` the - induction has to be carried on. The :n:`in @goal_occurrences` clause is an - occurrence clause whose syntax and behavior is described in - :ref:`occurrences sets `. If variables or hypotheses not - mentioning :n:`@term` in their type are listed in :n:`@goal_occurrences`, - those are generalized as well in the statement to prove. - - .. example:: - - .. coqtop:: reset all - - Lemma comm x y : x + y = y + x. - induction y in x |- *. - Show 2. - -.. tacv:: induction @term with @bindings_list as @or_and_intropattern_loc using @term with @bindings_list in @goal_occurrences - einduction @term with @bindings_list as @or_and_intropattern_loc using @term with @bindings_list in @goal_occurrences - - These are the most general forms of :tacn:`induction` and :tacn:`einduction`. It combines the - effects of the with, as, using, and in clauses. - -.. tacv:: elim @term - :name: elim - - This is a more basic induction tactic. Again, the type of the argument - :n:`@term` must be an inductive type. Then, according to the type of the - goal, the tactic ``elim`` chooses the appropriate destructor and applies it - as the tactic :tacn:`apply` would do. For instance, if the proof context - contains :g:`n:nat` and the current goal is :g:`T` of type :g:`Prop`, then - :n:`elim n` is equivalent to :n:`apply nat_ind with (n:=n)`. The tactic - ``elim`` does not modify the context of the goal, neither introduces the - induction loading into the context of hypotheses. More generally, - :n:`elim @term` also works when the type of :n:`@term` is a statement - with premises and whose conclusion is inductive. In that case the tactic - performs induction on the conclusion of the type of :n:`@term` and leaves the - non-dependent premises of the type as subgoals. In the case of dependent - products, the tactic tries to find an instance for which the elimination - lemma applies and fails otherwise. - -.. tacv:: elim @term with @bindings_list - :name: elim ... with - - Allows to give explicit instances to the premises of the type of :n:`@term` - (see :ref:`bindings list `). - -.. tacv:: eelim @term - :name: eelim - - In case the type of :n:`@term` has dependent premises, this turns them into - existential variables to be resolved later on. - -.. tacv:: elim @term using @term - elim @term using @term with @bindings_list - - Allows the user to give explicitly an induction principle :n:`@term` that - is not the standard one for the underlying inductive type of :n:`@term`. The - :n:`@bindings_list` clause allows instantiating premises of the type of - :n:`@term`. - -.. tacv:: elim @term with @bindings_list using @term with @bindings_list - eelim @term with @bindings_list using @term with @bindings_list - - These are the most general forms of :tacn:`elim` and :tacn:`eelim`. It combines the - effects of the ``using`` clause and of the two uses of the ``with`` clause. - -.. tacv:: elimtype @type - :name: elimtype - - The argument :token:`type` must be inductively defined. :n:`elimtype I` is - equivalent to :n:`cut I. intro Hn; elim Hn; clear Hn.` Therefore the - hypothesis :g:`Hn` will not appear in the context(s) of the subgoal(s). - Conversely, if :g:`t` is a :n:`@term` of (inductive) type :g:`I` that does - not occur in the goal, then :n:`elim t` is equivalent to - :n:`elimtype I; 2:exact t.` - -.. tacv:: simple induction @ident - :name: simple induction - - This tactic behaves as :n:`intros until @ident; elim @ident` when - :n:`@ident` is a quantified variable of the goal. - -.. tacv:: simple induction @num - - This tactic behaves as :n:`intros until @num; elim @ident` where :n:`@ident` - is the name given by :n:`intros until @num` to the :n:`@num`-th non-dependent - premise of the goal. - -.. tacn:: double induction @ident @ident - :name: double induction - - This tactic is deprecated and should be replaced by - :n:`induction @ident; induction @ident` (or - :n:`induction @ident ; destruct @ident` depending on the exact needs). - -.. tacv:: double induction @num__1 @num__2 - - This tactic is deprecated and should be replaced by - :n:`induction num1; induction num3` where :n:`num3` is the result - of :n:`num2 - num1` - -.. tacn:: dependent induction @ident - :name: dependent induction - - The *experimental* tactic dependent induction performs induction- - inversion on an instantiated inductive predicate. One needs to first - require the Coq.Program.Equality module to use this tactic. The tactic - is based on the BasicElim tactic by Conor McBride - :cite:`DBLP:conf/types/McBride00` and the work of Cristina Cornes around - inversion :cite:`DBLP:conf/types/CornesT95`. From an instantiated - inductive predicate and a goal, it generates an equivalent goal where - the hypothesis has been generalized over its indexes which are then - constrained by equalities to be the right instances. This permits to - state lemmas without resorting to manually adding these equalities and - still get enough information in the proofs. - -.. example:: - - .. coqtop:: reset all - - Lemma lt_1_r : forall n:nat, n < 1 -> n = 0. - intros n H ; induction H. - - Here we did not get any information on the indexes to help fulfill - this proof. The problem is that, when we use the ``induction`` tactic, we - lose information on the hypothesis instance, notably that the second - argument is 1 here. Dependent induction solves this problem by adding - the corresponding equality to the context. - - .. coqtop:: reset all - - Require Import Coq.Program.Equality. - Lemma lt_1_r : forall n:nat, n < 1 -> n = 0. - intros n H ; dependent induction H. - - The subgoal is cleaned up as the tactic tries to automatically - simplify the subgoals with respect to the generated equalities. In - this enriched context, it becomes possible to solve this subgoal. - - .. coqtop:: all - - reflexivity. - - Now we are in a contradictory context and the proof can be solved. - - .. coqtop:: all - - inversion H. - - This technique works with any inductive predicate. In fact, the - ``dependent induction`` tactic is just a wrapper around the ``induction`` - tactic. One can make its own variant by just writing a new tactic - based on the definition found in ``Coq.Program.Equality``. - -.. tacv:: dependent induction @ident generalizing {+ @ident} - - This performs dependent induction on the hypothesis :n:`@ident` but first - generalizes the goal by the given variables so that they are universally - quantified in the goal. This is generally what one wants to do with the - variables that are inside some constructors in the induction hypothesis. The - other ones need not be further generalized. - -.. tacv:: dependent destruction @ident - :name: dependent destruction - - This performs the generalization of the instance :n:`@ident` but uses - ``destruct`` instead of induction on the generalized hypothesis. This gives - results equivalent to ``inversion`` or ``dependent inversion`` if the - hypothesis is dependent. - -See also the larger example of :tacn:`dependent induction` -and an explanation of the underlying technique. - .. tacn:: function induction (@qualid {+ @term}) :name: function induction @@ -2154,569 +53,6 @@ and an explanation of the underlying technique. .. exn:: Not the right number of induction arguments. :undocumented: -.. tacv:: functional induction (@qualid {+ @term}) as @simple_intropattern using @term with @bindings_list - - Similarly to :tacn:`induction` and :tacn:`elim`, this allows giving - explicitly the name of the introduced variables, the induction principle, and - the values of dependent premises of the elimination scheme, including - *predicates* for mutual induction when :n:`@qualid` is part of a mutually - recursive definition. - -.. tacn:: discriminate @term - :name: discriminate - - This tactic proves any goal from an assumption stating that two - structurally different :n:`@term`\s of an inductive set are equal. For - example, from :g:`(S (S O))=(S O)` we can derive by absurdity any - proposition. - - The argument :n:`@term` is assumed to be a proof of a statement of - conclusion :n:`@term = @term` with the two terms being elements of an - inductive set. To build the proof, the tactic traverses the normal forms - [3]_ of the terms looking for a couple of subterms :g:`u` and :g:`w` (:g:`u` - subterm of the normal form of :n:`@term` and :g:`w` subterm of the normal - form of :n:`@term`), placed at the same positions and whose head symbols are - two different constructors. If such a couple of subterms exists, then the - proof of the current goal is completed, otherwise the tactic fails. - -.. note:: - The syntax :n:`discriminate @ident` can be used to refer to a hypothesis - quantified in the goal. In this case, the quantified hypothesis whose name is - :n:`@ident` is first introduced in the local context using - :n:`intros until @ident`. - -.. exn:: No primitive equality found. - :undocumented: - -.. exn:: Not a discriminable equality. - :undocumented: - -.. tacv:: discriminate @num - - This does the same thing as :n:`intros until @num` followed by - :n:`discriminate @ident` where :n:`@ident` is the identifier for the last - introduced hypothesis. - -.. tacv:: discriminate @term with @bindings_list - - This does the same thing as :n:`discriminate @term` but using the given - bindings to instantiate parameters or hypotheses of :n:`@term`. - -.. tacv:: ediscriminate @num - ediscriminate @term {? with @bindings_list} - :name: ediscriminate; _ - - This works the same as :tacn:`discriminate` but if the type of :token:`term`, or the - type of the hypothesis referred to by :token:`num`, has uninstantiated - parameters, these parameters are left as existential variables. - -.. tacv:: discriminate - - This behaves like :n:`discriminate @ident` if ident is the name of an - hypothesis to which ``discriminate`` is applicable; if the current goal is of - the form :n:`@term <> @term`, this behaves as - :n:`intro @ident; discriminate @ident`. - - .. exn:: No discriminable equalities. - :undocumented: - -.. tacn:: injection @term - :name: injection - - The injection tactic exploits the property that constructors of - inductive types are injective, i.e. that if :g:`c` is a constructor of an - inductive type and :g:`c t`:sub:`1` and :g:`c t`:sub:`2` are equal then - :g:`t`:sub:`1` and :g:`t`:sub:`2` are equal too. - - If :n:`@term` is a proof of a statement of conclusion :n:`@term = @term`, - then :tacn:`injection` applies the injectivity of constructors as deep as - possible to derive the equality of all the subterms of :n:`@term` and - :n:`@term` at positions where the terms start to differ. For example, from - :g:`(S p, S n) = (q, S (S m))` we may derive :g:`S p = q` and - :g:`n = S m`. For this tactic to work, the terms should be typed with an - inductive type and they should be neither convertible, nor having a different - head constructor. If these conditions are satisfied, the tactic derives the - equality of all the subterms at positions where they differ and adds them as - antecedents to the conclusion of the current goal. - - .. example:: - - Consider the following goal: - - .. coqtop:: in - - Inductive list : Set := - | nil : list - | cons : nat -> list -> list. - Parameter P : list -> Prop. - Goal forall l n, P nil -> cons n l = cons 0 nil -> P l. - - .. coqtop:: all - - intros. - injection H0. - - Beware that injection yields an equality in a sigma type whenever the - injected object has a dependent type :g:`P` with its two instances in - different types :g:`(P t`:sub:`1` :g:`... t`:sub:`n` :g:`)` and - :g:`(P u`:sub:`1` :g:`... u`:sub:`n` :sub:`)`. If :g:`t`:sub:`1` and - :g:`u`:sub:`1` are the same and have for type an inductive type for which a decidable - equality has been declared using the command :cmd:`Scheme Equality` - (see :ref:`proofschemes-induction-principles`), - the use of a sigma type is avoided. - - .. note:: - If some quantified hypothesis of the goal is named :n:`@ident`, - then :n:`injection @ident` first introduces the hypothesis in the local - context using :n:`intros until @ident`. - - .. exn:: Not a projectable equality but a discriminable one. - :undocumented: - - .. exn:: Nothing to do, it is an equality between convertible terms. - :undocumented: - - .. exn:: Not a primitive equality. - :undocumented: - - .. exn:: Nothing to inject. - :undocumented: - - .. tacv:: injection @num - - This does the same thing as :n:`intros until @num` followed by - :n:`injection @ident` where :n:`@ident` is the identifier for the last - introduced hypothesis. - - .. tacv:: injection @term with @bindings_list - - This does the same as :n:`injection @term` but using the given bindings to - instantiate parameters or hypotheses of :n:`@term`. - - .. tacv:: einjection @num - einjection @term {? with @bindings_list} - :name: einjection; _ - - This works the same as :n:`injection` but if the type of :n:`@term`, or the - type of the hypothesis referred to by :n:`@num`, has uninstantiated - parameters, these parameters are left as existential variables. - - .. tacv:: injection - - If the current goal is of the form :n:`@term <> @term` , this behaves as - :n:`intro @ident; injection @ident`. - - .. exn:: goal does not satisfy the expected preconditions. - :undocumented: - - .. tacv:: injection @term {? with @bindings_list} as {+ @simple_intropattern} - injection @num as {+ @simple_intropattern} - injection as {+ @simple_intropattern} - einjection @term {? with @bindings_list} as {+ @simple_intropattern} - einjection @num as {+ @simple_intropattern} - einjection as {+ @simple_intropattern} - - These variants apply :n:`intros {+ @simple_intropattern}` after the call to - :tacn:`injection` or :tacn:`einjection` so that all equalities generated are moved in - the context of hypotheses. The number of :n:`@simple_intropattern` must not exceed - the number of equalities newly generated. If it is smaller, fresh - names are automatically generated to adjust the list of :n:`@simple_intropattern` - to the number of new equalities. The original equality is erased if it - corresponds to a hypothesis. - - .. tacv:: injection @term {? with @bindings_list} as @injection_intropattern - injection @num as @injection_intropattern - injection as @injection_intropattern - einjection @term {? with @bindings_list} as @injection_intropattern - einjection @num as @injection_intropattern - einjection as @injection_intropattern - - These are equivalent to the previous variants but using instead the - syntax :token:`injection_intropattern` which :tacn:`intros` - uses. In particular :n:`as [= {+ @simple_intropattern}]` behaves - the same as :n:`as {+ @simple_intropattern}`. - - .. flag:: Structural Injection - - This flag ensures that :n:`injection @term` erases the original hypothesis - and leaves the generated equalities in the context rather than putting them - as antecedents of the current goal, as if giving :n:`injection @term as` - (with an empty list of names). This flag is off by default. - - .. flag:: Keep Proof Equalities - - By default, :tacn:`injection` only creates new equalities between :n:`@term`\s - whose type is in sort :g:`Type` or :g:`Set`, thus implementing a special - behavior for objects that are proofs of a statement in :g:`Prop`. This flag - controls this behavior. - -.. tacn:: inversion @ident - :name: inversion - - Let the type of :n:`@ident` in the local context be :g:`(I t)`, where :g:`I` - is a (co)inductive predicate. Then, ``inversion`` applied to :n:`@ident` - derives for each possible constructor :g:`c i` of :g:`(I t)`, all the - necessary conditions that should hold for the instance :g:`(I t)` to be - proved by :g:`c i`. - -.. note:: - If :n:`@ident` does not denote a hypothesis in the local context but - refers to a hypothesis quantified in the goal, then the latter is - first introduced in the local context using :n:`intros until @ident`. - -.. note:: - As ``inversion`` proofs may be large in size, we recommend the - user to stock the lemmas whenever the same instance needs to be - inverted several times. See :ref:`derive-inversion`. - -.. note:: - Part of the behavior of the ``inversion`` tactic is to generate - equalities between expressions that appeared in the hypothesis that is - being processed. By default, no equalities are generated if they - relate two proofs (i.e. equalities between :token:`term`\s whose type is in sort - :g:`Prop`). This behavior can be turned off by using the - :flag:`Keep Proof Equalities` setting. - -.. tacv:: inversion @num - - This does the same thing as :n:`intros until @num` then :n:`inversion @ident` - where :n:`@ident` is the identifier for the last introduced hypothesis. - -.. tacv:: inversion_clear @ident - :name: inversion_clear - - This behaves as :n:`inversion` and then erases :n:`@ident` from the context. - -.. tacv:: inversion @ident as @or_and_intropattern_loc - - This generally behaves as inversion but using names in :n:`@or_and_intropattern_loc` - for naming hypotheses. The :n:`@or_and_intropattern_loc` must have the form - :n:`[p`:sub:`11` :n:`... p`:sub:`1n` :n:`| ... | p`:sub:`m1` :n:`... p`:sub:`mn` :n:`]` - with `m` being the number of constructors of the type of :n:`@ident`. Be - careful that the list must be of length `m` even if ``inversion`` discards - some cases (which is precisely one of its roles): for the discarded - cases, just use an empty list (i.e. `n = 0`).The arguments of the i-th - constructor and the equalities that ``inversion`` introduces in the - context of the goal corresponding to the i-th constructor, if it - exists, get their names from the list :n:`p`:sub:`i1` :n:`... p`:sub:`in` in - order. If there are not enough names, ``inversion`` invents names for the - remaining variables to introduce. In case an equation splits into several - equations (because ``inversion`` applies ``injection`` on the equalities it - generates), the corresponding name :n:`p`:sub:`ij` in the list must be - replaced by a sublist of the form :n:`[p`:sub:`ij1` :n:`... p`:sub:`ijq` :n:`]` - (or, equivalently, :n:`(p`:sub:`ij1` :n:`, ..., p`:sub:`ijq` :n:`)`) where - `q` is the number of subequalities obtained from splitting the original - equation. Here is an example. The ``inversion ... as`` variant of - ``inversion`` generally behaves in a slightly more expectable way than - ``inversion`` (no artificial duplication of some hypotheses referring to - other hypotheses). To take benefit of these improvements, it is enough to use - ``inversion ... as []``, letting the names being finally chosen by Coq. - - .. example:: - - .. coqtop:: reset all - - Inductive contains0 : list nat -> Prop := - | in_hd : forall l, contains0 (0 :: l) - | in_tl : forall l b, contains0 l -> contains0 (b :: l). - Goal forall l:list nat, contains0 (1 :: l) -> contains0 l. - intros l H; inversion H as [ | l' p Hl' [Heqp Heql'] ]. - -.. tacv:: inversion @num as @or_and_intropattern_loc - - This allows naming the hypotheses introduced by :n:`inversion @num` in the - context. - -.. tacv:: inversion_clear @ident as @or_and_intropattern_loc - - This allows naming the hypotheses introduced by ``inversion_clear`` in the - context. Notice that hypothesis names can be provided as if ``inversion`` - were called, even though the ``inversion_clear`` will eventually erase the - hypotheses. - -.. tacv:: inversion @ident in {+ @ident} - - Let :n:`{+ @ident}` be identifiers in the local context. This tactic behaves as - generalizing :n:`{+ @ident}`, and then performing ``inversion``. - -.. tacv:: inversion @ident as @or_and_intropattern_loc in {+ @ident} - - This allows naming the hypotheses introduced in the context by - :n:`inversion @ident in {+ @ident}`. - -.. tacv:: inversion_clear @ident in {+ @ident} - - Let :n:`{+ @ident}` be identifiers in the local context. This tactic behaves - as generalizing :n:`{+ @ident}`, and then performing ``inversion_clear``. - -.. tacv:: inversion_clear @ident as @or_and_intropattern_loc in {+ @ident} - - This allows naming the hypotheses introduced in the context by - :n:`inversion_clear @ident in {+ @ident}`. - -.. tacv:: dependent inversion @ident - :name: dependent inversion - - That must be used when :n:`@ident` appears in the current goal. It acts like - ``inversion`` and then substitutes :n:`@ident` for the corresponding - :n:`@@term` in the goal. - -.. tacv:: dependent inversion @ident as @or_and_intropattern_loc - - This allows naming the hypotheses introduced in the context by - :n:`dependent inversion @ident`. - -.. tacv:: dependent inversion_clear @ident - - Like ``dependent inversion``, except that :n:`@ident` is cleared from the - local context. - -.. tacv:: dependent inversion_clear @ident as @or_and_intropattern_loc - - This allows naming the hypotheses introduced in the context by - :n:`dependent inversion_clear @ident`. - -.. tacv:: dependent inversion @ident with @term - :name: dependent inversion ... with ... - - This variant allows you to specify the generalization of the goal. It is - useful when the system fails to generalize the goal automatically. If - :n:`@ident` has type :g:`(I t)` and :g:`I` has type :g:`forall (x:T), s`, - then :n:`@term` must be of type :g:`I:forall (x:T), I x -> s'` where - :g:`s'` is the type of the goal. - -.. tacv:: dependent inversion @ident as @or_and_intropattern_loc with @term - - This allows naming the hypotheses introduced in the context by - :n:`dependent inversion @ident with @term`. - -.. tacv:: dependent inversion_clear @ident with @term - - Like :tacn:`dependent inversion ... with ...` with but clears :n:`@ident` from the - local context. - -.. tacv:: dependent inversion_clear @ident as @or_and_intropattern_loc with @term - - This allows naming the hypotheses introduced in the context by - :n:`dependent inversion_clear @ident with @term`. - -.. tacv:: simple inversion @ident - :name: simple inversion - - It is a very primitive inversion tactic that derives all the necessary - equalities but it does not simplify the constraints as ``inversion`` does. - -.. tacv:: simple inversion @ident as @or_and_intropattern_loc - - This allows naming the hypotheses introduced in the context by - ``simple inversion``. - -.. tacv:: inversion @ident using @ident - :name: inversion ... using ... - - Let :n:`@ident` have type :g:`(I t)` (:g:`I` an inductive predicate) in the - local context, and :n:`@ident` be a (dependent) inversion lemma. Then, this - tactic refines the current goal with the specified lemma. - -.. tacv:: inversion @ident using @ident in {+ @ident} - - This tactic behaves as generalizing :n:`{+ @ident}`, then doing - :n:`inversion @ident using @ident`. - -.. tacv:: inversion_sigma - :name: inversion_sigma - - This tactic turns equalities of dependent pairs (e.g., - :g:`existT P x p = existT P y q`, frequently left over by inversion on - a dependent type family) into pairs of equalities (e.g., a hypothesis - :g:`H : x = y` and a hypothesis of type :g:`rew H in p = q`); these - hypotheses can subsequently be simplified using :tacn:`subst`, without ever - invoking any kind of axiom asserting uniqueness of identity proofs. If you - want to explicitly specify the hypothesis to be inverted, or name the - generated hypotheses, you can invoke - :n:`induction H as [H1 H2] using eq_sigT_rect.` This tactic also works for - :g:`sig`, :g:`sigT2`, and :g:`sig2`, and there are similar :g:`eq_sig` - :g:`***_rect` induction lemmas. - -.. example:: - - *Non-dependent inversion*. - - Let us consider the relation :g:`Le` over natural numbers: - - .. coqtop:: reset in - - Inductive Le : nat -> nat -> Set := - | LeO : forall n:nat, Le 0 n - | LeS : forall n m:nat, Le n m -> Le (S n) (S m). - - - Let us consider the following goal: - - .. coqtop:: none - - Section Section. - Variable P : nat -> nat -> Prop. - Variable Q : forall n m:nat, Le n m -> Prop. - Goal forall n m, Le (S n) m -> P n m. - - .. coqtop:: out - - intros. - - To prove the goal, we may need to reason by cases on :g:`H` and to derive - that :g:`m` is necessarily of the form :g:`(S m0)` for certain :g:`m0` and that - :g:`(Le n m0)`. Deriving these conditions corresponds to proving that the only - possible constructor of :g:`(Le (S n) m)` is :g:`LeS` and that we can invert - the arrow in the type of :g:`LeS`. This inversion is possible because :g:`Le` - is the smallest set closed by the constructors :g:`LeO` and :g:`LeS`. - - .. coqtop:: all - - inversion_clear H. - - Note that :g:`m` has been substituted in the goal for :g:`(S m0)` and that the - hypothesis :g:`(Le n m0)` has been added to the context. - - Sometimes it is interesting to have the equality :g:`m = (S m0)` in the - context to use it after. In that case we can use :tacn:`inversion` that does - not clear the equalities: - - .. coqtop:: none restart - - intros. - - .. coqtop:: all - - inversion H. - -.. example:: - - *Dependent inversion.* - - Let us consider the following goal: - - .. coqtop:: none - - Abort. - Goal forall n m (H:Le (S n) m), Q (S n) m H. - - .. coqtop:: out - - intros. - - As :g:`H` occurs in the goal, we may want to reason by cases on its - structure and so, we would like inversion tactics to substitute :g:`H` by - the corresponding @term in constructor form. Neither :tacn:`inversion` nor - :tacn:`inversion_clear` do such a substitution. To have such a behavior we - use the dependent inversion tactics: - - .. coqtop:: all - - dependent inversion_clear H. - - Note that :g:`H` has been substituted by :g:`(LeS n m0 l)` and :g:`m` by :g:`(S m0)`. - -.. example:: - - *Using inversion_sigma.* - - Let us consider the following inductive type of - length-indexed lists, and a lemma about inverting equality of cons: - - .. coqtop:: reset all - - Require Import Coq.Logic.Eqdep_dec. - - Inductive vec A : nat -> Type := - | nil : vec A O - | cons {n} (x : A) (xs : vec A n) : vec A (S n). - - Lemma invert_cons : forall A n x xs y ys, - @cons A n x xs = @cons A n y ys - -> xs = ys. - - Proof. - intros A n x xs y ys H. - - After performing inversion, we are left with an equality of existTs: - - .. coqtop:: all - - inversion H. - - We can turn this equality into a usable form with inversion_sigma: - - .. coqtop:: all - - inversion_sigma. - - To finish cleaning up the proof, we will need to use the fact that - that all proofs of n = n for n a nat are eq_refl: - - .. coqtop:: all - - let H := match goal with H : n = n |- _ => H end in - pose proof (Eqdep_dec.UIP_refl_nat _ H); subst H. - simpl in *. - - Finally, we can finish the proof: - - .. coqtop:: all - - assumption. - Qed. - -.. tacn:: fix @ident @num - :name: fix - - This tactic is a primitive tactic to start a proof by induction. In - general, it is easier to rely on higher-level induction tactics such - as the ones described in :tacn:`induction`. - - In the syntax of the tactic, the identifier :n:`@ident` is the name given to - the induction hypothesis. The natural number :n:`@num` tells on which - premise of the current goal the induction acts, starting from 1, - counting both dependent and non dependent products, but skipping local - definitions. Especially, the current lemma must be composed of at - least :n:`@num` products. - - Like in a fix expression, the induction hypotheses have to be used on - structurally smaller arguments. The verification that inductive proof - arguments are correct is done only at the time of registering the - lemma in the environment. To know if the use of induction hypotheses - is correct at some time of the interactive development of a proof, use - the command ``Guarded`` (see Section :ref:`requestinginformation`). - -.. tacv:: fix @ident @num with {+ (@ident {+ @binder} [{struct @ident}] : @type)} - - This starts a proof by mutual induction. The statements to be simultaneously - proved are respectively :g:`forall binder ... binder, type`. - The identifiers :n:`@ident` are the names of the induction hypotheses. The identifiers - :n:`@ident` are the respective names of the premises on which the induction - is performed in the statements to be simultaneously proved (if not given, the - system tries to guess itself what they are). - -.. tacn:: cofix @ident - :name: cofix - - This tactic starts a proof by coinduction. The identifier :n:`@ident` is the - name given to the coinduction hypothesis. Like in a cofix expression, - the use of induction hypotheses have to guarded by a constructor. The - verification that the use of co-inductive hypotheses is correct is - done only at the time of registering the lemma in the environment. To - know if the use of coinduction hypotheses is correct at some time of - the interactive development of a proof, use the command ``Guarded`` - (see Section :ref:`requestinginformation`). - -.. tacv:: cofix @ident with {+ (@ident {+ @binder} : @type)} - - This starts a proof by mutual coinduction. The statements to be - simultaneously proved are respectively :g:`forall binder ... binder, type` - The identifiers :n:`@ident` are the names of the coinduction hypotheses. - -.. _rewritingexpressions: - Rewriting expressions --------------------- -- cgit v1.2.3 From ec34150a537dee4662a48c8a083f257e3837315e Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Tue, 21 Apr 2020 16:51:01 +0200 Subject: Remove parts of the Tactics chapter. --- doc/sphinx/proof-engine/tactics.rst | 1800 ----------------------------------- 1 file changed, 1800 deletions(-) (limited to 'doc') diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index f2c662e053..439be0ecf8 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -53,1806 +53,6 @@ .. exn:: Not the right number of induction arguments. :undocumented: -Rewriting expressions ---------------------- - -These tactics use the equality :g:`eq:forall A:Type, A->A->Prop` defined in -file ``Logic.v`` (see :ref:`coq-library-logic`). The notation for :g:`eq T t u` is -simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. - -.. tacn:: rewrite @term - :name: rewrite - - This tactic applies to any goal. The type of :token:`term` must have the form - - ``forall (x``:sub:`1` ``:A``:sub:`1` ``) ... (x``:sub:`n` ``:A``:sub:`n` ``), eq term``:sub:`1` ``term``:sub:`2` ``.`` - - where :g:`eq` is the Leibniz equality or a registered setoid equality. - - Then :n:`rewrite @term` finds the first subterm matching `term`\ :sub:`1` in the goal, - resulting in instances `term`:sub:`1`' and `term`:sub:`2`' and then - replaces every occurrence of `term`:subscript:`1`' by `term`:subscript:`2`'. - Hence, some of the variables :g:`x`\ :sub:`i` are solved by unification, - and some of the types :g:`A`\ :sub:`1`:g:`, ..., A`\ :sub:`n` become new - subgoals. - - .. exn:: The @term provided does not end with an equation. - :undocumented: - - .. exn:: Tactic generated a subgoal identical to the original goal. This happens if @term does not occur in the goal. - :undocumented: - - .. tacv:: rewrite -> @term - - Is equivalent to :n:`rewrite @term` - - .. tacv:: rewrite <- @term - - Uses the equality :n:`@term`:sub:`1` :n:`= @term` :sub:`2` from right to left - - .. tacv:: rewrite @term in @goal_occurrences - - Analogous to :n:`rewrite @term` but rewriting is done following - the clause :token:`goal_occurrences`. For instance: - - + :n:`rewrite H in H'` will rewrite `H` in the hypothesis - ``H'`` instead of the current goal. - + :n:`rewrite H in H' at 1, H'' at - 2 |- *` means - :n:`rewrite H; rewrite H in H' at 1; rewrite H in H'' at - 2.` - In particular a failure will happen if any of these three simpler tactics - fails. - + :n:`rewrite H in * |-` will do :n:`rewrite H in H'` for all hypotheses - :g:`H'` different from :g:`H`. - A success will happen as soon as at least one of these simpler tactics succeeds. - + :n:`rewrite H in *` is a combination of :n:`rewrite H` and :n:`rewrite H in * |-` - that succeeds if at least one of these two tactics succeeds. - - Orientation :g:`->` or :g:`<-` can be inserted before the :token:`term` to rewrite. - - .. tacv:: rewrite @term at @occurrences - - Rewrite only the given :token:`occurrences` of :token:`term`. Occurrences are - specified from left to right as for pattern (:tacn:`pattern`). The rewrite is - always performed using setoid rewriting, even for Leibniz’s equality, so one - has to ``Import Setoid`` to use this variant. - - .. tacv:: rewrite @term by @tactic - - Use tactic to completely solve the side-conditions arising from the - :tacn:`rewrite`. - - .. tacv:: rewrite {+, @orientation @term} {? in @ident } - - Is equivalent to the `n` successive tactics :n:`{+; rewrite @term}`, each one - working on the first subgoal generated by the previous one. An :production:`orientation` - ``->`` or ``<-`` can be inserted before each :token:`term` to rewrite. One - unique clause can be added at the end after the keyword in; it will then - affect all rewrite operations. - - In all forms of rewrite described above, a :token:`term` to rewrite can be - immediately prefixed by one of the following modifiers: - - + `?` : the tactic :n:`rewrite ?@term` performs the rewrite of :token:`term` as many - times as possible (perhaps zero time). This form never fails. - + :n:`@num?` : works similarly, except that it will do at most :token:`num` rewrites. - + `!` : works as `?`, except that at least one rewrite should succeed, otherwise - the tactic fails. - + :n:`@num!` (or simply :n:`@num`) : precisely :token:`num` rewrites of :token:`term` will be done, - leading to failure if these :token:`num` rewrites are not possible. - - .. tacv:: erewrite @term - :name: erewrite - - This tactic works as :n:`rewrite @term` but turning - unresolved bindings into existential variables, if any, instead of - failing. It has the same variants as :tacn:`rewrite` has. - - .. flag:: Keyed Unification - - Makes higher-order unification used by :tacn:`rewrite` rely on a set of keys to drive - unification. The subterms, considered as rewriting candidates, must start with - the same key as the left- or right-hand side of the lemma given to rewrite, and the arguments - are then unified up to full reduction. - -.. tacn:: replace @term with @term’ - :name: replace - - This tactic applies to any goal. It replaces all free occurrences of :n:`@term` - in the current goal with :n:`@term’` and generates an equality :n:`@term = @term’` - as a subgoal. This equality is automatically solved if it occurs among - the assumptions, or if its symmetric form occurs. It is equivalent to - :n:`cut @term = @term’; [intro H`:sub:`n` :n:`; rewrite <- H`:sub:`n` :n:`; clear H`:sub:`n`:n:`|| assumption || symmetry; try assumption]`. - - .. exn:: Terms do not have convertible types. - :undocumented: - - .. tacv:: replace @term with @term’ by @tactic - - This acts as :n:`replace @term with @term’` but applies :token:`tactic` to solve the generated - subgoal :n:`@term = @term’`. - - .. tacv:: replace @term - - Replaces :n:`@term` with :n:`@term’` using the first assumption whose type has - the form :n:`@term = @term’` or :n:`@term’ = @term`. - - .. tacv:: replace -> @term - - Replaces :n:`@term` with :n:`@term’` using the first assumption whose type has - the form :n:`@term = @term’` - - .. tacv:: replace <- @term - - Replaces :n:`@term` with :n:`@term’` using the first assumption whose type has - the form :n:`@term’ = @term` - - .. tacv:: replace @term {? with @term} in @goal_occurrences {? by @tactic} - replace -> @term in @goal_occurrences - replace <- @term in @goal_occurrences - - Acts as before but the replacements take place in the specified clauses - (:token:`goal_occurrences`) (see :ref:`performingcomputations`) and not - only in the conclusion of the goal. The clause argument must not contain - any ``type of`` nor ``value of``. - - .. tacv:: cutrewrite <- (@term = @term’) - :name: cutrewrite - - .. deprecated:: 8.5 - - This tactic can be replaced by :n:`enough (@term = @term’) as <-`. - - .. tacv:: cutrewrite -> (@term = @term’) - - .. deprecated:: 8.5 - - This tactic can be replaced by :n:`enough (@term = @term’) as ->`. - - -.. tacn:: subst @ident - :name: subst - - This tactic applies to a goal that has :n:`@ident` in its context and (at - least) one hypothesis, say :g:`H`, of type :n:`@ident = t` or :n:`t = @ident` - with :n:`@ident` not occurring in :g:`t`. Then it replaces :n:`@ident` by - :g:`t` everywhere in the goal (in the hypotheses and in the conclusion) and - clears :n:`@ident` and :g:`H` from the context. - - If :n:`@ident` is a local definition of the form :n:`@ident := t`, it is also - unfolded and cleared. - - .. note:: - + When several hypotheses have the form :n:`@ident = t` or :n:`t = @ident`, the - first one is used. - - + If :g:`H` is itself dependent in the goal, it is replaced by the proof of - reflexivity of equality. - - .. tacv:: subst {+ @ident} - - This is equivalent to :n:`subst @ident`:sub:`1`:n:`; ...; subst @ident`:sub:`n`. - - .. tacv:: subst - - This applies subst repeatedly from top to bottom to all identifiers of the - context for which an equality of the form :n:`@ident = t` or :n:`t = @ident` - or :n:`@ident := t` exists, with :n:`@ident` not occurring in ``t``. - - .. flag:: Regular Subst Tactic - - This flag controls the behavior of :tacn:`subst`. When it is - activated (it is by default), :tacn:`subst` also deals with the following corner cases: - - + A context with ordered hypotheses :n:`@ident`:sub:`1` :n:`= @ident`:sub:`2` - and :n:`@ident`:sub:`1` :n:`= t`, or :n:`t′ = @ident`:sub:`1`` with `t′` not - a variable, and no other hypotheses of the form :n:`@ident`:sub:`2` :n:`= u` - or :n:`u = @ident`:sub:`2`; without the flag, a second call to - subst would be necessary to replace :n:`@ident`:sub:`2` by `t` or - `t′` respectively. - + The presence of a recursive equation which without the flag would - be a cause of failure of :tacn:`subst`. - + A context with cyclic dependencies as with hypotheses :n:`@ident`:sub:`1` :n:`= f @ident`:sub:`2` - and :n:`@ident`:sub:`2` :n:`= g @ident`:sub:`1` which without the - flag would be a cause of failure of :tacn:`subst`. - - Additionally, it prevents a local definition such as :n:`@ident := t` to be - unfolded which otherwise it would exceptionally unfold in configurations - containing hypotheses of the form :n:`@ident = u`, or :n:`u′ = @ident` - with `u′` not a variable. Finally, it preserves the initial order of - hypotheses, which without the flag it may break. - default. - - -.. tacn:: stepl @term - :name: stepl - - This tactic is for chaining rewriting steps. It assumes a goal of the - form :n:`R @term @term` where ``R`` is a binary relation and relies on a - database of lemmas of the form :g:`forall x y z, R x y -> eq x z -> R z y` - where `eq` is typically a setoid equality. The application of :n:`stepl @term` - then replaces the goal by :n:`R @term @term` and adds a new goal stating - :n:`eq @term @term`. - - .. cmd:: Declare Left Step @term - - Adds :n:`@term` to the database used by :tacn:`stepl`. - - This tactic is especially useful for parametric setoids which are not accepted - as regular setoids for :tacn:`rewrite` and :tacn:`setoid_replace` (see - :ref:`Generalizedrewriting`). - - .. tacv:: stepl @term by @tactic - - This applies :n:`stepl @term` then applies :token:`tactic` to the second goal. - - .. tacv:: stepr @term by @tactic - :name: stepr - - This behaves as :tacn:`stepl` but on the right-hand-side of the binary - relation. Lemmas are expected to be of the form - :g:`forall x y z, R x y -> eq y z -> R x z`. - - .. cmd:: Declare Right Step @term - - Adds :n:`@term` to the database used by :tacn:`stepr`. - - -.. tacn:: change @term - :name: change - - This tactic applies to any goal. It implements the rule ``Conv`` given in - :ref:`subtyping-rules`. :g:`change U` replaces the current goal `T` - with `U` providing that `U` is well-formed and that `T` and `U` are - convertible. - - .. exn:: Not convertible. - :undocumented: - - .. tacv:: change @term with @term’ - - This replaces the occurrences of :n:`@term` by :n:`@term’` in the current goal. - The term :n:`@term` and :n:`@term’` must be convertible. - - .. tacv:: change @term at {+ @num} with @term’ - - This replaces the occurrences numbered :n:`{+ @num}` of :n:`@term` by :n:`@term’` - in the current goal. The terms :n:`@term` and :n:`@term’` must be convertible. - - .. exn:: Too few occurrences. - :undocumented: - - .. tacv:: change @term {? {? at {+ @num}} with @term} in @ident - - This applies the :tacn:`change` tactic not to the goal but to the hypothesis :n:`@ident`. - - .. tacv:: now_show @term - - This is a synonym of :n:`change @term`. It can be used to - make some proof steps explicit when refactoring a proof script - to make it readable. - - .. seealso:: :ref:`Performing computations ` - -.. _performingcomputations: - -Performing computations ---------------------------- - -This set of tactics implements different specialized usages of the -tactic :tacn:`change`. - -All conversion tactics (including :tacn:`change`) can be parameterized by the -parts of the goal where the conversion can occur. This is done using -*goal clauses* which consists in a list of hypotheses and, optionally, -of a reference to the conclusion of the goal. For defined hypothesis -it is possible to specify if the conversion should occur on the type -part, the body part or both (default). - -Goal clauses are written after a conversion tactic (tactics :tacn:`set`, -:tacn:`rewrite`, :tacn:`replace` and :tacn:`autorewrite` also use goal -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}`. - -.. tacn:: cbv {* @flag} - lazy {* @flag} - :name: cbv; lazy - - These parameterized reduction tactics apply to any goal and perform - the normalization of the goal according to the specified flags. In - correspondence with the kinds of reduction considered in Coq namely - :math:`\beta` (reduction of functional application), :math:`\delta` - (unfolding of transparent constants, see :ref:`vernac-controlling-the-reduction-strategies`), - :math:`\iota` (reduction of - pattern matching over a constructed term, and unfolding of :g:`fix` and - :g:`cofix` expressions) and :math:`\zeta` (contraction of local definitions), the - flags are either ``beta``, ``delta``, ``match``, ``fix``, ``cofix``, - ``iota`` or ``zeta``. The ``iota`` flag is a shorthand for ``match``, ``fix`` - and ``cofix``. The ``delta`` flag itself can be refined into - :n:`delta [ {+ @qualid} ]` or :n:`delta - [ {+ @qualid} ]`, restricting in the first - case the constants to unfold to the constants listed, and restricting in the - second case the constant to unfold to all but the ones explicitly mentioned. - Notice that the ``delta`` flag does not apply to variables bound by a let-in - construction inside the :n:`@term` itself (use here the ``zeta`` flag). In - any cases, opaque constants are not unfolded (see :ref:`vernac-controlling-the-reduction-strategies`). - - Normalization according to the flags is done by first evaluating the - head of the expression into a *weak-head* normal form, i.e. until the - evaluation is blocked by a variable (or an opaque constant, or an - axiom), as e.g. in :g:`x u1 ... un` , or :g:`match x with ... end`, or - :g:`(fix f x {struct x} := ...) x`, or is a constructed form (a - :math:`\lambda`-expression, a constructor, a cofixpoint, an inductive type, a - product type, a sort), or is a redex that the flags prevent to reduce. Once a - weak-head normal form is obtained, subterms are recursively reduced using the - same strategy. - - Reduction to weak-head normal form can be done using two strategies: - *lazy* (``lazy`` tactic), or *call-by-value* (``cbv`` tactic). The lazy - strategy is a call-by-need strategy, with sharing of reductions: the - arguments of a function call are weakly evaluated only when necessary, - and if an argument is used several times then it is weakly computed - only once. This reduction is efficient for reducing expressions with - dead code. For instance, the proofs of a proposition :g:`exists x. P(x)` - reduce to a pair of a witness :g:`t`, and a proof that :g:`t` satisfies the - predicate :g:`P`. Most of the time, :g:`t` may be computed without computing - the proof of :g:`P(t)`, thanks to the lazy strategy. - - The call-by-value strategy is the one used in ML languages: the - arguments of a function call are systematically weakly evaluated - first. Despite the lazy strategy always performs fewer reductions than - the call-by-value strategy, the latter is generally more efficient for - evaluating purely computational expressions (i.e. with little dead code). - -.. tacv:: compute - cbv - :name: compute; _ - - These are synonyms for ``cbv beta delta iota zeta``. - -.. tacv:: lazy - - This is a synonym for ``lazy beta delta iota zeta``. - -.. tacv:: compute [ {+ @qualid} ] - cbv [ {+ @qualid} ] - - These are synonyms of :n:`cbv beta delta {+ @qualid} iota zeta`. - -.. tacv:: compute - [ {+ @qualid} ] - cbv - [ {+ @qualid} ] - - These are synonyms of :n:`cbv beta delta -{+ @qualid} iota zeta`. - -.. tacv:: lazy [ {+ @qualid} ] - lazy - [ {+ @qualid} ] - - These are respectively synonyms of :n:`lazy beta delta {+ @qualid} iota zeta` - and :n:`lazy beta delta -{+ @qualid} iota zeta`. - -.. tacv:: vm_compute - :name: vm_compute - - This tactic evaluates the goal using the optimized call-by-value evaluation - bytecode-based virtual machine described in :cite:`CompiledStrongReduction`. - This algorithm is dramatically more efficient than the algorithm used for the - :tacn:`cbv` tactic, but it cannot be fine-tuned. It is especially interesting for - full evaluation of algebraic objects. This includes the case of - reflection-based tactics. - -.. tacv:: native_compute - :name: native_compute - - This tactic evaluates the goal by compilation to OCaml as described - in :cite:`FullReduction`. If Coq is running in native code, it can be - typically two to five times faster than :tacn:`vm_compute`. Note however that the - compilation cost is higher, so it is worth using only for intensive - computations. - - .. flag:: NativeCompute Timing - - This flag causes all calls to the native compiler to print - timing information for the compilation, execution, and - reification phases of native compilation. - - .. flag:: NativeCompute Profiling - - On Linux, if you have the ``perf`` profiler installed, this flag makes - it possible to profile :tacn:`native_compute` evaluations. - - .. opt:: NativeCompute Profile Filename @string - :name: NativeCompute Profile Filename - - This option specifies the profile output; the default is - ``native_compute_profile.data``. The actual filename used - will contain extra characters to avoid overwriting an existing file; that - filename is reported to the user. - That means you can individually profile multiple uses of - :tacn:`native_compute` in a script. From the Linux command line, run ``perf report`` - on the profile file to see the results. Consult the ``perf`` documentation - for more details. - -.. flag:: Debug Cbv - - This flag makes :tacn:`cbv` (and its derivative :tacn:`compute`) print - information about the constants it encounters and the unfolding decisions it - makes. - -.. tacn:: red - :name: red - - This tactic applies to a goal that has the form:: - - forall (x:T1) ... (xk:Tk), T - - with :g:`T` :math:`\beta`:math:`\iota`:math:`\zeta`-reducing to :g:`c t`:sub:`1` :g:`... t`:sub:`n` and :g:`c` a - constant. If :g:`c` is transparent then it replaces :g:`c` with its - definition (say :g:`t`) and then reduces - :g:`(t t`:sub:`1` :g:`... t`:sub:`n` :g:`)` according to :math:`\beta`:math:`\iota`:math:`\zeta`-reduction rules. - -.. exn:: Not reducible. - :undocumented: - -.. exn:: No head constant to reduce. - :undocumented: - -.. tacn:: hnf - :name: hnf - - This tactic applies to any goal. It replaces the current goal with its - head normal form according to the :math:`\beta`:math:`\delta`:math:`\iota`:math:`\zeta`-reduction rules, i.e. it - reduces the head of the goal until it becomes a product or an - irreducible term. All inner :math:`\beta`:math:`\iota`-redexes are also reduced. - - Example: The term :g:`fun n : nat => S n + S n` is not reduced by :n:`hnf`. - -.. note:: - The :math:`\delta` rule only applies to transparent constants (see :ref:`vernac-controlling-the-reduction-strategies` - on transparency and opacity). - -.. tacn:: cbn - simpl - :name: cbn; simpl - - These tactics apply to any goal. They try to reduce a term to - something still readable instead of fully normalizing it. They perform - a sort of strong normalization with two key differences: - - + They unfold a constant if and only if it leads to a :math:`\iota`-reduction, - i.e. reducing a match or unfolding a fixpoint. - + While reducing a constant unfolding to (co)fixpoints, the tactics - use the name of the constant the (co)fixpoint comes from instead of - the (co)fixpoint definition in recursive calls. - - The :tacn:`cbn` tactic is claimed to be a more principled, faster and more - predictable replacement for :tacn:`simpl`. - - The :tacn:`cbn` tactic accepts the same flags as :tacn:`cbv` and - :tacn:`lazy`. The behavior of both :tacn:`simpl` and :tacn:`cbn` - can be tuned using the Arguments vernacular command as follows: - - + A constant can be marked to be never unfolded by :tacn:`cbn` or - :tacn:`simpl`: - - .. example:: - - .. coqtop:: all - - Arguments minus n m : simpl never. - - After that command an expression like :g:`(minus (S x) y)` is left - untouched by the tactics :tacn:`cbn` and :tacn:`simpl`. - - + A constant can be marked to be unfolded only if applied to enough - arguments. The number of arguments required can be specified using the - ``/`` symbol in the argument list of the :cmd:`Arguments` command. - - .. example:: - - .. coqtop:: all - - Definition fcomp A B C f (g : A -> B) (x : A) : C := f (g x). - Arguments fcomp {A B C} f g x /. - Notation "f \o g" := (fcomp f g) (at level 50). - - After that command the expression :g:`(f \o g)` is left untouched by - :tacn:`simpl` while :g:`((f \o g) t)` is reduced to :g:`(f (g t))`. - The same mechanism can be used to make a constant volatile, i.e. - always unfolded. - - .. example:: - - .. coqtop:: all - - Definition volatile := fun x : nat => x. - Arguments volatile / x. - - + A constant can be marked to be unfolded only if an entire set of - arguments evaluates to a constructor. The ``!`` symbol can be used to mark - such arguments. - - .. example:: - - .. coqtop:: all - - Arguments minus !n !m. - - After that command, the expression :g:`(minus (S x) y)` is left untouched - by :tacn:`simpl`, while :g:`(minus (S x) (S y))` is reduced to :g:`(minus x y)`. - - + A special heuristic to determine if a constant has to be unfolded - can be activated with the following command: - - .. example:: - - .. coqtop:: all - - Arguments minus n m : simpl nomatch. - - The heuristic avoids to perform a simplification step that would expose a - match construct in head position. For example the expression - :g:`(minus (S (S x)) (S y))` is simplified to :g:`(minus (S x) y)` - even if an extra simplification is possible. - - In detail, the tactic :tacn:`simpl` first applies :math:`\beta`:math:`\iota`-reduction. Then, it - expands transparent constants and tries to reduce further using :math:`\beta`:math:`\iota`-reduction. - But, when no :math:`\iota` rule is applied after unfolding then - :math:`\delta`-reductions are not applied. For instance trying to use :tacn:`simpl` on - :g:`(plus n O) = n` changes nothing. - - Notice that only transparent constants whose name can be reused in the - recursive calls are possibly unfolded by :tacn:`simpl`. For instance a - constant defined by :g:`plus' := plus` is possibly unfolded and reused in - the recursive calls, but a constant such as :g:`succ := plus (S O)` is - never unfolded. This is the main difference between :tacn:`simpl` and :tacn:`cbn`. - The tactic :tacn:`cbn` reduces whenever it will be able to reuse it or not: - :g:`succ t` is reduced to :g:`S t`. - -.. tacv:: cbn [ {+ @qualid} ] - cbn - [ {+ @qualid} ] - - These are respectively synonyms of :n:`cbn beta delta [ {+ @qualid} ] iota zeta` - and :n:`cbn beta delta - [ {+ @qualid} ] iota zeta` (see :tacn:`cbn`). - -.. tacv:: simpl @pattern - - This applies :tacn:`simpl` only to the subterms matching - :n:`@pattern` in the current goal. - -.. tacv:: simpl @pattern at {+ @num} - - This applies :tacn:`simpl` only to the :n:`{+ @num}` occurrences of the subterms - matching :n:`@pattern` in the current goal. - - .. exn:: Too few occurrences. - :undocumented: - -.. tacv:: simpl @qualid - simpl @string - - This applies :tacn:`simpl` only to the applicative subterms whose head occurrence - is the unfoldable constant :n:`@qualid` (the constant can be referred to by - its notation using :n:`@string` if such a notation exists). - -.. tacv:: simpl @qualid at {+ @num} - simpl @string at {+ @num} - - This applies :tacn:`simpl` only to the :n:`{+ @num}` applicative subterms whose - head occurrence is :n:`@qualid` (or :n:`@string`). - -.. flag:: Debug RAKAM - - This flag makes :tacn:`cbn` print various debugging information. - ``RAKAM`` is the Refolding Algebraic Krivine Abstract Machine. - -.. tacn:: unfold @qualid - :name: unfold - - This tactic applies to any goal. The argument qualid must denote a - defined transparent constant or local definition (see - :ref:`gallina-definitions` and - :ref:`vernac-controlling-the-reduction-strategies`). The tactic - :tacn:`unfold` applies the :math:`\delta` rule to each occurrence - of the constant to which :n:`@qualid` refers in the current goal - and then replaces it with its :math:`\beta\iota\zeta`-normal form. - Use the general reduction tactics if you want to avoid this final - reduction, for instance :n:`cbv delta [@qualid]`. - - .. exn:: Cannot coerce @qualid to an evaluable reference. - - This error is frequent when trying to unfold something that has - defined as an inductive type (or constructor) and not as a - definition. - - .. example:: - - .. coqtop:: abort all fail - - Goal 0 <= 1. - unfold le. - - This error can also be raised if you are trying to unfold - something that has been marked as opaque. - - .. example:: - - .. coqtop:: abort all fail - - Opaque Nat.add. - Goal 1 + 0 = 1. - unfold Nat.add. - - .. tacv:: unfold @qualid in @goal_occurrences - - Replaces :n:`@qualid` in hypothesis (or hypotheses) designated - by :token:`goal_occurrences` with its definition and replaces - the hypothesis with its :math:`\beta`:math:`\iota` normal form. - - .. tacv:: unfold {+, @qualid} - - Replaces :n:`{+, @qualid}` with their definitions and replaces - the current goal with its :math:`\beta`:math:`\iota` normal - form. - - .. tacv:: unfold {+, @qualid at @occurrences } - - The list :token:`occurrences` specify the occurrences of - :n:`@qualid` to be unfolded. Occurrences are located from left - to right. - - .. exn:: Bad occurrence number of @qualid. - :undocumented: - - .. exn:: @qualid does not occur. - :undocumented: - - .. tacv:: unfold @string - - If :n:`@string` denotes the discriminating symbol of a notation - (e.g. "+") or an expression defining a notation (e.g. `"_ + - _"`), and this notation denotes an application whose head symbol - is an unfoldable constant, then the tactic unfolds it. - - .. tacv:: unfold @string%@ident - - This is variant of :n:`unfold @string` where :n:`@string` gets - its interpretation from the scope bound to the delimiting key - :token:`ident` instead of its default interpretation (see - :ref:`Localinterpretationrulesfornotations`). - - .. tacv:: unfold {+, {| @qualid | @string{? %@ident } } {? at @occurrences } } {? in @goal_occurrences } - - This is the most general form. - -.. tacn:: fold @term - :name: fold - - This tactic applies to any goal. The term :n:`@term` is reduced using the - :tacn:`red` tactic. Every occurrence of the resulting :n:`@term` in the goal is - then replaced by :n:`@term`. This tactic is particularly useful when a fixpoint - definition has been wrongfully unfolded, making the goal very hard to read. - On the other hand, when an unfolded function applied to its argument has been - reduced, the :tacn:`fold` tactic won't do anything. - - .. example:: - - .. coqtop:: all abort - - Goal ~0=0. - unfold not. - Fail progress fold not. - pattern (0 = 0). - fold not. - - .. tacv:: fold {+ @term} - - Equivalent to :n:`fold @term ; ... ; fold @term`. - -.. tacn:: pattern @term - :name: pattern - - This command applies to any goal. The argument :n:`@term` must be a free - subterm of the current goal. The command pattern performs :math:`\beta`-expansion - (the inverse of :math:`\beta`-reduction) of the current goal (say :g:`T`) by - - + replacing all occurrences of :n:`@term` in :g:`T` with a fresh variable - + abstracting this variable - + applying the abstracted goal to :n:`@term` - - For instance, if the current goal :g:`T` is expressible as - :math:`\varphi`:g:`(t)` where the notation captures all the instances of :g:`t` - in :math:`\varphi`:g:`(t)`, then :n:`pattern t` transforms it into - :g:`(fun x:A =>` :math:`\varphi`:g:`(x)) t`. This tactic can be used, for - instance, when the tactic ``apply`` fails on matching. - -.. tacv:: pattern @term at {+ @num} - - Only the occurrences :n:`{+ @num}` of :n:`@term` are considered for - :math:`\beta`-expansion. Occurrences are located from left to right. - -.. tacv:: pattern @term at - {+ @num} - - All occurrences except the occurrences of indexes :n:`{+ @num }` - of :n:`@term` are considered for :math:`\beta`-expansion. Occurrences are located from - left to right. - -.. tacv:: pattern {+, @term} - - Starting from a goal :math:`\varphi`:g:`(t`:sub:`1` :g:`... t`:sub:`m`:g:`)`, - the tactic :n:`pattern t`:sub:`1`:n:`, ..., t`:sub:`m` generates the - equivalent goal - :g:`(fun (x`:sub:`1`:g:`:A`:sub:`1`:g:`) ... (x`:sub:`m` :g:`:A`:sub:`m` :g:`) =>`:math:`\varphi`:g:`(x`:sub:`1` :g:`... x`:sub:`m` :g:`)) t`:sub:`1` :g:`... t`:sub:`m`. - If :g:`t`:sub:`i` occurs in one of the generated types :g:`A`:sub:`j` these - occurrences will also be considered and possibly abstracted. - -.. tacv:: pattern {+, @term at {+ @num}} - - This behaves as above but processing only the occurrences :n:`{+ @num}` of - :n:`@term` starting from :n:`@term`. - -.. tacv:: pattern {+, @term {? at {? -} {+, @num}}} - - This is the most general syntax that combines the different variants. - -Conversion tactics applied to hypotheses -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -.. tacn:: @tactic in {+, @ident} - - Applies :token:`tactic` (any of the conversion tactics listed in this - section) to the hypotheses :n:`{+ @ident}`. - - If :token:`ident` is a local definition, then :token:`ident` can be replaced by - :n:`type of @ident` to address not the body but the type of the local - definition. - - Example: :n:`unfold not in (type of H1) (type of H3)`. - -.. 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 @num - - Forces the search depth to be :token:`num`. 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 ` 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 {? @num} {? 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 {? @num} {? 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 ` - - -.. 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 ` 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 `). 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 `), - 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 {? | {? @num} {? @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:`@num` 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 @num {? @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: - - .. productionlist:: regexp - 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. When required, the module Omega also extends the - database zarith with a high-cost hint that calls ``omega`` 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 {+ @term} using @tactic : {+ @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 imported (using e.g. ``Require Import 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 @num - :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 @num - - Tries to add at most :token:`num` instances of hypotheses stating quantified equalities - to the problem in order to solve it. A bigger value of :token:`num` 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 `). - -.. 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 --------------------------- -- cgit v1.2.3 From 042800c30d380f11041867e09ee4ba5e3625d3ff Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Tue, 21 Apr 2020 16:53:35 +0200 Subject: Remove parts of the Tactics chapter. --- doc/sphinx/proof-engine/tactics.rst | 459 ------------------------------------ 1 file changed, 459 deletions(-) (limited to 'doc') diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 439be0ecf8..adabc56c50 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -53,89 +53,6 @@ .. exn:: Not the right number of induction arguments. :undocumented: -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 @num - - This does the same thing as :n:`intros until @num` then - :n:`simplify_eq @ident` where :n:`@ident` is the identifier for the last - introduced hypothesis. - -.. tacv:: simplify_eq @term with @bindings_list - - 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 @num - esimplify_eq @term {? with @bindings_list} - :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:`@num`, 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. - -Inversion ---------- - .. tacn:: functional inversion @ident :name: functional inversion @@ -168,379 +85,3 @@ Inversion :n:`@qualid__1` and :n:`@qualid__2` are valid candidates to functional inversion, this variant allows choosing which :token:`qualid` is inverted. - -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: - - .. _btauto_grammar: - - .. productionlist:: sentence - 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. - -.. tacn:: omega - :name: omega - - The tactic :tacn:`omega`, due to Pierre Crégut, is an automatic decision - procedure for Presburger arithmetic. It solves quantifier-free - formulas built with `~`, `\\/`, `/\\`, `->` on top of equalities, - inequalities and disequalities on both the type :g:`nat` of natural numbers - and :g:`Z` of binary integers. This tactic must be loaded by the command - ``Require Import Omega``. See the additional documentation about omega - (see Chapter :ref:`omega`). - - -.. tacn:: ring - :name: ring - - This tactic solves equations upon polynomial expressions of a ring - (or semiring) structure. It proceeds by normalizing both hand sides - of the equation (w.r.t. associativity, commutativity and - distributivity, constant propagation) and comparing syntactically the - results. - -.. tacn:: ring_simplify {* @term} - :name: ring_simplify - - This tactic applies the normalization procedure described above to - the given terms. The tactic then replaces all occurrences of the terms - given in the conclusion of the goal by their normal forms. If no term - is given, then the conclusion should be an equation and both hand - sides are normalized. - -See :ref:`Theringandfieldtacticfamilies` for more information on -the tactic and how to declare new ring structures. All declared field structures -can be printed with the ``Print Rings`` command. - -.. tacn:: field - field_simplify {* @term} - field_simplify_eq - :name: field; field_simplify; 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/setoid_ring/RealField.v for an example of instantiation, - theory theories/Reals for many examples of use of field. - -Non-logical tactics ------------------------- - - -.. tacn:: cycle @num - :name: cycle - - This tactic puts the :n:`@num` first goals at the end of the list of goals. - If :n:`@num` is negative, it will put the last :math:`|num|` goals at the - beginning of the list. - -.. 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 @num @num - :name: swap - - This tactic switches the position of the goals of indices :n:`@num` and - :n:`@num`. If either :n:`@num` or :n:`@num` is negative then goals are - counted from the end of the focused goal list. Goals are indexed from 1, - there is no goal with position 0. - -.. 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 - - This tactics reverses the list of the focused goals. - - .. 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 :n:`change @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 :g:`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 `change`'s variants. - - .. tacv:: change_no_check @term with @term’ - :undocumented: - - .. tacv:: change_no_check @term at {+ @num} with @term’ - :undocumented: - - .. tacv:: change_no_check @term {? {? at {+ @num}} 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 :n:`exact @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 explanations. - - .. 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 :n:`exact_no_check @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 :n:`exact_no_check @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. -- cgit v1.2.3 From 3d0c9b418d88b698e1446c10a26e00686a71a0a8 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Tue, 21 Apr 2020 17:26:23 +0200 Subject: Extract funind tactics to funind section of the Libraries chapter. --- doc/sphinx/proof-engine/tactics.rst | 87 ----------------------------------- doc/sphinx/using/libraries/funind.rst | 87 +++++++++++++++++++++++++++++++++++ 2 files changed, 87 insertions(+), 87 deletions(-) delete mode 100644 doc/sphinx/proof-engine/tactics.rst create mode 100644 doc/sphinx/using/libraries/funind.rst (limited to 'doc') diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst deleted file mode 100644 index adabc56c50..0000000000 --- a/doc/sphinx/proof-engine/tactics.rst +++ /dev/null @@ -1,87 +0,0 @@ -.. tacn:: function induction (@qualid {+ @term}) - :name: function induction - - The tactic functional induction performs case analysis and induction - following the definition of a function. It makes use of a principle - generated by ``Function`` (see :ref:`advanced-recursive-functions`) or - ``Functional Scheme`` (see :ref:`functional-scheme`). - Note that this tactic is only available after a ``Require Import FunInd``. - -.. example:: - - .. coqtop:: reset all - - Require Import FunInd. - Functional Scheme minus_ind := Induction for minus Sort Prop. - Check minus_ind. - Lemma le_minus (n m:nat) : n - m <= n. - functional induction (minus n m) using minus_ind; simpl; auto. - Qed. - -.. note:: - :n:`(@qualid {+ @term})` must be a correct full application - of :n:`@qualid`. In particular, the rules for implicit arguments are the - same as usual. For example use :n:`@qualid` if you want to write implicit - arguments explicitly. - -.. note:: - Parentheses around :n:`@qualid {+ @term}` are not mandatory and can be skipped. - -.. note:: - :n:`functional induction (f x1 x2 x3)` is actually a wrapper for - :n:`induction x1, x2, x3, (f x1 x2 x3) using @qualid` followed by a cleaning - phase, where :n:`@qualid` is the induction principle registered for :g:`f` - (by the ``Function`` (see :ref:`advanced-recursive-functions`) or - ``Functional Scheme`` (see :ref:`functional-scheme`) - command) corresponding to the sort of the goal. Therefore - ``functional induction`` may fail if the induction scheme :n:`@qualid` is not - defined. See also :ref:`advanced-recursive-functions` for the function - terms accepted by ``Function``. - -.. note:: - There is a difference between obtaining an induction scheme - for a function by using :g:`Function` (see :ref:`advanced-recursive-functions`) - and by using :g:`Functional Scheme` after a normal definition using - :g:`Fixpoint` or :g:`Definition`. See :ref:`advanced-recursive-functions` - for details. - -.. seealso:: :ref:`advanced-recursive-functions`, :ref:`functional-scheme` and :tacn:`inversion` - -.. exn:: Cannot find induction information on @qualid. - :undocumented: - -.. exn:: Not the right number of induction arguments. - :undocumented: - -.. tacn:: functional inversion @ident - :name: functional inversion - - :tacn:`functional inversion` is a tactic that performs inversion on hypothesis - :n:`@ident` of the form :n:`@qualid {+ @term} = @term` or :n:`@term = @qualid - {+ @term}` where :n:`@qualid` must have been defined using Function (see - :ref:`advanced-recursive-functions`). Note that this tactic is only - available after a ``Require Import FunInd``. - - .. exn:: Hypothesis @ident must contain at least one Function. - :undocumented: - - .. exn:: Cannot find inversion information for hypothesis @ident. - - This error may be raised when some inversion lemma failed to be generated by - Function. - - - .. tacv:: functional inversion @num - - This does the same thing as :n:`intros until @num` followed by - :n:`functional inversion @ident` where :token:`ident` is the - identifier for the last introduced hypothesis. - - .. tacv:: functional inversion @ident @qualid - functional inversion @num @qualid - - If the hypothesis :token:`ident` (or :token:`num`) has a type of the form - :n:`@qualid__1 {+ @term__i } = @qualid__2 {+ @term__j }` where - :n:`@qualid__1` and :n:`@qualid__2` are valid candidates to - functional inversion, this variant allows choosing which :token:`qualid` - is inverted. diff --git a/doc/sphinx/using/libraries/funind.rst b/doc/sphinx/using/libraries/funind.rst new file mode 100644 index 0000000000..adabc56c50 --- /dev/null +++ b/doc/sphinx/using/libraries/funind.rst @@ -0,0 +1,87 @@ +.. tacn:: function induction (@qualid {+ @term}) + :name: function induction + + The tactic functional induction performs case analysis and induction + following the definition of a function. It makes use of a principle + generated by ``Function`` (see :ref:`advanced-recursive-functions`) or + ``Functional Scheme`` (see :ref:`functional-scheme`). + Note that this tactic is only available after a ``Require Import FunInd``. + +.. example:: + + .. coqtop:: reset all + + Require Import FunInd. + Functional Scheme minus_ind := Induction for minus Sort Prop. + Check minus_ind. + Lemma le_minus (n m:nat) : n - m <= n. + functional induction (minus n m) using minus_ind; simpl; auto. + Qed. + +.. note:: + :n:`(@qualid {+ @term})` must be a correct full application + of :n:`@qualid`. In particular, the rules for implicit arguments are the + same as usual. For example use :n:`@qualid` if you want to write implicit + arguments explicitly. + +.. note:: + Parentheses around :n:`@qualid {+ @term}` are not mandatory and can be skipped. + +.. note:: + :n:`functional induction (f x1 x2 x3)` is actually a wrapper for + :n:`induction x1, x2, x3, (f x1 x2 x3) using @qualid` followed by a cleaning + phase, where :n:`@qualid` is the induction principle registered for :g:`f` + (by the ``Function`` (see :ref:`advanced-recursive-functions`) or + ``Functional Scheme`` (see :ref:`functional-scheme`) + command) corresponding to the sort of the goal. Therefore + ``functional induction`` may fail if the induction scheme :n:`@qualid` is not + defined. See also :ref:`advanced-recursive-functions` for the function + terms accepted by ``Function``. + +.. note:: + There is a difference between obtaining an induction scheme + for a function by using :g:`Function` (see :ref:`advanced-recursive-functions`) + and by using :g:`Functional Scheme` after a normal definition using + :g:`Fixpoint` or :g:`Definition`. See :ref:`advanced-recursive-functions` + for details. + +.. seealso:: :ref:`advanced-recursive-functions`, :ref:`functional-scheme` and :tacn:`inversion` + +.. exn:: Cannot find induction information on @qualid. + :undocumented: + +.. exn:: Not the right number of induction arguments. + :undocumented: + +.. tacn:: functional inversion @ident + :name: functional inversion + + :tacn:`functional inversion` is a tactic that performs inversion on hypothesis + :n:`@ident` of the form :n:`@qualid {+ @term} = @term` or :n:`@term = @qualid + {+ @term}` where :n:`@qualid` must have been defined using Function (see + :ref:`advanced-recursive-functions`). Note that this tactic is only + available after a ``Require Import FunInd``. + + .. exn:: Hypothesis @ident must contain at least one Function. + :undocumented: + + .. exn:: Cannot find inversion information for hypothesis @ident. + + This error may be raised when some inversion lemma failed to be generated by + Function. + + + .. tacv:: functional inversion @num + + This does the same thing as :n:`intros until @num` followed by + :n:`functional inversion @ident` where :token:`ident` is the + identifier for the last introduced hypothesis. + + .. tacv:: functional inversion @ident @qualid + functional inversion @num @qualid + + If the hypothesis :token:`ident` (or :token:`num`) has a type of the form + :n:`@qualid__1 {+ @term__i } = @qualid__2 {+ @term__j }` where + :n:`@qualid__1` and :n:`@qualid__2` are valid candidates to + functional inversion, this variant allows choosing which :token:`qualid` + is inverted. -- cgit v1.2.3