[ssr] under: Strenghten over & Add test_big_andb

* Rely on a new tactic unify_helper that workarounds the fact
  [apply Under.under_done] cannot unify (?G i...) with (expr i...) in
  [|- @Under T (expr i...) (?G i...)]
  when expr is a constant expression, or has more than one var (i...).
  Idea: massage the expression with Ltac to obtain a beta redex.

* Simplify test-suite/ssr/under.v by using TestSuite.ssr_mini_mathcomp
  and add a test-case [test_big_andb].

* Summary of commands to quickly test [under]:
  $ cd .../coq
  $ make plugins/ssr/ssreflect.vo plugins/ssr/ssrfun.vo plugins/ssr/ssrbool.vo
  $ cd test-suite
  $ touch prerequisite/ssr_mini_mathcomp.v
  $ make
  $ emacs under.v

3 files changed, 46 insertions, 63 deletions

diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v
index 229f6ceb1a..7e2c1c913f 100644
--- a/plugins/ssr/ssreflect.v
+++ b/plugins/ssr/ssreflect.v
@@ -550,8 +550,33 @@ End Under.
 Register Under as plugins.ssreflect.Under.
 Register Under_from_eq as plugins.ssreflect.Under_from_eq.
 
+Ltac beta_expand c e :=
+  match e with
+  | ?G ?z =>
+    let T := type of z in
+    match c with
+    | context f [z] =>
+      let b := constr:(fun x : T => ltac:(let r := context f [x] in refine r)) in
+      rewrite -{1}[c]/(b z); beta_expand b G
+    | (* constante *) _ =>
+      let b := constr:(fun x : T => ltac:(exact c)) in
+      rewrite -{1}[c]/(b z); beta_expand b G
+    end
+  | ?G => idtac
+  end.
+
+Ltac unify_helper :=
+  move=> *;
+  lazymatch goal with
+  | [ |- @Under _ ?c ?e ] =>
+    beta_expand c e
+  end.
+
 Ltac over :=
-  solve [ apply Under.under_done | by rewrite over ].
+  solve [ apply Under.under_done
+        | by rewrite over
+        | unify_helper; eapply Under.under_done
+        ].
 
 (* The 2 variants below wouldn't work on [test-suite/ssr/over.v:test_over_2_1]
    (2-var test case with evars).
diff --git a/test-suite/ssr/over.v b/test-suite/ssr/over.v
index c6bccd1d77..3bb5c03e08 100644
--- a/test-suite/ssr/over.v
+++ b/test-suite/ssr/over.v
@@ -45,8 +45,6 @@ assert (H : i + 2 * j - i = x2 i j).
   apply Under_from_eq.
   Fail done.
 
-  Fail over. (* Bug: doesn't work so we have to make a beta-expansion by hand *)
-  rewrite -[i + 2 * j - i]/((fun x y => x + 2 * y - x) i j). (* todo: automate? *)
   over.
   myadmit.
 Qed.
@@ -64,7 +62,8 @@ assert (H : i + 2 * j - i = x2 i j).
 
   rewrite over.
   Fail done. (* Bug: doesn't work so we have to make a beta-expansion by hand *)
-  rewrite -[i + 2 * j - i]/((fun x y => x + 2 * y - x) i j). (* todo: automate? *)
+  rewrite -[i + 2 * j - i]/((fun x y => x + 2 * y - x) i j).
+  (* cf. [plugins/ssr/ssreflect.v:unify_helper] *)
   done.
   myadmit.
 Qed.
diff --git a/test-suite/ssr/under.v b/test-suite/ssr/under.v
index 066f89cfcf..cc85b96a3a 100644
--- a/test-suite/ssr/under.v
+++ b/test-suite/ssr/under.v
@@ -1,4 +1,6 @@
 Require Import ssreflect.
+Require Import ssrbool TestSuite.ssr_mini_mathcomp.
+Global Unset SsrOldRewriteGoalsOrder.
 
 (* under <names>: {occs}[patt]<lemma>.
    under <names>: {occs}[patt]<lemma> by tac1.
@@ -16,17 +18,9 @@ Module Mocks.
 (* Mock bigop.v definitions to test the behavior of under with bigops
    without requiring mathcomp *)
 
-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.
-
 Definition eqfun :=
   fun (A B : Type) (f g : forall _ : B, A) => forall x : B, @eq A (f x) (g x).
 
-Definition pred := fun T : Type => forall _ : T, bool.
-
 Section Defix.
 Variables (T : Type) (n : nat) (f : forall _ : T, T) (x : T).
 Fixpoint loop (m : nat) : T :=
@@ -37,18 +31,6 @@ Fixpoint loop (m : nat) : T :=
 Definition iter := loop n.
 End Defix.
 
-Definition addn := nosimpl plus.
-Definition subn := nosimpl minus.
-Definition muln := nosimpl mult.
-
-Fixpoint seq_iota (m n : nat) {struct n} : list nat :=
-  match n return (list nat) with
-  | O => @nil nat
-  | S n' => @cons nat m (seq_iota (S m) n')
-  end.
-
-Definition index_iota := fun m n : nat => seq_iota m (subn n m).
-
 Parameter eq_bigl :
   forall (R : Type) (idx : R) (op : forall (_ : R) (_ : R), R) (I : Type)
          (r : list I) (P1 P2 : pred I) (F : forall _ : I, R) (_ : @eqfun bool I P1 P2),
@@ -74,25 +56,9 @@ Parameter big_const_nat :
     @eq R (@bigop R nat idx (index_iota m n) (fun i : nat => @BigBody R nat i op true x))
         (@iter R (subn n m) (op x) idx).
 
-Delimit Scope bool_scope with B.
-Open Scope bool_scope.
-
 Delimit Scope N_scope with num.
 Delimit Scope nat_scope with N.
 
-Delimit Scope big_scope with BIG.
-Open Scope big_scope.
-
-Reserved Notation "~~ b" (at level 35, right associativity).
-Notation "~~ b" := (negb b) : bool_scope.
-
-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 ']'").
-
 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 ']'").
@@ -100,31 +66,15 @@ 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 ']'").
 
-Notation "\big [ op / idx ]_ ( m <= i < n | P ) F" :=
-  (bigop idx (index_iota m n) (fun i : nat => BigBody i op P%B F))
-     : big_scope.
-Notation "\big [ op / idx ]_ ( m <= i < n ) F" :=
-  (bigop idx (index_iota m n) (fun i : nat => BigBody i op true F))
-     : big_scope.
-
 Local Notation "+%N" := addn (at level 0, only parsing).
 
 Notation "\sum_ ( m <= i < n | P ) F" :=
-  (\big[+%N/0%N]_(m <= i < n | P%B) F%N) : nat_scope.
+  (\big[+%N/0%N]_(m <= i < n | P%B) F%N) : (*nat_scope*) big_scope.
 Notation "\sum_ ( m <= i < n ) F" :=
-  (\big[+%N/0%N]_(m <= i < n) F%N) : nat_scope.
-
-Fixpoint odd n := if n is S n' then ~~ odd n' else false.
-
-Parameter addnC : forall m n : nat, m + n = n + m.
-Parameter mulnC : forall m n : nat, m * n = n * m.
-Parameter addnA : forall x y z : nat, x + (y + z) = ((x + y) + z).
-Parameter mulnA : forall x y z : nat, x * (y * z) = ((x * y) * z).
+  (\big[+%N/0%N]_(m <= i < n) F%N) : (*nat_scope*) big_scope.
 
 Parameter iter_addn_0 : forall m n : nat, @eq nat (@iter nat n (addn m) O) (muln m n).
 
-Notation "x == y" := (Nat.eqb x y)
-  (at level 70, no associativity) : bool_scope.
 End Mocks.
 
 Import Mocks.
@@ -138,7 +88,7 @@ Proof.
 (* in interactive mode *)
 under i Hi: eq_bigr.
   under j Hj: eq_big.
-  { by rewrite mulnC /= addnC /= over. }
+  { by rewrite muln1 over. }
   { by rewrite addnC over. }
   over.
 done.
@@ -149,7 +99,7 @@ Lemma test_big_nested_2 (F G : nat -> nat) (m n : nat) :
   \sum_(0 <= i < m) \sum_(0 <= j < n | odd j) (j + i).
 Proof.
 (* in one-liner mode *)
-under i I: eq_bigr by under j J: eq_big by [rewrite mulnC /= addnC|rewrite addnC].
+under i Hi: eq_bigr by under j Hj: eq_big by [rewrite muln1 | rewrite addnC].
 done.
 Qed.
 
@@ -167,8 +117,7 @@ Lemma test_big_patt2 (F G : nat -> nat) (n : nat) :
   \sum_(0 <= i < n) 0 + \sum_(0 <= i < n) (F i * 2).
 Proof.
 under i Hi: [X in _ = _ + X]eq_bigr.
-  (* the proof is not idiomatic as mathcomp lemmas are not available here *)
-  rewrite mulnC /= addnA -plus_n_O.
+  rewrite mulnS muln1.
   over.
 by rewrite big_const_nat iter_addn_0.
 Qed.
@@ -177,7 +126,7 @@ Lemma test_big_occs (F G : nat -> nat) (n : nat) :
   \sum_(0 <= i < n) (i * 0) = \sum_(0 <= i < n) (i * 0) + \sum_(0 <= i < n) (i * 0).
 Proof.
 under i Hi: {2}[in RHS]eq_bigr.
-  by rewrite mulnC /= over.
+  by rewrite muln0 /= over.
 by rewrite big_const_nat iter_addn_0.
 Qed.
 
@@ -190,3 +139,13 @@ under a A: [RHS]eq_bigr by under b B: eq_bigr by []. (* renaming bound vars *)
 simpl.
 myadmit.
 Qed.
+
+Lemma test_big_andb (F : nat -> nat) (m n : nat) :
+  \sum_(0 <= i < 5 | odd i && (i == 1)) i = 1.
+Proof.
+under i: eq_bigl by rewrite andb_idl; first by move/eqP->.
+simpl.
+under i: eq_bigr by move/eqP=>{1}->. (* the 2nd occ should not be touched *)
+simpl.
+myadmit.
+Qed.