Move files in examples directory to tests directory. They are not real examples

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

examples/ex10.lean

@@ -1,24 +0,0 @@
-(* Define a "fake" type to simulate the natural numbers. This is just a test. *)
-Variable Natural : Type
-Variable lt : Natural -> Natural -> Bool
-Variable zero : Natural
-Variable one : Natural
-Variable two : Natural
-Variable three : Natural
-Infix 50 < : lt
-Axiom two_lt_three : two < three
-Definition vector (A : Type) (n : Natural) : Type := Pi (i : Natural) (H : i < n), A
-Definition const (A : Type) (n : Natural) (d : A) : vector A n := fun (i : Natural) (H : i < n), d
-Definition update (A : Type) (n : Natural) (v : vector A n) (i : Natural) (d : A) : vector A n := fun (j : Natural) (H : j < n), if A (j = i) d (v j H)
-Definition select (A : Type) (n : Natural) (v : vector A n) (i : Natural) (H : i < n) : A := v i H
-Definition map (A B C : Type) (n : Natural) (f : A -> B -> C) (v1 : vector A n) (v2 : vector B n) : vector C n := fun (i : Natural) (H : i < n), f (v1 i H) (v2 i H)
-Show Environment
-Check select Bool three (update Bool three (const Bool three false) two true) two two_lt_three
-Eval select Bool three (update Bool three (const Bool three false) two true) two two_lt_three
-Check select
-Echo "\nmap type ---> "
-Check map
-Echo "\nmap normal form --> "
-Eval map
-Echo "\nupdate normal form --> "
-Eval update

examples/ex2.lean

@@ -1,6 +0,0 @@
-Check fun x : Bool, x
-Show fun x y : Bool, x
-Show fun (A : Type) (x y : A), x = y
-Check fun (A : Type) (x y : A), x = y
-Check Pi (A B : Type), Type
-Show Pi (A B : Type), A = B

src/kernel/arith/arith.cpp

@@ -19,8 +19,8 @@ public:
     virtual expr get_type() const { return Type(); }
     virtual bool normalize(unsigned num_args, expr const * args, expr & r) const { return false; }
     virtual bool operator==(value const & other) const { return other.kind() == kind(); }
-    virtual void display(std::ostream & out) const { out << "int"; }
-    virtual format pp() const { return format("int"); }
+    virtual void display(std::ostream & out) const { out << "Int"; }
+    virtual format pp() const { return format("Int"); }
     virtual unsigned hash() const { return 41; }
 };
 

src/shell/CMakeLists.txt

@@ -2,23 +2,6 @@ configure_file("${LEAN_SOURCE_DIR}/shell/version.h.in" "${LEAN_BINARY_DIR}/versi
 include_directories("${LEAN_BINARY_DIR}")
 add_executable(lean lean.cpp)
 target_link_libraries(lean ${EXTRA_LIBS})
-add_test(lean1 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/ex1.lean")
-add_test(lean2 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/ex2.lean")
-add_test(lean3 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/ex3.lean")
-add_test(lean4 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/ex4.lean")
-add_test(lean5 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/ex5.lean")
-add_test(lean6 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/ex6.lean")
-add_test(lean7 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/ex7.lean")
-add_test(lean8 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/ex8.lean")
-add_test(lean9 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/ex9.lean")
-add_test(lean10 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/ex10.lean")
-add_test(lean11 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/ex11.lean")
-add_test(lean12 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/ex12.lean")
-add_test(lean13 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/ex13.lean")
-add_test(lean14 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/ex14.lean")
-add_test(lean15 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/ex15.lean")
-add_test(lean16 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/ex16.lean")
-add_test(lean17 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/ex17.lean")
 add_test(NAME leantests
          WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean"
          COMMAND "./test.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean")

tests/lean/tst1.lean

@@ -0,0 +1,26 @@
+(* Define a "fake" type to simulate the natural numbers. This is just a test. *)
+Variable N : Type
+Variable lt : N -> N -> Bool
+Variable zero : N
+Variable one : N
+Variable two : N
+Variable three : N
+Infix 50 < : lt
+Axiom two_lt_three : two < three
+Definition vector (A : Type) (n : N) : Type := Pi (i : N) (H : i < n), A
+Definition const {A : Type} (n : N) (d : A) : vector A n := fun (i : N) (H : i < n), d
+Definition update {A : Type} {n : N} (v : vector A n) (i : N) (d : A) : vector A n := fun (j : N) (H : j < n), if A (j = i) d (v j H)
+Definition select {A : Type} {n : N} (v : vector A n) (i : N) (H : i < n) : A := v i H
+Definition map {A B C : Type} {n : N} (f : A -> B -> C) (v1 : vector A n) (v2 : vector B n) : vector C n := fun (i : N) (H : i < n), f (v1 i H) (v2 i H)
+Show Environment 10
+Check select (update (const three false) two true) two two_lt_three
+Eval select (update (const three false) two true) two two_lt_three
+Check update (const three false) two true
+Echo "\n--------"
+Check select::explicit
+Echo "\nmap type ---> "
+Check map::explicit
+Echo "\nmap normal form --> "
+Eval map::explicit
+Echo "\nupdate normal form --> "
+Eval update::explicit

tests/lean/tst1.lean.expected.out

@@ -0,0 +1,47 @@
+  Assumed: N
+  Assumed: lt
+  Assumed: zero
+  Assumed: one
+  Assumed: two
+  Assumed: three
+  Assumed: two_lt_three
+  Defined: vector
+  Defined: const
+  Defined: update
+  Defined: select
+  Defined: map
+Axiom two_lt_three : two < three
+Definition vector (A : Type) (n : N) : Type := Π (i : N) (H : i < n), A
+Definition const {A : Type} (n : N) (d : A) : vector A n := λ (i : N) (H : i < n), d
+Definition const::explicit (A : Type) (n : N) (d : A) : vector A n := const n d
+Definition update {A : Type} {n : N} (v : vector A n) (i : N) (d : A) : vector A n :=
+    λ (j : N) (H : j < n), if A (j = i) d (v j H)
+Definition update::explicit (A : Type) (n : N) (v : vector A n) (i : N) (d : A) : vector A n := update v i d
+Definition select {A : Type} {n : N} (v : vector A n) (i : N) (H : i < n) : A := v i H
+Definition select::explicit (A : Type) (n : N) (v : vector A n) (i : N) (H : i < n) : A := select v i H
+Definition map {A B C : Type} {n : N} (f : A → B → C) (v1 : vector A n) (v2 : vector B n) : vector C n :=
+    λ (i : N) (H : i < n), f (v1 i H) (v2 i H)
+Definition map::explicit (A B C : Type) (n : N) (f : A → B → C) (v1 : vector A n) (v2 : vector B n) : vector C n :=
+    map f v1 v2
+Bool
+⊤
+vector Bool three
+
+--------
+Π (A : Type) (n : N) (v : vector A n) (i : N) (H : i < n), A
+
+map type ---> 
+Π (A B C : Type) (n : N) (f : A → B → C) (v1 : vector A n) (v2 : vector B n), vector C n
+
+map normal form --> 
+λ (A B C : Type)
+  (n : N)
+  (f : A → B → C)
+  (v1 : Π (i : N) (H : i < n), A)
+  (v2 : Π (i : N) (H : i < n), B)
+  (i : N)
+  (H : i < n),
+  f (v1 i H) (v2 i H)
+
+update normal form --> 
+λ (A : Type) (n : N) (v : Π (i : N) (H : i < n), A) (i : N) (d : A) (j : N) (H : j < n), ite A (j = i) d (v j H)

tests/lean/tst10.lean.expected.out

@@ -0,0 +1,22 @@
+  Assumed: a
+  Assumed: b
+a ∧ b
+a ∧ b ∧ a
+a ∧ b
+a ∧ b
+a ∧ b
+a ∧ b
+a ∨ b
+a ∨ b
+a ∨ b
+a ∨ b
+a ∨ a ∨ b
+a ⇒ b ⇒ a
+Bool
+ite Bool a a ⊤
+a
+  Assumed: H1
+  Assumed: H2
+Π (a b : Bool) (H1 : a ⇒ b) (H2 : a), b
+MP H2 H1
+b

tests/lean/tst11.lean.expected.out

@@ -0,0 +1,10 @@
+  Defined: xor
+⊤ ⊕ ⊥
+⊥
+⊤
+  Assumed: a
+a ⊕ a ⊕ a
+Π (A : Type u) (a b : A) (P : A → Bool) (H1 : P a) (H2 : a = b), P b
+  Proved: EM2
+Π a : Bool, a ∨ ¬ a
+a ∨ ¬ a

tests/lean/tst12.lean.expected.out

@@ -0,0 +1,7 @@
+λ x y : Bool, x ∧ y
+let x := ⊤,
+    y := ⊤,
+    z := x ∧ y,
+    f := λ arg1 arg2 : Bool, arg1 ∧ arg2 ⇔ arg2 ∧ arg1 ⇔ arg1 ∨ arg2 ∨ arg2
+in (f x y) ∨ z
+⊤

tests/lean/tst13.lean.expected.out

@@ -0,0 +1,2 @@
+λ x x : Bool, x
+let x := ⊤, y := ⊤, z := x ∧ y, f := λ x y : Bool, x ∧ y ⇔ y ∧ x ⇔ x ∨ y ∨ y in (f x y) ∨ z

tests/lean/tst14.lean.expected.out

@@ -0,0 +1,5 @@
+Int → Int → Int
+  Assumed: f
+f 0
+Int → Int
+Int

tests/lean/tst15.lean.expected.out

@@ -0,0 +1,20 @@
+  Assumed: x
+Type u+3 ⊔ m+2 ⊔ 3
+  Assumed: f
+Type u+10 → Type
+Type
+Type 5
+Type u+3 ⊔ m+2 ⊔ 3
+Type u+1 ⊔ m+1
+Type u+3
+Type u+4
+Type u+1 ⊔ m+1
+Type u+1 ⊔ m+1 ⊔ 4
+Type u+1 ⊔ m ⊔ 3
+Type u+2 ⊔ m+1 ⊔ 4
+Type u → Type 5
+Type u+1 ⊔ 6
+Type m+1 ⊔ 4 ⊔ u+6
+Type m ⊔ 3 → Type u → Type 5
+Type m+1 ⊔ 6 ⊔ u+1
+Type u

tests/lean/tst16.lean.expected.out

@@ -0,0 +1,15 @@
+  Assumed: f
+∀ a b : Type, (f a) = (f b)
+  Assumed: g
+∀ (a b : Type) (c : Bool), g c ((f a) = (f b))
+∃ (a b : Type) (c : Bool), g c ((f a) = (f b))
+∀ (a b : Type) (c : Bool), (g c (f a)) = (f b) ⇒ (f a)
+Bool
+∀ (a b : Type) (c : Bool), g c ((f a) = (f b))
+∀ a b : Type, (f a) = (f b)
+∃ a b : Type, (f a) = (f b) ∧ (f a)
+∃ a b : Type, (f a) = (f b) ∨ (f b)
+  Assumed: a
+(f a) ∨ (f a)
+(f a) = a ∨ (f a)
+(f a) = a ∧ (f a)

tests/lean/tst17.lean.expected.out

@@ -0,0 +1,8 @@
+  Assumed: f
+  Assumed: g
+∀ a b : Type, ∃ c : Type, (g a b) = (f c)
+Bool
+(λ a : Type,
+   (λ b : Type, ite Bool ((λ x : Type, ite Bool ((g a b) = (f x)) ⊥ ⊤) = (λ x : Type, ⊤)) ⊥ ⊤) =
+   (λ x : Type, ⊤)) =
+(λ x : Type, ⊤)

tests/lean/tst2.lean

@@ -5,8 +5,7 @@ Show a/\b
 Set lean::pp::notation false
 Show Options
 Show a/\b
-Show Environment 5
+Show Environment 2
 Set lean::pp::notation true
 Show Options
 Show a/\b
-

tests/lean/tst2.lean.expected.out

@@ -0,0 +1,12 @@
+⟨⟩
+  Assumed: a
+  Assumed: b
+a ∧ b
+  Set option: lean::pp::notation
+⟨lean::pp::notation ↦ false⟩
+and a b
+Variable a : Bool
+Variable b : Bool
+  Set option: lean::pp::notation
+⟨lean::pp::notation ↦ true⟩
+a ∧ b

tests/lean/tst3.lean

@@ -1,5 +1,3 @@
-
-
 Set lean::parser::verbose false.
 Notation 10 if _ then _ : implies.
 Show Environment 1.

tests/lean/tst3.lean.expected.out

@@ -0,0 +1,25 @@
+Notation 10 if _ then _ : implies
+if ⊤ then ⊥
+if ⊤ then (if a then ⊥)
+implies true (implies a false)
+Notation 100 _ |- _ ; _ : f
+f c d e
+c |- d ; e
+(a !) !
+fact (fact a)
+[ c ; d ]
+[ c ; ([ d ; e ]) ]
+g c (g d e)
+Notation 40 _ << _ end : h
+d << e end
+[ c ; d << e end ]
+g c (h d e)
+c ** d ++ e ** c
+p1 ∨ p2 ∧ p3
+r (s c d) (s e c)
+or p1 (and p2 p3)
+c = d ∨ d = c
+¬ p1 ∨ p2
+p1 ∧ p3 ∨ p2 ∧ p3
+or (not p1) p2
+or (and p1 p3) (and p2 p3)

tests/lean/tst4.lean

@@ -1,4 +1,3 @@
-
 Variable f {A : Type} (a b : A) : A
 Variable N : Type
 Variable n1 : N
@@ -20,5 +19,3 @@ Axiom H1 : a = b && b = c
 Theorem Pr : (g a) = (g c) :=
     Congr (Refl g) (Trans (Conjunct1 H1) (Conjunct2 H1))
 Show Environment 2
-
-

tests/lean/tst4.lean.expected.out

@@ -0,0 +1,28 @@
+  Assumed: f
+  Assumed: N
+  Assumed: n1
+  Assumed: n2
+  Set option: lean::pp::implicit
+f::explicit N n1 n2
+f::explicit ((N → N) → N → N) (λ x : N → N, x) (λ y : N → N, y)
+  Assumed: EqNice
+EqNice::explicit N n1 n2
+N
+Π (A : Type u) (B : A → Type u) (f g : Π x : A, B x) (a b : A) (H1 : f = g) (H2 : a = b), (f a) = (g b)
+f::explicit N n1 n2
+  Assumed: a
+  Assumed: b
+  Assumed: c
+  Assumed: g
+  Assumed: H1
+  Proved: Pr
+Axiom H1 : a = b ∧ b = c
+Theorem Pr : (g a) = (g c) :=
+    let κ::1 := Trans::explicit
+                     N
+                     a
+                     b
+                     c
+                     (Conjunct1::explicit (a = b) (b = c) H1)
+                     (Conjunct2::explicit (a = b) (b = c) H1)
+    in Congr::explicit N (λ x : N, N) g g a c (Refl::explicit (N → N) g) κ::1

tests/lean/tst5.lean.expected.out

@@ -0,0 +1,9 @@
+  Assumed: N
+  Assumed: a
+  Assumed: b
+a ≃ b
+Bool
+  Set option: lean::pp::implicit
+heq::explicit N a b
+heq::explicit Type 2 Type 1 Type 1
+heq::explicit Bool ⊤ ⊥

tests/lean/tst6.lean.expected.out

@@ -0,0 +1,106 @@
+  Assumed: N
+  Assumed: h
+  Proved: CongrH
+  Set option: lean::pp::implicit
+Theorem CongrH {a1 a2 b1 b2 : N} (H1 : a1 = b1) (H2 : a2 = b2) : (h a1 a2) = (h b1 b2) :=
+    Congr::explicit
+        N
+        (λ x : N, N)
+        (h a1)
+        (h b1)
+        a2
+        b2
+        (Congr::explicit N (λ x : N, N → N) h h a1 b1 (Refl::explicit (N → N → N) h) H1)
+        H2
+Theorem CongrH::explicit (a1 a2 b1 b2 : N) (H1 : a1 = b1) (H2 : a2 = b2) : (h a1 a2) = (h b1 b2) :=
+    CongrH::explicit a1 a2 b1 b2 H1 H2
+  Set option: lean::pp::implicit
+Theorem CongrH {a1 a2 b1 b2 : N} (H1 : a1 = b1) (H2 : a2 = b2) : (h a1 a2) = (h b1 b2) := Congr (Congr (Refl h) H1) H2
+Theorem CongrH::explicit (a1 a2 b1 b2 : N) (H1 : a1 = b1) (H2 : a2 = b2) : (h a1 a2) = (h b1 b2) := CongrH H1 H2
+  Proved: Example1
+  Set option: lean::pp::implicit
+Theorem Example1 (a b c d : N) (H : a = b ∧ b = c ∨ a = d ∧ d = c) : (h a b) = (h c b) :=
+    DisjCases::explicit
+        (a = b ∧ b = c)
+        (a = d ∧ d = c)
+        ((h a b) = (h c b))
+        H
+        (λ H1 : a = b ∧ b = c,
+           CongrH::explicit
+               a
+               b
+               c
+               b
+               (Trans::explicit
+                    N
+                    a
+                    b
+                    c
+                    (Conjunct1::explicit (a = b) (b = c) H1)
+                    (Conjunct2::explicit (a = b) (b = c) H1))
+               (Refl::explicit N b))
+        (λ H1 : a = d ∧ d = c,
+           CongrH::explicit
+               a
+               b
+               c
+               b
+               (Trans::explicit
+                    N
+                    a
+                    d
+                    c
+                    (Conjunct1::explicit (a = d) (d = c) H1)
+                    (Conjunct2::explicit (a = d) (d = c) H1))
+               (Refl::explicit N b))
+  Proved: Example2
+  Set option: lean::pp::implicit
+Theorem Example2 (a b c d : N) (H : a = b ∧ b = c ∨ a = d ∧ d = c) : (h a b) = (h c b) :=
+    DisjCases::explicit
+        (a = b ∧ b = c)
+        (a = d ∧ d = c)
+        ((h a b) = (h c b))
+        H
+        (λ H1 : a = b ∧ b = c,
+           CongrH::explicit
+               a
+               b
+               c
+               b
+               (Trans::explicit
+                    N
+                    a
+                    b
+                    c
+                    (Conjunct1::explicit (a = b) (b = c) H1)
+                    (Conjunct2::explicit (a = b) (b = c) H1))
+               (Refl::explicit N b))
+        (λ H1 : a = d ∧ d = c,
+           CongrH::explicit
+               a
+               b
+               c
+               b
+               (Trans::explicit
+                    N
+                    a
+                    d
+                    c
+                    (Conjunct1::explicit (a = d) (d = c) H1)
+                    (Conjunct2::explicit (a = d) (d = c) H1))
+               (Refl::explicit N b))
+  Proved: Example3
+  Set option: lean::pp::implicit
+Theorem Example3 (a b c d e : N) (H : a = b ∧ b = e ∧ b = c ∨ a = d ∧ d = c) : (h a b) = (h c b) :=
+    DisjCases
+        H
+        (λ H1 : a = b ∧ b = e ∧ b = c, CongrH (Trans (Conjunct1 H1) (Conjunct2 (Conjunct2 H1))) (Refl b))
+        (λ H1 : a = d ∧ d = c, CongrH (Trans (Conjunct1 H1) (Conjunct2 H1)) (Refl b))
+  Proved: Example4
+  Set option: lean::pp::implicit
+Theorem Example4 (a b c d e : N) (H : a = b ∧ b = e ∧ b = c ∨ a = d ∧ d = c) : (h a c) = (h c a) :=
+    DisjCases
+        H
+        (λ H1 : a = b ∧ b = e ∧ b = c,
+           let AeqC := Trans (Conjunct1 H1) (Conjunct2 (Conjunct2 H1)) in CongrH AeqC (Symm AeqC))
+        (λ H1 : a = d ∧ d = c, let AeqC := Trans (Conjunct1 H1) (Conjunct2 H1) in CongrH AeqC (Symm AeqC))

tests/lean/tst7.lean

@@ -1,7 +1,7 @@
 Variable f : Pi (A : Type), A -> Bool
 Show fun (A B : Type) (a : _), f B a
 (* The following one should produce an error *)
-(* Show fun (A : Type) (a : _) (B : Type), f B a *)
+Show fun (A : Type) (a : _) (B : Type), f B a
 
 Variable myeq : Pi (A : Type u), A -> A -> Bool
 Show  myeq _ (fun (A : Type) (a : _), a) (fun (B : Type) (b : B), b)

tests/lean/tst7.lean.expected.out

@@ -0,0 +1,14 @@
+  Assumed: f
+λ (A B : Type) (a : B), f B a
+Error (line: 4, pos: 40) application type mismatch during term elaboration at term
+    f B a
+Elaborator state
+    ?M0 := [unassigned]
+    ?M1 := [unassigned]
+    #0 ≈ lift:0:0 ?M0
+  Assumed: myeq
+myeq (Π (A : Type) (a : A), A) (λ (A : Type) (a : A), a) (λ (B : Type) (b : B), b)
+Bool
+  Assumed: R
+  Assumed: h
+Bool → (Π (f1 g1 : Π A : Type, R A) (G : Π A : Type, myeq (R A) (f1 A) (g1 A)), Bool)

tests/lean/tst8.lean.expected.out

@@ -0,0 +1,3 @@
+Π (A : Type) (a : A), A
+  Assumed: g
+  Defined: f

tests/lean/tst9.lean

@@ -0,0 +1,5 @@
+Variable f : Pi A : Type, A -> A -> A
+Variable N : Type
+Variable g : N -> N -> Bool
+Variable a : N
+Check g true (f _ a a)

tests/lean/tst9.lean.expected.out

@@ -0,0 +1,10 @@
+  Assumed: f
+  Assumed: N
+  Assumed: g
+  Assumed: a
+Error (line: 5, pos: 6) type mismatch at application argument 1 of
+    g ⊤ (f N a a)
+expected type
+    N
+given type
+    Bool