test(frontends/lean): all 'bad' examples can be solved

Move them to the main test directory

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

tests/lean/bad/t1.lean

@@ -1,24 +0,0 @@
-Variable g : Pi A : Type, A -> A.
-Variables a b : Int
-(*
-The following example demonstrates a limitation in the current elaborator.
-The current elaborator decides overloads before filling holes.
-The symbol '>' is overloaded. The possible overloads are:
-    Nat::lt   Nat -> Nat -> Nat
-    Int::lt   Int -> Int -> Int
-    Real::lt  Real -> Real -> Real
-The type of (g _ a) is not available when the overload is decided, and
-0 has type Nat. Then, the overload resolver selects
-    Nat::lt   Nat -> Nat -> Nat
-Now, when we fill the holes, (g _ a) is elaborated to (g Int a) which
-has type Int, and we fail.
-If the hole elaborator and overload resolver are executed simultaneously,
-we would get the fully elaborated term:
-
-    Int::le (g Int a) (nat_to_int 0)
-*)
-Axiom H1 : g _ a > 0
-(*
-One workaround consists in manually providing the coercion.
-*)
-Axiom H1 : g _ a > (nat_to_int 0)

tests/lean/bad/t4.lean

@@ -1,16 +0,0 @@
-Variable f {A : Type} (a : A) : A
-Variable a : Int
-Definition tst : Bool := (fun x, (f x) > 10) a
-(*
-The definition above should create the following problem for the new elaborator engine:
-
-Definition tst : Int := (fun x : _, ((choice Nat::lt Int::lt Real::lt) (f _ x) ((choice id nat_to_int real_to_int) 10))) a
-
-The first choice is generated because > is an overloaded notation.
-
-The second choice is generated because we have coercions from nat->int
-and nat->real, and it is unclear which one we need until we select the overload.
-*)
-
-(* Workaround: again add coercion manually *)
-Definition tst : Bool := (fun x, (f x) > (nat_to_int 10)) a

tests/lean/bad/t5.lean

@@ -1,27 +0,0 @@
-Variable g {A : Type} (a : A) : A
-Variable a : Int
-Variable b : Int
-Axiom H1 : a = b
-(*
-The following axiom fails to be elaborated because:
-1- (g a) is actually (g _ a)
-2- > is overloaded notation for Nat::gt, Int::gt and Real::gt
-3- The current elaborator selects one of the overloads before
-   the hole in (g _ a) is solved. Thus, it selects Nat::gt.
-4- During elaboration, we transform (g _ a) into (g Int a),
-   and a type error is detected.
-
-The next elaborator should address this problem.
-*)
-Axiom H2 : (g a) > 0
-
-(*
-A possible workaround is to manually add the coercion in 0.
-The coercion is called nat_to_int. We define the notation
-_ i to make it easier to write
-*)
-Notation 100 _ i : nat_to_int
-Axiom H2 : (g a) > 0i
-
-Theorem T1 : (g b) > 0i := Subst (λ x, (g x) > 0i) H2 H1
-Show Environment 2

tests/lean/bad/t6.lean

@@ -1,23 +0,0 @@
-Variable f {A : Type} (a : A) : A
-Variable a : Int
-Variable b : Real
-Definition tst : Bool := (fun x y, (f x) > (f y)) a b
-(*
-In the current version, the example above does not work without user's help.
-We can compile this example into the following elaborator problem:
-
-Definition tst : Bool := (fun (x : _) (y : _),
-                           ((choice Nat::lt Int::lt Real::lt)
-                            ((choice id nat_to_int nat_to_real int_to_real) (f _ x))
-                            ((choice id nat_to_int nat_to_real int_to_real) (f _ y))))
-                         a b
-
-The first choice construct is generated because > is overloaded notation.
-
-The second and third choices are selected because Nat::lt, Int::lt and
-Real::lt expect Nat, Int and Real arguments respectively.
-The type of the expressions (f _ x) and (f _ y) is unknown at problem generation time.
-So, we create a choice with all relevant coercions. The choice `id` represents "no coercion" is
-needed.
-*)
-Definition tst : Bool := (fun x y, (int_to_real (f x)) > (f y)) a b

tests/lean/bad/t7.lean

@@ -1,27 +0,0 @@
-Variable f {A : Type} (a b : A) : Bool
-Variable a : Int
-Variable b : Real
-Definition tst : Bool := (fun x y, f x y) a b
-(*
-The example above demonstrates that may not be easy to eagerly create
-choice constructs that cover all needed coercions.
-
-The variables `a` and `b` have type Int and Real respectively.
-Since the type of the function is not known at compilation time, we
-add choice constructs that accomodate possible coercions.
-So, we get the problem:
-
-Definition tst : Bool := (fun (x : _) (y : _), f _ x y)
-                         ((choice id int_to_real a))
-                         b
-*)
-Definition tst1 : Bool := (fun x y, f x y) (int_to_real a) b
-Set pp::coercion true
-Set pp::implicit true
-Show Environment 1
-(*
-It is unclear how to implement a simple elaboration problem generator that will produce
-a problem that has the following solution.
-*)
-Definition tst2 : Bool := (fun x y, f (int_to_real x) y) a b
-Show Environment 1

tests/lean/bad1.lean

@@ -0,0 +1,3 @@
+Variable g : Pi A : Type, A -> A.
+Variables a b : Int
+Axiom H1 : g _ a > 0

tests/lean/bad1.lean.expected.out

@@ -0,0 +1,6 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Assumed: g
+  Assumed: a
+  Assumed: b
+  Assumed: H1

tests/lean/bad2.lean.expected.out

@@ -0,0 +1,15 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Assumed: list
+  Assumed: nil
+  Assumed: cons
+  Defined: n1
+  Defined: n2
+  Defined: n3
+  Defined: n3a
+  Defined: n3b
+  Defined: n4
+  Defined: n5
+  Set: lean::pp::coercion
+  Set: lean::pp::implicit
+Definition n5 : list ℕ := cons::explicit ℕ 10 (nil::explicit ℕ)

tests/lean/bad3.lean

@@ -3,10 +3,6 @@ Variable nil  {A : Type} : list A
 Variable cons {A : Type} (head : A) (tail : list A) : list A
 Variables a b : Int
 Variables n m : Nat
-(*
-Here are other examples showing that coercions and implicit arguments
-do not "interact well with each other" in the current implementation.
-*)
 Definition l1 : list Int := cons a (cons b (cons n nil))
 Definition l2 : list Int := cons a (cons n (cons b nil))
 Check cons a (cons b (cons n nil))

tests/lean/bad3.lean.expected.out

@@ -0,0 +1,12 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Assumed: list
+  Assumed: nil
+  Assumed: cons
+  Assumed: a
+  Assumed: b
+  Assumed: n
+  Assumed: m
+  Defined: l1
+  Defined: l2
+cons a (cons b (cons n nil)) : list ℤ

tests/lean/bad4.lean

@@ -0,0 +1,3 @@
+Variable f {A : Type} (a : A) : A
+Variable a : Int
+Definition tst : Bool := (fun x, (f x) > 10) a

tests/lean/bad4.lean.expected.out

@@ -0,0 +1,5 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Assumed: f
+  Assumed: a
+  Defined: tst

tests/lean/bad5.lean

@@ -0,0 +1,7 @@
+Variable g {A : Type} (a : A) : A
+Variable a : Int
+Variable b : Int
+Axiom H1 : a = b
+Axiom H2 : (g a) > 0
+Theorem T1 : (g b) > 0 := Subst (λ x, (g x) > 0) H2 H1
+Show Environment 2

tests/lean/bad5.lean.expected.out

@@ -0,0 +1,10 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Assumed: g
+  Assumed: a
+  Assumed: b
+  Assumed: H1
+  Assumed: H2
+  Proved: T1
+Axiom H2 : (g a) > 0
+Theorem T1 : (g b) > 0 := Subst (λ x : ℤ, (g x) > 0) H2 H1

tests/lean/bad6.lean

@@ -0,0 +1,4 @@
+Variable f {A : Type} (a : A) : A
+Variable a : Int
+Variable b : Real
+Definition tst : Bool := (fun x y, (f x) > (f y)) a b

tests/lean/bad6.lean.expected.out

@@ -0,0 +1,6 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Assumed: f
+  Assumed: a
+  Assumed: b
+  Defined: tst

tests/lean/bad7.lean

@@ -0,0 +1,5 @@
+Variable f {A : Type} (a b : A) : Bool
+Variable a : Int
+Variable b : Real
+Definition tst : Bool := (fun x y, f x y) a b
+Show Environment 1

tests/lean/bad7.lean.expected.out

@@ -0,0 +1,7 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Assumed: f
+  Assumed: a
+  Assumed: b
+  Defined: tst
+Definition tst : Bool := (λ x y : ℝ, f x y) a b