From 2f3db0b605b3aa345c1fea26c263ba6793a0fa51 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 17 Jan 2019 16:17:41 +0100 Subject: [ssr] compile "=> {} y" as "=> {y} y" --- doc/sphinx/proof-engine/ssreflect-proof-language.rst | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'doc') diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 92bd4dbd1d..59d64feece 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -1559,7 +1559,7 @@ whose general syntax is i_view ::= {? %{%} } /@term %| /ltac:( @tactic ) .. prodn:: - i_pattern ::= @ident %| > %| _ %| ? %| * %| + %| {? @occ_switch } -> %| {? @occ_switch }<- %| [ {?| @i_item } ] %| - %| [: {+ @ident } ] + i_pattern ::= {? %{%} } @ident %| > %| _ %| ? %| * %| + %| {? @occ_switch } -> %| {? @occ_switch }<- %| [ {?| @i_item } ] %| - %| [: {+ @ident } ] .. prodn:: i_block ::= [^ @ident ] %| [^~ @ident ] %| [^~ @num ] @@ -1615,6 +1615,10 @@ annotation: views are interpreted opening the ``ssripat`` scope. 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. + An empty occurrence switch ``{}`` has the effect of clearing + the :token:`ident` before performing the introduction of :token:`ident`. + In other words by prefixing the :token:`ident` with ``{}`` one can + *replace* the context entry. ``>`` pops every variable occurring in the rest of the stack. Type class instances are popped even if they don't occur -- cgit v1.2.3 From 1b9c386bb5118145f0a2b46c523dd195d97c8413 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 17 Jan 2019 18:01:42 +0100 Subject: [ssr] compile "=> {x..} y" as "=> {x..y} y" This is for consistency with "rewrite {x..} y" --- doc/sphinx/proof-engine/ssreflect-proof-language.rst | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) (limited to 'doc') diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 59d64feece..c058279207 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -1592,9 +1592,13 @@ of the remaining subgoals. 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 ``move/term``. The optional flag ``{}`` can -be used to signal that the :token:`term`, when it is a context entry, -has to be cleared. +It is equivalent to ``move/term``. + +A :token:`clear_switch` that immediately precedes an :token:`i_view` +that happen to be a :token:`ident` is extended with that +:token:`ident` and the :token:`clear_switch` is executed after the view. +Eg ``{}/v`` is equivalent to ``/v{v}``. + 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. @@ -1615,8 +1619,9 @@ annotation: views are interpreted opening the ``ssripat`` scope. 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. - An empty occurrence switch ``{}`` has the effect of clearing - the :token:`ident` before performing the introduction of :token:`ident`. + A :token:`clear_switch` (even an empty one) immediately preceding a + :token:`ident` is extended with that :token:`ident` if the identifier + points to an existing context entry. In other words by prefixing the :token:`ident` with ``{}`` one can *replace* the context entry. ``>`` -- cgit v1.2.3 From be7e584921ca1bed7e37c2d15ab2def0e8dfe484 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 21 Jan 2019 10:47:17 +0100 Subject: [ssr] better structure the ipats doc --- .../proof-engine/ssreflect-proof-language.rst | 46 ++++++++++++++++------ 1 file changed, 33 insertions(+), 13 deletions(-) (limited to 'doc') diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index c058279207..d40474188f 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -1559,7 +1559,7 @@ whose general syntax is i_view ::= {? %{%} } /@term %| /ltac:( @tactic ) .. prodn:: - i_pattern ::= {? %{%} } @ident %| > %| _ %| ? %| * %| + %| {? @occ_switch } -> %| {? @occ_switch }<- %| [ {?| @i_item } ] %| - %| [: {+ @ident } ] + i_pattern ::= @ident %| > %| _ %| ? %| * %| + %| {? @occ_switch } -> %| {? @occ_switch }<- %| [ {?| @i_item } ] %| - %| [: {+ @ident } ] .. prodn:: i_block ::= [^ @ident ] %| [^~ @ident ] %| [^~ @num ] @@ -1572,6 +1572,9 @@ 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 @@ -1583,12 +1586,15 @@ An :token:`s_item` can simplify the set of subgoals or the subgoals themselves: ``/= //``, i.e., ``simpl; try done``. -When an :token:`s_item` bears a :token:`clear_switch`, then the +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`. @@ -1612,6 +1618,9 @@ Notations can be used to name tactics, for example:: 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` @@ -1621,9 +1630,8 @@ annotation: views are interpreted opening the ``ssripat`` scope. required to expose the top variable or assumption. A :token:`clear_switch` (even an empty one) immediately preceding a :token:`ident` is extended with that :token:`ident` if the identifier - points to an existing context entry. - In other words by prefixing the :token:`ident` with ``{}`` one can - *replace* the context entry. + points to an existing context entry. As a consequence by prefixing the + :token:`ident` with ``{}`` one can *replace* a context entry. ``>`` pops every variable occurring in the rest of the stack. Type class instances are popped even if they don't occur @@ -1717,6 +1725,9 @@ annotation: views are interpreted opening the ``ssripat`` scope. 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:: @@ -1739,6 +1750,9 @@ 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 @@ -1763,6 +1777,9 @@ interpretation, e.g.: are all equivalent. +Block introduction +`````````````````` + |SSR| supports the following :token:`i_block`\s: :n:`[^ @ident ]` @@ -3039,13 +3056,20 @@ operation should be performed: pattern. In its simplest form, it is a regular term. If no explicit redex switch is present the rewrite pattern to be matched is inferred from the :token:`r_item`. -+ This optional term, or the :token:`r_item`, may be preceded by an occurrence - switch (see section :ref:`selectors_ssr`) or a clear item - (see section :ref:`discharge_ssr`), - these two possibilities being exclusive. An occurrence switch selects ++ This optional term, or the :token:`r_item`, may be preceded by an + :token:`occ_switch` (see section :ref:`selectors_ssr`) or a + :token:`clear_switch` (see section :ref:`discharge_ssr`), + these two possibilities being exclusive. + + An occurrence switch selects the occurrences of the rewrite pattern which should be affected by the rewrite operation. + A clear switch, even an empty one, is is performed *after* the + :token:`r_item` is actually processed and is complemented with the name of + the rewrite rule when it is a simple context entry. As a consequence one can + write ``rewrite {}H`` to rewrite with ``H`` and dispose ``H`` immediately + afterwards. An :token:`r_item` can be: @@ -3300,10 +3324,6 @@ the rewrite tactic. The effect of the tactic on the initial goal is to rewrite this lemma at the second occurrence of the first matching ``x + y + 0`` of the explicit rewrite redex ``_ + y + 0``. -An empty occurrence switch ``{}`` is not interpreted as a valid occurrence -switch. It has the effect of clearing the :token:`r_item` (when it is the name -of a context entry). - Occurrence selection and repetition ``````````````````````````````````` -- cgit v1.2.3 From 60113af483a6cd98a4b26ae7ee7d76c9380f341d Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Tue, 22 Jan 2019 10:07:59 +0100 Subject: Apply suggestions from code review Co-Authored-By: gares --- doc/sphinx/proof-engine/ssreflect-proof-language.rst | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'doc') diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index d40474188f..ae721c2430 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -1598,12 +1598,12 @@ 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 ``move/term``. +It is equivalent to :n:`move/@term`. A :token:`clear_switch` that immediately precedes an :token:`i_view` that happen to be a :token:`ident` is extended with that :token:`ident` and the :token:`clear_switch` is executed after the view. -Eg ``{}/v`` is equivalent to ``/v{v}``. +E.g. ``{}/v`` is equivalent to ``/v{v}``. If the next :token:`i_item` is a view, then the view is applied to the assumption in top position once all the @@ -1628,7 +1628,7 @@ Intro patterns 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 a + A :token:`clear_switch` (even an empty one) immediately preceding an :token:`ident` is extended with that :token:`ident` if the identifier points to an existing context entry. As a consequence by prefixing the :token:`ident` with ``{}`` one can *replace* a context entry. @@ -3065,7 +3065,7 @@ operation should be performed: the occurrences of the rewrite pattern which should be affected by the rewrite operation. - A clear switch, even an empty one, is is performed *after* the + A clear switch, even an empty one, is performed *after* the :token:`r_item` is actually processed and is complemented with the name of the rewrite rule when it is a simple context entry. As a consequence one can write ``rewrite {}H`` to rewrite with ``H`` and dispose ``H`` immediately -- cgit v1.2.3 From 5cf39fac26282b63b2c90663ef0be3c4e7b051ff Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 22 Jan 2019 11:13:10 +0100 Subject: clarify when an ident is added to the clear switch --- doc/sphinx/proof-engine/ssreflect-proof-language.rst | 18 +++++++++++++----- 1 file changed, 13 insertions(+), 5 deletions(-) (limited to 'doc') diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index ae721c2430..d7aa0e1b07 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -1601,10 +1601,14 @@ 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` -that happen to be a :token:`ident` is extended with that -:token:`ident` and the :token:`clear_switch` is executed after the view. +is complemented with the name of the view whenever the :token:`i_view` +is a simple proof context entry [#10]_. E.g. ``{}/v`` is equivalent to ``/v{v}``. +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. @@ -1629,8 +1633,9 @@ Intro patterns 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 extended with that :token:`ident` if the identifier - points to an existing context entry. As a consequence by prefixing the + :token:`ident` is complemented with that :token:`ident` 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. ``>`` pops every variable occurring in the rest of the stack. @@ -3067,7 +3072,8 @@ operation should be performed: A clear switch, even an empty one, is performed *after* the :token:`r_item` is actually processed and is complemented with the name of - the rewrite rule when it is a simple context entry. As a consequence one can + the rewrite rule when it is a simple proof context entry [#10]_. + As a consequence one can write ``rewrite {}H`` to rewrite with ``H`` and dispose ``H`` immediately afterwards. @@ -5549,3 +5555,5 @@ Settings in the metatheory .. [#9] The current state of the proof shall be displayed by the Show Proof command of |Coq| proof mode. +.. [#10] A simple proof context entry is a naked identifier (i.e. not between + parentheses) designating a context entry that is not a section variable. -- cgit v1.2.3 From fddca21344c6f72f7442f2a44fd46212b11ac521 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 24 Jan 2019 14:33:01 +0100 Subject: [doc] explain how to avoid automatic clears --- doc/sphinx/proof-engine/ssreflect-proof-language.rst | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'doc') diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index d7aa0e1b07..8c1ca036cb 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -1604,6 +1604,9 @@ A :token:`clear_switch` that immediately precedes an :token:`i_view` is complemented with the name of the view whenever 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. @@ -1637,6 +1640,8 @@ Intro patterns 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 @@ -3076,6 +3081,7 @@ operation should be performed: As a consequence one can write ``rewrite {}H`` to rewrite with ``H`` and dispose ``H`` immediately afterwards. + This behavior can be avoided by putting parentheses around the rewrite rule. An :token:`r_item` can be: -- cgit v1.2.3 From b62320f274b221d44ef3fb9c17d1444cd1179ac6 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 24 Jan 2019 14:51:16 +0100 Subject: [doc] more precise description of when automatic clears are triggered --- doc/sphinx/proof-engine/ssreflect-proof-language.rst | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'doc') diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 8c1ca036cb..7c597d3ffa 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -1601,7 +1601,7 @@ 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 whenever the :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` @@ -1636,8 +1636,8 @@ Intro patterns 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 the identifier - is a simple proof context entry [#10]_. + :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` @@ -3077,7 +3077,7 @@ operation should be performed: A clear switch, even an empty one, is performed *after* the :token:`r_item` is actually processed and is complemented with the name of - the rewrite rule when it is a simple proof context entry [#10]_. + the rewrite rule if an only if it is a simple proof context entry [#10]_. As a consequence one can write ``rewrite {}H`` to rewrite with ``H`` and dispose ``H`` immediately afterwards. -- cgit v1.2.3 From 932880e247e963116b576701e76ce18b3450bec1 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 24 Jan 2019 14:53:56 +0100 Subject: [doc] warn that (automatic) clears can result in errors --- doc/sphinx/proof-engine/ssreflect-proof-language.rst | 10 ++++++++++ 1 file changed, 10 insertions(+) (limited to 'doc') diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 7c597d3ffa..483dbd311d 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -1445,6 +1445,16 @@ 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 ```````````````````````````` -- cgit v1.2.3