Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Sprache: Unknown

Haftungsausschluß.rst KontaktHaskell {Haskell[399] Ada[642] Abap[905]}diese Dinge liegen außhalb unserer Verantwortung

.. _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_tactics_ssr`,
  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_of_equations_ssr`),
  and is only allowed if tactic is ``move``, ``case`` or ``elim``, or the
  application of the view tactical ‘/’ (section :ref:`interpreting_assumptions_ssr`) to ``case`` or ``elim``.
+ An :token:`occ_switch` selects occurrences of :token:`term`, as in :ref:`abbreviations_ssr`; :token:`occ_switch`
  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 (step
  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_ssr`).

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

--> --------------------

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Sprache: Unknown

[ Verzeichnis aufwärts0.371unsichere Verbindung ]

^© Kompilation durch diese Firma