From 43633085b95a67053f97617cb070c31d01f21fdd Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 16 Dec 2014 13:28:43 -0800
Subject: [PATCH] fix(tests/lean): adjust tests to recent changes in the lean
 libraries

---
 tests/lean/hott/329.hlean                     | 19 ++++++++++++
 tests/lean/hott/366.hlean                     |  7 +++++
 .../apply_class_issue.hlean}                  |  4 +--
 tests/lean/hott/beginend2.hlean               | 10 ++++++
 tests/lean/hott/get_tac1.hlean                | 10 ++++++
 tests/lean/run/329.lean                       | 20 ------------
 tests/lean/run/366.lean                       |  8 -----
 tests/lean/run/beginend2.lean                 | 12 -------
 tests/lean/run/fibrant.lean                   |  4 ---
 tests/lean/run/get_tac1.lean                  | 11 -------
 tests/lean/slow/path_ind.lean                 | 31 -------------------
 11 files changed, 47 insertions(+), 89 deletions(-)
 create mode 100644 tests/lean/hott/329.hlean
 create mode 100644 tests/lean/hott/366.hlean
 rename tests/lean/{run/apply_class_issue.lean => hott/apply_class_issue.hlean} (71%)
 create mode 100644 tests/lean/hott/beginend2.hlean
 create mode 100644 tests/lean/hott/get_tac1.hlean
 delete mode 100644 tests/lean/run/329.lean
 delete mode 100644 tests/lean/run/366.lean
 delete mode 100644 tests/lean/run/beginend2.lean
 delete mode 100644 tests/lean/run/fibrant.lean
 delete mode 100644 tests/lean/run/get_tac1.lean
 delete mode 100644 tests/lean/slow/path_ind.lean

diff --git a/tests/lean/hott/329.hlean b/tests/lean/hott/329.hlean
new file mode 100644
index 000000000..e50722551
--- /dev/null
+++ b/tests/lean/hott/329.hlean
@@ -0,0 +1,19 @@
+open eq sigma
+
+variables {A : Type} {B : A → Type} {C : Πa, B a → Type} {D : Πa b, C a b → Type}
+          {a a' a'' : A} {b b₁ b₂ : B a} {b' : B a'} {b'' : B a''} {u v w : Σa, B a}
+
+definition path_sigma_dpair (p : a = a') (q : p ▹ b = b') : dpair a b = dpair a' b' :=
+eq.rec_on p (λb b' q, eq.rec_on q idp) b b' q
+
+definition path_sigma (p :  dpr1 u = dpr1 v) (q : p ▹ dpr2 u = dpr2 v) : u = v :=
+destruct u
+         (λu1 u2, destruct v (λ v1 v2, path_sigma_dpair))
+         p q
+
+definition path_path_sigma_lemma' {p1 : a = a'} {p2 : p1 ▹ b = b'} {q2 : p1 ▹ b = b'}
+    (s : idp ▹ p2 = q2) : path_sigma p1 p2 = path_sigma p1 q2 :=
+begin
+  apply (eq.rec_on s),
+  apply idp,
+end
diff --git a/tests/lean/hott/366.hlean b/tests/lean/hott/366.hlean
new file mode 100644
index 000000000..1efc92e20
--- /dev/null
+++ b/tests/lean/hott/366.hlean
@@ -0,0 +1,7 @@
+open eq
+definition foo (A : Type) : Type := Π (a : A), a = a
+definition thm : Π (A : Type), foo A :=
+begin
+  intros,
+  apply idp
+end
diff --git a/tests/lean/run/apply_class_issue.lean b/tests/lean/hott/apply_class_issue.hlean
similarity index 71%
rename from tests/lean/run/apply_class_issue.lean
rename to tests/lean/hott/apply_class_issue.hlean
index d0035b74c..e36d28a2e 100644
--- a/tests/lean/run/apply_class_issue.lean
+++ b/tests/lean/hott/apply_class_issue.hlean
@@ -1,9 +1,7 @@
-import hott.trunc
 open truncation
---structure is_contr [class] (A : Type) : Type
 
 context
-parameters {P : Π(A : Type), A → Prop}
+parameters {P : Π(A : Type), A → Type}
 
 definition my_contr {A : Type} [H : is_contr A] (a : A) : P A a := sorry
 
diff --git a/tests/lean/hott/beginend2.hlean b/tests/lean/hott/beginend2.hlean
new file mode 100644
index 000000000..c02cbe02c
--- /dev/null
+++ b/tests/lean/hott/beginend2.hlean
@@ -0,0 +1,10 @@
+open eq tactic
+open eq (rec_on)
+
+definition concat_whisker2 {A} {x y z : A} (p p' : x = y) (q q' : y = z) (a : p = p') (b : q = q') :
+  (whiskerR a q) ⬝ (whiskerL p' b) = (whiskerL p b) ⬝ (whiskerR a q') :=
+begin
+  apply (rec_on b),
+  apply (rec_on a),
+  apply ((concat_1p _)⁻¹),
+end
diff --git a/tests/lean/hott/get_tac1.hlean b/tests/lean/hott/get_tac1.hlean
new file mode 100644
index 000000000..b404277e9
--- /dev/null
+++ b/tests/lean/hott/get_tac1.hlean
@@ -0,0 +1,10 @@
+open eq
+
+definition concat_pV_p {A : Type} {x y z : A} (p : x = z) (q : y = z) : (p ⬝ q⁻¹) ⬝ q = p :=
+begin
+  generalize p,
+  apply (eq.rec_on q),
+  intro p,
+  apply (eq.rec_on p),
+  apply idp
+end
diff --git a/tests/lean/run/329.lean b/tests/lean/run/329.lean
deleted file mode 100644
index 02cdb8828..000000000
--- a/tests/lean/run/329.lean
+++ /dev/null
@@ -1,20 +0,0 @@
-import hott data.sigma
-open path sigma
-
-variables {A : Type} {B : A → Type} {C : Πa, B a → Type} {D : Πa b, C a b → Type}
-          {a a' a'' : A} {b b₁ b₂ : B a} {b' : B a'} {b'' : B a''} {u v w : Σa, B a}
-
-definition path_sigma_dpair (p : a ≈ a') (q : p ▹ b ≈ b') : dpair a b ≈ dpair a' b' :=
-path.rec_on p (λb b' q, path.rec_on q idp) b b' q
-
-definition path_sigma (p :  dpr1 u ≈ dpr1 v) (q : p ▹ dpr2 u ≈ dpr2 v) : u ≈ v :=
-destruct u
-         (λu1 u2, destruct v (λ v1 v2, path_sigma_dpair))
-         p q
-
-definition path_path_sigma_lemma' {p1 : a ≈ a'} {p2 : p1 ▹ b ≈ b'} {q2 : p1 ▹ b ≈ b'}
-    (s : idp ▹ p2 ≈ q2) : path_sigma p1 p2 ≈ path_sigma p1 q2 :=
-begin
-  apply (path.rec_on s),
-  apply idp,
-end
diff --git a/tests/lean/run/366.lean b/tests/lean/run/366.lean
deleted file mode 100644
index 897344e54..000000000
--- a/tests/lean/run/366.lean
+++ /dev/null
@@ -1,8 +0,0 @@
-import hott.path
-open path
-definition foo (A : Type) : Type := Π (a : A), a ≈ a
-definition thm : Π (A : Type), foo A :=
-begin
-  intros,
-  apply idp
-end
diff --git a/tests/lean/run/beginend2.lean b/tests/lean/run/beginend2.lean
deleted file mode 100644
index 502dd2be4..000000000
--- a/tests/lean/run/beginend2.lean
+++ /dev/null
@@ -1,12 +0,0 @@
-import hott.path
-
-open path tactic
-open path (rec_on)
-
-definition concat_whisker2 {A} {x y z : A} (p p' : x ≈ y) (q q' : y ≈ z) (a : p ≈ p') (b : q ≈ q') :
-  (whiskerR a q) ⬝ (whiskerL p' b) ≈ (whiskerL p b) ⬝ (whiskerR a q') :=
-begin
-  apply (rec_on b),
-  apply (rec_on a),
-  apply ((concat_1p _)⁻¹),
-end
diff --git a/tests/lean/run/fibrant.lean b/tests/lean/run/fibrant.lean
deleted file mode 100644
index f503ff6d2..000000000
--- a/tests/lean/run/fibrant.lean
+++ /dev/null
@@ -1,4 +0,0 @@
-import hott.fibrant
-open prod sum fibrant
-
-theorem test_fibrant : fibrant (nat × (nat ⊎ nat))
diff --git a/tests/lean/run/get_tac1.lean b/tests/lean/run/get_tac1.lean
deleted file mode 100644
index f90219e21..000000000
--- a/tests/lean/run/get_tac1.lean
+++ /dev/null
@@ -1,11 +0,0 @@
-import hott.path
-open path
-
-definition concat_pV_p {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) : (p ⬝ q⁻¹) ⬝ q ≈ p :=
-begin
-  generalize p,
-  apply (path.rec_on q),
-  intro p,
-  apply (path.rec_on p),
-  apply idp
-end
diff --git a/tests/lean/slow/path_ind.lean b/tests/lean/slow/path_ind.lean
deleted file mode 100644
index 760fdf775..000000000
--- a/tests/lean/slow/path_ind.lean
+++ /dev/null
@@ -1,31 +0,0 @@
-import hott
-
-open path
-set_option pp.beta true
-
-variables {A : Type} {B : A → Type} {C : Π a : A, B a → Type} {D : Π (a : A) (b : B a), C a b → Type}
-
-structure foo :=
-mk :: (a : A) (b : B a) (c : C a b)
-
-set_option unifier.max_steps 50000
-
-definition foo.eq {a₁ a₂ : A} {b₁ : B a₁} {b₂ : B a₂} {c₁ : C a₁ b₁} {c₂ : C a₂ b₂}
-                  (H₁ : a₁ ≈ a₂)
-                  (H₂ : path.rec_on H₁ b₁ ≈ b₂)
-                  (H₃ : path.rec_on H₂ (path.rec_on H₁ c₁) ≈ c₂)
-                  : foo.mk a₁ b₁ c₁ ≈ foo.mk a₂ b₂ c₂ :=
-have aux₁: Π (b₂ : B a₁) (c₂ : C a₁ b₂)
-             (H₂ : path.rec_on idp b₁ ≈ b₂)
-             (H₃ : path.rec_on H₂ (path.rec_on idp c₁) ≈ c₂),
-             foo.mk a₁ b₁ c₁ ≈ foo.mk a₁ b₂ c₂, from
-  λ (b₂ : B a₁) (c₂ : C a₁ b₂)
-    (H₂ : b₁ ≈ b₂) (H₃ : path.rec_on H₂ c₁ ≈ c₂),
-    have aux₂ : Π (c₂ : C a₁ b₁) (H₃ : path.rec_on idp c₁ ≈ c₂),
-               foo.mk a₁ b₁ c₁ ≈ foo.mk a₁ b₁ c₂, from
-      λ (c₂ : C a₁ b₁) (H₃ : c₁ ≈ c₂),
-        have aux₃ : foo.mk a₁ b₁ c₁ ≈ foo.mk a₁ b₁ c₁, from
-          idp,
-        path.rec_on H₃ aux₃,
-    path.rec_on H₂ aux₂ c₂ H₃,
-path.rec_on H₁ aux₁ b₂ c₂ H₂ H₃