[ssr] Define both a lemma "over" (in sig UNDER) and an ltac "over"

Both can be use to close the "under goals", in rewrite style or in
closing-tactic style.

Contrarily to the previous implementation that assumed
  "over : forall (T : Type) (x : T), @Under T x x <-> True"
this new design won't require the Setoid library.

Extend the test-suite (in test-suite/ssr/under.v)

2 files changed, 148 insertions, 14 deletions

diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v
index e0b775f07b..d2b44a869a 100644
--- a/plugins/ssr/ssreflect.v
+++ b/plugins/ssr/ssreflect.v
@@ -528,25 +528,49 @@ Module Type UNDER.
 Parameter Under :
   forall (R : Type), R -> R -> Prop.
 Parameter Under_from_eq :
-  forall (T : Type) (x y : T),
-  @Under T x y -> x = y.
+  forall (T : Type) (x y : T), @Under T x y -> x = y.
+
+(** [Over, over, over_done]: for "by rewrite over" *)
+Parameter Over :
+  forall (R : Type), R -> R -> Prop.
 Parameter over :
-  forall (T : Type) (x : T),
-  @Under T x x <-> True.
+  forall (T : Type) (x : T) (y : T), @Under T x y = @Over T x y.
+Parameter over_done :
+  forall (T : Type) (x : T), @Over T x x.
+(* We need both hints below, otherwise the test-suite does not pass *)
+Hint Extern 0 (@Over _ _ _) => solve [ apply over_done ] : core.
+(* => for test_under_eq_big *)
+Hint Resolve over_done : core.
+(* => for test_over_1_1 *)
+
+(** [under_done]: for Ltac-style over *)
+Parameter under_done :
+  forall (T : Type) (x : T), @Under T x x.
 Notation "''Under[' x ]" := (@Under _ x _)
   (at level 8, format "''Under['  x  ]").
 End UNDER.
 
 Module Export Under : UNDER.
 Definition Under := @eq.
-Definition Under_done := @refl_equal.
 Lemma Under_from_eq (T : Type) (x y : T) :
   @Under T x y -> x = y.
-Proof. easy. Qed.
-Lemma over (T : Type) (x : T) :
-  @Under T x x <-> True.
-Proof. easy. Qed.
+Proof. by []. Qed.
+Definition Over := Under.
+Lemma over :
+  forall (T : Type) (x : T) (y : T), @Under T x y = @Over T x y.
+Proof. by []. Qed.
+Lemma over_done :
+  forall (T : Type) (x : T), @Over T x x.
+Proof. by []. Qed.
+Lemma under_done :
+  forall (T : Type) (x : T), @Under T x x.
+Proof. by []. Qed.
 End Under.
 
 Register Under as plugins.ssreflect.Under.
 Register Under_from_eq as plugins.ssreflect.Under_from_eq.
+
+Ltac over :=
+  by apply Under.under_done.
+(* [exact: Under.under_done] woud be more satisfying,
+   but issue with 2-var test-suite (test_over_2_2) *)
diff --git a/test-suite/ssr/under.v b/test-suite/ssr/under.v
index 9947d2bf4c..67e4316ba8 100644
--- a/test-suite/ssr/under.v
+++ b/test-suite/ssr/under.v
@@ -1,5 +1,75 @@
 Require Import ssreflect.
 
+Axiom admit : False.
+
+(** Testing over for the 1-var case *)
+Lemma test_over_1_1 : forall i : nat, False.
+intros.
+evar (I : Type); evar (R : Type); evar (x2 : I -> R).
+assert (H : i + 2 * i - i = x2 i).
+  unfold x2 in *; clear x2;
+  unfold R in *; clear R;
+  unfold I in *; clear I.
+  apply Under_from_eq.
+  Fail done.
+
+  over.
+  case: admit.
+Qed.
+
+Lemma test_over_1_2 : forall i : nat, False.
+intros.
+evar (I : Type); evar (R : Type); evar (x2 : I -> R).
+assert (H : i + 2 * i - i = x2 i).
+  unfold x2 in *; clear x2;
+  unfold R in *; clear R;
+  unfold I in *; clear I.
+  apply Under_from_eq.
+  Fail done.
+
+  by rewrite over.
+  case: admit.
+Qed.
+
+(** Testing over for the 2-var case *)
+
+Lemma test_over_2_1 : forall i j : nat, False.
+intros.
+evar (I : Type); evar (J : Type); evar (R : Type); evar (x2 : I -> J -> R).
+assert (H : i + 2 * j - i = x2 i j).
+  unfold x2 in *; clear x2;
+  unfold R in *; clear R;
+  unfold J in *; clear J;
+  unfold I in *; clear I.
+  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.
+  case: admit.
+Qed.
+
+Lemma test_over_2_2 : forall i j : nat, False.
+intros.
+evar (I : Type); evar (J : Type); evar (R : Type); evar (x2 : I -> J -> R).
+assert (H : i + 2 * j - i = x2 i j).
+  unfold x2 in *; clear x2;
+  unfold R in *; clear R;
+  unfold J in *; clear J;
+  unfold I in *; clear I.
+  apply Under_from_eq.
+  Fail done.
+
+  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? *)
+  done.
+  case: admit.
+Qed.
+
+(** Testing under for the 1-var case *)
+
 Inductive body :=
  mk_body : bool -> nat -> nat -> body.
 
@@ -13,17 +83,57 @@ Axiom eq_big :
 
 Axiom leb : nat -> nat -> bool.
 
-Axiom admit : False.
+Axiom addnC : forall p q : nat, p + q = q + p.
 
-Lemma test :
+Lemma test_under_eq_big :
   (big (fun x => mk_body (leb x 3) (S x + x) x))
  = 3.
 Proof.
  Set Debug Ssreflect.
- under i : {1}eq_big.
-  { by apply over. }
-  { move=> Pi. by apply over. }
+ under i : {1}[in LHS]eq_big.
+
+  { over. }
+  { move=> Pi; by rewrite addnC over. }
+
  rewrite /=.
 
  case: admit.
 Qed.
+Unset Debug Ssreflect.
+
+(** 2-var test
+
+Erik: Note that this axiomatization does not faithfully follow that of
+mathcomp’s implementation of matrices. We may want to refine this test
+once [eq_mx] has been integrated in mathcomp. *)
+
+Axiom I_ : nat -> Type.
+
+(* Inductive matrix (R : Type) (m n : nat) : Type := Matrix (_ : list (I_ m * I_ n * R)). *)
+Inductive matrix (R : Type) (m n : nat) : Type := Matrix (_ : I_ m -> I_ n -> R).
+
+Axiom mx_of_fun : forall (R : Type) (m n : nat),
+  unit -> (I_ m -> I_ n -> R) -> matrix R m n.
+
+Axiom eq_mx : forall (R : Type) m n (k : unit) (F1 F2 : I_ m -> I_ n -> R),
+  (forall foo bar, F1 foo bar = F2 foo bar) ->
+  (mx_of_fun R m n k (fun a b => F1 a b)) = (mx_of_fun R m n k (fun c d => F2 c d)).
+Arguments eq_mx [R m n k F1] F2 _.
+
+Definition fun_of_mx (R : Type) (m n : nat) (M : matrix R m n) :=
+  let: Matrix _ _ _ F := M in F.
+
+Coercion fun_of_mx : matrix >-> Funclass.
+
+Definition addmx : forall (m n : nat) (A B : matrix nat m n), matrix nat m n :=
+  fun m n A B => mx_of_fun nat m n tt (fun x y => A x y + B x y).
+Arguments addmx [m n].
+
+Lemma test_under_eq_mx (m n : nat) (A B C : matrix nat m n) :
+  addmx (addmx A B) C = addmx C (addmx A B).
+Proof.
+(* Set Debug Ssreflect. *)
+under i j : [addmx C _ in RHS]eq_mx.
+  by rewrite addnC over.
+done.
+Qed.