From c9454e2f4a083006d7145389beabcf8e4b10caa9 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Fri, 1 Mar 2019 19:47:41 +0100
Subject: [ssr] under: Add doc for {under, over} & Add entry in CHANGES.md

* For better uniformity, replace "intro-pattern" with "intro pattern"
  in the ssr doc.
---
 .../proof-engine/ssreflect-proof-language.rst      | 239 ++++++++++++++++++++-
 1 file changed, 235 insertions(+), 4 deletions(-)

(limited to 'doc/sphinx/proof-engine')

diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index b240cef40c..a4ab038314 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,230 @@ rewriting rule is stated using Leibniz equality (as opposed to setoid
 relations). It will be extended to other rewriting relations in the
 future.
 
+.. _under_over_ssr:
+
+A convenience under tactic
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+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 G : (nat -> nat) -> nat -> nat.
+      Axiom eq_G :
+        forall F1 F2 : nat -> nat,
+        (forall n : nat, F1 n = F2 n) ->
+        forall n : nat, G F1 n = G F2 n.
+
+   .. coqtop:: all
+
+      Lemma example_G (n : nat) : G (fun n => n - n) n >= 0.
+
+   In this context, one cannot directly use ``eq_G``:
+
+   .. coqtop:: all fail
+
+      rewrite eq_G.
+
+   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. We can thus do:
+
+   .. coqtop:: all abort
+
+      rewrite (@eq_G _ (fun _ : nat => 0)); last first.
+        by move=> m; rewrite subnn.
+
+   Otherwise, a more convenient approach consists in relying on the
+   :tacn:`under` tactic that alleviates this bookkeeping:
+
+   .. coqtop:: all abort
+
+      Lemma example_G (n : nat) : G (fun n => n - n) n >= 0.
+      under m: eq_G by rewrite subnn.
+
+  ``(* FIXME: replace with do... *)``
+
+.. tacn:: under {? @occ_switch} {? [ @r_pattern ] } @term {? => @i_item} {? do ( @tactic | [ {*| @tactic } ] ) }
+   :name: under
+
+    Rewrite under :token:`term`. 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.
+
+   .. exn:: Incorrect number of tactics (expected N tactics, was given N').
+
+      This error can occur when using the version with a ``do`` clause.
+
+.. _under_interactive:
+
+Interactive mode
+````````````````
+The execution of the Ltac expression:
+:n:`under {@occ_switch}[@r_pattern]@term => [i|j].`
+involves the following steps:
+
++ It performs a full-blown :n:`rewrite {@occ_switch}[@r_pattern]@term`,
+  without failing like in the above example with ``eq_G``, but
+  creating evars.
++ As a 2-branches intro pattern is provided, it checks that 3 subgoals
+  have been created (the last one being the initial, main subgoal that
+  now contains some evars).
++ In the first 2 subgoals, it introduces ``i``, resp. ``j``, and tests
+  whether these 2 subgoals are (quantified) equalities involving
+  an evar. For example: ``some_expr(i) = ?Goal i``.
++ If this is the case, the subgoal is manipulated to get the
+  provably equivalent goal ``Under _ (some_expr i) (?Goal i)``,
+  pretty-printed as ``Under[ some_expr i ]``.
+  This change avoids instantiating the evar by accident (e.g., if one
+  uses a proof script such as: :n:`rewrite lem1 // lem2`).
++ Finally, a post-processing step is performed in the main (here, 3rd)
+  subgoal to try keeping (in the object after the rewrite) the same
+  bound variables as the identifers provided in the first
+  intro pattern branch (here, ``i``).
+
+If the intro pattern is omitted, the Ltac expression:
+:n:`under {@occ_switch}[@r_pattern]@term.` defaults to:
+:n:`under {@occ_switch}[@r_pattern]@term => *.`
+
+Two equivalent facilities (a terminator and a lemma) are provided to
+close intermediate subgoal ``Under[ … ]`` and instantiate the
+corresponding evar:
+
+.. 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`` lemma.
+
+Let us focus again on the simple example involving an extensionality
+lemma ``eq_G``, but this time in interactive mode:
+
+.. example::
+
+   .. coqtop:: all abort
+
+      Lemma example_G (n : nat) : G (fun n => n - n) n >= 0.
+      under m: eq_G.
+        rewrite subnn.
+        over.
+
+   ``(* FIXME: replace with do... *)``
+
+.. _under_one_liner:
+
+One-liner mode
+``````````````
+
+The Ltac expression:
+:n:`under {@occ_switch}[@r_pattern]@term => [i|j] do [tac1|tac2]`
+can be viewed as a shorter form for the following Ltac expression:
+:n:`under {@occ_switch}[@r_pattern]@term => [i|j]; [tac1; over | tac2; over | cbv beta iota].`
+
+Here, the ``beta-iota`` reduction is useful to get rid of the beta
+redexes that will typically be introduced after the substitution of
+the evars by the :tacn:`under` tactic.
+
+Note that the provided tactics (e.g., ``tac1``) can just 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 are optional, i.e.:
+:n:`under @term => i do [tac1]` can be
+shortened to: :n:`under @term => i do tac1.`
+
+.. example::
+
+   .. coqtop:: reset none
+
+      From Coq Require Import ssreflect.
+      Set Implicit Arguments.
+      Unset Strict Implicit.
+      Unset Printing Implicit Defensive.
+
+      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 ']'").
+      Reserved Notation "\big [ op / idx ]_ ( m <= i < n ) F"
+        (at level 36, F at level 36, op, idx at level 10, i, m, n at level 50,
+                 format "'[' \big [ op / idx ]_ ( m  <=  i  <  n ) '/  '  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, P x = true -> 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 ']'").
+      Reserved Notation "\sum_ ( m <= i < n ) F"
+        (at level 41, F at level 41, i, m, n at level 50,
+                 format "'[' \sum_ ( m  <=  i  <  n ) '/  '  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 "\big [ op / idx ]_ ( m <= i < n ) F" :=
+        (bigop idx (index_iota m n) (fun i : nat => BigBody i op true F)).
+
+      Notation "\sum_ ( m <= i < n | P ) F" :=
+        (\big[plus/O]_(m <= i < n | P%bool) F%nat).
+      Notation "\sum_ ( m <= i < n ) F" :=
+        (\big[plus/O]_(m <= i < n) F%nat).
+
+   .. coqtop:: in
+
+      Parameter addnC : forall m n : nat, m + n = n + m.
+      Parameter muln1 : forall n : nat, n * 1 = n.
+      Parameter odd : nat -> bool.
+
+   .. coqtop:: all
+
+      Lemma test_big_nested (F G : nat -> nat) (m n : nat) :
+        \sum_(0 <= a < m) \sum_(0 <= j < n | odd (j * 1)) (a + j) =
+        \sum_(0 <= i < m) \sum_(0 <= j < n | odd j) (j + i).
+      under i I: eq_bigr by under j J: eq_big by [rewrite muln1|rewrite addnC].
+
+   ``(* FIXME: replace with do... *)``
 
 .. _locking_ssr:
 
@@ -5373,7 +5596,15 @@ respectively.
 
 .. tacn:: rewrite {+ @r_step }
 
-   rewrite  (see :ref:`rewriting_ssr`)
+   rewrite (see :ref:`rewriting_ssr`)
+
+.. tacn:: under {? @occ_switch} {? [ @r_pattern ] } @term {? => @i_item} {? do ( @tactic | [ {*| @tactic } ] )}
+
+   under (see :ref:`under_over_ssr`)
+
+.. tacn:: over
+
+   over (see :ref:`under_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 }
-- 
cgit v1.2.3


From e68bccba9344c1b3d77d3e815af6cce1ce50b731 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 21 Mar 2019 10:08:29 +0100
Subject: [ssr] new syntax for the under tactic

---
 doc/sphinx/proof-engine/ssreflect-proof-language.rst | 10 +++-------
 1 file changed, 3 insertions(+), 7 deletions(-)

(limited to 'doc/sphinx/proof-engine')

diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index a4ab038314..cb529bd68e 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -3692,9 +3692,7 @@ complete terms, as shown by the simple example below.
    .. coqtop:: all abort
 
       Lemma example_G (n : nat) : G (fun n => n - n) n >= 0.
-      under m: eq_G by rewrite subnn.
-
-  ``(* FIXME: replace with do... *)``
+      under eq_G => n do rewrite subnn.
 
 .. tacn:: under {? @occ_switch} {? [ @r_pattern ] } @term {? => @i_item} {? do ( @tactic | [ {*| @tactic } ] ) }
    :name: under
@@ -3762,7 +3760,7 @@ lemma ``eq_G``, but this time in interactive mode:
    .. coqtop:: all abort
 
       Lemma example_G (n : nat) : G (fun n => n - n) n >= 0.
-      under m: eq_G.
+      under eq_G => m.
         rewrite subnn.
         over.
 
@@ -3857,9 +3855,7 @@ shortened to: :n:`under @term => i do tac1.`
       Lemma test_big_nested (F G : nat -> nat) (m n : nat) :
         \sum_(0 <= a < m) \sum_(0 <= j < n | odd (j * 1)) (a + j) =
         \sum_(0 <= i < m) \sum_(0 <= j < n | odd j) (j + i).
-      under i I: eq_bigr by under j J: eq_big by [rewrite muln1|rewrite addnC].
-
-   ``(* FIXME: replace with do... *)``
+      under eq_bigr => i Hi do under eq_big => [j|j Hj] do [rewrite muln1|rewrite addnC].
 
 .. _locking_ssr:
 
-- 
cgit v1.2.3


From 96513a4a8bb361aee6034b1f76127acaf613415a Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Tue, 2 Apr 2019 15:49:12 +0200
Subject: [ssr] under: Fix and extend the documentation

---
 .../proof-engine/ssreflect-proof-language.rst      | 74 +++++++++++++---------
 1 file changed, 44 insertions(+), 30 deletions(-)

(limited to 'doc/sphinx/proof-engine')

diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index cb529bd68e..0df0f937a6 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -3683,7 +3683,7 @@ complete terms, as shown by the simple example below.
 
    .. coqtop:: all abort
 
-      rewrite (@eq_G _ (fun _ : nat => 0)); last first.
+      rewrite (@eq_G _ (fun _ : nat => 0)).
         by move=> m; rewrite subnn.
 
    Otherwise, a more convenient approach consists in relying on the
@@ -3692,7 +3692,7 @@ complete terms, as shown by the simple example below.
    .. coqtop:: all abort
 
       Lemma example_G (n : nat) : G (fun n => n - n) n >= 0.
-      under eq_G => n do rewrite subnn.
+      under eq_G => m do rewrite subnn.
 
 .. tacn:: under {? @occ_switch} {? [ @r_pattern ] } @term {? => @i_item} {? do ( @tactic | [ {*| @tactic } ] ) }
    :name: under
@@ -3714,28 +3714,39 @@ The execution of the Ltac expression:
 :n:`under {@occ_switch}[@r_pattern]@term => [i|j].`
 involves the following steps:
 
-+ It performs a full-blown :n:`rewrite {@occ_switch}[@r_pattern]@term`,
-  without failing like in the above example with ``eq_G``, but
-  creating evars.
-+ As a 2-branches intro pattern is provided, it checks that 3 subgoals
-  have been created (the last one being the initial, main subgoal that
-  now contains some evars).
-+ In the first 2 subgoals, it introduces ``i``, resp. ``j``, and tests
-  whether these 2 subgoals are (quantified) equalities involving
-  an evar. For example: ``some_expr(i) = ?Goal i``.
-+ If this is the case, the subgoal is manipulated to get the
-  provably equivalent goal ``Under _ (some_expr i) (?Goal i)``,
-  pretty-printed as ``Under[ some_expr i ]``.
-  This change avoids instantiating the evar by accident (e.g., if one
-  uses a proof script such as: :n:`rewrite lem1 // lem2`).
-+ Finally, a post-processing step is performed in the main (here, 3rd)
-  subgoal to try keeping (in the object after the rewrite) the same
-  bound variables as the identifers provided in the first
-  intro pattern branch (here, ``i``).
-
-If the intro pattern is omitted, the Ltac expression:
-:n:`under {@occ_switch}[@r_pattern]@term.` defaults to:
-:n:`under {@occ_switch}[@r_pattern]@term => *.`
+1. It performs a full-blown :n:`rewrite {@occ_switch}[@r_pattern]@term`,
+   without failing like in the above example with ``eq_G``, but
+   creating evars.
+
+2. As a 2-branches intro pattern is provided, it checks that 3 subgoals
+   have been created (the last one being the initial, main subgoal that
+   now contains some evars).
+
+3. In the first 2 subgoals, it introduces ``i``, resp. ``j``, and tests
+   whether these 2 subgoals are (quantified) equalities involving
+   an evar. For example: ``some_expr(i) = ?Goal i``.
+
+4. If this is the case, the subgoal is manipulated to get the
+   provably equivalent goal ``Under _ (some_expr i) (?Goal i)``,
+   pretty-printed as ``'Under[ some_expr i ]``.
+   This change avoids instantiating the evar by accident (e.g., if one
+   uses a proof script such as: :n:`rewrite lem1 // lem2`).
+
+5. Finally, a post-processing step is performed in the main (here, 3rd)
+   subgoal to try keeping (in the object after the rewrite) the same
+   bound variables as the identifers provided in the first
+   intro pattern branch (here, ``i``).
+
+Notes:
+
++ For the steps 3. and 4. above, the :tacn:`under` tactic also
+  supports subgoals of the form ``some_expr(i) <-> ?Goal i``, which
+  are "protected" in the form ``Under_iff (some_expr i) (?Goal i)``,
+  itself pretty-printed as ``'Under_iff[ some_expr i ]``.
+
++ If the intro pattern is omitted, the Ltac expression:
+  :n:`under {@occ_switch}[@r_pattern]@term.` defaults to:
+  :n:`under {@occ_switch}[@r_pattern]@term => *.`
 
 Two equivalent facilities (a terminator and a lemma) are provided to
 close intermediate subgoal ``Under[ … ]`` and instantiate the
@@ -3745,13 +3756,18 @@ corresponding evar:
    :name: over
 
    This terminator tactic allows one to close goals of the form
-   ``Under[ … ]``.
+   ``'Under[ … ]`` or ``'Under_iff[ … ]``.
 
 .. tacv:: by rewrite over
 
    This is a variant of :tacn:`over` in order to close ``Under[ … ]``
    goals, relying on the ``over`` lemma.
 
+.. tacv:: by rewrite over_iff
+
+   This is a variant of :tacn:`over` in order to close ``Under_iff[ … ]``
+   goals, relying on the ``over_iff`` lemma.
+
 Let us focus again on the simple example involving an extensionality
 lemma ``eq_G``, but this time in interactive mode:
 
@@ -3764,8 +3780,6 @@ lemma ``eq_G``, but this time in interactive mode:
         rewrite subnn.
         over.
 
-   ``(* FIXME: replace with do... *)``
-
 .. _under_one_liner:
 
 One-liner mode
@@ -3774,11 +3788,11 @@ One-liner mode
 The Ltac expression:
 :n:`under {@occ_switch}[@r_pattern]@term => [i|j] do [tac1|tac2]`
 can be viewed as a shorter form for the following Ltac expression:
-:n:`under {@occ_switch}[@r_pattern]@term => [i|j]; [tac1; over | tac2; over | cbv beta iota].`
+:n:`under {@occ_switch}[@r_pattern]@term => [i|j|]; [tac1; over | tac2; over | cbv beta iota].`
 
 Here, the ``beta-iota`` reduction is useful to get rid of the beta
-redexes that will typically be introduced after the substitution of
-the evars by the :tacn:`under` tactic.
+redexes that could be introduced after the substitution of the evars
+by the :tacn:`under` tactic.
 
 Note that the provided tactics (e.g., ``tac1``) can just as well
 involve other :tacn:`under` tactics. See below for a typical example
-- 
cgit v1.2.3


From 04da1739139c8d96469a2b86280e520e532beb39 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Wed, 3 Apr 2019 01:08:38 +0200
Subject: [ssr] under: Fix the defective form ("=> [*|*]" implied) and its doc

* Add tests accordingly.
---
 .../proof-engine/ssreflect-proof-language.rst      | 32 ++++++++++++----------
 1 file changed, 18 insertions(+), 14 deletions(-)

(limited to 'doc/sphinx/proof-engine')

diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 0df0f937a6..c32788c9da 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -3737,17 +3737,13 @@ involves the following steps:
    bound variables as the identifers provided in the first
    intro pattern branch (here, ``i``).
 
-Notes:
+Note:
 
 + For the steps 3. and 4. above, the :tacn:`under` tactic also
   supports subgoals of the form ``some_expr(i) <-> ?Goal i``, which
   are "protected" in the form ``Under_iff (some_expr i) (?Goal i)``,
   itself pretty-printed as ``'Under_iff[ some_expr i ]``.
 
-+ If the intro pattern is omitted, the Ltac expression:
-  :n:`under {@occ_switch}[@r_pattern]@term.` defaults to:
-  :n:`under {@occ_switch}[@r_pattern]@term => *.`
-
 Two equivalent facilities (a terminator and a lemma) are provided to
 close intermediate subgoal ``Under[ … ]`` and instantiate the
 corresponding evar:
@@ -3790,17 +3786,25 @@ The Ltac expression:
 can be viewed as a shorter form for the following Ltac expression:
 :n:`under {@occ_switch}[@r_pattern]@term => [i|j|]; [tac1; over | tac2; over | cbv beta iota].`
 
-Here, the ``beta-iota`` reduction is useful to get rid of the beta
-redexes that could be introduced after the substitution of the evars
-by the :tacn:`under` tactic.
+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 (e.g., ``tac1``) can just as well
+  involve other :tacn:`under` tactics. See below for a typical example
+  involving the `bigop` theory from the Mathematical Components library.
 
-Note that the provided tactics (e.g., ``tac1``) can just 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 are optional, i.e.:
+  :n:`under @term => [i] do [tac1]` is equivalent to:
+  :n:`under @term => i do tac1.` and that shorter form should be
+  preferred.
 
-If there is only one tactic, the brackets are optional, i.e.:
-:n:`under @term => i do [tac1]` can be
-shortened to: :n:`under @term => i do tac1.`
++ If the ``do`` clause is provided but the intro pattern is omitted,
+  the Ltac expression:
+  :n:`under {@occ_switch}[@r_pattern]@term do [tac1|tac2]` defaults to:
+  :n:`under {@occ_switch}[@r_pattern]@term => [*|*] do [tac1|tac2].`
 
 .. example::
 
-- 
cgit v1.2.3


From e1e5d40a0f351cbf01f7e66d049f9a937d5f8563 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 3 Apr 2019 14:36:57 +0200
Subject: [doc] ssr_under: a few improvements

---
 .../proof-engine/ssreflect-proof-language.rst      | 214 ++++++++++++---------
 1 file changed, 122 insertions(+), 92 deletions(-)

(limited to 'doc/sphinx/proof-engine')

diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index c32788c9da..7545e1b8d7 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -3636,10 +3636,10 @@ rewriting rule is stated using Leibniz equality (as opposed to setoid
 relations). It will be extended to other rewriting relations in the
 future.
 
-.. _under_over_ssr:
+.. _under_ssr:
 
-A convenience under tactic
-~~~~~~~~~~~~~~~~~~~~~~~~~~
+Rewriting under binders
+~~~~~~~~~~~~~~~~~~~~~~~
 
 Goals involving objects defined with higher-order functions often
 require "rewriting under binders". While setoid rewriting is a
@@ -3661,92 +3661,127 @@ complete terms, as shown by the simple example below.
    .. coqtop:: in
 
       Axiom subnn : forall n : nat, n - n = 0.
-      Parameter G : (nat -> nat) -> nat -> nat.
-      Axiom eq_G :
+      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 n : nat, G F1 n = G F2 n.
+        forall l : list nat, map F1 l = map F2 l.
 
    .. coqtop:: all
 
-      Lemma example_G (n : nat) : G (fun n => n - n) n >= 0.
+      Lemma example_map l : sumlist (map (fun m => m - m) l) = 0.
 
-   In this context, one cannot directly use ``eq_G``:
+   In this context, one cannot directly use ``eq_map``:
 
    .. coqtop:: all fail
 
-      rewrite eq_G.
+      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. We can thus do:
+   rewriting step. In order to perform the rewrie step one has to
+   provide the term by hand as follows:
 
    .. coqtop:: all abort
 
-      rewrite (@eq_G _ (fun _ : nat => 0)).
+      rewrite (@eq_map _ (fun _ : nat => 0)).
         by move=> m; rewrite subnn.
 
-   Otherwise, a more convenient approach consists in relying on the
-   :tacn:`under` tactic that alleviates this bookkeeping:
+   The :tacn:`under` tactic lets one perform the same operation in a more
+   convenient way:
 
    .. coqtop:: all abort
 
-      Lemma example_G (n : nat) : G (fun n => n - n) n >= 0.
-      under eq_G => m do rewrite subnn.
+      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 {? @occ_switch} {? [ @r_pattern ] } @term {? => @i_item} {? do ( @tactic | [ {*| @tactic } ] ) }
+.. tacn:: under {? @r_prefix } @term {? => {+ @i_item}} {? do ( @tactic | [ {*| @tactic } ] ) }
    :name: under
 
-    Rewrite under :token:`term`. 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.
+   Operate under the context proved to be extensional by
+   lemma :token:`term`.
 
-   .. exn:: Incorrect number of tactics (expected N tactics, was given N').
+   .. 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.
+        by over.
+
 The execution of the Ltac expression:
-:n:`under {@occ_switch}[@r_pattern]@term => [i|j].`
+
+:n:`under @term => [ @i_item__1 | … | @i_item__n ].`
+
 involves the following steps:
 
-1. It performs a full-blown :n:`rewrite {@occ_switch}[@r_pattern]@term`,
-   without failing like in the above example with ``eq_G``, but
-   creating evars.
+1. It performs a :n:`rewrite @term`
+   without failing like in the above example with ``eq_map``, but
+   creating evars (see :tacn:`evar`). If :n:`term` is prefixed by
+   a pattern or an occurrence selector, then the modifiers is 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. 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).
 
-2. As a 2-branches intro pattern is provided, it checks that 3 subgoals
-   have been created (the last one being the initial, main subgoal that
-   now contains some evars).
+4. If so :tacn:`under` executes the corresponding
+   intro pattern :n:`@ipat__i` in each goal.
 
-3. In the first 2 subgoals, it introduces ``i``, resp. ``j``, and tests
-   whether these 2 subgoals are (quantified) equalities involving
-   an evar. For example: ``some_expr(i) = ?Goal i``.
+5. Then :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).
 
-4. If this is the case, the subgoal is manipulated to get the
-   provably equivalent goal ``Under _ (some_expr i) (?Goal i)``,
-   pretty-printed as ``'Under[ some_expr i ]``.
-   This change avoids instantiating the evar by accident (e.g., if one
-   uses a proof script such as: :n:`rewrite lem1 // lem2`).
+6. The expression inside the ``Under[ … ]`` notation can be
+   proved equivalent to the desired expression
+   by using a regular tacn:`rewrite` tactic.
 
-5. Finally, a post-processing step is performed in the main (here, 3rd)
-   subgoal to try keeping (in the object after the rewrite) the same
-   bound variables as the identifers provided in the first
-   intro pattern branch (here, ``i``).
+7. Interactive editing of the first n goals has to be signalled by
+   using the :tacn:`over` tactic or rewrite rule (see below).
 
-Note:
+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.
 
-+ For the steps 3. and 4. above, the :tacn:`under` tactic also
-  supports subgoals of the form ``some_expr(i) <-> ?Goal i``, which
-  are "protected" in the form ``Under_iff (some_expr i) (?Goal i)``,
-  itself pretty-printed as ``'Under_iff[ some_expr i ]``.
+.. _over_ssr:
+
+The over tactic
++++++++++++++++
 
 Two equivalent facilities (a terminator and a lemma) are provided to
-close intermediate subgoal ``Under[ … ]`` and instantiate the
-corresponding evar:
+close intermediate subgoals generated by :tacn:`under` (i.e. goals
+displayed as ``Under[ … ]``):
 
 .. tacn:: over
    :name: over
@@ -3764,27 +3799,18 @@ corresponding evar:
    This is a variant of :tacn:`over` in order to close ``Under_iff[ … ]``
    goals, relying on the ``over_iff`` lemma.
 
-Let us focus again on the simple example involving an extensionality
-lemma ``eq_G``, but this time in interactive mode:
-
-.. example::
-
-   .. coqtop:: all abort
-
-      Lemma example_G (n : nat) : G (fun n => n - n) n >= 0.
-      under eq_G => m.
-        rewrite subnn.
-        over.
-
 .. _under_one_liner:
 
 One-liner mode
 ``````````````
 
 The Ltac expression:
-:n:`under {@occ_switch}[@r_pattern]@term => [i|j] do [tac1|tac2]`
-can be viewed as a shorter form for the following Ltac expression:
-:n:`under {@occ_switch}[@r_pattern]@term => [i|j|]; [tac1; over | tac2; over | cbv beta iota].`
+
+: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:
 
@@ -3792,19 +3818,19 @@ Notes:
   redexes that could be introduced after the substitution of the evars
   by the :tacn:`under` tactic.
 
-+ Note that the provided tactics (e.g., ``tac1``) can just as well
++ 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 are optional, i.e.:
-  :n:`under @term => [i] do [tac1]` is equivalent to:
-  :n:`under @term => i do tac1.` and that shorter form should be
++ 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 but the intro pattern is omitted,
-  the Ltac expression:
-  :n:`under {@occ_switch}[@r_pattern]@term do [tac1|tac2]` defaults to:
-  :n:`under {@occ_switch}[@r_pattern]@term => [*|*] do [tac1|tac2].`
++ If the ``do`` clause is provided and the intro pattern is omitted,
+  then the defeault :token:`i_item` ``*`` is applied to each branch.
+  Eg the Ltac expression
+  :n:`under @term do [ @tac__1 | … | @tac__n ]` is equivalent to
+  :n:`under @term => [ * | … | * ] do [ @tac__1 | … | @tac__n ].`
 
 .. example::
 
@@ -3815,27 +3841,25 @@ Notes:
       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 ']'").
-      Reserved Notation "\big [ op / idx ]_ ( m <= i < n ) F"
-        (at level 36, F at level 36, op, idx at level 10, i, m, n at level 50,
-                 format "'[' \big [ op / idx ]_ ( m  <=  i  <  n ) '/  '  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 :
+      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, P x = true -> F1 x = F2 x) ->
+          (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 :
+      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) ->
@@ -3846,34 +3870,40 @@ Notes:
       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 ']'").
-      Reserved Notation "\sum_ ( m <= i < n ) F"
-        (at level 41, F at level 41, i, m, n at level 50,
-                 format "'[' \sum_ ( m  <=  i  <  n ) '/  '  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 "\big [ op / idx ]_ ( m <= i < n ) F" :=
-        (bigop idx (index_iota m n) (fun i : nat => BigBody i op true F)).
 
       Notation "\sum_ ( m <= i < n | P ) F" :=
         (\big[plus/O]_(m <= i < n | P%bool) F%nat).
-      Notation "\sum_ ( m <= i < n ) F" :=
-        (\big[plus/O]_(m <= i < n) 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.
-      Parameter odd : nat -> bool.
 
    .. coqtop:: all
 
-      Lemma test_big_nested (F G : nat -> nat) (m n : nat) :
-        \sum_(0 <= a < m) \sum_(0 <= j < n | odd (j * 1)) (a + j) =
-        \sum_(0 <= i < m) \sum_(0 <= j < n | odd j) (j + i).
-      under eq_bigr => i Hi do under eq_big => [j|j Hj] do [rewrite muln1|rewrite addnC].
+      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:
 
@@ -5612,13 +5642,13 @@ respectively.
 
    rewrite (see :ref:`rewriting_ssr`)
 
-.. tacn:: under {? @occ_switch} {? [ @r_pattern ] } @term {? => @i_item} {? do ( @tactic | [ {*| @tactic } ] )}
+.. tacn:: under {? @r_prefix } @term {? => {+ @i_item}} {? do ( @tactic | [ {*| @tactic } ] )}
 
-   under (see :ref:`under_over_ssr`)
+   under (see :ref:`under_ssr`)
 
 .. tacn:: over
 
-   over (see :ref:`under_over_ssr`)
+   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 }
-- 
cgit v1.2.3


From 4bc91ba5654574d156ebf2934a6fb36d31b40ff9 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Wed, 3 Apr 2019 15:03:02 +0200
Subject: [ssr] Define over as a rewrite rule & Merge 'Under[ _ ] notations

as suggested by @gares, and:

* Rename some Under_* terms for better uniformity;
* Update & Improve minor details in the documentation.
---
 .../proof-engine/ssreflect-proof-language.rst      | 39 ++++++++++------------
 1 file changed, 17 insertions(+), 22 deletions(-)

(limited to 'doc/sphinx/proof-engine')

diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 7545e1b8d7..a40dfa486f 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -3680,7 +3680,7 @@ complete terms, as shown by the simple example below.
 
    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 rewrie step one has to
+   rewriting step. In order to perform the rewrite step one has to
    provide the term by hand as follows:
 
    .. coqtop:: all abort
@@ -3742,30 +3742,30 @@ The execution of the Ltac expression:
 involves the following steps:
 
 1. It performs a :n:`rewrite @term`
-   without failing like in the above example with ``eq_map``, but
-   creating evars (see :tacn:`evar`). If :n:`term` is prefixed by
-   a pattern or an occurrence selector, then the modifiers is honoured.
+   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. Then :tacn:`under` checks that the first n subgoals
+3. If so :tacn:`under` 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).
 
-4. If so :tacn:`under` executes the corresponding
-   intro pattern :n:`@ipat__i` in each goal.
-
-5. Then :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).
+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.
+   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).
@@ -3787,17 +3787,12 @@ displayed as ``Under[ … ]``):
    :name: over
 
    This terminator tactic allows one to close goals of the form
-   ``'Under[ … ]`` or ``'Under_iff[ … ]``.
+   ``'Under[ … ]``.
 
 .. tacv:: by rewrite over
 
    This is a variant of :tacn:`over` in order to close ``Under[ … ]``
-   goals, relying on the ``over`` lemma.
-
-.. tacv:: by rewrite over_iff
-
-   This is a variant of :tacn:`over` in order to close ``Under_iff[ … ]``
-   goals, relying on the ``over_iff`` lemma.
+   goals, relying on the ``over`` rewrite rule.
 
 .. _under_one_liner:
 
@@ -3828,8 +3823,8 @@ Notes:
 
 + If the ``do`` clause is provided and the intro pattern is omitted,
   then the defeault :token:`i_item` ``*`` is applied to each branch.
-  Eg the Ltac expression
-  :n:`under @term do [ @tac__1 | … | @tac__n ]` is equivalent to
+  E.g., the Ltac expression:
+  :n:`under @term do [ @tac__1 | … | @tac__n ]` is equivalent to:
   :n:`under @term => [ * | … | * ] do [ @tac__1 | … | @tac__n ].`
 
 .. example::
-- 
cgit v1.2.3


From 36488400952da5e12c8af451b1a936a34b26039d Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Wed, 3 Apr 2019 15:39:11 +0200
Subject: [ssr] under: optimization of the tactic for (under eq_bigl => *)

so it acts "more naturally" like (under eq_bigl; [hnf|]); move=> [*|].

Also: replace "by over." in the doc example with "over."
---
 doc/sphinx/proof-engine/ssreflect-proof-language.rst | 15 +++++++++------
 1 file changed, 9 insertions(+), 6 deletions(-)

(limited to 'doc/sphinx/proof-engine')

diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index a40dfa486f..4e40df6f94 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -3733,7 +3733,7 @@ Let us redo the running example in interactive mode.
       Lemma example_map l : sumlist (map (fun m => m - m) l) = 0.
       under eq_map => m.
         rewrite subnn.
-        by over.
+        over.
 
 The execution of the Ltac expression:
 
@@ -3751,8 +3751,9 @@ involves the following steps:
    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` executes the corresponding
-   intro pattern :n:`@ipat__i` in each goal.
+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
@@ -3805,7 +3806,7 @@ The Ltac expression:
 
 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 ].`
+:n:`(under @term) => [ @i_item__1 | … | @i_item__n | ]; [ @tac__1; over | … | @tac__n; over | cbv beta iota ].`
 
 Notes:
 
@@ -3822,10 +3823,12 @@ Notes:
   preferred.
 
 + If the ``do`` clause is provided and the intro pattern is omitted,
-  then the defeault :token:`i_item` ``*`` is applied to each branch.
+  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 ].`
+  :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::
 
-- 
cgit v1.2.3