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

feat(*): change name conventions for Lean builtin libraries

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-01-05 19:10:21 -08:00
parent 771b099c0c
commit 935c2a03a3
130 changed files with 927 additions and 965 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
doc/lean/calc.md
View file

@ -17,7 +17,7 @@ may also be of the form `{ <pr> }`, where `<pr>` is a proof
for some equality `a = b`. The form `{ <pr> }` is just syntax sugar for some equality `a = b`. The form `{ <pr> }` is just syntax sugar
for for
Subst (Refl <expr>_{i-1}) <pr> subst (refl <expr>_{i-1}) <pr>
That is, we are claiming we can obtain `<expr>_i` by replacing `a` with `b` That is, we are claiming we can obtain `<expr>_i` by replacing `a` with `b`
in `<expr>_{i-1}`. in `<expr>_{i-1}`.
@ -35,8 +35,8 @@ Here is an example
:= calc a = b : Ax1 := calc a = b : Ax1
... = c + 1 : Ax2 ... = c + 1 : Ax2
... = d + 1 : { Ax3 } ... = d + 1 : { Ax3 }
... = 1 + d : Nat::PlusComm d 1 ... = 1 + d : Nat::plus::comm d 1
... = e : Symm Ax4. ... = e : symm Ax4.
``` ```
The proof expressions `<proof>_i` do not need to be explicitly provided. The proof expressions `<proof>_i` do not need to be explicitly provided.
@ -45,7 +45,7 @@ proof expression using the given tactic or solver.
Even when tactics and solvers are not used, we can still use the elaboration engine to fill Even when tactics and solvers are not used, we can still use the elaboration engine to fill
gaps in our calculational proofs. In the previous examples, we can use `_` as arguments for the gaps in our calculational proofs. In the previous examples, we can use `_` as arguments for the
`Nat::PlusComm` theorem. The Lean elaboration engine will infer `d` and `1` for us. `Nat::plus::comm` theorem. The Lean elaboration engine will infer `d` and `1` for us.
Here is the same example using placeholders. Here is the same example using placeholders.
```lean ```lean
@ -53,8 +53,8 @@ Here is the same example using placeholders.
:= calc a = b : Ax1 := calc a = b : Ax1
... = c + 1 : Ax2 ... = c + 1 : Ax2
... = d + 1 : { Ax3 } ... = d + 1 : { Ax3 }
... = 1 + d : Nat::PlusComm _ _ ... = 1 + d : Nat::plus::comm _ _
... = e : Symm Ax4. ... = e : symm Ax4.
``` ```
We can also use the operators `=>`, `⇒`, `<=>`, `⇔` and `≠` in calculational proofs. We can also use the operators `=>`, `⇒`, `<=>`, `⇔` and `≠` in calculational proofs.
@ -64,7 +64,7 @@ Here is an example.
theorem T2 (a b c : Nat) (H1 : a = b) (H2 : b = c + 1) : a ≠ 0 theorem T2 (a b c : Nat) (H1 : a = b) (H2 : b = c + 1) : a ≠ 0
:= calc a = b : H1 := calc a = b : H1
... = c + 1 : H2 ... = c + 1 : H2
... ≠ 0 : Nat::SuccNeZero _. ... ≠ 0 : Nat::succ::nz _.
``` ```
The Lean `let` construct can also be used to build calculational-like proofs. The Lean `let` construct can also be used to build calculational-like proofs.
@ -75,9 +75,9 @@ The Lean `let` construct can also be used to build calculational-like proofs.
axiom Axf (a : Nat) : f (f a) = a. axiom Axf (a : Nat) : f (f a) = a.
theorem T3 (a b : Nat) (H : P (f (f (f (f a)))) (f (f b))) : P a b theorem T3 (a b : Nat) (H : P (f (f (f (f a)))) (f (f b))) : P a b
:= let s1 : P (f (f a)) (f (f b)) := Subst H (Axf a), := let s1 : P (f (f a)) (f (f b)) := subst H (Axf a),
s2 : P a (f (f b)) := Subst s1 (Axf a), s2 : P a (f (f b)) := subst s1 (Axf a),
s3 : P a b := Subst s2 (Axf b) s3 : P a b := subst s2 (Axf b)
in s3. in s3.
``` ```

30
examples/lean/even.lean
View file

@ -8,19 +8,19 @@ definition odd (a : Nat) := ∃ b, a = 2*b + 1.
-- Prove that the sum of two even numbers is even. -- Prove that the sum of two even numbers is even.
-- --
-- Notes: we use the macro -- Notes: we use the macro
-- Obtain [bindings] ',' 'from' [expr]_1 ',' [expr]_2 -- obtain [bindings] ',' 'from' [expr]_1 ',' [expr]_2
-- --
-- It is syntax sugar for existential elimination. -- It is syntax sugar for existential elimination.
-- It expands to -- It expands to
-- --
-- ExistsElim [expr]_1 (fun [binding], [expr]_2) -- exists::elim [expr]_1 (fun [binding], [expr]_2)
-- --
-- It is defined in the file macros.lua. -- It is defined in the file macros.lua.
-- --
-- We also use the calculational proof style. -- We also use the calculational proof style.
-- See doc/lean/calc.md for more information. -- See doc/lean/calc.md for more information.
-- --
-- We use the first two Obtain-expressions to extract the -- We use the first two obtain-expressions to extract the
-- witnesses w1 and w2 s.t. a = 2*w1 and b = 2*w2. -- witnesses w1 and w2 s.t. a = 2*w1 and b = 2*w2.
-- We can do that because H1 and H2 are evidence/proof for the -- We can do that because H1 and H2 are evidence/proof for the
-- fact that 'a' and 'b' are even. -- fact that 'a' and 'b' are even.
@ -29,12 +29,12 @@ definition odd (a : Nat) := ∃ b, a = 2*b + 1.
-- the witness w1+w2 for the fact that a+b is also even. -- the witness w1+w2 for the fact that a+b is also even.
-- That is, we provide a derivation showing that a+b = 2*(w1 + w2) -- That is, we provide a derivation showing that a+b = 2*(w1 + w2)
theorem EvenPlusEven {a b : Nat} (H1 : even a) (H2 : even b) : even (a + b) theorem EvenPlusEven {a b : Nat} (H1 : even a) (H2 : even b) : even (a + b)
:= Obtain (w1 : Nat) (Hw1 : a = 2*w1), from H1, := obtain (w1 : Nat) (Hw1 : a = 2*w1), from H1,
Obtain (w2 : Nat) (Hw2 : b = 2*w2), from H2, obtain (w2 : Nat) (Hw2 : b = 2*w2), from H2,
ExistsIntro (w1 + w2) exists::intro (w1 + w2)
(calc a + b = 2*w1 + b : { Hw1 } (calc a + b = 2*w1 + b : { Hw1 }
... = 2*w1 + 2*w2 : { Hw2 } ... = 2*w1 + 2*w2 : { Hw2 }
... = 2*(w1 + w2) : Symm (Nat::Distribute 2 w1 w2)). ... = 2*(w1 + w2) : symm (Nat::distribute 2 w1 w2)).
-- In the following example, we omit the arguments for Nat::PlusAssoc, Refl and Nat::Distribute. -- In the following example, we omit the arguments for Nat::PlusAssoc, Refl and Nat::Distribute.
-- Lean can infer them automatically. -- Lean can infer them automatically.
@ -50,12 +50,12 @@ theorem EvenPlusEven {a b : Nat} (H1 : even a) (H2 : even b) : even (a + b)
-- is left associative. Moreover, Lean normalizer does not use -- is left associative. Moreover, Lean normalizer does not use
-- any theorems such as + associativity. -- any theorems such as + associativity.
theorem OddPlusOne {a : Nat} (H : odd a) : even (a + 1) theorem OddPlusOne {a : Nat} (H : odd a) : even (a + 1)
:= Obtain (w : Nat) (Hw : a = 2*w + 1), from H, := obtain (w : Nat) (Hw : a = 2*w + 1), from H,
ExistsIntro (w + 1) exists::intro (w + 1)
(calc a + 1 = 2*w + 1 + 1 : { Hw } (calc a + 1 = 2*w + 1 + 1 : { Hw }
... = 2*w + (1 + 1) : Symm (Nat::PlusAssoc _ _ _) ... = 2*w + (1 + 1) : symm (Nat::plus::assoc _ _ _)
... = 2*w + 2*1 : Refl _ ... = 2*w + 2*1 : refl _
... = 2*(w + 1) : Symm (Nat::Distribute _ _ _)). ... = 2*(w + 1) : symm (Nat::distribute _ _ _)).
-- The following command displays the proof object produced by Lean after -- The following command displays the proof object produced by Lean after
-- expanding macros, and infering implicit/missing arguments. -- expanding macros, and infering implicit/missing arguments.

12
examples/lean/ex1.lean
View file

@ -2,8 +2,8 @@ variable N : Type
variable h : N -> N -> N variable h : N -> N -> N
-- Specialize congruence theorem for h-applications -- Specialize congruence theorem for h-applications
theorem CongrH {a1 a2 b1 b2 : N} (H1 : a1 = b1) (H2 : a2 = b2) : (h a1 a2) = (h b1 b2) := theorem congrh {a1 a2 b1 b2 : N} (H1 : a1 = b1) (H2 : a2 = b2) : (h a1 a2) = (h b1 b2) :=
Congr (Congr (Refl h) H1) H2 congr (congr (refl h) H1) H2
-- Declare some variables -- Declare some variables
variable a : N variable a : N
@ -18,13 +18,13 @@ axiom H2 : b = e
-- Proof that (h a b) = (h c e) -- Proof that (h a b) = (h c e)
theorem T1 : (h a b) = (h c e) := theorem T1 : (h a b) = (h c e) :=
DisjCases H1 or::elim H1
(λ C1, CongrH (Trans (Conjunct1 C1) (Conjunct2 C1)) H2) (λ C1, congrh ((and::eliml C1) ⋈ (and::elimr C1)) H2)
(λ C2, CongrH (Trans (Conjunct2 C2) (Conjunct1 C2)) H2) (λ C2, congrh ((and::elimr C2) ⋈ (and::eliml C2)) H2)
-- We can use theorem T1 to prove other theorems -- We can use theorem T1 to prove other theorems
theorem T2 : (h a (h a b)) = (h a (h c e)) := theorem T2 : (h a (h a b)) = (h a (h c e)) :=
CongrH (Refl a) T1 congrh (refl a) T1
-- Display the last two objects (i.e., theorems) added to the environment -- Display the last two objects (i.e., theorems) added to the environment
print environment 2 print environment 2

15
examples/lean/ex2.lean
View file

@ -1,19 +1,16 @@
import macros. import macros.
theorem simple (p q r : Bool) : (p ⇒ q) ∧ (q ⇒ r) ⇒ p ⇒ r theorem simple (p q r : Bool) : (p ⇒ q) ∧ (q ⇒ r) ⇒ p ⇒ r
:= Assume H_pq_qr H_p, := assume H_pq_qr H_p,
let P_pq := Conjunct1 H_pq_qr, let P_pq := and::eliml H_pq_qr,
P_qr := Conjunct2 H_pq_qr, P_qr := and::elimr H_pq_qr
P_q := MP P_pq H_p in P_qr ◂ (P_pq ◂ H_p)
in MP P_qr P_q.
setoption pp::implicit true. setoption pp::implicit true.
print environment 1. print environment 1.
theorem simple2 (a b c : Bool) : (a ⇒ b ⇒ c) ⇒ (a ⇒ b) ⇒ a ⇒ c theorem simple2 (a b c : Bool) : (a ⇒ b ⇒ c) ⇒ (a ⇒ b) ⇒ a ⇒ c
:= Assume H_abc H_ab H_a, := assume H_abc H_ab H_a,
let P_b := (MP H_ab H_a), (H_abc ◂ H_a) ◂ (H_ab ◂ H_a)
P_bc := (MP H_abc H_a)
in MP P_bc P_b.
print environment 1. print environment 1.

22
examples/lean/ex3.lean
View file

@ -1,28 +1,28 @@
import macros. import macros.
theorem and_comm (a b : Bool) : (a ∧ b) ⇒ (b ∧ a) theorem and_comm (a b : Bool) : (a ∧ b) ⇒ (b ∧ a)
:= Assume H_ab, Conj (Conjunct2 H_ab) (Conjunct1 H_ab). := assume H_ab, and::intro (and::elimr H_ab) (and::eliml H_ab).
theorem or_comm (a b : Bool) : (a ∨ b) ⇒ (b ∨ a) theorem or_comm (a b : Bool) : (a ∨ b) ⇒ (b ∨ a)
:= Assume H_ab, := assume H_ab,
DisjCases H_ab or::elim H_ab
(λ H_a, Disj2 b H_a) (λ H_a, or::intror b H_a)
(λ H_b, Disj1 H_b a). (λ H_b, or::introl H_b a).
-- (EM a) is the excluded middle a ∨ ¬a -- (em a) is the excluded middle a ∨ ¬a
-- (MT H H_na) is Modus Tollens with -- (mt H H_na) is Modus Tollens with
-- H : (a ⇒ b) ⇒ a) -- H : (a ⇒ b) ⇒ a)
-- H_na : ¬a -- H_na : ¬a
-- produces -- produces
-- ¬(a ⇒ b) -- ¬(a ⇒ b)
-- --
-- NotImp1 applied to -- not::imp::eliml applied to
-- (MT H H_na) : ¬(a ⇒ b) -- (MT H H_na) : ¬(a ⇒ b)
-- produces -- produces
-- a -- a
theorem pierce (a b : Bool) : ((a ⇒ b) ⇒ a) ⇒ a theorem pierce (a b : Bool) : ((a ⇒ b) ⇒ a) ⇒ a
:= Assume H, DisjCases (EM a) := assume H, or::elim (em a)
(λ H_a, H_a) (λ H_a, H_a)
(λ H_na, NotImp1 (MT H H_na)). (λ H_na, not::imp::eliml (mt H H_na)).
print environment 3. print environment 3.

6
examples/lean/ex4.lean
View file

@ -2,7 +2,7 @@ import Int
import tactic import tactic
definition a : Nat := 10 definition a : Nat := 10
-- Trivial indicates a "proof by evaluation" -- Trivial indicates a "proof by evaluation"
theorem T1 : a > 0 := Trivial theorem T1 : a > 0 := trivial
theorem T2 : a - 5 > 3 := Trivial theorem T2 : a - 5 > 3 := trivial
-- The next one is commented because it fails -- The next one is commented because it fails
-- theorem T3 : a > 11 := Trivial -- theorem T3 : a > 11 := trivial

65
examples/lean/ex5.lean
View file

@ -1,72 +1,49 @@
import macros
scope scope
theorem ReflIf (A : Type) theorem ReflIf (A : Type)
(R : A → A → Bool) (R : A → A → Bool)
(Symmetry : Π x y, R x y → R y x) (Symm : Π x y, R x y → R y x)
(Transitivity : Π x y z, R x y → R y z → R x z) (Trans : Π x y z, R x y → R y z → R x z)
(Linked : Π x, ∃ y, R x y) (Linked : Π x, ∃ y, R x y)
: :
Π x, R x x := Π x, R x x :=
fun x, ExistsElim (Linked x) λ x, obtain (w : A) (H : R x w), from (Linked x),
(fun (w : A) (H : R x w), let L1 : R w x := Symm x w H
let L1 : R w x := Symmetry x w H in Trans x w x H L1
in Transitivity x w x H L1)
pop::scope pop::scope
scope scope
-- Same example but using ∀ instead of Π and ⇒ instead of → -- Same example but using ∀ instead of Π and ⇒ instead of →.
-- Remark: H ↓ x is syntax sugar for forall::elim H x
-- Remark: H1 ◂ H2 is syntax sugar for mp H1 H2
theorem ReflIf (A : Type) theorem ReflIf (A : Type)
(R : A → A → Bool) (R : A → A → Bool)
(Symmetry : ∀ x y, R x y ⇒ R y x) (Symm : ∀ x y, R x y ⇒ R y x)
(Transitivity : ∀ x y z, R x y ⇒ R y z ⇒ R x z) (Trans : ∀ x y z, R x y ⇒ R y z ⇒ R x z)
(Linked : ∀ x, ∃ y, R x y) (Linked : ∀ x, ∃ y, R x y)
: :
∀ x, R x x := ∀ x, R x x :=
ForallIntro (fun x, take x, obtain (w : A) (H : R x w), from (Linked ↓ x),
ExistsElim (ForallElim Linked x) let L1 : R w x := Symm ↓ x ↓ w ◂ H
(fun (w : A) (H : R x w), in Trans ↓ x ↓ w ↓ x ◂ H ◂ L1
let L1 : R w x := (MP (ForallElim (ForallElim Symmetry x) w) H)
in (MP (MP (ForallElim (ForallElim (ForallElim Transitivity x) w) x) H) L1)))
-- We can make the previous example less verbose by using custom notation
infixl 50 ! : ForallElim
infixl 30 << : MP
theorem ReflIf2 (A : Type)
(R : A → A → Bool)
(Symmetry : ∀ x y, R x y ⇒ R y x)
(Transitivity : ∀ x y z, R x y ⇒ R y z ⇒ R x z)
(Linked : ∀ x, ∃ y, R x y)
:
∀ x, R x x :=
ForallIntro (fun x,
ExistsElim (Linked ! x)
(fun (w : A) (H : R x w),
let L1 : R w x := Symmetry ! x ! w << H
in Transitivity ! x ! w ! x << H << L1))
print environment 1
pop::scope pop::scope
scope scope
-- Same example again. -- Same example again.
variable A : Type variable A : Type
variable R : A → A → Bool variable R : A → A → Bool
axiom Symmetry {x y : A} : R x y → R y x axiom Symm {x y : A} : R x y → R y x
axiom Transitivity {x y z : A} : R x y → R y z → R x z axiom Trans {x y z : A} : R x y → R y z → R x z
axiom Linked (x : A) : ∃ y, R x y axiom Linked (x : A) : ∃ y, R x y
theorem ReflIf (x : A) : R x x := theorem ReflIf (x : A) : R x x :=
ExistsElim (Linked x) (fun (w : A) (H : R x w), obtain (w : A) (H : R x w), from (Linked x),
let L1 : R w x := Symmetry H let L1 : R w x := Symm H
in Transitivity H L1) in Trans H L1
-- Even more compact proof of the same theorem
theorem ReflIf2 (x : A) : R x x :=
ExistsElim (Linked x) (fun w H, Transitivity H (Symmetry H))
-- The command Endscope exports both theorem to the main scope
-- The variables and axioms in the scope become parameters to both theorems.
end end
-- Display the last two theorems -- Display the last two theorems

41
examples/lean/set.lean
View file

@ -8,31 +8,30 @@ 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 infix 50 ⊆ : subset
theorem SubsetTrans (A : Type) : ∀ s1 s2 s3 : Set A, s1 ⊆ s2 ⇒ s2 ⊆ s3 ⇒ s1 ⊆ s3 := 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), take s1 s2 s3, assume (H1 : s1 ⊆ s2) (H2 : s2 ⊆ s3),
have s1 ⊆ s3 : have s1 ⊆ s3 :
take x, Assume Hin : x ∈ s1, take x, assume Hin : x ∈ s1,
have x ∈ s3 : have x ∈ s3 :
let L1 : x ∈ s2 := MP (Instantiate H1 x) Hin let L1 : x ∈ s2 := H1 ↓ x ◂ Hin
in MP (Instantiate H2 x) L1 in H2 ↓ x ◂ L1
theorem SubsetExt (A : Type) : ∀ s1 s2 : Set A, (∀ x, x ∈ s1 = x ∈ s2) ⇒ s1 = s2 := 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), take s1 s2, assume (H : ∀ x, x ∈ s1 = x ∈ s2),
Abst (fun x, Instantiate H x) abst (λ x, H ↓ x)
theorem SubsetAntiSymm (A : Type) : ∀ s1 s2 : Set A, s1 ⊆ s2 ⇒ s2 ⊆ s1 ⇒ s1 = s2 := 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), take s1 s2, assume (H1 : s1 ⊆ s2) (H2 : s2 ⊆ s1),
have s1 = s2 : have s1 = s2 :
MP (have (∀ x, x ∈ s1 = x ∈ s2) ⇒ s1 = s2 : (have (∀ x, x ∈ s1 = x ∈ s2) ⇒ s1 = s2 :
Instantiate (SubsetExt A) s1 s2) (subset::ext A) ↓ s1 ↓ s2)
(have (∀ x, x ∈ s1 = x ∈ s2) : ◂ (have (∀ x, x ∈ s1 = x ∈ s2) :
take x, have x ∈ s1 = x ∈ s2 : take x, have x ∈ s1 = x ∈ s2 :
let L1 : x ∈ s1 ⇒ x ∈ s2 := Instantiate H1 x, iff::intro (have x ∈ s1 ⇒ x ∈ s2 : H1 ↓ x)
L2 : x ∈ s2 ⇒ x ∈ s1 := Instantiate H2 x (have x ∈ s2 ⇒ x ∈ s1 : H2 ↓ x))
in ImpAntisym L1 L2)
-- Compact (but less readable) version of the previous theorem -- Compact (but less readable) version of the previous theorem
theorem SubsetAntiSymm2 (A : Type) : ∀ s1 s2 : Set A, s1 ⊆ s2 ⇒ s2 ⊆ s1 ⇒ s1 = s2 := theorem subset::antisym2 (A : Type) : ∀ s1 s2 : Set A, s1 ⊆ s2 ⇒ s2 ⊆ s1 ⇒ s1 = s2 :=
take s1 s2, Assume H1 H2, take s1 s2, assume H1 H2,
MP (Instantiate (SubsetExt A) s1 s2) (subset::ext A) ↓ s1 ↓ s2 ◂ (take x, iff::intro (H1 ↓ x) (H2 ↓ x))
(take x, ImpAntisym (Instantiate H1 x) (Instantiate H2 x))

4
examples/lean/tactic1.lean
View file

@ -1,10 +1,8 @@
-- This example demonstrates how to specify a proof skeleton that contains -- This example demonstrates how to specify a proof skeleton that contains
-- "holes" that must be filled using user-defined tactics. -- "holes" that must be filled using user-defined tactics.
import tactic
(* (*
-- import useful macros for creating tactics
import("tactic.lua")
-- Define a simple tactic using Lua -- Define a simple tactic using Lua
auto = Repeat(OrElse(assumption_tac(), conj_tac(), conj_hyp_tac())) auto = Repeat(OrElse(assumption_tac(), conj_tac(), conj_hyp_tac()))

2
examples/lean/tactic_in_lua.lean
View file

@ -42,7 +42,7 @@
local pb = s:proof_builder() local pb = s:proof_builder()
local new_pb = local new_pb =
function(m, a) function(m, a)
local Conj = Const("Conj") local Conj = Const({"and", "intro"})
local new_m = proof_map(m) -- Copy proof map m local new_m = proof_map(m) -- Copy proof map m
for _, p in ipairs(proof_info) do for _, p in ipairs(proof_info) do
local n = p[1] -- n is the name of the goal splitted by this tactic local n = p[1] -- n is the name of the goal splitted by this tactic

310
src/builtin/Nat.lean
View file

@ -30,219 +30,217 @@ infix 50 > : gt
definition id (a : Nat) := a definition id (a : Nat) := a
notation 55 | _ | : id notation 55 | _ | : id
axiom SuccNeZero (a : Nat) : a + 1 ≠ 0 axiom succ::nz (a : Nat) : a + 1 ≠ 0
axiom SuccInj {a b : Nat} (H : a + 1 = b + 1) : a = b axiom succ::inj {a b : Nat} (H : a + 1 = b + 1) : a = b
axiom PlusZero (a : Nat) : a + 0 = a axiom plus::zeror (a : Nat) : a + 0 = a
axiom PlusSucc (a b : Nat) : a + (b + 1) = (a + b) + 1 axiom plus::succr (a b : Nat) : a + (b + 1) = (a + b) + 1
axiom MulZero (a : Nat) : a * 0 = 0 axiom mul::zeror (a : Nat) : a * 0 = 0
axiom MulSucc (a b : Nat) : a * (b + 1) = a * b + a axiom mul::succr (a b : Nat) : a * (b + 1) = a * b + a
axiom LeDef (a b : Nat) : a ≤ b ⇔ ∃ c, a + c = b 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 induction {P : Nat → Bool} (a : Nat) (H1 : P 0) (H2 : Π (n : Nat) (iH : P n), P (n + 1)) : P a
theorem ZeroNeOne : 0 ≠ 1 := Trivial theorem pred::nz' (a : Nat) : a ≠ 0 ⇒ ∃ b, b + 1 = a
:= induction a
theorem NeZeroPred' (a : Nat) : a ≠ 0 ⇒ ∃ b, b + 1 = a (assume H : 0 ≠ 0, false::elim (∃ b, b + 1 = 0) H)
:= Induction a
(Assume H : 0 ≠ 0, FalseElim (∃ b, b + 1 = 0) H)
(λ (n : Nat) (iH : n ≠ 0 ⇒ ∃ b, b + 1 = n), (λ (n : Nat) (iH : n ≠ 0 ⇒ ∃ b, b + 1 = n),
Assume H : n + 1 ≠ 0, assume H : n + 1 ≠ 0,
DisjCases (EM (n = 0)) or::elim (em (n = 0))
(λ Heq0 : n = 0, ExistsIntro 0 (calc 0 + 1 = n + 1 : { Symm Heq0 })) (λ Heq0 : n = 0, exists::intro 0 (calc 0 + 1 = n + 1 : { symm Heq0 }))
(λ Hne0 : n ≠ 0, (λ Hne0 : n ≠ 0,
Obtain (w : Nat) (Hw : w + 1 = n), from (MP iH Hne0), obtain (w : Nat) (Hw : w + 1 = n), from (iH ◂ Hne0),
ExistsIntro (w + 1) (calc w + 1 + 1 = n + 1 : { Hw }))) exists::intro (w + 1) (calc w + 1 + 1 = n + 1 : { Hw })))
theorem NeZeroPred {a : Nat} (H : a ≠ 0) : ∃ b, b + 1 = a theorem pred::nz {a : Nat} (H : a ≠ 0) : ∃ b, b + 1 = a
:= MP (NeZeroPred' a) H := (pred::nz' a) ◂ H
theorem Destruct {B : Bool} {a : Nat} (H1: a = 0 → B) (H2 : Π n, a = n + 1 → B) : B theorem destruct {B : Bool} {a : Nat} (H1: a = 0 → B) (H2 : Π n, a = n + 1 → B) : B
:= DisjCases (EM (a = 0)) := or::elim (em (a = 0))
(λ Heq0 : a = 0, H1 Heq0) (λ Heq0 : a = 0, H1 Heq0)
(λ Hne0 : a ≠ 0, Obtain (w : Nat) (Hw : w + 1 = a), from (NeZeroPred Hne0), (λ Hne0 : a ≠ 0, obtain (w : Nat) (Hw : w + 1 = a), from (pred::nz Hne0),
H2 w (Symm Hw)) H2 w (symm Hw))
theorem ZeroPlus (a : Nat) : 0 + a = a theorem plus::zerol (a : Nat) : 0 + a = a
:= Induction a := induction a
(have 0 + 0 = 0 : Trivial) (have 0 + 0 = 0 : trivial)
(λ (n : Nat) (iH : 0 + n = n), (λ (n : Nat) (iH : 0 + n = n),
calc 0 + (n + 1) = (0 + n) + 1 : PlusSucc 0 n calc 0 + (n + 1) = (0 + n) + 1 : plus::succr 0 n
... = n + 1 : { iH }) ... = n + 1 : { iH })
theorem SuccPlus (a b : Nat) : (a + 1) + b = (a + b) + 1 theorem plus::succl (a b : Nat) : (a + 1) + b = (a + b) + 1
:= Induction b := induction b
(calc (a + 1) + 0 = a + 1 : PlusZero (a + 1) (calc (a + 1) + 0 = a + 1 : plus::zeror (a + 1)
... = (a + 0) + 1 : { Symm (PlusZero a) }) ... = (a + 0) + 1 : { symm (plus::zeror a) })
(λ (n : Nat) (iH : (a + 1) + n = (a + n) + 1), (λ (n : Nat) (iH : (a + 1) + n = (a + n) + 1),
calc (a + 1) + (n + 1) = ((a + 1) + n) + 1 : PlusSucc (a + 1) n calc (a + 1) + (n + 1) = ((a + 1) + n) + 1 : plus::succr (a + 1) n
... = ((a + n) + 1) + 1 : { iH } ... = ((a + n) + 1) + 1 : { iH }
... = (a + (n + 1)) + 1 : { have (a + n) + 1 = a + (n + 1) : Symm (PlusSucc a n) }) ... = (a + (n + 1)) + 1 : { have (a + n) + 1 = a + (n + 1) : symm (plus::succr a n) })
theorem PlusComm (a b : Nat) : a + b = b + a theorem plus::comm (a b : Nat) : a + b = b + a
:= Induction b := induction b
(calc a + 0 = a : PlusZero a (calc a + 0 = a : plus::zeror a
... = 0 + a : Symm (ZeroPlus a)) ... = 0 + a : symm (plus::zerol a))
(λ (n : Nat) (iH : a + n = n + a), (λ (n : Nat) (iH : a + n = n + a),
calc a + (n + 1) = (a + n) + 1 : PlusSucc a n calc a + (n + 1) = (a + n) + 1 : plus::succr a n
... = (n + a) + 1 : { iH } ... = (n + a) + 1 : { iH }
... = (n + 1) + a : Symm (SuccPlus n a)) ... = (n + 1) + a : symm (plus::succl n a))
theorem PlusAssoc (a b c : Nat) : a + (b + c) = (a + b) + c theorem plus::assoc (a b c : Nat) : a + (b + c) = (a + b) + c
:= Induction a := induction a
(calc 0 + (b + c) = b + c : ZeroPlus (b + c) (calc 0 + (b + c) = b + c : plus::zerol (b + c)
... = (0 + b) + c : { Symm (ZeroPlus b) }) ... = (0 + b) + c : { symm (plus::zerol b) })
(λ (n : Nat) (iH : n + (b + c) = (n + b) + c), (λ (n : Nat) (iH : n + (b + c) = (n + b) + c),
calc (n + 1) + (b + c) = (n + (b + c)) + 1 : SuccPlus n (b + c) calc (n + 1) + (b + c) = (n + (b + c)) + 1 : plus::succl n (b + c)
... = ((n + b) + c) + 1 : { iH } ... = ((n + b) + c) + 1 : { iH }
... = ((n + b) + 1) + c : Symm (SuccPlus (n + b) c) ... = ((n + b) + 1) + c : symm (plus::succl (n + b) c)
... = ((n + 1) + b) + c : { have (n + b) + 1 = (n + 1) + b : Symm (SuccPlus n b) }) ... = ((n + 1) + b) + c : { have (n + b) + 1 = (n + 1) + b : symm (plus::succl n b) })
theorem ZeroMul (a : Nat) : 0 * a = 0 theorem mul::zerol (a : Nat) : 0 * a = 0
:= Induction a := induction a
(have 0 * 0 = 0 : Trivial) (have 0 * 0 = 0 : trivial)
(λ (n : Nat) (iH : 0 * n = 0), (λ (n : Nat) (iH : 0 * n = 0),
calc 0 * (n + 1) = (0 * n) + 0 : MulSucc 0 n calc 0 * (n + 1) = (0 * n) + 0 : mul::succr 0 n
... = 0 + 0 : { iH } ... = 0 + 0 : { iH }
... = 0 : Trivial) ... = 0 : trivial)
theorem SuccMul (a b : Nat) : (a + 1) * b = a * b + b theorem mul::succl (a b : Nat) : (a + 1) * b = a * b + b
:= Induction b := induction b
(calc (a + 1) * 0 = 0 : MulZero (a + 1) (calc (a + 1) * 0 = 0 : mul::zeror (a + 1)
... = a * 0 : Symm (MulZero a) ... = a * 0 : symm (mul::zeror a)
... = a * 0 + 0 : Symm (PlusZero (a * 0))) ... = a * 0 + 0 : symm (plus::zeror (a * 0)))
(λ (n : Nat) (iH : (a + 1) * n = a * n + n), (λ (n : Nat) (iH : (a + 1) * n = a * n + n),
calc (a + 1) * (n + 1) = (a + 1) * n + (a + 1) : MulSucc (a + 1) n calc (a + 1) * (n + 1) = (a + 1) * n + (a + 1) : mul::succr (a + 1) n
... = a * n + n + (a + 1) : { iH } ... = a * n + n + (a + 1) : { iH }
... = a * n + n + a + 1 : PlusAssoc (a * n + n) a 1 ... = a * n + n + a + 1 : plus::assoc (a * n + n) a 1
... = a * n + (n + a) + 1 : { have a * n + n + a = a * n + (n + a) : Symm (PlusAssoc (a * n) n a) } ... = a * n + (n + a) + 1 : { have a * n + n + a = a * n + (n + a) : symm (plus::assoc (a * n) n a) }
... = a * n + (a + n) + 1 : { PlusComm n a } ... = a * n + (a + n) + 1 : { plus::comm n a }
... = a * n + a + n + 1 : { PlusAssoc (a * n) a n } ... = a * n + a + n + 1 : { plus::assoc (a * n) a n }
... = a * (n + 1) + n + 1 : { Symm (MulSucc a n) } ... = a * (n + 1) + n + 1 : { symm (mul::succr a n) }
... = a * (n + 1) + (n + 1) : Symm (PlusAssoc (a * (n + 1)) n 1)) ... = a * (n + 1) + (n + 1) : symm (plus::assoc (a * (n + 1)) n 1))
theorem OneMul (a : Nat) : 1 * a = a theorem mul::lhs::one (a : Nat) : 1 * a = a
:= Induction a := induction a
(have 1 * 0 = 0 : Trivial) (have 1 * 0 = 0 : trivial)
(λ (n : Nat) (iH : 1 * n = n), (λ (n : Nat) (iH : 1 * n = n),
calc 1 * (n + 1) = 1 * n + 1 : MulSucc 1 n calc 1 * (n + 1) = 1 * n + 1 : mul::succr 1 n
... = n + 1 : { iH }) ... = n + 1 : { iH })
theorem MulOne (a : Nat) : a * 1 = a theorem mul::rhs::one (a : Nat) : a * 1 = a
:= Induction a := induction a
(have 0 * 1 = 0 : Trivial) (have 0 * 1 = 0 : trivial)
(λ (n : Nat) (iH : n * 1 = n), (λ (n : Nat) (iH : n * 1 = n),
calc (n + 1) * 1 = n * 1 + 1 : SuccMul n 1 calc (n + 1) * 1 = n * 1 + 1 : mul::succl n 1
... = n + 1 : { iH }) ... = n + 1 : { iH })
theorem MulComm (a b : Nat) : a * b = b * a theorem mul::comm (a b : Nat) : a * b = b * a
:= Induction b := induction b
(calc a * 0 = 0 : MulZero a (calc a * 0 = 0 : mul::zeror a
... = 0 * a : Symm (ZeroMul a)) ... = 0 * a : symm (mul::zerol a))
(λ (n : Nat) (iH : a * n = n * a), (λ (n : Nat) (iH : a * n = n * a),
calc a * (n + 1) = a * n + a : MulSucc a n calc a * (n + 1) = a * n + a : mul::succr a n
... = n * a + a : { iH } ... = n * a + a : { iH }
... = (n + 1) * a : Symm (SuccMul n a)) ... = (n + 1) * a : symm (mul::succl n a))
theorem Distribute (a b c : Nat) : a * (b + c) = a * b + a * c theorem distribute (a b c : Nat) : a * (b + c) = a * b + a * c
:= Induction a := induction a
(calc 0 * (b + c) = 0 : ZeroMul (b + c) (calc 0 * (b + c) = 0 : mul::zerol (b + c)
... = 0 + 0 : Trivial ... = 0 + 0 : trivial
... = 0 * b + 0 : { Symm (ZeroMul b) } ... = 0 * b + 0 : { symm (mul::zerol b) }
... = 0 * b + 0 * c : { Symm (ZeroMul c) }) ... = 0 * b + 0 * c : { symm (mul::zerol c) })
(λ (n : Nat) (iH : n * (b + c) = n * b + n * c), (λ (n : Nat) (iH : n * (b + c) = n * b + n * c),
calc (n + 1) * (b + c) = n * (b + c) + (b + c) : SuccMul n (b + c) calc (n + 1) * (b + c) = n * (b + c) + (b + c) : mul::succl n (b + c)
... = n * b + n * c + (b + c) : { iH } ... = n * b + n * c + (b + c) : { iH }
... = n * b + n * c + b + c : PlusAssoc (n * b + n * c) b c ... = n * b + n * c + b + c : plus::assoc (n * b + n * c) b c
... = n * b + (n * c + b) + c : { Symm (PlusAssoc (n * b) (n * c) b) } ... = n * b + (n * c + b) + c : { symm (plus::assoc (n * b) (n * c) b) }
... = n * b + (b + n * c) + c : { PlusComm (n * c) b } ... = n * b + (b + n * c) + c : { plus::comm (n * c) b }
... = n * b + b + n * c + c : { PlusAssoc (n * b) b (n * c) } ... = n * b + b + n * c + c : { plus::assoc (n * b) b (n * c) }
... = (n + 1) * b + n * c + c : { Symm (SuccMul n b) } ... = (n + 1) * b + n * c + c : { symm (mul::succl n b) }
... = (n + 1) * b + (n * c + c) : Symm (PlusAssoc ((n + 1) * b) (n * c) c) ... = (n + 1) * b + (n * c + c) : symm (plus::assoc ((n + 1) * b) (n * c) c)
... = (n + 1) * b + (n + 1) * c : { Symm (SuccMul n c) }) ... = (n + 1) * b + (n + 1) * c : { symm (mul::succl n c) })
theorem Distribute2 (a b c : Nat) : (a + b) * c = a * c + b * c theorem distribute2 (a b c : Nat) : (a + b) * c = a * c + b * c
:= calc (a + b) * c = c * (a + b) : MulComm (a + b) c := calc (a + b) * c = c * (a + b) : mul::comm (a + b) c
... = c * a + c * b : Distribute c a b ... = c * a + c * b : distribute c a b
... = a * c + c * b : { MulComm c a } ... = a * c + c * b : { mul::comm c a }
... = a * c + b * c : { MulComm c b } ... = a * c + b * c : { mul::comm c b }
theorem MulAssoc (a b c : Nat) : a * (b * c) = a * b * c theorem mul::assoc (a b c : Nat) : a * (b * c) = a * b * c
:= Induction a := induction a
(calc 0 * (b * c) = 0 : ZeroMul (b * c) (calc 0 * (b * c) = 0 : mul::zerol (b * c)
... = 0 * c : Symm (ZeroMul c) ... = 0 * c : symm (mul::zerol c)
... = (0 * b) * c : { Symm (ZeroMul b) }) ... = (0 * b) * c : { symm (mul::zerol b) })
(λ (n : Nat) (iH : n * (b * c) = n * b * c), (λ (n : Nat) (iH : n * (b * c) = n * b * c),
calc (n + 1) * (b * c) = n * (b * c) + (b * c) : SuccMul n (b * c) calc (n + 1) * (b * c) = n * (b * c) + (b * c) : mul::succl n (b * c)
... = n * b * c + (b * c) : { iH } ... = n * b * c + (b * c) : { iH }
... = (n * b + b) * c : Symm (Distribute2 (n * b) b c) ... = (n * b + b) * c : symm (distribute2 (n * b) b c)
... = (n + 1) * b * c : { Symm (SuccMul n b) }) ... = (n + 1) * b * c : { symm (mul::succl n b) })
theorem PlusInj' (a b c : Nat) : a + b = a + c ⇒ b = c theorem plus::inj' (a b c : Nat) : a + b = a + c ⇒ b = c
:= Induction a := induction a
(Assume H : 0 + b = 0 + c, (assume H : 0 + b = 0 + c,
calc b = 0 + b : Symm (ZeroPlus b) calc b = 0 + b : symm (plus::zerol b)
... = 0 + c : H ... = 0 + c : H
... = c : ZeroPlus c) ... = c : plus::zerol c)
(λ (n : Nat) (iH : n + b = n + c ⇒ b = c), (λ (n : Nat) (iH : n + b = n + c ⇒ b = c),
Assume H : n + 1 + b = n + 1 + c, assume H : n + 1 + b = n + 1 + c,
let L1 : n + b + 1 = n + c + 1 let L1 : n + b + 1 = n + c + 1
:= (calc n + b + 1 = n + (b + 1) : Symm (PlusAssoc n b 1) := (calc n + b + 1 = n + (b + 1) : symm (plus::assoc n b 1)
... = n + (1 + b) : { PlusComm b 1 } ... = n + (1 + b) : { plus::comm b 1 }
... = n + 1 + b : PlusAssoc n 1 b ... = n + 1 + b : plus::assoc n 1 b
... = n + 1 + c : H ... = n + 1 + c : H
... = n + (1 + c) : Symm (PlusAssoc n 1 c) ... = n + (1 + c) : symm (plus::assoc n 1 c)
... = n + (c + 1) : { PlusComm 1 c } ... = n + (c + 1) : { plus::comm 1 c }
... = n + c + 1 : PlusAssoc n c 1), ... = n + c + 1 : plus::assoc n c 1),
L2 : n + b = n + c := SuccInj L1 L2 : n + b = n + c := succ::inj L1
in MP iH L2) in iH ◂ L2)
theorem PlusInj {a b c : Nat} (H : a + b = a + c) : b = c theorem plus::inj {a b c : Nat} (H : a + b = a + c) : b = c
:= MP (PlusInj' a b c) H := (plus::inj' a b c) ◂ H
theorem PlusEq0 {a b : Nat} (H : a + b = 0) : a = 0 theorem plus::eqz {a b : Nat} (H : a + b = 0) : a = 0
:= Destruct (λ H1 : a = 0, H1) := destruct (λ H1 : a = 0, H1)
(λ (n : Nat) (H1 : a = n + 1), (λ (n : Nat) (H1 : a = n + 1),
AbsurdElim (a = 0) absurd::elim (a = 0)
H (calc a + b = n + 1 + b : { H1 } H (calc a + b = n + 1 + b : { H1 }
... = n + (1 + b) : Symm (PlusAssoc n 1 b) ... = n + (1 + b) : symm (plus::assoc n 1 b)
... = n + (b + 1) : { PlusComm 1 b } ... = n + (b + 1) : { plus::comm 1 b }
... = n + b + 1 : PlusAssoc n b 1 ... = n + b + 1 : plus::assoc n b 1
... ≠ 0 : SuccNeZero (n + b))) ... ≠ 0 : succ::nz (n + b)))
theorem LeIntro {a b c : Nat} (H : a + c = b) : a ≤ b theorem le::intro {a b c : Nat} (H : a + c = b) : a ≤ b
:= EqMP (Symm (LeDef a b)) (have (∃ x, a + x = b) : ExistsIntro c H) := (symm (le::def a b)) ◆ (have (∃ x, a + x = b) : exists::intro c H)
theorem LeElim {a b : Nat} (H : a ≤ b) : ∃ x, a + x = b theorem le::elim {a b : Nat} (H : a ≤ b) : ∃ x, a + x = b
:= EqMP (LeDef a b) H := (le::def a b) ◆ H
theorem LeRefl (a : Nat) : a ≤ a := LeIntro (PlusZero a) theorem le::refl (a : Nat) : a ≤ a := le::intro (plus::zeror a)
theorem LeZero (a : Nat) : 0 ≤ a := LeIntro (ZeroPlus a) theorem le::zero (a : Nat) : 0 ≤ a := le::intro (plus::zerol a)
theorem LeTrans {a b c : Nat} (H1 : a ≤ b) (H2 : b ≤ c) : a ≤ c theorem le::trans {a b c : Nat} (H1 : a ≤ b) (H2 : b ≤ c) : a ≤ c
:= Obtain (w1 : Nat) (Hw1 : a + w1 = b), from (LeElim H1), := obtain (w1 : Nat) (Hw1 : a + w1 = b), from (le::elim H1),
Obtain (w2 : Nat) (Hw2 : b + w2 = c), from (LeElim H2), obtain (w2 : Nat) (Hw2 : b + w2 = c), from (le::elim H2),
LeIntro (calc a + (w1 + w2) = a + w1 + w2 : PlusAssoc a w1 w2 le::intro (calc a + (w1 + w2) = a + w1 + w2 : plus::assoc a w1 w2
... = b + w2 : { Hw1 } ... = b + w2 : { Hw1 }
... = c : Hw2) ... = c : Hw2)
theorem LeInj {a b : Nat} (H : a ≤ b) (c : Nat) : a + c ≤ b + c theorem le::plus {a b : Nat} (H : a ≤ b) (c : Nat) : a + c ≤ b + c
:= Obtain (w : Nat) (Hw : a + w = b), from (LeElim H), := obtain (w : Nat) (Hw : a + w = b), from (le::elim H),
LeIntro (calc a + c + w = a + (c + w) : Symm (PlusAssoc a c w) le::intro (calc a + c + w = a + (c + w) : symm (plus::assoc a c w)
... = a + (w + c) : { PlusComm c w } ... = a + (w + c) : { plus::comm c w }
... = a + w + c : PlusAssoc a w c ... = a + w + c : plus::assoc a w c
... = b + c : { Hw }) ... = b + c : { Hw })
theorem LeAntiSymm {a b : Nat} (H1 : a ≤ b) (H2 : b ≤ a) : a = b theorem le::antisym {a b : Nat} (H1 : a ≤ b) (H2 : b ≤ a) : a = b
:= Obtain (w1 : Nat) (Hw1 : a + w1 = b), from (LeElim H1), := obtain (w1 : Nat) (Hw1 : a + w1 = b), from (le::elim H1),
Obtain (w2 : Nat) (Hw2 : b + w2 = a), from (LeElim H2), obtain (w2 : Nat) (Hw2 : b + w2 = a), from (le::elim H2),
let L1 : w1 + w2 = 0 let L1 : w1 + w2 = 0
:= PlusInj (calc a + (w1 + w2) = a + w1 + w2 : { PlusAssoc a w1 w2 } := plus::inj (calc a + (w1 + w2) = a + w1 + w2 : { plus::assoc a w1 w2 }
... = b + w2 : { Hw1 } ... = b + w2 : { Hw1 }
... = a : Hw2 ... = a : Hw2
... = a + 0 : Symm (PlusZero a)), ... = a + 0 : symm (plus::zeror a)),
L2 : w1 = 0 := PlusEq0 L1 L2 : w1 = 0 := plus::eqz L1
in calc a = a + 0 : Symm (PlusZero a) in calc a = a + 0 : symm (plus::zeror a)
... = a + w1 : { Symm L2 } ... = a + w1 : { symm L2 }
... = b : Hw1 ... = b : Hw1
setopaque ge true setopaque ge true

10
src/builtin/cast.lean
View file

@ -5,20 +5,20 @@
variable cast {A B : (Type U)} : A == B → A → B. variable cast {A B : (Type U)} : A == B → A → B.
-- The CastEq axiom states that for any cast of x is equal to x. -- The CastEq axiom states that for any cast of x is equal to x.
axiom CastEq {A B : (Type U)} (H : A == B) (x : A) : x == cast H x. axiom cast::eq {A B : (Type U)} (H : A == B) (x : A) : x == cast H x.
-- The CastApp axiom "propagates" the cast over application -- The CastApp axiom "propagates" the cast over application
axiom CastApp {A A' : (Type U)} {B : A → (Type U)} {B' : A' → (Type U)} 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') (H1 : (Π x : A, B x) == (Π x : A', B' x)) (H2 : A == A')
(f : Π x : A, B x) (x : A) : (f : Π x : A, B x) (x : A) :
cast H1 f (cast H2 x) == f x. cast H1 f (cast H2 x) == f x.
-- If two (dependent) function spaces are equal, then their domains are equal. -- 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)} 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'. A == A'.
-- If two (dependent) function spaces are equal, then their ranges are equal. -- 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)} 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). B a == B' (cast (dominj H) a).

416
src/builtin/kernel.lean
View file

@ -64,172 +64,176 @@ definition neq {A : TypeU} (a b : A) : Bool
infix 50 ≠ : neq infix 50 ≠ : neq
axiom MP {a b : Bool} (H1 : a ⇒ b) (H2 : a) : b axiom mp {a b : Bool} (H1 : a ⇒ b) (H2 : a) : b
axiom Discharge {a b : Bool} (H : a → b) : a ⇒ b infixl 100 <| : mp
infixl 100 ◂ : mp
axiom Case (P : Bool → Bool) (H1 : P true) (H2 : P false) (a : Bool) : P a axiom discharge {a b : Bool} (H : a → b) : a ⇒ b
axiom Refl {A : TypeU} (a : A) : a == a axiom case (P : Bool → Bool) (H1 : P true) (H2 : P false) (a : Bool) : P a
axiom Subst {A : TypeU} {a b : A} {P : A → Bool} (H1 : P a) (H2 : a == b) : P b axiom refl {A : TypeU} (a : A) : a == a
definition SubstP {A : TypeU} {a b : A} (P : A → Bool) (H1 : P a) (H2 : a == b) : P b axiom subst {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 definition substp {A : TypeU} {a b : A} (P : A → Bool) (H1 : P a) (H2 : a == b) : P b
:= subst H1 H2
axiom ImpAntisym {a b : Bool} (H1 : a ⇒ b) (H2 : b ⇒ a) : a == b axiom eta {A : TypeU} {B : A → TypeU} (f : Π x : A, B x) : (λ x : A, f x) == f
axiom Abst {A : TypeU} {B : A → TypeU} {f g : Π x : A, B x} (H : Π x : A, f x == g x) : f == g axiom iff::intro {a b : Bool} (H1 : a ⇒ b) (H2 : b ⇒ a) : iff a b
axiom HSymm {A B : TypeU} {a : A} {b : B} (H : a == b) : b == a axiom abst {A : TypeU} {B : A → TypeU} {f g : Π x : A, B x} (H : Π x : A, f x == g x) : f == g
axiom HTrans {A B C : TypeU} {a : A} {b : B} {c : C} (H1 : a == b) (H2 : b == c) : a == c axiom hsymm {A B : TypeU} {a : A} {b : B} (H : a == b) : b == a
theorem Trivial : true axiom htrans {A B C : TypeU} {a : A} {b : B} {c : C} (H1 : a == b) (H2 : b == c) : a == c
:= Refl true
theorem TrueNeFalse : not (true == false) theorem trivial : true
:= Trivial := refl true
theorem EM (a : Bool) : a ∨ ¬ a theorem em (a : Bool) : a ∨ ¬ a
:= Case (λ x, x ∨ ¬ x) Trivial Trivial a := case (λ x, x ∨ ¬ x) trivial trivial a
theorem FalseElim (a : Bool) (H : false) : a theorem false::elim (a : Bool) (H : false) : a
:= Case (λ x, x) Trivial H a := case (λ x, x) trivial H a
theorem Absurd {a : Bool} (H1 : a) (H2 : ¬ a) : false theorem absurd {a : Bool} (H1 : a) (H2 : ¬ a) : false
:= MP H2 H1 := H2 ◂ H1
theorem EqMP {a b : Bool} (H1 : a == b) (H2 : a) : b theorem eq::mp {a b : Bool} (H1 : a == b) (H2 : a) : b
:= Subst H2 H1 := subst H2 H1
-- Assume is a 'macro' that expands into a Discharge infixl 100 <|> : eq::mp
infixl 100 ◆ : eq::mp
theorem ImpTrans {a b c : Bool} (H1 : a ⇒ b) (H2 : b ⇒ c) : a ⇒ c -- assume is a 'macro' that expands into a discharge
:= Assume Ha, MP H2 (MP H1 Ha)
theorem ImpEqTrans {a b c : Bool} (H1 : a ⇒ b) (H2 : b == c) : a ⇒ c theorem imp::trans {a b c : Bool} (H1 : a ⇒ b) (H2 : b ⇒ c) : a ⇒ c
:= Assume Ha, EqMP H2 (MP H1 Ha) := assume Ha, H2 ◂ (H1 ◂ Ha)
theorem EqImpTrans {a b c : Bool} (H1 : a == b) (H2 : b ⇒ c) : a ⇒ c theorem imp::eq::trans {a b c : Bool} (H1 : a ⇒ b) (H2 : b == c) : a ⇒ c
:= Assume Ha, MP H2 (EqMP H1 Ha) := assume Ha, H2 ◆ (H1 ◂ Ha)
theorem DoubleNeg (a : Bool) : (¬ ¬ a) == a theorem eq::imp::trans {a b c : Bool} (H1 : a == b) (H2 : b ⇒ c) : a ⇒ c
:= Case (λ x, (¬ ¬ x) == x) Trivial Trivial a := assume Ha, H2 ◂ (H1 ◆ Ha)
theorem DoubleNegElim {a : Bool} (H : ¬ ¬ a) : a theorem not::not::eq (a : Bool) : (¬ ¬ a) == a
:= EqMP (DoubleNeg a) H := case (λ x, (¬ ¬ x) == x) trivial trivial a
theorem MT {a b : Bool} (H1 : a ⇒ b) (H2 : ¬ b) : ¬ a theorem not::not::elim {a : Bool} (H : ¬ ¬ a) : a
:= Assume H : a, Absurd (MP H1 H) H2 := (not::not::eq a) ◆ H
theorem Contrapos {a b : Bool} (H : a ⇒ b) : ¬ b ⇒ ¬ a theorem mt {a b : Bool} (H1 : a ⇒ b) (H2 : ¬ b) : ¬ a
:= Assume H1 : ¬ b, MT H H1 := assume H : a, absurd (H1 ◂ H) H2
theorem AbsurdElim {a : Bool} (b : Bool) (H1 : a) (H2 : ¬ a) : b theorem contrapos {a b : Bool} (H : a ⇒ b) : ¬ b ⇒ ¬ a
:= FalseElim b (Absurd H1 H2) := assume H1 : ¬ b, mt H H1
theorem NotImp1 {a b : Bool} (H : ¬ (a ⇒ b)) : a theorem absurd::elim {a : Bool} (b : Bool) (H1 : a) (H2 : ¬ a) : b
:= DoubleNegElim := false::elim b (absurd H1 H2)
theorem not::imp::eliml {a b : Bool} (H : ¬ (a ⇒ b)) : a
:= not::not::elim
(have ¬ ¬ a : (have ¬ ¬ a :
Assume H1 : ¬ a, Absurd (have a ⇒ b : Assume H2 : a, AbsurdElim b H2 H1) assume H1 : ¬ a, absurd (have a ⇒ b : assume H2 : a, absurd::elim b H2 H1)
(have ¬ (a ⇒ b) : H)) (have ¬ (a ⇒ b) : H))
theorem NotImp2 {a b : Bool} (H : ¬ (a ⇒ b)) : ¬ b theorem not::imp::elimr {a b : Bool} (H : ¬ (a ⇒ b)) : ¬ b
:= Assume H1 : b, Absurd (have a ⇒ b : Assume H2 : a, H1) := assume H1 : b, absurd (have a ⇒ b : assume H2 : a, H1)
(have ¬ (a ⇒ b) : H) (have ¬ (a ⇒ b) : H)
theorem resolve1 {a b : Bool} (H1 : a ∨ b) (H2 : ¬ a) : b
:= H1 ◂ H2
-- Remark: conjunction is defined as ¬ (a ⇒ ¬ b) in Lean -- Remark: conjunction is defined as ¬ (a ⇒ ¬ b) in Lean
theorem Conj {a b : Bool} (H1 : a) (H2 : b) : a ∧ b theorem and::intro {a b : Bool} (H1 : a) (H2 : b) : a ∧ b
:= Assume H : a ⇒ ¬ b, Absurd H2 (MP H H1) := assume H : a ⇒ ¬ b, absurd H2 (H ◂ H1)
theorem Conjunct1 {a b : Bool} (H : a ∧ b) : a theorem and::eliml {a b : Bool} (H : a ∧ b) : a
:= NotImp1 H := not::imp::eliml H
theorem Conjunct2 {a b : Bool} (H : a ∧ b) : b theorem and::elimr {a b : Bool} (H : a ∧ b) : b
:= DoubleNegElim (NotImp2 H) := 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 Disj1 {a : Bool} (H : a) (b : Bool) : a ∨ b theorem or::introl {a : Bool} (H : a) (b : Bool) : a ∨ b
:= Assume H1 : ¬ a, AbsurdElim b H H1 := assume H1 : ¬ a, absurd::elim b H H1
theorem Disj2 {b : Bool} (a : Bool) (H : b) : a ∨ b theorem or::intror {b : Bool} (a : Bool) (H : b) : a ∨ b
:= Assume H1 : ¬ a, H := assume H1 : ¬ a, H
theorem ArrowToImplies {a b : Bool} (H : a → b) : a ⇒ b theorem or::elim {a b c : Bool} (H1 : a ∨ b) (H2 : a → c) (H3 : b → c) : c
:= Assume H1 : a, H H1 := not::not::elim
(assume H : ¬ c,
theorem Resolve1 {a b : Bool} (H1 : a ∨ b) (H2 : ¬ a) : b absurd (have c : H3 (have b : resolve1 H1 (have ¬ a : (mt (assume Ha : a, H2 Ha) H))))
:= MP H1 H2
theorem DisjCases {a b c : Bool} (H1 : a ∨ b) (H2 : a → c) (H3 : b → c) : c
:= DoubleNegElim
(Assume H : ¬ c,
Absurd (have c : H3 (have b : Resolve1 H1 (have ¬ a : (MT (ArrowToImplies H2) H))))
H) H)
theorem Refute {a : Bool} (H : ¬ a → false) : a theorem refute {a : Bool} (H : ¬ a → false) : a
:= DisjCases (EM a) (λ H1 : a, H1) (λ H1 : ¬ a, FalseElim a (H H1)) := or::elim (em a) (λ H1 : a, H1) (λ H1 : ¬ a, false::elim a (H H1))
theorem Symm {A : TypeU} {a b : A} (H : a == b) : b == a theorem symm {A : TypeU} {a b : A} (H : a == b) : b == a
:= Subst (Refl a) H := subst (refl a) H
theorem NeSymm {A : TypeU} {a b : A} (H : a ≠ b) : b ≠ a theorem trans {A : TypeU} {a b c : A} (H1 : a == b) (H2 : b == c) : a == c
:= Assume H1 : b = a, MP H (Symm H1) := subst H1 H2
theorem EqNeTrans {A : TypeU} {a b c : A} (H1 : a = b) (H2 : b ≠ c) : a ≠ c infixl 100 ⋈ : trans
:= Subst H2 (Symm H1)
theorem NeEqTrans {A : TypeU} {a b c : A} (H1 : a ≠ b) (H2 : b = c) : a ≠ c theorem ne::symm {A : TypeU} {a b : A} (H : a ≠ b) : b ≠ a
:= Subst H1 H2 := assume H1 : b = a, H ◂ (symm H1)
theorem Trans {A : TypeU} {a b c : A} (H1 : a == b) (H2 : b == c) : a == c theorem eq::ne::trans {A : TypeU} {a b c : A} (H1 : a = b) (H2 : b ≠ c) : a ≠ c
:= Subst H1 H2 := subst H2 (symm H1)
theorem EqTElim {a : Bool} (H : a == true) : a theorem ne::eq::trans {A : TypeU} {a b c : A} (H1 : a ≠ b) (H2 : b = c) : a ≠ c
:= EqMP (Symm H) Trivial := subst H1 H2
theorem EqTIntro {a : Bool} (H : a) : a == true theorem eqt::elim {a : Bool} (H : a == true) : a
:= ImpAntisym (Assume H1 : a, Trivial) := (symm H) ◆ trivial
(Assume 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 theorem eqt::intro {a : Bool} (H : a) : a == true
:= SubstP (fun h : (Π x : A, B x), f a == h a) (Refl (f a)) H := iff::intro (assume H1 : a, trivial)
(assume 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
-- Remark: we must use heterogeneous equality in the following theorem because the types of (f a) and (f b) -- 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) -- are not "definitionally equal" They are (B a) and (B b)
-- They are provably equal, we just have to apply Congr1 -- 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 := 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 -- Remark: like the previous theorem we use heterogeneous equality We cannot use Trans theorem
-- because the types are not definitionally equal -- 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) := htrans (congr2 f H2) (congr1 b H1)
theorem ForallElim {A : TypeU} {P : A → Bool} (H : Forall A P) (a : A) : P a theorem forall::elim {A : TypeU} {P : A → Bool} (H : Forall A P) (a : A) : P a
:= EqTElim (Congr1 a H) := eqt::elim (congr1 a H)
theorem ForallIntro {A : TypeU} {P : A → Bool} (H : Π x : A, P x) : Forall A P infixl 100 ! : forall::elim
:= Trans (Symm (Eta P)) infixl 100 ↓ : forall::elim
(Abst (λ x, EqTIntro (H x)))
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)) -- Remark: the existential is defined as (¬ (forall x : A, ¬ P x))
theorem ExistsElim {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, := refute (λ R : ¬ B,
Absurd (ForallIntro (λ a : A, MT (Assume H : P a, H2 a H) R)) absurd (forall::intro (λ a : A, mt (assume H : P a, H2 a H) R))
H1) H1)
theorem ExistsIntro {A : TypeU} {P : A → Bool} (a : A) (H : P a) : Exists A P theorem exists::intro {A : TypeU} {P : A → Bool} (a : A) (H : P a) : Exists A P
:= Assume H1 : (∀ x : A, ¬ P x), := assume H1 : (∀ x : A, ¬ P x),
Absurd H (ForallElim H1 a) absurd H (forall::elim H1 a)
-- At this point, we have proved the theorems we need using the -- At this point, we have proved the theorems we need using the
-- definitions of forall, exists, and, or, =>, not We mark (some of) -- definitions of forall, exists, and, or, =>, not We mark (some of)
@ -242,155 +246,151 @@ setopaque or true
setopaque and true setopaque and true
setopaque forall true setopaque forall true
theorem OrComm (a b : Bool) : (a ∨ b) == (b ∨ a) theorem or::comm (a b : Bool) : (a ∨ b) == (b ∨ a)
:= ImpAntisym (Assume H, DisjCases H (λ H1, Disj2 b H1) (λ H2, Disj1 H2 a)) := iff::intro (assume H, or::elim H (λ H1, or::intror b H1) (λ H2, or::introl H2 a))
(Assume H, DisjCases H (λ H1, Disj2 a H1) (λ H2, Disj1 H2 b)) (assume 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,
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),
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 OrAssoc (a b c : Bool) : ((a ∨ b) ∨ c) == (a ∨ (b ∨ c)) theorem or::id (a : Bool) : (a ∨ a) == a
:= ImpAntisym (Assume H : (a ∨ b) ∨ c, := iff::intro (assume H, or::elim H (λ H1, H1) (λ H2, H2))
DisjCases H (λ H1 : a ∨ b, DisjCases H1 (λ Ha : a, Disj1 Ha (b ∨ c)) (λ Hb : b, Disj2 a (Disj1 Hb c))) (assume H, or::introl H a)
(λ Hc : c, Disj2 a (Disj2 b Hc)))
(Assume H : a ∨ (b ∨ c),
DisjCases H (λ Ha : a, (Disj1 (Disj1 Ha b) c))
(λ H1 : b ∨ c, DisjCases H1 (λ Hb : b, Disj1 (Disj2 a Hb) c)
(λ Hc : c, Disj2 (a ∨ b) Hc)))
theorem OrId (a : Bool) : (a ∨ a) == a theorem or::falsel (a : Bool) : (a ∨ false) == a
:= ImpAntisym (Assume H, DisjCases H (λ H1, H1) (λ H2, H2)) := iff::intro (assume H, or::elim H (λ H1, H1) (λ H2, false::elim a H2))
(Assume H, Disj1 H a) (assume H, or::introl H false)
theorem OrRhsFalse (a : Bool) : (a ∨ false) == a theorem or::falser (a : Bool) : (false ∨ a) == a
:= ImpAntisym (Assume H, DisjCases H (λ H1, H1) (λ H2, FalseElim a H2)) := (or::comm false a) ⋈ (or::falsel a)
(Assume H, Disj1 H false)
theorem OrLhsFalse (a : Bool) : (false ∨ a) == a theorem or::truel (a : Bool) : (true ∨ a) == true
:= Trans (OrComm false a) (OrRhsFalse a) := eqt::intro (case (λ x : Bool, true ∨ x) trivial trivial a)
theorem OrLhsTrue (a : Bool) : (true ∨ a) == true theorem or::truer (a : Bool) : (a ∨ true) == true
:= EqTIntro (Case (λ x : Bool, true ∨ x) Trivial Trivial a) := (or::comm a true) ⋈ (or::truel a)
theorem OrRhsTrue (a : Bool) : (a ∨ true) == true theorem or::tauto (a : Bool) : (a ∨ ¬ a) == true
:= Trans (OrComm a true) (OrLhsTrue a) := eqt::intro (em a)
theorem OrAnotA (a : Bool) : (a ∨ ¬ a) == true theorem and::comm (a b : Bool) : (a ∧ b) == (b ∧ a)
:= EqTIntro (EM a) := iff::intro (assume H, and::intro (and::elimr H) (and::eliml H))
(assume H, and::intro (and::elimr H) (and::eliml H))
theorem AndComm (a b : Bool) : (a ∧ b) == (b ∧ a) theorem and::id (a : Bool) : (a ∧ a) == a
:= ImpAntisym (Assume H, Conj (Conjunct2 H) (Conjunct1 H)) := iff::intro (assume H, and::eliml H)
(Assume H, Conj (Conjunct2 H) (Conjunct1 H)) (assume H, and::intro H H)
theorem AndId (a : Bool) : (a ∧ a) == a theorem and::assoc (a b c : Bool) : ((a ∧ b) ∧ c) == (a ∧ (b ∧ c))
:= ImpAntisym (Assume H, Conjunct1 H) := iff::intro (assume H, and::intro (and::eliml (and::eliml H)) (and::intro (and::elimr (and::eliml H)) (and::elimr H)))
(Assume H, Conj H H) (assume H, and::intro (and::intro (and::eliml H) (and::eliml (and::elimr H))) (and::elimr (and::elimr H)))
theorem AndAssoc (a b c : Bool) : ((a ∧ b) ∧ c) == (a ∧ (b ∧ c)) theorem and::truer (a : Bool) : (a ∧ true) == a
:= ImpAntisym (Assume H, Conj (Conjunct1 (Conjunct1 H)) (Conj (Conjunct2 (Conjunct1 H)) (Conjunct2 H))) := iff::intro (assume H : a ∧ true, and::eliml H)
(Assume H, Conj (Conj (Conjunct1 H) (Conjunct1 (Conjunct2 H))) (Conjunct2 (Conjunct2 H))) (assume H : a, and::intro H trivial)
theorem AndRhsTrue (a : Bool) : (a ∧ true) == a theorem and::truel (a : Bool) : (true ∧ a) == a
:= ImpAntisym (Assume H : a ∧ true, Conjunct1 H) := trans (and::comm true a) (and::truer a)
(Assume H : a, Conj H Trivial)
theorem AndLhsTrue (a : Bool) : (true ∧ a) == a theorem and::falsel (a : Bool) : (a ∧ false) == false
:= Trans (AndComm true a) (AndRhsTrue a) := iff::intro (assume H, and::elimr H)
(assume H, false::elim (a ∧ false) H)
theorem AndRhsFalse (a : Bool) : (a ∧ false) == false theorem and::falser (a : Bool) : (false ∧ a) == false
:= ImpAntisym (Assume H, Conjunct2 H) := (and::comm false a) ⋈ (and::falsel a)
(Assume H, FalseElim (a ∧ false) H)
theorem AndLhsFalse (a : Bool) : (false ∧ a) == false theorem and::absurd (a : Bool) : (a ∧ ¬ a) == false
:= Trans (AndComm false a) (AndRhsFalse a) := iff::intro (assume H, absurd (and::eliml H) (and::elimr H))
(assume H, false::elim (a ∧ ¬ a) H)
theorem AndAnotA (a : Bool) : (a ∧ ¬ a) == false theorem not::true : (¬ true) == false
:= ImpAntisym (Assume H, Absurd (Conjunct1 H) (Conjunct2 H)) := trivial
(Assume H, FalseElim (a ∧ ¬ a) H)
theorem NotTrue : (¬ true) == false theorem not::false : (¬ false) == true
:= Trivial := trivial
theorem NotFalse : (¬ false) == true theorem not::and (a b : Bool) : (¬ (a ∧ b)) == (¬ a ∨ ¬ b)
:= Trivial := case (λ x, (¬ (x ∧ b)) == (¬ x ∨ ¬ b))
(case (λ y, (¬ (true ∧ y)) == (¬ true ∨ ¬ y)) trivial trivial b)
theorem NotAnd (a b : Bool) : (¬ (a ∧ b)) == (¬ a ∨ ¬ b) (case (λ y, (¬ (false ∧ y)) == (¬ false ∨ ¬ y)) trivial trivial 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 a
theorem NotAndElim {a b : Bool} (H : ¬ (a ∧ b)) : ¬ a ∨ ¬ b theorem not::and::elim {a b : Bool} (H : ¬ (a ∧ b)) : ¬ a ∨ ¬ b
:= EqMP (NotAnd a b) H := (not::and a b) ◆ H
theorem NotOr (a b : Bool) : (¬ (a ∨ b)) == (¬ a ∧ ¬ b) theorem not::or (a b : Bool) : (¬ (a ∨ b)) == (¬ a ∧ ¬ b)
:= Case (λ x, (¬ (x ∨ b)) == (¬ x ∧ ¬ b)) := case (λ x, (¬ (x ∨ b)) == (¬ x ∧ ¬ b))
(Case (λ y, (¬ (true ∨ y)) == (¬ true ∧ ¬ y)) Trivial Trivial b) (case (λ y, (¬ (true ∨ y)) == (¬ true ∧ ¬ y)) trivial trivial b)
(Case (λ y, (¬ (false ∨ y)) == (¬ false ∧ ¬ y)) Trivial Trivial b) (case (λ y, (¬ (false ∨ y)) == (¬ false ∧ ¬ y)) trivial trivial b)
a a
theorem NotOrElim {a b : Bool} (H : ¬ (a ∨ b)) : ¬ a ∧ ¬ b theorem not::or::elim {a b : Bool} (H : ¬ (a ∨ b)) : ¬ a ∧ ¬ b
:= EqMP (NotOr a b) H := (not::or a b) ◆ H
theorem NotEq (a b : Bool) : (¬ (a == b)) == ((¬ a) == b) theorem not::iff (a b : Bool) : (¬ (a == b)) == ((¬ a) == b)
:= Case (λ x, (¬ (x == b)) == ((¬ x) == b)) := case (λ x, (¬ (x == b)) == ((¬ x) == b))
(Case (λ y, (¬ (true == y)) == ((¬ true) == y)) Trivial Trivial b) (case (λ y, (¬ (true == y)) == ((¬ true) == y)) trivial trivial b)
(Case (λ y, (¬ (false == y)) == ((¬ false) == y)) Trivial Trivial b) (case (λ y, (¬ (false == y)) == ((¬ false) == y)) trivial trivial b)
a a
theorem NotEqElim {a b : Bool} (H : ¬ (a == b)) : (¬ a) == b theorem not::iff::elim {a b : Bool} (H : ¬ (a == b)) : (¬ a) == b
:= EqMP (NotEq a b) H := (not::iff a b) ◆ H
theorem NotImp (a b : Bool) : (¬ (a ⇒ b)) == (a ∧ ¬ b) theorem not::implies (a b : Bool) : (¬ (a ⇒ b)) == (a ∧ ¬ b)
:= Case (λ x, (¬ (x ⇒ b)) == (x ∧ ¬ b)) := case (λ x, (¬ (x ⇒ b)) == (x ∧ ¬ b))
(Case (λ y, (¬ (true ⇒ y)) == (true ∧ ¬ y)) Trivial Trivial b) (case (λ y, (¬ (true ⇒ y)) == (true ∧ ¬ y)) trivial trivial b)
(Case (λ y, (¬ (false ⇒ y)) == (false ∧ ¬ y)) Trivial Trivial b) (case (λ y, (¬ (false ⇒ y)) == (false ∧ ¬ y)) trivial trivial b)
a a
theorem NotImpElim {a b : Bool} (H : ¬ (a ⇒ b)) : a ∧ ¬ b theorem not::implies::elim {a b : Bool} (H : ¬ (a ⇒ b)) : a ∧ ¬ b
:= EqMP (NotImp a b) H := (not::implies a b) ◆ H
theorem NotCongr {a b : Bool} (H : a == b) : (¬ a) == (¬ b) theorem not::congr {a b : Bool} (H : a == b) : (¬ a) == (¬ b)
:= Congr2 not H := congr2 not H
theorem ForallEqIntro {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::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) := congr2 (Forall A) (abst H)
theorem ExistsEqIntro {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 : Pi x : A, P x == Q x) : (∃ x : A, P x) == (∃ x : A, Q x)
:= Congr2 (Exists A) (Abst H) := congr2 (Exists A) (abst H)
theorem NotForall (A : (Type U)) (P : A → Bool) : (¬ (∀ x : A, P x)) == (∃ x : A, ¬ P x) theorem not::forall (A : (Type U)) (P : A → Bool) : (¬ (∀ x : A, P x)) == (∃ x : A, ¬ P x)
:= let L1 : (¬ ∀ x : A, ¬ ¬ P x) == (∃ x : A, ¬ P x) := Refl (∃ 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)))))
L2 : (¬ ∀ x : A, P x) == (¬ ∀ x : A, ¬ ¬ P x) := ... = (∃ x : A, ¬ P x) : refl (∃ x : A, ¬ P x)
NotCongr (ForallEqIntro (λ x : A, (Symm (DoubleNeg (P x)))))
in Trans L2 L1
theorem NotForallElim {A : (Type U)} {P : A → Bool} (H : ¬ (∀ x : A, P x)) : ∃ x : A, ¬ P x theorem not::forall::elim {A : (Type U)} {P : A → Bool} (H : ¬ (∀ x : A, P x)) : ∃ x : A, ¬ P x
:= EqMP (NotForall A P) H := (not::forall A P) ◆ H
theorem NotExists (A : (Type U)) (P : A → Bool) : (¬ ∃ x : A, P x) == (∀ x : A, ¬ P x) theorem not::exists (A : (Type U)) (P : A → Bool) : (¬ ∃ x : A, P x) == (∀ x : A, ¬ P x)
:= let L1 : (¬ ∃ x : A, P x) == (¬ ¬ ∀ x : A, ¬ P x) := Refl (¬ ∃ x : A, P x), := calc (¬ ∃ x : A, P x) = (¬ ¬ ∀ x : A, ¬ P x) : refl (¬ ∃ x : A, P x)
L2 : (¬ ¬ ∀ x : A, ¬ P x) == (∀ x : A, ¬ P x) := DoubleNeg (∀ x : A, ¬ P x) ... = (∀ x : A, ¬ P x) : not::not::eq (∀ x : A, ¬ P x)
in Trans L1 L2
theorem NotExistsElim {A : (Type U)} {P : A → Bool} (H : ¬ ∃ x : A, P x) : ∀ x : A, ¬ P x theorem not::exists::elim {A : (Type U)} {P : A → Bool} (H : ¬ ∃ x : A, P x) : ∀ x : A, ¬ P x
:= EqMP (NotExists A P) H := (not::exists A P) ◆ H
theorem UnfoldExists1 {A : TypeU} {P : A → Bool} (a : A) (H : ∃ x : A, P x) : P a ∨ (∃ x : A, x ≠ a ∧ P x) theorem exists::unfold1 {A : TypeU} {P : A → Bool} (a : A) (H : ∃ x : A, P x) : P a ∨ (∃ x : A, x ≠ a ∧ P x)
:= ExistsElim H := exists::elim H
(λ (w : A) (H1 : P w), (λ (w : A) (H1 : P w),
DisjCases (EM (w = a)) or::elim (em (w = a))
(λ Heq : w = a, Disj1 (Subst H1 Heq) (∃ x : A, x ≠ a ∧ P x)) (λ Heq : w = a, or::introl (subst H1 Heq) (∃ x : A, x ≠ a ∧ P x))
(λ Hne : w ≠ a, Disj2 (P a) (ExistsIntro w (Conj Hne H1)))) (λ Hne : w ≠ a, or::intror (P a) (exists::intro w (and::intro Hne H1))))
theorem UnfoldExists2 {A : TypeU} {P : A → Bool} (a : A) (H : P a ∨ (∃ x : A, x ≠ a ∧ P x)) : ∃ x : A, P x theorem exists::unfold2 {A : TypeU} {P : A → Bool} (a : A) (H : P a ∨ (∃ x : A, x ≠ a ∧ P x)) : ∃ x : A, P x
:= DisjCases H := or::elim H
(λ H1 : P a, ExistsIntro a H1) (λ H1 : P a, exists::intro a H1)
(λ H2 : (∃ x : A, x ≠ a ∧ P x), (λ H2 : (∃ x : A, x ≠ a ∧ P x),
ExistsElim H2 exists::elim H2
(λ (w : A) (Hw : w ≠ a ∧ P w), (λ (w : A) (Hw : w ≠ a ∧ P w),
ExistsIntro w (Conjunct2 Hw))) exists::intro w (and::elimr Hw)))
theorem UnfoldExists {A : TypeU} (P : A → Bool) (a : A) : (∃ x : A, P x) = (P a ∨ (∃ x : A, x ≠ a ∧ P x)) theorem exists::unfold {A : TypeU} (P : A → Bool) (a : A) : (∃ x : A, P x) = (P a ∨ (∃ x : A, x ≠ a ∧ P x))
:= ImpAntisym (Assume H : (∃ x : A, P x), UnfoldExists1 a H) := iff::intro (assume H : (∃ x : A, P x), exists::unfold1 a H)
(Assume H : (P a ∨ (∃ x : A, x ≠ a ∧ P x)), UnfoldExists2 a H) (assume H : (P a ∨ (∃ x : A, x ≠ a ∧ P x)), exists::unfold2 a H)
setopaque exists true setopaque exists true

20
src/builtin/macros.lua
View file

@ -83,11 +83,9 @@ function nary_macro(name, f, farity)
end) end)
end end
binder_macro("take", Const("ForallIntro"), 3, 1, 3) binder_macro("take", Const({"forall", "intro"}), 3, 1, 3)
binder_macro("Assume", Const("Discharge"), 3, 1, 3) binder_macro("assume", Const("discharge"), 3, 1, 3)
nary_macro("Instantiate", Const("ForallElim"), 4) nary_macro("instantiate", Const({"forall", "elim"}), 4)
nary_macro("MP'", Const("MP"), 4)
nary_macro("Subst'", Const("Subst"), 6)
-- ExistsElim syntax-sugar -- ExistsElim syntax-sugar
-- Example: -- Example:
@ -96,14 +94,14 @@ nary_macro("Subst'", Const("Subst"), 6)
-- Axiom Ax2: forall x y, not P x y -- Axiom Ax2: forall x y, not P x y
-- Now, the following macro expression -- Now, the following macro expression
-- obtain (a b : Nat) (H : P a b) from Ax1, -- obtain (a b : Nat) (H : P a b) from Ax1,
-- show false, Absurd H (instantiate Ax2 a b) -- have false : absurd H (instantiate Ax2 a b)
-- expands to -- expands to
-- ExistsElim Ax1 -- exists::elim Ax1
-- (fun (a : Nat) (Haux : ...), -- (fun (a : Nat) (Haux : ...),
-- ExistsElim Haux -- exists::elim Haux
-- (fun (b : Na) (H : P a b), -- (fun (b : Na) (H : P a b),
-- show false, Absurd H (instantiate Ax2 a b) -- have false : absurd H (instantiate Ax2 a b)
macro("Obtain", { macro_arg.Parameters, macro_arg.Comma, macro_arg.Id, macro_arg.Expr, macro_arg.Comma, macro_arg.Expr }, macro("obtain", { macro_arg.Parameters, macro_arg.Comma, macro_arg.Id, macro_arg.Expr, macro_arg.Comma, macro_arg.Expr },
function (env, bindings, fromid, exPr, body) function (env, bindings, fromid, exPr, body)
local n = #bindings local n = #bindings
if n < 2 then if n < 2 then
@ -112,7 +110,7 @@ macro("Obtain", { macro_arg.Parameters, macro_arg.Comma, macro_arg.Id, macro_arg
if fromid ~= name("from") then if fromid ~= name("from") then
error("invalid 'obtain' expression, 'from' keyword expected, got '" .. tostring(fromid) .. "'") error("invalid 'obtain' expression, 'from' keyword expected, got '" .. tostring(fromid) .. "'")
end end
local exElim = mk_constant("ExistsElim") local exElim = mk_constant({"exists", "elim"})
local H_name = bindings[n][1] local H_name = bindings[n][1]
local H_type = bindings[n][2] local H_type = bindings[n][2]
local a_name = bindings[n-1][1] local a_name = bindings[n-1][1]

BIN
src/builtin/obj/Nat.olean
View file

Binary file not shown.

BIN
src/builtin/obj/cast.olean
View file

Binary file not shown.

BIN
src/builtin/obj/kernel.olean
View file

Binary file not shown.

10
src/frontends/lean/parser_calc.cpp
View file

@ -44,11 +44,11 @@ void calc_proof_parser::add_trans_step(expr const & op1, expr const & op2, trans
m_trans_ops.emplace_front(op1, op2, d); m_trans_ops.emplace_front(op1, op2, d);
} }
static name g_eq_imp_trans("EqImpTrans"); static name g_eq_imp_trans({"eq", "imp", "trans"});
static name g_imp_eq_trans("ImpEqTrans"); static name g_imp_eq_trans({"imp", "eq", "trans"});
static name g_imp_trans("ImpTrans"); static name g_imp_trans({"imp", "trans"});
static name g_eq_ne_trans("EqNeTrans"); static name g_eq_ne_trans({"eq", "ne", "trans"});
static name g_ne_eq_trans("NeEqTrans"); static name g_ne_eq_trans({"ne", "eq", "trans"});
static name g_neq("neq"); static name g_neq("neq");
calc_proof_parser::calc_proof_parser() { calc_proof_parser::calc_proof_parser() {

82
src/kernel/builtin.cpp
View file

@ -127,49 +127,47 @@ MK_CONSTANT(forall_fn, name("forall"));
MK_CONSTANT(exists_fn, name("exists")); MK_CONSTANT(exists_fn, name("exists"));
MK_CONSTANT(homo_eq_fn, name("eq")); MK_CONSTANT(homo_eq_fn, name("eq"));
// Axioms // Axioms
MK_CONSTANT(mp_fn, name("MP")); MK_CONSTANT(mp_fn, name("mp"));
MK_CONSTANT(discharge_fn, name("Discharge")); MK_CONSTANT(discharge_fn, name("discharge"));
MK_CONSTANT(case_fn, name("Case")); MK_CONSTANT(case_fn, name("case"));
MK_CONSTANT(refl_fn, name("Refl")); MK_CONSTANT(refl_fn, name("refl"));
MK_CONSTANT(subst_fn, name("Subst")); MK_CONSTANT(subst_fn, name("subst"));
MK_CONSTANT(eta_fn, name("Eta")); MK_CONSTANT(eta_fn, name("eta"));
MK_CONSTANT(imp_antisym_fn, name("ImpAntisym")); MK_CONSTANT(imp_antisym_fn, name({"iff", "intro"}));
MK_CONSTANT(abst_fn, name("Abst")); MK_CONSTANT(abst_fn, name("abst"));
MK_CONSTANT(htrans_fn, name("HTrans")); MK_CONSTANT(htrans_fn, name("htrans"));
MK_CONSTANT(hsymm_fn, name("HSymm")); MK_CONSTANT(hsymm_fn, name("hsymm"));
// Theorems // Theorems
MK_CONSTANT(trivial, name("Trivial")); MK_CONSTANT(trivial, name("trivial"));
MK_CONSTANT(true_neq_false, name("TrueNeFalse")); MK_CONSTANT(false_elim_fn, name({"false", "elim"}));
MK_CONSTANT(false_elim_fn, name("FalseElim")); MK_CONSTANT(absurd_fn, name("absurd"));
MK_CONSTANT(absurd_fn, name("Absurd")); MK_CONSTANT(em_fn, name("em"));
MK_CONSTANT(em_fn, name("EM")); MK_CONSTANT(double_neg_fn, name("doubleneg"));
MK_CONSTANT(double_neg_fn, name("DoubleNeg")); MK_CONSTANT(double_neg_elim_fn, name({"doubleneg", "elim"}));
MK_CONSTANT(double_neg_elim_fn, name("DoubleNegElim")); MK_CONSTANT(mt_fn, name("mt"));
MK_CONSTANT(mt_fn, name("MT")); MK_CONSTANT(contrapos_fn, name("contrapos"));
MK_CONSTANT(contrapos_fn, name("Contrapos")); MK_CONSTANT(absurd_elim_fn, name({"absurd", "elim"}));
MK_CONSTANT(false_imp_any_fn, name("FalseImpAny")); MK_CONSTANT(eq_mp_fn, name({"eq", "mp"}));
MK_CONSTANT(absurd_elim_fn, name("AbsurdElim")); MK_CONSTANT(not_imp1_fn, name({"not", "imp", "eliml"}));
MK_CONSTANT(eq_mp_fn, name("EqMP")); MK_CONSTANT(not_imp2_fn, name({"not", "imp", "elimr"}));
MK_CONSTANT(not_imp1_fn, name("NotImp1")); MK_CONSTANT(conj_fn, name({"and", "intro"}));
MK_CONSTANT(not_imp2_fn, name("NotImp2")); MK_CONSTANT(conjunct1_fn, name({"and", "eliml"}));
MK_CONSTANT(conj_fn, name("Conj")); MK_CONSTANT(conjunct2_fn, name({"and", "elimr"}));
MK_CONSTANT(conjunct1_fn, name("Conjunct1")); MK_CONSTANT(disj1_fn, name({"or", "introl"}));
MK_CONSTANT(conjunct2_fn, name("Conjunct2")); MK_CONSTANT(disj2_fn, name({"or", "intror"}));
MK_CONSTANT(disj1_fn, name("Disj1")); MK_CONSTANT(disj_cases_fn, name({"or", "elim"}));
MK_CONSTANT(disj2_fn, name("Disj2")); MK_CONSTANT(refute_fn, name("refute"));
MK_CONSTANT(disj_cases_fn, name("DisjCases")); MK_CONSTANT(symm_fn, name("symm"));
MK_CONSTANT(refute_fn, name("Refute")); MK_CONSTANT(trans_fn, name("trans"));
MK_CONSTANT(symm_fn, name("Symm")); MK_CONSTANT(congr1_fn, name("congr1"));
MK_CONSTANT(trans_fn, name("Trans")); MK_CONSTANT(congr2_fn, name("congr2"));
MK_CONSTANT(congr1_fn, name("Congr1")); MK_CONSTANT(congr_fn, name("congr"));
MK_CONSTANT(congr2_fn, name("Congr2")); MK_CONSTANT(eqt_elim_fn, name({"eqt", "elim"}));
MK_CONSTANT(congr_fn, name("Congr")); MK_CONSTANT(eqt_intro_fn, name({"eqt", "intro"}));
MK_CONSTANT(eqt_elim_fn, name("EqTElim")); MK_CONSTANT(forall_elim_fn, name({"forall", "elim"}));
MK_CONSTANT(eqt_intro_fn, name("EqTIntro")); MK_CONSTANT(forall_intro_fn, name({"forall", "intro"}));
MK_CONSTANT(forall_elim_fn, name("ForallElim")); MK_CONSTANT(exists_elim_fn, name({"exists", "elim"}));
MK_CONSTANT(forall_intro_fn, name("ForallIntro")); MK_CONSTANT(exists_intro_fn, name({"exists", "intro"}));
MK_CONSTANT(exists_elim_fn, name("ExistsElim"));
MK_CONSTANT(exists_intro_fn, name("ExistsIntro"));
void import_kernel(environment const & env, io_state const & ios) { void import_kernel(environment const & env, io_state const & ios) {
env->import("kernel", ios); env->import("kernel", ios);

2
src/tests/frontends/lean/frontend.cpp
View file

@ -120,7 +120,7 @@ static void tst8() {
environment env; io_state ios = init_frontend(env); environment env; io_state ios = init_frontend(env);
formatter fmt = mk_pp_formatter(env); formatter fmt = mk_pp_formatter(env);
add_infixl(env, ios, "<-$->", 10, mk_refl_fn()); add_infixl(env, ios, "<-$->", 10, mk_refl_fn());
std::cout << fmt(*(env->find_object("Trivial"))) << "\n"; std::cout << fmt(*(env->find_object("trivial"))) << "\n";
} }
static void tst9() { static void tst9() {

10
src/tests/library/rewriter/rewriter.cpp
View file

@ -341,7 +341,7 @@ static void try_rewriter1_tst() {
cout << " " << concl << " := " << proof << std::endl; cout << " " << concl << " := " << proof << std::endl;
lean_assert_eq(concl, mk_eq(a_plus_b, a_plus_b)); lean_assert_eq(concl, mk_eq(a_plus_b, a_plus_b));
lean_assert_eq(proof, Const("Refl")(Nat, a_plus_b)); lean_assert_eq(proof, Const("refl")(Nat, a_plus_b));
env->add_theorem("New_theorem6", concl, proof); env->add_theorem("New_theorem6", concl, proof);
} }
@ -451,7 +451,7 @@ static void app_rewriter1_tst() {
<< "Proof = " << proof << std::endl; << "Proof = " << proof << std::endl;
lean_assert_eq(concl, mk_eq(v, f1(b_plus_a))); lean_assert_eq(concl, mk_eq(v, f1(b_plus_a)));
lean_assert_eq(proof, lean_assert_eq(proof,
Const("Congr2")(Nat, Fun(name("_"), Nat, Nat), a_plus_b, b_plus_a, f1, Const("ADD_COMM")(a, b))); Const("congr2")(Nat, Fun(name("_"), Nat, Nat), a_plus_b, b_plus_a, f1, Const("ADD_COMM")(a, b)));
env->add_theorem("app_rewriter2", concl, proof); env->add_theorem("app_rewriter2", concl, proof);
cout << "====================================================" << std::endl; cout << "====================================================" << std::endl;
v = f4(nVal(0), a_plus_b, nVal(0), b_plus_a); v = f4(nVal(0), a_plus_b, nVal(0), b_plus_a);
@ -464,11 +464,11 @@ static void app_rewriter1_tst() {
// Congr Nat (fun _ : Nat, Nat) (f4 0 (Nat::add a b) 0) (f4 0 (Nat::add b a) 0) (Nat::add b a) (Nat::add a b) (Congr1 Nat (fun _ : Nat, (Nat -> Nat)) (f4 0 (Nat::add a b)) (f4 0 (Nat::add b a)) 0 (Congr2 Nat (fun _ : Nat, (Nat -> Nat -> Nat)) (Nat::add a b) (Nat::add b a) (f4 0) (ADD_COMM a b))) (ADD_COMM b a) // Congr Nat (fun _ : Nat, Nat) (f4 0 (Nat::add a b) 0) (f4 0 (Nat::add b a) 0) (Nat::add b a) (Nat::add a b) (Congr1 Nat (fun _ : Nat, (Nat -> Nat)) (f4 0 (Nat::add a b)) (f4 0 (Nat::add b a)) 0 (Congr2 Nat (fun _ : Nat, (Nat -> Nat -> Nat)) (Nat::add a b) (Nat::add b a) (f4 0) (ADD_COMM a b))) (ADD_COMM b a)
lean_assert_eq(proof, lean_assert_eq(proof,
Const("Congr")(Nat, Fun(name("_"), Nat, Nat), f4(zero, a_plus_b, zero), f4(zero, b_plus_a, zero), Const("congr")(Nat, Fun(name("_"), Nat, Nat), f4(zero, a_plus_b, zero), f4(zero, b_plus_a, zero),
b_plus_a, a_plus_b, b_plus_a, a_plus_b,
Const("Congr1")(Nat, Fun(name("_"), Nat, Nat >> Nat), f4(zero, a_plus_b), Const("congr1")(Nat, Fun(name("_"), Nat, Nat >> Nat), f4(zero, a_plus_b),
f4(zero, b_plus_a), zero, f4(zero, b_plus_a), zero,
Const("Congr2")(Nat, Fun(name("_"), Nat, Nat >> (Nat >> Nat)), Const("congr2")(Nat, Fun(name("_"), Nat, Nat >> (Nat >> Nat)),
a_plus_b, b_plus_a, f4(zero), a_plus_b, b_plus_a, f4(zero),
Const("ADD_COMM")(a, b))), Const("ADD_COMM")(a, b))),
Const("ADD_COMM")(b, a))); Const("ADD_COMM")(b, a)));

4
tests/lean/abst.lean
View file

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

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

@ -3,7 +3,7 @@
Imported 'Int' Imported 'Int'
Assumed: PlusComm Assumed: PlusComm
Assumed: a Assumed: a
Abst (λ x : ℤ, PlusComm a x) : (λ x : ℤ, a + x) == (λ x : ℤ, x + a) abst (λ x : ℤ, PlusComm a x) : (λ x : ℤ, a + x) == (λ x : ℤ, x + a)
Set: lean::pp::implicit Set: lean::pp::implicit
@Abst ℤ (λ x : ℤ, ℤ) (λ x : ℤ, a + x) (λ x : ℤ, x + a) (λ x : ℤ, PlusComm a x) : @abst ℤ (λ x : ℤ, ℤ) (λ x : ℤ, a + x) (λ x : ℤ, x + a) (λ x : ℤ, PlusComm a x) :
(λ x : ℤ, a + x) == (λ x : ℤ, x + a) (λ x : ℤ, a + x) == (λ x : ℤ, x + a)

4
tests/lean/apply_tac1.lean
View file

@ -5,7 +5,7 @@ variable f : Int -> Int -> Bool
variable P : Int -> Int -> Bool variable P : Int -> Int -> Bool
axiom Ax1 (x y : Int) (H : P x y) : (f x y) axiom Ax1 (x y : Int) (H : P x y) : (f x y)
theorem T1 (a : Int) : (P a a) => (f a a). theorem T1 (a : Int) : (P a a) => (f a a).
apply Discharge. apply discharge.
apply Ax1. apply Ax1.
exact. exact.
done. done.
@ -19,7 +19,7 @@ theorem T2 (a : Int) : (P a a) => (f a a).
done. done.
theorem T3 (a : Int) : (P a a) => (f a a). theorem T3 (a : Int) : (P a a) => (f a a).
Repeat (OrElse (apply Discharge) exact (apply Ax2) (apply Ax1)). Repeat (OrElse (apply discharge) exact (apply Ax2) (apply Ax1)).
done. done.
print environment 2. print environment 2.

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

@ -10,5 +10,5 @@
Assumed: Ax2 Assumed: Ax2
Proved: T2 Proved: T2
Proved: T3 Proved: T3
theorem T2 (a : ℤ) : P a a ⇒ f a a := Discharge (λ H : P a a, Ax1 a a H) 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 T3 (a : ℤ) : P a a ⇒ f a a := discharge (λ H : P a a, Ax1 a a H)

8
tests/lean/apply_tac2.lean
View file

@ -1,8 +1,8 @@
(* import("tactic.lua") *) (* import("tactic.lua") *)
check @Discharge check @discharge
theorem T (a b : Bool) : a => b => b => a. theorem T (a b : Bool) : a => b => b => a.
apply Discharge. apply discharge.
apply Discharge. apply discharge.
apply Discharge. apply discharge.
exact. exact.
done. done.

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

@ -1,4 +1,4 @@
Set: pp::colors Set: pp::colors
Set: pp::unicode Set: pp::unicode
@Discharge : Π (a b : Bool), (a → b) → (a ⇒ b) @discharge : Π (a b : Bool), (a → b) → (a ⇒ b)
Proved: T Proved: T

2
tests/lean/bad10.lean
View file

@ -3,6 +3,6 @@ setoption pp::colors false.
variable N : Type. variable N : Type.
definition T (a : N) (f : _ -> _) (H : f a == a) : f (f _) == f _ := definition T (a : N) (f : _ -> _) (H : f a == a) : f (f _) == f _ :=
SubstP (fun x : N, f (f a) == _) (Refl (f (f _))) H. substp (fun x : N, f (f a) == _) (refl (f (f _))) H.
print environment 1. print environment 1.

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

@ -5,4 +5,4 @@
Assumed: N Assumed: N
Defined: T Defined: T
definition T (a : N) (f : N → N) (H : f a == a) : f (f a) == f (f a) := definition T (a : N) (f : N → N) (H : f a == a) : f (f a) == f (f a) :=
@SubstP N (f a) a (λ x : N, f (f a) == f (f a)) (@Refl N (f (f a))) H @substp N (f a) a (λ x : N, f (f a) == f (f a)) (@refl N (f (f a))) H

2
tests/lean/bad5.lean
View file

@ -4,5 +4,5 @@ variable a : Int
variable b : Int variable b : Int
axiom H1 : a = b axiom H1 : a = b
axiom H2 : (g a) > 0 axiom H2 : (g a) > 0
theorem T1 : (g b) > 0 := SubstP (λ x, (g x) > 0) H2 H1 theorem T1 : (g b) > 0 := substp (λ x, (g x) > 0) H2 H1
print environment 2 print environment 2

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

@ -8,4 +8,4 @@
Assumed: H2 Assumed: H2
Proved: T1 Proved: T1
axiom H2 : g a > 0 axiom H2 : g a > 0
theorem T1 : g b > 0 := SubstP (λ x : ℤ, g x > 0) H2 H1 theorem T1 : g b > 0 := substp (λ x : ℤ, g x > 0) H2 H1

2
tests/lean/bad9.lean
View file

@ -4,5 +4,5 @@ variable N : Type.
check check
fun (a : N) (f : N -> N) (H : f a == a), fun (a : N) (f : N -> N) (H : f a == a),
let calc1 : f a == a := SubstP (fun x : N, f a == _) (Refl (f a)) H let calc1 : f a == a := substp (fun x : N, f a == _) (refl (f a)) H
in calc1. in calc1.

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

@ -4,5 +4,5 @@
Set: pp::colors Set: pp::colors
Assumed: N Assumed: N
λ (a : N) (f : N → N) (H : f a == a), λ (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 : 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

2
tests/lean/bug.lean
View file

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

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

@ -3,7 +3,7 @@
Failed to solve Failed to solve
A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::3 ≺ TypeU A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::3 ≺ TypeU
(line: 1: pos: 44) Type of argument 1 must be convertible to the expected type in the application of (line: 1: pos: 44) Type of argument 1 must be convertible to the expected type in the application of
@Symm @symm
with arguments: with arguments:
?M::0 ?M::0
A A

2
tests/lean/cast1.lean
View file

@ -4,7 +4,7 @@ import Int.
variable vector : Type -> Nat -> Type variable vector : Type -> Nat -> Type
axiom N0 (n : Nat) : n + 0 = n axiom N0 (n : Nat) : n + 0 = n
theorem V0 (T : Type) (n : Nat) : (vector T (n + 0)) = (vector T n) := theorem V0 (T : Type) (n : Nat) : (vector T (n + 0)) = (vector T n) :=
Congr (Refl (vector T)) (N0 n) congr (refl (vector T)) (N0 n)
variable f (n : Nat) (v : vector Int n) : Int variable f (n : Nat) (v : vector Int n) : Int
variable m : Nat variable m : Nat
variable v1 : vector Int (m + 0) variable v1 : vector Int (m + 0)

8
tests/lean/cast2.lean
View file

@ -5,8 +5,8 @@ variable A' : Type
variable B' : Type variable B' : Type
axiom H : (A -> B) = (A' -> B') axiom H : (A -> B) = (A' -> B')
variable a : A variable a : A
check DomInj H check dominj H
theorem BeqB' : B = B' := RanInj H a theorem BeqB' : B = B' := raninj H a
setoption pp::implicit true setoption pp::implicit true
print DomInj H print dominj H
print RanInj H a print raninj H a

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

@ -7,8 +7,8 @@
Assumed: B' Assumed: B'
Assumed: H Assumed: H
Assumed: a Assumed: a
DomInj H : A == A' dominj H : A == A'
Proved: BeqB' Proved: BeqB'
Set: lean::pp::implicit Set: lean::pp::implicit
@DomInj A A' (λ x : A, B) (λ x : A', B') H @dominj A A' (λ x : A, B) (λ x : A', B') H
@RanInj A A' (λ x : A, B) (λ x : A', B') H a @raninj A A' (λ x : A, B) (λ x : A', B') H a

4
tests/lean/cast3.lean
View file

@ -2,8 +2,8 @@ import cast
variables A A' B B' : Type variables A A' B B' : Type
variable x : A variable x : A
eval cast (Refl A) x eval cast (refl A) x
eval x = (cast (Refl A) x) eval x = (cast (refl A) x)
variable b : B variable b : B
definition f (x : A) : B := b definition f (x : A) : B := b
axiom H : (A -> B) = (A' -> B) axiom H : (A -> B) = (A' -> B)

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

@ -6,8 +6,8 @@
Assumed: B Assumed: B
Assumed: B' Assumed: B'
Assumed: x Assumed: x
cast (Refl A) x cast (refl A) x
x == cast (Refl A) x x == cast (refl A) x
Assumed: b Assumed: b
Defined: f Defined: f
Assumed: H Assumed: H

22
tests/lean/cast4.lean
View file

@ -12,16 +12,16 @@ check fun (A A': TypeM)
(H2 : f == g) (H2 : f == g)
(H3 : a == b), (H3 : a == b),
let let
S1 : (Pi x : A', B' x) == (Pi x : A, B x) := Symm H1, S1 : (Pi x : A', B' x) == (Pi x : A, B x) := symm H1,
L2 : A' == A := DomInj S1, L2 : A' == A := dominj S1,
b' : A := cast L2 b, b' : A := cast L2 b,
L3 : b == b' := CastEq L2 b, L3 : b == b' := cast::eq L2 b,
L4 : a == b' := HTrans H3 L3, L4 : a == b' := htrans H3 L3,
L5 : f a == f b' := Congr2 f L4, L5 : f a == f b' := congr2 f L4,
g' : (Pi x : A, B x) := cast S1 g, g' : (Pi x : A, B x) := cast S1 g,
L6 : g == g' := CastEq S1 g, L6 : g == g' := cast::eq S1 g,
L7 : f == g' := HTrans H2 L6, L7 : f == g' := htrans H2 L6,
L8 : f b' == g' b' := Congr1 b' L7, L8 : f b' == g' b' := congr1 b' L7,
L9 : f a == g' b' := HTrans L5 L8, L9 : f a == g' b' := htrans L5 L8,
L10 : g' b' == g b := CastApp S1 L2 g b L10 : g' b' == g b := cast::app S1 L2 g b
in HTrans L9 L10 in htrans L9 L10

22
tests/lean/cast4.lean.expected.out
View file

@ -12,18 +12,18 @@
(H1 : (Π x : A, B x) == (Π x : A', B' x)) (H1 : (Π x : A, B x) == (Π x : A', B' x))
(H2 : f == g) (H2 : f == g)
(H3 : a == b), (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, L2 : A' == A := dominj S1,
b' : A := cast L2 b, b' : A := cast L2 b,
L3 : b == b' := CastEq L2 b, L3 : b == b' := cast::eq L2 b,
L4 : a == b' := HTrans H3 L3, L4 : a == b' := htrans H3 L3,
L5 : f a == f b' := Congr2 f L4, 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' := CastEq S1 g, L6 : g == g' := cast::eq S1 g,
L7 : f == g' := HTrans H2 L6, L7 : f == g' := htrans H2 L6,
L8 : f b' == g' b' := Congr1 b' L7, L8 : f b' == g' b' := congr1 b' L7,
L9 : f a == g' b' := HTrans L5 L8, L9 : f a == g' b' := htrans L5 L8,
L10 : g' b' == g b := CastApp S1 L2 g b L10 : g' b' == g b := cast::app S1 L2 g b
in HTrans L9 L10 : 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'), Π (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 (Π x : A, B x) == (Π x : A', B' x) → f == g → a == b → f a == g b

8
tests/lean/discharge.lean
View file

@ -1,8 +1,8 @@
import tactic import tactic
check @Discharge check @discharge
theorem T (a b : Bool) : a => b => b => a. theorem T (a b : Bool) : a => b => b => a.
apply Discharge. apply discharge.
apply Discharge. apply discharge.
apply Discharge. apply discharge.
exact. exact.
done. done.

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

@ -1,5 +1,5 @@
Set: pp::colors Set: pp::colors
Set: pp::unicode Set: pp::unicode
Imported 'tactic' Imported 'tactic'
@Discharge : Π (a b : Bool), (a → b) → (a ⇒ b) @discharge : Π (a b : Bool), (a → b) → (a ⇒ b)
Proved: T Proved: T

2
tests/lean/disj1.lean
View file

@ -1,7 +1,7 @@
import tactic import tactic
theorem T1 (a b : Bool) : a \/ b => b \/ a. theorem T1 (a b : Bool) : a \/ b => b \/ a.
apply Discharge. apply discharge.
(* disj_hyp_tac() *) (* disj_hyp_tac() *)
(* disj_tac() *) (* disj_tac() *)
back back

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

@ -4,4 +4,4 @@
Proved: T1 Proved: T1
Proved: T2 Proved: T2
theorem T2 (a b : Bool) : a ∨ b ⇒ b ∨ a := theorem T2 (a b : Bool) : a ∨ b ⇒ b ∨ a :=
Discharge (λ H : a ∨ b, DisjCases H (λ H : a, Disj2 b H) (λ H : b, Disj1 H a)) discharge (λ H : a ∨ b, or::elim H (λ H : a, or::intror b H) (λ H : b, or::introl H a))

8
tests/lean/disjcases.lean
View file

@ -2,10 +2,10 @@
variables a b c : Bool variables a b c : Bool
axiom H : a \/ b axiom H : a \/ b
theorem T (a b : Bool) : a \/ b => b \/ a. theorem T (a b : Bool) : a \/ b => b \/ a.
apply Discharge. apply discharge.
apply (DisjCases H). apply (or::elim H).
apply Disj2. apply or::intror.
exact. exact.
apply Disj1. apply or::introl.
exact. exact.
done. done.

8
tests/lean/elab1.lean
View file

@ -1,5 +1,3 @@
variable f {A : Type} (a b : A) : A. variable f {A : Type} (a b : A) : A.
check f 10 true check f 10 true
@ -17,13 +15,13 @@ check fun (A B : Type) (a : _) (b : _) (C : Type), my_eq C a b.
variable a : Bool variable a : Bool
variable b : Bool variable b : Bool
variable H : a /\ b variable H : a /\ b
theorem t1 : b := Discharge (fun H1, Conj H1 (Conjunct1 H)). theorem t1 : b := discharge (fun H1, and::intro H1 (and::eliml H)).
theorem t2 : a = b := Trans (Refl a) (Refl b). theorem t2 : a = b := trans (refl a) (refl b).
check f Bool Bool. check f Bool Bool.
theorem pierce (a b : Bool) : ((a ⇒ b) ⇒ a) ⇒ a := theorem pierce (a b : Bool) : ((a ⇒ b) ⇒ a) ⇒ a :=
Discharge (λ H, DisjCases (EM a) discharge (λ H, or::elim (EM a)
(λ H_a, H) (λ H_a, H)
(λ H_na, NotImp1 (MT H H_na))) (λ H_na, NotImp1 (MT H H_na)))

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

@ -3,19 +3,19 @@
Assumed: f Assumed: f
Failed to solve Failed to solve
⊢ Bool ≺ ℕ ⊢ Bool ≺ ℕ
(line: 4: pos: 6) Type of argument 3 must be convertible to the expected type in the application of (line: 2: pos: 6) Type of argument 3 must be convertible to the expected type in the application of
@f @f
with arguments: with arguments:
ℕ ℕ
10 10
⊤ ⊤
Assumed: g Assumed: g
Error (line: 7, pos: 8) invalid expression, it still contains metavariables after elaboration, metavariable: ?M::1, type: Error (line: 5, pos: 8) invalid expression, it still contains metavariables after elaboration, metavariable: ?M::1, type:
Type Type
Assumed: h Assumed: h
Failed to solve Failed to solve
x : ?M::0, A : Type ⊢ ?M::0 ≺ A x : ?M::0, A : Type ⊢ ?M::0 ≺ A
(line: 11: pos: 27) Type of argument 2 must be convertible to the expected type in the application of (line: 9: pos: 27) Type of argument 2 must be convertible to the expected type in the application of
h h
with arguments: with arguments:
A A
@ -23,7 +23,7 @@ x : ?M::0, A : Type ⊢ ?M::0 ≺ A
Assumed: my_eq Assumed: my_eq
Failed to solve Failed to solve
A : Type, B : Type, a : ?M::0, b : ?M::1, C : Type ⊢ ?M::0[lift:0:3] ≺ C A : Type, B : Type, a : ?M::0, b : ?M::1, C : Type ⊢ ?M::0[lift:0:3] ≺ C
(line: 15: pos: 51) Type of argument 2 must be convertible to the expected type in the application of (line: 13: pos: 51) Type of argument 2 must be convertible to the expected type in the application of
my_eq my_eq
with arguments: with arguments:
C C
@ -34,34 +34,24 @@ A : Type, B : Type, a : ?M::0, b : ?M::1, C : Type ⊢ ?M::0[lift:0:3] ≺ C
Assumed: H Assumed: H
Failed to solve Failed to solve
⊢ ?M::0 ⇒ ?M::3 ∧ a ≺ b ⊢ ?M::0 ⇒ ?M::3 ∧ a ≺ b
(line: 20: pos: 18) Type of definition 't1' must be convertible to expected type. (line: 18: pos: 18) Type of definition 't1' must be convertible to expected type.
Failed to solve Failed to solve
⊢ b == b ≺ a == b ⊢ b == b ≺ a == b
(line: 22: pos: 22) Type of argument 6 must be convertible to the expected type in the application of (line: 20: pos: 22) Type of argument 6 must be convertible to the expected type in the application of
@Trans @trans
with arguments: with arguments:
?M::1 ?M::1
a a
a a
b b
Refl a refl a
Refl b refl b
Failed to solve Failed to solve
⊢ ?M::1 ≺ Type ⊢ ?M::1 ≺ Type
(line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of (line: 22: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
@f @f
with arguments: with arguments:
?M::0 ?M::0
Bool Bool
Bool Bool
Failed to solve Error (line: 25, pos: 31) unknown identifier 'EM'
a : Bool, b : Bool, H : (a ⇒ b) ⇒ a ⊢ a → (a ⇒ b) ⇒ a ≺ a → a
(line: 27: pos: 21) Type of argument 5 must be convertible to the expected type in the application of
@DisjCases
with arguments:
a
¬ a
a
EM a
λ H_a : a, H
λ H_na : ¬ a, NotImp1 (MT H H_na)

20
tests/lean/elab7.lean
View file

@ -4,18 +4,18 @@ variable F1 : A -> B -> C
variable F2 : A -> B -> C variable F2 : A -> B -> C
variable H : Pi (a : A) (b : B), (F1 a b) == (F2 a b) variable H : Pi (a : A) (b : B), (F1 a b) == (F2 a b)
variable a : A variable a : A
check Eta (F2 a) check eta (F2 a)
check Abst (fun a : A, check abst (fun a : A,
(Trans (Symm (Eta (F1 a))) (trans (symm (eta (F1 a)))
(Trans (Abst (fun (b : B), H a b)) (trans (abst (fun (b : B), H a b))
(Eta (F2 a))))) (eta (F2 a)))))
check Abst (fun a, (Abst (fun b, H a b))) check abst (fun a, (abst (fun b, H a b)))
theorem T1 : F1 = F2 := Abst (fun a, (Abst (fun b, H a b))) theorem T1 : F1 = F2 := abst (fun a, (abst (fun b, H a b)))
theorem T2 : (fun (x1 : A) (x2 : B), F1 x1 x2) = F2 := Abst (fun a, (Abst (fun b, H a b))) theorem T2 : (fun (x1 : A) (x2 : B), F1 x1 x2) = F2 := abst (fun a, (abst (fun b, H a b)))
theorem T3 : F1 = (fun (x1 : A) (x2 : B), F2 x1 x2) := Abst (fun a, (Abst (fun b, H a b))) theorem T3 : F1 = (fun (x1 : A) (x2 : B), F2 x1 x2) := abst (fun a, (abst (fun b, H a b)))
theorem T4 : (fun (x1 : A) (x2 : B), F1 x1 x2) = (fun (x1 : A) (x2 : B), F2 x1 x2) := Abst (fun a, (Abst (fun b, H a b))) theorem T4 : (fun (x1 : A) (x2 : B), F1 x1 x2) = (fun (x1 : A) (x2 : B), F2 x1 x2) := abst (fun a, (abst (fun b, H a b)))
print environment 4 print environment 4
setoption pp::implicit true setoption pp::implicit true
print environment 4 print environment 4

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

@ -8,37 +8,36 @@
Assumed: F2 Assumed: F2
Assumed: H Assumed: H
Assumed: a Assumed: a
Eta (F2 a) : (λ x : B, F2 a x) == F2 a eta (F2 a) : (λ x : B, F2 a x) == F2 a
Abst (λ a : A, Trans (Symm (Eta (F1 a))) (Trans (Abst (λ b : B, H a b)) (Eta (F2 a)))) : abst (λ a : A, symm (eta (F1 a)) ⋈ (abst (λ b : B, H a b) ⋈ eta (F2 a))) : (λ x : A, F1 x) == (λ x : A, F2 x)
(λ x : A, F1 x) == (λ x : A, F2 x) abst (λ a : A, abst (λ b : B, H a b)) : (λ (x : A) (x::1 : B), F1 x x::1) == (λ (x : A) (x::1 : B), F2 x x::1)
Abst (λ a : A, Abst (λ b : B, H a b)) : (λ (x : A) (x::1 : B), F1 x x::1) == (λ (x : A) (x::1 : B), F2 x x::1)
Proved: T1 Proved: T1
Proved: T2 Proved: T2
Proved: T3 Proved: T3
Proved: T4 Proved: T4
theorem T1 : F1 = F2 := Abst (λ a : A, Abst (λ b : B, H a b)) theorem T1 : F1 = F2 := abst (λ a : A, abst (λ b : B, H a b))
theorem T2 : (λ (x1 : A) (x2 : B), F1 x1 x2) = F2 := Abst (λ a : A, Abst (λ b : B, H a b)) theorem T2 : (λ (x1 : A) (x2 : B), F1 x1 x2) = F2 := abst (λ a : A, abst (λ b : B, H a b))
theorem T3 : F1 = (λ (x1 : A) (x2 : B), F2 x1 x2) := Abst (λ a : A, Abst (λ b : B, H a b)) theorem T3 : F1 = (λ (x1 : A) (x2 : B), F2 x1 x2) := abst (λ a : A, abst (λ b : B, H a b))
theorem T4 : (λ (x1 : A) (x2 : B), F1 x1 x2) = (λ (x1 : A) (x2 : B), F2 x1 x2) := theorem T4 : (λ (x1 : A) (x2 : B), F1 x1 x2) = (λ (x1 : A) (x2 : B), F2 x1 x2) :=
Abst (λ a : A, Abst (λ b : B, H a b)) abst (λ a : A, abst (λ b : B, H a b))
Set: lean::pp::implicit Set: lean::pp::implicit
theorem T1 : @eq (A → B → C) F1 F2 := theorem T1 : @eq (A → B → C) F1 F2 :=
@Abst A (λ x : A, B → C) F1 F2 (λ a : A, @Abst B (λ x : B, C) (F1 a) (F2 a) (λ b : B, H a b)) @abst A (λ x : A, B → C) F1 F2 (λ a : A, @abst B (λ x : B, C) (F1 a) (F2 a) (λ b : B, H a b))
theorem T2 : @eq (A → B → C) (λ (x1 : A) (x2 : B), F1 x1 x2) F2 := theorem T2 : @eq (A → B → C) (λ (x1 : A) (x2 : B), F1 x1 x2) F2 :=
@Abst A @abst A
(λ x : A, B → C) (λ x : A, B → C)
(λ (x1 : A) (x2 : B), F1 x1 x2) (λ (x1 : A) (x2 : B), F1 x1 x2)
F2 F2
(λ a : A, @Abst B (λ x : B, C) (λ x2 : B, F1 a x2) (F2 a) (λ b : B, H a b)) (λ a : A, @abst B (λ x : B, C) (λ x2 : B, F1 a x2) (F2 a) (λ b : B, H a b))
theorem T3 : @eq (A → B → C) F1 (λ (x1 : A) (x2 : B), F2 x1 x2) := theorem T3 : @eq (A → B → C) F1 (λ (x1 : A) (x2 : B), F2 x1 x2) :=
@Abst A @abst A
(λ x : A, B → C) (λ x : A, B → C)
F1 F1
(λ (x1 : A) (x2 : B), F2 x1 x2) (λ (x1 : A) (x2 : B), F2 x1 x2)
(λ a : A, @Abst B (λ x : B, C) (F1 a) (λ x2 : B, F2 a x2) (λ b : B, H a b)) (λ a : A, @abst B (λ x : B, C) (F1 a) (λ x2 : B, F2 a x2) (λ b : B, H a b))
theorem T4 : @eq (A → B → C) (λ (x1 : A) (x2 : B), F1 x1 x2) (λ (x1 : A) (x2 : B), F2 x1 x2) := theorem T4 : @eq (A → B → C) (λ (x1 : A) (x2 : B), F1 x1 x2) (λ (x1 : A) (x2 : B), F2 x1 x2) :=
@Abst A @abst A
(λ x : A, B → C) (λ x : A, B → C)
(λ (x1 : A) (x2 : B), F1 x1 x2) (λ (x1 : A) (x2 : B), F1 x1 x2)
(λ (x1 : A) (x2 : B), F2 x1 x2) (λ (x1 : A) (x2 : B), F2 x1 x2)
(λ a : A, @Abst B (λ x : B, C) (λ x2 : B, F1 a x2) (λ x2 : B, F2 a x2) (λ b : B, H a b)) (λ a : A, @abst B (λ x : B, C) (λ x2 : B, F1 a x2) (λ x2 : B, F2 a x2) (λ b : B, H a b))

4
tests/lean/eq3.lean
View file

@ -5,6 +5,6 @@ variable v2 : Vector (n + 0)
variable v3 : Vector (0 + n) variable v3 : Vector (0 + n)
axiom H1 : v1 == v2 axiom H1 : v1 == v2
axiom H2 : v2 == v3 axiom H2 : v2 == v3
check HTrans H1 H2 check htrans H1 H2
setoption pp::implicit true setoption pp::implicit true
check HTrans H1 H2 check htrans H1 H2

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

@ -7,6 +7,6 @@
Assumed: v3 Assumed: v3
Assumed: H1 Assumed: H1
Assumed: H2 Assumed: H2
HTrans H1 H2 : v1 == v3 htrans H1 H2 : v1 == v3
Set: lean::pp::implicit Set: lean::pp::implicit
@HTrans (Vector n) (Vector (n + 0)) (Vector (0 + n)) v1 v2 v3 H1 H2 : v1 == v3 @htrans (Vector n) (Vector (n + 0)) (Vector (0 + n)) v1 v2 v3 H1 H2 : v1 == v3

2
tests/lean/errmsg1.lean
View file

@ -5,4 +5,4 @@ check fun x, x
theorem T (A : Type) (x : A) : Pi (y : A), A theorem T (A : Type) (x : A) : Pi (y : A), A
:= _. := _.
theorem T (x : _) : x = x := Refl x. theorem T (x : _) : x = x := refl x.

2
tests/lean/exists1.lean
View file

@ -2,5 +2,5 @@ import Int.
variable a : Int variable a : Int
variable P : Int -> Int -> Bool variable P : Int -> Int -> Bool
axiom H : P a a axiom H : P a a
theorem T : exists x : Int, P a a := ExistsIntro a H. theorem T : exists x : Int, P a a := exists::intro a H.
print environment 1. print environment 1.

2
tests/lean/exists1.lean.expected.out
View file

@ -5,4 +5,4 @@
Assumed: P Assumed: P
Assumed: H Assumed: H
Proved: T Proved: T
theorem T : ∃ x : ℤ, P a a := ExistsIntro a H theorem T : ∃ x : ℤ, P a a := exists::intro a H

16
tests/lean/exists2.lean
View file

@ -6,13 +6,13 @@ variable g : Int -> Int
axiom H1 : P (f a (g a)) (f a (g a)) axiom H1 : P (f a (g a)) (f a (g a))
axiom H2 : P (f (g a) (g a)) (f (g a) (g a)) axiom H2 : P (f (g a) (g a)) (f (g a) (g a))
axiom H3 : P (f (g a) (g a)) (g a) axiom H3 : P (f (g a) (g a)) (g a)
theorem T1 : exists x y : Int, P (f y x) (f y x) := ExistsIntro _ (ExistsIntro _ H1) theorem T1 : exists x y : Int, P (f y x) (f y x) := exists::intro _ (exists::intro _ H1)
theorem T2 : exists x : Int, P (f x (g x)) (f x (g x)) := ExistsIntro _ H1 theorem T2 : exists x : Int, P (f x (g x)) (f x (g x)) := exists::intro _ H1
theorem T3 : exists x : Int, P (f x x) (f x x) := ExistsIntro _ H2 theorem T3 : exists x : Int, P (f x x) (f x x) := exists::intro _ H2
theorem T4 : exists x : Int, P (f (g a) x) (f x x) := ExistsIntro _ H2 theorem T4 : exists x : Int, P (f (g a) x) (f x x) := exists::intro _ H2
theorem T5 : exists x : Int, P x x := ExistsIntro _ H2 theorem T5 : exists x : Int, P x x := exists::intro _ H2
theorem T6 : exists x y : Int, P x y := ExistsIntro _ (ExistsIntro _ H3) theorem T6 : exists x y : Int, P x y := exists::intro _ (exists::intro _ H3)
theorem T7 : exists x : Int, P (f x x) x := ExistsIntro _ H3 theorem T7 : exists x : Int, P (f x x) x := exists::intro _ H3
theorem T8 : exists x y : Int, P (f x x) y := ExistsIntro _ (ExistsIntro _ H3) theorem T8 : exists x y : Int, P (f x x) y := exists::intro _ (exists::intro _ H3)
print environment 8. print environment 8.

16
tests/lean/exists2.lean.expected.out
View file

@ -16,11 +16,11 @@
Proved: T6 Proved: T6
Proved: T7 Proved: T7
Proved: T8 Proved: T8
theorem T1 : ∃ x y : ℤ, P (f y x) (f y x) := ExistsIntro (g a) (ExistsIntro a H1) theorem T1 : ∃ x y : ℤ, P (f y x) (f y x) := exists::intro (g a) (exists::intro a H1)
theorem T2 : ∃ x : ℤ, P (f x (g x)) (f x (g x)) := ExistsIntro a H1 theorem T2 : ∃ x : ℤ, P (f x (g x)) (f x (g x)) := exists::intro a H1
theorem T3 : ∃ x : ℤ, P (f x x) (f x x) := ExistsIntro (g a) H2 theorem T3 : ∃ x : ℤ, P (f x x) (f x x) := exists::intro (g a) H2
theorem T4 : ∃ x : ℤ, P (f (g a) x) (f x x) := ExistsIntro (g a) H2 theorem T4 : ∃ x : ℤ, P (f (g a) x) (f x x) := exists::intro (g a) H2
theorem T5 : ∃ x : ℤ, P x x := ExistsIntro (f (g a) (g a)) H2 theorem T5 : ∃ x : ℤ, P x x := exists::intro (f (g a) (g a)) H2
theorem T6 : ∃ x y : ℤ, P x y := ExistsIntro (f (g a) (g a)) (ExistsIntro (g a) H3) theorem T6 : ∃ x y : ℤ, P x y := exists::intro (f (g a) (g a)) (exists::intro (g a) H3)
theorem T7 : ∃ x : ℤ, P (f x x) x := ExistsIntro (g a) H3 theorem T7 : ∃ x : ℤ, P (f x x) x := exists::intro (g a) H3
theorem T8 : ∃ x y : ℤ, P (f x x) y := ExistsIntro (g a) (ExistsIntro (g a) H3) theorem T8 : ∃ x y : ℤ, P (f x x) y := exists::intro (g a) (exists::intro (g a) H3)

34
tests/lean/exists3.lean
View file

@ -4,26 +4,26 @@ variable P : Int -> Int -> Bool
setopaque exists false. setopaque exists false.
theorem T1 (R1 : not (exists x y, P x y)) : forall x y, not (P x y) := theorem T1 (R1 : not (exists x y, P x y)) : forall x y, not (P x y) :=
ForallIntro (fun a, forall::intro (fun a,
ForallIntro (fun b, forall::intro (fun b,
ForallElim (DoubleNegElim (ForallElim (DoubleNegElim R1) a)) b)) forall::elim (not::not::elim (forall::elim (not::not::elim R1) a)) b))
axiom Ax : forall x, exists y, P x y axiom Ax : forall x, exists y, P x y
theorem T2 : exists x y, P x y := theorem T2 : exists x y, P x y :=
Refute (fun R : not (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) := ForallIntro (fun a, let L1 : forall x y, not (P x y) := forall::intro (fun a,
ForallIntro (fun b, forall::intro (fun b,
ForallElim (DoubleNegElim (ForallElim (DoubleNegElim R) a)) b)), forall::elim (not::not::elim (forall::elim (not::not::elim R) a)) b)),
L2 : exists y, P 0 y := ForallElim Ax 0 L2 : exists y, P 0 y := forall::elim Ax 0
in ExistsElim L2 (fun (w : Int) (H : P 0 w), in exists::elim L2 (fun (w : Int) (H : P 0 w),
Absurd H (ForallElim (ForallElim L1 0) w))). absurd H (forall::elim (forall::elim 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 := 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), refute (fun R : not (exists x y, P x y),
let L1 : forall x y, not (P x y) := ForallIntro (fun a, let L1 : forall x y, not (P x y) := forall::intro (fun a,
ForallIntro (fun b, forall::intro (fun b,
ForallElim (DoubleNegElim (ForallElim (DoubleNegElim R) a)) b)), forall::elim (not::not::elim (forall::elim (not::not::elim R) a)) b)),
L2 : exists y, P a y := ForallElim H1 a L2 : exists y, P a y := forall::elim H1 a
in ExistsElim L2 (fun (w : A) (H : P a w), in exists::elim L2 (fun (w : A) (H : P a w),
Absurd H (ForallElim (ForallElim L1 a) w))). absurd H (forall::elim (forall::elim L1 a) w))).

12
tests/lean/exists4.lean
View file

@ -3,14 +3,14 @@ variables a b c : N
variables P : N -> N -> N -> Bool variables P : N -> N -> N -> Bool
axiom H3 : P a b c axiom H3 : P a b c
theorem T1 : exists x y z : N, P x y z := @ExistsIntro N (fun x : N, exists y z : N, P x y z) a theorem T1 : exists x y z : N, P x y z := exists::@intro N (fun x : N, exists y z : N, P x y z) a
(@ExistsIntro N _ b (exists::@intro N _ b
(@ExistsIntro N (fun z : N, P a b z) c H3)) (exists::@intro N (fun z : N, P a b z) c H3))
theorem T2 : exists x y z : N, P x y z := ExistsIntro a (ExistsIntro b (ExistsIntro c H3)) theorem T2 : exists x y z : N, P x y z := exists::intro a (exists::intro b (exists::intro c H3))
theorem T3 : exists x y z : N, P x y z := ExistsIntro _ (ExistsIntro _ (ExistsIntro _ H3)) theorem T3 : exists x y z : N, P x y z := exists::intro _ (exists::intro _ (exists::intro _ H3))
theorem T4 (H : P a a b) : exists x y z, P x y z := ExistsIntro _ (ExistsIntro _ (ExistsIntro _ H)) theorem T4 (H : P a a b) : exists x y z, P x y z := exists::intro _ (exists::intro _ (exists::intro _ H))
print environment 4 print environment 4

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

@ -11,11 +11,11 @@
Proved: T3 Proved: T3
Proved: T4 Proved: T4
theorem T1 : ∃ x y z : N, P x y z := theorem T1 : ∃ x y z : N, P x y z :=
@ExistsIntro exists::@intro
N N
(λ x : N, ∃ y z : N, P x y z) (λ x : N, ∃ y z : N, P x y z)
a a
(@ExistsIntro N (λ y : N, ∃ z : N, P a y z) b (@ExistsIntro N (λ z : N, P a b z) c H3)) (exists::@intro N (λ y : N, ∃ z : N, P a y z) b (exists::@intro N (λ z : N, P a b z) c H3))
theorem T2 : ∃ x y z : N, P x y z := ExistsIntro a (ExistsIntro b (ExistsIntro c H3)) theorem T2 : ∃ x y z : N, P x y z := exists::intro a (exists::intro b (exists::intro c H3))
theorem T3 : ∃ x y z : N, P x y z := ExistsIntro a (ExistsIntro b (ExistsIntro c H3)) theorem T3 : ∃ x y z : N, P x y z := exists::intro a (exists::intro b (exists::intro c H3))
theorem T4 (H : P a a b) : ∃ x y z : N, P x y z := ExistsIntro a (ExistsIntro a (ExistsIntro b H)) theorem T4 (H : P a a b) : ∃ x y z : N, P x y z := exists::intro a (exists::intro a (exists::intro b H))

2
tests/lean/exists5.lean
View file

@ -2,6 +2,6 @@ variable N : Type
variables a b c : N variables a b c : N
variables P : N -> N -> N -> Bool variables P : N -> N -> N -> Bool
theorem T1 (f : N -> N) (H : P (f a) b (f (f c))) : exists x y z, P x y z := ExistsIntro _ (ExistsIntro _ (ExistsIntro _ H)) theorem T1 (f : N -> N) (H : P (f a) b (f (f c))) : exists x y z, P x y z := exists::intro _ (exists::intro _ (exists::intro _ H))
print environment 1. print environment 1.

2
tests/lean/exists5.lean.expected.out
View file

@ -7,4 +7,4 @@
Assumed: P Assumed: P
Proved: T1 Proved: T1
theorem T1 (f : N → N) (H : P (f a) b (f (f c))) : ∃ x y z : N, P x y z := theorem T1 (f : N → N) (H : P (f a) b (f (f c))) : ∃ x y z : N, P x y z :=
ExistsIntro (f a) (ExistsIntro b (ExistsIntro (f (f c)) H)) exists::intro (f a) (exists::intro b (exists::intro (f (f c)) H))

6
tests/lean/exists6.lean
View file

@ -3,6 +3,6 @@ variable P : Int -> Int -> Int -> Bool
axiom Ax1 : exists x y z, P x y z axiom Ax1 : exists x y z, P x y z
axiom Ax2 : forall x y z, not (P x y z) axiom Ax2 : forall x y z, not (P x y z)
theorem T : false := theorem T : false :=
ExistsElim Ax1 (fun a H1, ExistsElim H1 (fun b H2, ExistsElim H2 (fun (c : Int) (H3 : P a b c), 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) := ForallElim (ForallElim (ForallElim Ax2 a) b) c let notH3 : not (P a b c) := forall::elim (forall::elim (forall::elim Ax2 a) b) c
in Absurd H3 notH3))) in absurd H3 notH3)))

2
tests/lean/exists7.lean
View file

@ -7,6 +7,6 @@ setopaque forall false.
setopaque exists false. setopaque exists false.
setopaque not false. setopaque not false.
theorem T1 (f : N -> N) (H : P (f a) b (f (f c))) : exists x y z, P x y z := ExistsIntro _ (ExistsIntro _ (ExistsIntro _ H)) theorem T1 (f : N -> N) (H : P (f a) b (f (f c))) : exists x y z, P x y z := exists::intro _ (exists::intro _ (exists::intro _ H))
print environment 1. print environment 1.

2
tests/lean/exists7.lean.expected.out
View file

@ -8,4 +8,4 @@
Assumed: P Assumed: P
Proved: T1 Proved: T1
theorem T1 (f : N → N) (H : P (f a) b (f (f c))) : ∃ x y z : N, P x y z := theorem T1 (f : N → N) (H : P (f a) b (f (f c))) : ∃ x y z : N, P x y z :=
ExistsIntro (f a) (ExistsIntro b (ExistsIntro (f (f c)) H)) exists::intro (f a) (exists::intro b (exists::intro (f (f c)) H))

34
tests/lean/exists8.lean
View file

@ -2,26 +2,26 @@ import Int.
variable P : Int -> Int -> Bool variable P : Int -> Int -> Bool
theorem T1 (R1 : not (exists x y, P x y)) : forall x y, not (P x y) := theorem T1 (R1 : not (exists x y, P x y)) : forall x y, not (P x y) :=
ForallIntro (fun a, forall::intro (fun a,
ForallIntro (fun b, forall::intro (fun b,
ForallElim (NotExistsElim (ForallElim (NotExistsElim R1) a)) b)) forall::elim (not::exists::elim (forall::elim (not::exists::elim R1) a)) b))
axiom Ax : forall x, exists y, P x y axiom Ax : forall x, exists y, P x y
theorem T2 : exists x y, P x y := theorem T2 : exists x y, P x y :=
Refute (fun R : not (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) := ForallIntro (fun a, let L1 : forall x y, not (P x y) := forall::intro (fun a,
ForallIntro (fun b, forall::intro (fun b,
ForallElim (NotExistsElim (ForallElim (NotExistsElim R) a)) b)), forall::elim (not::exists::elim (forall::elim (not::exists::elim R) a)) b)),
L2 : exists y, P 0 y := ForallElim Ax 0 L2 : exists y, P 0 y := forall::elim Ax 0
in ExistsElim L2 (fun (w : Int) (H : P 0 w), in exists::elim L2 (fun (w : Int) (H : P 0 w),
Absurd H (ForallElim (ForallElim L1 0) w))). absurd H (forall::elim (forall::elim 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 := 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), refute (fun R : not (exists x y, P x y),
let L1 : forall x y, not (P x y) := ForallIntro (fun a, let L1 : forall x y, not (P x y) := forall::intro (fun a,
ForallIntro (fun b, forall::intro (fun b,
ForallElim (NotExistsElim (ForallElim (NotExistsElim R) a)) b)), forall::elim (not::exists::elim (forall::elim (not::exists::elim R) a)) b)),
L2 : exists y, P a y := ForallElim H1 a L2 : exists y, P a y := forall::elim H1 a
in ExistsElim L2 (fun (w : A) (H : P a w), in exists::elim L2 (fun (w : A) (H : P a w),
Absurd H (ForallElim (ForallElim L1 a) w))). absurd H (forall::elim (forall::elim L1 a) w))).

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

@ -1,8 +1,8 @@
Set: pp::colors Set: pp::colors
Set: pp::unicode Set: pp::unicode
Imported 'find' 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 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 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 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: 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:24), no object name in the environment matches the regular expression '(ab' Error (line: 4, pos: 0) executing external script (/home/leo/projects/lean/build/debug/shell/find.lua:18), unfinished capture

2
tests/lean/forall1.lean
View file

@ -1,4 +1,4 @@
import Int. import Int.
variable P : Int -> Bool variable P : Int -> Bool
axiom Ax (x : Int) : P x axiom Ax (x : Int) : P x
check ForallIntro Ax check forall::intro Ax

2
tests/lean/forall1.lean.expected.out
View file

@ -3,4 +3,4 @@
Imported 'Int' Imported 'Int'
Assumed: P Assumed: P
Assumed: Ax Assumed: Ax
ForallIntro Ax : ∀ x : ℤ, P x forall::intro Ax : ∀ x : ℤ, P x

2
tests/lean/ho.lean
View file

@ -4,5 +4,5 @@ variable a : Int
variable b : Int variable b : Int
axiom H1 : a = b axiom H1 : a = b
axiom H2 : (g a) > 0 axiom H2 : (g a) > 0
theorem T1 : (g b) > 0 := Subst H2 H1 theorem T1 : (g b) > 0 := subst H2 H1
print environment 2 print environment 2

2
tests/lean/ho.lean.expected.out
View file

@ -8,4 +8,4 @@
Assumed: H2 Assumed: H2
Proved: T1 Proved: T1
axiom H2 : g a > 0 axiom H2 : g a > 0
theorem T1 : g b > 0 := Subst H2 H1 theorem T1 : g b > 0 := subst H2 H1

4
tests/lean/interactive/elab6.lean
View file

@ -5,5 +5,5 @@
local env = get_environment() local env = get_environment()
env:set_opaque("forall", false) env:set_opaque("forall", false)
*) *)
theorem ForallIntro2 (A : (Type U)) (P : A -> Bool) (H : Pi x, P x) : forall x, P x := theorem forall::intro2 (A : (Type U)) (P : A -> Bool) (H : Pi x, P x) : forall x, P x :=
Abst (fun x, EqTIntro (H x)) abst (fun x, eqt::intro (H x))

2
tests/lean/interactive/elab6.lean.expected.out
View file

@ -1,3 +1,3 @@
# Set: pp::colors # Set: pp::colors
Set: pp::unicode Set: pp::unicode
Proved: ForallIntro2 Proved: forall::intro2

2
tests/lean/interactive/t10.lean
View file

@ -3,7 +3,7 @@ simple_tac = Repeat(OrElse(conj_hyp_tac(), conj_tac(), assumption_tac()))
*) *)
theorem T2 (A B : Bool) : A /\ B => B /\ A := theorem T2 (A B : Bool) : A /\ B => B /\ A :=
Discharge (fun H : A /\ B, discharge (fun H : A /\ B,
let H1 : A := _, let H1 : A := _,
H2 : B := _, H2 : B := _,
main : B /\ A := _ main : B /\ A := _

2
tests/lean/interactive/t12.lean
View file

@ -28,7 +28,7 @@ theorem T3 (A B : Bool) : A /\ B -> B /\ A :=
in _. in _.
conj_hyp. exact. done. conj_hyp. exact. done.
conj_hyp. exact. done. conj_hyp. exact. done.
apply Conj. exact. done. apply and::intro. exact. done.
theorem T4 (A B : Bool) : A /\ B -> B /\ A := theorem T4 (A B : Bool) : A /\ B -> B /\ A :=
fun assumption : A /\ B, fun assumption : A /\ B,

2
tests/lean/interactive/t12.lean.expected.out
View file

@ -2,7 +2,7 @@
Set: pp::unicode Set: pp::unicode
Proved: T1 Proved: T1
theorem T1 (A B : Bool) (assumption : A ∧ B) : B ∧ A := theorem T1 (A B : Bool) (assumption : A ∧ B) : B ∧ A :=
let lemma1 : A := Conjunct1 assumption, lemma2 : B := Conjunct2 assumption in Conj lemma2 lemma1 let lemma1 : A := and::eliml assumption, lemma2 : B := and::elimr assumption in and::intro lemma2 lemma1
# Proof state: # Proof state:
A : Bool, B : Bool, assumption : A ∧ B ⊢ A A : Bool, B : Bool, assumption : A ∧ B ⊢ A
## Proof state: ## Proof state:

2
tests/lean/interactive/t13.lean.expected.out
View file

@ -2,5 +2,5 @@
Set: pp::unicode Set: pp::unicode
Proved: T1 Proved: T1
theorem T1 (A B : Bool) (assumption : A ∧ B) : B ∧ A := theorem T1 (A B : Bool) (assumption : A ∧ B) : B ∧ A :=
let lemma1 := Conjunct1 assumption, lemma2 := Conjunct2 assumption in Conj lemma2 lemma1 let lemma1 := and::eliml assumption, lemma2 := and::elimr assumption in and::intro lemma2 lemma1
# #

2
tests/lean/interactive/t3.lean.expected.out
View file

@ -14,5 +14,5 @@ H : b, a : Bool, b : Bool ⊢ b
## Proof state: ## Proof state:
no goals no goals
## Proved: T2 ## Proved: T2
# theorem T2 (a b : Bool) : b ⇒ a ∨ b := Discharge (λ H : b, Disj2 a H) # theorem T2 (a b : Bool) : b ⇒ a ∨ b := discharge (λ H : b, or::intror a H)
# #

2
tests/lean/interactive/t6.lean
View file

@ -2,6 +2,6 @@
theorem T1 (a b : Bool) : a => b => a /\ b. theorem T1 (a b : Bool) : a => b => a /\ b.
(* imp_tac() *). (* imp_tac() *).
(* imp_tac() *). (* imp_tac() *).
apply Conj. apply and::intro.
exact. exact.
done. done.

4
tests/lean/interactive/t8.lean
View file

@ -1,7 +1,7 @@
(* import("tactic.lua") *) (* import("tactic.lua") *)
setoption tactic::proof_state::goal_names true. setoption tactic::proof_state::goal_names true.
theorem T (a : Bool) : a => a /\ a. theorem T (a : Bool) : a => a /\ a.
apply Discharge. apply discharge.
apply Conj. apply and::intro.
exact. exact.
done. done.

6
tests/lean/interactive/t9.lean
View file

@ -1,6 +1,6 @@
(* import("tactic.lua") *) (* import("tactic.lua") *)
theorem T1 (A B : Bool) : A /\ B => B /\ A := theorem T1 (A B : Bool) : A /\ B => B /\ A :=
Discharge (fun H : A /\ B, discharge (fun H : A /\ B,
let main : B /\ A := let main : B /\ A :=
(let H1 : B := _, (let H1 : B := _,
H2 : A := _ H2 : A := _
@ -12,7 +12,7 @@ theorem T1 (A B : Bool) : A /\ B => B /\ A :=
conj_hyp. conj_hyp.
exact. exact.
done. done.
apply Conj. apply and::intro.
exact. exact.
done. done.
@ -21,7 +21,7 @@ simple_tac = Repeat(OrElse(conj_hyp_tac(), conj_tac(), assumption_tac()))
*) *)
theorem T2 (A B : Bool) : A /\ B => B /\ A := theorem T2 (A B : Bool) : A /\ B => B /\ A :=
Discharge (fun H : A /\ B, discharge (fun H : A /\ B,
let H1 : A := _, let H1 : A := _,
H2 : B := _, H2 : B := _,
main : B /\ A := _ main : B /\ A := _

10
tests/lean/let2.lean
View file

@ -1,10 +1,10 @@
-- Annotating lemmas -- Annotating lemmas
theorem simple (p q r : Bool) : (p ⇒ q) ∧ (q ⇒ r) ⇒ p ⇒ r := theorem simple (p q r : Bool) : (p ⇒ q) ∧ (q ⇒ r) ⇒ p ⇒ r :=
Discharge (λ H_pq_qr, Discharge (λ H_p, discharge (λ H_pq_qr, discharge (λ H_p,
let P_pq : (p ⇒ q) := Conjunct1 H_pq_qr, let P_pq : (p ⇒ q) := and::eliml H_pq_qr,
P_qr : (q ⇒ r) := Conjunct2 H_pq_qr, P_qr : (q ⇒ r) := and::elimr H_pq_qr,
P_q : q := MP P_pq H_p P_q : q := mp P_pq H_p
in MP P_qr P_q)) in mp P_qr P_q))
print environment 1 print environment 1

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

@ -2,11 +2,11 @@
Set: pp::unicode Set: pp::unicode
Proved: simple Proved: simple
theorem simple (p q r : Bool) : (p ⇒ q) ∧ (q ⇒ r) ⇒ p ⇒ r := theorem simple (p q r : Bool) : (p ⇒ q) ∧ (q ⇒ r) ⇒ p ⇒ r :=
Discharge discharge
(λ H_pq_qr : (p ⇒ q) ∧ (q ⇒ r), (λ H_pq_qr : (p ⇒ q) ∧ (q ⇒ r),
Discharge discharge
(λ H_p : p, (λ H_p : p,
let P_pq : p ⇒ q := Conjunct1 H_pq_qr, let P_pq : p ⇒ q := and::eliml H_pq_qr,
P_qr : q ⇒ r := Conjunct2 H_pq_qr, P_qr : q ⇒ r := and::elimr H_pq_qr,
P_q : q := MP P_pq H_p P_q : q := P_pq ◂ H_p
in MP P_qr P_q)) in P_qr ◂ P_q))

6
tests/lean/lua11.lean
View file

@ -44,9 +44,9 @@ import Int.
assert(env:find_object("val"):get_value() == Const("x")) assert(env:find_object("val"):get_value() == Const("x"))
assert(env:find_object("val"):get_weight() == 1) assert(env:find_object("val"):get_weight() == 1)
assert(not pcall(function() M:get_weight() end)) assert(not pcall(function() M:get_weight() end))
assert(env:find_object("Congr"):is_opaque()) assert(env:find_object("congr"):is_opaque())
assert(env:find_object("Congr"):is_theorem()) assert(env:find_object("congr"):is_theorem())
assert(env:find_object("Refl"):is_axiom()) assert(env:find_object("refl"):is_axiom())
assert(env:find_object(name("Int", "sub")):is_definition()) assert(env:find_object(name("Int", "sub")):is_definition())
assert(env:find_object("x"):is_var_decl()) assert(env:find_object("x"):is_var_decl())
*) *)

14
tests/lean/norm_bug1.lean
View file

@ -5,8 +5,8 @@ check fun (A A': TypeM)
(a : A) (a : A)
(b : A') (b : A')
(L2 : A' == A), (L2 : A' == A),
let b' : A := cast L2 b, let b' : A := cast L2 b,
L3 : b == b' := CastEq L2 b L3 : b == b' := cast::eq L2 b
in L3 in L3
check fun (A A': TypeM) check fun (A A': TypeM)
@ -19,10 +19,10 @@ check fun (A A': TypeM)
(H1 : (Pi x : A, B x) == (Pi x : A', B' x)) (H1 : (Pi x : A, B x) == (Pi x : A', B' x))
(H2 : f == g) (H2 : f == g)
(H3 : a == b), (H3 : a == b),
let L1 : A == A' := DomInj H1, let L1 : A == A' := dominj H1,
L2 : A' == A := Symm L1, L2 : A' == A := symm L1,
b' : A := cast L2 b, b' : A := cast L2 b,
L3 : b == b' := CastEq L2 b, L3 : b == b' := cast::eq L2 b,
L4 : a == b' := HTrans H3 L3, L4 : a == b' := htrans H3 L3,
L5 : f a == f b' := Congr2 f L4 L5 : f a == f b' := congr2 f L4
in L5 in L5

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

@ -2,7 +2,7 @@
Set: pp::unicode Set: pp::unicode
Imported 'cast' Imported 'cast'
Set: pp::colors Set: pp::colors
λ (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), let b' : A := cast L2 b, L3 : b == b' := CastEq L2 b in L3 : λ (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) λ (A A' : TypeM)
(B : A → TypeM) (B : A → TypeM)
@ -14,12 +14,12 @@
(H1 : (Π x : A, B x) == (Π x : A', B' x)) (H1 : (Π x : A, B x) == (Π x : A', B' x))
(H2 : f == g) (H2 : f == g)
(H3 : a == b), (H3 : a == b),
let L1 : A == A' := DomInj H1, let L1 : A == A' := dominj H1,
L2 : A' == A := Symm L1, L2 : A' == A := symm L1,
b' : A := cast L2 b, b' : A := cast L2 b,
L3 : b == b' := CastEq L2 b, L3 : b == b' := cast::eq L2 b,
L4 : a == b' := HTrans H3 L3, L4 : a == b' := htrans H3 L3,
L5 : f a == f b' := Congr2 f L4 L5 : f a == f b' := congr2 f L4
in L5 : in L5 :
Π (A A' : TypeM) Π (A A' : TypeM)
(B : A → TypeM) (B : A → TypeM)
@ -29,4 +29,4 @@
(a : A) (a : A)
(b : 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) f == g → a == b → f a == f (cast (symm (dominj H1)) b)

2
tests/lean/norm_tac.lean.expected.out
View file

@ -9,7 +9,7 @@
Assumed: read Assumed: read
Assumed: V1 Assumed: V1
Defined: D Defined: D
definition D : ℤ := @read ℤ 10 V1 1 Trivial definition D : ℤ := @read ℤ 10 V1 1 trivial
Assumed: b Assumed: b
Defined: a Defined: a
Proved: T Proved: T

2
tests/lean/ns1.lean
View file

@ -3,7 +3,7 @@ import Int.
namespace foo. namespace foo.
variable a : Nat. variable a : Nat.
definition b := a. definition b := a.
theorem T : a = b := Refl a. theorem T : a = b := refl a.
axiom H : b >= a. axiom H : b >= a.
namespace bla. namespace bla.
variables a c d : Int. variables a c d : Int.

2
tests/lean/refute1.lean
View file

@ -1,3 +1,3 @@
variables a b : Bool variables a b : Bool
axiom H : a /\ b axiom H : a /\ b
theorem T : a := Refute (fun R, Absurd (Conjunct1 H) R) theorem T : a := refute (fun R, absurd (and::eliml H) R)

14
tests/lean/scope.lean
View file

@ -9,18 +9,18 @@ scope
variable hinv : B -> A variable hinv : B -> A
axiom Inv (x : A) : hinv (h x) = x axiom Inv (x : A) : hinv (h x) = x
axiom H1 (x y : A) : f x y = f y x axiom H1 (x y : A) : f x y = f y x
theorem f_eq_g : f = g := Abst (fun x, (Abst (fun y, theorem f_eq_g : f = g := abst (fun x, (abst (fun y,
let L1 : f x y = f y x := H1 x y, let L1 : f x y = f y x := H1 x y,
L2 : f y x = g x y := Refl (g x y) L2 : f y x = g x y := refl (g x y)
in Trans L1 L2))) in trans L1 L2)))
theorem Inj (x y : A) (H : h x = h y) : x = y := theorem Inj (x y : A) (H : h x = h y) : x = y :=
let L1 : hinv (h x) = hinv (h y) := Congr2 hinv H, let L1 : hinv (h x) = hinv (h y) := congr2 hinv H,
L2 : hinv (h x) = x := Inv x, L2 : hinv (h x) = x := Inv x,
L3 : hinv (h y) = y := Inv y, L3 : hinv (h y) = y := Inv y,
L4 : x = hinv (h x) := Symm L2, L4 : x = hinv (h x) := symm L2,
L5 : x = hinv (h y) := Trans L4 L1 L5 : x = hinv (h y) := trans L4 L1
in Trans L5 L3. in trans L5 L3.
end end
print environment 3. print environment 3.

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

@ -13,15 +13,14 @@
Proved: Inj Proved: Inj
definition g (A : Type) (f : A → A → A) (x y : A) : A := f y x 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 (λ x : A,
Abst (λ y : 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))
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 Trans 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 = 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 := y :=
let L1 : hinv (h x) = hinv (h y) := Congr2 hinv H, let L1 : hinv (h x) = hinv (h y) := congr2 hinv H,
L2 : hinv (h x) = x := Inv x, L2 : hinv (h x) = x := Inv x,
L3 : hinv (h y) = y := Inv y, L3 : hinv (h y) = y := Inv y,
L4 : x = hinv (h x) := Symm L2, L4 : x = hinv (h x) := symm L2,
L5 : x = hinv (h y) := Trans L4 L1 L5 : x = hinv (h y) := L4 ⋈ L1
in Trans L5 L3 in L5 ⋈ L3
10 10

2
tests/lean/slow/tactic1.lean
View file

@ -5,7 +5,7 @@ definition big {A : Type} (f : A -> A) : A -> A := (double (double (double (doub
(* (*
-- Tactic for trying to prove goal using Reflexivity, Congruence and available assumptions -- Tactic for trying to prove goal using Reflexivity, Congruence and available assumptions
local congr_tac = Repeat(OrElse(apply_tac("Refl"), apply_tac("Congr"), assumption_tac())) local congr_tac = Repeat(OrElse(apply_tac("refl"), apply_tac("congr"), assumption_tac()))
-- Create an eager tactic that only tries to prove goal after unfolding everything -- Create an eager tactic that only tries to prove goal after unfolding everything
eager_tac = Then(-- unfold homogeneous equality eager_tac = Then(-- unfold homogeneous equality

2
tests/lean/subst.lean
View file

@ -3,7 +3,7 @@ variable a : Int
variable n : Nat variable n : Nat
axiom H1 : a + a + a = 10 axiom H1 : a + a + a = 10
axiom H2 : a = n axiom H2 : a = n
theorem T : a + n + a = 10 := Subst H1 H2 theorem T : a + n + a = 10 := subst H1 H2
setoption pp::coercion true setoption pp::coercion true
setoption pp::notation false setoption pp::notation false
setoption pp::implicit true setoption pp::implicit true

2
tests/lean/subst.lean.expected.out
View file

@ -10,4 +10,4 @@
Set: lean::pp::notation Set: lean::pp::notation
Set: lean::pp::implicit Set: lean::pp::implicit
theorem T : @eq ℤ (Int::add (Int::add a (nat_to_int n)) a) (nat_to_int 10) := theorem T : @eq ℤ (Int::add (Int::add a (nat_to_int n)) a) (nat_to_int 10) :=
@Subst ℤ a (nat_to_int n) (λ x : ℤ, @eq ℤ (Int::add (Int::add a x) a) (nat_to_int 10)) H1 H2 @subst ℤ a (nat_to_int n) (λ x : ℤ, @eq ℤ (Int::add (Int::add a x) a) (nat_to_int 10)) H1 H2

14
tests/lean/subst2.lean
View file

@ -1,15 +1,15 @@
(* import("tactic.lua") *) (* 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). 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 ForallIntro. apply forall::intro.
beta. beta.
apply ForallIntro. apply forall::intro.
beta. beta.
apply ForallIntro. apply forall::intro.
beta. beta.
apply Discharge. apply discharge.
apply Discharge. apply discharge.
apply Discharge. apply discharge.
apply (Subst (Subst H H::1) H::2) apply (subst (subst H H::1) H::2)
done. done.
print environment 1. print environment 1.

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

@ -3,13 +3,13 @@
Proved: T Proved: T
theorem T (A : Type) (p : A → Bool) (f : A → A → A) : ∀ x y z : A, 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) := p (f x x) ⇒ x = y ⇒ x = z ⇒ p (f y z) :=
ForallIntro forall::intro
(λ x : A, (λ x : A,
ForallIntro forall::intro
(λ x::1 : A, (λ x::1 : A,
ForallIntro forall::intro
(λ x::2 : A, (λ x::2 : A,
Discharge discharge
(λ H : p (f x x), (λ H : p (f x x),
Discharge discharge
(λ H::1 : x = x::1, Discharge (λ H::2 : x = x::2, Subst (Subst H H::1) H::2)))))) (λ H::1 : x = x::1, discharge (λ H::2 : x = x::2, subst (subst H H::1) H::2))))))

6
tests/lean/subst3.lean
View file

@ -1,7 +1,7 @@
(* import("macros.lua") *) 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) := 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), take x y z, assume (H1 : p (f x x)) (H2 : x = y) (H3 : x = z),
Subst' H1 H2 H3. subst (subst H1 H2) H3
print environment 1. print environment 1.

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

@ -1,14 +1,15 @@
Set: pp::colors Set: pp::colors
Set: pp::unicode Set: pp::unicode
Imported 'macros'
Proved: T Proved: T
theorem T (A : Type) (p : A → Bool) (f : A → A → A) : ∀ x y z : A, 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) := p (f x x) ⇒ x = y ⇒ x = z ⇒ p (f y z) :=
ForallIntro forall::intro
(λ x : A, (λ x : A,
ForallIntro forall::intro
(λ y : A, (λ y : A,
ForallIntro forall::intro
(λ z : A, (λ z : A,
Discharge discharge
(λ H1 : p (f x x), (λ H1 : p (f x x),
Discharge (λ H2 : x = y, Discharge (λ H3 : x = z, Subst (Subst H1 H2) H3)))))) discharge (λ H2 : x = y, discharge (λ H3 : x = z, subst (subst H1 H2) H3))))))

2
tests/lean/tactic1.lean.expected.out
View file

@ -3,4 +3,4 @@
Assumed: p Assumed: p
Assumed: q Assumed: q
Assumed: r Assumed: r
theorem T1 : p ⇒ q ⇒ p ∧ q := Discharge (λ H : p, Discharge (λ H::1 : q, Conj H H::1)) theorem T1 : p ⇒ q ⇒ p ∧ q := discharge (λ H : p, discharge (λ H::1 : q, and::intro H H::1))

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