michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

test(lean): remove tests using Lean old syntax and kernel

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-17 10:38:53 -07:00
parent 989bcdc7ad
commit 9f06cd553e
525 changed files with 0 additions and 7728 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
tests/lean/abst.lean
View file

@ -1,6 +0,0 @@
import Int.
axiom PlusComm(a b : Int) : a + b = b + a.
variable a : Int.
check (funext (fun x : Int, (PlusComm a x))).
set_option pp::implicit true.
check (funext (fun x : Int, (PlusComm a x))).

9
tests/lean/abst.lean.expected.out
View file

@ -1,9 +0,0 @@
Set: pp::colors
Set: pp::unicode
Imported 'Int'
Assumed: PlusComm
Assumed: a
funext (λ x : ℤ, PlusComm a x) : (λ x : ℤ, a + x) = (λ x : ℤ, x + a)
Set: lean::pp::implicit
@funext ℤ (λ x : ℤ, ℤ) (λ x : ℤ, a + x) (λ x : ℤ, x + a) (λ x : ℤ, PlusComm a x) :
@eq (∀ x : ℤ, (λ x : ℤ, ℤ) x) (λ x : ℤ, a + x) (λ x : ℤ, x + a)

17
tests/lean/add_assoc.lean
View file

@ -1,17 +0,0 @@
import tactic
using Nat
rewrite_set basic
add_rewrite add_zerol add_succl eq_id : basic
theorem add_assoc (a b c : Nat) : a + (b + c) = (a + b) + c
:= induction_on a
(show 0 + (b + c) = (0 + b) + c, by simp basic)
(λ (n : Nat) (iH : n + (b + c) = (n + b) + c),
show (n + 1) + (b + c) = ((n + 1) + b) + c, by simp basic)
check add_zerol
check add_succl
check @eq_id
print environment 1

17
tests/lean/add_assoc.lean.expected.out
View file

@ -1,17 +0,0 @@
Set: pp::colors
Set: pp::unicode
Imported 'tactic'
Using: Nat
Proved: add_assoc
Nat::add_zerol : ∀ a : ℕ, 0 + a = a
Nat::add_succl : ∀ a b : ℕ, a + 1 + b = a + b + 1
@eq_id : ∀ (A : (Type U)) (a : A), a = a ↔ ⊤
theorem add_assoc (a b c : ℕ) : a + (b + c) = a + b + c :=
Nat::induction_on
a
(eqt_elim (trans (congr (congr2 eq (Nat::add_zerol (b + c))) (congr1 (congr2 Nat::add (Nat::add_zerol b)) c))
(eq_id (b + c))))
(λ (n : ℕ) (iH : n + (b + c) = n + b + c),
eqt_elim (trans (congr (congr2 eq (trans (Nat::add_succl n (b + c)) (congr1 (congr2 Nat::add iH) 1)))
(trans (congr1 (congr2 Nat::add (Nat::add_succl n b)) c) (Nat::add_succl (n + b) c)))
(eq_id (n + b + c + 1))))

3
tests/lean/alias1.lean
View file

@ -1,3 +0,0 @@
alias BB : Bool.
variable x : BB.
print environment 1.

4
tests/lean/alias1.lean.expected.out
View file

@ -1,4 +0,0 @@
Set: pp::colors
Set: pp::unicode
Assumed: x
variable x : BB

16
tests/lean/alias2.lean
View file

@ -1,16 +0,0 @@
scope
variable Natural : Type.
alias ℕℕ : Natural.
variable x : Natural.
print environment 1.
set_option pp::unicode false.
print environment 1.
set_option pp::unicode true.
print environment 1.
alias NN : Natural.
print environment 2.
alias ℕℕℕ : Natural.
print environment 3.
set_option pp::unicode false.
print environment 3.
pop_scope

18
tests/lean/alias2.lean.expected.out
View file

@ -1,18 +0,0 @@
Set: pp::colors
Set: pp::unicode
Assumed: Natural
Assumed: x
variable x : ℕℕ
Set: pp::unicode
variable x : Natural
Set: pp::unicode
variable x : ℕℕ
variable x : NN
alias NN : Natural
variable x : ℕℕℕ
alias NN : Natural
alias ℕℕℕ : Natural
Set: pp::unicode
variable x : NN
alias NN : Natural
alias ℕℕℕ : Natural

2
tests/lean/alias3.lean
View file

@ -1,2 +0,0 @@
alias A : Bool
alias A : Nat

3
tests/lean/alias3.lean.expected.out
View file

@ -1,3 +0,0 @@
Set: pp::colors
Set: pp::unicode
alias3.lean:2:0: error: alias 'A' was already defined

24
tests/lean/apply_tac1.lean
View file

@ -1,24 +0,0 @@
import tactic.
import Int.
variable f : Int -> Int -> Bool
variable P : Int -> Int -> Bool
axiom Ax1 (x y : Int) (H : P x y) : (f x y)
theorem T1 (a : Int) : (P a a) → (f a a).
apply Ax1.
exact.
done.
variable b : Int
axiom Ax2 (x : Int) : (f x b)
(*
simple_tac = Repeat(OrElse(assumption_tac(), apply_tac("Ax2"), apply_tac("Ax1")))
*)
theorem T2 (a : Int) : (P a a) → (f a a).
simple_tac.
done.
theorem T3 (a : Int) : (P a a) → (f a a).
Repeat (OrElse exact (apply Ax2) (apply Ax1)).
done.
print environment 2.

14
tests/lean/apply_tac1.lean.expected.out
View file

@ -1,14 +0,0 @@
Set: pp::colors
Set: pp::unicode
Imported 'tactic'
Imported 'Int'
Assumed: f
Assumed: P
Assumed: Ax1
Proved: T1
Assumed: b
Assumed: Ax2
Proved: T2
Proved: T3
theorem T2 (a : ℤ) (H : P a a) : f a a := Ax1 a a H
theorem T3 (a : ℤ) (H : P a a) : f a a := Ax1 a a H

4
tests/lean/apply_tac2.lean
View file

@ -1,4 +0,0 @@
(* import("tactic.lua") *)
theorem T (a b : Bool) : a → b → b → a.
exact.
done.

3
tests/lean/apply_tac2.lean.expected.out
View file

@ -1,3 +0,0 @@
Set: pp::colors
Set: pp::unicode
Proved: T

8
tests/lean/apply_tac_bug.lean
View file

@ -1,8 +0,0 @@
import macros
import tactic
theorem my_proof_irrel {a b : Bool} (H1 : a) (H2 : b) : H1 == H2
:= let H1b : b := cast (by simp) H1,
H1_eq_H1b : H1 == H1b := hsymm (cast_heq (by simp) H1),
H1b_eq_H2 : H1b == H2 := to_heq (proof_irrel H1b H2)
in htrans H1_eq_H1b H1b_eq_H2

5
tests/lean/apply_tac_bug.lean.expected.out
View file

@ -1,5 +0,0 @@
Set: pp::colors
Set: pp::unicode
Imported 'macros'
Imported 'tactic'
Proved: my_proof_irrel

18
tests/lean/arith1.lean
View file

@ -1,18 +0,0 @@
import Int.
check 10 + 20
check 10
check 10 - 20
eval 10 - 20
eval 15 + 10 - 20
check 15 + 10 - 20
variable x : Int
variable n : Nat
variable m : Nat
print n + m
print n + x + m
set_option lean::pp::coercion true
print n + x + m + 10
print x + n + m + 10
print n + m + 10 + x
set_option lean::pp::notation false
print n + m + 10 + x

20
tests/lean/arith1.lean.expected.out
View file

@ -1,20 +0,0 @@
Set: pp::colors
Set: pp::unicode
Imported 'Int'
10 + 20 : ℕ
10 : ℕ
10 - 20 : ℤ
10 - 20
25 - 20
15 + 10 - 20 : ℤ
Assumed: x
Assumed: n
Assumed: m
n + m
n + x + m
Set: lean::pp::coercion
nat_to_int n + x + nat_to_int m + nat_to_int 10
x + nat_to_int n + nat_to_int m + nat_to_int 10
nat_to_int (n + m + 10) + x
Set: lean::pp::notation
Int::add (nat_to_int (Nat::add (Nat::add n m) 10)) x

16
tests/lean/arith2.lean
View file

@ -1,16 +0,0 @@
import Int.
import Real.
print 1/2
eval 4/6
print 3 div 2
variable x : Real
variable i : Int
variable n : Nat
print x + i + 1 + n
set_option lean::pp::coercion true
print x + i + 1 + n
print x * i + x
print x - i + x - x >= 0
print x < x
print x <= x
print x > x

18
tests/lean/arith2.lean.expected.out
View file

@ -1,18 +0,0 @@
Set: pp::colors
Set: pp::unicode
Imported 'Int'
Imported 'Real'
1 / 2
2/3
3 div 2
Assumed: x
Assumed: i
Assumed: n
x + i + 1 + n
Set: lean::pp::coercion
x + int_to_real i + nat_to_real 1 + nat_to_real n
x * int_to_real i + x
x - int_to_real i + x - x ≥ nat_to_real 0
x < x
x ≤ x
x > x

10
tests/lean/arith3.lean
View file

@ -1,10 +0,0 @@
import Int.
eval 8 mod 3
eval 8 div 4
eval 7 div 3
eval 7 mod 3
print -8 mod 3
set_option lean::pp::notation false
print -8 mod 3
eval -8 mod 3
eval (-8 div 3)*3 + (-8 mod 3)

12
tests/lean/arith3.lean.expected.out
View file

@ -1,12 +0,0 @@
Set: pp::colors
Set: pp::unicode
Imported 'Int'
8 mod 3
2
2
7 mod 3
-8 mod 3
Set: lean::pp::notation
Int::mod -8 3
Int::mod -8 3
Int::add -6 (Int::mod -8 3)

8
tests/lean/arith4.lean
View file

@ -1,8 +0,0 @@
import specialfn.
variable x : Real
eval sin(x)
eval cos(x)
eval tan(x)
eval cot(x)
eval sec(x)
eval csc(x)

10
tests/lean/arith4.lean.expected.out
View file

@ -1,10 +0,0 @@
Set: pp::colors
Set: pp::unicode
Imported 'specialfn'
Assumed: x
sin x
sin (x + -1 * (π / 2))
sin x / sin (x + -1 * (π / 2))
sin (x + -1 * (π / 2)) / sin x
1 / sin (x + -1 * (π / 2))
1 / sin x

8
tests/lean/arith5.lean
View file

@ -1,8 +0,0 @@
import specialfn.
variable x : Real
eval sinh(x)
eval cosh(x)
eval tanh(x)
eval coth(x)
eval sech(x)
eval csch(x)

10
tests/lean/arith5.lean.expected.out
View file

@ -1,10 +0,0 @@
Set: pp::colors
Set: pp::unicode
Imported 'specialfn'
Assumed: x
(1 + -1 * exp (-2 * x)) / (2 * exp (-1 * x))
(1 + exp (-2 * x)) / (2 * exp (-1 * x))
(1 + -1 * exp (-2 * x)) / (2 * exp (-1 * x)) / ((1 + exp (-2 * x)) / (2 * exp (-1 * x)))
(1 + exp (-2 * x)) / (2 * exp (-1 * x)) / ((1 + -1 * exp (-2 * x)) / (2 * exp (-1 * x)))
1 / ((1 + exp (-2 * x)) / (2 * exp (-1 * x)))
1 / ((1 + -1 * exp (-2 * x)) / (2 * exp (-1 * x)))

13
tests/lean/arith6.lean
View file

@ -1,13 +0,0 @@
import Int.
set_option pp::unicode false
print 3 | 6
eval 3 | 6
eval 3 | 7
eval 2 | 6
eval 1 | 6
variable x : Int
eval x | 3
eval 3 | x
eval 6 | 3
set_option pp::notation false
print 3 | x

15
tests/lean/arith6.lean.expected.out
View file

@ -1,15 +0,0 @@
Set: pp::colors
Set: pp::unicode
Imported 'Int'
Set: pp::unicode
3 | 6
3 | 6
3 | 7
2 | 6
1 | 6
Assumed: x
x | 3
3 | x
6 | 3
Set: lean::pp::notation
Int::divides 3 x

16
tests/lean/arith7.lean
View file

@ -1,16 +0,0 @@
import Int.
check | -2 |
-- Unfortunately, we can't write |-2|, because |- is considered a single token.
-- It is not wise to change that since the symbol |- can be used as the notation for
-- entailment relation in Lean.
eval |3|
definition x : Int := -3
check |x + 1|
check |x + 1| > 0
variable y : Int
check |x + y|
print |x + y| > x
set_option pp::notation false
print |x + y| > x
print |x + y| + |y + x| > x

14
tests/lean/arith7.lean.expected.out
View file

@ -1,14 +0,0 @@
Set: pp::colors
Set: pp::unicode
Imported 'Int'
| -2 | : ℤ
| 3 |
Defined: x
| x + 1 | : ℤ
| x + 1 | > 0 : Bool
Assumed: y
| x + y | : ℤ
| x + y | > x
Set: lean::pp::notation
Int::gt (Int::abs (Int::add x y)) x
Int::gt (Int::add (Int::abs (Int::add x y)) (Int::abs (Int::add y x))) x

6
tests/lean/arith8.lean
View file

@ -1,6 +0,0 @@
import Real.
eval 10.3
eval 0.3
eval 0.3 + 0.1
eval 0.2 + 0.7
eval 1/3 + 0.1

8
tests/lean/arith8.lean.expected.out
View file

@ -1,8 +0,0 @@
Set: pp::colors
Set: pp::unicode
Imported 'Real'
103/10
3/10
2/5
9/10
13/30

5
tests/lean/arrow.lean
View file

@ -1,5 +0,0 @@
import Int.
print (Int -> Int) -> Int
print Int -> Int -> Int
print Int -> (Int -> Int)
print (Int -> Int) -> (Int -> Int) -> Int

7
tests/lean/arrow.lean.expected.out
View file

@ -1,7 +0,0 @@
Set: pp::colors
Set: pp::unicode
Imported 'Int'
(ℤ → ℤ) → ℤ
ℤ → ℤ → ℤ
ℤ → ℤ → ℤ
(ℤ → ℤ) → (ℤ → ℤ) → ℤ

4
tests/lean/bad1.lean
View file

@ -1,4 +0,0 @@
import Int.
variable g : forall A : Type, A -> A.
variables a b : Int
axiom H1 : g _ a > 0

7
tests/lean/bad1.lean.expected.out
View file

@ -1,7 +0,0 @@
Set: pp::colors
Set: pp::unicode
Imported 'Int'
Assumed: g
Assumed: a
Assumed: b
Assumed: H1

8
tests/lean/bad10.lean
View file

@ -1,8 +0,0 @@
set_option pp::implicit true.
set_option pp::colors false.
variable N : Type.
definition T (a : N) (f : _ -> _) (H : f a = a) : f (f _) = f _ :=
substp (fun x : N, f (f a) = _) (refl (f (f _))) H.
print environment 1.

8
tests/lean/bad10.lean.expected.out
View file

@ -1,8 +0,0 @@
Set: pp::colors
Set: pp::unicode
Set: lean::pp::implicit
Set: pp::colors
Assumed: N
Defined: T
definition T (a : N) (f : N → N) (H : @eq N (f a) a) : @eq N (f (f a)) (f (f a)) :=
@substp N (f a) a (λ x : N, @eq N (f (f a)) (f (f a))) (@refl N (f (f a))) H

13
tests/lean/bad2.lean
View file

@ -1,13 +0,0 @@
import Int.
variable list : Type -> Type
variable nil {A : Type} : list A
variable cons {A : Type} (head : A) (tail : list A) : list A
definition n1 : list Int := cons (nat_to_int 10) nil
definition n2 : list Nat := cons 10 nil
definition n3 : list Int := cons 10 nil
definition n4 : list Int := nil
definition n5 : _ := cons 10 nil
set_option pp::coercion true
set_option pp::implicit true
print environment 1.

14
tests/lean/bad2.lean.expected.out
View file

@ -1,14 +0,0 @@
Set: pp::colors
Set: pp::unicode
Imported 'Int'
Assumed: list
Assumed: nil
Assumed: cons
Defined: n1
Defined: n2
Defined: n3
Defined: n4
Defined: n5
Set: lean::pp::coercion
Set: lean::pp::implicit
definition n5 : list ℕ := @cons ℕ 10 (@nil ℕ)

9
tests/lean/bad3.lean
View file

@ -1,9 +0,0 @@
import Int.
variable list : Type -> Type
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
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))

13
tests/lean/bad3.lean.expected.out
View file

@ -1,13 +0,0 @@
Set: pp::colors
Set: pp::unicode
Imported 'Int'
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 ℤ

4
tests/lean/bad4.lean
View file

@ -1,4 +0,0 @@
import Int.
variable f {A : Type} (a : A) : A
variable a : Int
definition tst : Bool := (fun x, (f x) > 10) a

6
tests/lean/bad4.lean.expected.out
View file

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

8
tests/lean/bad5.lean
View file

@ -1,8 +0,0 @@
import Int.
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 := substp (λ x, (g x) > 0) H2 H1
print environment 2

11
tests/lean/bad5.lean.expected.out
View file

@ -1,11 +0,0 @@
Set: pp::colors
Set: pp::unicode
Imported 'Int'
Assumed: g
Assumed: a
Assumed: b
Assumed: H1
Assumed: H2
Proved: T1
axiom H2 : g a > 0
theorem T1 : g b > 0 := substp (λ x : ℤ, g x > 0) H2 H1

6
tests/lean/bad6.lean
View file

@ -1,6 +0,0 @@
import Int.
import Real.
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

8
tests/lean/bad6.lean.expected.out
View file

@ -1,8 +0,0 @@
Set: pp::colors
Set: pp::unicode
Imported 'Int'
Imported 'Real'
Assumed: f
Assumed: a
Assumed: b
Defined: tst

6
tests/lean/bad7.lean
View file

@ -1,6 +0,0 @@
import Real.
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
print environment 1

8
tests/lean/bad7.lean.expected.out
View file

@ -1,8 +0,0 @@
Set: pp::colors
Set: pp::unicode
Imported 'Real'
Assumed: f
Assumed: a
Assumed: b
Defined: tst
definition tst : Bool := (λ x y : ℝ, f x y) a b

10
tests/lean/bad8.lean
View file

@ -1,10 +0,0 @@
import Int.
variable list : Type → Type
variable nil {A : Type} : list A
variable cons {A : Type} (head : A) (tail : list A) : list A
variable a : ℤ
variable b : ℤ
variable n : ℕ
variable m : ℕ
definition l1 : list ℤ := cons a (cons b (cons n nil))
definition l2 : list ℤ := cons a (cons n (cons b nil))

12
tests/lean/bad8.lean.expected.out
View file

@ -1,12 +0,0 @@
Set: pp::colors
Set: pp::unicode
Imported 'Int'
Assumed: list
Assumed: nil
Assumed: cons
Assumed: a
Assumed: b
Assumed: n
Assumed: m
Defined: l1
Defined: l2

8
tests/lean/bad9.lean
View file

@ -1,8 +0,0 @@
set_option pp::implicit true.
set_option pp::colors false.
variable N : Type.
check
fun (a : N) (f : N -> N) (H : f a = a),
let calc1 : f a = a := substp (fun x : N, f a = _) (refl (f a)) H
in calc1.

8
tests/lean/bad9.lean.expected.out
View file

@ -1,8 +0,0 @@
Set: pp::colors
Set: pp::unicode
Set: lean::pp::implicit
Set: pp::colors
Assumed: N
λ (a : N) (f : N → N) (H : @eq N (f a) a),
let calc1 : @eq N (f a) a := @substp N (f a) a (λ x : N, @eq N (f a) x) (@refl N (f a)) H in calc1 :
∀ (a : N) (f : N → N), @eq N (f a) a → @eq N (f a) a

14
tests/lean/bad_simp.lean
View file

@ -1,14 +0,0 @@
variable f : Nat → Nat
variable g : Nat → Nat
axiom Ax1 : ∀ x, f x = g (f x)
rewrite_set S
add_rewrite Ax1 : S
-- Ax1 is not included in the rewrite rule set because the left-hand-side occurs in the right-hand side
print rewrite_set S
axiom Ax2 : ∀ x, f x > 0 → f x = x
add_rewrite Ax2 : S
-- Ax2 is not included in the rewrite rule set because the left-hand-side occurs in the hypothesis
print rewrite_set S
print "done"

9
tests/lean/bad_simp.lean.expected.out
View file

@ -1,9 +0,0 @@
Set: pp::colors
Set: pp::unicode
Assumed: f
Assumed: g
Assumed: Ax1
Assumed: Ax2
done

53
tests/lean/bad_simp2.lean
View file

@ -1,53 +0,0 @@
import tactic
universe U >= 2
variable f (A : (Type 1)) : (Type 1)
axiom Ax1 (a : Type) : f a = a
rewrite_set S
add_rewrite Ax1 eq_id : S
theorem T1a (A : Type) : f A = A
:= by simp S
-- The following theorem should not be provable.
-- The axiom Ax1 is only for arguments convertible to Type (i.e., Type 0)
-- The argument A in the following theorem lives in (Type 1)
theorem T1b (A : (Type 1)) : f A = A
:= by simp S
variable g (A : Type → (Type 1)) : (Type 1)
axiom Ax2 (a : Type → Type) : g a = a Bool
add_rewrite Ax2 : S
theorem T2a (A : Type → Type) : g A = A Bool
:= by simp S
-- The following theorem should not be provable.
-- See T1b
theorem T2b (A : Type → (Type 1)) : g A = A Bool
:= by simp S
variable h (A : Type) (B : (Type 1)) : (Type 1)
axiom Ax3 (a : Type) : h a a = a
add_rewrite Ax3 : S
theorem T3a (A : Type) : h A A = A
:= by simp S
axiom Ax4 (a b : Type) : h a b = b
add_rewrite Ax4 : S
theorem T4a (A : Type) (B : Type) : h A B = B
:= by simp S
-- The following theorem should not be provable.
-- See T1b
theorem T4b (A : Type) (B : (Type 1)) : h A B = B
:= by simp S
variable h2 (A : Type) (B : (Type 1)) : Type
axiom Ax5 (a b : Type) : f a = a -> h2 a b = a
add_rewrite Ax5 : S
theorem T5a (A B : Type) : h2 A B = A
:= by simp S
-- The following theorem should not be provable.
-- See T1b
theorem T5b (A : Type) (B : (Type 1)) : h2 A B = A
:= by simp S
print environment 1

32
tests/lean/bad_simp2.lean.expected.out
View file

@ -1,32 +0,0 @@
Set: pp::colors
Set: pp::unicode
Imported 'tactic'
Assumed: f
Assumed: Ax1
Proved: T1a
bad_simp2.lean:14:3: error: failed to create proof for the following proof state
Proof state:
A : (Type 1) ⊢ f A = A
Assumed: g
Assumed: Ax2
Proved: T2a
bad_simp2.lean:24:3: error: failed to create proof for the following proof state
Proof state:
A : Type → (Type 1) ⊢ g A = A Bool
Assumed: h
Assumed: Ax3
Proved: T3a
Assumed: Ax4
Proved: T4a
bad_simp2.lean:40:3: error: failed to create proof for the following proof state
Proof state:
A : Type, B : (Type 1) ⊢ h A B = B
Assumed: h2
Assumed: Ax5
Proved: T5a
bad_simp2.lean:51:3: error: failed to create proof for the following proof state
Proof state:
A : Type, B : (Type 1) ⊢ h2 A B = A
theorem T5a (A B : Type) : h2 A B = A :=
eqt_elim (trans (congr1 (congr2 eq (Ax5 A B (eqt_elim (trans (congr1 (congr2 eq (Ax1 A)) A) (eq_id A))))) A)
(eq_id A))

165
tests/lean/bare/NatHoles.lean
View file

@ -1,165 +0,0 @@
(*
Nat library full of "holes".
We provide only the proof skeletons, and let Lean infer the rest.
*)
Import kernel.
Variable Nat : Type.
Alias ℕ : Nat.
Namespace Nat.
Builtin numeral.
Builtin add : Nat → Nat → Nat.
Infixl 65 + : add.
Builtin mul : Nat → Nat → Nat.
Infixl 70 * : mul.
Builtin le : Nat → Nat → Bool.
Infix 50 <= : le.
Infix 50 ≤ : le.
Definition ge (a b : Nat) := b ≤ a.
Infix 50 >= : ge.
Infix 50 ≥ : ge.
Definition lt (a b : Nat) := ¬ (a ≥ b).
Infix 50 < : lt.
Definition gt (a b : Nat) := ¬ (a ≤ b).
Infix 50 > : gt.
Definition id (a : Nat) := a.
Notation 55 | _ | : id.
Axiom SuccInj {a b : Nat} (H : a + 1 = b + 1) : a = b
Axiom PlusZero (a : Nat) : a + 0 = a.
Axiom PlusSucc (a b : Nat) : a + (b + 1) = (a + b) + 1.
Axiom MulZero (a : Nat) : a * 0 = 0.
Axiom MulSucc (a b : Nat) : a * (b + 1) = a * b + a.
Axiom Induction {P : Nat → Bool} (Hb : P 0) (iH : Π (n : Nat) (H : P n), P (n + 1)) (a : Nat) : P a.
Theorem ZeroNeOne : 0 ≠ 1 := Trivial.
Theorem ZeroPlus (a : Nat) : 0 + a = a
:= Induction (show 0 + 0 = 0, Trivial)
(λ (n : Nat) (iH : 0 + n = n),
calc 0 + (n + 1) = (0 + n) + 1 : PlusSucc _ _
... = n + 1 : { iH })
a.
Theorem SuccPlus (a b : Nat) : (a + 1) + b = (a + b) + 1
:= Induction (calc (a + 1) + 0 = a + 1 : PlusZero _
... = (a + 0) + 1 : { Symm (PlusZero _) })
(λ (n : Nat) (iH : (a + 1) + n = (a + n) + 1),
calc (a + 1) + (n + 1) = ((a + 1) + n) + 1 : PlusSucc _ _
... = ((a + n) + 1) + 1 : { iH }
... = (a + (n + 1)) + 1 : { Symm (PlusSucc _ _) })
b.
Theorem PlusComm (a b : Nat) : a + b = b + a
:= Induction (calc a + 0 = a : PlusZero a
... = 0 + a : Symm (ZeroPlus a))
(λ (n : Nat) (iH : a + n = n + a),
calc a + (n + 1) = (a + n) + 1 : PlusSucc _ _
... = (n + a) + 1 : { iH }
... = (n + 1) + a : Symm (SuccPlus _ _))
b.
Theorem PlusAssoc (a b c : Nat) : a + (b + c) = (a + b) + c
:= Induction (calc 0 + (b + c) = b + c : ZeroPlus _
... = (0 + b) + c : { Symm (ZeroPlus _) })
(λ (n : Nat) (iH : n + (b + c) = (n + b) + c),
calc (n + 1) + (b + c) = (n + (b + c)) + 1 : SuccPlus _ _
... = ((n + b) + c) + 1 : { iH }
... = ((n + b) + 1) + c : Symm (SuccPlus _ _)
... = ((n + 1) + b) + c : { Symm (SuccPlus _ _) })
a.
Theorem ZeroMul (a : Nat) : 0 * a = 0
:= Induction (show 0 * 0 = 0, Trivial)
(λ (n : Nat) (iH : 0 * n = 0),
calc 0 * (n + 1) = (0 * n) + 0 : MulSucc _ _
... = 0 + 0 : { iH }
... = 0 : Trivial)
a.
Theorem SuccMul (a b : Nat) : (a + 1) * b = a * b + b
:= Induction (calc (a + 1) * 0 = 0 : MulZero _
... = a * 0 : Symm (MulZero _)
... = a * 0 + 0 : Symm (PlusZero _))
(λ (n : Nat) (iH : (a + 1) * n = a * n + n),
calc (a + 1) * (n + 1) = (a + 1) * n + (a + 1) : MulSucc _ _
... = a * n + n + (a + 1) : { iH }
... = a * n + n + a + 1 : PlusAssoc _ _ _
... = a * n + (n + a) + 1 : { Symm (PlusAssoc _ _ _) }
... = a * n + (a + n) + 1 : { PlusComm _ _ }
... = a * n + a + n + 1 : { PlusAssoc _ _ _ }
... = a * (n + 1) + n + 1 : { Symm (MulSucc _ _) }
... = a * (n + 1) + (n + 1) : Symm (PlusAssoc _ _ _))
b.
Theorem OneMul (a : Nat) : 1 * a = a
:= Induction (show 1 * 0 = 0, Trivial)
(λ (n : Nat) (iH : 1 * n = n),
calc 1 * (n + 1) = 1 * n + 1 : MulSucc _ _
... = n + 1 : { iH })
a.
Theorem MulOne (a : Nat) : a * 1 = a
:= Induction (show 0 * 1 = 0, Trivial)
(λ (n : Nat) (iH : n * 1 = n),
calc (n + 1) * 1 = n * 1 + 1 : SuccMul _ _
... = n + 1 : { iH })
a.
Theorem MulComm (a b : Nat) : a * b = b * a
:= Induction (calc a * 0 = 0 : MulZero a
... = 0 * a : Symm (ZeroMul a))
(λ (n : Nat) (iH : a * n = n * a),
calc a * (n + 1) = a * n + a : MulSucc _ _
... = n * a + a : { iH }
... = (n + 1) * a : Symm (SuccMul _ _))
b.
Theorem Distribute (a b c : Nat) : a * (b + c) = a * b + a * c
:= Induction (calc 0 * (b + c) = 0 : ZeroMul _
... = 0 + 0 : Trivial
... = 0 * b + 0 : { Symm (ZeroMul _) }
... = 0 * b + 0 * c : { Symm (ZeroMul _) })
(λ (n : Nat) (iH : n * (b + c) = n * b + n * c),
calc (n + 1) * (b + c) = n * (b + c) + (b + c) : SuccMul _ _
... = n * b + n * c + (b + c) : { iH }
... = n * b + n * c + b + c : PlusAssoc _ _ _
... = n * b + (n * c + b) + c : { Symm (PlusAssoc _ _ _) }
... = n * b + (b + n * c) + c : { PlusComm _ _ }
... = n * b + b + n * c + c : { PlusAssoc _ _ _ }
... = (n + 1) * b + n * c + c : { Symm (SuccMul _ _) }
... = (n + 1) * b + (n * c + c) : Symm (PlusAssoc _ _ _)
... = (n + 1) * b + (n + 1) * c : { Symm (SuccMul _ _) })
a.
Theorem Distribute2 (a b c : Nat) : (a + b) * c = a * c + b * c
:= calc (a + b) * c = c * (a + b) : MulComm _ _
... = c * a + c * b : Distribute _ _ _
... = a * c + c * b : { MulComm _ _ }
... = a * c + b * c : { MulComm _ _}.
Theorem MulAssoc (a b c : Nat) : a * (b * c) = a * b * c
:= Induction (calc 0 * (b * c) = 0 : ZeroMul _
... = 0 * c : Symm (ZeroMul _)
... = (0 * b) * c : { Symm (ZeroMul _) })
(λ (n : Nat) (iH : n * (b * c) = n * b * c),
calc (n + 1) * (b * c) = n * (b * c) + (b * c) : SuccMul _ _
... = n * b * c + (b * c) : { iH }
... = (n * b + b) * c : Symm (Distribute2 _ _ _)
... = (n + 1) * b * c : { Symm (SuccMul _ _) })
a.
SetOpaque ge true.
SetOpaque lt true.
SetOpaque gt true.
SetOpaque id true.
EndNamespace.

1
tests/lean/bug.lean
View file

@ -1 +0,0 @@
check fun (A A' : (Type U)) (H : A = A'), symm H

10
tests/lean/bug.lean.expected.out
View file

@ -1,10 +0,0 @@
Set: pp::colors
Set: pp::unicode
Failed to solve
A : (Type U), A' : (Type U) ⊢ ?M::4 ≺ (Type U)
bug.lean:1:36: Type of argument 1 must be convertible to the expected type in the application of
@eq
with arguments:
?M::0
A
A'

15
tests/lean/calc1.lean
View file

@ -1,15 +0,0 @@
import tactic.
infixl 50 => : implies
variables a b c d e : Bool.
axiom H1 : a → b.
axiom H2 : b = c.
axiom H3 : c → d.
axiom H4 : d = e.
theorem T : a → e
:= calc a => b : H1
... = c : H2
... => d : H3
... = e : H4.

13
tests/lean/calc1.lean.expected.out
View file

@ -1,13 +0,0 @@
Set: pp::colors
Set: pp::unicode
Imported 'tactic'
Assumed: a
Assumed: b
Assumed: c
Assumed: d
Assumed: e
Assumed: H1
Assumed: H2
Assumed: H3
Assumed: H4
Proved: T

10
tests/lean/calc2.lean
View file

@ -1,10 +0,0 @@
variables a b c d e : Nat.
variable f : Nat -> Nat.
axiom H1 : f a = a.
theorem T : f (f (f a)) = a
:= calc f (f (f a)) = f (f a) : { H1 }
... = f a : { H1 }
... = a : { H1 }.

10
tests/lean/calc2.lean.expected.out
View file

@ -1,10 +0,0 @@
Set: pp::colors
Set: pp::unicode
Assumed: a
Assumed: b
Assumed: c
Assumed: d
Assumed: e
Assumed: f
Assumed: H1
Proved: T

15
tests/lean/coercion1.lean
View file

@ -1,15 +0,0 @@
variable T : Type
variable R : Type
variable f : T -> R
coercion f
print environment 2
variable g : T -> R
coercion g
variable h : forall (x : Type), x
coercion h
definition T2 : Type := T
definition R2 : Type := R
variable f2 : T2 -> R2
coercion f2
variable id : T -> T
coercion id

18
tests/lean/coercion1.lean.expected.out
View file

@ -1,18 +0,0 @@
Set: pp::colors
Set: pp::unicode
Assumed: T
Assumed: R
Assumed: f
Coercion f
variable f : T → R
coercion f
Assumed: g
coercion1.lean:7:0: error: invalid coercion declaration, frontend already has a coercion for the given types
Assumed: h
coercion1.lean:9:0: error: invalid coercion declaration, a coercion must have an arrow type (i.e., a non-dependent functional type)
Defined: T2
Defined: R2
Assumed: f2
coercion1.lean:13:0: error: invalid coercion declaration, frontend already has a coercion for the given types
Assumed: id
coercion1.lean:15:0: error: invalid coercion declaration, 'from' and 'to' types are the same

32
tests/lean/coercion2.lean
View file

@ -1,32 +0,0 @@
variable T : Type
variable R : Type
variable t2r : T -> R
coercion t2r
variable g : R -> R -> R
variable a : T
print g a a
variable b : R
print g a b
print g b a
set_option lean::pp::coercion true
print g a a
print g a b
print g b a
set_option lean::pp::coercion false
variable S : Type
variable s : S
variable r : S
variable h : S -> S -> S
infixl 10 ++ : g
infixl 10 ++ : h
set_option lean::pp::notation false
print a ++ b ++ a
print r ++ s ++ r
check a ++ b ++ a
check r ++ s ++ r
set_option lean::pp::coercion true
print a ++ b ++ a
print r ++ s ++ r
set_option lean::pp::notation true
print a ++ b ++ a
print r ++ s ++ r

32
tests/lean/coercion2.lean.expected.out
View file

@ -1,32 +0,0 @@
Set: pp::colors
Set: pp::unicode
Assumed: T
Assumed: R
Assumed: t2r
Coercion t2r
Assumed: g
Assumed: a
g a a
Assumed: b
g a b
g b a
Set: lean::pp::coercion
g (t2r a) (t2r a)
g (t2r a) b
g b (t2r a)
Set: lean::pp::coercion
Assumed: S
Assumed: s
Assumed: r
Assumed: h
Set: lean::pp::notation
g (g a b) a
h (h r s) r
g (g a b) a : R
h (h r s) r : S
Set: lean::pp::coercion
g (g (t2r a) b) (t2r a)
h (h r s) r
Set: lean::pp::notation
t2r a ++ b ++ t2r a
r ++ s ++ r

5
tests/lean/compact_def.lean
View file

@ -1,5 +0,0 @@
import specialfn.
definition f x y := x + y
definition g x y := sin x + y
definition h x y := x * sin (x + y)
print environment 3

9
tests/lean/compact_def.lean.expected.out
View file

@ -1,9 +0,0 @@
Set: pp::colors
Set: pp::unicode
Imported 'specialfn'
Defined: f
Defined: g
Defined: h
definition f (x y : ℕ) : ℕ := x + y
definition g (x y : ℝ) : ℝ := sin x + y
definition h (x y : ℝ) : ℝ := x * sin (x + y)

39
tests/lean/cond_tac.lean
View file

@ -1,39 +0,0 @@
import tactic
(*
simple_tac = Cond(function(env, ios, s)
local gs = s:goals()
local n, g = gs:head()
local r = g:conclusion():is_and()
print ("Cond result: " .. tostring(r))
return r
end,
Then(apply_tac("and_intro"), assumption_tac()),
Then(apply_tac("or_introl"), assumption_tac()))
simple2_tac = When(function(env, ios, s)
local gs = s:goals()
local n, g = gs:head()
local r = g:conclusion():is_and()
print ("When result: " .. tostring(r))
return r
end,
apply_tac("and_intro"))
*)
theorem T1 (a b c : Bool) : a -> b -> c -> a ∧ b.
(* simple_tac *)
done
theorem T2 (a b : Bool) : a -> a ∨ b.
(* simple_tac *)
done
theorem T4 (a b c : Bool) : a -> b -> c -> a ∧ b.
(* simple2_tac *)
exact
done
theorem T5 (a b c : Bool) : a -> b -> c -> a ∨ b.
(* simple2_tac *)
apply or_introl
exact
done

11
tests/lean/cond_tac.lean.expected.out
View file

@ -1,11 +0,0 @@
Set: pp::colors
Set: pp::unicode
Imported 'tactic'
Cond result: true
Proved: T1
Cond result: false
Proved: T2
When result: true
Proved: T4
When result: false
Proved: T5

3
tests/lean/config.lean
View file

@ -1,3 +0,0 @@
-- set_option default configuration for tests
set_option pp::colors false
set_option pp::unicode true

4
tests/lean/config.lean.expected.out
View file

@ -1,4 +0,0 @@
Set: pp::colors
Set: pp::unicode
Set: pp::colors
Set: pp::unicode

20
tests/lean/conv.lean
View file

@ -1,20 +0,0 @@
import Int.
definition id (A : Type) : (Type U) := A.
variable p : (Int -> Int) -> Bool.
check fun (x : id Int), x.
variable f : (id Int) -> (id Int).
check p f.
definition c (A : (Type 3)) : (Type 3) := (Type 1).
variable g : (c (Type 2)) -> Bool.
variable a : (c (Type 1)).
check g a.
definition c2 {T : Type} (A : (Type 3)) (a : T) : (Type 3) := (Type 1)
variable b : Int
check @c2
variable g2 : (c2 (Type 2) b) -> Bool
check g2
variable a2 : (c2 (Type 1) b).
check g2 a2
check fun x : (c2 (Type 1) b), g2 x

20
tests/lean/conv.lean.expected.out
View file

@ -1,20 +0,0 @@
Set: pp::colors
Set: pp::unicode
Imported 'Int'
Defined: id
Assumed: p
λ x : id ℤ, x : id ℤ → id ℤ
Assumed: f
p f : Bool
Defined: c
Assumed: g
Assumed: a
g a : Bool
Defined: c2
Assumed: b
@c2 : ∀ (T : Type), (Type 3) → T → (Type 3)
Assumed: g2
g2 : c2 (Type 2) b → Bool
Assumed: a2
g2 a2 : Bool
λ x : c2 (Type 1) b, g2 x : c2 (Type 1) b → Bool

4
tests/lean/discharge.lean
View file

@ -1,4 +0,0 @@
import tactic
theorem T (a b : Bool) : a → b → b → a.
exact.
done.

4
tests/lean/discharge.lean.expected.out
View file

@ -1,4 +0,0 @@
Set: pp::colors
Set: pp::unicode
Imported 'tactic'
Proved: T

20
tests/lean/disj1.lean
View file

@ -1,20 +0,0 @@
import tactic
theorem T1 (a b : Bool) : a \/ b → b \/ a.
(* disj_hyp_tac() *)
(* disj_tac() *)
back
exact.
(* disj_tac() *)
exact.
done.
(*
simple_tac = Repeat(OrElse(assumption_tac(), disj_hyp_tac(), disj_tac())) .. now_tac()
*)
theorem T2 (a b : Bool) : a \/ b → b \/ a.
simple_tac.
done.
print environment 1.

6
tests/lean/disj1.lean.expected.out
View file

@ -1,6 +0,0 @@
Set: pp::colors
Set: pp::unicode
Imported 'tactic'
Proved: T1
Proved: T2
theorem T2 (a b : Bool) (H : a ∨ b) : b ∨ a := or_elim H (λ H : a, or_intror b H) (λ H : b, or_introl H a)

10
tests/lean/disjcases.lean
View file

@ -1,10 +0,0 @@
(* import("tactic.lua") *)
variables a b c : Bool
axiom H : a \/ b
theorem T (a b : Bool) : a \/ b → b \/ a.
apply (or_elim H).
apply or_intror.
exact.
apply or_introl.
exact.
done.

7
tests/lean/disjcases.lean.expected.out
View file

@ -1,7 +0,0 @@
Set: pp::colors
Set: pp::unicode
Assumed: a
Assumed: b
Assumed: c
Assumed: H
Proved: T

27
tests/lean/elab1.lean
View file

@ -1,27 +0,0 @@
variable f {A : Type} (a b : A) : A.
check f 10 true
variable g {A B : Type} (a : A) : A.
check g 10
variable h : forall (A : Type), A -> A.
check fun x, fun A : Type, h A x
variable my_eq : forall A : Type, A -> A -> Bool.
check fun (A B : Type) (a : _) (b : _) (C : Type), my_eq C a b.
variable a : Bool
variable b : Bool
variable H : a /\ b
theorem t1 : b := (fun H1, and_intro H1 (and_eliml H)).
theorem t2 : a = b := trans (refl a) (refl b).
check f Bool Bool.
theorem pierce (a b : Bool) : ((a -> b) -> a) -> a :=
λ H, or_elim (EM a)
(λ H_a, H)
(λ H_na, NotImp1 (MT H H_na))

58
tests/lean/elab1.lean.expected.out
View file

@ -1,58 +0,0 @@
Set: pp::colors
Set: pp::unicode
Assumed: f
Failed to solve
⊢ Bool ≺ ℕ
elab1.lean:2:6: Type of argument 3 must be convertible to the expected type in the application of
@f
with arguments:
ℕ
10
⊤
Assumed: g
elab1.lean:5:0: error: invalid expression, it still contains metavariables after elaboration
@g ℕ ?M::1 10
elab1.lean:5:8: error: unsolved metavar M::1
Assumed: h
Failed to solve
x : ?M::0, A : Type ⊢ ?M::0 ≺ A
elab1.lean:9:27: Type of argument 2 must be convertible to the expected type in the application of
h
with arguments:
A
x
Assumed: my_eq
Failed to solve
A : Type, B : Type, a : ?M::0, b : ?M::1, C : Type ⊢ ?M::0[lift:0 3] ≺ C
elab1.lean:13:51: Type of argument 2 must be convertible to the expected type in the application of
my_eq
with arguments:
C
a
b
Assumed: a
Assumed: b
Assumed: H
Failed to solve
⊢ ∀ H1 : ?M::0, ?M::1 ∧ a ≈ b
elab1.lean:18:18: Type of definition 't1' must be convertible to expected type.
Failed to solve
⊢ @eq ?M::6 b b ≺ @eq ?M::1 a b
elab1.lean:20:22: Type of argument 6 must be convertible to the expected type in the application of
@trans
with arguments:
?M::1
a
a
b
@refl ?M::1 a
@refl ?M::6 b
Failed to solve
⊢ ?M::1 ≺ Type
elab1.lean:22:6: Type of argument 1 must be convertible to the expected type in the application of
@f
with arguments:
?M::0
Bool
Bool
elab1.lean:25:18: error: unknown identifier 'EM'

24
tests/lean/elab2.lean
View file

@ -1,24 +0,0 @@
variable C : forall (A B : Type) (H : A = B) (a : A), B
variable D : forall (A A' : Type) (B : A -> Type) (B' : A' -> Type) (H : (forall x : A, B x) = (forall x : A', B' x)), A = A'
variable R : forall (A A' : Type) (B : A -> Type) (B' : A' -> Type) (H : (forall x : A, B x) = (forall x : A', B' x)) (a : A),
(B a) = (B' (C A A' (D A A' B B' H) a))
theorem R2 (A A' B B' : Type) (H : (A -> B) = (A' -> B')) (a : A) : B = B' := R _ _ _ _ H a
print environment 1
theorem R3 : forall (A1 A2 B1 B2 : Type) (H : (A1 -> B1) = (A2 -> B2)) (a : A1), B1 = B2 :=
fun (A1 A2 B1 B2 : Type) (H : (A1 -> B1) = (A2 -> B2)) (a : A1),
R _ _ _ _ H a
theorem R4 : forall (A1 A2 B1 B2 : Type) (H : (A1 -> B1) = (A2 -> B2)) (a : A1), B1 = B2 :=
fun (A1 A2 B1 B2 : Type) (H : (A1 -> B1) = (A2 -> B2)) (a : _),
R _ _ _ _ H a
theorem R5 : forall (A1 A2 B1 B2 : Type) (H : (A1 -> B1) = (A2 -> B2)) (a : A1), B1 = B2 :=
fun (A1 A2 B1 B2 : Type) (H : _) (a : _),
R _ _ _ _ H a
print environment 1

12
tests/lean/elab2.lean.expected.out
View file

@ -1,12 +0,0 @@
Set: pp::colors
Set: pp::unicode
Assumed: C
Assumed: D
Assumed: R
Proved: R2
theorem R2 (A A' B B' : Type) (H : (A → B) = (A' → B')) (a : A) : B = B' := R A A' (λ x : A, B) (λ x : A', B') H a
Proved: R3
Proved: R4
Proved: R5
theorem R5 (A1 A2 B1 B2 : Type) (H : (A1 → B1) = (A2 → B2)) (a : A1) : B1 = B2 :=
R A1 A2 (λ x : A1, B1) (λ x : A2, B2) H a

12
tests/lean/elab3.lean
View file

@ -1,12 +0,0 @@
variable C : forall (A B : Type) (H : A = B) (a : A), B
variable D : forall (A A' : Type) (B : A -> Type) (B' : A' -> Type) (H : (forall x : A, B x) = (forall x : A', B' x)), A = A'
variable R : forall (A A' : Type) (B : A -> Type) (B' : A' -> Type) (H : (forall x : A, B x) = (forall x : A', B' x)) (a : A),
(B a) = (B' (C A A' (D A A' B B' H) a))
theorem R2 : forall (A1 A2 B1 B2 : Type) (H : (A1 -> B1) = (A2 -> B2)) (a : A1), B1 = B2 :=
fun A1 A2 B1 B2 H a,
R _ _ _ _ H a
print environment 1.

8
tests/lean/elab3.lean.expected.out
View file

@ -1,8 +0,0 @@
Set: pp::colors
Set: pp::unicode
Assumed: C
Assumed: D
Assumed: R
Proved: R2
theorem R2 (A1 A2 B1 B2 : Type) (H : (A1 → B1) = (A2 → B2)) (a : A1) : B1 = B2 :=
R A1 A2 (λ x : A1, B1) (λ x : A2, B2) H a

12
tests/lean/elab4.lean
View file

@ -1,12 +0,0 @@
variable C {A B : Type} (H : A = B) (a : A) : B
variable D {A A' : Type} {B : A -> Type} {B' : A' -> Type} (H : (forall x : A, B x) = (forall x : A', B' x)) : A = A'
variable R {A A' : Type} {B : A -> Type} {B' : A' -> Type} (H : (forall x : A, B x) = (forall x : A', B' x)) (a : A) :
(B a) = (B' (C (D H) a))
theorem R2 : forall (A1 A2 B1 B2 : Type) (H : (A1 -> B1) = (A2 -> B2)) (a : A1), B1 = B2 :=
fun A1 A2 B1 B2 H a, R H a
set_option pp::implicit true
print environment 7.

20
tests/lean/elab4.lean.expected.out
View file

@ -1,20 +0,0 @@
Set: pp::colors
Set: pp::unicode
Assumed: C
Assumed: D
Assumed: R
Proved: R2
Set: lean::pp::implicit
import "kernel"
import "Nat"
variable C {A B : Type} (H : @eq Type A B) (a : A) : B
variable D {A A' : Type} {B : A → Type} {B' : A' → Type} (H : @eq Type (∀ x : A, B x) (∀ x : A', B' x)) :
@eq Type A A'
variable R {A A' : Type}
{B : A → Type}
{B' : A' → Type}
(H : @eq Type (∀ x : A, B x) (∀ x : A', B' x))
(a : A) :
@eq Type (B a) (B' (@C A A' (@D A A' (λ x : A, B x) (λ x : A', B' x) H) a))
theorem R2 (A1 A2 B1 B2 : Type) (H : @eq Type (A1 → B1) (A2 → B2)) (a : A1) : @eq Type B1 B2 :=
@R A1 A2 (λ x : A1, B1) (λ x : A2, B2) H a

12
tests/lean/elab5.lean
View file

@ -1,12 +0,0 @@
variable C {A B : Type} (H : A = B) (a : A) : B
variable D {A A' : Type} {B : A -> Type} {B' : A' -> Type} (H : (forall x : A, B x) = (forall x : A', B' x)) : A = A'
variable R {A A' : Type} {B : A -> Type} {B' : A' -> Type} (H : (forall x : A, B x) = (forall x : A', B' x)) (a : A) :
(B a) = (B' (C (D H) a))
theorem R2 : forall (A1 A2 B1 B2 : Type), ((A1 -> B1) = (A2 -> B2)) -> A1 -> (B1 = B2) :=
fun A1 A2 B1 B2 H a, R H a
set_option pp::implicit true
print environment 7.

20
tests/lean/elab5.lean.expected.out
View file

@ -1,20 +0,0 @@
Set: pp::colors
Set: pp::unicode
Assumed: C
Assumed: D
Assumed: R
Proved: R2
Set: lean::pp::implicit
import "kernel"
import "Nat"
variable C {A B : Type} (H : @eq Type A B) (a : A) : B
variable D {A A' : Type} {B : A → Type} {B' : A' → Type} (H : @eq Type (∀ x : A, B x) (∀ x : A', B' x)) :
@eq Type A A'
variable R {A A' : Type}
{B : A → Type}
{B' : A' → Type}
(H : @eq Type (∀ x : A, B x) (∀ x : A', B' x))
(a : A) :
@eq Type (B a) (B' (@C A A' (@D A A' (λ x : A, B x) (λ x : A', B' x) H) a))
theorem R2 (A1 A2 B1 B2 : Type) (H : @eq Type (A1 → B1) (A2 → B2)) (a : A1) : @eq Type B1 B2 :=
@R A1 A2 (λ x : A1, B1) (λ x : A2, B2) H a

21
tests/lean/elab7.lean
View file

@ -1,21 +0,0 @@
variables A B C : (Type U)
variable P : A -> Bool
variable F1 : A -> B -> C
variable F2 : A -> B -> C
variable H : forall (a : A) (b : B), (F1 a b) = (F2 a b)
variable a : A
check eta (F2 a)
check funext (fun a : A,
(trans (symm (eta (F1 a)))
(trans (funext (fun (b : B), H a b))
(eta (F2 a)))))
check funext (fun a, (funext (fun b, H a b)))
theorem T1 : F1 = F2 := funext (fun a, (funext (fun b, H a b)))
theorem T2 : (fun (x1 : A) (x2 : B), F1 x1 x2) = F2 := funext (fun a, (funext (fun b, H a b)))
theorem T3 : F1 = (fun (x1 : A) (x2 : B), F2 x1 x2) := funext (fun a, (funext (fun b, H a b)))
theorem T4 : (fun (x1 : A) (x2 : B), F1 x1 x2) = (fun (x1 : A) (x2 : B), F2 x1 x2) := funext (fun a, (funext (fun b, H a b)))
print environment 4
set_option pp::implicit true
print environment 4

44
tests/lean/elab7.lean.expected.out
View file

@ -1,44 +0,0 @@
Set: pp::colors
Set: pp::unicode
Assumed: A
Assumed: B
Assumed: C
Assumed: P
Assumed: F1
Assumed: F2
Assumed: H
Assumed: a
eta (F2 a) : (λ x : B, F2 a x) = F2 a
funext (λ a : A, trans (symm (eta (F1 a))) (trans (funext (λ b : B, H a b)) (eta (F2 a)))) :
(λ x : A, F1 x) = (λ x : A, F2 x)
funext (λ a : A, funext (λ b : B, H a b)) : (λ (x : A) (x::1 : B), F1 x x::1) = (λ (x : A) (x::1 : B), F2 x x::1)
Proved: T1
Proved: T2
Proved: T3
Proved: T4
theorem T1 : F1 = F2 := funext (λ a : A, funext (λ b : B, H a b))
theorem T2 : (λ (x1 : A) (x2 : B), F1 x1 x2) = F2 := funext (λ a : A, funext (λ b : B, H a b))
theorem T3 : F1 = (λ (x1 : A) (x2 : B), F2 x1 x2) := funext (λ a : A, funext (λ b : B, H a b))
theorem T4 : (λ (x1 : A) (x2 : B), F1 x1 x2) = (λ (x1 : A) (x2 : B), F2 x1 x2) :=
funext (λ a : A, funext (λ b : B, H a b))
Set: lean::pp::implicit
theorem T1 : @eq (A → B → C) F1 F2 :=
@funext A (λ x : A, B → C) F1 F2 (λ a : A, @funext B (λ x : B, C) (F1 a) (F2 a) (λ b : B, H a b))
theorem T2 : @eq (A → B → C) (λ (x1 : A) (x2 : B), F1 x1 x2) F2 :=
@funext A
(λ x : A, B → C)
(λ (x1 : A) (x2 : B), F1 x1 x2)
F2
(λ a : A, @funext B (λ x : B, C) (λ x2 : B, F1 a x2) (F2 a) (λ b : B, H a b))
theorem T3 : @eq (A → B → C) F1 (λ (x1 : A) (x2 : B), F2 x1 x2) :=
@funext A
(λ x : A, B → C)
F1
(λ (x1 : A) (x2 : B), F2 x1 x2)
(λ a : A, @funext B (λ x : B, C) (F1 a) (λ x2 : B, F2 a x2) (λ b : B, H a b))
theorem T4 : @eq (A → B → C) (λ (x1 : A) (x2 : B), F1 x1 x2) (λ (x1 : A) (x2 : B), F2 x1 x2) :=
@funext A
(λ x : A, B → C)
(λ (x1 : A) (x2 : B), F1 x1 x2)
(λ (x1 : A) (x2 : B), F2 x1 x2)
(λ a : A, @funext B (λ x : B, C) (λ x2 : B, F1 a x2) (λ x2 : B, F2 a x2) (λ b : B, H a b))

3
tests/lean/elab8.lean
View file

@ -1,3 +0,0 @@
definition D1 (A : (Type U)) (B : Nat → (Type U)) := true
definition D2 (A : (Type U)) (B : A → (Type U)) := true
definition D3 (A : (Type U)) (B : A → (Type U)) := false

5
tests/lean/elab8.lean.expected.out
View file

@ -1,5 +0,0 @@
Set: pp::colors
Set: pp::unicode
Defined: D1
Defined: D2
Defined: D3

4
tests/lean/elab_bug1.lean
View file

@ -1,4 +0,0 @@
set_option pp::implicit true
check let P : Nat → Bool := λ x, x ≠ 0,
Q : ∀ x, P (x + 1) := λ x, Nat::succ_nz x
in Q

5
tests/lean/elab_bug1.lean.expected.out
View file

@ -1,5 +0,0 @@
Set: pp::colors
Set: pp::unicode
Set: lean::pp::implicit
let P : ℕ → Bool := λ x : ℕ, @neq ℕ x 0, Q : ∀ x : ℕ, P (x + 1) := λ x : ℕ, Nat::succ_nz x in Q :
∀ x : ℕ, (λ x : ℕ, @neq ℕ x 0) (x + 1)

27
tests/lean/env_errors.lean
View file

@ -1,27 +0,0 @@
variable x : Nat
set_opaque x true.
print "before import"
(*
local env = get_environment()
env:import("tstblafoo.lean")
*)
print "before load1"
(*
local env = get_environment()
env:load("tstblafoo.lean")
*)
print "before load2"
(*
local env = get_environment()
env:load("fake1.olean")
*)
print "before load3"
(*
local env = get_environment()
env:load("fake2.olean")
*)

Some files were not shown because too many files have changed in this diff Show more