From 73dec1be45bdf9dc43b4e7df1630113e5838a939 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 14 Nov 2020 18:04:22 -0800
Subject: [PATCH] test: add tests for Lean3 bugs

---
 tests/lean/run/102_lean3.lean | 12 +++++++++++
 tests/lean/run/436_lean3.lean | 39 +++++++++++++++++++++++++++++++++++
 tests/lean/run/447_lean3.lean | 11 ++++++++++
 tests/lean/run/470_lean3.lean |  7 +++++++
 tests/lean/run/474_lean3.lean | 13 ++++++++++++
 tests/lean/run/492_lean3.lean | 26 +++++++++++++++++++++++
 tests/lean/run/500_lean3.lean |  4 ++++
 tests/lean/run/52_lean3.lean  | 19 +++++++++++++++++
 tests/lean/run/91_lean3.lean  | 12 +++++++++++
 9 files changed, 143 insertions(+)
 create mode 100644 tests/lean/run/102_lean3.lean
 create mode 100644 tests/lean/run/436_lean3.lean
 create mode 100644 tests/lean/run/447_lean3.lean
 create mode 100644 tests/lean/run/470_lean3.lean
 create mode 100644 tests/lean/run/474_lean3.lean
 create mode 100644 tests/lean/run/492_lean3.lean
 create mode 100644 tests/lean/run/500_lean3.lean
 create mode 100644 tests/lean/run/52_lean3.lean
 create mode 100644 tests/lean/run/91_lean3.lean

diff --git a/tests/lean/run/102_lean3.lean b/tests/lean/run/102_lean3.lean
new file mode 100644
index 0000000000..30890244b3
--- /dev/null
+++ b/tests/lean/run/102_lean3.lean
@@ -0,0 +1,12 @@
+inductive time (D : Type) : Type
+| start : time D
+| after : (D → time D) → time D
+
+def foo (C D : Type) : time D → (γ : Type) × γ → C
+| time.start    => ⟨C, id⟩
+| time.after ts => ⟨(∀ (i : D), (foo C D $ ts i).1) × D, λ p => (foo C D $ ts p.2).2 $ p.1 p.2⟩
+
+theorem fooEq1 (C D) : foo C D time.start = ⟨C, id⟩ :=
+  rfl
+theorem fooEq2 (C D) (ts : D → time D): foo C D (time.after ts) = ⟨(∀ (i : D), (foo C D $ ts i).1) × D, λ p => (foo C D $ ts p.2).2 $ p.1 p.2⟩ :=
+  rfl
diff --git a/tests/lean/run/436_lean3.lean b/tests/lean/run/436_lean3.lean
new file mode 100644
index 0000000000..48036257ce
--- /dev/null
+++ b/tests/lean/run/436_lean3.lean
@@ -0,0 +1,39 @@
+inductive bvar : Type
+  | mk (n : Nat)
+
+def bvar_eq : bvar → bvar → Bool
+  | bvar.mk n1, bvar.mk n2 => n1=n2
+
+inductive bExpr : Type
+  | BLit (b: Bool)
+  | BVar (v: bvar)
+
+def benv := bvar → Bool
+
+def bEval : bExpr → benv → Bool
+  | bExpr.BLit b, i => b
+  | bExpr.BVar v, i => i v
+
+def init_benv : benv := λ v => false
+
+def update_benv : benv → bvar → Bool → benv
+  | i, v, b => λ v2 => if (bvar_eq v v2) then b else (i v2)
+
+inductive bCmd : Type
+  | bAssm (v : bvar) (e : bExpr)
+  | bSeq (c1 c2 : bCmd)
+
+-- Unlike Lean 3, we can have nested match-expressions and still use structural recursion
+def cEval : benv → bCmd → benv
+| i0, c => match c with
+  | bCmd.bAssm v e  => update_benv i0 v (bEval e i0)
+  | bCmd.bSeq c1 c2 =>
+    let i1 := cEval i0 c1
+    cEval i1 c2
+
+def myFirstProg := bCmd.bAssm (bvar.mk 0) (bExpr.BLit false)
+
+def newEnv :=
+  cEval init_benv myFirstProg
+
+#eval newEnv (bvar.mk 0)
diff --git a/tests/lean/run/447_lean3.lean b/tests/lean/run/447_lean3.lean
new file mode 100644
index 0000000000..733d0bf489
--- /dev/null
+++ b/tests/lean/run/447_lean3.lean
@@ -0,0 +1,11 @@
+inductive S
+| mk : (_foo : Nat → Int) → S
+
+namespace S
+
+def bar (s : S) : Nat := 0
+
+variable (s : S)
+#check s.bar
+
+end S
diff --git a/tests/lean/run/470_lean3.lean b/tests/lean/run/470_lean3.lean
new file mode 100644
index 0000000000..aa6269dea8
--- /dev/null
+++ b/tests/lean/run/470_lean3.lean
@@ -0,0 +1,7 @@
+section foo
+
+axiom foo : Type
+
+constant bla : Nat
+
+end foo
diff --git a/tests/lean/run/474_lean3.lean b/tests/lean/run/474_lean3.lean
new file mode 100644
index 0000000000..faca80b6c0
--- /dev/null
+++ b/tests/lean/run/474_lean3.lean
@@ -0,0 +1,13 @@
+def my_eq {A : Type _} (a b : A) : Prop := true
+
+theorem id_map_is_right_neutral₁ {A : Type} (map : A -> A) :
+  my_eq (Function.comp.{1, 1, _} map map) map :=
+sorry
+
+theorem id_map_is_right_neutral₂ {A : Type} (map : A -> A) :
+  my_eq (Function.comp map map) map :=
+sorry
+
+theorem id_map_is_right_neutral₃ {A : Type} (map : A -> A) :
+  my_eq (map ∘ map) map :=
+sorry
diff --git a/tests/lean/run/492_lean3.lean b/tests/lean/run/492_lean3.lean
new file mode 100644
index 0000000000..16ad540872
--- /dev/null
+++ b/tests/lean/run/492_lean3.lean
@@ -0,0 +1,26 @@
+class foo (α : Type) : Type := (f : α)
+def foo.f' {α : Type} [c : foo α] : α := foo.f
+
+#print foo.f  -- def foo.f : {α : Type} → [self : foo α] → α
+#print foo.f' -- def foo.f' : {α : Type} → [c : foo α] → α
+
+variables {α : Type} [c : foo α]
+#check c.f  -- ok
+#check c.f' -- ok
+
+structure bar : Prop := (f : ∀ {m : Nat}, m = 0)
+def bar.f' : bar → ∀ {m : Nat}, m = 0 := bar.f
+
+#print bar.f  -- def bar.f  : bar → ∀ {m : ℕ}, m = 0
+#print bar.f' -- def bar.f' : bar → ∀ {m : ℕ}, m = 0
+
+variables (h : bar) (m : Nat)
+
+#check (h.f : ∀ {m : Nat}, m = 0) -- ok
+#check (h.f : m = 0)  -- ok
+#check h.f (m := m)   -- ok
+#check h.f (m := 0)   -- ok
+#check (h.f' : m = 0) -- ok
+
+theorem ex1 (n) : (h.f : n = 0) = h.f (m := n) :=
+  rfl
diff --git a/tests/lean/run/500_lean3.lean b/tests/lean/run/500_lean3.lean
new file mode 100644
index 0000000000..c0d63b5499
--- /dev/null
+++ b/tests/lean/run/500_lean3.lean
@@ -0,0 +1,4 @@
+example (foo bar : Option Nat) : False := by
+  have do { let x ← bar; foo } = bar >>= fun x => foo := rfl
+  admit
+  done
diff --git a/tests/lean/run/52_lean3.lean b/tests/lean/run/52_lean3.lean
new file mode 100644
index 0000000000..a2af776a3d
--- /dev/null
+++ b/tests/lean/run/52_lean3.lean
@@ -0,0 +1,19 @@
+universe u
+
+macro "Type*" : term => `(Type _)
+
+open Nat
+
+variable {α : Type u}
+
+def vec : Type u → Nat → Type*
+| A, 0      => PUnit
+| A, succ k => A × vec A k
+
+inductive dfin : Nat → Type
+  | fz {n} : dfin (succ n)
+  | fs {n} : dfin n → dfin (succ n)
+
+def kth_projn : (n : Nat) → vec α n → dfin n → α
+  | succ n, x,        dfin.fz   => x.fst
+  | succ n, (x, xs),  dfin.fs k => kth_projn n xs k
diff --git a/tests/lean/run/91_lean3.lean b/tests/lean/run/91_lean3.lean
new file mode 100644
index 0000000000..a27866d556
--- /dev/null
+++ b/tests/lean/run/91_lean3.lean
@@ -0,0 +1,12 @@
+def top := ∀ p : Prop, p → p
+def pext := ∀ (A B : Prop), A → B → A = B
+def supercast (h : pext) (A B : Prop) (a : A) (b : B) : B
+  := @cast A B (h A B a b) a
+def omega : pext → top :=
+  λ h A a => supercast h (top → top) A
+    (λ z: top => z (top → top) (λ x => x) z) a
+def Omega : pext → top :=
+  λ h => omega h (top → top) (λ x => x) (omega h)
+def Omega' : pext → top := λ h => (λ p x => x)
+
+theorem loopy : Omega = Omega' := rfl -- loops