From 9bb8c5c98a17810cc9f20309e1b45c2ce0b69ff0 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 5 May 2015 18:57:09 -0700
Subject: [PATCH] test(tests/lean/hott): test 'obtain' in the HoTT library

---
 tests/lean/hott/obtain_hott.hlean | 36 +++++++++++++++++++++++++++++++
 1 file changed, 36 insertions(+)
 create mode 100644 tests/lean/hott/obtain_hott.hlean

diff --git a/tests/lean/hott/obtain_hott.hlean b/tests/lean/hott/obtain_hott.hlean
new file mode 100644
index 000000000..3f6c0178a
--- /dev/null
+++ b/tests/lean/hott/obtain_hott.hlean
@@ -0,0 +1,36 @@
+open prod sigma
+
+theorem tst2 (A B C D : Type) : (A × B) × (C × D) → C × B × A :=
+assume p : (A × B) × (C × D),
+obtain [a b] [c d], from p,
+(c, (b, a))
+
+theorem tst22 (A B C D : Type) : (A × B) × (C × D) → C × B × A :=
+assume p,
+obtain [a b] [c d], from p,
+(c, (b, a))
+
+theorem tst3 (A B C D : Type) : A × B × C × D → C × B × A :=
+assume p,
+obtain a b c d, from p,
+(c, (b, a))
+
+example (p q : nat → nat → Type) : (Σ x y, p x y × q x y × q y x) → Σ x y, p x y :=
+assume ex,
+obtain x y pxy qxy qyx, from ex,
+⟨x, y, pxy⟩
+
+example (p : nat → nat → Type): (Σ x, p x x) → (Σ x y, p x y) :=
+assume sig,
+obtain x pxx, from sig,
+⟨x, x, pxx⟩
+
+open nat
+definition even (a : nat) := Σ x, a = 2*x
+
+example (a b : nat) (H₁ : even a) (H₂ : even b) : even (a+b) :=
+obtain x (Hx : a = 2*x), from H₁,
+obtain y (Hy : b = 2*y), from H₂,
+⟨x+y,
+ calc a+b = 2*x + 2*y : by rewrite [Hx, Hy]
+      ... = 2*(x+y)   : sorry⟩