[ssr] under: Add opaque modules for tagging and notation support

(Note: coq notations cannot contain \n)

Co-authored-by: Enrico Tassi <Enrico.Tassi@inria.fr>

1 files changed, 50 insertions, 0 deletions

diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v
index 4721e19a8b..e0b775f07b 100644
--- a/plugins/ssr/ssreflect.v
+++ b/plugins/ssr/ssreflect.v
@@ -500,3 +500,53 @@ Hint View for apply/ iffRLn|2 iffLRn|2 iffRL|2 iffLR|2.
 Lemma abstract_context T (P : T -> Type) x :
   (forall Q, Q = P -> Q x) -> P x.
 Proof. by move=> /(_ P); apply. Qed.
+
+(*****************************************************************************)
+(* Syntax proposal for the under tactic:
+
+under i: eq_bigr by []. (* renaming *)
+
+under i: eq_bigr.
+  by rewrite addnC over.
+(* oneliner version *)
+under i: eq_bigr by rewrite adnnC.
+
+under i: lem => /andP [H1 H2].
+  by rewrite addnC over.
+(* oneliner version *)
+under i: lem by move => /andP [H1 H2]; rewrite addnC.
+
+(* 2-var version *)
+under i j: {2}[in RHS]eq_mx.
+(* ... *)
+
+(* nested version *)
+under i: eq_bigr=> ?; under j: eq_bigl.
+ *)
+
+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.
+Parameter over :
+  forall (T : Type) (x : T),
+  @Under T x x <-> True.
+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.
+End Under.
+
+Register Under as plugins.ssreflect.Under.
+Register Under_from_eq as plugins.ssreflect.Under_from_eq.