From 72c607846a62bd55dd1c2d6c094b4d12ac9a65be Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 28 Jan 2014 16:05:46 -0800
Subject: [PATCH] test(tests/lean): add Jeremy's proof to test suite

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 tests/lean/j1.lean              | 25 +++++++++++++++++++++++++
 tests/lean/j1.lean.expected.out |  8 ++++++++
 2 files changed, 33 insertions(+)
 create mode 100644 tests/lean/j1.lean
 create mode 100644 tests/lean/j1.lean.expected.out

diff --git a/tests/lean/j1.lean b/tests/lean/j1.lean
new file mode 100644
index 000000000..d4fc14a2e
--- /dev/null
+++ b/tests/lean/j1.lean
@@ -0,0 +1,25 @@
+import tactic
+import macros
+
+definition bracket (A : Type) : Bool :=
+      ∀ p : Bool, (A → p) → p
+
+rewrite_set basic
+add_rewrite imp_truel imp_truer imp_id eq_id : basic
+set_option simp_tac::assumptions false
+
+theorem bracket_eq (x : Bool) : bracket x = x
+:= boolext
+    (assume H : ∀ p : Bool, (x → p) → p,
+       (have ((x → x) → x) = x : by simp basic) ◂ H x)
+    (assume H : x,
+       take p,
+          assume Hxp : x → p,
+            Hxp H)
+
+add_rewrite bracket_eq eq_id
+
+theorem coerce (a b : Bool) (H : @eq Type a b) : @eq Bool a b
+:=  calc a   = bracket a  : by simp
+         ... = bracket b  : @subst Type a b (λ x : Type, bracket a = bracket x) (refl (bracket a)) H
+         ... = b          : by simp
diff --git a/tests/lean/j1.lean.expected.out b/tests/lean/j1.lean.expected.out
new file mode 100644
index 000000000..12d73ac85
--- /dev/null
+++ b/tests/lean/j1.lean.expected.out
@@ -0,0 +1,8 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Imported 'tactic'
+  Imported 'macros'
+  Defined: bracket
+  Set: simp_tac::assumptions
+  Proved: bracket_eq
+  Proved: coerce