diff --git a/doc/design.md b/doc/design.md
index 194b2bf2a..e4f1ba45f 100644
--- a/doc/design.md
+++ b/doc/design.md
@@ -17,13 +17,13 @@ In Lean, we allow users to provide partially specified objects such as definitio
We use `_` to denote holes. In the simple example above, the "whole proof" must be automatically computed by Lean. Here is another simple example:
- variable f : Pi (A : Type), A -> A -> A
+ variable f : forall (A : Type), A -> A -> A
definition f00 : Nat := f _ 0 0
In this example, Lean will automatically fill the hole with `Nat` (the type of the natural numbers).
Here is another example with multiple holes.
- variable g : Pi (A : Type), A -> A
+ variable g : forall (A : Type), A -> A
variable a : Nat
variable b : Nat
axiom H1 : a = b
diff --git a/examples/lean/ex2.lean b/examples/lean/ex2.lean
index cabb95225..1ccbedbe6 100644
--- a/examples/lean/ex2.lean
+++ b/examples/lean/ex2.lean
@@ -1,16 +1,16 @@
import macros.
-theorem simple (p q r : Bool) : (p ⇒ q) ∧ (q ⇒ r) ⇒ p ⇒ r
-:= assume H_pq_qr H_p,
- let P_pq := and::eliml H_pq_qr,
- P_qr := and::elimr H_pq_qr
- in P_qr ◂ (P_pq ◂ H_p)
+theorem simple (p q r : Bool) : (p → q) ∧ (q → r) → p → r
+:= λ H_pq_qr H_p,
+ let P_pq := and::eliml H_pq_qr,
+ P_qr := and::elimr H_pq_qr
+ in P_qr (P_pq H_p)
set::option pp::implicit true.
print environment 1.
-theorem simple2 (a b c : Bool) : (a ⇒ b ⇒ c) ⇒ (a ⇒ b) ⇒ a ⇒ c
-:= assume H_abc H_ab H_a,
- (H_abc ◂ H_a) ◂ (H_ab ◂ H_a)
+theorem simple2 (a b c : Bool) : (a → b → c) → (a → b) → a → c
+:= λ H_abc H_ab H_a,
+ (H_abc H_a) (H_ab H_a)
print environment 1.
diff --git a/examples/lean/ex3.lean b/examples/lean/ex3.lean
index 2030cf415..01f497f78 100644
--- a/examples/lean/ex3.lean
+++ b/examples/lean/ex3.lean
@@ -1,28 +1,28 @@
import macros.
-theorem and_comm (a b : Bool) : (a ∧ b) ⇒ (b ∧ a)
-:= assume H_ab, and::intro (and::elimr H_ab) (and::eliml H_ab).
+theorem and_comm (a b : Bool) : (a ∧ b) → (b ∧ a)
+:= λ H_ab, and::intro (and::elimr H_ab) (and::eliml H_ab).
-theorem or_comm (a b : Bool) : (a ∨ b) ⇒ (b ∨ a)
-:= assume H_ab,
+theorem or_comm (a b : Bool) : (a ∨ b) → (b ∨ a)
+:= λ H_ab,
or::elim H_ab
(λ H_a, or::intror b H_a)
(λ H_b, or::introl H_b a).
-- (em a) is the excluded middle a ∨ ¬a
-- (mt H H_na) is Modus Tollens with
--- H : (a ⇒ b) ⇒ a)
+-- H : (a → b) → a)
-- H_na : ¬a
-- produces
--- ¬(a ⇒ b)
+-- ¬(a → b)
--
-- not::imp::eliml applied to
--- (MT H H_na) : ¬(a ⇒ b)
+-- (MT H H_na) : ¬(a → b)
-- produces
-- a
-theorem pierce (a b : Bool) : ((a ⇒ b) ⇒ a) ⇒ a
-:= assume H, or::elim (em a)
- (λ H_a, H_a)
- (λ H_na, not::imp::eliml (mt H H_na)).
+theorem pierce (a b : Bool) : ((a → b) → a) → a
+:= λ H, or::elim (em a)
+ (λ H_a, H_a)
+ (λ H_na, not::imp::eliml (mt H H_na)).
print environment 3.
\ No newline at end of file
diff --git a/examples/lean/ex5.lean b/examples/lean/ex5.lean
index 5f2aaad08..ac375d2e0 100644
--- a/examples/lean/ex5.lean
+++ b/examples/lean/ex5.lean
@@ -3,34 +3,17 @@ import macros
scope
theorem ReflIf (A : Type)
(R : A → A → Bool)
- (Symm : Π x y, R x y → R y x)
- (Trans : Π x y z, R x y → R y z → R x z)
- (Linked : Π x, ∃ y, R x y)
+ (Symm : ∀ x y, R x y → R y x)
+ (Trans : ∀ x y z, R x y → R y z → R x z)
+ (Linked : ∀ x, ∃ y, R x y)
:
- Π x, R x x :=
+ ∀ x, R x x :=
λ x, obtain (w : A) (H : R x w), from (Linked x),
let L1 : R w x := Symm x w H
in Trans x w x H L1
pop::scope
-scope
- -- Same example but using ∀ instead of Π and ⇒ instead of →.
- -- Remark: H ◂ x is syntax sugar for forall::elim H x,
- -- and H1 ◂ H2 is syntax sugar for mp H1 H2
- theorem ReflIf (A : Type)
- (R : A → A → Bool)
- (Symm : ∀ x y, R x y ⇒ R y x)
- (Trans : ∀ x y z, R x y ⇒ R y z ⇒ R x z)
- (Linked : ∀ x, ∃ y, R x y)
- :
- ∀ x, R x x :=
- take x, obtain (w : A) (H : R x w), from (Linked ◂ x),
- let L1 : R w x := Symm ◂ x ◂ w ◂ H
- in Trans ◂ x ◂ w ◂ x ◂ H ◂ L1
-
-pop::scope
-
scope
-- Same example again.
variable A : Type
diff --git a/examples/lean/set.lean b/examples/lean/set.lean
index 7b2edb8bc..396aeb98d 100644
--- a/examples/lean/set.lean
+++ b/examples/lean/set.lean
@@ -5,33 +5,20 @@ definition Set (A : Type) : Type := A → Bool
definition element {A : Type} (x : A) (s : Set A) := s x
infix 60 ∈ : element
-definition subset {A : Type} (s1 : Set A) (s2 : Set A) := ∀ x, x ∈ s1 ⇒ x ∈ s2
+definition subset {A : Type} (s1 : Set A) (s2 : Set A) := ∀ x, x ∈ s1 → x ∈ s2
infix 50 ⊆ : subset
-theorem subset::trans (A : Type) : ∀ s1 s2 s3 : Set A, s1 ⊆ s2 ⇒ s2 ⊆ s3 ⇒ s1 ⊆ s3 :=
- take s1 s2 s3, assume (H1 : s1 ⊆ s2) (H2 : s2 ⊆ s3),
- have s1 ⊆ s3 :
- take x, assume Hin : x ∈ s1,
- have x ∈ s3 :
- let L1 : x ∈ s2 := H1 ◂ x ◂ Hin
- in H2 ◂ x ◂ L1
+theorem subset::trans {A : Type} {s1 s2 s3 : Set A} (H1 : s1 ⊆ s2) (H2 : s2 ⊆ s3) : s1 ⊆ s3
+:= λ (x : A) (Hin : x ∈ s1),
+ have x ∈ s3 :
+ let L1 : x ∈ s2 := H1 x Hin
+ in H2 x L1
-theorem subset::ext (A : Type) : ∀ s1 s2 : Set A, (∀ x, x ∈ s1 = x ∈ s2) ⇒ s1 = s2 :=
- take s1 s2, assume (H : ∀ x, x ∈ s1 = x ∈ s2),
- abst (λ x, H ◂ x)
+theorem subset::ext {A : Type} {s1 s2 : Set A} (H : ∀ x, x ∈ s1 = x ∈ s2) : s1 = s2
+:= abst H
-theorem subset::antisym (A : Type) : ∀ s1 s2 : Set A, s1 ⊆ s2 ⇒ s2 ⊆ s1 ⇒ s1 = s2 :=
- take s1 s2, assume (H1 : s1 ⊆ s2) (H2 : s2 ⊆ s1),
- have s1 = s2 :
- (have (∀ x, x ∈ s1 = x ∈ s2) ⇒ s1 = s2 :
- (subset::ext A) ◂ s1 ◂ s2)
- ◂ (have (∀ x, x ∈ s1 = x ∈ s2) :
- take x, have x ∈ s1 = x ∈ s2 :
- iff::intro (have x ∈ s1 ⇒ x ∈ s2 : H1 ◂ x)
- (have x ∈ s2 ⇒ x ∈ s1 : H2 ◂ x))
-
-
--- Compact (but less readable) version of the previous theorem
-theorem subset::antisym2 (A : Type) : ∀ s1 s2 : Set A, s1 ⊆ s2 ⇒ s2 ⊆ s1 ⇒ s1 = s2 :=
- take s1 s2, assume H1 H2,
- (subset::ext A) ◂ s1 ◂ s2 ◂ (take x, iff::intro (H1 ◂ x) (H2 ◂ x))
+theorem subset::antisym {A : Type} {s1 s2 : Set A} (H1 : s1 ⊆ s2) (H2 : s2 ⊆ s1) : s1 = s2
+:= subset::ext (have (∀ x, x ∈ s1 = x ∈ s2) :
+ λ x, have x ∈ s1 = x ∈ s2 :
+ iff::intro (have x ∈ s1 → x ∈ s2 : H1 x)
+ (have x ∈ s2 → x ∈ s1 : H2 x))
diff --git a/examples/lean/tactic_in_lua.lean b/examples/lean/tactic_in_lua.lean
index e2f86d5a1..165844870 100644
--- a/examples/lean/tactic_in_lua.lean
+++ b/examples/lean/tactic_in_lua.lean
@@ -64,8 +64,8 @@
-- Now, the tactic conj_in_lua can be used when proving theorems in Lean.
*)
-theorem T (a b : Bool) : a => b => a /\ b := _.
- (* Then(Repeat(OrElse(imp_tac(), conj_in_lua)), assumption_tac()) *)
+theorem T (a b : Bool) : a -> b -> a /\ b := _.
+ (* Then(conj_in_lua, assumption_tac()) *)
done
-- print proof created using our script
diff --git a/src/builtin/Nat.lean b/src/builtin/Nat.lean
index a54161f17..bfb1963ff 100644
--- a/src/builtin/Nat.lean
+++ b/src/builtin/Nat.lean
@@ -36,28 +36,24 @@ axiom add::zeror (a : Nat) : a + 0 = a
axiom add::succr (a b : Nat) : a + (b + 1) = (a + b) + 1
axiom mul::zeror (a : Nat) : a * 0 = 0
axiom mul::succr (a b : Nat) : a * (b + 1) = a * b + a
-axiom le::def (a b : Nat) : a ≤ b ⇔ ∃ c, a + c = b
-axiom induction {P : Nat → Bool} (a : Nat) (H1 : P 0) (H2 : Π (n : Nat) (iH : P n), P (n + 1)) : P a
+axiom le::def (a b : Nat) : a ≤ b = ∃ c, a + c = b
+axiom induction {P : Nat → Bool} (a : Nat) (H1 : P 0) (H2 : ∀ (n : Nat) (iH : P n), P (n + 1)) : P a
-theorem pred::nz' (a : Nat) : a ≠ 0 ⇒ ∃ b, b + 1 = a
+theorem pred::nz {a : Nat} : a ≠ 0 → ∃ b, b + 1 = a
:= induction a
- (assume H : 0 ≠ 0, false::elim (∃ b, b + 1 = 0) H)
- (λ (n : Nat) (iH : n ≠ 0 ⇒ ∃ b, b + 1 = n),
- assume H : n + 1 ≠ 0,
- or::elim (em (n = 0))
- (λ Heq0 : n = 0, exists::intro 0 (calc 0 + 1 = n + 1 : { symm Heq0 }))
- (λ Hne0 : n ≠ 0,
- obtain (w : Nat) (Hw : w + 1 = n), from (iH ◂ Hne0),
- exists::intro (w + 1) (calc w + 1 + 1 = n + 1 : { Hw })))
+ (λ H : 0 ≠ 0, false::elim (∃ b, b + 1 = 0) H)
+ (λ (n : Nat) (iH : n ≠ 0 → ∃ b, b + 1 = n) (H : n + 1 ≠ 0),
+ or::elim (em (n = 0))
+ (λ Heq0 : n = 0, exists::intro 0 (calc 0 + 1 = n + 1 : { symm Heq0 }))
+ (λ Hne0 : n ≠ 0,
+ obtain (w : Nat) (Hw : w + 1 = n), from (iH Hne0),
+ exists::intro (w + 1) (calc w + 1 + 1 = n + 1 : { Hw })))
-theorem pred::nz {a : Nat} (H : a ≠ 0) : ∃ b, b + 1 = a
-:= (pred::nz' a) ◂ H
-
-theorem discriminate {B : Bool} {a : Nat} (H1: a = 0 → B) (H2 : Π n, a = n + 1 → B) : B
+theorem discriminate {B : Bool} {a : Nat} (H1: a = 0 → B) (H2 : ∀ n, a = n + 1 → B) : B
:= or::elim (em (a = 0))
(λ Heq0 : a = 0, H1 Heq0)
(λ Hne0 : a ≠ 0, obtain (w : Nat) (Hw : w + 1 = a), from (pred::nz Hne0),
- H2 w (symm Hw))
+ H2 w (symm Hw))
theorem add::zerol (a : Nat) : 0 + a = a
:= induction a
@@ -174,27 +170,23 @@ theorem mul::assoc (a b c : Nat) : a * (b * c) = a * b * c
... = (n * b + b) * c : symm (distributel (n * b) b c)
... = (n + 1) * b * c : { symm (mul::succl n b) })
-theorem add::inj' (a b c : Nat) : a + b = a + c ⇒ b = c
+theorem add::inj {a b c : Nat} : a + b = a + c → b = c
:= induction a
- (assume H : 0 + b = 0 + c,
+ (λ H : 0 + b = 0 + c,
calc b = 0 + b : symm (add::zerol b)
... = 0 + c : H
... = c : add::zerol c)
- (λ (n : Nat) (iH : n + b = n + c ⇒ b = c),
- assume H : n + 1 + b = n + 1 + c,
- let L1 : n + b + 1 = n + c + 1
- := (calc n + b + 1 = n + (b + 1) : symm (add::assoc n b 1)
- ... = n + (1 + b) : { add::comm b 1 }
- ... = n + 1 + b : add::assoc n 1 b
- ... = n + 1 + c : H
- ... = n + (1 + c) : symm (add::assoc n 1 c)
- ... = n + (c + 1) : { add::comm 1 c }
- ... = n + c + 1 : add::assoc n c 1),
- L2 : n + b = n + c := succ::inj L1
- in iH ◂ L2)
-
-theorem add::inj {a b c : Nat} (H : a + b = a + c) : b = c
-:= (add::inj' a b c) ◂ H
+ (λ (n : Nat) (iH : n + b = n + c → b = c) (H : n + 1 + b = n + 1 + c),
+ let L1 : n + b + 1 = n + c + 1
+ := (calc n + b + 1 = n + (b + 1) : symm (add::assoc n b 1)
+ ... = n + (1 + b) : { add::comm b 1 }
+ ... = n + 1 + b : add::assoc n 1 b
+ ... = n + 1 + c : H
+ ... = n + (1 + c) : symm (add::assoc n 1 c)
+ ... = n + (c + 1) : { add::comm 1 c }
+ ... = n + c + 1 : add::assoc n c 1),
+ L2 : n + b = n + c := succ::inj L1
+ in iH L2)
theorem add::eqz {a b : Nat} (H : a + b = 0) : a = 0
:= discriminate
@@ -217,6 +209,7 @@ theorem le::refl (a : Nat) : a ≤ a := le::intro (add::zeror a)
theorem le::zero (a : Nat) : 0 ≤ a := le::intro (add::zerol a)
+
theorem le::trans {a b c : Nat} (H1 : a ≤ b) (H2 : b ≤ c) : a ≤ c
:= obtain (w1 : Nat) (Hw1 : a + w1 = b), from (le::elim H1),
obtain (w2 : Nat) (Hw2 : b + w2 = c), from (le::elim H2),
diff --git a/src/builtin/cast.lean b/src/builtin/cast.lean
index 8bc01e02f..1510e6f83 100644
--- a/src/builtin/cast.lean
+++ b/src/builtin/cast.lean
@@ -9,16 +9,16 @@ axiom cast::eq {A B : (Type U)} (H : A == B) (x : A) : x == cast H x.
-- The CastApp axiom "propagates" the cast over application
axiom cast::app {A A' : (Type U)} {B : A → (Type U)} {B' : A' → (Type U)}
- (H1 : (Π x : A, B x) == (Π x : A', B' x)) (H2 : A == A')
- (f : Π x : A, B x) (x : A) :
+ (H1 : (∀ x : A, B x) == (∀ x : A', B' x)) (H2 : A == A')
+ (f : ∀ x : A, B x) (x : A) :
cast H1 f (cast H2 x) == f x.
-- If two (dependent) function spaces are equal, then their domains are equal.
axiom dominj {A A' : (Type U)} {B : A → (Type U)} {B' : A' → (Type U)}
- (H : (Π x : A, B x) == (Π x : A', B' x)) :
+ (H : (∀ x : A, B x) == (∀ x : A', B' x)) :
A == A'.
-- If two (dependent) function spaces are equal, then their ranges are equal.
axiom raninj {A A' : (Type U)} {B : A → (Type U)} {B' : A' → (Type U)}
- (H : (Π x : A, B x) == (Π x : A', B' x)) (a : A) :
+ (H : (∀ x : A, B x) == (∀ x : A', B' x)) (a : A) :
B a == B' (cast (dominj H) a).
diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean
index 72ccbd2e1..6a4ca392e 100644
--- a/src/builtin/kernel.lean
+++ b/src/builtin/kernel.lean
@@ -12,47 +12,30 @@ builtin if {A : (Type U)} : Bool → A → A → A
definition TypeU := (Type U)
definition TypeM := (Type M)
-definition implies (a b : Bool) : Bool
-:= if a b true
-
-infixr 25 => : implies
-infixr 25 ⇒ : implies
-
-definition iff (a b : Bool) : Bool
-:= a == b
-
-infixr 25 <=> : iff
-infixr 25 ⇔ : iff
-
definition not (a : Bool) : Bool
-:= if a false true
+:= a → false
notation 40 ¬ _ : not
definition or (a b : Bool) : Bool
-:= ¬ a ⇒ b
+:= ¬ a → b
infixr 30 || : or
infixr 30 \/ : or
infixr 30 ∨ : or
definition and (a b : Bool) : Bool
-:= ¬ (a ⇒ ¬ b)
+:= ¬ (a → ¬ b)
+
+definition implies (a b : Bool) : Bool
+:= a → b
infixr 35 && : and
infixr 35 /\ : and
infixr 35 ∧ : and
--- Forall is a macro for the identifier forall, we use that
--- because the Lean parser has the builtin syntax sugar:
--- forall x : T, P x
--- for
--- (forall T (fun x : T, P x))
-definition Forall (A : TypeU) (P : A → Bool) : Bool
-:= P == (λ x : A, true)
-
definition Exists (A : TypeU) (P : A → Bool) : Bool
-:= ¬ (Forall A (λ x : A, ¬ (P x)))
+:= ¬ (∀ x : A, ¬ (P x))
definition eq {A : TypeU} (a b : A) : Bool
:= a == b
@@ -64,13 +47,6 @@ definition neq {A : TypeU} (a b : A) : Bool
infix 50 ≠ : neq
-axiom mp {a b : Bool} (H1 : a ⇒ b) (H2 : a) : b
-
-infixl 100 <| : mp
-infixl 100 ◂ : mp
-
-axiom discharge {a b : Bool} (H : a → b) : a ⇒ b
-
axiom case (P : Bool → Bool) (H1 : P true) (H2 : P false) (a : Bool) : P a
axiom refl {A : TypeU} (a : A) : a == a
@@ -80,11 +56,13 @@ axiom subst {A : TypeU} {a b : A} {P : A → Bool} (H1 : P a) (H2 : a == b) : P
definition substp {A : TypeU} {a b : A} (P : A → Bool) (H1 : P a) (H2 : a == b) : P b
:= subst H1 H2
-axiom eta {A : TypeU} {B : A → TypeU} (f : Π x : A, B x) : (λ x : A, f x) == f
+axiom eta {A : TypeU} {B : A → TypeU} (f : ∀ x : A, B x) : (λ x : A, f x) == f
-axiom iff::intro {a b : Bool} (H1 : a ⇒ b) (H2 : b ⇒ a) : iff a b
+axiom iff::intro {a b : Bool} (H1 : a → b) (H2 : b → a) : a == b
-axiom abst {A : TypeU} {B : A → TypeU} {f g : Π x : A, B x} (H : Π x : A, f x == g x) : f == g
+axiom abst {A : TypeU} {B : A → TypeU} {f g : ∀ x : A, B x} (H : ∀ x : A, f x == g x) : f == g
+
+axiom abstpi {A : TypeU} {B C : A → TypeU} (H : ∀ x : A, B x == C x) : (∀ x : A, B x) == (∀ x : A, C x)
axiom hsymm {A B : TypeU} {a : A} {b : B} (H : a == b) : b == a
@@ -100,24 +78,24 @@ theorem false::elim (a : Bool) (H : false) : a
:= case (λ x, x) trivial H a
theorem absurd {a : Bool} (H1 : a) (H2 : ¬ a) : false
-:= H2 ◂ H1
+:= H2 H1
-theorem eq::mp {a b : Bool} (H1 : a == b) (H2 : a) : b
+theorem eqmp {a b : Bool} (H1 : a == b) (H2 : a) : b
:= subst H2 H1
-infixl 100 <| : eq::mp
-infixl 100 ◂ : eq::mp
+infixl 100 <| : eqmp
+infixl 100 ◂ : eqmp
-- assume is a 'macro' that expands into a discharge
-theorem imp::trans {a b c : Bool} (H1 : a ⇒ b) (H2 : b ⇒ c) : a ⇒ c
-:= assume Ha, H2 ◂ (H1 ◂ Ha)
+theorem imp::trans {a b c : Bool} (H1 : a → b) (H2 : b → c) : a → c
+:= λ Ha, H2 (H1 Ha)
-theorem imp::eq::trans {a b c : Bool} (H1 : a ⇒ b) (H2 : b == c) : a ⇒ c
-:= assume Ha, H2 ◂ (H1 ◂ Ha)
+theorem imp::eq::trans {a b c : Bool} (H1 : a → b) (H2 : b == c) : a → c
+:= λ Ha, H2 ◂ (H1 Ha)
-theorem eq::imp::trans {a b c : Bool} (H1 : a == b) (H2 : b ⇒ c) : a ⇒ c
-:= assume Ha, H2 ◂ (H1 ◂ Ha)
+theorem eq::imp::trans {a b c : Bool} (H1 : a == b) (H2 : b → c) : a → c
+:= λ Ha, H2 (H1 ◂ Ha)
theorem not::not::eq (a : Bool) : (¬ ¬ a) == a
:= case (λ x, (¬ ¬ x) == x) trivial trivial a
@@ -125,32 +103,32 @@ theorem not::not::eq (a : Bool) : (¬ ¬ a) == a
theorem not::not::elim {a : Bool} (H : ¬ ¬ a) : a
:= (not::not::eq a) ◂ H
-theorem mt {a b : Bool} (H1 : a ⇒ b) (H2 : ¬ b) : ¬ a
-:= assume H : a, absurd (H1 ◂ H) H2
+theorem mt {a b : Bool} (H1 : a → b) (H2 : ¬ b) : ¬ a
+:= λ Ha, absurd (H1 Ha) H2
-theorem contrapos {a b : Bool} (H : a ⇒ b) : ¬ b ⇒ ¬ a
-:= assume H1 : ¬ b, mt H H1
+theorem contrapos {a b : Bool} (H : a → b) : ¬ b → ¬ a
+:= λ Hnb : ¬ b, mt H Hnb
theorem absurd::elim {a : Bool} (b : Bool) (H1 : a) (H2 : ¬ a) : b
:= false::elim b (absurd H1 H2)
-theorem not::imp::eliml {a b : Bool} (H : ¬ (a ⇒ b)) : a
+theorem not::imp::eliml {a b : Bool} (Hnab : ¬ (a → b)) : a
:= not::not::elim
(have ¬ ¬ a :
- assume H1 : ¬ a, absurd (have a ⇒ b : assume H2 : a, absurd::elim b H2 H1)
- (have ¬ (a ⇒ b) : H))
+ λ Hna : ¬ a, absurd (have a → b : λ Ha : a, absurd::elim b Ha Hna)
+ Hnab)
-theorem not::imp::elimr {a b : Bool} (H : ¬ (a ⇒ b)) : ¬ b
-:= assume H1 : b, absurd (have a ⇒ b : assume H2 : a, H1)
- (have ¬ (a ⇒ b) : H)
+theorem not::imp::elimr {a b : Bool} (H : ¬ (a → b)) : ¬ b
+:= λ Hb : b, absurd (have a → b : λ Ha : a, Hb)
+ (have ¬ (a → b) : H)
theorem resolve1 {a b : Bool} (H1 : a ∨ b) (H2 : ¬ a) : b
-:= H1 ◂ H2
+:= H1 H2
--- Remark: conjunction is defined as ¬ (a ⇒ ¬ b) in Lean
+-- Remark: conjunction is defined as ¬ (a → ¬ b) in Lean
theorem and::intro {a b : Bool} (H1 : a) (H2 : b) : a ∧ b
-:= assume H : a ⇒ ¬ b, absurd H2 (H ◂ H1)
+:= λ H : a → ¬ b, absurd H2 (H H1)
theorem and::eliml {a b : Bool} (H : a ∧ b) : a
:= not::imp::eliml H
@@ -158,18 +136,18 @@ theorem and::eliml {a b : Bool} (H : a ∧ b) : a
theorem and::elimr {a b : Bool} (H : a ∧ b) : b
:= not::not::elim (not::imp::elimr H)
--- Remark: disjunction is defined as ¬ a ⇒ b in Lean
+-- Remark: disjunction is defined as ¬ a → b in Lean
theorem or::introl {a : Bool} (H : a) (b : Bool) : a ∨ b
-:= assume H1 : ¬ a, absurd::elim b H H1
+:= λ H1 : ¬ a, absurd::elim b H H1
theorem or::intror {b : Bool} (a : Bool) (H : b) : a ∨ b
-:= assume H1 : ¬ a, H
+:= λ H1 : ¬ a, H
theorem or::elim {a b c : Bool} (H1 : a ∨ b) (H2 : a → c) (H3 : b → c) : c
:= not::not::elim
- (assume H : ¬ c,
- absurd (have c : H3 (have b : resolve1 H1 (have ¬ a : (mt (assume Ha : a, H2 Ha) H))))
+ (λ H : ¬ c,
+ absurd (have c : H3 (have b : resolve1 H1 (have ¬ a : (mt (λ Ha : a, H2 Ha) H))))
H)
theorem refute {a : Bool} (H : ¬ a → false) : a
@@ -184,7 +162,7 @@ theorem trans {A : TypeU} {a b c : A} (H1 : a == b) (H2 : b == c) : a == c
infixl 100 ⋈ : trans
theorem ne::symm {A : TypeU} {a b : A} (H : a ≠ b) : b ≠ a
-:= assume H1 : b = a, H ◂ (symm H1)
+:= λ H1 : b = a, H (symm H1)
theorem eq::ne::trans {A : TypeU} {a b c : A} (H1 : a = b) (H2 : b ≠ c) : a ≠ c
:= subst H2 (symm H1)
@@ -196,76 +174,61 @@ theorem eqt::elim {a : Bool} (H : a == true) : a
:= (symm H) ◂ trivial
theorem eqt::intro {a : Bool} (H : a) : a == true
-:= iff::intro (assume H1 : a, trivial)
- (assume H2 : true, H)
+:= iff::intro (λ H1 : a, trivial)
+ (λ H2 : true, H)
-theorem congr1 {A : TypeU} {B : A → TypeU} {f g : Π x : A, B x} (a : A) (H : f == g) : f a == g a
-:= substp (fun h : (Π x : A, B x), f a == h a) (refl (f a)) H
+theorem congr1 {A : TypeU} {B : A → TypeU} {f g : ∀ x : A, B x} (a : A) (H : f == g) : f a == g a
+:= substp (fun h : (∀ x : A, B x), f a == h a) (refl (f a)) H
-- Remark: we must use heterogeneous equality in the following theorem because the types of (f a) and (f b)
-- are not "definitionally equal" They are (B a) and (B b)
-- They are provably equal, we just have to apply Congr1
-theorem congr2 {A : TypeU} {B : A → TypeU} {a b : A} (f : Π x : A, B x) (H : a == b) : f a == f b
+theorem congr2 {A : TypeU} {B : A → TypeU} {a b : A} (f : ∀ x : A, B x) (H : a == b) : f a == f b
:= substp (fun x : A, f a == f x) (refl (f a)) H
-- Remark: like the previous theorem we use heterogeneous equality We cannot use Trans theorem
-- because the types are not definitionally equal
-theorem congr {A : TypeU} {B : A → TypeU} {f g : Π x : A, B x} {a b : A} (H1 : f == g) (H2 : a == b) : f a == g b
+theorem congr {A : TypeU} {B : A → TypeU} {f g : ∀ x : A, B x} {a b : A} (H1 : f == g) (H2 : a == b) : f a == g b
:= htrans (congr2 f H2) (congr1 b H1)
-theorem forall::elim {A : TypeU} {P : A → Bool} (H : Forall A P) (a : A) : P a
-:= eqt::elim (congr1 a H)
-
-infixl 100 <| : forall::elim
-infixl 100 ◂ : forall::elim
-
-theorem forall::intro {A : TypeU} {P : A → Bool} (H : Π x : A, P x) : Forall A P
-:= (symm (eta P)) ⋈ (abst (λ x, eqt::intro (H x)))
-
-- Remark: the existential is defined as (¬ (forall x : A, ¬ P x))
-theorem exists::elim {A : TypeU} {P : A → Bool} {B : Bool} (H1 : Exists A P) (H2 : Π (a : A) (H : P a), B) : B
+theorem exists::elim {A : TypeU} {P : A → Bool} {B : Bool} (H1 : Exists A P) (H2 : ∀ (a : A) (H : P a), B) : B
:= refute (λ R : ¬ B,
- absurd (forall::intro (λ a : A, mt (assume H : P a, H2 a H) R))
+ absurd (λ a : A, mt (λ H : P a, H2 a H) R)
H1)
theorem exists::intro {A : TypeU} {P : A → Bool} (a : A) (H : P a) : Exists A P
-:= assume H1 : (∀ x : A, ¬ P x),
- absurd H (forall::elim H1 a)
+:= λ H1 : (∀ x : A, ¬ P x),
+ absurd H (H1 a)
-- At this point, we have proved the theorems we need using the
-- definitions of forall, exists, and, or, =>, not We mark (some of)
-- them as opaque Opaque definitions improve performance, and
-- effectiveness of Lean's elaborator
-set::opaque implies true
-set::opaque not true
-set::opaque or true
-set::opaque and true
-set::opaque forall true
-
theorem or::comm (a b : Bool) : (a ∨ b) == (b ∨ a)
-:= iff::intro (assume H, or::elim H (λ H1, or::intror b H1) (λ H2, or::introl H2 a))
- (assume H, or::elim H (λ H1, or::intror a H1) (λ H2, or::introl H2 b))
+:= iff::intro (λ H, or::elim H (λ H1, or::intror b H1) (λ H2, or::introl H2 a))
+ (λ H, or::elim H (λ H1, or::intror a H1) (λ H2, or::introl H2 b))
theorem or::assoc (a b c : Bool) : ((a ∨ b) ∨ c) == (a ∨ (b ∨ c))
-:= iff::intro (assume H : (a ∨ b) ∨ c,
+:= iff::intro (λ H : (a ∨ b) ∨ c,
or::elim H (λ H1 : a ∨ b, or::elim H1 (λ Ha : a, or::introl Ha (b ∨ c)) (λ Hb : b, or::intror a (or::introl Hb c)))
(λ Hc : c, or::intror a (or::intror b Hc)))
- (assume H : a ∨ (b ∨ c),
+ (λ H : a ∨ (b ∨ c),
or::elim H (λ Ha : a, (or::introl (or::introl Ha b) c))
(λ H1 : b ∨ c, or::elim H1 (λ Hb : b, or::introl (or::intror a Hb) c)
(λ Hc : c, or::intror (a ∨ b) Hc)))
theorem or::id (a : Bool) : (a ∨ a) == a
-:= iff::intro (assume H, or::elim H (λ H1, H1) (λ H2, H2))
- (assume H, or::introl H a)
+:= iff::intro (λ H, or::elim H (λ H1, H1) (λ H2, H2))
+ (λ H, or::introl H a)
theorem or::falsel (a : Bool) : (a ∨ false) == a
-:= iff::intro (assume H, or::elim H (λ H1, H1) (λ H2, false::elim a H2))
- (assume H, or::introl H false)
+:= iff::intro (λ H, or::elim H (λ H1, H1) (λ H2, false::elim a H2))
+ (λ H, or::introl H false)
theorem or::falser (a : Bool) : (false ∨ a) == a
:= (or::comm false a) ⋈ (or::falsel a)
@@ -280,34 +243,34 @@ theorem or::tauto (a : Bool) : (a ∨ ¬ a) == true
:= eqt::intro (em a)
theorem and::comm (a b : Bool) : (a ∧ b) == (b ∧ a)
-:= iff::intro (assume H, and::intro (and::elimr H) (and::eliml H))
- (assume H, and::intro (and::elimr H) (and::eliml H))
+:= iff::intro (λ H, and::intro (and::elimr H) (and::eliml H))
+ (λ H, and::intro (and::elimr H) (and::eliml H))
theorem and::id (a : Bool) : (a ∧ a) == a
-:= iff::intro (assume H, and::eliml H)
- (assume H, and::intro H H)
+:= iff::intro (λ H, and::eliml H)
+ (λ H, and::intro H H)
theorem and::assoc (a b c : Bool) : ((a ∧ b) ∧ c) == (a ∧ (b ∧ c))
-:= iff::intro (assume H, and::intro (and::eliml (and::eliml H)) (and::intro (and::elimr (and::eliml H)) (and::elimr H)))
- (assume H, and::intro (and::intro (and::eliml H) (and::eliml (and::elimr H))) (and::elimr (and::elimr H)))
+:= iff::intro (λ H, and::intro (and::eliml (and::eliml H)) (and::intro (and::elimr (and::eliml H)) (and::elimr H)))
+ (λ H, and::intro (and::intro (and::eliml H) (and::eliml (and::elimr H))) (and::elimr (and::elimr H)))
theorem and::truer (a : Bool) : (a ∧ true) == a
-:= iff::intro (assume H : a ∧ true, and::eliml H)
- (assume H : a, and::intro H trivial)
+:= iff::intro (λ H : a ∧ true, and::eliml H)
+ (λ H : a, and::intro H trivial)
theorem and::truel (a : Bool) : (true ∧ a) == a
:= trans (and::comm true a) (and::truer a)
theorem and::falsel (a : Bool) : (a ∧ false) == false
-:= iff::intro (assume H, and::elimr H)
- (assume H, false::elim (a ∧ false) H)
+:= iff::intro (λ H, and::elimr H)
+ (λ H, false::elim (a ∧ false) H)
theorem and::falser (a : Bool) : (false ∧ a) == false
:= (and::comm false a) ⋈ (and::falsel a)
theorem and::absurd (a : Bool) : (a ∧ ¬ a) == false
-:= iff::intro (assume H, absurd (and::eliml H) (and::elimr H))
- (assume H, false::elim (a ∧ ¬ a) H)
+:= iff::intro (λ H, absurd (and::eliml H) (and::elimr H))
+ (λ H, false::elim (a ∧ ¬ a) H)
theorem not::true : (¬ true) == false
:= trivial
@@ -342,27 +305,28 @@ theorem not::iff (a b : Bool) : (¬ (a == b)) == ((¬ a) == b)
theorem not::iff::elim {a b : Bool} (H : ¬ (a == b)) : (¬ a) == b
:= (not::iff a b) ◂ H
-theorem not::implies (a b : Bool) : (¬ (a ⇒ b)) == (a ∧ ¬ b)
-:= case (λ x, (¬ (x ⇒ b)) == (x ∧ ¬ b))
- (case (λ y, (¬ (true ⇒ y)) == (true ∧ ¬ y)) trivial trivial b)
- (case (λ y, (¬ (false ⇒ y)) == (false ∧ ¬ y)) trivial trivial b)
+theorem not::implies (a b : Bool) : (¬ (a → b)) == (a ∧ ¬ b)
+:= case (λ x, (¬ (x → b)) == (x ∧ ¬ b))
+ (case (λ y, (¬ (true → y)) == (true ∧ ¬ y)) trivial trivial b)
+ (case (λ y, (¬ (false → y)) == (false ∧ ¬ y)) trivial trivial b)
a
-theorem not::implies::elim {a b : Bool} (H : ¬ (a ⇒ b)) : a ∧ ¬ b
+theorem not::implies::elim {a b : Bool} (H : ¬ (a → b)) : a ∧ ¬ b
:= (not::implies a b) ◂ H
theorem not::congr {a b : Bool} (H : a == b) : (¬ a) == (¬ b)
:= congr2 not H
-theorem eq::forall::intro {A : (Type U)} {P Q : A → Bool} (H : Pi x : A, P x == Q x) : (∀ x : A, P x) == (∀ x : A, Q x)
-:= congr2 (Forall A) (abst H)
-
-theorem eq::exists::intro {A : (Type U)} {P Q : A → Bool} (H : Pi x : A, P x == Q x) : (∃ x : A, P x) == (∃ x : A, Q x)
+theorem eq::exists::intro {A : (Type U)} {P Q : A → Bool} (H : ∀ x : A, P x == Q x) : (∃ x : A, P x) == (∃ x : A, Q x)
:= congr2 (Exists A) (abst H)
theorem not::forall (A : (Type U)) (P : A → Bool) : (¬ (∀ x : A, P x)) == (∃ x : A, ¬ P x)
-:= calc (¬ ∀ x : A, P x) = (¬ ∀ x : A, ¬ ¬ P x) : not::congr (eq::forall::intro (λ x : A, (symm (not::not::eq (P x)))))
- ... = (∃ x : A, ¬ P x) : refl (∃ x : A, ¬ P x)
+:= let
+ l1 : ∀ x : A, P x == ¬ ¬ P x := λ x : A, symm (not::not::eq (P x)),
+ l2 : (∀ x : A, P x) == (∀ x : A, ¬ ¬ P x) := abstpi l1,
+ s1 : (¬ ∀ x : A, P x) == (¬ ∀ x : A, ¬ ¬ P x) := not::congr l2,
+ s2 : (¬ ∀ x : A, ¬ ¬ P x) == (∃ x : A, ¬ P x) := refl (∃ x : A, ¬ P x)
+ in trans s1 s2
theorem not::forall::elim {A : (Type U)} {P : A → Bool} (H : ¬ (∀ x : A, P x)) : ∃ x : A, ¬ P x
:= (not::forall A P) ◂ H
@@ -390,7 +354,10 @@ theorem exists::unfold2 {A : TypeU} {P : A → Bool} (a : A) (H : P a ∨ (∃ x
exists::intro w (and::elimr Hw)))
theorem exists::unfold {A : TypeU} (P : A → Bool) (a : A) : (∃ x : A, P x) = (P a ∨ (∃ x : A, x ≠ a ∧ P x))
-:= iff::intro (assume H : (∃ x : A, P x), exists::unfold1 a H)
- (assume H : (P a ∨ (∃ x : A, x ≠ a ∧ P x)), exists::unfold2 a H)
+:= iff::intro (λ H : (∃ x : A, P x), exists::unfold1 a H)
+ (λ H : (P a ∨ (∃ x : A, x ≠ a ∧ P x)), exists::unfold2 a H)
-set::opaque exists true
+set::opaque exists true
+set::opaque not true
+set::opaque or true
+set::opaque and true
diff --git a/src/builtin/obj/Nat.olean b/src/builtin/obj/Nat.olean
index 97e51328a..c5df55a1e 100644
Binary files a/src/builtin/obj/Nat.olean and b/src/builtin/obj/Nat.olean differ
diff --git a/src/builtin/obj/kernel.olean b/src/builtin/obj/kernel.olean
index 5fc347ce9..0474c65b8 100644
Binary files a/src/builtin/obj/kernel.olean and b/src/builtin/obj/kernel.olean differ
diff --git a/src/frontends/lean/parser_cmds.cpp b/src/frontends/lean/parser_cmds.cpp
index 8b185b1cb..8a615cda9 100644
--- a/src/frontends/lean/parser_cmds.cpp
+++ b/src/frontends/lean/parser_cmds.cpp
@@ -529,9 +529,7 @@ void parser_imp::parse_set_option() {
void parser_imp::parse_set_opaque() {
next();
name id;
- if (curr() == scanner::token::Forall) {
- id = "forall";
- } else if (curr() == scanner::token::Exists) {
+ if (curr() == scanner::token::Exists) {
id = "exists";
} else {
check_identifier("invalid set opaque, identifier expected");
diff --git a/src/frontends/lean/parser_expr.cpp b/src/frontends/lean/parser_expr.cpp
index 9a7fcfa06..4c376c2f4 100644
--- a/src/frontends/lean/parser_expr.cpp
+++ b/src/frontends/lean/parser_expr.cpp
@@ -730,37 +730,24 @@ expr parser_imp::parse_pi() {
return parse_abstraction(false);
}
-/** \brief Parse forall/exists */
-expr parser_imp::parse_quantifier(bool is_forall) {
+/** \brief Parse exists */
+expr parser_imp::parse_exists() {
next();
mk_scope scope(*this);
parameter_buffer parameters;
parse_expr_parameters(parameters);
- check_comma_next("invalid quantifier, ',' expected");
+ check_comma_next("invalid exists, ',' expected");
expr result = parse_expr();
unsigned i = parameters.size();
while (i > 0) {
--i;
pos_info p = parameters[i].m_pos;
expr lambda = save(mk_lambda(parameters[i].m_name, parameters[i].m_type, result), p);
- if (is_forall)
- result = save(mk_forall(parameters[i].m_type, lambda), p);
- else
- result = save(mk_exists(parameters[i].m_type, lambda), p);
+ result = save(mk_exists(parameters[i].m_type, lambda), p);
}
return result;
}
-/** \brief Parse 'forall' parameters ',' expr. */
-expr parser_imp::parse_forall() {
- return parse_quantifier(true);
-}
-
-/** \brief Parse 'exists' parameters ',' expr. */
-expr parser_imp::parse_exists() {
- return parse_quantifier(false);
-}
-
/** \brief Parse Let expression. */
expr parser_imp::parse_let() {
next();
@@ -931,7 +918,6 @@ expr parser_imp::parse_nud() {
case scanner::token::LeftParen: return parse_lparen();
case scanner::token::Lambda: return parse_lambda();
case scanner::token::Pi: return parse_pi();
- case scanner::token::Forall: return parse_forall();
case scanner::token::Exists: return parse_exists();
case scanner::token::Let: return parse_let();
case scanner::token::IntVal: return parse_nat_int();
diff --git a/src/frontends/lean/parser_imp.h b/src/frontends/lean/parser_imp.h
index 2a98c1624..19aaa88e2 100644
--- a/src/frontends/lean/parser_imp.h
+++ b/src/frontends/lean/parser_imp.h
@@ -299,8 +299,6 @@ private:
expr parse_abstraction(bool is_lambda);
expr parse_lambda();
expr parse_pi();
- expr parse_quantifier(bool is_forall);
- expr parse_forall();
expr parse_exists();
expr parse_let();
expr parse_type(bool level_expected);
diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index 4ead0ef7c..f27846cb7 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -66,14 +66,12 @@ namespace lean {
static format g_Type_fmt = highlight_builtin(format("Type"));
static format g_eq_fmt = format("==");
static format g_lambda_n_fmt = highlight_keyword(format("\u03BB"));
-static format g_Pi_n_fmt = highlight_keyword(format("\u03A0"));
+static format g_Pi_n_fmt = highlight_keyword(format("\u2200"));
static format g_lambda_fmt = highlight_keyword(format("fun"));
-static format g_Pi_fmt = highlight_keyword(format("Pi"));
+static format g_Pi_fmt = highlight_keyword(format("forall"));
static format g_arrow_n_fmt = highlight_keyword(format("\u2192"));
static format g_arrow_fmt = highlight_keyword(format("->"));
-static format g_forall_n_fmt = highlight_keyword(format("\u2200"));
static format g_exists_n_fmt = highlight_keyword(format("\u2203"));
-static format g_forall_fmt = highlight_keyword(format("forall"));
static format g_exists_fmt = highlight_keyword(format("exists"));
static format g_ellipsis_n_fmt= highlight(format("\u2026"));
static format g_ellipsis_fmt = highlight(format("..."));
@@ -263,9 +261,6 @@ class pp_fn {
name const & n = const_name(e);
if (is_placeholder(e)) {
return mk_result(format("_"), 1);
- } else if (is_forall_fn(e)) {
- // use alias when forall is used as a function symbol
- return mk_result(format("Forall"), 1);
} else if (is_exists_fn(e)) {
// use alias when exists is used as a function symbol
return mk_result(format("Exists"), 1);
@@ -320,61 +315,50 @@ class pp_fn {
return pp_child_with_paren(e, depth);
}
- bool is_forall_expr(expr const & e) {
- return is_app(e) && arg(e, 0) == mk_forall_fn() && num_args(e) == 3;
- }
-
bool is_exists_expr(expr const & e) {
return is_app(e) && arg(e, 0) == mk_exists_fn() && num_args(e) == 3;
}
- bool is_quant_expr(expr const & e, bool is_forall) {
- return is_forall ? is_forall_expr(e) : is_exists_expr(e);
- }
-
/**
\brief Collect nested quantifiers, and instantiate
variables with unused names. Store in \c r the selected names
and associated domains. Return the body of the sequence of
nested quantifiers.
*/
- expr collect_nested_quantifiers(expr const & e, bool is_forall, buffer> & r) {
- lean_assert(is_quant_expr(e, is_forall));
+ expr collect_nested_quantifiers(expr const & e, buffer> & r) {
+ lean_assert(is_exists_expr(e));
if (is_lambda(arg(e, 2))) {
expr lambda = arg(e, 2);
name n1 = get_unused_name(lambda);
m_local_names.insert(n1);
r.emplace_back(n1, abst_domain(lambda));
expr b = replace_var_with_name(abst_body(lambda), n1);
- if (is_quant_expr(b, is_forall))
- return collect_nested_quantifiers(b, is_forall, r);
+ if (is_exists_expr(b))
+ return collect_nested_quantifiers(b, r);
else
return b;
} else {
// Quantifier is not in normal form. That is, it might be
- // (forall t p) or (exists t p) where p is not a lambda
+ // (exists t p) where p is not a lambda
// abstraction
// So, we put it in normal form
- // (forall t (fun x : t, p x))
- // or
// (exists t (fun x : t, p x))
expr new_body = mk_lambda("x", arg(e, 1), mk_app(lift_free_vars(arg(e, 2), 1), mk_var(0)));
expr normal_form = mk_app(arg(e, 0), arg(e, 1), new_body);
- return collect_nested_quantifiers(normal_form, is_forall, r);
+ return collect_nested_quantifiers(normal_form, r);
}
}
- /** \brief Auxiliary function for pretty printing exists and
- forall formulas */
- result pp_quantifier(expr const & e, unsigned depth, bool is_forall) {
+ /** \brief Auxiliary function for pretty printing exists formulas */
+ result pp_exists(expr const & e, unsigned depth) {
buffer> nested;
local_names::mk_scope mk(m_local_names);
- expr b = collect_nested_quantifiers(e, is_forall, nested);
+ expr b = collect_nested_quantifiers(e, nested);
format head;
if (m_unicode)
- head = is_forall ? g_forall_n_fmt : g_exists_n_fmt;
+ head = g_exists_n_fmt;
else
- head = is_forall ? g_forall_fmt : g_exists_fmt;
+ head = g_exists_fmt;
format sep = comma();
expr domain0 = nested[0].second;
// TODO(Leo): the following code is very similar to pp_abstraction
@@ -416,14 +400,6 @@ class pp_fn {
}
}
- result pp_forall(expr const & e, unsigned depth) {
- return pp_quantifier(e, depth, true);
- }
-
- result pp_exists(expr const & e, unsigned depth) {
- return pp_quantifier(e, depth, false);
- }
-
operator_info find_op_for(expr const & e) const {
if (is_constant(e) && m_local_names.find(const_name(e)) != m_local_names.end())
return operator_info();
@@ -463,7 +439,7 @@ class pp_fn {
return g_eq_precedence;
} else if (is_arrow(e)) {
return g_arrow_precedence;
- } else if (is_lambda(e) || is_pi(e) || is_let(e) || is_forall(e) || is_exists(e)) {
+ } else if (is_lambda(e) || is_pi(e) || is_let(e) || is_exists(e)) {
return 0;
} else {
return g_app_precedence;
@@ -723,15 +699,13 @@ class pp_fn {
return mk_result(group(r_format), r_weight);
}}
lean_unreachable(); // LCOV_EXCL_LINE
- } else if (m_notation && is_forall_expr(e)) {
- return pp_forall(e, depth);
} else if (m_notation && is_exists_expr(e)) {
return pp_exists(e, depth);
} else {
// standard function application
expr const & f = app.get_function();
result p;
- bool is_const = is_constant(f) && !is_forall_fn(f) && !is_exists_fn(f);
+ bool is_const = is_constant(f) && !is_exists_fn(f);
if (is_const)
p = mk_result(format(const_name(f)), 1);
else if (is_choice(f))
diff --git a/src/frontends/lean/scanner.cpp b/src/frontends/lean/scanner.cpp
index 556e1def9..838c78741 100644
--- a/src/frontends/lean/scanner.cpp
+++ b/src/frontends/lean/scanner.cpp
@@ -14,18 +14,15 @@ Author: Leonardo de Moura
namespace lean {
static name g_lambda_unicode("\u03BB");
-static name g_pi_unicode("\u03A0");
+static name g_pi_unicode("\u2200");
static name g_arrow_unicode("\u2192");
static name g_lambda_name("fun");
static name g_type_name("Type");
-static name g_pi_name("Pi");
+static name g_pi_name("forall");
static name g_let_name("let");
static name g_in_name("in");
static name g_arrow_name("->");
static name g_eq_name("==");
-static name g_forall_name("forall");
-static name g_Forall_name("Forall");
-static name g_forall_unicode("\u2200");
static name g_exists_name("exists");
static name g_Exists_name("Exists");
static name g_exists_unicode("\u2203");
@@ -200,8 +197,6 @@ scanner::token scanner::read_a_symbol() {
return token::Lambda;
} else if (m_name_val == g_pi_name) {
return token::Pi;
- } else if (m_name_val == g_forall_name) {
- return token::Forall;
} else if (m_name_val == g_exists_name) {
return token::Exists;
} else if (m_name_val == g_type_name) {
@@ -216,9 +211,6 @@ scanner::token scanner::read_a_symbol() {
return token::Have;
} else if (m_name_val == g_by_name) {
return token::By;
- } else if (m_name_val == g_Forall_name) {
- m_name_val = g_forall_name;
- return token::Id;
} else if (m_name_val == g_Exists_name) {
m_name_val = g_exists_name;
return token::Id;
@@ -269,8 +261,6 @@ scanner::token scanner::read_c_symbol() {
return token::Lambda;
else if (m_name_val == g_pi_unicode)
return token::Pi;
- else if (m_name_val == g_forall_unicode)
- return token::Forall;
else if (m_name_val == g_exists_unicode)
return token::Exists;
else
@@ -445,7 +435,6 @@ std::ostream & operator<<(std::ostream & out, scanner::token const & t) {
case scanner::token::Period: out << "."; break;
case scanner::token::Lambda: out << g_lambda_unicode; break;
case scanner::token::Pi: out << g_pi_unicode; break;
- case scanner::token::Forall: out << g_forall_unicode; break;
case scanner::token::Exists: out << g_exists_unicode; break;
case scanner::token::Arrow: out << g_arrow_unicode; break;
case scanner::token::Let: out << "let"; break;
diff --git a/src/frontends/lean/scanner.h b/src/frontends/lean/scanner.h
index 9b6216d78..9a8ffbf84 100644
--- a/src/frontends/lean/scanner.h
+++ b/src/frontends/lean/scanner.h
@@ -20,7 +20,7 @@ class scanner {
public:
enum class token {
LeftParen, RightParen, LeftCurlyBracket, RightCurlyBracket, Colon, Comma, Period, Lambda, Pi, Arrow,
- Let, In, Forall, Exists, Id, CommandId, IntVal, DecimalVal, StringVal, Eq, Assign, Type, Placeholder,
+ Let, In, Exists, Id, CommandId, IntVal, DecimalVal, StringVal, Eq, Assign, Type, Placeholder,
Have, By, ScriptBlock, Ellipsis, Eof
};
protected:
diff --git a/src/kernel/builtin.cpp b/src/kernel/builtin.cpp
index 629e59b69..0e79d06f1 100644
--- a/src/kernel/builtin.cpp
+++ b/src/kernel/builtin.cpp
@@ -147,7 +147,7 @@ MK_CONSTANT(double_neg_elim_fn, name({"doubleneg", "elim"}));
MK_CONSTANT(mt_fn, name("mt"));
MK_CONSTANT(contrapos_fn, name("contrapos"));
MK_CONSTANT(absurd_elim_fn, name({"absurd", "elim"}));
-MK_CONSTANT(eq_mp_fn, name({"eq", "mp"}));
+MK_CONSTANT(eq_mp_fn, name("eqmp"));
MK_CONSTANT(not_imp1_fn, name({"not", "imp", "eliml"}));
MK_CONSTANT(not_imp2_fn, name({"not", "imp", "elimr"}));
MK_CONSTANT(conj_fn, name({"and", "intro"}));
diff --git a/src/kernel/expr.h b/src/kernel/expr.h
index 560cda622..ddcfcbd8f 100644
--- a/src/kernel/expr.h
+++ b/src/kernel/expr.h
@@ -637,6 +637,9 @@ template expr update_abst(expr const & e, F f) {
return e;
}
}
+inline expr update_abst(expr const & e, expr const & new_d, expr const & new_b) {
+ return update_abst(e, [&](expr const &, expr const &) { return mk_pair(new_d, new_b); });
+}
template expr update_let(expr const & e, F f) {
static_assert(std::is_same const &, expr const &, expr const &)>::type,
std::tuple, expr, expr>>::value,
diff --git a/src/kernel/normalizer.cpp b/src/kernel/normalizer.cpp
index 355fc5d25..4ca30d523 100644
--- a/src/kernel/normalizer.cpp
+++ b/src/kernel/normalizer.cpp
@@ -155,12 +155,10 @@ class normalizer::imp {
if (is_abstraction(e)) {
freset reset(m_cache);
flet set(m_ctx, ctx);
- return update_abst(e, [&](expr const & d, expr const & b) {
- expr new_d = reify(normalize(d, s, k), k);
- m_cache.clear(); // make sure we do not reuse cached values from the previous call
- expr new_b = reify(normalize(b, extend(s, mk_var(k)), k+1), k+1);
- return mk_pair(new_d, new_b);
- });
+ expr new_d = reify(normalize(abst_domain(e), s, k), k);
+ m_cache.clear(); // make sure we do not reuse cached values from the previous call
+ expr new_b = reify(normalize(abst_body(e), extend(s, mk_var(k)), k+1), k+1);
+ return update_abst(e, new_d, new_b);
} else {
lean_assert(is_metavar(e));
// We use the following trick to reify a metavariable in the context of the value_stack s, and context ctx.
@@ -234,7 +232,22 @@ class normalizer::imp {
expr r;
switch (a.kind()) {
- case expr_kind::MetaVar: case expr_kind::Pi: case expr_kind::Lambda:
+ case expr_kind::Pi: {
+ if (is_arrow(a)) {
+ expr new_d = reify(normalize(abst_domain(a), s, k), k);
+ if (is_bool_value(new_d)) {
+ m_cache.clear();
+ expr new_b = reify(normalize(abst_body(a), extend(s, mk_var(k)), k+1), k+1);
+ if (is_bool_value(new_b)) {
+ r = mk_bool_value(is_false(new_d) || is_true(new_b));
+ break;
+ }
+ }
+ }
+ r = mk_closure(a, m_ctx, s);
+ break;
+ }
+ case expr_kind::MetaVar: case expr_kind::Lambda:
r = mk_closure(a, m_ctx, s);
break;
case expr_kind::Var:
diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp
index d6770f985..743d69830 100644
--- a/src/kernel/type_checker.cpp
+++ b/src/kernel/type_checker.cpp
@@ -41,25 +41,19 @@ class type_checker::imp {
expr normalize(expr const & e, context const & ctx, bool unfold_opaque) { return m_normalizer(e, ctx, m_menv.to_some_menv(), unfold_opaque); }
expr check_type(expr const & e, expr const & s, context const & ctx) {
- if (is_type(e))
+ if (is_type(e) || is_bool(e))
return e;
- if (is_bool(e))
- return Type();
expr u = normalize(e, ctx, false);
- if (is_type(u))
+ if (is_type(u) || is_bool(u))
return u;
- if (is_bool(u))
- return Type();
if (has_metavar(u) && m_menv && m_uc) {
justification jst = mk_type_expected_justification(ctx, s);
m_uc->push_back(mk_convertible_constraint(ctx, e, TypeU, jst));
return u;
}
u = normalize(e, ctx, true);
- if (is_type(u))
+ if (is_type(u) || is_bool(u))
return u;
- if (is_bool(u))
- return Type();
throw type_expected_exception(env(), ctx, s);
}
@@ -265,19 +259,23 @@ class type_checker::imp {
}
case expr_kind::Pi: {
expr t1 = check_type(infer_type_core(abst_domain(e), ctx), abst_domain(e), ctx);
- optional t2;
+ if (is_bool(t1))
+ t1 = Type();
+ expr t2;
context new_ctx = extend(ctx, abst_name(e), abst_domain(e));
{
freset reset(m_cache);
t2 = check_type(infer_type_core(abst_body(e), new_ctx), abst_body(e), new_ctx);
}
- if (is_type(t1) && is_type(*t2)) {
- return save_result(e, mk_type(max(ty_level(t1), ty_level(*t2))), shared);
+ if (is_bool(t2))
+ return t2;
+ if (is_type(t1) && is_type(t2)) {
+ return save_result(e, mk_type(max(ty_level(t1), ty_level(t2))), shared);
} else {
lean_assert(m_uc);
justification jst = mk_max_type_justification(ctx, e);
expr r = m_menv->mk_metavar(ctx);
- m_uc->push_back(mk_max_constraint(new_ctx, lift_free_vars(t1, 0, 1), *t2, r, jst));
+ m_uc->push_back(mk_max_constraint(new_ctx, lift_free_vars(t1, 0, 1), t2, r, jst));
return save_result(e, r, shared);
}
}
diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp
index 8cfeb660c..43dd68765 100644
--- a/src/library/elaborator/elaborator.cpp
+++ b/src/library/elaborator/elaborator.cpp
@@ -1487,6 +1487,11 @@ class elaborator::imp {
push_active(mk_max_constraint(get_context(c), new_lhs1, new_lhs2, new_rhs, new_jst));
return true;
}
+ if (is_bool(lhs2)) {
+ justification new_jst(new normalize_justification(c));
+ push_new_eq_constraint(get_context(c), lhs2, rhs, new_jst);
+ return true;
+ }
if (!is_metavar(lhs1) && !is_type(lhs1)) {
new_lhs1 = normalize(get_context(c), lhs1);
modified = (lhs1 != new_lhs1);
diff --git a/src/tests/frontends/lean/parser.cpp b/src/tests/frontends/lean/parser.cpp
index 75071c945..8f9d2fcc2 100644
--- a/src/tests/frontends/lean/parser.cpp
+++ b/src/tests/frontends/lean/parser.cpp
@@ -44,13 +44,13 @@ static void parse_error(environment const & env, io_state const & ios, char cons
static void tst1() {
environment env; io_state ios = init_test_frontend(env);
- parse(env, ios, "variable x : Bool variable y : Bool axiom H : x && y || x => x");
+ parse(env, ios, "variable x : Bool variable y : Bool axiom H : x && y || x -> x");
parse(env, ios, "eval true && true");
parse(env, ios, "print true && false eval true && false");
parse(env, ios, "infixl 35 & : and print true & false & false eval true & false");
parse(env, ios, "notation 100 if _ then _ fi : implies print if true then false fi");
- parse(env, ios, "print Pi (A : Type), A -> A");
- parse(env, ios, "check Pi (A : Type), A -> A");
+ parse(env, ios, "print forall (A : Type), A -> A");
+ parse(env, ios, "check forall (A : Type), A -> A");
}
static void check(environment const & env, io_state & ios, char const * str, expr const & expected) {
@@ -73,11 +73,11 @@ static void tst2() {
check(env, ios, "x && y || z", Or(And(x, y), z));
check(env, ios, "x || y && z", Or(x, And(y, z)));
check(env, ios, "x || y || x && z", Or(x, Or(y, And(x, z))));
- check(env, ios, "x || y || x && z => x && y", Implies(Or(x, Or(y, And(x, z))), And(x, y)));
- check(env, ios, "x ∨ y ∨ x ∧ z ⇒ x ∧ y", Implies(Or(x, Or(y, And(x, z))), And(x, y)));
- check(env, ios, "x⇒y⇒z⇒x", Implies(x, Implies(y, Implies(z, x))));
- check(env, ios, "x=>y=>z=>x", Implies(x, Implies(y, Implies(z, x))));
- check(env, ios, "x=>(y=>z)=>x", Implies(x, Implies(Implies(y, z), x)));
+ check(env, ios, "x || y || x && z -> x && y", mk_arrow(Or(x, Or(y, And(x, z))), And(x, y)));
+ check(env, ios, "x ∨ y ∨ x ∧ z → x ∧ y", mk_arrow(Or(x, Or(y, And(x, z))), And(x, y)));
+ check(env, ios, "x→y→z→x", mk_arrow(x, mk_arrow(y, mk_arrow(z, x))));
+ check(env, ios, "x->y->z->x", mk_arrow(x, mk_arrow(y, mk_arrow(z, x))));
+ check(env, ios, "x->(y->z)->x", mk_arrow(x, mk_arrow(mk_arrow(y, z), x)));
}
static void tst3() {
diff --git a/src/tests/frontends/lean/scanner.cpp b/src/tests/frontends/lean/scanner.cpp
index d2b080bfe..b8f4bf381 100644
--- a/src/tests/frontends/lean/scanner.cpp
+++ b/src/tests/frontends/lean/scanner.cpp
@@ -69,7 +69,7 @@ static void check_name(char const * str, name const & expected) {
}
static void tst1() {
- scan("fun(x: Pi A : Type, A -> A), x+1 = 2.0 λ");
+ scan("fun(x: forall A : Type, A -> A), x+1 = 2.0 λ");
}
static void tst2() {
@@ -87,7 +87,7 @@ static void tst2() {
check("x := 10", {st::Id, st::Assign, st::IntVal});
check("(x+1):Int", {st::LeftParen, st::Id, st::Id, st::IntVal, st::RightParen, st::Colon, st::Id});
check("{x}", {st::LeftCurlyBracket, st::Id, st::RightCurlyBracket});
- check("\u03BB \u03A0 \u2192", {st::Lambda, st::Pi, st::Arrow});
+ check("\u03BB \u2200 \u2192", {st::Lambda, st::Pi, st::Arrow});
scan("++\u2295++x\u2296\u2296");
check("++\u2295++x\u2296\u2296", {st::Id, st::Id, st::Id, st::Id, st::Id});
scan("x10 ... == (* print('hello') *) have by");
diff --git a/src/tests/kernel/type_checker.cpp b/src/tests/kernel/type_checker.cpp
index ebb2bbdbe..fe31fe4d4 100644
--- a/src/tests/kernel/type_checker.cpp
+++ b/src/tests/kernel/type_checker.cpp
@@ -108,9 +108,6 @@ static void tst5() {
pr = Conj(P, prop, H, pr);
prop = And(P, prop);
}
- expr impPr = Discharge(P, prop, Fun({H, P}, pr));
- expr prop2 = type_check(impPr, env);
- lean_assert(Implies(P, prop) == prop2);
}
static void tst6() {
diff --git a/src/tests/library/tactic/tactic.cpp b/src/tests/library/tactic/tactic.cpp
index 1b4eb3999..4ddecc58c 100644
--- a/src/tests/library/tactic/tactic.cpp
+++ b/src/tests/library/tactic/tactic.cpp
@@ -114,40 +114,8 @@ static void tst1() {
std::cout << "done\n";
}
-static void tst2() {
- environment env;
- io_state io(options(), mk_simple_formatter());
- init_test_frontend(env);
- env->add_var("p", Bool);
- env->add_var("q", Bool);
- env->add_var("r", Bool);
- env->add_var("s", Bool);
- expr p = Const("p");
- expr q = Const("q");
- expr r = Const("r");
- expr s = Const("s");
- context ctx;
- ctx = extend(ctx, "H1", p);
- ctx = extend(ctx, "H2", q);
- std::cout << "proof: " << (repeat(conj_tactic()) << assumption_tactic()).solve(env, io, ctx, And(And(p, q), And(p, p))).get_proof()
- << "\n";
- std::cout << "-------------\n";
- // Theorem to be proved
- expr F = Implies(And(p, And(r, s)), Implies(q, And(And(p, q), And(r, p))));
- // Tactic
- tactic T = append(id_tactic() << assumption_tactic(),
- repeat(conj_tactic() || conj_hyp_tactic() || imp_tactic()) << trace_state_tactic() << assumption_tactic());
- // Generate proof using tactic
- expr pr = T.solve(env, io, context(), F).get_proof();
- // Print proof
- std::cout << pr << "\n";
- // Check whether the proof is correct or not.
- std::cout << env->type_check(pr) << "\n";
-}
-
int main() {
save_stack_info();
tst1();
- tst2();
return has_violations() ? 1 : 0;
}
diff --git a/tests/lean/apply_tac1.lean b/tests/lean/apply_tac1.lean
index 467e3f229..5dd4d6a96 100644
--- a/tests/lean/apply_tac1.lean
+++ b/tests/lean/apply_tac1.lean
@@ -4,22 +4,21 @@ 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 discharge.
+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(imp_tac(), assumption_tac(), apply_tac("Ax2"), apply_tac("Ax1")))
+simple_tac = Repeat(OrElse(assumption_tac(), apply_tac("Ax2"), apply_tac("Ax1")))
*)
-theorem T2 (a : Int) : (P a a) => (f a a).
+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 (apply discharge) exact (apply Ax2) (apply Ax1)).
+theorem T3 (a : Int) : (P a a) → (f a a).
+ Repeat (OrElse exact (apply Ax2) (apply Ax1)).
done.
print environment 2.
\ No newline at end of file
diff --git a/tests/lean/apply_tac1.lean.expected.out b/tests/lean/apply_tac1.lean.expected.out
index 4aa254fdf..53a553d64 100644
--- a/tests/lean/apply_tac1.lean.expected.out
+++ b/tests/lean/apply_tac1.lean.expected.out
@@ -10,5 +10,5 @@
Assumed: Ax2
Proved: T2
Proved: T3
-theorem T2 (a : ℤ) : P a a ⇒ f a a := discharge (λ H : P a a, Ax1 a a H)
-theorem T3 (a : ℤ) : P a a ⇒ f a a := discharge (λ H : P a a, Ax1 a a H)
+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
diff --git a/tests/lean/apply_tac2.lean b/tests/lean/apply_tac2.lean
index 32ab828b0..0681a9c9d 100644
--- a/tests/lean/apply_tac2.lean
+++ b/tests/lean/apply_tac2.lean
@@ -1,8 +1,4 @@
(* import("tactic.lua") *)
-check @discharge
-theorem T (a b : Bool) : a => b => b => a.
- apply discharge.
- apply discharge.
- apply discharge.
+theorem T (a b : Bool) : a → b → b → a.
exact.
done.
\ No newline at end of file
diff --git a/tests/lean/apply_tac2.lean.expected.out b/tests/lean/apply_tac2.lean.expected.out
index 08e2efc27..ed7015541 100644
--- a/tests/lean/apply_tac2.lean.expected.out
+++ b/tests/lean/apply_tac2.lean.expected.out
@@ -1,4 +1,3 @@
Set: pp::colors
Set: pp::unicode
-@discharge : Π (a b : Bool), (a → b) → (a ⇒ b)
Proved: T
diff --git a/tests/lean/bad1.lean b/tests/lean/bad1.lean
index 56070772a..9e61e4f84 100644
--- a/tests/lean/bad1.lean
+++ b/tests/lean/bad1.lean
@@ -1,4 +1,4 @@
import Int.
-variable g : Pi A : Type, A -> A.
+variable g : forall A : Type, A -> A.
variables a b : Int
axiom H1 : g _ a > 0
diff --git a/tests/lean/bad9.lean.expected.out b/tests/lean/bad9.lean.expected.out
index 3c9fee4c2..6f73ca340 100644
--- a/tests/lean/bad9.lean.expected.out
+++ b/tests/lean/bad9.lean.expected.out
@@ -5,4 +5,4 @@
Assumed: N
λ (a : N) (f : N → N) (H : f a == a),
let calc1 : f a == a := @substp N (f a) a (λ x : N, f a == x) (@refl N (f a)) H in calc1 :
- Π (a : N) (f : N → N), f a == a → f a == a
+ ∀ (a : N) (f : N → N), f a == a → f a == a
diff --git a/tests/lean/calc1.lean b/tests/lean/calc1.lean
index 2f9412341..b439bfadb 100644
--- a/tests/lean/calc1.lean
+++ b/tests/lean/calc1.lean
@@ -1,13 +1,15 @@
import tactic.
-variables a b c d e : Bool.
-axiom H1 : a => b.
-axiom H2 : b = c.
-axiom H3 : c => d.
-axiom H4 : d <=> e.
+infixl 50 => : implies
-theorem T : a => e
+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 : (by apply H3)
- ... <=> e : H4.
+ ... => d : H3
+ ... = e : H4.
diff --git a/tests/lean/cast1.lean.expected.out b/tests/lean/cast1.lean.expected.out
index 7a2e8fd61..ea66abcba 100644
--- a/tests/lean/cast1.lean.expected.out
+++ b/tests/lean/cast1.lean.expected.out
@@ -11,7 +11,7 @@
Error (line: 13, pos: 7) type mismatch at application
f m v1
Function type:
- Π (n : ℕ), vector ℤ n → ℤ
+ ∀ (n : ℕ), vector ℤ n → ℤ
Arguments types:
m : ℕ
v1 : vector ℤ (m + 0)
diff --git a/tests/lean/cast4.lean b/tests/lean/cast4.lean
index c92bedf88..92a2dbc6e 100644
--- a/tests/lean/cast4.lean
+++ b/tests/lean/cast4.lean
@@ -4,21 +4,21 @@ set::option pp::colors false
check fun (A A': TypeM)
(B : A -> TypeM)
(B' : A' -> TypeM)
- (f : Pi x : A, B x)
- (g : Pi x : A', B' x)
+ (f : forall x : A, B x)
+ (g : forall x : A', B' x)
(a : A)
(b : A')
- (H1 : (Pi x : A, B x) == (Pi x : A', B' x))
+ (H1 : (forall x : A, B x) == (forall x : A', B' x))
(H2 : f == g)
(H3 : a == b),
let
- S1 : (Pi x : A', B' x) == (Pi x : A, B x) := symm H1,
+ S1 : (forall x : A', B' x) == (forall x : A, B x) := symm H1,
L2 : A' == A := dominj S1,
b' : A := cast L2 b,
L3 : b == b' := cast::eq L2 b,
L4 : a == b' := htrans H3 L3,
L5 : f a == f b' := congr2 f L4,
- g' : (Pi x : A, B x) := cast S1 g,
+ g' : (forall x : A, B x) := cast S1 g,
L6 : g == g' := cast::eq S1 g,
L7 : f == g' := htrans H2 L6,
L8 : f b' == g' b' := congr1 b' L7,
diff --git a/tests/lean/cast4.lean.expected.out b/tests/lean/cast4.lean.expected.out
index f76e10055..3ac2e07f2 100644
--- a/tests/lean/cast4.lean.expected.out
+++ b/tests/lean/cast4.lean.expected.out
@@ -5,25 +5,31 @@
λ (A A' : TypeM)
(B : A → TypeM)
(B' : A' → TypeM)
- (f : Π x : A, B x)
- (g : Π x : A', B' x)
+ (f : ∀ x : A, B x)
+ (g : ∀ x : A', B' x)
(a : A)
(b : A')
- (H1 : (Π x : A, B x) == (Π x : A', B' x))
+ (H1 : (∀ x : A, B x) == (∀ x : A', B' x))
(H2 : f == g)
(H3 : a == b),
- let S1 : (Π x : A', B' x) == (Π x : A, B x) := symm H1,
+ let S1 : (∀ x : A', B' x) == (∀ x : A, B x) := symm H1,
L2 : A' == A := dominj S1,
b' : A := cast L2 b,
L3 : b == b' := cast::eq L2 b,
L4 : a == b' := htrans H3 L3,
L5 : f a == f b' := congr2 f L4,
- g' : Π x : A, B x := cast S1 g,
+ g' : ∀ x : A, B x := cast S1 g,
L6 : g == g' := cast::eq S1 g,
L7 : f == g' := htrans H2 L6,
L8 : f b' == g' b' := congr1 b' L7,
L9 : f a == g' b' := htrans L5 L8,
L10 : g' b' == g b := cast::app S1 L2 g b
in htrans L9 L10 :
- Π (A A' : TypeM) (B : A → TypeM) (B' : A' → TypeM) (f : Π x : A, B x) (g : Π x : A', B' x) (a : A) (b : A'),
- (Π x : A, B x) == (Π x : A', B' x) → f == g → a == b → f a == g b
+ ∀ (A A' : TypeM)
+ (B : A → TypeM)
+ (B' : A' → TypeM)
+ (f : ∀ x : A, B x)
+ (g : ∀ x : A', B' x)
+ (a : A)
+ (b : A'),
+ (∀ x : A, B x) == (∀ x : A', B' x) → f == g → a == b → f a == g b
diff --git a/tests/lean/coercion1.lean b/tests/lean/coercion1.lean
index 6814fbeb5..e03ca9014 100644
--- a/tests/lean/coercion1.lean
+++ b/tests/lean/coercion1.lean
@@ -5,7 +5,7 @@ coercion f
print environment 2
variable g : T -> R
coercion g
-variable h : Pi (x : Type), x
+variable h : forall (x : Type), x
coercion h
definition T2 : Type := T
definition R2 : Type := R
diff --git a/tests/lean/conv.lean.expected.out b/tests/lean/conv.lean.expected.out
index dda57cc03..3b849dc79 100644
--- a/tests/lean/conv.lean.expected.out
+++ b/tests/lean/conv.lean.expected.out
@@ -12,7 +12,7 @@ p f : Bool
g a : Bool
Defined: c2
Assumed: b
-@c2 : Π (T : Type), (Type 3) → T → (Type 3)
+@c2 : ∀ (T : Type), (Type 3) → T → (Type 3)
Assumed: g2
g2 : c2 (Type 2) b → Bool
Assumed: a2
diff --git a/tests/lean/discharge.lean b/tests/lean/discharge.lean
index 69e6baca4..f709cf7c9 100644
--- a/tests/lean/discharge.lean
+++ b/tests/lean/discharge.lean
@@ -1,8 +1,4 @@
import tactic
-check @discharge
-theorem T (a b : Bool) : a => b => b => a.
- apply discharge.
- apply discharge.
- apply discharge.
+theorem T (a b : Bool) : a → b → b → a.
exact.
done.
\ No newline at end of file
diff --git a/tests/lean/discharge.lean.expected.out b/tests/lean/discharge.lean.expected.out
index c61b7f7e9..7e7aa4182 100644
--- a/tests/lean/discharge.lean.expected.out
+++ b/tests/lean/discharge.lean.expected.out
@@ -1,5 +1,4 @@
Set: pp::colors
Set: pp::unicode
Imported 'tactic'
-@discharge : Π (a b : Bool), (a → b) → (a ⇒ b)
Proved: T
diff --git a/tests/lean/disj1.lean b/tests/lean/disj1.lean
index ba0fb3e83..a96174561 100644
--- a/tests/lean/disj1.lean
+++ b/tests/lean/disj1.lean
@@ -1,7 +1,6 @@
import tactic
-theorem T1 (a b : Bool) : a \/ b => b \/ a.
- apply discharge.
+theorem T1 (a b : Bool) : a \/ b → b \/ a.
(* disj_hyp_tac() *)
(* disj_tac() *)
back
@@ -11,10 +10,10 @@ theorem T1 (a b : Bool) : a \/ b => b \/ a.
done.
(*
-simple_tac = Repeat(OrElse(imp_tac(), assumption_tac(), disj_hyp_tac(), disj_tac())) .. now_tac()
+simple_tac = Repeat(OrElse(assumption_tac(), disj_hyp_tac(), disj_tac())) .. now_tac()
*)
-theorem T2 (a b : Bool) : a \/ b => b \/ a.
+theorem T2 (a b : Bool) : a \/ b → b \/ a.
simple_tac.
done.
diff --git a/tests/lean/disj1.lean.expected.out b/tests/lean/disj1.lean.expected.out
index e5ffd0e1d..aac263c31 100644
--- a/tests/lean/disj1.lean.expected.out
+++ b/tests/lean/disj1.lean.expected.out
@@ -3,5 +3,4 @@
Imported 'tactic'
Proved: T1
Proved: T2
-theorem T2 (a b : Bool) : a ∨ b ⇒ b ∨ a :=
- discharge (λ H : a ∨ b, or::elim H (λ H : a, or::intror b H) (λ H : b, or::introl H a))
+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)
diff --git a/tests/lean/disjcases.lean b/tests/lean/disjcases.lean
index 56b81a478..4cbe446dc 100644
--- a/tests/lean/disjcases.lean
+++ b/tests/lean/disjcases.lean
@@ -1,8 +1,7 @@
(* import("tactic.lua") *)
variables a b c : Bool
axiom H : a \/ b
-theorem T (a b : Bool) : a \/ b => b \/ a.
- apply discharge.
+theorem T (a b : Bool) : a \/ b → b \/ a.
apply (or::elim H).
apply or::intror.
exact.
diff --git a/tests/lean/elab1.lean b/tests/lean/elab1.lean
index a49b1b786..f36ff722b 100644
--- a/tests/lean/elab1.lean
+++ b/tests/lean/elab1.lean
@@ -4,24 +4,24 @@ check f 10 true
variable g {A B : Type} (a : A) : A.
check g 10
-variable h : Pi (A : Type), A -> A.
+variable h : forall (A : Type), A -> A.
check fun x, fun A : Type, h A x
-variable my_eq : Pi A : Type, A -> A -> Bool.
+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 := discharge (fun H1, and::intro H1 (and::eliml H)).
+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 :=
- discharge (λ H, or::elim (EM a)
- (λ H_a, H)
- (λ H_na, NotImp1 (MT H H_na)))
+theorem pierce (a b : Bool) : ((a -> b) -> a) -> a :=
+ λ H, or::elim (EM a)
+ (λ H_a, H)
+ (λ H_na, NotImp1 (MT H H_na))
diff --git a/tests/lean/elab1.lean.expected.out b/tests/lean/elab1.lean.expected.out
index 07e8341f4..dc491adac 100644
--- a/tests/lean/elab1.lean.expected.out
+++ b/tests/lean/elab1.lean.expected.out
@@ -33,7 +33,7 @@ A : Type, B : Type, a : ?M::0, b : ?M::1, C : Type ⊢ ?M::0[lift:0:3] ≺ C
Assumed: b
Assumed: H
Failed to solve
- ⊢ ?M::0 ⇒ ?M::3 ∧ a ≺ b
+ ⊢ ∀ H1 : ?M::0, ?M::1 ∧ a ≺ b
(line: 18: pos: 18) Type of definition 't1' must be convertible to expected type.
Failed to solve
⊢ b == b ≺ a == b
@@ -54,4 +54,4 @@ Failed to solve
?M::0
Bool
Bool
-Error (line: 25, pos: 31) unknown identifier 'EM'
+Error (line: 25, pos: 19) unknown identifier 'EM'
diff --git a/tests/lean/elab2.lean b/tests/lean/elab2.lean
index 0b4485a31..b0b1e2be5 100644
--- a/tests/lean/elab2.lean
+++ b/tests/lean/elab2.lean
@@ -1,23 +1,23 @@
-variable C : Pi (A B : Type) (H : A = B) (a : A), B
+variable C : forall (A B : Type) (H : A = B) (a : A), B
-variable D : Pi (A A' : Type) (B : A -> Type) (B' : A' -> Type) (H : (Pi x : A, B x) = (Pi x : A', B' x)), A = A'
+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 : Pi (A A' : Type) (B : A -> Type) (B' : A' -> Type) (H : (Pi x : A, B x) = (Pi 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 : Pi (A1 A2 B1 B2 : Type) (H : (A1 -> B1) = (A2 -> B2)) (a : A1), B1 = B2 :=
+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 : Pi (A1 A2 B1 B2 : Type) (H : (A1 -> B1) = (A2 -> B2)) (a : A1), B1 = B2 :=
+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 : Pi (A1 A2 B1 B2 : Type) (H : (A1 -> B1) = (A2 -> B2)) (a : A1), B1 = B2 :=
+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
diff --git a/tests/lean/elab3.lean b/tests/lean/elab3.lean
index 9eb0cd8e5..4d0a0a956 100644
--- a/tests/lean/elab3.lean
+++ b/tests/lean/elab3.lean
@@ -1,11 +1,11 @@
-variable C : Pi (A B : Type) (H : A = B) (a : A), B
+variable C : forall (A B : Type) (H : A = B) (a : A), B
-variable D : Pi (A A' : Type) (B : A -> Type) (B' : A' -> Type) (H : (Pi x : A, B x) = (Pi x : A', B' x)), A = A'
+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 : Pi (A A' : Type) (B : A -> Type) (B' : A' -> Type) (H : (Pi x : A, B x) = (Pi 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 : Pi (A1 A2 B1 B2 : Type) (H : (A1 -> B1) = (A2 -> B2)) (a : A1), B1 = B2 :=
+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
diff --git a/tests/lean/elab4.lean b/tests/lean/elab4.lean
index ae6fabcc7..7463c1337 100644
--- a/tests/lean/elab4.lean
+++ b/tests/lean/elab4.lean
@@ -1,11 +1,11 @@
variable C {A B : Type} (H : A = B) (a : A) : B
-variable D {A A' : Type} {B : A -> Type} {B' : A' -> Type} (H : (Pi x : A, B x) = (Pi x : A', B' x)) : A = A'
+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 : (Pi x : A, B x) = (Pi 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 : Pi (A1 A2 B1 B2 : Type) (H : (A1 -> B1) = (A2 -> B2)) (a : A1), B1 = B2 :=
+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
diff --git a/tests/lean/elab4.lean.expected.out b/tests/lean/elab4.lean.expected.out
index 9901889a8..144ace9e8 100644
--- a/tests/lean/elab4.lean.expected.out
+++ b/tests/lean/elab4.lean.expected.out
@@ -8,9 +8,13 @@
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)) :
+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) :
+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
diff --git a/tests/lean/elab5.lean b/tests/lean/elab5.lean
index 0768e3d40..2494e5028 100644
--- a/tests/lean/elab5.lean
+++ b/tests/lean/elab5.lean
@@ -1,11 +1,11 @@
variable C {A B : Type} (H : A = B) (a : A) : B
-variable D {A A' : Type} {B : A -> Type} {B' : A' -> Type} (H : (Pi x : A, B x) = (Pi x : A', B' x)) : A = A'
+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 : (Pi x : A, B x) = (Pi 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 : Pi (A1 A2 B1 B2 : Type), ((A1 -> B1) = (A2 -> B2)) -> A1 -> (B1 = B2) :=
+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
diff --git a/tests/lean/elab5.lean.expected.out b/tests/lean/elab5.lean.expected.out
index 9901889a8..144ace9e8 100644
--- a/tests/lean/elab5.lean.expected.out
+++ b/tests/lean/elab5.lean.expected.out
@@ -8,9 +8,13 @@
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)) :
+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) :
+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
diff --git a/tests/lean/elab7.lean b/tests/lean/elab7.lean
index 7a4281881..36a860fa7 100644
--- a/tests/lean/elab7.lean
+++ b/tests/lean/elab7.lean
@@ -2,7 +2,7 @@ variables A B C : (Type U)
variable P : A -> Bool
variable F1 : A -> B -> C
variable F2 : A -> B -> C
-variable H : Pi (a : A) (b : B), (F1 a b) == (F2 a b)
+variable H : forall (a : A) (b : B), (F1 a b) == (F2 a b)
variable a : A
check eta (F2 a)
check abst (fun a : A,
diff --git a/tests/lean/errmsg1.lean b/tests/lean/errmsg1.lean
index ce0c79e3c..c978ca343 100644
--- a/tests/lean/errmsg1.lean
+++ b/tests/lean/errmsg1.lean
@@ -2,7 +2,7 @@ eval fun x, x
print fun x, x
check fun x, x
-theorem T (A : Type) (x : A) : Pi (y : A), A
+theorem T (A : Type) (x : A) : forall (y : A), A
:= _.
theorem T (x : _) : x = x := refl x.
diff --git a/tests/lean/ex3.lean b/tests/lean/ex3.lean
index 726240b8a..9186daa05 100644
--- a/tests/lean/ex3.lean
+++ b/tests/lean/ex3.lean
@@ -1,4 +1,4 @@
-variable myeq : Pi (A : Type), A -> A -> Bool
+variable myeq : forall (A : Type), A -> A -> Bool
print myeq _ true false
variable T : Type
variable a : T
diff --git a/tests/lean/exists3.lean b/tests/lean/exists3.lean
index 77c98c645..22f6cbbb0 100644
--- a/tests/lean/exists3.lean
+++ b/tests/lean/exists3.lean
@@ -4,26 +4,22 @@ variable P : Int -> Int -> Bool
set::opaque exists false.
theorem T1 (R1 : not (exists x y, P x y)) : forall x y, not (P x y) :=
- forall::intro (fun a,
- forall::intro (fun b,
- forall::elim (not::not::elim (forall::elim (not::not::elim R1) a)) b))
+ fun a b,
+ not::not::elim (not::not::elim R1 a) b
axiom Ax : forall x, exists y, P x y
theorem T2 : exists x y, P x y :=
refute (fun R : not (exists x y, P x y),
- let L1 : forall x y, not (P x y) := forall::intro (fun a,
- forall::intro (fun b,
- forall::elim (not::not::elim (forall::elim (not::not::elim R) a)) b)),
- L2 : exists y, P 0 y := forall::elim Ax 0
+ let L1 : forall x y, not (P x y) := fun a b, (not::not::elim ((not::not::elim R) a)) b,
+ L2 : exists y, P 0 y := Ax 0
in exists::elim L2 (fun (w : Int) (H : P 0 w),
- absurd H (forall::elim (forall::elim L1 0) w))).
+ absurd H (L1 0 w))).
theorem T3 (A : (Type U)) (P : A -> A -> Bool) (a : A) (H1 : forall x, exists y, P x y) : exists x y, P x y :=
refute (fun R : not (exists x y, P x y),
- let L1 : forall x y, not (P x y) := forall::intro (fun a,
- forall::intro (fun b,
- forall::elim (not::not::elim (forall::elim (not::not::elim R) a)) b)),
- L2 : exists y, P a y := forall::elim H1 a
+ let L1 : forall x y, not (P x y) := fun a b,
+ (not::not::elim ((not::not::elim R) a)) b,
+ L2 : exists y, P a y := H1 a
in exists::elim L2 (fun (w : A) (H : P a w),
- absurd H (forall::elim (forall::elim L1 a) w))).
+ absurd H (L1 a w))).
diff --git a/tests/lean/exists6.lean b/tests/lean/exists6.lean
index e34270ba4..162520625 100644
--- a/tests/lean/exists6.lean
+++ b/tests/lean/exists6.lean
@@ -4,5 +4,5 @@ axiom Ax1 : exists x y z, P x y z
axiom Ax2 : forall x y z, not (P x y z)
theorem T : false :=
exists::elim Ax1 (fun a H1, exists::elim H1 (fun b H2, exists::elim H2 (fun (c : Int) (H3 : P a b c),
- let notH3 : not (P a b c) := forall::elim (forall::elim (forall::elim Ax2 a) b) c
+ let notH3 : not (P a b c) := Ax2 a b c
in absurd H3 notH3)))
diff --git a/tests/lean/exists7.lean b/tests/lean/exists7.lean
index 9de3711cb..fe6b0ba96 100644
--- a/tests/lean/exists7.lean
+++ b/tests/lean/exists7.lean
@@ -3,7 +3,6 @@ variable N : Type
variables a b c : N
variables P : N -> N -> N -> Bool
-set::opaque forall false.
set::opaque exists false.
set::opaque not false.
diff --git a/tests/lean/exists8.lean b/tests/lean/exists8.lean
index a31cf7c47..20cb0f461 100644
--- a/tests/lean/exists8.lean
+++ b/tests/lean/exists8.lean
@@ -2,26 +2,23 @@ import Int.
variable P : Int -> Int -> Bool
theorem T1 (R1 : not (exists x y, P x y)) : forall x y, not (P x y) :=
- forall::intro (fun a,
- forall::intro (fun b,
- forall::elim (not::exists::elim (forall::elim (not::exists::elim R1) a)) b))
+ fun a b,
+ (not::exists::elim (not::exists::elim R1 a)) b
axiom Ax : forall x, exists y, P x y
theorem T2 : exists x y, P x y :=
refute (fun R : not (exists x y, P x y),
- let L1 : forall x y, not (P x y) := forall::intro (fun a,
- forall::intro (fun b,
- forall::elim (not::exists::elim (forall::elim (not::exists::elim R) a)) b)),
- L2 : exists y, P 0 y := forall::elim Ax 0
+ let L1 : forall x y, not (P x y) := fun a b,
+ (not::exists::elim ((not::exists::elim R) a)) b,
+ L2 : exists y, P 0 y := Ax 0
in exists::elim L2 (fun (w : Int) (H : P 0 w),
- absurd H (forall::elim (forall::elim L1 0) w))).
+ absurd H (L1 0 w))).
theorem T3 (A : (Type U)) (P : A -> A -> Bool) (a : A) (H1 : forall x, exists y, P x y) : exists x y, P x y :=
refute (fun R : not (exists x y, P x y),
- let L1 : forall x y, not (P x y) := forall::intro (fun a,
- forall::intro (fun b,
- forall::elim (not::exists::elim (forall::elim (not::exists::elim R) a)) b)),
- L2 : exists y, P a y := forall::elim H1 a
+ let L1 : forall x y, not (P x y) := fun a b,
+ (not::exists::elim ((not::exists::elim R) a)) b,
+ L2 : exists y, P a y := H1 a
in exists::elim L2 (fun (w : A) (H : P a w),
- absurd H (forall::elim (forall::elim L1 a) w))).
+ absurd H ((L1 a) w))).
diff --git a/tests/lean/explicit.lean.expected.out b/tests/lean/explicit.lean.expected.out
index 56af01505..89041fe0d 100644
--- a/tests/lean/explicit.lean.expected.out
+++ b/tests/lean/explicit.lean.expected.out
@@ -3,10 +3,10 @@
Imported 'Int'
Assumed: f
Assumed: module::g
-@f : Π (A : Type), A → A → A
-module::@g : Π (A : Type), A → A → A
+@f : ∀ (A : Type), A → A → A
+module::@g : ∀ (A : Type), A → A → A
Assumed: h::1
-h::1::explicit : Π (A B : Type), A → B → A
+h::1::explicit : ∀ (A B : Type), A → B → A
Assumed: @h
Assumed: h
Error (line: 9, pos: 37) failed to mark implicit arguments for 'h', the frontend already has an object named '@h'
diff --git a/tests/lean/find.lean.expected.out b/tests/lean/find.lean.expected.out
index 2cdffce2d..36c97ed20 100644
--- a/tests/lean/find.lean.expected.out
+++ b/tests/lean/find.lean.expected.out
@@ -1,8 +1,8 @@
Set: pp::colors
Set: pp::unicode
Imported 'find'
-theorem congr1 {A : TypeU} {B : A → TypeU} {f g : Π x : A, B x} (a : A) (H : f == g) : f a == g a
-theorem congr2 {A : TypeU} {B : A → TypeU} {a b : A} (f : Π x : A, B x) (H : a == b) : f a == f b
-theorem congr {A : TypeU} {B : A → TypeU} {f g : Π x : A, B x} {a b : A} (H1 : f == g) (H2 : a == b) : f a == g b
+theorem congr1 {A : TypeU} {B : A → TypeU} {f g : ∀ x : A, B x} (a : A) (H : f == g) : f a == g a
+theorem congr2 {A : TypeU} {B : A → TypeU} {a b : A} (f : ∀ x : A, B x) (H : a == b) : f a == f b
+theorem congr {A : TypeU} {B : A → TypeU} {f g : ∀ x : A, B x} {a b : A} (H1 : f == g) (H2 : a == b) : f a == g b
Error (line: 3, pos: 0) executing external script (/home/leo/projects/lean/build/debug/shell/find.lua:24), no object name in the environment matches the regular expression 'foo'
Error (line: 4, pos: 0) executing external script (/home/leo/projects/lean/build/debug/shell/find.lua:18), unfinished capture
diff --git a/tests/lean/forall1.lean b/tests/lean/forall1.lean
index 8d6659565..ab5dd4a5a 100644
--- a/tests/lean/forall1.lean
+++ b/tests/lean/forall1.lean
@@ -1,4 +1,4 @@
import Int.
variable P : Int -> Bool
axiom Ax (x : Int) : P x
-check forall::intro Ax
\ No newline at end of file
+check Ax
\ No newline at end of file
diff --git a/tests/lean/forall1.lean.expected.out b/tests/lean/forall1.lean.expected.out
index 1bea43e06..bd1002ecc 100644
--- a/tests/lean/forall1.lean.expected.out
+++ b/tests/lean/forall1.lean.expected.out
@@ -3,4 +3,4 @@
Imported 'Int'
Assumed: P
Assumed: Ax
-forall::intro Ax : ∀ x : ℤ, P x
+Ax : ∀ x : ℤ, P x
diff --git a/tests/lean/implicit2.lean.expected.out b/tests/lean/implicit2.lean.expected.out
index 571070a1f..9964848de 100644
--- a/tests/lean/implicit2.lean.expected.out
+++ b/tests/lean/implicit2.lean.expected.out
@@ -4,7 +4,7 @@
Assumed: f
f 10 20 : ℕ
f 10 : ℕ → ℕ
-@f : Π (A : Type), A → A → A
+@f : ∀ (A : Type), A → A → A
Assumed: g
g 10 20 ⊤ : Bool → Bool
let r : ℝ → ℝ → ℝ := g 10 20 in r : ℝ → ℝ → ℝ
diff --git a/tests/lean/induction1.lean b/tests/lean/induction1.lean
index 8db848fc3..72aaa9501 100644
--- a/tests/lean/induction1.lean
+++ b/tests/lean/induction1.lean
@@ -1,34 +1,34 @@
-import macros -- loads the take, assume, obtain macros
+import macros -- loads the λ, λ, obtain macros
using Nat -- using the Nat namespace (it allows us to suppress the Nat:: prefix)
-axiom Induction : ∀ P : Nat → Bool, P 0 ⇒ (∀ n, P n ⇒ P (n + 1)) ⇒ ∀ n, P n.
+axiom Induction : ∀ P : Nat → Bool, P 0 → (∀ n, P n → P (n + 1)) → ∀ n, P n.
-- induction on n
theorem Comm1 : ∀ n m, n + m = m + n
:= Induction
- ◂ _ -- I use a placeholder because I do not want to write the P
- ◂ (take m, -- Base case
+ _ -- I use a placeholder because I do not want to write the P
+ (λ m, -- Base case
calc 0 + m = m : add::zerol m
... = m + 0 : symm (add::zeror m))
- ◂ (take n, -- Inductive case
- assume (iH : ∀ m, n + m = m + n),
- take m,
+ (λ n, -- Inductive case
+ λ (iH : ∀ m, n + m = m + n),
+ λ m,
calc n + 1 + m = (n + m) + 1 : add::succl n m
- ... = (m + n) + 1 : { iH ◂ m }
+ ... = (m + n) + 1 : { iH m }
... = m + (n + 1) : symm (add::succr m n))
-- indunction on m
theorem Comm2 : ∀ n m, n + m = m + n
-:= take n,
+:= λ n,
Induction
- ◂ _
- ◂ (calc n + 0 = n : add::zeror n
+ _
+ (calc n + 0 = n : add::zeror n
... = 0 + n : symm (add::zerol n))
- ◂ (take m,
- assume (iH : n + m = m + n),
+ (λ m,
+ λ (iH : n + m = m + n),
calc n + (m + 1) = (n + m) + 1 : add::succr n m
... = (m + n) + 1 : { iH }
... = (m + 1) + n : symm (add::succl m n))
diff --git a/tests/lean/induction1.lean.expected.out b/tests/lean/induction1.lean.expected.out
index 0106c05a2..f7532df89 100644
--- a/tests/lean/induction1.lean.expected.out
+++ b/tests/lean/induction1.lean.expected.out
@@ -6,11 +6,9 @@
Proved: Comm1
Proved: Comm2
theorem Comm2 : ∀ n m : ℕ, n + m = m + n :=
- forall::intro
- (λ n : ℕ,
- Induction ◂ (λ x : ℕ, n + x == x + n) ◂ (Nat::add::zeror n ⋈ symm (Nat::add::zerol n)) ◂
- forall::intro
- (λ m : ℕ,
- discharge
- (λ iH : n + m = m + n,
- Nat::add::succr n m ⋈ subst (refl (n + m + 1)) iH ⋈ symm (Nat::add::succl m n))))
+ λ n : ℕ,
+ Induction
+ (λ x : ℕ, n + x == x + n)
+ (Nat::add::zeror n ⋈ symm (Nat::add::zerol n))
+ (λ (m : ℕ) (iH : n + m = m + n),
+ Nat::add::succr n m ⋈ subst (refl (n + m + 1)) iH ⋈ symm (Nat::add::succl m n))
diff --git a/tests/lean/induction2.lean b/tests/lean/induction2.lean
index 2663f77f3..1febcba76 100644
--- a/tests/lean/induction2.lean
+++ b/tests/lean/induction2.lean
@@ -1,21 +1,18 @@
-import macros -- loads the take, assume, obtain macros
+import macros -- loads the λ, λ, obtain macros
using Nat -- using the Nat namespace (it allows us to suppress the Nat:: prefix)
-axiom Induction : ∀ P : Nat → Bool, P 0 ⇒ (∀ n, P n ⇒ P (n + 1)) ⇒ ∀ n, P n.
+axiom Induction : ∀ P : Nat → Bool, P 0 → (∀ n, P n → P (n + 1)) → ∀ n, P n.
-- induction on n
theorem Comm1 : ∀ n m, n + m = m + n
:= Induction
- ◂ _ -- I use a placeholder because I do not want to write the P
- ◂ (take m, -- Base case
+ _ -- I use a placeholder because I do not want to write the P
+ (λ m, -- Base case
calc 0 + m = m : add::zerol m
... = m + 0 : symm (add::zeror m))
- ◂ (take n, -- Inductive case
- assume iH,
- take m,
- calc n + 1 + m = (n + m) + 1 : add::succl n m
- ... = (m + n) + 1 : { iH } -- Error is here
- ... = m + (n + 1) : symm (add::succr m n))
-
+ (λ n iH m, -- Inductive case
+ calc n + 1 + m = (n + m) + 1 : add::succl n m
+ ... = (m + n) + 1 : { iH } -- Error is here
+ ... = m + (n + 1) : symm (add::succr m n))
diff --git a/tests/lean/induction2.lean.expected.out b/tests/lean/induction2.lean.expected.out
index a028dad8a..c16f7e28c 100644
--- a/tests/lean/induction2.lean.expected.out
+++ b/tests/lean/induction2.lean.expected.out
@@ -4,101 +4,11 @@
Using: Nat
Assumed: Induction
Failed to solve
- ⊢ (?M::10 ≈ @mp) ⊕ (?M::10 ≈ eq::@mp) ⊕ (?M::10 ≈ forall::@elim)
- (line: 11: pos: 5) Overloading at
- (forall::@elim | eq::@mp | @mp) _ _ Induction _
- Failed to solve
- ⊢ (ℕ → Bool) → Bool ≺ Bool
- (line: 11: pos: 5) Type of argument 3 must be convertible to the expected type in the application of
- @mp
- with arguments:
- ?M::7
- λ P : ℕ → Bool, P 0 ⇒ (∀ n : ℕ, P n ⇒ P (n + 1)) ⇒ (∀ n : ℕ, P n)
- Induction
- ?M::9
- Failed to solve
- ⊢ ∀ P : ℕ → Bool, P 0 ⇒ (∀ n : ℕ, P n ⇒ P (n + 1)) ⇒ (∀ n : ℕ, P n) ≺ ?M::7 == ?M::8
- (line: 11: pos: 5) Type of argument 3 must be convertible to the expected type in the application of
- eq::@mp
- with arguments:
- ?M::7
- ?M::8
- Induction
- ?M::9
- Failed to solve
- ⊢ (?M::17 ≈ @mp) ⊕ (?M::17 ≈ eq::@mp) ⊕ (?M::17 ≈ forall::@elim)
- (line: 12: pos: 6) Overloading at
- (forall::@elim | eq::@mp | @mp)
- _
- _
- ((forall::@elim | eq::@mp | @mp) _ _ Induction _)
- (forall::intro (λ m : _, Nat::add::zerol m ⋈ symm (Nat::add::zeror m)))
- Failed to solve
- ⊢ (?M::34 ≈ @mp) ⊕ (?M::34 ≈ eq::@mp) ⊕ (?M::34 ≈ forall::@elim)
- (line: 15: pos: 5) Overloading at
- let κ::1 := (forall::@elim | eq::@mp | @mp)
- _
- _
- ((forall::@elim | eq::@mp | @mp) _ _ Induction _)
- (forall::intro (λ m : _, Nat::add::zerol m ⋈ symm (Nat::add::zeror m))),
- κ::2 := λ n : _,
- discharge
- (λ iH : _,
- forall::intro
- (λ m : _,
- Nat::add::succl n m ⋈ subst (refl (n + m + 1)) iH ⋈
- symm (Nat::add::succr m n)))
- in (forall::@elim | eq::@mp | @mp) _ _ κ::1 (forall::intro κ::2)
- Failed to solve
- ⊢ ∀ n : ℕ, ?M::9 n ≺ ∀ n m : ℕ, n + m = m + n
- (line: 15: pos: 5) Type of definition 'Comm1' must be convertible to expected type.
- Failed to solve
- ⊢ (∀ n : ℕ, ?M::9 n ⇒ ?M::9 (n + 1)) ⇒ (∀ n : ℕ, ?M::9 n) ≺ ?M::3 == ?M::4
- (line: 15: pos: 5) Type of argument 3 must be convertible to the expected type in the application of
- eq::@mp
- with arguments:
- ?M::3
- ?M::4
- Induction ◂ ?M::9 ◂ forall::intro (λ m : ℕ, Nat::add::zerol m ⋈ symm (Nat::add::zeror m))
- forall::intro
- (λ n : ℕ,
- discharge
- (λ iH : ?M::20,
- forall::intro
- (λ m : ℕ,
- Nat::add::succl n m ⋈ subst (refl (n + m + 1)) iH ⋈
- symm (Nat::add::succr m n))))
- Failed to solve
- ⊢ Bool ≺ ?M::3 → Bool
- (line: 15: pos: 5) Type of argument 3 must be convertible to the expected type in the application of
- forall::@elim
- with arguments:
- ?M::3
- ∀ n : ℕ, ?M::9 n
- Induction ◂ ?M::9 ◂ forall::intro (λ m : ℕ, Nat::add::zerol m ⋈ symm (Nat::add::zeror m))
- forall::intro
- (λ n : ℕ,
- discharge
- (λ iH : ?M::20,
- forall::intro
- (λ m : ℕ,
- Nat::add::succl n m ⋈ subst (refl (n + m + 1)) iH ⋈
- symm (Nat::add::succr m n))))
- Failed to solve
- ⊢ ?M::9 0 ⇒ (∀ n : ℕ, ?M::9 n ⇒ ?M::9 (n + 1)) ⇒ (∀ n : ℕ, ?M::9 n) ≺ ?M::5 == ?M::6
- (line: 12: pos: 6) Type of argument 3 must be convertible to the expected type in the application of
- eq::@mp
- with arguments:
- ?M::5
- ?M::6
- Induction ◂ ?M::9
- forall::intro (λ m : ℕ, Nat::add::zerol m ⋈ symm (Nat::add::zeror m))
- Failed to solve
- ⊢ Bool ≺ ?M::5 → Bool
- (line: 12: pos: 6) Type of argument 3 must be convertible to the expected type in the application of
- forall::@elim
- with arguments:
- ?M::5
- (∀ n : ℕ, ?M::9 n ⇒ ?M::9 (n + 1)) ⇒ (∀ n : ℕ, ?M::9 n)
- Induction ◂ ?M::9
- forall::intro (λ m : ℕ, Nat::add::zerol m ⋈ symm (Nat::add::zeror m))
+ ⊢ ∀ m : ℕ, 0 + m == m + 0 ≺ ?M::3 0
+ (line: 10: pos: 3) Type of argument 2 must be convertible to the expected type in the application of
+ Induction
+ with arguments:
+ ?M::3
+ λ m : ℕ, Nat::add::zerol m ⋈ symm (Nat::add::zeror m)
+ λ (n : ℕ) (iH : ?M::3 n) (m : ℕ),
+ Nat::add::succl n m ⋈ subst (refl (n + m + 1)) iH ⋈ symm (Nat::add::succr m n)
diff --git a/tests/lean/interactive/elab6.lean b/tests/lean/interactive/elab6.lean
index d0eae73d1..28a1e5068 100644
--- a/tests/lean/interactive/elab6.lean
+++ b/tests/lean/interactive/elab6.lean
@@ -3,7 +3,6 @@
-- To be able to prove the following theorem, we have to unmark the
-- 'forall'
local env = get_environment()
-env:set_opaque("forall", false)
*)
-theorem forall::intro2 (A : (Type U)) (P : A -> Bool) (H : Pi x, P x) : forall x, P x :=
- abst (fun x, eqt::intro (H x))
+theorem forall::intro2 (A : (Type U)) (P : A -> Bool) (H : forall x, P x) : forall x, P x :=
+ H
diff --git a/tests/lean/interactive/t1.lean b/tests/lean/interactive/t1.lean
index 66e578907..031dad0e1 100644
--- a/tests/lean/interactive/t1.lean
+++ b/tests/lean/interactive/t1.lean
@@ -1,11 +1,8 @@
-theorem T2 (a b : Bool) : a => b => a /\ b.
+theorem T2 (a b : Bool) : a → b → a /\ b.
done.
done.
-(* imp_tac() *).
imp_tac2.
foo.
-(* imp_tac() *).
-(* imp_tac() *).
(* conj_tac() *).
back.
(* assumption_tac() *).
diff --git a/tests/lean/interactive/t1.lean.expected.out b/tests/lean/interactive/t1.lean.expected.out
index c83d8bdae..c38116d22 100644
--- a/tests/lean/interactive/t1.lean.expected.out
+++ b/tests/lean/interactive/t1.lean.expected.out
@@ -1,29 +1,22 @@
# Set: pp::colors
Set: pp::unicode
Proof state:
-a : Bool, b : Bool ⊢ a ⇒ b ⇒ a ∧ b
+a : Bool, b : Bool, H : a, H::1 : b ⊢ a ∧ b
## Error (line: 5, pos: 0) invalid 'done' command, proof cannot be produced from this state
Proof state:
-a : Bool, b : Bool ⊢ a ⇒ b ⇒ a ∧ b
+a : Bool, b : Bool, H : a, H::1 : b ⊢ a ∧ b
## Error (line: 6, pos: 0) invalid 'done' command, proof cannot be produced from this state
Proof state:
-a : Bool, b : Bool ⊢ a ⇒ b ⇒ a ∧ b
+a : Bool, b : Bool, H : a, H::1 : b ⊢ a ∧ b
+## Error (line: 7, pos: 0) unknown tactic 'imp_tac2'
+## Error (line: 8, pos: 0) unknown tactic 'foo'
## Proof state:
-H : a, a : Bool, b : Bool ⊢ b ⇒ a ∧ b
-## Error (line: 8, pos: 0) unknown tactic 'imp_tac2'
-## Error (line: 9, pos: 0) unknown tactic 'foo'
-## Proof state:
-H::1 : b, H : a, a : Bool, b : Bool ⊢ a ∧ b
-## Error (line: 11, pos: 0) tactic failed
+a : Bool, b : Bool, H : a, H::1 : b ⊢ a
+a : Bool, b : Bool, H : a, H::1 : b ⊢ b
+## Error (line: 10, pos: 0) failed to backtrack
Proof state:
-H::1 : b, H : a, a : Bool, b : Bool ⊢ a ∧ b
-## Proof state:
-H::1 : b, H : a, a : Bool, b : Bool ⊢ a
-H::1 : b, H : a, a : Bool, b : Bool ⊢ b
-## Error (line: 13, pos: 0) failed to backtrack
-Proof state:
-H::1 : b, H : a, a : Bool, b : Bool ⊢ a
-H::1 : b, H : a, a : Bool, b : Bool ⊢ b
+a : Bool, b : Bool, H : a, H::1 : b ⊢ a
+a : Bool, b : Bool, H : a, H::1 : b ⊢ b
## Proof state:
no goals
## Proved: T2
diff --git a/tests/lean/interactive/t10.lean b/tests/lean/interactive/t10.lean
index d5143352d..fbf8b46de 100644
--- a/tests/lean/interactive/t10.lean
+++ b/tests/lean/interactive/t10.lean
@@ -2,12 +2,12 @@
simple_tac = Repeat(OrElse(conj_hyp_tac(), conj_tac(), assumption_tac()))
*)
-theorem T2 (A B : Bool) : A /\ B => B /\ A :=
- discharge (fun H : A /\ B,
- let H1 : A := _,
- H2 : B := _,
- main : B /\ A := _
- in main).
+theorem T2 (A B : Bool) : A /\ B → B /\ A :=
+ fun H : A /\ B,
+ let H1 : A := _,
+ H2 : B := _,
+ main : B /\ A := _
+ in main.
simple_tac. done.
simple2_tac. done.
simple_tac. done.
diff --git a/tests/lean/interactive/t2.lean b/tests/lean/interactive/t2.lean
index 5fad68a4a..f14dba4bf 100644
--- a/tests/lean/interactive/t2.lean
+++ b/tests/lean/interactive/t2.lean
@@ -1,8 +1,5 @@
-theorem T2 (a b : Bool) : a => b => a /\ b.
-(* imp_tac() *)
-(* imp_tac2() *)
+theorem T2 (a b : Bool) : a → b → a /\ b.
foo.
-(* imp_tac() *)
abort.
variables a b : Bool.
diff --git a/tests/lean/interactive/t2.lean.expected.out b/tests/lean/interactive/t2.lean.expected.out
index 4c5b21e08..4161b2172 100644
--- a/tests/lean/interactive/t2.lean.expected.out
+++ b/tests/lean/interactive/t2.lean.expected.out
@@ -1,11 +1,11 @@
# Set: pp::colors
Set: pp::unicode
Proof state:
-a : Bool, b : Bool ⊢ a ⇒ b ⇒ a ∧ b
-## Error (line: 6, pos: 0) executing external script ([string "return imp_tac2() "]:1), attempt to call global 'imp_tac2' (a nil value)
-## Error (line: 9, pos: 5) failed to prove theorem, proof has been aborted
+a : Bool, b : Bool, H : a, H::1 : b ⊢ a ∧ b
+## Error (line: 5, pos: 0) unknown tactic 'foo'
+## Error (line: 6, pos: 5) failed to prove theorem, proof has been aborted
Proof state:
-H::1 : b, H : a, a : Bool, b : Bool ⊢ a ∧ b
+a : Bool, b : Bool, H : a, H::1 : b ⊢ a ∧ b
# Assumed: a
Assumed: b
# variable a : Bool
diff --git a/tests/lean/interactive/t3.lean b/tests/lean/interactive/t3.lean
index 03e933d5a..2f3e3ecce 100644
--- a/tests/lean/interactive/t3.lean
+++ b/tests/lean/interactive/t3.lean
@@ -1,7 +1,6 @@
(* import("tactic.lua") *)
-theorem T2 (a b : Bool) : b => a \/ b.
-(* imp_tac() *).
+theorem T2 (a b : Bool) : b → a \/ b.
(* disj_tac() *).
back.
back.
diff --git a/tests/lean/interactive/t3.lean.expected.out b/tests/lean/interactive/t3.lean.expected.out
index 74cab7ec4..6a1df9284 100644
--- a/tests/lean/interactive/t3.lean.expected.out
+++ b/tests/lean/interactive/t3.lean.expected.out
@@ -1,18 +1,16 @@
# Set: pp::colors
Set: pp::unicode
Proof state:
-a : Bool, b : Bool ⊢ b ⇒ a ∨ b
+a : Bool, b : Bool, H : b ⊢ a ∨ b
## Proof state:
-H : b, a : Bool, b : Bool ⊢ a ∨ b
+a : Bool, b : Bool, H : b ⊢ a
## Proof state:
-H : b, a : Bool, b : Bool ⊢ a
-## Proof state:
-H : b, a : Bool, b : Bool ⊢ b
-## Error (line: 10, pos: 0) failed to backtrack
+a : Bool, b : Bool, H : b ⊢ b
+## Error (line: 9, pos: 0) failed to backtrack
Proof state:
-H : b, a : Bool, b : Bool ⊢ b
+a : Bool, b : Bool, H : b ⊢ b
## Proof state:
no goals
## Proved: T2
-# theorem T2 (a b : Bool) : b ⇒ a ∨ b := discharge (λ H : b, or::intror a H)
+# theorem T2 (a b : Bool) (H : b) : a ∨ b := or::intror a H
#
\ No newline at end of file
diff --git a/tests/lean/interactive/t6.lean b/tests/lean/interactive/t6.lean
index f9bc99ebe..c4ff76e2b 100644
--- a/tests/lean/interactive/t6.lean
+++ b/tests/lean/interactive/t6.lean
@@ -1,7 +1,5 @@
(* import("tactic.lua") *)
-theorem T1 (a b : Bool) : a => b => a /\ b.
- (* imp_tac() *).
- (* imp_tac() *).
+theorem T1 (a b : Bool) : a → b → a /\ b.
apply and::intro.
exact.
done.
diff --git a/tests/lean/interactive/t6.lean.expected.out b/tests/lean/interactive/t6.lean.expected.out
index f61cedfab..f4bf12ace 100644
--- a/tests/lean/interactive/t6.lean.expected.out
+++ b/tests/lean/interactive/t6.lean.expected.out
@@ -1,14 +1,10 @@
# Set: pp::colors
Set: pp::unicode
Proof state:
-a : Bool, b : Bool ⊢ a ⇒ b ⇒ a ∧ b
+a : Bool, b : Bool, H : a, H::1 : b ⊢ a ∧ b
## Proof state:
-H : a, a : Bool, b : Bool ⊢ b ⇒ a ∧ b
-## Proof state:
-H::1 : b, H : a, a : Bool, b : Bool ⊢ a ∧ b
-## Proof state:
-H::1 : b, H : a, a : Bool, b : Bool ⊢ a
-H::1 : b, H : a, a : Bool, b : Bool ⊢ b
+a : Bool, b : Bool, H : a, H::1 : b ⊢ a
+a : Bool, b : Bool, H : a, H::1 : b ⊢ b
## Proof state:
no goals
## Proved: T1
diff --git a/tests/lean/interactive/t7.lean b/tests/lean/interactive/t7.lean
index 15849d843..266750d10 100644
--- a/tests/lean/interactive/t7.lean
+++ b/tests/lean/interactive/t7.lean
@@ -4,8 +4,7 @@ variable q : Int -> Int -> Bool.
variable p : Int -> Bool.
axiom Ax (a b : Int) (H : q a b) : p b.
variable a : Int.
-theorem T (x : Int) : (q a x) => (p x).
- (* imp_tac() *).
+theorem T (x : Int) : (q a x) → (p x).
apply (Ax a).
exact.
done.
diff --git a/tests/lean/interactive/t7.lean.expected.out b/tests/lean/interactive/t7.lean.expected.out
index 4b5e23b5f..5bcbc12d1 100644
--- a/tests/lean/interactive/t7.lean.expected.out
+++ b/tests/lean/interactive/t7.lean.expected.out
@@ -6,11 +6,9 @@
# Assumed: Ax
# Assumed: a
# Proof state:
-x : ℤ ⊢ q a x ⇒ p x
+x : ℤ, H : q a x ⊢ p x
## Proof state:
-H : q a x, x : ℤ ⊢ p x
-## Proof state:
-H : q a x, x : ℤ ⊢ q a x
+x : ℤ, H : q a x ⊢ q a x
## Proof state:
no goals
## Proved: T
diff --git a/tests/lean/interactive/t8.lean b/tests/lean/interactive/t8.lean
index 185a8125f..f90c641f2 100644
--- a/tests/lean/interactive/t8.lean
+++ b/tests/lean/interactive/t8.lean
@@ -1,7 +1,6 @@
(* import("tactic.lua") *)
set::option tactic::proof_state::goal_names true.
-theorem T (a : Bool) : a => a /\ a.
- apply discharge.
+theorem T (a : Bool) : a → a /\ a.
apply and::intro.
exact.
done.
diff --git a/tests/lean/interactive/t8.lean.expected.out b/tests/lean/interactive/t8.lean.expected.out
index d6c22e416..d0dbea375 100644
--- a/tests/lean/interactive/t8.lean.expected.out
+++ b/tests/lean/interactive/t8.lean.expected.out
@@ -2,12 +2,10 @@
Set: pp::unicode
Set: tactic::proof_state::goal_names
# Proof state:
-main: a : Bool ⊢ a ⇒ a ∧ a
+main: a : Bool, H : a ⊢ a ∧ a
## Proof state:
-main::1: H : a, a : Bool ⊢ a ∧ a
-## Proof state:
-main::1::1: H : a, a : Bool ⊢ a
-main::1::2: H : a, a : Bool ⊢ a
+main::1: a : Bool, H : a ⊢ a
+main::2: a : Bool, H : a ⊢ a
## Proof state:
no goals
## Proved: T
diff --git a/tests/lean/interactive/t9.lean b/tests/lean/interactive/t9.lean
index b4b7b1a41..f8da56ea9 100644
--- a/tests/lean/interactive/t9.lean
+++ b/tests/lean/interactive/t9.lean
@@ -1,11 +1,11 @@
(* import("tactic.lua") *)
-theorem T1 (A B : Bool) : A /\ B => B /\ A :=
- discharge (fun H : A /\ B,
- let main : B /\ A :=
- (let H1 : B := _,
- H2 : A := _
- in _)
- in main).
+theorem T1 (A B : Bool) : A /\ B → B /\ A :=
+ fun H : A /\ B,
+ let main : B /\ A :=
+ (let H1 : B := _,
+ H2 : A := _
+ in _)
+ in main.
conj_hyp.
exact.
done.
@@ -20,12 +20,12 @@ theorem T1 (A B : Bool) : A /\ B => B /\ A :=
simple_tac = Repeat(OrElse(conj_hyp_tac(), conj_tac(), assumption_tac()))
*)
-theorem T2 (A B : Bool) : A /\ B => B /\ A :=
- discharge (fun H : A /\ B,
- let H1 : A := _,
- H2 : B := _,
- main : B /\ A := _
- in main).
+theorem T2 (A B : Bool) : A /\ B → B /\ A :=
+ fun H : A /\ B,
+ let H1 : A := _,
+ H2 : B := _,
+ main : B /\ A := _
+ in main.
simple_tac. done.
simple_tac. done.
simple_tac. done.
diff --git a/tests/lean/let2.lean b/tests/lean/let2.lean
index 34352789b..cc10f337a 100644
--- a/tests/lean/let2.lean
+++ b/tests/lean/let2.lean
@@ -1,10 +1,10 @@
-- Annotating lemmas
-theorem simple (p q r : Bool) : (p ⇒ q) ∧ (q ⇒ r) ⇒ p ⇒ r :=
- discharge (λ H_pq_qr, discharge (λ H_p,
- let P_pq : (p ⇒ q) := and::eliml H_pq_qr,
- P_qr : (q ⇒ r) := and::elimr H_pq_qr,
- P_q : q := mp P_pq H_p
- in mp P_qr P_q))
+theorem simple (p q r : Bool) : (p → q) ∧ (q → r) → p → r :=
+ λ H_pq_qr H_p,
+ let P_pq : (p → q) := and::eliml H_pq_qr,
+ P_qr : (q → r) := and::elimr H_pq_qr,
+ P_q : q := P_pq H_p
+ in P_qr P_q
print environment 1
\ No newline at end of file
diff --git a/tests/lean/let2.lean.expected.out b/tests/lean/let2.lean.expected.out
index 9681b9ddc..a786aa1ee 100644
--- a/tests/lean/let2.lean.expected.out
+++ b/tests/lean/let2.lean.expected.out
@@ -1,12 +1,5 @@
Set: pp::colors
Set: pp::unicode
Proved: simple
-theorem simple (p q r : Bool) : (p ⇒ q) ∧ (q ⇒ r) ⇒ p ⇒ r :=
- discharge
- (λ H_pq_qr : (p ⇒ q) ∧ (q ⇒ r),
- discharge
- (λ H_p : p,
- let P_pq : p ⇒ q := and::eliml H_pq_qr,
- P_qr : q ⇒ r := and::elimr H_pq_qr,
- P_q : q := P_pq ◂ H_p
- in P_qr ◂ P_q))
+theorem simple (p q r : Bool) (H_pq_qr : (p → q) ∧ (q → r)) (H_p : p) : r :=
+ let P_pq : p → q := and::eliml H_pq_qr, P_qr : q → r := and::elimr H_pq_qr, P_q : q := P_pq H_p in P_qr P_q
diff --git a/tests/lean/let3.lean b/tests/lean/let3.lean
index 5f9c77ae3..857de3218 100644
--- a/tests/lean/let3.lean
+++ b/tests/lean/let3.lean
@@ -1,6 +1,6 @@
import Int.
-variable magic : Pi (H : Bool), H
+variable magic : forall (H : Bool), H
set::option pp::notation false
set::option pp::coercion true
diff --git a/tests/lean/mod1.lean.expected.out b/tests/lean/mod1.lean.expected.out
index c51516045..f9055fbcb 100644
--- a/tests/lean/mod1.lean.expected.out
+++ b/tests/lean/mod1.lean.expected.out
@@ -2,5 +2,5 @@
Set: pp::unicode
Imported 'cast'
Imported 'cast'
-@cast : Π (A B : (Type U)), A == B → A → B
-@cast : Π (A B : (Type U)), A == B → A → B
+@cast : ∀ (A B : (Type U)), A == B → A → B
+@cast : ∀ (A B : (Type U)), A == B → A → B
diff --git a/tests/lean/mp_forallelim.lean b/tests/lean/mp_forallelim.lean
index 08829eb06..029c50efa 100644
--- a/tests/lean/mp_forallelim.lean
+++ b/tests/lean/mp_forallelim.lean
@@ -1,7 +1,7 @@
variable p : Nat -> Nat -> Bool
check fun (a b c : Bool) (p : Nat -> Nat -> Bool) (n m : Nat)
- (H : a => b => (forall x y, c => p (x + n) (x + m)))
+ (H : a → b → (forall x y, c → p (x + n) (x + m)))
(Ha : a)
(Hb : b)
(Hc : c),
- H ◂ Ha ◂ Hb ◂ 0 ◂ 1 ◂ Hc
+ H Ha Hb 0 1 Hc
diff --git a/tests/lean/mp_forallelim.lean.expected.out b/tests/lean/mp_forallelim.lean.expected.out
index 1941d0554..3a5792bc4 100644
--- a/tests/lean/mp_forallelim.lean.expected.out
+++ b/tests/lean/mp_forallelim.lean.expected.out
@@ -4,10 +4,10 @@
λ (a b c : Bool)
(p : ℕ → ℕ → Bool)
(n m : ℕ)
- (H : a ⇒ b ⇒ (∀ x y : ℕ, c ⇒ p (x + n) (x + m)))
+ (H : a → b → (∀ (x y : ℕ), c → p (x + n) (x + m)))
(Ha : a)
(Hb : b)
(Hc : c),
- H ◂ Ha ◂ Hb ◂ 0 ◂ 1 ◂ Hc :
- Π (a b c : Bool) (p : ℕ → ℕ → Bool) (n m : ℕ),
- (a ⇒ b ⇒ (∀ x y : ℕ, c ⇒ p (x + n) (x + m))) → a → b → c → p (0 + n) (0 + m)
+ H Ha Hb 0 1 Hc :
+ ∀ (a b c : Bool) (p : ℕ → ℕ → Bool) (n m : ℕ),
+ (a → b → (∀ (x y : ℕ), c → p (x + n) (x + m))) → a → b → c → p (0 + n) (0 + m)
diff --git a/tests/lean/norm1.lean b/tests/lean/norm1.lean
index 67c79cf58..8ebbc8d91 100644
--- a/tests/lean/norm1.lean
+++ b/tests/lean/norm1.lean
@@ -8,7 +8,7 @@ eval fun f : N -> N, (fun x y : N, g x) (f a)
eval fun (a : N) (f : N -> N) (g : (N -> N) -> N -> N) (h : N -> N -> N),
(fun (x : N) (y : N) (z : N), h x y) (g (fun x : N, f (f x)) (f a)) (f a)
eval fun (a b : N) (g : Bool -> N), (fun x y : Bool, g x) (a == b)
-eval fun (a : Type) (b : a -> Type) (g : (Type U) -> Bool), (fun x y : (Type U), g x) (Pi x : a, b x)
+eval fun (a : Type) (b : a -> Type) (g : (Type U) -> Bool), (fun x y : (Type U), g x) (forall x : a, b x)
eval fun f : N -> N, (fun x y z : N, g x) (f a)
eval fun f g : N -> N, (fun x y z : N, g x) (f a)
eval fun f : N -> N, (fun x : N, fun y : N, fun z : N, P x y z) (f a)
diff --git a/tests/lean/norm1.lean.expected.out b/tests/lean/norm1.lean.expected.out
index 84cf91d82..168dab14e 100644
--- a/tests/lean/norm1.lean.expected.out
+++ b/tests/lean/norm1.lean.expected.out
@@ -8,7 +8,7 @@
λ (f : N → N) (y : N), g (f a)
λ (a : N) (f : N → N) (g : (N → N) → N → N) (h : N → N → N) (z : N), h (g (λ x : N, f (f x)) (f a)) (f a)
λ (a b : N) (g : Bool → N) (y : Bool), g (a == b)
-λ (a : Type) (b : a → Type) (g : (Type U) → Bool) (y : (Type U)), g (Π x : a, b x)
+λ (a : Type) (b : a → Type) (g : (Type U) → Bool) (y : (Type U)), g (∀ x : a, b x)
λ (f : N → N) (y z : N), g (f a)
λ (f g : N → N) (y z : N), g (f a)
λ (f : N → N) (y z : N), P (f a) y z
diff --git a/tests/lean/norm_bug1.lean b/tests/lean/norm_bug1.lean
index 202cb80c2..983defd58 100644
--- a/tests/lean/norm_bug1.lean
+++ b/tests/lean/norm_bug1.lean
@@ -12,11 +12,11 @@ check fun (A A': TypeM)
check fun (A A': TypeM)
(B : A -> TypeM)
(B' : A' -> TypeM)
- (f : Pi x : A, B x)
- (g : Pi x : A', B' x)
+ (f : forall x : A, B x)
+ (g : forall x : A', B' x)
(a : A)
(b : A')
- (H1 : (Pi x : A, B x) == (Pi x : A', B' x))
+ (H1 : (forall x : A, B x) == (forall x : A', B' x))
(H2 : f == g)
(H3 : a == b),
let L1 : A == A' := dominj H1,
diff --git a/tests/lean/norm_bug1.lean.expected.out b/tests/lean/norm_bug1.lean.expected.out
index b5eb5ea11..cfbb3104f 100644
--- a/tests/lean/norm_bug1.lean.expected.out
+++ b/tests/lean/norm_bug1.lean.expected.out
@@ -3,15 +3,15 @@
Imported 'cast'
Set: pp::colors
λ (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), let b' : A := cast L2 b, L3 : b == b' := cast::eq L2 b in L3 :
- Π (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), b == cast L2 b
+ ∀ (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), b == cast L2 b
λ (A A' : TypeM)
(B : A → TypeM)
(B' : A' → TypeM)
- (f : Π x : A, B x)
- (g : Π x : A', B' x)
+ (f : ∀ x : A, B x)
+ (g : ∀ x : A', B' x)
(a : A)
(b : A')
- (H1 : (Π x : A, B x) == (Π x : A', B' x))
+ (H1 : (∀ x : A, B x) == (∀ x : A', B' x))
(H2 : f == g)
(H3 : a == b),
let L1 : A == A' := dominj H1,
@@ -21,12 +21,12 @@
L4 : a == b' := htrans H3 L3,
L5 : f a == f b' := congr2 f L4
in L5 :
- Π (A A' : TypeM)
+ ∀ (A A' : TypeM)
(B : A → TypeM)
(B' : A' → TypeM)
- (f : Π x : A, B x)
- (g : Π x : A', B' x)
+ (f : ∀ x : A, B x)
+ (g : ∀ x : A', B' x)
(a : A)
(b : A')
- (H1 : (Π x : A, B x) == (Π x : A', B' x)),
+ (H1 : (∀ x : A, B x) == (∀ x : A', B' x)),
f == g → a == b → f a == f (cast (symm (dominj H1)) b)
diff --git a/tests/lean/norm_tac.lean b/tests/lean/norm_tac.lean
index 219aa95ab..63c436f52 100644
--- a/tests/lean/norm_tac.lean
+++ b/tests/lean/norm_tac.lean
@@ -10,4 +10,4 @@ definition D := read V1 1 (by trivial)
print environment 1
variable b : Bool
definition a := b
-theorem T : b => a := (by (* imp_tac() .. normalize_tac() .. assumption_tac() *))
+theorem T : b → a := (by (* normalize_tac() .. assumption_tac() *))
diff --git a/tests/lean/revapp.lean b/tests/lean/revapp.lean
index 44f8e4600..c552cdc40 100644
--- a/tests/lean/revapp.lean
+++ b/tests/lean/revapp.lean
@@ -1,5 +1,5 @@
import Int.
-definition revapp {A : (Type U)} {B : A -> (Type U)} (a : A) (f : Pi (x : A), B x) : (B a) := f a.
+definition revapp {A : (Type U)} {B : A -> (Type U)} (a : A) (f : forall (x : A), B x) : (B a) := f a.
infixl 100 |> : revapp
eval 10 |> (fun x, x + 1)
diff --git a/tests/lean/scope.lean.expected.out b/tests/lean/scope.lean.expected.out
index 79224d990..26f666cbf 100644
--- a/tests/lean/scope.lean.expected.out
+++ b/tests/lean/scope.lean.expected.out
@@ -12,11 +12,15 @@
Proved: f_eq_g
Proved: Inj
definition g (A : Type) (f : A → A → A) (x y : A) : A := f y x
-theorem f_eq_g (A : Type) (f : A → A → A) (H1 : Π x y : A, f x y = f y x) : f = g A f :=
+theorem f_eq_g (A : Type) (f : A → A → A) (H1 : ∀ x y : A, f x y = f y x) : f = g A f :=
abst (λ x : A,
abst (λ y : A, let L1 : f x y = f y x := H1 x y, L2 : f y x = g A f x y := refl (g A f x y) in L1 ⋈ L2))
-theorem Inj (A B : Type) (h : A → B) (hinv : B → A) (Inv : Π x : A, hinv (h x) = x) (x y : A) (H : h x = h y) : x =
- y :=
+theorem Inj (A B : Type)
+ (h : A → B)
+ (hinv : B → A)
+ (Inv : ∀ x : A, hinv (h x) = x)
+ (x y : A)
+ (H : h x = h y) : x = y :=
let L1 : hinv (h x) = hinv (h y) := congr2 hinv H,
L2 : hinv (h x) = x := Inv x,
L3 : hinv (h y) = y := Inv y,
diff --git a/tests/lean/subst2.lean b/tests/lean/subst2.lean
index cf01df570..41023b907 100644
--- a/tests/lean/subst2.lean
+++ b/tests/lean/subst2.lean
@@ -1,14 +1,5 @@
(* import("tactic.lua") *)
-theorem T (A : Type) (p : A -> Bool) (f : A -> A -> A) : forall x y z, p (f x x) => x = y => x = z => p (f y z).
- apply forall::intro.
- beta.
- apply forall::intro.
- beta.
- apply forall::intro.
- beta.
- apply discharge.
- apply discharge.
- apply discharge.
+theorem T (A : Type) (p : A -> Bool) (f : A -> A -> A) : forall x y z, p (f x x) → x = y → x = z → p (f y z).
apply (subst (subst H H::1) H::2)
done.
diff --git a/tests/lean/subst2.lean.expected.out b/tests/lean/subst2.lean.expected.out
index 105c51865..6e38b9a45 100644
--- a/tests/lean/subst2.lean.expected.out
+++ b/tests/lean/subst2.lean.expected.out
@@ -1,15 +1,11 @@
Set: pp::colors
Set: pp::unicode
Proved: T
-theorem T (A : Type) (p : A → Bool) (f : A → A → A) : ∀ x y z : A,
- p (f x x) ⇒ x = y ⇒ x = z ⇒ p (f y z) :=
- forall::intro
- (λ x : A,
- forall::intro
- (λ x::1 : A,
- forall::intro
- (λ x::2 : A,
- discharge
- (λ H : p (f x x),
- discharge
- (λ H::1 : x = x::1, discharge (λ H::2 : x = x::2, subst (subst H H::1) H::2))))))
+theorem T (A : Type)
+ (p : A → Bool)
+ (f : A → A → A)
+ (x y z : A)
+ (H : p (f x x))
+ (H::1 : x = y)
+ (H::2 : x = z) : p (f y z) :=
+ subst (subst H H::1) H::2
diff --git a/tests/lean/subst3.lean b/tests/lean/subst3.lean
index 3c011904c..a415b5163 100644
--- a/tests/lean/subst3.lean
+++ b/tests/lean/subst3.lean
@@ -1,7 +1,7 @@
import macros
-theorem T (A : Type) (p : A -> Bool) (f : A -> A -> A) : forall x y z, p (f x x) => x = y => x = z => p (f y z) :=
- take x y z, assume (H1 : p (f x x)) (H2 : x = y) (H3 : x = z),
+theorem T (A : Type) (p : A -> Bool) (f : A -> A -> A) : forall x y z, p (f x x) → x = y → x = z → p (f y z) :=
+ λ x y z, λ (H1 : p (f x x)) (H2 : x = y) (H3 : x = z),
subst (subst H1 H2) H3
print environment 1.
\ No newline at end of file
diff --git a/tests/lean/subst3.lean.expected.out b/tests/lean/subst3.lean.expected.out
index 1314ef553..2c0b56907 100644
--- a/tests/lean/subst3.lean.expected.out
+++ b/tests/lean/subst3.lean.expected.out
@@ -2,14 +2,11 @@
Set: pp::unicode
Imported 'macros'
Proved: T
-theorem T (A : Type) (p : A → Bool) (f : A → A → A) : ∀ x y z : A,
- p (f x x) ⇒ x = y ⇒ x = z ⇒ p (f y z) :=
- forall::intro
- (λ x : A,
- forall::intro
- (λ y : A,
- forall::intro
- (λ z : A,
- discharge
- (λ H1 : p (f x x),
- discharge (λ H2 : x = y, discharge (λ H3 : x = z, subst (subst H1 H2) H3))))))
+theorem T (A : Type)
+ (p : A → Bool)
+ (f : A → A → A)
+ (x y z : A)
+ (H1 : p (f x x))
+ (H2 : x = y)
+ (H3 : x = z) : p (f y z) :=
+ subst (subst H1 H2) H3
diff --git a/tests/lean/tactic1.lean b/tests/lean/tactic1.lean
index 278f420a3..f556e672e 100644
--- a/tests/lean/tactic1.lean
+++ b/tests/lean/tactic1.lean
@@ -2,7 +2,7 @@ variables p q r : Bool
(*
local env = get_environment()
- local conjecture = parse_lean('p => q => p && q')
+ local conjecture = parse_lean('p → q → p && q')
local tac = Repeat(conj_tac() ^ imp_tac() ^ assumption_tac())
local proof = tac:solve(env, context(), conjecture)
env:add_theorem("T1", conjecture, proof)
diff --git a/tests/lean/tactic1.lean.expected.out b/tests/lean/tactic1.lean.expected.out
index e3b118305..4f3276d2b 100644
--- a/tests/lean/tactic1.lean.expected.out
+++ b/tests/lean/tactic1.lean.expected.out
@@ -3,4 +3,4 @@
Assumed: p
Assumed: q
Assumed: r
-theorem T1 : p ⇒ q ⇒ p ∧ q := discharge (λ H : p, discharge (λ H::1 : q, and::intro H H::1))
+theorem T1 (H : p) (H::1 : q) : p ∧ q := and::intro H H::1
diff --git a/tests/lean/tactic10.lean b/tests/lean/tactic10.lean
index 43d61479a..a9c45d834 100644
--- a/tests/lean/tactic10.lean
+++ b/tests/lean/tactic10.lean
@@ -2,22 +2,20 @@
definition f(a : Bool) : Bool := not a.
definition g(a b : Bool) : Bool := a \/ b.
-theorem T1 (a b : Bool) : (g a b) => (f b) => a := _.
+theorem T1 (a b : Bool) : (g a b) → (f b) → a := _.
unfold_all
- apply discharge
- apply discharge
disj_hyp
exact
absurd
done.
(*
-simple_tac = Repeat(unfold_tac()) .. Repeat(OrElse(imp_tac(), conj_hyp_tac(), assumption_tac(), absurd_tac(), conj_hyp_tac(), disj_hyp_tac()))
+simple_tac = Repeat(unfold_tac()) .. Repeat(OrElse(conj_hyp_tac(), assumption_tac(), absurd_tac(), conj_hyp_tac(), disj_hyp_tac()))
*)
definition h(a b : Bool) : Bool := g a b.
-theorem T2 (a b : Bool) : (h a b) => (f b) => a := _.
+theorem T2 (a b : Bool) : (h a b) → (f b) → a := _.
simple_tac
done.
diff --git a/tests/lean/tactic10.lean.expected.out b/tests/lean/tactic10.lean.expected.out
index f5abe8d09..1d28c4c9c 100644
--- a/tests/lean/tactic10.lean.expected.out
+++ b/tests/lean/tactic10.lean.expected.out
@@ -5,5 +5,4 @@
Proved: T1
Defined: h
Proved: T2
-theorem T2 (a b : Bool) : h a b ⇒ f b ⇒ a :=
- discharge (λ H : a ∨ b, discharge (λ H::1 : ¬ b, or::elim H (λ H : a, H) (λ H : b, absurd::elim a H H::1)))
+theorem T2 (a b : Bool) (H : h a b) (H::1 : f b) : a := or::elim H (λ H : a, H) (λ H : b, absurd::elim a H H::1)
diff --git a/tests/lean/tactic11.lean b/tests/lean/tactic11.lean
index f44ce4cec..5ac6d3655 100644
--- a/tests/lean/tactic11.lean
+++ b/tests/lean/tactic11.lean
@@ -1,7 +1,6 @@
(* import("tactic.lua") *)
-theorem T (a b : Bool) : ((fun x, x /\ b) a) => ((fun x, x) a) := _ .
+theorem T (a b : Bool) : ((fun x, x /\ b) a) → ((fun x, x) a) := _ .
beta.
- apply discharge.
conj_hyp.
exact.
done.
diff --git a/tests/lean/tactic12.lean b/tests/lean/tactic12.lean
index b254ddc7f..998204998 100644
--- a/tests/lean/tactic12.lean
+++ b/tests/lean/tactic12.lean
@@ -1,14 +1,12 @@
(* import("tactic.lua") *)
-theorem T (a b : Bool) : ((fun x, x /\ b) a) => ((fun x, x) a).
+theorem T (a b : Bool) : ((fun x, x /\ b) a) → ((fun x, x) a).
beta.
- apply discharge.
conj_hyp.
exact.
done.
variables p q : Bool.
-theorem T2 : p /\ q => q.
- apply discharge.
+theorem T2 : p /\ q → q.
conj_hyp.
exact.
done.
\ No newline at end of file
diff --git a/tests/lean/tactic2.lean b/tests/lean/tactic2.lean
index 3fc564fdb..1ade0a10d 100644
--- a/tests/lean/tactic2.lean
+++ b/tests/lean/tactic2.lean
@@ -1,37 +1,36 @@
(* import("tactic.lua") *)
variables p q r : Bool
-theorem T1 : p => q => p /\ q :=
- discharge (fun H1,
- discharge (fun H2,
- let H1 : p := _,
- H2 : q := _
- in and::intro H1 H2
- )).
+theorem T1 : p → q → p /\ q :=
+ (fun H1 H2,
+ let H1 : p := _,
+ H2 : q := _
+ in and::intro H1 H2
+ ).
exact -- solve first metavar
done
exact -- solve second metavar
done
(*
-simple_tac = Repeat(imp_tac() ^ conj_tac() ^ assumption_tac())
+simple_tac = Repeat(conj_tac() ^ assumption_tac())
*)
-theorem T2 : p => q => p /\ q /\ p := _.
+theorem T2 : p → q → p /\ q /\ p := _.
simple_tac
done
print environment 1
-theorem T3 : p => p /\ q => r => q /\ r /\ p := _.
- (* Repeat(OrElse(imp_tac(), conj_tac(), conj_hyp_tac(), assumption_tac())) *)
+theorem T3 : p → p /\ q → r → q /\ r /\ p := _.
+ (* Repeat(OrElse(conj_tac(), conj_hyp_tac(), assumption_tac())) *)
done
-- Display proof term generated by previous tac
print environment 1
-theorem T4 : p => p /\ q => r => q /\ r /\ p := _.
- Repeat (OrElse (apply discharge) (apply and::intro) conj_hyp exact)
+theorem T4 : p → p /\ q → r → q /\ r /\ p := _.
+ Repeat (OrElse (apply and::intro) conj_hyp exact)
done
-- Display proof term generated by previous tac --
diff --git a/tests/lean/tactic2.lean.expected.out b/tests/lean/tactic2.lean.expected.out
index fad00475d..642db319f 100644
--- a/tests/lean/tactic2.lean.expected.out
+++ b/tests/lean/tactic2.lean.expected.out
@@ -5,21 +5,8 @@
Assumed: r
Proved: T1
Proved: T2
-theorem T2 : p ⇒ q ⇒ p ∧ q ∧ p :=
- discharge (λ H : p, discharge (λ H::1 : q, and::intro H (and::intro H::1 H)))
+theorem T2 (H : p) (H::1 : q) : p ∧ q ∧ p := and::intro H (and::intro H::1 H)
Proved: T3
-theorem T3 : p ⇒ p ∧ q ⇒ r ⇒ q ∧ r ∧ p :=
- discharge
- (λ H : p,
- discharge
- (λ H::1 : p ∧ q,
- discharge (λ H::2 : r, and::intro (and::elimr H::1) (and::intro H::2 (and::eliml H::1)))))
+theorem T3 (H : p) (H::1 : p ∧ q) (H::2 : r) : q ∧ r ∧ p := and::intro (and::elimr H::1) (and::intro H::2 H)
Proved: T4
-theorem T4 : p ⇒ p ∧ q ⇒ r ⇒ q ∧ r ∧ p :=
- discharge
- (λ H : p,
- discharge
- (λ H::1 : p ∧ q,
- discharge
- (λ H::2 : r,
- and::intro (and::elimr H::1) (let H::1::1 := and::eliml H::1 in and::intro H::2 H::1::1))))
+theorem T4 (H : p) (H::1 : p ∧ q) (H::2 : r) : q ∧ r ∧ p := and::intro (and::elimr H::1) (and::intro H::2 H)
diff --git a/tests/lean/tactic3.lean b/tests/lean/tactic3.lean
index 9e58081cc..94afc0f0d 100644
--- a/tests/lean/tactic3.lean
+++ b/tests/lean/tactic3.lean
@@ -1,7 +1,7 @@
(* import("tactic.lua") *)
variables p q r : Bool
-theorem T1 : p => p /\ q => r => q /\ r /\ p := _.
+theorem T1 : p → p /\ q → r → q /\ r /\ p := _.
(* Repeat(OrElse(imp_tac(), conj_tac(), conj_hyp_tac(), assumption_tac())) *)
done
diff --git a/tests/lean/tactic3.lean.expected.out b/tests/lean/tactic3.lean.expected.out
index ac015c76a..bfcc44270 100644
--- a/tests/lean/tactic3.lean.expected.out
+++ b/tests/lean/tactic3.lean.expected.out
@@ -4,9 +4,4 @@
Assumed: q
Assumed: r
Proved: T1
-theorem T1 : p ⇒ p ∧ q ⇒ r ⇒ q ∧ r ∧ p :=
- discharge
- (λ H : p,
- discharge
- (λ H::1 : p ∧ q,
- discharge (λ H::2 : r, and::intro (and::elimr H::1) (and::intro H::2 (and::eliml H::1)))))
+theorem T1 (H : p) (H::1 : p ∧ q) (H::2 : r) : q ∧ r ∧ p := and::intro (and::elimr H::1) (and::intro H::2 H)
diff --git a/tests/lean/tactic4.lean b/tests/lean/tactic4.lean
index eeae9a2ba..7c7cd23d0 100644
--- a/tests/lean/tactic4.lean
+++ b/tests/lean/tactic4.lean
@@ -2,7 +2,7 @@
simple_tac = Repeat(OrElse(imp_tac(), conj_tac())) .. assumption_tac()
*)
-theorem T4 (a b : Bool) : a => b => a /\ b := _.
+theorem T4 (a b : Bool) : a → b → a /\ b := _.
simple_tac
done
diff --git a/tests/lean/tactic4.lean.expected.out b/tests/lean/tactic4.lean.expected.out
index ea948013c..8e9fca032 100644
--- a/tests/lean/tactic4.lean.expected.out
+++ b/tests/lean/tactic4.lean.expected.out
@@ -1,4 +1,4 @@
Set: pp::colors
Set: pp::unicode
Proved: T4
-theorem T4 (a b : Bool) : a ⇒ b ⇒ a ∧ b := discharge (λ H : a, discharge (λ H::1 : b, and::intro H H::1))
+theorem T4 (a b : Bool) (H : a) (H::1 : b) : a ∧ b := and::intro H H::1
diff --git a/tests/lean/tactic5.lean b/tests/lean/tactic5.lean
index a6b9dfe16..5567fdd00 100644
--- a/tests/lean/tactic5.lean
+++ b/tests/lean/tactic5.lean
@@ -2,7 +2,7 @@
simple_tac = Repeat(OrElse(imp_tac(), conj_tac())) .. assumption_tac()
*)
-theorem T4 (a b : Bool) : a => b => a /\ b /\ a := _.
+theorem T4 (a b : Bool) : a → b → a /\ b /\ a := _.
simple_tac
done
diff --git a/tests/lean/tactic5.lean.expected.out b/tests/lean/tactic5.lean.expected.out
index 15c9d9b11..1f95d5412 100644
--- a/tests/lean/tactic5.lean.expected.out
+++ b/tests/lean/tactic5.lean.expected.out
@@ -1,5 +1,4 @@
Set: pp::colors
Set: pp::unicode
Proved: T4
-theorem T4 (a b : Bool) : a ⇒ b ⇒ a ∧ b ∧ a :=
- discharge (λ H : a, discharge (λ H::1 : b, and::intro H (and::intro H::1 H)))
+theorem T4 (a b : Bool) (H : a) (H::1 : b) : a ∧ b ∧ a := and::intro H (and::intro H::1 H)
diff --git a/tests/lean/tactic6.lean b/tests/lean/tactic6.lean
index d61430d25..c61e31265 100644
--- a/tests/lean/tactic6.lean
+++ b/tests/lean/tactic6.lean
@@ -1,16 +1,12 @@
(* import("tactic.lua") *)
-theorem T (a b c : Bool): a => b /\ c => c /\ a /\ b := _.
- apply discharge
- apply discharge
+theorem T (a b c : Bool): a → b /\ c → c /\ a /\ b := _.
conj_hyp
apply and::intro
(* Focus(Then(show_tac(), conj_tac(), show_tac(), assumption_tac()), 2) *)
exact
done
-theorem T2 (a b c : Bool): a => b /\ c => c /\ a /\ b := _.
- apply discharge
- apply discharge
+theorem T2 (a b c : Bool): a → b /\ c → c /\ a /\ b := _.
conj_hyp
apply and::intro
(* show_tac() *)
diff --git a/tests/lean/tactic6.lean.expected.out b/tests/lean/tactic6.lean.expected.out
index 7971625b0..94457225c 100644
--- a/tests/lean/tactic6.lean.expected.out
+++ b/tests/lean/tactic6.lean.expected.out
@@ -1,19 +1,19 @@
Set: pp::colors
Set: pp::unicode
Proof state:
-H::1::1 : b, H::1::2 : c, H : a, a : Bool, b : Bool, c : Bool ⊢ a ∧ b
+a : Bool, b : Bool, c : Bool, H : a, H::1::1 : b, H::1::2 : c ⊢ a ∧ b
Proof state:
-H::1::1 : b, H::1::2 : c, H : a, a : Bool, b : Bool, c : Bool ⊢ a
-H::1::1 : b, H::1::2 : c, H : a, a : Bool, b : Bool, c : Bool ⊢ b
+a : Bool, b : Bool, c : Bool, H : a, H::1::1 : b, H::1::2 : c ⊢ a
+a : Bool, b : Bool, c : Bool, H : a, H::1::1 : b, H::1::2 : c ⊢ b
Proved: T
Proof state:
-H::1::1 : b, H::1::2 : c, H : a, a : Bool, b : Bool, c : Bool ⊢ c
-H::1::1 : b, H::1::2 : c, H : a, a : Bool, b : Bool, c : Bool ⊢ a ∧ b
+a : Bool, b : Bool, c : Bool, H : a, H::1::1 : b, H::1::2 : c ⊢ c
+a : Bool, b : Bool, c : Bool, H : a, H::1::1 : b, H::1::2 : c ⊢ a ∧ b
Proof state:
-H::1::1 : b, H::1::2 : c, H : a, a : Bool, b : Bool, c : Bool ⊢ a ∧ b
+a : Bool, b : Bool, c : Bool, H : a, H::1::1 : b, H::1::2 : c ⊢ a ∧ b
Proof state:
-H::1::1 : b, H::1::2 : c, H : a, a : Bool, b : Bool, c : Bool ⊢ c
-H::1::1 : b, H::1::2 : c, H : a, a : Bool, b : Bool, c : Bool ⊢ b
+a : Bool, b : Bool, c : Bool, H : a, H::1::1 : b, H::1::2 : c ⊢ c
+a : Bool, b : Bool, c : Bool, H : a, H::1::1 : b, H::1::2 : c ⊢ b
Proof state:
-H::1::1 : b, H::1::2 : c, H : a, a : Bool, b : Bool, c : Bool ⊢ b
+a : Bool, b : Bool, c : Bool, H : a, H::1::1 : b, H::1::2 : c ⊢ b
Proved: T2
diff --git a/tests/lean/tactic8.lean b/tests/lean/tactic8.lean
index ead518c71..e3c6503a9 100644
--- a/tests/lean/tactic8.lean
+++ b/tests/lean/tactic8.lean
@@ -1,7 +1,5 @@
(* import("tactic.lua") *)
-theorem T (a b : Bool) : a \/ b => (not b) => a := _.
- apply discharge
- apply discharge
+theorem T (a b : Bool) : a \/ b → (not b) → a := _.
disj_hyp
exact
absurd
diff --git a/tests/lean/tactic8.lean.expected.out b/tests/lean/tactic8.lean.expected.out
index c053ca4f6..2f702c1d2 100644
--- a/tests/lean/tactic8.lean.expected.out
+++ b/tests/lean/tactic8.lean.expected.out
@@ -1,5 +1,4 @@
Set: pp::colors
Set: pp::unicode
Proved: T
-theorem T (a b : Bool) : a ∨ b ⇒ ¬ b ⇒ a :=
- discharge (λ H : a ∨ b, discharge (λ H::1 : ¬ b, or::elim H (λ H : a, H) (λ H : b, absurd::elim a H H::1)))
+theorem T (a b : Bool) (H : a ∨ b) (H::1 : ¬ b) : a := or::elim H (λ H : a, H) (λ H : b, absurd::elim a H H::1)
diff --git a/tests/lean/tactic9.lean b/tests/lean/tactic9.lean
index 4fdb20b89..3f721190a 100644
--- a/tests/lean/tactic9.lean
+++ b/tests/lean/tactic9.lean
@@ -1,9 +1,7 @@
(* import("tactic.lua") *)
definition f(a : Bool) : Bool := not a.
-theorem T (a b : Bool) : a \/ b => (f b) => a := _.
- apply discharge
- apply discharge
+theorem T (a b : Bool) : a \/ b → (f b) → a := _.
disj_hyp
unfold f
exact
diff --git a/tests/lean/tactic9.lean.expected.out b/tests/lean/tactic9.lean.expected.out
index fbbaf838f..3da17962c 100644
--- a/tests/lean/tactic9.lean.expected.out
+++ b/tests/lean/tactic9.lean.expected.out
@@ -2,5 +2,4 @@
Set: pp::unicode
Defined: f
Proved: T
-theorem T (a b : Bool) : a ∨ b ⇒ f b ⇒ a :=
- discharge (λ H : a ∨ b, discharge (λ H::1 : f b, or::elim H (λ H : a, H) (λ H : b, absurd::elim a H H::1)))
+theorem T (a b : Bool) (H : a ∨ b) (H::1 : f b) : a := or::elim H (λ H : a, H) (λ H : b, absurd::elim a H H::1)
diff --git a/tests/lean/tst1.lean b/tests/lean/tst1.lean
index c0137a4e2..b872329ff 100644
--- a/tests/lean/tst1.lean
+++ b/tests/lean/tst1.lean
@@ -7,7 +7,7 @@ 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 vector (A : Type) (n : N) : Type := forall (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 (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
diff --git a/tests/lean/tst1.lean.expected.out b/tests/lean/tst1.lean.expected.out
index eb3bc6ba3..f3d47c176 100644
--- a/tests/lean/tst1.lean.expected.out
+++ b/tests/lean/tst1.lean.expected.out
@@ -17,7 +17,7 @@ variable two : N
variable three : N
infix 50 < : lt
axiom two_lt_three : two < three
-definition vector (A : Type) (n : N) : Type := Π (i : N), i < n → A
+definition vector (A : Type) (n : N) : Type := ∀ (i : N), i < n → A
definition const {A : Type} (n : N) (d : A) : vector A n := λ (i : N) (H : i < 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 (j = i) d (v j H)
@@ -29,20 +29,20 @@ if (two == two) ⊤ ⊥
update (const three ⊥) two ⊤ : vector Bool three
--------
-@select : Π (A : Type) (n : N) (v : vector A n) (i : N), i < n → A
+@select : ∀ (A : Type) (n : N) (v : vector A n) (i : N), i < n → A
map type --->
-@map : Π (A B C : Type) (n : N), (A → B → C) → vector A n → vector B n → vector C n
+@map : ∀ (A B C : Type) (n : N), (A → B → C) → vector A n → vector B n → vector C n
map normal form -->
λ (A B C : Type)
(n : N)
(f : A → B → C)
- (v1 : Π (i : N), i < n → A)
- (v2 : Π (i : N), i < n → B)
+ (v1 : ∀ (i : N), i < n → A)
+ (v2 : ∀ (i : N), 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), i < n → A) (i : N) (d : A) (j : N) (H : j < n), if (j == i) d (v j H)
+λ (A : Type) (n : N) (v : ∀ (i : N), i < n → A) (i : N) (d : A) (j : N) (H : j < n), if (j == i) d (v j H)
diff --git a/tests/lean/tst10.lean b/tests/lean/tst10.lean
index d2af22553..f825b758d 100644
--- a/tests/lean/tst10.lean
+++ b/tests/lean/tst10.lean
@@ -14,13 +14,10 @@ print a ∨ b
print (or a b)
print or a (or a b)
-- Simple Formulas
-print a => b => a
-check a => b
-eval a => a
-eval true => a
+print a → b → a
+check a → b
+eval a → a
+eval true → a
-- Simple proof
axiom H1 : a
-axiom H2 : a => b
-check @mp
-print mp H2 H1
-check mp H2 H1
+axiom H2 : a → b
diff --git a/tests/lean/tst10.lean.expected.out b/tests/lean/tst10.lean.expected.out
index 4c1d64f48..3ad203a8e 100644
--- a/tests/lean/tst10.lean.expected.out
+++ b/tests/lean/tst10.lean.expected.out
@@ -13,12 +13,9 @@ a ∨ b
a ∨ b
a ∨ b
a ∨ a ∨ b
-a ⇒ b ⇒ a
-a ⇒ b : Bool
-if a a ⊤
-if ⊤ a ⊤
+a → b → a
+a → b : Bool
+a → a
+⊤ → a
Assumed: H1
Assumed: H2
-@mp : Π (a b : Bool), (a ⇒ b) → a → b
-H2 ◂ H1
-H2 ◂ H1 : b
diff --git a/tests/lean/tst11.lean.expected.out b/tests/lean/tst11.lean.expected.out
index d161d3388..216238d02 100644
--- a/tests/lean/tst11.lean.expected.out
+++ b/tests/lean/tst11.lean.expected.out
@@ -6,7 +6,7 @@
⊤
Assumed: a
a ⊕ a ⊕ a
-@subst : Π (A : TypeU) (a b : A) (P : A → Bool), P a → a == b → P b
+@subst : ∀ (A : TypeU) (a b : A) (P : A → Bool), P a → a == b → P b
Proved: EM2
-EM2 : Π a : Bool, a ∨ ¬ a
+EM2 : ∀ a : Bool, a ∨ ¬ a
EM2 a : a ∨ ¬ a
diff --git a/tests/lean/tst12.lean b/tests/lean/tst12.lean
index ac798c02f..5b32e27b4 100644
--- a/tests/lean/tst12.lean
+++ b/tests/lean/tst12.lean
@@ -2,14 +2,14 @@ print (fun x : Bool, (fun y : Bool, x /\ y))
print let x := true,
y := true
in (let z := x /\ y,
- f := (fun arg1 arg2 : Bool, arg1 /\ arg2 <=>
- arg2 /\ arg1 <=>
+ f := (fun arg1 arg2 : Bool, arg1 /\ arg2 =
+ arg2 /\ arg1 =
arg1 \/ arg2 \/ arg2)
in (f x y) \/ z)
eval let x := true,
y := true,
z := x /\ y,
- f := (fun arg1 arg2 : Bool, arg1 /\ arg2 <=>
- arg2 /\ arg1 <=>
+ f := (fun arg1 arg2 : Bool, arg1 /\ arg2 =
+ arg2 /\ arg1 =
arg1 \/ arg2 \/ arg2)
in (f x y) \/ z
diff --git a/tests/lean/tst12.lean.expected.out b/tests/lean/tst12.lean.expected.out
index dc10413e4..6aaf0e525 100644
--- a/tests/lean/tst12.lean.expected.out
+++ b/tests/lean/tst12.lean.expected.out
@@ -4,6 +4,6 @@
let x := ⊤,
y := ⊤,
z := x ∧ y,
- f := λ arg1 arg2 : Bool, arg1 ∧ arg2 ⇔ arg2 ∧ arg1 ⇔ arg1 ∨ arg2 ∨ arg2
+ f := λ arg1 arg2 : Bool, arg1 ∧ arg2 = arg2 ∧ arg1 = arg1 ∨ arg2 ∨ arg2
in f x y ∨ z
⊤
diff --git a/tests/lean/tst13.lean b/tests/lean/tst13.lean
index 2c07e525f..56367f583 100644
--- a/tests/lean/tst13.lean
+++ b/tests/lean/tst13.lean
@@ -2,7 +2,7 @@ print fun x : Bool, (fun x : Bool, x).
print let x := true,
y := true
in (let z := x /\ y,
- f := (fun x y : Bool, x /\ y <=>
- y /\ x <=>
+ f := (fun x y : Bool, x /\ y =
+ y /\ x =
x \/ y \/ y)
in (f x y) \/ z)
diff --git a/tests/lean/tst13.lean.expected.out b/tests/lean/tst13.lean.expected.out
index 856ad6996..e751e01ac 100644
--- a/tests/lean/tst13.lean.expected.out
+++ b/tests/lean/tst13.lean.expected.out
@@ -1,4 +1,4 @@
Set: pp::colors
Set: pp::unicode
λ 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
+let x := ⊤, y := ⊤, z := x ∧ y, f := λ x y : Bool, x ∧ y = y ∧ x = x ∨ y ∨ y in f x y ∨ z
diff --git a/tests/lean/tst16.lean b/tests/lean/tst16.lean
index f42f460be..ebfefd24d 100644
--- a/tests/lean/tst16.lean
+++ b/tests/lean/tst16.lean
@@ -3,7 +3,7 @@ print forall a b : Type, (f a) = (f b)
variable g : Bool -> Bool -> Bool
print forall (a b : Type) (c : Bool), g c ((f a) = (f b))
print exists (a b : Type) (c : Bool), g c ((f a) = (f b))
-print forall (a b : Type) (c : Bool), (g c (f a) = (f b)) ⇒ (f a)
+print forall (a b : Type) (c : Bool), (g c (f a) = (f b)) -> (f a)
check forall (a b : Type) (c : Bool), g c ((f a) = (f b))
print ∀ (a b : Type) (c : Bool), g c ((f a) = (f b))
print ∀ a b : Type, (f a) = (f b)
diff --git a/tests/lean/tst16.lean.expected.out b/tests/lean/tst16.lean.expected.out
index 7089f5aac..125ced330 100644
--- a/tests/lean/tst16.lean.expected.out
+++ b/tests/lean/tst16.lean.expected.out
@@ -5,7 +5,7 @@
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
+∀ (a b : Type) (c : Bool), g c (f a) = f b → f a
∀ (a b : Type) (c : Bool), g c (f a = f b) : Bool
∀ (a b : Type) (c : Bool), g c (f a = f b)
∀ a b : Type, f a = f b
diff --git a/tests/lean/tst17.lean.expected.out b/tests/lean/tst17.lean.expected.out
index 25cf4e9ed..6c7a9feea 100644
--- a/tests/lean/tst17.lean.expected.out
+++ b/tests/lean/tst17.lean.expected.out
@@ -4,6 +4,4 @@
Assumed: g
∀ a b : Type, ∃ c : Type, g a b = f c
∀ a b : Type, ∃ c : Type, g a b = f c : Bool
-(λ a : Type,
- (λ b : Type, if ((λ x : Type, if (g a b == f x) ⊥ ⊤) == (λ x : Type, ⊤)) ⊥ ⊤) == (λ x : Type, ⊤)) ==
-(λ x : Type, ⊤)
+∀ (a b : Type), (∀ (x : Type), g a b == f x → ⊥) → ⊥
diff --git a/tests/lean/tst4.lean.expected.out b/tests/lean/tst4.lean.expected.out
index 54af34420..e9365109c 100644
--- a/tests/lean/tst4.lean.expected.out
+++ b/tests/lean/tst4.lean.expected.out
@@ -10,7 +10,7 @@
Assumed: EqNice
@EqNice N n1 n2
@f N n1 n2 : N
-@congr : Π (A : TypeU) (B : A → TypeU) (f g : Π x : A, B x) (a b : A), f == g → a == b → f a == g b
+@congr : ∀ (A : TypeU) (B : A → TypeU) (f g : ∀ x : A, B x) (a b : A), f == g → a == b → f a == g b
@f N n1 n2
Assumed: a
Assumed: b
diff --git a/tests/lean/tst7.lean b/tests/lean/tst7.lean
index f6c6f9fe3..7b8376944 100644
--- a/tests/lean/tst7.lean
+++ b/tests/lean/tst7.lean
@@ -1,17 +1,17 @@
-variable f : Pi (A : Type), A -> Bool
+variable f : forall (A : Type), A -> Bool
print fun (A B : Type) (a : _), f B a
-- The following one should produce an error
print fun (A : Type) (a : _) (B : Type), f B a
-variable myeq : Pi A : (Type U), A -> A -> Bool
+variable myeq : forall A : (Type U), A -> A -> Bool
print myeq _ (fun (A : Type) (a : _), a) (fun (B : Type) (b : B), b)
check myeq _ (fun (A : Type) (a : _), a) (fun (B : Type) (b : B), b)
variable R : Type -> Bool
-variable h : (Pi (A : Type), R A) -> Bool
+variable h : (forall (A : Type), R A) -> Bool
check (fun (H : Bool)
- (f1 : Pi (A : Type), R _)
- (g1 : Pi (A : Type), R A)
- (G : Pi (A : Type), myeq _ (f1 _) (g1 A)),
+ (f1 : forall (A : Type), R _)
+ (g1 : forall (A : Type), R A)
+ (G : forall (A : Type), myeq _ (f1 _) (g1 A)),
h f1)
diff --git a/tests/lean/tst7.lean.expected.out b/tests/lean/tst7.lean.expected.out
index cfd1737bf..3caee97fc 100644
--- a/tests/lean/tst7.lean.expected.out
+++ b/tests/lean/tst7.lean.expected.out
@@ -10,9 +10,9 @@ A : Type, a : ?M::0, B : Type ⊢ ?M::0[lift:0:2] ≺ B
B
a
Assumed: myeq
-myeq (Π (A : Type), A → A) (λ (A : Type) (a : A), a) (λ (B : Type) (b : B), b)
-myeq (Π (A : Type), A → A) (λ (A : Type) (a : A), a) (λ (B : Type) (b : B), b) : Bool
+myeq (∀ (A : Type), A → A) (λ (A : Type) (a : A), a) (λ (B : Type) (b : B), b)
+myeq (∀ (A : Type), A → A) (λ (A : Type) (a : A), a) (λ (B : Type) (b : B), b) : Bool
Assumed: R
Assumed: h
-λ (H : Bool) (f1 g1 : Π A : Type, R A) (G : Π A : Type, myeq (R A) (f1 A) (g1 A)), h f1 :
- Bool → (Π (f1 g1 : Π A : Type, R A), (Π A : Type, myeq (R A) (f1 A) (g1 A)) → Bool)
+λ (H : Bool) (f1 g1 : ∀ A : Type, R A) (G : ∀ A : Type, myeq (R A) (f1 A) (g1 A)), h f1 :
+ Bool → (∀ (f1 g1 : ∀ A : Type, R A), (∀ A : Type, myeq (R A) (f1 A) (g1 A)) → Bool)
diff --git a/tests/lean/tst8.lean b/tests/lean/tst8.lean
index 5340ae5c8..5d32c19ef 100644
--- a/tests/lean/tst8.lean
+++ b/tests/lean/tst8.lean
@@ -3,7 +3,7 @@ check fun (A : Type) (a : A),
let b := a
in b
-variable g : Pi A : Type, A -> A
+variable g : forall A : Type, A -> A
definition f (A: Type) (a : A) : A :=
let b := g A a,
diff --git a/tests/lean/tst8.lean.expected.out b/tests/lean/tst8.lean.expected.out
index 65f1f6e69..604aee8ac 100644
--- a/tests/lean/tst8.lean.expected.out
+++ b/tests/lean/tst8.lean.expected.out
@@ -1,7 +1,7 @@
Set: pp::colors
Set: pp::unicode
Imported 'Int'
-λ (A : Type) (a : A), let b := a in b : Π (A : Type), A → A
+λ (A : Type) (a : A), let b := a in b : ∀ (A : Type), A → A
Assumed: g
Defined: f
f ℕ 10
diff --git a/tests/lean/tst9.lean b/tests/lean/tst9.lean
index 3bc77d7f0..ab7c8e521 100644
--- a/tests/lean/tst9.lean
+++ b/tests/lean/tst9.lean
@@ -1,4 +1,4 @@
-variable f : Pi A : Type, A -> A -> A
+variable f : forall A : Type, A -> A -> A
variable N : Type
variable g : N -> N -> Bool
variable a : N
diff --git a/tests/lean/type_inf_bug1.lean b/tests/lean/type_inf_bug1.lean
index 8dd251ec7..eb1f1e326 100644
--- a/tests/lean/type_inf_bug1.lean
+++ b/tests/lean/type_inf_bug1.lean
@@ -12,11 +12,11 @@ check fun (A A': TypeM)
check fun (A A': TypeM)
(B : A -> TypeM)
(B' : A' -> TypeM)
- (f : Pi x : A, B x)
- (g : Pi x : A', B' x)
+ (f : forall x : A, B x)
+ (g : forall x : A', B' x)
(a : A)
(b : A')
- (H1 : (Pi x : A, B x) == (Pi x : A', B' x))
+ (H1 : (forall x : A, B x) == (forall x : A', B' x))
(H2 : f == g)
(H3 : a == b),
let L1 : A == A' := dominj H1,
@@ -25,8 +25,8 @@ check fun (A A': TypeM)
L3 : b == b' := cast::eq L2 b,
L4 : a == b' := htrans H3 L3,
L5 : f a == f b' := congr2 f L4,
- S1 : (Pi x : A', B' x) == (Pi x : A, B x) := symm H1,
- g' : (Pi x : A, B x) := cast S1 g,
+ S1 : (forall x : A', B' x) == (forall x : A, B x) := symm H1,
+ g' : (forall x : A, B x) := cast S1 g,
L6 : g == g' := cast::eq S1 g,
L7 : f == g' := htrans H2 L6,
L8 : f b' == g' b' := congr1 b' L7,
diff --git a/tests/lean/type_inf_bug1.lean.expected.out b/tests/lean/type_inf_bug1.lean.expected.out
index 2947a7c3c..9da17743b 100644
--- a/tests/lean/type_inf_bug1.lean.expected.out
+++ b/tests/lean/type_inf_bug1.lean.expected.out
@@ -3,15 +3,15 @@
Imported 'cast'
Set: pp::colors
λ (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), let b' : A := cast L2 b, L3 : b == b' := cast::eq L2 b in L3 :
- Π (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), b == cast L2 b
+ ∀ (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), b == cast L2 b
λ (A A' : TypeM)
(B : A → TypeM)
(B' : A' → TypeM)
- (f : Π x : A, B x)
- (g : Π x : A', B' x)
+ (f : ∀ x : A, B x)
+ (g : ∀ x : A', B' x)
(a : A)
(b : A')
- (H1 : (Π x : A, B x) == (Π x : A', B' x))
+ (H1 : (∀ x : A, B x) == (∀ x : A', B' x))
(H2 : f == g)
(H3 : a == b),
let L1 : A == A' := dominj H1,
@@ -20,19 +20,19 @@
L3 : b == b' := cast::eq L2 b,
L4 : a == b' := htrans H3 L3,
L5 : f a == f b' := congr2 f L4,
- S1 : (Π x : A', B' x) == (Π x : A, B x) := symm H1,
- g' : Π x : A, B x := cast S1 g,
+ S1 : (∀ x : A', B' x) == (∀ x : A, B x) := symm H1,
+ g' : ∀ x : A, B x := cast S1 g,
L6 : g == g' := cast::eq S1 g,
L7 : f == g' := htrans H2 L6,
L8 : f b' == g' b' := congr1 b' L7,
L9 : f a == g' b' := htrans L5 L8
in L9 :
- Π (A A' : TypeM)
+ ∀ (A A' : TypeM)
(B : A → TypeM)
(B' : A' → TypeM)
- (f : Π x : A, B x)
- (g : Π x : A', B' x)
+ (f : ∀ x : A, B x)
+ (g : ∀ x : A', B' x)
(a : A)
(b : A')
- (H1 : (Π x : A, B x) == (Π x : A', B' x)),
+ (H1 : (∀ x : A, B x) == (∀ x : A', B' x)),
f == g → a == b → f a == cast (symm H1) g (cast (symm (dominj H1)) b)