| products/Sources/formale Sprachen/Coq/doc/sphinx/proof-engine/ |
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei: DoubleStreamTestDataProvider.java Sprache: Unknown
|
Columbo aufrufen.rst zum Wurzelverzeichnis wechselnHaskell {Haskell[399] Ada[642] Abap[905]}Datei anzeigen .. _thessreflectprooflanguage: ------------------------------ The |SSR| proof language ------------------------------ :Authors: Georges Gonthier, Assia Mahboubi, Enrico Tassi Introduction ------------ This chapter describes a set of tactics known as |SSR| originally designed to provide support for the so-called *small scale reflection* proof methodology. Despite the original purpose this set of tactic is of general interest and is available in |Coq| starting from version 8.7. |SSR| was developed independently of the tactics described in Chapter :ref:`tactics`. Indeed the scope of the tactics part of |SSR| largely overlaps with the standard set of tactics. Eventually the overlap will be reduced in future releases of |Coq|. Proofs written in |SSR| typically look quite different from the ones written using only tactics as per Chapter :ref:`tactics`. We try to summarise here the most “visible” ones in order to help the reader already accustomed to the tactics described in Chapter :ref:`tactics` to read this chapter. The first difference between the tactics described in this chapter and the tactics described in Chapter :ref:`tactics` is the way hypotheses are managed (we call this *bookkeeping*). In Chapter :ref:`tactics` the most common approach is to avoid moving explicitly hypotheses back and forth between the context and the conclusion of the goal. On the contrary in |SSR| all bookkeeping is performed on the conclusion of the goal, using for that purpose a couple of syntactic constructions behaving similar to tacticals (and often named as such in this chapter). The ``:`` tactical moves hypotheses from the context to the conclusion, while ``=>`` moves hypotheses from the conclusion to the context, and ``in`` moves back and forth a hypothesis from the context to the conclusion for the time of applying an action to it. While naming hypotheses is commonly done by means of an ``as`` clause in the basic model of Chapter :ref:`tactics`, it is here to ``=>`` that this task is devoted. Tactics frequently leave new assumptions in the conclusion, and are often followed by ``=>`` to explicitly name them. While generalizing the goal is normally not explicitly needed in Chapter :ref:`tactics`, it is an explicit operation performed by ``:``. .. seealso:: :ref:`bookkeeping_ssr` Beside the difference of bookkeeping model, this chapter includes specific tactics which have no explicit counterpart in Chapter :ref:`tactics` such as tactics to mix forward steps and generalizations as :tacn:`generally have` or :tacn:`without loss`. |SSR| adopts the point of view that rewriting, definition expansion and partial evaluation participate all to a same concept of rewriting a goal in a larger sense. As such, all these functionalities are provided by the :tacn:`rewrite <rewrite (ssreflect)>` tactic. |SSR| includes a little language of patterns to select subterms in tactics or tacticals where it matters. Its most notable application is in the :tacn:`rewrite <rewrite (ssreflect)>` tactic, where patterns are used to specify where the rewriting step has to take place. Finally, |SSR| supports so-called reflection steps, typically allowing to switch back and forth between the computational view and logical view of a concept. To conclude it is worth mentioning that |SSR| tactics can be mixed with non |SSR| tactics in the same proof, or in the same Ltac expression. The few exceptions to this statement are described in section :ref:`compatibility_issues_ssr`. Acknowledgments ~~~~~~~~~~~~~~~ The authors would like to thank Frédéric Blanqui, François Pottier and Laurence Rideau for their comments and suggestions. Usage ----- Getting started ~~~~~~~~~~~~~~~ To be available, the tactics presented in this manual need the following minimal set of libraries to be loaded: ``ssreflect.v``, ``ssrfun.v`` and ``ssrbool.v``. Moreover, these tactics come with a methodology specific to the authors of |SSR| and which requires a few options to be set in a different way than in their default way. All in all, this corresponds to working in the following context: .. coqtop:: in From Coq Require Import ssreflect ssrfun ssrbool. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. .. seealso:: :flag:`Implicit Arguments`, :flag:`Strict Implicit`, :flag:`Printing Implicit Defensive` .. _compatibility_issues_ssr: Compatibility issues ~~~~~~~~~~~~~~~~~~~~ Requiring the above modules creates an environment which is mostly compatible with the rest of |Coq|, up to a few discrepancies: + New keywords (``is``) might clash with variable, constant, tactic or tactical names, or with quasi-keywords in tactic or vernacular notations. + New tactic(al)s names (:tacn:`last`, :tacn:`done`, :tacn:`have`, :tacn:`suffices`, :tacn:`suff`, :tacn:`without loss`, :tacn:`wlog`, :tacn:`congr`, :tacn:`unlock`) might clash with user tactic names. + Identifiers with both leading and trailing ``_``, such as ``_x_``, are reserved by |SSR| and cannot appear in scripts. + The extensions to the :tacn:`rewrite` tactic are partly incompatible with those available in current versions of |Coq|; in particular: ``rewrite .. in (type of k)`` or ``rewrite .. in *`` or any other variant of :tacn:`rewrite` will not work, and the |SSR| syntax and semantics for occurrence selection and rule chaining is different. Use an explicit rewrite direction (``rewrite <- …`` or ``rewrite -> …``) to access the |Coq| rewrite tactic. + New symbols (``//``, ``/=``, ``//=``) might clash with adjacent existing symbols. This can be avoided by inserting white spaces. + New constant and theorem names might clash with the user theory. This can be avoided by not importing all of |SSR|: .. coqtop:: in From Coq Require ssreflect. Import ssreflect.SsrSyntax. Note that the full syntax of |SSR|’s rewrite and reserved identifiers are enabled only if the ssreflect module has been required and if ``SsrSyntax`` has been imported. Thus a file that requires (without importing) ``ssreflect`` and imports ``SsrSyntax``, can be required and imported without automatically enabling |SSR|’s extended rewrite syntax and reserved identifiers. + Some user notations (in particular, defining an infix ``;``) might interfere with the "open term", parenthesis free, syntax of tactics such as have, set and pose. + The generalization of if statements to non-Boolean conditions is turned off by |SSR|, because it is mostly subsumed by Coercion to ``bool`` of the ``sumXXX`` types (declared in ``ssrfun.v``) and the :n:`if @term is @pattern then @term else @term` construct (see :ref:`pattern_conditional_ssr`). To use the generalized form, turn off the |SSR| Boolean ``if`` notation using the command: ``Close Scope boolean_if_scope``. + The following flags can be unset to make |SSR| more compatible with parts of Coq: .. flag:: SsrRewrite Controls whether the incompatible rewrite syntax is enabled (the default). Disabling the flag makes the syntax compatible with other parts of Coq. .. flag:: SsrIdents Controls whether tactics can refer to |SSR|-generated variables that are in the form _xxx_. Scripts with explicit references to such variables are fragile; they are prone to failure if the proof is later modified or if the details of variable name generation change in future releases of Coq. The default is on, which gives an error message when the user tries to create such identifiers. Disabling the flag generates a warning instead, increasing compatibility with other parts of Coq. |Gallina| extensions -------------------- Small-scale reflection makes an extensive use of the programming subset of |Gallina|, |Coq|’s logical specification language. This subset is quite suited to the description of functions on representations, because it closely follows the well-established design of the ML programming language. The |SSR| extension provides three additions to |Gallina|, for pattern assignment, pattern testing, and polymorphism; these mitigate minor but annoying discrepancies between |Gallina| and ML. Pattern assignment ~~~~~~~~~~~~~~~~~~ The |SSR| extension provides the following construct for irrefutable pattern matching, that is, destructuring assignment: .. prodn:: term += let: @pattern := @term in @term Note the colon ``:`` after the ``let`` keyword, which avoids any ambiguity with a function definition or |Coq|’s basic destructuring let. The let: construct differs from the latter in that + The pattern can be nested (deep pattern matching), in particular, this allows expression of the form: .. coqdoc:: let: exist (x, y) p_xy := Hp in … . + The destructured constructor is explicitly given in the pattern, and is used for type inference. .. example:: .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. .. coqtop:: all Definition f u := let: (m, n) := u in m + n. Check f. Using :g:`let:` Coq infers a type for :g:`f`, whereas with a usual ``let`` the same term requires an extra type annotation in order to type check. .. coqtop:: reset all Fail Definition f u := let (m, n) := u in m + n. The ``let:`` construct is just (more legible) notation for the primitive |Gallina| expression :n:`match @term with @pattern => @term end`. The |SSR| destructuring assignment supports all the dependent match annotations; the full syntax is .. prodn:: term += let: @pattern {? as @ident} {? in @pattern} := @term {? return @term} in @term where the second :token:`pattern` and the second :token:`term` are *types*. When the ``as`` and ``return`` keywords are both present, then :token:`ident` is bound in both the second :token:`pattern` and the second :token:`term`; variables in the optional type :token:`pattern` are bound only in the second term, and other variables in the first :token:`pattern` are bound only in the third :token:`term`, however. .. _pattern_conditional_ssr: Pattern conditional ~~~~~~~~~~~~~~~~~~~ The following construct can be used for a refutable pattern matching, that is, pattern testing: .. prodn:: term += if @term is @pattern then @term else @term Although this construct is not strictly ML (it does exist in variants such as the pattern calculus or the ρ-calculus), it turns out to be very convenient for writing functions on representations, because most such functions manipulate simple data types such as Peano integers, options, lists, or binary trees, and the pattern conditional above is almost always the right construct for analyzing such simple types. For example, the null and all list function(al)s can be defined as follows: .. example:: .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. Section Test. .. coqtop:: all Variable d: Set. Fixpoint null (s : list d) := if s is nil then true else false. Variable a : d -> bool. Fixpoint all (s : list d) : bool := if s is cons x s' then a x && all s' else true. The pattern conditional also provides a notation for destructuring assignment with a refutable pattern, adapted to the pure functional setting of |Gallina|, which lacks a ``Match_Failure`` exception. Like ``let:`` above, the ``if…is`` construct is just (more legible) notation for the primitive |Gallina| expression :n:`match @term with @pattern => @term | _ => @term end`. Similarly, it will always be displayed as the expansion of this form in terms of primitive match expressions (where the default expression may be replicated). Explicit pattern testing also largely subsumes the generalization of the ``if`` construct to all binary data types; compare :n:`if @term is inl _ then @term else @term` and :n:`if @term then @term else @term`. The latter appears to be marginally shorter, but it is quite ambiguous, and indeed often requires an explicit annotation ``(term : {_} + {_})`` to type check, which evens the character count. Therefore, |SSR| restricts by default the condition of a plain if construct to the standard ``bool`` type; this avoids spurious type annotations. .. example:: .. coqtop:: all Definition orb b1 b2 := if b1 then true else b2. As pointed out in section :ref:`compatibility_issues_ssr`, this restriction can be removed with the command: ``Close Scope boolean_if_scope.`` Like ``let:`` above, the ``if-is-then-else`` construct supports the dependent match annotations: .. prodn:: term += if @term is @pattern as @ident in @pattern return @term then @term else @term As in ``let:`` the variable :token:`ident` (and those in the type pattern) are bound in the second :token:`term`; :token:`ident` is also bound in the third :token:`term` (but not in the fourth :token:`term`), while the variables in the first :token:`pattern` are bound only in the third :token:`term`. Another variant allows to treat the ``else`` case first: .. prodn:: term += if @term isn't @pattern then @term else @term Note that :token:`pattern` eventually binds variables in the third :token:`term` and not in the second :token:`term`. .. _parametric_polymorphism_ssr: Parametric polymorphism ~~~~~~~~~~~~~~~~~~~~~~~ Unlike ML, polymorphism in core |Gallina| is explicit: the type parameters of polymorphic functions must be declared explicitly, and supplied at each point of use. However, |Coq| provides two features to suppress redundant parameters: + Sections are used to provide (possibly implicit) parameters for a set of definitions. + Implicit arguments declarations are used to tell |Coq| to use type inference to deduce some parameters from the context at each point of call. The combination of these features provides a fairly good emulation of ML-style polymorphism, but unfortunately this emulation breaks down for higher-order programming. Implicit arguments are indeed not inferred at all points of use, but only at points of call, leading to expressions such as .. example:: .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. Section Test. Variable T : Type. Variable null : forall T : Type, T -> bool. Variable all : (T -> bool) -> list T -> bool. .. coqtop:: all Definition all_null (s : list T) := all (@null T) s. Unfortunately, such higher-order expressions are quite frequent in representation functions, especially those which use |Coq|'s ``Structures`` to emulate Haskell typeclasses. Therefore, |SSR| provides a variant of |Coq|’s implicit argument declaration, which causes |Coq| to fill in some implicit parameters at each point of use, e.g., the above definition can be written: .. example:: .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. Section Test. Variable T : Type. Variable null : forall T : Type, T -> bool. Variable all : (T -> bool) -> list T -> bool. .. coqtop:: all Prenex Implicits null. Definition all_null (s : list T) := all null s. Better yet, it can be omitted entirely, since :g:`all_null s` isn’t much of an improvement over :g:`all null s`. The syntax of the new declaration is .. cmd:: Prenex Implicits {+ @ident__i} This command checks that each :n:`@ident__i` is the name of a functional constant, whose implicit arguments are prenex, i.e., the first :math:`n_i > 0` arguments of :n:`@ident__i` are implicit; then it assigns ``Maximal Implicit`` status to these arguments. As these prenex implicit arguments are ubiquitous and have often large display strings, it is strongly recommended to change the default display settings of |Coq| so that they are not printed (except after a ``Set Printing All`` command). All |SSR| library files thus start with the incantation .. coqdoc:: Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. Anonymous arguments ~~~~~~~~~~~~~~~~~~~ When in a definition, the type of a certain argument is mandatory, but not its name, one usually uses “arrow” abstractions for prenex arguments, or the ``(_ : term)`` syntax for inner arguments. In |SSR|, the latter can be replaced by the open syntax ``of term`` or (equivalently) ``& term``, which are both syntactically equivalent to a ``(_ : term)`` expression. This feature almost behaves as the following extension of the binder syntax: .. prodn:: binder += {| & @term | of @term } Caveat: ``& T`` and ``of T`` abbreviations have to appear at the end of a binder list. For instance, the usual two-constructor polymorphic type list, i.e. the one of the standard ``List`` library, can be defined by the following declaration: .. example:: .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. .. coqtop:: all Inductive list (A : Type) : Type := nil | cons of A & list A. Wildcards ~~~~~~~~~ The terms passed as arguments to |SSR| tactics can contain *holes*, materialized by wildcards ``_``. Since |SSR| allows a more powerful form of type inference for these arguments, it enhances the possibilities of using such wildcards. These holes are in particular used as a convenient shorthand for abstractions, especially in local definitions or type expressions. Wildcards may be interpreted as abstractions (see for example sections :ref:`definitions_ssr` and :ref:`structure_ssr`), or their content can be inferred from the whole context of the goal (see for example section :ref:`abbreviations_ssr`). .. _definitions_ssr: Definitions ~~~~~~~~~~~ .. tacn:: pose :name: pose (ssreflect) This tactic allows to add a defined constant to a proof context. |SSR| generalizes this tactic in several ways. In particular, the |SSR| pose tactic supports *open syntax*: the body of the definition does not need surrounding parentheses. For instance: .. coqdoc:: pose t := x + y. is a valid tactic expression. The pose tactic is also improved for the local definition of higher order terms. Local definitions of functions can use the same syntax as global ones. For example, the tactic :tacn:`pose <pose (ssreflect)>` supports parameters: .. example:: .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. .. coqtop:: all Lemma test : True. pose f x y := x + y. The |SSR| pose tactic also supports (co)fixpoints, by providing the local counterpart of the ``Fixpoint f := …`` and ``CoFixpoint f := …`` constructs. For instance, the following tactic: .. coqdoc:: pose fix f (x y : nat) {struct x} : nat := if x is S p then S (f p y) else 0. defines a local fixpoint ``f``, which mimics the standard plus operation on natural numbers. Similarly, local cofixpoints can be defined by a tactic of the form: .. coqdoc:: pose cofix f (arg : T) := … . The possibility to include wildcards in the body of the definitions offers a smooth way of defining local abstractions. The type of “holes” is guessed by type inference, and the holes are abstracted. For instance the tactic: .. coqdoc:: pose f := _ + 1. is shorthand for: .. coqdoc:: pose f n := n + 1. When the local definition of a function involves both arguments and holes, hole abstractions appear first. For instance, the tactic: .. coqdoc:: pose f x := x + _. is shorthand for: .. coqdoc:: pose f n x := x + n. The interaction of the pose tactic with the interpretation of implicit arguments results in a powerful and concise syntax for local definitions involving dependent types. For instance, the tactic: .. coqdoc:: pose f x y := (x, y). adds to the context the local definition: .. coqdoc:: pose f (Tx Ty : Type) (x : Tx) (y : Ty) := (x, y). The generalization of wildcards makes the use of the pose tactic resemble ML-like definitions of polymorphic functions. .. _abbreviations_ssr: Abbreviations ~~~~~~~~~~~~~ .. tacn:: set @ident {? : @term } := {? @occ_switch } @term :name: set (ssreflect) The |SSR| ``set`` tactic performs abbreviations: it introduces a defined constant for a subterm appearing in the goal and/or in the context. |SSR| extends the :tacn:`set` tactic by supplying: + an open syntax, similarly to the :tacn:`pose (ssreflect)` tactic; + a more aggressive matching algorithm; + an improved interpretation of wildcards, taking advantage of the matching algorithm; + an improved occurrence selection mechanism allowing to abstract only selected occurrences of a term. .. prodn:: occ_switch ::= { {? {| + | - } } {* @num } } where: + :token:`ident` is a fresh identifier chosen by the user. + term 1 is an optional type annotation. The type annotation term 1 can be given in open syntax (no surrounding parentheses). If no :token:`occ_switch` (described hereafter) is present, it is also the case for the second :token:`term`. On the other hand, in presence of :token:`occ_switch`, parentheses surrounding the second :token:`term` are mandatory. + In the occurrence switch :token:`occ_switch`, if the first element of the list is a natural, this element should be a number, and not an Ltac variable. The empty list ``{}`` is not interpreted as a valid occurrence switch, it is rather used as a flag to signal the intent of the user to clear the name following it (see :ref:`ssr_rewrite_occ_switch` and :ref:`introduction_ssr`) The tactic: .. example:: .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. Axiom f : nat -> nat. .. coqtop:: all Lemma test x : f x + f x = f x. set t := f _. .. coqtop:: all restart set t := {2}(f _). The type annotation may contain wildcards, which will be filled with the appropriate value by the matching process. The tactic first tries to find a subterm of the goal matching the second :token:`term` (and its type), and stops at the first subterm it finds. Then the occurrences of this subterm selected by the optional :token:`occ_switch` are replaced by :token:`ident` and a definition :n:`@ident := @term` is added to the context. If no :token:`occ_switch` is present, then all the occurrences are abstracted. Matching ```````` The matching algorithm compares a pattern :token:`term` with a subterm of the goal by comparing their heads and then pairwise unifying their arguments (modulo conversion). Head symbols match under the following conditions: + If the head of :token:`term` is a constant, then it should be syntactically equal to the head symbol of the subterm. + If this head is a projection of a canonical structure, then canonical structure equations are used for the matching. + If the head of term is *not* a constant, the subterm should have the same structure (λ abstraction, let…in structure …). + If the head of :token:`term` is a hole, the subterm should have at least as many arguments as :token:`term`. .. example:: .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. .. coqtop:: all Lemma test (x y z : nat) : x + y = z. set t := _ x. + In the special case where ``term`` is of the form ``(let f := t0 in f) t1 … tn`` , then the pattern ``term`` is treated as ``(_ t1 … tn)``. For each subterm in the goal having the form ``(A u1 … um)`` with m ≥ n, the matching algorithm successively tries to find the largest partial application ``(A u1 … uj)`` convertible to the head ``t0`` of ``term``. .. example:: .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. .. coqtop:: all Lemma test : (let f x y z := x + y + z in f 1) 2 3 = 6. set t := (let g y z := S y + z in g) 2. The notation ``unkeyed`` defined in ``ssreflect.v`` is a shorthand for the degenerate term ``let x := … in x``. Moreover: + Multiple holes in ``term`` are treated as independent placeholders. .. example:: .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. .. coqtop:: all Lemma test x y z : x + y = z. set t := _ + _. + The type of the subterm matched should fit the type (possibly casted by some type annotations) of the pattern ``term``. + The replacement of the subterm found by the instantiated pattern should not capture variables. In the example above ``x`` is bound and should not be captured. .. example:: .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. .. coqtop:: all Lemma test : forall x : nat, x + 1 = 0. Fail set t := _ + 1. + Typeclass inference should fill in any residual hole, but matching should never assign a value to a global existential variable. .. _occurrence_selection_ssr: Occurrence selection ```````````````````` |SSR| provides a generic syntax for the selection of occurrences by their position indexes. These *occurrence switches* are shared by all |SSR| tactics which require control on subterm selection like rewriting, generalization, … An *occurrence switch* can be: + A list natural numbers ``{+ n1 … nm}`` of occurrences affected by the tactic. .. example:: .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. Axiom f : nat -> nat. .. coqtop:: all Lemma test : f 2 + f 8 = f 2 + f 2. set x := {+1 3}(f 2). Notice that some occurrences of a given term may be hidden to the user, for example because of a notation. The vernacular ``Set Printing All`` command displays all these hidden occurrences and should be used to find the correct coding of the occurrences to be selected [#1]_. .. example:: .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. .. coqtop:: all Notation "a < b":= (le (S a) b). Lemma test x y : x < y -> S x < S y. set t := S x. + A list of natural numbers between ``{n1 … nm}``. This is equivalent to the previous ``{+ n1 … nm}`` but the list should start with a number, and not with an Ltac variable. + A list ``{- n1 … nm}`` of occurrences *not* to be affected by the tactic. .. example:: .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. Axiom f : nat -> nat. .. coqtop:: all Lemma test : f 2 + f 8 = f 2 + f 2. set x := {-2}(f 2). Note that, in this goal, it behaves like ``set x := {1 3}(f 2).`` + In particular, the switch ``{+}`` selects *all* the occurrences. This switch is useful to turn off the default behavior of a tactic which automatically clears some assumptions (see section :ref:`discharge_ssr` for instance). + The switch ``{-}`` imposes that *no* occurrences of the term should be affected by the tactic. The tactic: ``set x := {-}(f 2).`` leaves the goal unchanged and adds the definition ``x := f 2`` to the context. This kind of tactic may be used to take advantage of the power of the matching algorithm in a local definition, instead of copying large terms by hand. It is important to remember that matching *precedes* occurrence selection. .. example:: .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. .. coqtop:: all Lemma test x y z : x + y = x + y + z. set a := {2}(_ + _). Hence, in the following goal, the same tactic fails since there is only one occurrence of the selected term. .. example:: .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. .. coqtop:: all Lemma test x y z : (x + y) + (z + z) = z + z. Fail set a := {2}(_ + _). .. _basic_localization_ssr: Basic localization ~~~~~~~~~~~~~~~~~~ It is possible to define an abbreviation for a term appearing in the context of a goal thanks to the ``in`` tactical. .. tacv:: set @ident := @term in {+ @ident} This variant of :tacn:`set (ssreflect)` introduces a defined constant called :token:`ident` in the context, and folds it in the context entries mentioned on the right hand side of ``in``. The body of :token:`ident` is the first subterm matching these context entries (taken in the given order). .. example:: .. coqtop:: reset none From Coq Require Import ssreflect. .. coqtop:: all Lemma test x t (Hx : x = 3) : x + t = 4. set z := 3 in Hx. .. tacv:: set @ident := @term in {+ @ident} * This variant matches :token:`term` and then folds :token:`ident` similarly in all the given context entries but also folds :token:`ident` in the goal. .. example:: .. coqtop:: reset none From Coq Require Import ssreflect. .. coqtop:: all Lemma test x t (Hx : x = 3) : x + t = 4. set z := 3 in Hx * . Indeed, remember that 4 is just a notation for (S 3). The use of the ``in`` tactical is not limited to the localization of abbreviations: for a complete description of the in tactical, see section :ref:`bookkeeping_ssr` and :ref:`localization_ssr`. .. _basic_tactics_ssr: Basic tactics ------------- A sizable fraction of proof scripts consists of steps that do not "prove" anything new, but instead perform menial bookkeeping tasks such as selecting the names of constants and assumptions or splitting conjuncts. Although they are logically trivial, bookkeeping steps are extremely important because they define the structure of the data-flow of a proof script. This is especially true for reflection-based proofs, which often involve large numbers of constants and assumptions. Good bookkeeping consists in always explicitly declaring (i.e., naming) all new constants and assumptions in the script, and systematically pruning irrelevant constants and assumptions in the context. This is essential in the context of an interactive development environment (IDE), because it facilitates navigating the proof, allowing to instantly "jump back" to the point at which a questionable assumption was added, and to find relevant assumptions by browsing the pruned context. While novice or casual |Coq| users may find the automatic name selection feature convenient, the usage of such a feature severely undermines the readability and maintainability of proof scripts, much like automatic variable declaration in programming languages. The |SSR| tactics are therefore designed to support precise bookkeeping and to eliminate name generation heuristics. The bookkeeping features of |SSR| are implemented as tacticals (or pseudo-tacticals), shared across most |SSR| tactics, and thus form the foundation of the |SSR| proof language. .. _bookkeeping_ssr: Bookkeeping ~~~~~~~~~~~ During the course of a proof |Coq| always present the user with a *sequent* whose general form is:: ci : Ti … dj := ej : Tj … Fk : Pk … ================= forall (xl : Tl) …, let ym := bm in … in Pn -> … -> C The *goal* to be proved appears below the double line; above the line is the *context* of the sequent, a set of declarations of *constants* ``ci`` , *defined constants* ``dj`` , and *facts* ``Fk`` that can be used to prove the goal (usually, ``Ti`` , ``Tj : Type`` and ``Pk : Prop``). The various kinds of declarations can come in any order. The top part of the context consists of declarations produced by the Section commands ``Variable``, ``Let``, and ``Hypothesis``. This *section context* is never affected by the |SSR| tactics: they only operate on the lower part — the *proof context*. As in the figure above, the goal often decomposes into a series of (universally) quantified *variables* ``(xl : Tl)``, local *definitions* ``let ym := bm in``, and *assumptions* ``P n ->``, and a *conclusion* ``C`` (as in the context, variables, definitions, and assumptions can appear in any order). The conclusion is what actually needs to be proved — the rest of the goal can be seen as a part of the proof context that happens to be “below the line”. However, although they are logically equivalent, there are fundamental differences between constants and facts on the one hand, and variables and assumptions on the others. Constants and facts are *unordered*, but *named* explicitly in the proof text; variables and assumptions are *ordered*, but *unnamed*: the display names of variables may change at any time because of α-conversion. Similarly, basic deductive steps such as apply can only operate on the goal because the |Gallina| terms that control their action (e.g., the type of the lemma used by ``apply``) only provide unnamed bound variables. [#2]_ Since the proof script can only refer directly to the context, it must constantly shift declarations from the goal to the context and conversely in between deductive steps. In |SSR| these moves are performed by two *tacticals* ``=>`` and ``:``, so that the bookkeeping required by a deductive step can be directly associated to that step, and that tactics in an |SSR| script correspond to actual logical steps in the proof rather than merely shuffle facts. Still, some isolated bookkeeping is unavoidable, such as naming variables and assumptions at the beginning of a proof. |SSR| provides a specific ``move`` tactic for this purpose. Now ``move`` does essentially nothing: it is mostly a placeholder for ``=>`` and ``:``. The ``=>`` tactical moves variables, local definitions, and assumptions to the context, while the ``:`` tactical moves facts and constants to the goal. .. example:: For example, the proof of [#3]_ .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. .. coqtop:: all Lemma subnK : forall m n, n <= m -> m - n + n = m. might start with .. coqtop:: all move=> m n le_n_m. where move does nothing, but ``=> m n le_m_n`` changes the variables and assumption of the goal in the constants ``m n : nat`` and the fact ``le_n_m : n <= m``, thus exposing the conclusion ``m - n + n = m``. The ``:`` tactical is the converse of ``=>``, indeed it removes facts and constants from the context by turning them into variables and assumptions. .. coqtop:: all move: m le_n_m. turns back ``m`` and ``le_m_n`` into a variable and an assumption, removing them from the proof context, and changing the goal to ``forall m, n <= m -> m - n + n = m`` which can be proved by induction on ``n`` using ``elim: n``. Because they are tacticals, ``:`` and ``=>`` can be combined, as in .. coqdoc:: move: m le_n_m => p le_n_p. simultaneously renames ``m`` and ``le_m_n`` into ``p`` and ``le_n_p``, respectively, by first turning them into unnamed variables, then turning these variables back into constants and facts. Furthermore, |SSR| redefines the basic |Coq| tactics ``case``, ``elim``, and ``apply`` so that they can take better advantage of ``:`` and ``=>``. In there |SSR| variants, these tactic operate on the first variable or constant of the goal and they do not use or change the proof context. The ``:`` tactical is used to operate on an element in the context. .. example:: For instance the proof of ``subnK`` could continue with ``elim: n``. Instead of ``elim n`` (note, no colon), this has the advantage of removing n from the context. Better yet, this ``elim`` can be combined with previous move and with the branching version of the ``=>`` tactical (described in :ref:`introduction_ssr`), to encapsulate the inductive step in a single command: .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. .. coqtop:: all Lemma subnK : forall m n, n <= m -> m - n + n = m. move=> m n le_n_m. elim: n m le_n_m => [|n IHn] m => [_ | lt_n_m]. which breaks down the proof into two subgoals, the second one having in its context ``lt_n_m : S n <= m`` and ``IHn : forall m, n <= m -> m - n + n = m``. The ``:`` and ``=>`` tacticals can be explained very simply if one views the goal as a stack of variables and assumptions piled on a conclusion: + ``tactic : a b c`` pushes the context constants ``a``, ``b``, ``c`` as goal variables *before* performing tactic. + ``tactic => a b c`` pops the top three goal variables as context constants ``a``, ``b``, ``c``, *after* tactic has been performed. These pushes and pops do not need to balance out as in the examples above, so ``move: m le_n_m => p`` would rename ``m`` into ``p``, but leave an extra assumption ``n <= p`` in the goal. Basic tactics like apply and elim can also be used without the ’:’ tactical: for example we can directly start a proof of ``subnK`` by induction on the top variable ``m`` with .. coqdoc:: elim=> [|m IHm] n le_n. The general form of the localization tactical in is also best explained in terms of the goal stack:: tactic in a H1 H2 *. is basically equivalent to .. coqdoc:: move: a H1 H2; tactic => a H1 H2. with two differences: the in tactical will preserve the body of an if a is a defined constant, and if the ``*`` is omitted it will use a temporary abbreviation to hide the statement of the goal from ``tactic``. The general form of the in tactical can be used directly with the ``move``, ``case`` and ``elim`` tactics, so that one can write .. coqdoc:: elim: n => [|n IHn] in m le_n_m *. instead of .. coqdoc:: elim: n m le_n_m => [|n IHn] m le_n_m. This is quite useful for inductive proofs that involve many facts. See section :ref:`localization_ssr` for the general syntax and presentation of the in tactical. .. _the_defective_tactics_ssr: The defective tactics ~~~~~~~~~~~~~~~~~~~~~ In this section we briefly present the three basic tactics performing context manipulations and the main backward chaining tool. The move tactic. ```````````````` .. tacn:: move :name: move This tactic, in its defective form, behaves like the :tacn:`hnf` tactic. .. example:: .. coqtop:: reset all Require Import ssreflect. Goal not False. move. More precisely, the :tacn:`move` tactic inspects the goal and does nothing (:tacn:`idtac`) if an introduction step is possible, i.e. if the goal is a product or a ``let … in``, and performs :tacn:`hnf` otherwise. Of course this tactic is most often used in combination with the bookkeeping tacticals (see section :ref:`introduction_ssr` and :ref:`discharge_ssr`). These combinations mostly subsume the :tacn:`intros`, :tacn:`generalize`, :tacn:`revert`, :tacn:`rename`, :tacn:`clear` and :tacn:`pattern` tactics. The case tactic ``````````````` .. tacn:: case :name: case (ssreflect) This tactic performs *primitive case analysis* on (co)inductive types; specifically, it destructs the top variable or assumption of the goal, exposing its constructor(s) and its arguments, as well as setting the value of its type family indices if it belongs to a type family (see section :ref:`type_families_ssr`). The |SSR| case tactic has a special behavior on equalities. If the top assumption of the goal is an equality, the case tactic “destructs” it as a set of equalities between the constructor arguments of its left and right hand sides, as per the tactic injection. For example, ``case`` changes the goal:: (x, y) = (1, 2) -> G. into:: x = 1 -> y = 2 -> G. Note also that the case of |SSR| performs :g:`False` elimination, even if no branch is generated by this case operation. Hence the tactic :tacn:`case` on a goal of the form :g:`False -> G` will succeed and prove the goal. The elim tactic ``````````````` .. tacn:: elim :name: elim (ssreflect) This tactic performs inductive elimination on inductive types. In its defective form, the tactic performs inductive elimination on a goal whose top assumption has an inductive type. .. example:: .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. .. coqtop:: all Lemma test m : forall n : nat, m <= n. elim. .. _apply_ssr: The apply tactic ```````````````` .. tacn:: apply {? @term } :name: apply (ssreflect) This is the main backward chaining tactic of the proof system. It takes as argument any :token:`term` and applies it to the goal. Assumptions in the type of :token:`term` that don’t directly match the goal may generate one or more subgoals. In its defective form, this tactic is a synonym for:: intro top; first [refine top | refine (top _) | refine (top _ _) | …]; clear top. where :g:`top` is a fresh name, and the sequence of :tacn:`refine` tactics tries to catch the appropriate number of wildcards to be inserted. Note that this use of the :tacn:`refine` tactic implies that the tactic tries to match the goal up to expansion of constants and evaluation of subterms. :tacn:`apply (ssreflect)` has a special behavior on goals containing existential metavariables of sort :g:`Prop`. .. example:: .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. Axiom lt_trans : forall a b c, a < b -> b < c -> a < c. .. coqtop:: all Lemma test : forall y, 1 < y -> y < 2 -> exists x : { n | n < 3 }, 0 < proj1_sig x. move=> y y_gt1 y_lt2; apply: (ex_intro _ (exist _ y _)). by apply: lt_trans y_lt2 _. by move=> y_lt3; apply: lt_trans y_gt1. Note that the last ``_`` of the tactic ``apply: (ex_intro _ (exist _ y _))`` represents a proof that ``y < 3``. Instead of generating the goal:: 0 < proj1_sig (exist (fun n : nat => n < 3) y ?Goal). the system tries to prove ``y < 3`` calling the trivial tactic. If it succeeds, let’s say because the context contains ``H : y < 3``, then the system generates the following goal:: 0 < proj1_sig (exist (fun n => n < 3) y H). Otherwise the missing proof is considered to be irrelevant, and is thus discharged generating the two goals shown above. Last, the user can replace the trivial tactic by defining an Ltac expression named ``ssrautoprop``. .. _discharge_ssr: Discharge ~~~~~~~~~ The general syntax of the discharging tactical ``:`` is: .. tacn:: @tactic {? @ident } : {+ @d_item } {? @clear_switch } :name: ... : ... (ssreflect) :undocumented: .. prodn:: d_item ::= {? {| @occ_switch | @clear_switch } } @term .. prodn:: clear_switch ::= { {+ @ident } } with the following requirements: + :token:`tactic` must be one of the four basic tactics described in :ref:`the_defective_tac i.e., ``move``, ``case``, ``elim`` or ``apply``, the ``exact`` tactic (section :ref:`terminators_ssr`), the ``congr`` tactic (section :ref:`congruence_ssr`), or the application of the *view* tactical ‘/’ (section :ref:`interpreting_assumptions_ssr`) to one of move, case, or elim. + The optional :token:`ident` specifies *equation generation* (section :ref:`generation_ and is only allowed if tactic is ``move``, ``case`` or ``elim``, or the application of the view tactical ‘/’ (section :ref:`interpreting_assumptions_ssr`) to ``cas + An :token:`occ_switch` selects occurrences of :token:`term`, as in :ref:`abbreviations_ is not allowed if :token:`tactic` is ``apply`` or ``exact``. + A clear item :token:`clear_switch` specifies facts and constants to be deleted from the proof context (as per the clear tactic). The ``:`` tactical first *discharges* all the :token:`d_item`, right to left, and then performs tactic, i.e., for each :token:`d_item`, starting with the last one : #. The |SSR| matching algorithm described in section :ref:`abbreviations_ssr` is used to find occurrences of term in the goal, after filling any holes ‘_’ in term; however if tactic is apply or exact a different matching algorithm, described below, is used [#4]_. #. These occurrences are replaced by a new variable; in particular, if term is a fact, this adds an assumption to the goal. #. If term is *exactly* the name of a constant or fact in the proof context, it is deleted from the context, unless there is an :token:`occ_switch`. Finally, tactic is performed just after the first :token:`d_item` has been generalized — that is, between steps 2 and 3. The names listed in the final :token:`clear_switch` (if it is present) are cleared first, before :token:`d_item` n is discharged. Switches affect the discharging of a :token:`d_item` as follows: + An :token:`occ_switch` restricts generalization (step 2) to a specific subset of the occurrences of term, as per section :ref:`abbreviations_ssr`, and prevents clearing ( 3). + All the names specified by a :token:`clear_switch` are deleted from the context in step 3, possibly in addition to term. For example, the tactic: .. coqdoc:: move: n {2}n (refl_equal n). + first generalizes ``(refl_equal n : n = n)``; + then generalizes the second occurrence of ``n``. + finally generalizes all the other occurrences of ``n``, and clears ``n`` from the proof context (assuming n is a proof constant). Therefore this tactic changes any goal ``G`` into .. coqdoc:: forall n n0 : nat, n = n0 -> G. where the name ``n0`` is picked by the |Coq| display function, and assuming ``n`` appeared only in ``G``. Finally, note that a discharge operation generalizes defined constants as variables, and not as local definitions. To override this behavior, prefix the name of the local definition with a ``@``, like in ``move: @n``. This is in contrast with the behavior of the in tactical (see section :ref:`localization_ssr`), which preserves local definitions by default. Clear rules ``````````` The clear step will fail if term is a proof constant that appears in other facts; in that case either the facts should be cleared explicitly with a :token:`clear_switch`, or the clear step should be disabled. The latter can be done by adding an :token:`occ_switch` or simply by putting parentheses around term: both ``move: (n).`` and ``move: {+}n.`` generalize ``n`` without clearing ``n`` from the proof context. The clear step will also fail if the :token:`clear_switch` contains a :token:`ident` that is not in the *proof* context. Note that |SSR| never clears a section constant. If tactic is ``move`` or ``case`` and an equation :token:`ident` is given, then clear (step 3) for :token:`d_item` is suppressed (see section :ref:`generation_of_equations_ss Intro patterns (see section :ref:`introduction_ssr`) and the ``rewrite`` tactic (see section :ref:`rewriting_ssr`) let one place a :token:`clear_switch` in the middle of other items (namely identifiers, views and rewrite rules). This can trigger the addition of proof context items to the ones being explicitly cleared, and in turn this can result in clear errors (e.g. if the context item automatically added occurs in the goal). The relevant sections describe ways to avoid the unintended clear of context items. Matching for apply and exact ```````````````````````````` The matching algorithm for :token:`d_item` of the |SSR| ``apply`` and ``exact`` tactics exploits the type of the first :token:`d_item` to interpret wildcards in the other :token:`d_item` and to determine which occurrences of these should be generalized. Therefore, occur switches are not needed for apply and exact. Indeed, the |SSR| tactic ``apply: H x`` is equivalent to ``refine (@H _ … _ x); clear H x`` with an appropriate number of wildcards between ``H`` and ``x``. Note that this means that matching for ``apply`` and ``exact`` has much more context to interpret wildcards; in particular it can accommodate the ``_`` :token:`d_item`, which would always be rejected after ``move:``. .. example:: .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. Axiom f : nat -> nat. Axiom g : nat -> nat. .. coqtop:: all Lemma test (Hfg : forall x, f x = g x) a b : f a = g b. apply: trans_equal (Hfg _) _. This tactic is equivalent (see section :ref:`bookkeeping_ssr`) to: ``refine (trans_equal (Hfg _) _).`` and this is a common idiom for applying transitivity on the left hand side of an equation. .. _abstract_ssr: The abstract tactic ``````````````````` .. tacn:: abstract: {+ @d_item} :name: abstract (ssreflect) This tactic assigns an abstract constant previously introduced with the :n:`[: @ident ]` intro pattern (see section :ref:`introduction_ssr`). In a goal like the following:: m : nat abs : <hidden> n : nat ============= m < 5 + n The tactic ``abstract: abs n`` first generalizes the goal with respect ton (that is not visible to the abstract constant abs) and then assigns abs. The resulting goal is:: m : nat n : nat ============= m < 5 + n Once this subgoal is closed, all other goals having abs in their context see the type assigned to ``abs``. In this case:: m : nat abs : forall n, m < 5 + n ============= … For a more detailed example the reader should refer to section :ref:`structure_ssr`. .. _introduction_ssr: Introduction in the context ~~~~~~~~~~~~~~~~~~~~~~~~~~~ The application of a tactic to a given goal can generate (quantified) variables, assumptions, or definitions, which the user may want to *introduce* as new facts, constants or defined constants, respectively. If the tactic splits the goal into several subgoals, each of them may require the introduction of different constants and facts. Furthermore it is very common to immediately decompose or rewrite with an assumption instead of adding it to the context, as the goal can often be simplified and even proved after this. All these operations are performed by the introduction tactical ``=>``, whose general syntax is .. tacn:: @tactic => {+ @i_item } :name: => :undocumented: .. prodn:: i_item ::= {| @i_pattern | @s_item | @clear_switch | @i_view | @i_block } .. prodn:: s_item ::= {| /= | // | //= } .. prodn:: i_view ::= {? %{%} } {| /@term | /ltac:( @tactic ) } .. prodn:: i_pattern ::= {| @ident | > | _ | ? | * | + | {? @occ_switch } {| -> | <- } | [ {?| @i_item } ] | - | [: {+ @ident } ] } .. prodn:: i_block ::= {| [^ @ident ] | [^~ {| @ident | @num } ] } The ``=>`` tactical first executes :token:`tactic`, then the :token:`i_item`\s, left to right. An :token:`s_item` specifies a simplification operation; a :token:`clear_switch` specifies context pruning as in :ref:`discharge_ssr`. The :token:`i_pattern`\s can be seen as a variant of *intro patterns* (see :tacn:`intros`:) each performs an introduction operation, i.e., pops some variables or assumptions from the goal. Simplification items ````````````````````` An :token:`s_item` can simplify the set of subgoals or the subgoals themselves: + ``//`` removes all the “trivial” subgoals that can be resolved by the |SSR| tactic :tacn:`done` described in :ref:`terminators_ssr`, i.e., it executes ``try done``. + ``/=`` simplifies the goal by performing partial evaluation, as per the tactic :tacn:`simpl` [#5]_. + ``//=`` combines both kinds of simplification; it is equivalent to ``/= //``, i.e., ``simpl; try done``. When an :token:`s_item` immediately precedes a :token:`clear_switch`, then the :token:`clear_switch` is executed *after* the :token:`s_item`, e.g., ``{IHn}//`` will solve some subgoals, possibly using the fact ``IHn``, and will erase ``IHn`` from the context of the remaining subgoals. Views ````` The first entry in the :token:`i_view` grammar rule, :n:`/@term`, represents a view (see section :ref:`views_and_reflection_ssr`). It interprets the top of the stack with the view :token:`term`. It is equivalent to :n:`move/@term`. A :token:`clear_switch` that immediately precedes an :token:`i_view` is complemented with the name of the view if an only if the :token:`i_view` is a simple proof context entry [#10]_. E.g. ``{}/v`` is equivalent to ``/v{v}``. This behavior can be avoided by separating the :token:`clear_switch` from the :token:`i_view` with the ``-`` intro pattern or by putting parentheses around the view. A :token:`clear_switch` that immediately precedes an :token:`i_view` is executed after the view application. If the next :token:`i_item` is a view, then the view is applied to the assumption in top position once all the previous :token:`i_item` have been performed. The second entry in the :token:`i_view` grammar rule, ``/ltac:(`` :token:`tactic` ``)``, executes :token:`tactic`. Notations can be used to name tactics, for example:: Notation myop := (ltac:(some ltac code)) : ssripat_scope. lets one write just ``/myop`` in the intro pattern. Note the scope annotation: views are interpreted opening the ``ssripat`` scope. Intro patterns `````````````` |SSR| supports the following :token:`i_pattern`\s: :token:`ident` pops the top variable, assumption, or local definition into a new constant, fact, or defined constant :token:`ident`, respectively. Note that defined constants cannot be introduced when δ-expansion is required to expose the top variable or assumption. A :token:`clear_switch` (even an empty one) immediately preceding an :token:`ident` is complemented with that :token:`ident` if and only if the identifier is a simple proof context entry [#10]_. As a consequence by prefixing the :token:`ident` with ``{}`` one can *replace* a context entry. This behavior can be avoided by separating the :token:`clear_switch` from the :token:`ident` with the ``-`` intro pattern. ``>`` pops every variable occurring in the rest of the stack. Type class instances are popped even if they don't occur in the rest of the stack. The tactic ``move=> >`` is equivalent to ``move=> ? ?`` on a goal such as:: forall x y, x < y -> G A typical use if ``move=>> H`` to name ``H`` the first assumption, in the example above ``x < y``. ``?`` pops the top variable into an anonymous constant or fact, whose name is picked by the tactic interpreter. |SSR| only generates names that cannot appear later in the user script [#6]_. ``_`` pops the top variable into an anonymous constant that will be deleted from the proof context of all the subgoals produced by the ``=>`` tactical. They should thus never be displayed, except in an error message if the constant is still actually used in the goal or context after the last :token:`i_item` has been executed (:token:`s_item` can erase goals or terms where the constant appears). ``*`` pops all the remaining apparent variables/assumptions as anonymous constants/facts. Unlike ``?`` and ``move`` the ``*`` :token:`i_item` does not expand definitions in the goal to expose quantifiers, so it may be useful to repeat a ``move=> *`` tactic, e.g., on the goal:: forall a b : bool, a <> b a first ``move=> *`` adds only ``_a_ : bool`` and ``_b_ : bool`` to the context; it takes a second ``move=> *`` to add ``_Hyp_ : _a_ = _b_``. ``+`` temporarily introduces the top variable. It is discharged at the end of the intro pattern. For example ``move=> + y`` on a goal:: forall x y, P is equivalent to ``move=> _x_ y; move: _x_`` that results in the goal:: forall x, P :n:`{? occ_switch } ->` (resp. :token:`occ_switch` ``<-``) pops the top assumption (which should be a rewritable proposition) into an anonymous fact, rewrites (resp. rewrites right to left) the goal with this fact (using the |SSR| ``rewrite`` tactic described in section :ref:`rewriting_ssr`, and honoring the optional occurrence selector), and finally deletes the anonymous fact from the context. ``[`` :token:`i_item` * ``| … |`` :token:`i_item` * ``]`` when it is the very *first* :token:`i_pattern` after tactic ``=>`` tactical *and* tactic is not a move, is a *branching*:token:`i_pattern`. It executes the sequence :token:`i_item`:math:`_i` on the i-th subgoal produced by tactic. The execution of tactic should thus generate exactly m subgoals, unless the ``[…]`` :token:`i_pattern` comes after an initial ``//`` or ``//=`` :token:`s_item` that closes some of the goals produced by ``tactic``, in which case exactly m subgoals should remain after the :token:`s_item`, or we have the trivial branching :token:`i_pattern` [], which always does nothing, regardless of the number of remaining subgoals. ``[`` :token:`i_item` * ``| … |`` :token:`i_item` * ``]`` when it is *not* the first :token:`i_pattern` or when tactic is a ``move``, is a *destructing* :token:`i_pattern`. It starts by destructing the top variable, using the |SSR| ``case`` tactic described in :ref:`the_defective_tactics_ssr`. It then behaves as the corresponding branching :token:`i_pattern`, executing the sequence :n:`@i_item__i` in the i-th subgoal generated by the case analysis; unless we have the trivial destructing :token:`i_pattern` ``[]``, the latter should generate exactly m subgoals, i.e., the top variable should have an inductive type with exactly m constructors [#7]_. While it is good style to use the :token:`i_item` i * to pop the variables and assumptions corresponding to each constructor, this is not enforced by |SSR|. ``-`` does nothing, but counts as an intro pattern. It can also be used to force the interpretation of ``[`` :token:`i_item` * ``| … |`` :token:`i_item` * ``]`` as a case analysis like in ``move=> -[H1 H2]``. It can also be used to indicate explicitly the link between a view and a name like in ``move=> /eqP-H1``. Last, it can serve as a separator between views. Section :ref:`views_and_reflection_ssr` [#9]_ explains in which respect the tactic ``move=> /v1/v2`` differs from the tactic ``move=> /v1-/v2``. ``[:`` :token:`ident` ``…]`` introduces in the context an abstract constant for each :token:`ident`. Its type has to be fixed later on by using the ``abstract`` tactic. Before then the type displayed is ``<hidden>``. Note that |SSR| does not support the syntax ``(ipat, …, ipat)`` for destructing intro patterns. Clear switch ```````````` Clears are deferred until the end of the intro pattern. .. example:: .. coqtop:: reset none From Coq Require Import ssreflect ssrbool. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. .. coqtop:: all Lemma test x y : Nat.leb 0 x = true -> (Nat.leb 0 x) && (Nat.leb y 2) = true. move=> {x} ->. If the cleared names are reused in the same intro pattern, a renaming is performed behind the scenes. Facts mentioned in a clear switch must be valid names in the proof context (excluding the section context). Branching and destructuring ``````````````````````````` The rules for interpreting branching and destructing :token:`i_pattern` are motivated by the fact that it would be pointless to have a branching pattern if tactic is a ``move``, and in most of the remaining cases tactic is ``case`` or ``elim``, which implies destruction. The rules above imply that: + ``move=> [a b].`` + ``case=> [a b].`` + ``case=> a b.`` are all equivalent, so which one to use is a matter of style; ``move`` should be used for casual decomposition, such as splitting a pair, and ``case`` should be used for actual decompositions, in particular for type families (see :ref:`type_families_ssr`) and proof by contradiction. The trivial branching :token:`i_pattern` can be used to force the branching interpretation, e.g.: + ``case=> [] [a b] c.`` + ``move=> [[a b] c].`` + ``case; case=> a b c.`` are all equivalent. Block introduction `````````````````` |SSR| supports the following :token:`i_block`\s: :n:`[^ @ident ]` *block destructing* :token:`i_pattern`. It performs a case analysis on the top variable and introduces, in one go, all the variables coming from the case analysis. The names of these variables are obtained by taking the names used in the inductive type declaration and prefixing them with :token:`ident`. If the intro pattern immediately follows a call to ``elim`` with a custom eliminator (see :ref:`custom_elim_ssr`) then the names are taken from the ones used in the type of the eliminator. .. example:: .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. .. coqtop:: all Record r := { a : nat; b := (a, 3); _ : bool; }. Lemma test : r -> True. Proof. move => [^ x ]. :n:`[^~ @ident ]` *block destructing* using :token:`ident` as a suffix. :n:`[^~ @num ]` *block destructing* using :token:`num` as a suffix. Only a :token:`s_item` is allowed between the elimination tactic and the block destructing. .. _generation_of_equations_ssr: Generation of equations ~~~~~~~~~~~~~~~~~~~~~~~ The generation of named equations option stores the definition of a new constant as an equation. The tactic: .. coqdoc:: move En: (size l) => n. where ``l`` is a list, replaces ``size l`` by ``n`` in the goal and adds the fact ``En : size l = n`` to the context. This is quite different from: .. coqdoc:: pose n := (size l). which generates a definition ``n := (size l)``. It is not possible to generalize or rewrite such a definition; on the other hand, it is automatically expanded during computation, whereas expanding the equation ``En`` requires explicit rewriting. The use of this equation name generation option with a ``case`` or an ``elim`` tactic changes the status of the first :token:`i_item`, in order to deal with the possible parameters of the constants introduced. .. example:: .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. .. coqtop:: all Lemma test (a b :nat) : a <> b. case E : a => [|n]. If the user does not provide a branching :token:`i_item` as first :token:`i_item`, or if the :token:`i_item` does not provide enough names for the arguments of a constructor, then the constants generated are introduced under fresh |SSR| names. .. example:: .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. .. coqtop:: all Lemma test (a b :nat) : a <> b. case E : a => H. Show 2. Combining the generation of named equations mechanism with the :tacn:`case` tactic strengthens the power of a case analysis. On the other hand, when combined with the :tacn:`elim` tactic, this feature is mostly useful for debug purposes, to trace the values of decomposed parameters and pinpoint failing branches. .. _type_families_ssr: Type families ~~~~~~~~~~~~~ When the top assumption of a goal has an inductive type, two specific operations are possible: the case analysis performed by the :tacn:`case` tactic, and the application of an induction principle, performed by the :tacn:`elim` tactic. When this top assumption has an inductive type, which is moreover an instance of a type family, |Coq| may need help from the user to specify which occurrences of the parameters of the type should be substituted. .. tacv:: case: {+ @d_item } / {+ @d_item } elim: {+ @d_item } / {+ @d_item } A specific ``/`` switch indicates the type family parameters of the type of a :token:`d_item` immediately following this ``/`` switch. The :token:`d_item` on the right side of the ``/`` switch are discharged as described in section :ref:`discharge_ssr`. The case analysis or elimination --> -------------------- --> maximum size reached --> -------------------- [ zur Elbe Produktseite wechseln0.336Quellennavigators ] |