[ssr] implement "under i: ext_lemma" by rewrite rule

Still to do: renaming the bound variables afterwards

1 files changed, 29 insertions, 0 deletions

diff --git a/test-suite/ssr/under.v b/test-suite/ssr/under.v
new file mode 100644
index 0000000000..43d319737a
--- /dev/null
+++ b/test-suite/ssr/under.v
@@ -0,0 +1,29 @@
+Require Import ssreflect.
+
+Inductive body :=
+ mk_body : bool -> nat -> nat -> body.
+
+Axiom big : (nat -> body) -> nat.
+
+Axiom eq_big :
+ forall P Q F G,
+(forall x, P x = Q x :> bool) ->
+ (forall x, (P x =true -> F x = G x : Type)) ->
+  big (fun x => mk_body (P x) (F x) x) = big (fun toto => mk_body (Q toto) (F toto) toto).
+
+Axiom leb : nat -> nat -> bool.
+
+Axiom admit : False.
+
+Lemma test :
+  (big (fun x => mk_body (leb x 3) (S x + x) x))
+ = 3.
+Proof.
+
+ under i : {1}eq_big.
+  { by apply over. }
+  { move=> Pi. by apply over. }
+ rewrite /=.
+
+ case: admit.
+Qed.