diff options
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/addendum/program.rst | 12 | ||||
| -rw-r--r-- | doc/sphinx/addendum/type-classes.rst | 22 | ||||
| -rw-r--r-- | doc/sphinx/practical-tools/coq-commands.rst | 7 | ||||
| -rw-r--r-- | doc/sphinx/practical-tools/utilities.rst | 4 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ssreflect-proof-language.rst | 281 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 30 | ||||
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 61 |
7 files changed, 324 insertions, 93 deletions
diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index 56f84d0ff0..b410833d25 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -194,14 +194,14 @@ Program Fixpoint The optional order annotation follows the grammar: .. productionlist:: orderannot - order : measure `term` (`term`)? | wf `term` `term` + order : measure `term` [ `term` ] | wf `term` `ident` - + :g:`measure f ( R )` where :g:`f` is a value of type :g:`X` computed on - any subset of the arguments and the optional (parenthesised) term - ``(R)`` is a relation on ``X``. By default ``X`` defaults to ``nat`` and ``R`` - to ``lt``. + + :g:`measure f R` where :g:`f` is a value of type :g:`X` computed on + any subset of the arguments and the optional term + :g:`R` is a relation on :g:`X`. :g:`X` defaults to :g:`nat` and :g:`R` + to :g:`lt`. - + :g:`wf R x` which is equivalent to :g:`measure x (R)`. + + :g:`wf R x` which is equivalent to :g:`measure x R`. The structural fixpoint operator behaves just like the one of |Coq| (see :cmd:`Fixpoint`), except it may also generate obligations. It works diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index b069cf27f4..a5e9023732 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -433,22 +433,26 @@ few other commands related to typeclasses. .. _TypeclassesTransparent: -Typeclasses Transparent, Typclasses Opaque -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Typeclasses Transparent, Typeclasses Opaque +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ .. cmd:: Typeclasses Transparent {+ @ident} This command makes the identifiers transparent during typeclass resolution. + Shortcut for :n:`Hint Transparent {+ @ident } : typeclass_instances`. .. cmd:: Typeclasses Opaque {+ @ident} - Make the identifiers opaque for typeclass search. It is useful when some - constants prevent some unifications and make resolution fail. It is also - useful to declare constants which should never be unfolded during - proof-search, like fixpoints or anything which does not look like an - abbreviation. This can additionally speed up proof search as the typeclass - map can be indexed by such rigid constants (see + Make the identifiers opaque for typeclass search. + Shortcut for :n:`Hint Opaque {+ @ident } : typeclass_instances`. + + It is useful when some constants prevent some unifications and make + resolution fail. It is also useful to declare constants which + should never be unfolded during proof-search, like fixpoints or + anything which does not look like an abbreviation. This can + additionally speed up proof search as the typeclass map can be + indexed by such rigid constants (see :ref:`thehintsdatabasesforautoandeauto`). By default, all constants and local variables are considered transparent. One @@ -458,8 +462,6 @@ type, like: .. coqdoc:: Definition relation A := A -> A -> Prop. -This is equivalent to ``Hint Transparent, Opaque ident : typeclass_instances``. - Settings ~~~~~~~~ diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index eebf1f11e1..bdda35fcc0 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -210,6 +210,13 @@ and ``coqtop``, unless stated otherwise: is intended to be used as a linter for developments that want to be robust to changes in the auto-generated name scheme. The options are provided to facilitate tracking down problems. +:-set *string*: Enable flags and set options. *string* should be + ``Option Name=value``, the value is interpreted according to the + type of the option. For flags ``Option Name`` is equivalent to + ``Option Name=true``. For instance ``-set "Universe Polymorphism"`` + will enable :flag:`Universe Polymorphism`. Note that the quotes are + shell syntax, Coq does not see them. +:-unset *string*: As ``-set`` but used to disable options and flags. :-compat *version*: Attempt to maintain some backward-compatibility with a previous version. :-dump-glob *file*: Dump references for global names in file *file* diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index 8346b72cb9..35231610fe 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -144,6 +144,10 @@ Here we describe only few of them. :CAMLFLAGS: can be used to specify additional flags to the |OCaml| compiler, like ``-bin-annot`` or ``-w``.... +:OCAMLWARN: + it contains a default of ``-warn-error +a-3``, useful to modify + this setting; beware this is not recommended for projects in + Coq's CI. :COQC, COQDEP, COQDOC: can be set in order to use alternative binaries (e.g. wrappers) diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index b240cef40c..4e40df6f94 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -1737,9 +1737,8 @@ Intro patterns 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. +destructing intro patterns. Clear switch ```````````` @@ -3626,7 +3625,7 @@ corresponding new goals will be generated. As in :ref:`apply_ssr`, the ``ssrautoprop`` tactic is used to try to solve the existential variable. - .. coqtop:: all + .. coqtop:: all abort Lemma test (x : 'I_2) y (H : y < 2) : Some x = insub 2 y. rewrite insubT. @@ -3637,6 +3636,272 @@ rewriting rule is stated using Leibniz equality (as opposed to setoid relations). It will be extended to other rewriting relations in the future. +.. _under_ssr: + +Rewriting under binders +~~~~~~~~~~~~~~~~~~~~~~~ + +Goals involving objects defined with higher-order functions often +require "rewriting under binders". While setoid rewriting is a +possible approach in this case, it is common to use regular rewriting +along with dedicated extensionality lemmas. This may cause some +practical issues during the development of the corresponding scripts, +notably as we might be forced to provide the rewrite tactic with +complete terms, as shown by the simple example below. + +.. example:: + + .. coqtop:: reset none + + From Coq Require Import ssreflect. + Set Implicit Arguments. + Unset Strict Implicit. + Unset Printing Implicit Defensive. + + .. coqtop:: in + + Axiom subnn : forall n : nat, n - n = 0. + Parameter map : (nat -> nat) -> list nat -> list nat. + Parameter sumlist : list nat -> nat. + Axiom eq_map : + forall F1 F2 : nat -> nat, + (forall n : nat, F1 n = F2 n) -> + forall l : list nat, map F1 l = map F2 l. + + .. coqtop:: all + + Lemma example_map l : sumlist (map (fun m => m - m) l) = 0. + + In this context, one cannot directly use ``eq_map``: + + .. coqtop:: all fail + + rewrite eq_map. + + as we need to explicitly provide the non-inferable argument ``F2``, + which corresponds here to the term we want to obtain *after* the + rewriting step. In order to perform the rewrite step one has to + provide the term by hand as follows: + + .. coqtop:: all abort + + rewrite (@eq_map _ (fun _ : nat => 0)). + by move=> m; rewrite subnn. + + The :tacn:`under` tactic lets one perform the same operation in a more + convenient way: + + .. coqtop:: all abort + + Lemma example_map l : sumlist (map (fun m => m - m) l) = 0. + under eq_map => m do rewrite subnn. + + +The under tactic +```````````````` + +The convenience :tacn:`under` tactic supports the following syntax: + +.. tacn:: under {? @r_prefix } @term {? => {+ @i_item}} {? do ( @tactic | [ {*| @tactic } ] ) } + :name: under + + Operate under the context proved to be extensional by + lemma :token:`term`. + + .. exn:: Incorrect number of tactics (expected N tactics, was given M). + + This error can occur when using the version with a ``do`` clause. + + The multiplier part of :token:`r_prefix` is not supported. + +We distinguish two modes, +:ref:`interactive mode <under_interactive>` without a ``do`` clause, and +:ref:`one-liner mode <under_one_liner>` with a ``do`` clause, +which are explained in more detail below. + +.. _under_interactive: + +Interactive mode +```````````````` + +Let us redo the running example in interactive mode. + +.. example:: + + .. coqtop:: all abort + + Lemma example_map l : sumlist (map (fun m => m - m) l) = 0. + under eq_map => m. + rewrite subnn. + over. + +The execution of the Ltac expression: + +:n:`under @term => [ @i_item__1 | … | @i_item__n ].` + +involves the following steps: + +1. It performs a :n:`rewrite @term` + without failing like in the first example with ``rewrite eq_map.``, + but creating evars (see :tacn:`evar`). If :n:`term` is prefixed by + a pattern or an occurrence selector, then the modifiers are honoured. + +2. As a n-branches intro pattern is provided :tacn:`under` checks that + n+1 subgoals have been created. The last one is the main subgoal, + while the other ones correspond to premises of the rewrite rule (such as + ``forall n, F1 n = F2 n`` for ``eq_map``). + +3. If so :tacn:`under` puts these n goals in head normal form (using + the defective form of the tactic :tacn:`move`), then executes + the corresponding intro pattern :n:`@ipat__i` in each goal. + +4. Then :tacn:`under` checks that the first n subgoals + are (quantified) equalities or double implications between a + term and an evar (e.g. ``m - m = ?F2 m`` in the running example). + +5. If so :tacn:`under` protects these n goals against an + accidental instantiation of the evar. + These protected goals are displayed using the ``Under[ … ]`` + notation (e.g. ``Under[ m - m ]`` in the running example). + +6. The expression inside the ``Under[ … ]`` notation can be + proved equivalent to the desired expression + by using a regular :tacn:`rewrite` tactic. + +7. Interactive editing of the first n goals has to be signalled by + using the :tacn:`over` tactic or rewrite rule (see below). + +8. Finally, a post-processing step is performed in the main goal + to keep the name(s) for the bound variables chosen by the user in + the intro pattern for the first branch. + +.. _over_ssr: + +The over tactic ++++++++++++++++ + +Two equivalent facilities (a terminator and a lemma) are provided to +close intermediate subgoals generated by :tacn:`under` (i.e. goals +displayed as ``Under[ … ]``): + +.. tacn:: over + :name: over + + This terminator tactic allows one to close goals of the form + ``'Under[ … ]``. + +.. tacv:: by rewrite over + + This is a variant of :tacn:`over` in order to close ``Under[ … ]`` + goals, relying on the ``over`` rewrite rule. + +.. _under_one_liner: + +One-liner mode +`````````````` + +The Ltac expression: + +:n:`under @term => [ @i_item__1 | … | @i_item__n ] do [ @tac__1 | … | @tac__n ].` + +can be seen as a shorter form for the following expression: + +:n:`(under @term) => [ @i_item__1 | … | @i_item__n | ]; [ @tac__1; over | … | @tac__n; over | cbv beta iota ].` + +Notes: + ++ The ``beta-iota`` reduction here is useful to get rid of the beta + redexes that could be introduced after the substitution of the evars + by the :tacn:`under` tactic. + ++ Note that the provided tactics can as well + involve other :tacn:`under` tactics. See below for a typical example + involving the `bigop` theory from the Mathematical Components library. + ++ If there is only one tactic, the brackets can be omitted, e.g.: + :n:`under @term => i do @tac.` and that shorter form should be + preferred. + ++ If the ``do`` clause is provided and the intro pattern is omitted, + then the default :token:`i_item` ``*`` is applied to each branch. + E.g., the Ltac expression: + :n:`under @term do [ @tac__1 | … | @tac__n ]` is equivalent to: + :n:`under @term => [ * | … | * ] do [ @tac__1 | … | @tac__n ]` + (and it can be noted here that the :tacn:`under` tactic performs a + ``move.`` before processing the intro patterns ``=> [ * | … | * ]``). + +.. example:: + + .. coqtop:: reset none + + From Coq Require Import ssreflect. + Set Implicit Arguments. + Unset Strict Implicit. + Unset Printing Implicit Defensive. + + Coercion is_true : bool >-> Sortclass. + + Reserved Notation "\big [ op / idx ]_ ( m <= i < n | P ) F" + (at level 36, F at level 36, op, idx at level 10, m, i, n at level 50, + format "'[' \big [ op / idx ]_ ( m <= i < n | P ) F ']'"). + Variant bigbody (R I : Type) : Type := + BigBody : forall (_ : I) (_ : forall (_ : R) (_ : R), R) (_ : bool) (_ : R), bigbody R I. + + Parameter bigop : + forall (R I : Type) (_ : R) (_ : list I) (_ : forall _ : I, bigbody R I), R. + + Axiom eq_bigr_ : + forall (R : Type) (idx : R) (op : forall (_ : R) (_ : R), R) (I : Type) + (r : list I) (P : I -> bool) (F1 F2 : I -> R), + (forall x : I, is_true (P x) -> F1 x = F2 x) -> + bigop idx r (fun i : I => BigBody i op (P i) (F1 i)) = + bigop idx r (fun i : I => BigBody i op (P i) (F2 i)). + + Axiom eq_big_ : + forall (R : Type) (idx : R) (op : R -> R -> R) (I : Type) (r : list I) + (P1 P2 : I -> bool) (F1 F2 : I -> R), + (forall x : I, P1 x = P2 x) -> + (forall i : I, is_true (P1 i) -> F1 i = F2 i) -> + bigop idx r (fun i : I => BigBody i op (P1 i) (F1 i)) = + bigop idx r (fun i : I => BigBody i op (P2 i) (F2 i)). + + Reserved Notation "\sum_ ( m <= i < n | P ) F" + (at level 41, F at level 41, i, m, n at level 50, + format "'[' \sum_ ( m <= i < n | P ) '/ ' F ']'"). + + Parameter index_iota : nat -> nat -> list nat. + + Notation "\big [ op / idx ]_ ( m <= i < n | P ) F" := + (bigop idx (index_iota m n) (fun i : nat => BigBody i op P%bool F)). + + Notation "\sum_ ( m <= i < n | P ) F" := + (\big[plus/O]_(m <= i < n | P%bool) F%nat). + + Notation eq_bigr := (fun n m => eq_bigr_ 0 plus (index_iota n m)). + Notation eq_big := (fun n m => eq_big_ 0 plus (index_iota n m)). + + Parameter odd : nat -> bool. + Parameter prime : nat -> bool. + + .. coqtop:: in + + Parameter addnC : forall m n : nat, m + n = n + m. + Parameter muln1 : forall n : nat, n * 1 = n. + + .. coqtop:: all + + Check eq_bigr. + Check eq_big. + + Lemma test_big_nested (m n : nat) : + \sum_(0 <= a < m | prime a) \sum_(0 <= j < n | odd (j * 1)) (a + j) = + \sum_(0 <= i < m | prime i) \sum_(0 <= j < n | odd j) (j + i). + under eq_bigr => i prime_i do + under eq_big => [ j | j odd_j ] do + [ rewrite (muln1 j) | rewrite (addnC i j) ]. + + Remark how the final goal uses the name ``i`` (the name given in the + intro pattern) rather than ``a`` in the binder of the first summation. .. _locking_ssr: @@ -5373,7 +5638,15 @@ respectively. .. tacn:: rewrite {+ @r_step } - rewrite (see :ref:`rewriting_ssr`) + rewrite (see :ref:`rewriting_ssr`) + +.. tacn:: under {? @r_prefix } @term {? => {+ @i_item}} {? do ( @tactic | [ {*| @tactic } ] )} + + under (see :ref:`under_ssr`) + +.. tacn:: over + + over (see :ref:`over_ssr`) .. tacn:: have {* @i_item } {? @i_pattern } {? @s_item %| {+ @ssr_binder } } {? : @term } := @term have {* @i_item } {? @i_pattern } {? @s_item %| {+ @ssr_binder } } : @term {? by @tactic } diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index afb0239be4..8d9e99b9d5 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3830,25 +3830,25 @@ The general command to add a hint to some databases :n:`{+ @ident}` is check with :cmd:`Print HintDb` to verify the current cut expression: .. productionlist:: regexp - e : `ident` hint or instance identifier - : _ any hint - : `e` | `e` disjunction - : `e` `e` sequence - : `e` * Kleene star - : emp empty - : eps epsilon - : ( `e` ) + regexp : `ident` (hint or instance identifier) + : _ (any hint) + : `regexp` | `regexp` (disjunction) + : `regexp` `regexp` (sequence) + : `regexp` * (Kleene star) + : emp (empty) + : eps (epsilon) + : ( `regexp` ) The `emp` regexp does not match any search path while `eps` matches the empty path. During proof search, the path of successive successful hints on a search branch is recorded, as a - list of identifiers for the hints (note that Hint Extern’s do not have + list of identifiers for the hints (note that :cmd:`Hint Extern`\’s do not have an associated identifier). Before applying any hint :n:`@ident` the current path `p` extended with :n:`@ident` is matched against the current cut expression `c` associated to the hint database. If matching succeeds, the hint is *not* applied. The - semantics of ``Hint Cut e`` is to set the cut expression to ``c | e``, the - initial cut expression being `emp`. + semantics of :n:`Hint Cut @regexp` is to set the cut expression + to :n:`c | regexp`, the initial cut expression being `emp`. .. cmdv:: Hint Mode @qualid {* (+ | ! | -)} : @ident :name: Hint Mode @@ -3875,7 +3875,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is .. note:: One can use an ``Extern`` hint with no pattern to do pattern matching on - hypotheses using ``match goal`` with inside the tactic. + hypotheses using ``match goal with`` inside the tactic. Hint databases defined in the Coq standard library @@ -4724,6 +4724,12 @@ Non-logical tactics from the shelf into focus, by appending them to the end of the current list of focused goals. +.. tacn:: unshelve @tactic + :name: unshelve + + Performs :n:`@tactic`, then unshelves existential variables added to the + shelf by the execution of :n:`@tactic`, prepending them to the current goal. + .. tacn:: give_up :name: give_up diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 63df3d37bf..3ca1dda4d6 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1040,8 +1040,6 @@ interpreted in the scope stack extended with the scope bound tokey. To remove a delimiting key of a scope, use the command :n:`Undelimit Scope @scope` -.. _ArgumentScopes: - Binding arguments of a constant to an interpretation scope +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ @@ -1311,65 +1309,6 @@ Displaying information about scopes It also displays the delimiting key if any and the class to which the scope is bound, if any. -Impact of scopes on printing -~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -When several notations are available for printing the same expression, -Coq will use the following rules for printing priorities: - -- If two notations are available in different scopes which are open, - the notation in the more recently opened scope takes precedence. - -- If two notations are available in the same scope, the more recently - defined (or imported) notation takes precedence. - -- Abbreviations and lonely notations, both of which have no scope, - take precedence over a notation in an open scope if and only if the - abbreviation or lonely notation was defined (or imported) more - recently than when the corresponding scope was open. They take - precedence over any notation not in an open scope, whether this scope - has a delimiter or not. - -- A scope is *active* for printing a term either because it was opened - with :cmd:`Open Scope`, or the term is the immediate argument of a - constant which temporarily opens a scope for this argument (see - :ref:`Arguments <ArgumentScopes>`) in which case this temporary - scope is the most recent open one. - -- In case no abbreviation, nor lonely notation, nor notation in an - explicitly open scope, nor notation in a temporarily open scope of - arguments, has been found, notations in those closed scopes which - have a delimiter are considered, giving priority to the most - recently defined (or imported) ones. The corresponding delimiter is - inserted, making the corresponding scope the most recent explicitly - open scope for all subterms of the current term. As an exception to - the insertion of the corresponding delimiter, when an expression is - statically known to be in a position expecting a type and the - notation is from scope ``type_scope``, and the latter is closed, the - delimiter is not inserted. This is because expressions statically - known to be in a position expecting a type are by default - interpreted with `type_scope` temporarily activated. Expressions - statically known to be in a position expecting a type typically - include being on the right-hand side of `:`, `<:`, `<<:` and after - the comma in a `forall` expression. - -- As a refinement of the previous rule, in the case of applied global - references, notations in a non-opened scope with delimiter - specifically defined for this applied global reference take priority - over notations in a non-opened scope with delimiter for generic - applications. For instance, in the presence of ``Notation "f ( x - )" := (f x) (at level 10, format "f ( x )") : app_scope`` and - ``Notation "x '.+1'" := (S x) (at level 10, format "x '.+1'") : - mynat_scope.`` and both of ``app_scope`` and ``mynat_scope`` being - bound to a delimiter *and* both not opened, the latter, more - specific notation will always take precedence over the first, more - generic one. - -- A scope can be closed by using :cmd:`Close Scope` and its delimiter - removed by using :cmd:`Undelimit Scope`. To remove automatic - temporary opening of scopes for arguments of a constant, use - :ref:`Arguments <ArgumentScopes>`. - .. _Abbreviations: Abbreviations |