From 717f77bbaf479ae1e8335ce226ad71c2c88df644 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 31 May 2018 16:12:33 +0200
Subject: [ssr] implement "under i: ext_lemma" by rewrite rule

Still to do: renaming the bound variables afterwards
---
 test-suite/ssr/under.v | 29 +++++++++++++++++++++++++++++
 1 file changed, 29 insertions(+)
 create mode 100644 test-suite/ssr/under.v

(limited to 'test-suite')

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.
-- 
cgit v1.2.3