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

chore(*): cleanup lean builtin symbols, replace :: with _

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-01-09 08:33:52 -08:00
parent 25086947fa
commit 57c0006916
125 changed files with 626 additions and 631 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
doc/lean/calc.md
View file

@ -35,7 +35,7 @@ Here is an example
:= calc a = b : Ax1
... = c + 1 : Ax2
... = d + 1 : { Ax3 }
... = 1 + d : Nat::add::comm d 1
... = 1 + d : Nat::add_comm d 1
... = e : symm Ax4.
```
@ -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
gaps in our calculational proofs. In the previous examples, we can use `_` as arguments for the
`Nat::add::comm` theorem. The Lean elaboration engine will infer `d` and `1` for us.
`Nat::add_comm` theorem. The Lean elaboration engine will infer `d` and `1` for us.
Here is the same example using placeholders.
```lean
@ -53,7 +53,7 @@ Here is the same example using placeholders.
:= calc a = b : Ax1
... = c + 1 : Ax2
... = d + 1 : { Ax3 }
... = 1 + d : Nat::add::comm _ _
... = 1 + d : Nat::add_comm _ _
... = e : symm Ax4.
```
@ -64,7 +64,7 @@ Here is an example.
theorem T2 (a b c : Nat) (H1 : a = b) (H2 : b = c + 1) : a ≠ 0
:= calc a = b : H1
... = c + 1 : H2
... ≠ 0 : Nat::succ::nz _.
... ≠ 0 : Nat::succ_nz _.
```
The Lean `let` construct can also be used to build calculational-like proofs.

10
doc/lean/expr.md
View file

@ -88,16 +88,16 @@ infix 50 = : eq
```
The curly braces indicate that the first argument of `eq` is implicit. The symbol `=` is just a syntax sugar for `eq`.
In the following example, we use the `set::option` command to force Lean to display implicit arguments and
In the following example, we use the `set_option` command to force Lean to display implicit arguments and
disable notation when pretty printing expressions.
```lean
set::option pp::implicit true
set::option pp::notation false
set_option pp::implicit true
set_option pp::notation false
check 1 = 2
-- restore default configuration
set::option pp::implicit false
set::option pp::notation true
set_option pp::implicit false
set_option pp::notation true
check 1 = 2
```

4
doc/lean/tutorial.md
View file

@ -76,7 +76,7 @@ In the following example we prove that `double x = 2 * x`
```lean
theorem double_x_eq_2x (x : Nat) : double x = 2 * x :=
calc double x = x + x : refl (double x)
... = 1*x + 1*x : { symm (mul::onel x) }
... = 1*x + 1*x : { symm (mul_onel x) }
... = (1 + 1)*x : symm (distributel 1 1 x)
... = 2 * x : { refl (1 + 1) }
```
@ -84,7 +84,7 @@ In the following example we prove that `double x = 2 * x`
In the example above, we provided the proof manually using a calculational proof style.
The terms after `:` are proof terms. They justify the equalities in the left-hand-side.
The proof term `refl (double x)` produces a proof for `t = s` where `t` and `s` have the same
normal form of `(double x)`. The proof term `{ symm (mul::onel x) }` is a justification for
normal form of `(double x)`. The proof term `{ symm (mul_onel x) }` is a justification for
the equality `x = 1*x`. The curly braces instruct Lean to replace `x` with `1*x`.
Similarly `{ symm (distributel 1 1 x) }` is a proof for `1*x + 1*x = (1 + 1)*x`.
The exact semantics of these expressions is not important at this point.

2
emacs/lean.el
View file

@ -23,7 +23,7 @@
(define-generic-mode
'lean-mode ;; name of the mode to create
'("--") ;; comments start with
'("import" "definition" "variable" "variables" "print" "axiom" "theorem" "universe" "alias" "help" "set::option" "set::opaque" "environment" "options" "infix" "infixl" "infixr" "notation" "eval" "check" "exit" "coercion" "end" "using" "namespace" "builtin" "scope" "pop::scope") ;; some keywords
'("import" "definition" "variable" "variables" "print" "axiom" "theorem" "universe" "alias" "help" "set_option" "set_opaque" "environment" "options" "infix" "infixl" "infixr" "notation" "eval" "check" "exit" "coercion" "end" "using" "namespace" "builtin" "scope" "pop_scope") ;; some keywords
'(("\\<\\(Bool\\|Int\\|Nat\\|Real\\|Type\\|TypeU\\|ℕ\\|ℤ\\)\\>" . 'font-lock-type-face)
("\\<\\(calc\\|have\\|in\\|let\\)\\>" . font-lock-keyword-face)
("\"[^\"]*\"" . 'font-lock-string-face)

12
examples/lean/even.lean
View file

@ -14,7 +14,7 @@ definition odd (a : Nat) := ∃ b, a = 2*b + 1
-- It is syntax sugar for existential elimination.
-- It expands to
--
-- exists::elim [expr]_1 (fun [binding], [expr]_2)
-- exists_elim [expr]_1 (fun [binding], [expr]_2)
--
-- It is defined in the file macros.lua.
--
@ -32,12 +32,12 @@ definition odd (a : Nat) := ∃ b, a = 2*b + 1
theorem EvenPlusEven {a b : Nat} (H1 : even a) (H2 : even b) : even (a + b)
:= obtain (w1 : Nat) (Hw1 : a = 2*w1), from H1,
obtain (w2 : Nat) (Hw2 : b = 2*w2), from H2,
exists::intro (w1 + w2)
exists_intro (w1 + w2)
(calc a + b = 2*w1 + b : { Hw1 }
... = 2*w1 + 2*w2 : { Hw2 }
... = 2*(w1 + w2) : symm (distributer 2 w1 w2))
-- In the following example, we omit the arguments for add::assoc, refl and distribute.
-- In the following example, we omit the arguments for add_assoc, refl and distribute.
-- Lean can infer them automatically.
--
-- refl is the reflexivity proof. (refl a) is a proof that two
@ -52,9 +52,9 @@ theorem EvenPlusEven {a b : Nat} (H1 : even a) (H2 : even b) : even (a + b)
-- any theorems such as + associativity.
theorem OddPlusOne {a : Nat} (H : odd a) : even (a + 1)
:= obtain (w : Nat) (Hw : a = 2*w + 1), from H,
exists::intro (w + 1)
exists_intro (w + 1)
(calc a + 1 = 2*w + 1 + 1 : { Hw }
... = 2*w + (1 + 1) : symm (add::assoc _ _ _)
... = 2*w + (1 + 1) : symm (add_assoc _ _ _)
... = 2*w + 2*1 : refl _
... = 2*(w + 1) : symm (distributer _ _ _))
@ -64,7 +64,7 @@ print environment 2
-- By default, Lean does not display implicit arguments.
-- The following command will force it to display them.
set::option pp::implicit true
set_option pp::implicit true
print environment 2

10
examples/lean/ex1.lean
View file

@ -18,9 +18,9 @@ axiom H2 : b = e
-- Proof that (h a b) = (h c e)
theorem T1 : (h a b) = (h c e) :=
or::elim H1
(λ C1, congrh ((and::eliml C1) ⋈ (and::elimr C1)) H2)
(λ C2, congrh ((and::elimr C2) ⋈ (and::eliml C2)) H2)
or_elim H1
(λ C1, congrh ((and_eliml C1) ⋈ (and_elimr C1)) H2)
(λ C2, congrh ((and_elimr C2) ⋈ (and_eliml C2)) H2)
-- We can use theorem T1 to prove other theorems
theorem T2 : (h a (h a b)) = (h a (h c e)) :=
@ -30,6 +30,6 @@ theorem T2 : (h a (h a b)) = (h a (h c e)) :=
print environment 2
-- print implicit arguments
set::option lean::pp::implicit true
set::option pp::width 150
set_option lean::pp::implicit true
set_option pp::width 150
print environment 2

6
examples/lean/ex2.lean
View file

@ -2,11 +2,11 @@ import macros.
theorem simple (p q r : Bool) : (p → q) ∧ (q → r) → p → r
:= λ H_pq_qr H_p,
let P_pq := and::eliml H_pq_qr,
P_qr := and::elimr H_pq_qr
let P_pq := and_eliml H_pq_qr,
P_qr := and_elimr H_pq_qr
in P_qr (P_pq H_p)
set::option pp::implicit true.
set_option pp::implicit true.
print environment 1.
theorem simple2 (a b c : Bool) : (a → b → c) → (a → b) → a → c

18
examples/lean/ex3.lean
View file

@ -1,13 +1,13 @@
import macros.
theorem and_comm (a b : Bool) : (a ∧ b) → (b ∧ a)
:= λ H_ab, and::intro (and::elimr H_ab) (and::eliml H_ab).
theorem my_and_comm (a b : Bool) : (a ∧ b) → (b ∧ a)
:= λ H_ab, and_intro (and_elimr H_ab) (and_eliml H_ab).
theorem or_comm (a b : Bool) : (a ∨ b) → (b ∨ a)
theorem my_or_comm (a b : Bool) : (a ∨ b) → (b ∨ a)
:= λ H_ab,
or::elim H_ab
(λ H_a, or::intror b H_a)
(λ H_b, or::introl H_b a).
or_elim H_ab
(λ H_a, or_intror b H_a)
(λ H_b, or_introl H_b a).
-- (em a) is the excluded middle a ∨ ¬a
-- (mt H H_na) is Modus Tollens with
@ -16,13 +16,13 @@ theorem or_comm (a b : Bool) : (a ∨ b) → (b ∨ a)
-- produces
-- ¬(a → b)
--
-- not::imp::eliml applied to
-- not_imp_eliml applied to
-- (MT H H_na) : ¬(a → b)
-- produces
-- a
theorem pierce (a b : Bool) : ((a → b) → a) → a
:= λ H, or::elim (em a)
:= λ H, or_elim (em a)
(λ H_a, H_a)
(λ H_na, not::imp::eliml (mt H H_na)).
(λ H_na, not_imp_eliml (mt H H_na)).
print environment 3.

2
examples/lean/ex5.lean
View file

@ -12,7 +12,7 @@ scope
let L1 : R w x := Symm x w H
in Trans x w x H L1
pop::scope
pop_scope
scope
-- Same example again.

8
examples/lean/set.lean
View file

@ -8,17 +8,17 @@ infix 60 ∈ : element
definition subset {A : Type} (s1 : Set A) (s2 : Set A) := ∀ x, x ∈ s1 → x ∈ s2
infix 50 ⊆ : subset
theorem subset::trans {A : Type} {s1 s2 s3 : Set A} (H1 : s1 ⊆ s2) (H2 : s2 ⊆ s3) : s1 ⊆ s3
theorem subset_trans {A : Type} {s1 s2 s3 : Set A} (H1 : s1 ⊆ s2) (H2 : s2 ⊆ s3) : s1 ⊆ s3
:= λ (x : A) (Hin : x ∈ s1),
have x ∈ s3 :
let L1 : x ∈ s2 := H1 x Hin
in H2 x L1
theorem subset::ext {A : Type} {s1 s2 : Set A} (H : ∀ x, x ∈ s1 = x ∈ s2) : s1 = s2
theorem subset_ext {A : Type} {s1 s2 : Set A} (H : ∀ x, x ∈ s1 = x ∈ s2) : s1 = s2
:= funext H
theorem subset::antisym {A : Type} {s1 s2 : Set A} (H1 : s1 ⊆ s2) (H2 : s2 ⊆ s1) : s1 = s2
:= subset::ext (have (∀ x, x ∈ s1 = x ∈ s2) :
theorem subset_antisym {A : Type} {s1 s2 : Set A} (H1 : s1 ⊆ s2) (H2 : s2 ⊆ s1) : s1 = s2
:= subset_ext (have (∀ x, x ∈ s1 = x ∈ s2) :
λ x, have x ∈ s1 = x ∈ s2 :
boolext (have x ∈ s1 → x ∈ s2 : H1 x)
(have x ∈ s2 → x ∈ s1 : H2 x))

2
examples/lean/tactic_in_lua.lean
View file

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

20
src/builtin/Int.lean
View file

@ -46,14 +46,14 @@ infix 50 | : divides
definition abs (a : Int) : Int := if (0 ≤ a) a (- a)
notation 55 | _ | : abs
set::opaque sub true
set::opaque neg true
set::opaque mod true
set::opaque divides true
set::opaque abs true
set::opaque ge true
set::opaque lt true
set::opaque gt true
set_opaque sub true
set_opaque neg true
set_opaque mod true
set_opaque divides true
set_opaque abs true
set_opaque ge true
set_opaque lt true
set_opaque gt true
end
namespace Nat
@ -63,6 +63,6 @@ infixl 65 - : sub
definition neg (a : Nat) : Int := - (nat_to_int a)
notation 75 - _ : neg
set::opaque sub true
set::opaque neg true
set_opaque sub true
set_opaque neg true
end

240
src/builtin/Nat.lean
View file

@ -30,219 +30,219 @@ infix 50 > : gt
definition id (a : Nat) := a
notation 55 | _ | : id
axiom succ::nz (a : Nat) : a + 1 ≠ 0
axiom succ::inj {a b : Nat} (H : a + 1 = b + 1) : a = b
axiom add::zeror (a : Nat) : a + 0 = a
axiom add::succr (a b : Nat) : a + (b + 1) = (a + b) + 1
axiom mul::zeror (a : Nat) : a * 0 = 0
axiom mul::succr (a b : Nat) : a * (b + 1) = a * b + a
axiom le::def (a b : Nat) : a ≤ b = ∃ c, a + c = b
axiom succ_nz (a : Nat) : a + 1 ≠ 0
axiom succ_inj {a b : Nat} (H : a + 1 = b + 1) : a = b
axiom add_zeror (a : Nat) : a + 0 = a
axiom add_succr (a b : Nat) : a + (b + 1) = (a + b) + 1
axiom mul_zeror (a : Nat) : a * 0 = 0
axiom mul_succr (a b : Nat) : a * (b + 1) = a * b + a
axiom le_def (a b : Nat) : a ≤ b = ∃ c, a + c = b
axiom induction {P : Nat → Bool} (a : Nat) (H1 : P 0) (H2 : ∀ (n : Nat) (iH : P n), P (n + 1)) : P a
theorem pred::nz {a : Nat} : a ≠ 0 → ∃ b, b + 1 = a
theorem pred_nz {a : Nat} : a ≠ 0 → ∃ b, b + 1 = a
:= induction a
(λ H : 0 ≠ 0, false::elim (∃ b, b + 1 = 0) H)
(λ H : 0 ≠ 0, false_elim (∃ b, b + 1 = 0) H)
(λ (n : Nat) (iH : n ≠ 0 → ∃ b, b + 1 = n) (H : n + 1 ≠ 0),
or::elim (em (n = 0))
(λ Heq0 : n = 0, exists::intro 0 (calc 0 + 1 = n + 1 : { symm Heq0 }))
or_elim (em (n = 0))
(λ Heq0 : n = 0, exists_intro 0 (calc 0 + 1 = n + 1 : { symm Heq0 }))
(λ Hne0 : n ≠ 0,
obtain (w : Nat) (Hw : w + 1 = n), from (iH Hne0),
exists::intro (w + 1) (calc w + 1 + 1 = n + 1 : { Hw })))
exists_intro (w + 1) (calc w + 1 + 1 = n + 1 : { Hw })))
theorem discriminate {B : Bool} {a : Nat} (H1: a = 0 → B) (H2 : ∀ n, a = n + 1 → B) : B
:= or::elim (em (a = 0))
:= or_elim (em (a = 0))
(λ Heq0 : a = 0, H1 Heq0)
(λ Hne0 : a ≠ 0, obtain (w : Nat) (Hw : w + 1 = a), from (pred::nz Hne0),
(λ Hne0 : a ≠ 0, obtain (w : Nat) (Hw : w + 1 = a), from (pred_nz Hne0),
H2 w (symm Hw))
theorem add::zerol (a : Nat) : 0 + a = a
theorem add_zerol (a : Nat) : 0 + a = a
:= induction a
(have 0 + 0 = 0 : trivial)
(λ (n : Nat) (iH : 0 + n = n),
calc 0 + (n + 1) = (0 + n) + 1 : add::succr 0 n
calc 0 + (n + 1) = (0 + n) + 1 : add_succr 0 n
... = n + 1 : { iH })
theorem add::succl (a b : Nat) : (a + 1) + b = (a + b) + 1
theorem add_succl (a b : Nat) : (a + 1) + b = (a + b) + 1
:= induction b
(calc (a + 1) + 0 = a + 1 : add::zeror (a + 1)
... = (a + 0) + 1 : { symm (add::zeror a) })
(calc (a + 1) + 0 = a + 1 : add_zeror (a + 1)
... = (a + 0) + 1 : { symm (add_zeror a) })
(λ (n : Nat) (iH : (a + 1) + n = (a + n) + 1),
calc (a + 1) + (n + 1) = ((a + 1) + n) + 1 : add::succr (a + 1) n
calc (a + 1) + (n + 1) = ((a + 1) + n) + 1 : add_succr (a + 1) n
... = ((a + n) + 1) + 1 : { iH }
... = (a + (n + 1)) + 1 : { have (a + n) + 1 = a + (n + 1) : symm (add::succr a n) })
... = (a + (n + 1)) + 1 : { have (a + n) + 1 = a + (n + 1) : symm (add_succr a n) })
theorem add::comm (a b : Nat) : a + b = b + a
theorem add_comm (a b : Nat) : a + b = b + a
:= induction b
(calc a + 0 = a : add::zeror a
... = 0 + a : symm (add::zerol a))
(calc a + 0 = a : add_zeror a
... = 0 + a : symm (add_zerol a))
(λ (n : Nat) (iH : a + n = n + a),
calc a + (n + 1) = (a + n) + 1 : add::succr a n
calc a + (n + 1) = (a + n) + 1 : add_succr a n
... = (n + a) + 1 : { iH }
... = (n + 1) + a : symm (add::succl n a))
... = (n + 1) + a : symm (add_succl n a))
theorem add::assoc (a b c : Nat) : a + (b + c) = (a + b) + c
theorem add_assoc (a b c : Nat) : a + (b + c) = (a + b) + c
:= induction a
(calc 0 + (b + c) = b + c : add::zerol (b + c)
... = (0 + b) + c : { symm (add::zerol b) })
(calc 0 + (b + c) = b + c : add_zerol (b + c)
... = (0 + b) + c : { symm (add_zerol b) })
(λ (n : Nat) (iH : n + (b + c) = (n + b) + c),
calc (n + 1) + (b + c) = (n + (b + c)) + 1 : add::succl n (b + c)
calc (n + 1) + (b + c) = (n + (b + c)) + 1 : add_succl n (b + c)
... = ((n + b) + c) + 1 : { iH }
... = ((n + b) + 1) + c : symm (add::succl (n + b) c)
... = ((n + 1) + b) + c : { have (n + b) + 1 = (n + 1) + b : symm (add::succl n b) })
... = ((n + b) + 1) + c : symm (add_succl (n + b) c)
... = ((n + 1) + b) + c : { have (n + b) + 1 = (n + 1) + b : symm (add_succl n b) })
theorem mul::zerol (a : Nat) : 0 * a = 0
theorem mul_zerol (a : Nat) : 0 * a = 0
:= induction a
(have 0 * 0 = 0 : trivial)
(λ (n : Nat) (iH : 0 * n = 0),
calc 0 * (n + 1) = (0 * n) + 0 : mul::succr 0 n
calc 0 * (n + 1) = (0 * n) + 0 : mul_succr 0 n
... = 0 + 0 : { iH }
... = 0 : trivial)
theorem mul::succl (a b : Nat) : (a + 1) * b = a * b + b
theorem mul_succl (a b : Nat) : (a + 1) * b = a * b + b
:= induction b
(calc (a + 1) * 0 = 0 : mul::zeror (a + 1)
... = a * 0 : symm (mul::zeror a)
... = a * 0 + 0 : symm (add::zeror (a * 0)))
(calc (a + 1) * 0 = 0 : mul_zeror (a + 1)
... = a * 0 : symm (mul_zeror a)
... = a * 0 + 0 : symm (add_zeror (a * 0)))
(λ (n : Nat) (iH : (a + 1) * n = a * n + n),
calc (a + 1) * (n + 1) = (a + 1) * n + (a + 1) : mul::succr (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 : add::assoc (a * n + n) a 1
... = a * n + (n + a) + 1 : { have a * n + n + a = a * n + (n + a) : symm (add::assoc (a * n) n a) }
... = a * n + (a + n) + 1 : { add::comm n a }
... = a * n + a + n + 1 : { add::assoc (a * n) a n }
... = a * (n + 1) + n + 1 : { symm (mul::succr a n) }
... = a * (n + 1) + (n + 1) : symm (add::assoc (a * (n + 1)) n 1))
... = a * n + n + a + 1 : add_assoc (a * n + n) a 1
... = a * n + (n + a) + 1 : { have a * n + n + a = a * n + (n + a) : symm (add_assoc (a * n) n a) }
... = a * n + (a + n) + 1 : { add_comm n a }
... = a * n + a + n + 1 : { add_assoc (a * n) a n }
... = a * (n + 1) + n + 1 : { symm (mul_succr a n) }
... = a * (n + 1) + (n + 1) : symm (add_assoc (a * (n + 1)) n 1))
theorem mul::onel (a : Nat) : 1 * a = a
theorem mul_onel (a : Nat) : 1 * a = a
:= induction a
(have 1 * 0 = 0 : trivial)
(λ (n : Nat) (iH : 1 * n = n),
calc 1 * (n + 1) = 1 * n + 1 : mul::succr 1 n
calc 1 * (n + 1) = 1 * n + 1 : mul_succr 1 n
... = n + 1 : { iH })
theorem mul::oner (a : Nat) : a * 1 = a
theorem mul_oner (a : Nat) : a * 1 = a
:= induction a
(have 0 * 1 = 0 : trivial)
(λ (n : Nat) (iH : n * 1 = n),
calc (n + 1) * 1 = n * 1 + 1 : mul::succl n 1
calc (n + 1) * 1 = n * 1 + 1 : mul_succl n 1
... = n + 1 : { iH })
theorem mul::comm (a b : Nat) : a * b = b * a
theorem mul_comm (a b : Nat) : a * b = b * a
:= induction b
(calc a * 0 = 0 : mul::zeror a
... = 0 * a : symm (mul::zerol a))
(calc a * 0 = 0 : mul_zeror a
... = 0 * a : symm (mul_zerol a))
(λ (n : Nat) (iH : a * n = n * a),
calc a * (n + 1) = a * n + a : mul::succr a n
calc a * (n + 1) = a * n + a : mul_succr a n
... = n * a + a : { iH }
... = (n + 1) * a : symm (mul::succl n a))
... = (n + 1) * a : symm (mul_succl n a))
theorem distributer (a b c : Nat) : a * (b + c) = a * b + a * c
:= induction a
(calc 0 * (b + c) = 0 : mul::zerol (b + c)
(calc 0 * (b + c) = 0 : mul_zerol (b + c)
... = 0 + 0 : trivial
... = 0 * b + 0 : { symm (mul::zerol b) }
... = 0 * b + 0 * c : { symm (mul::zerol c) })
... = 0 * b + 0 : { symm (mul_zerol b) }
... = 0 * b + 0 * c : { symm (mul_zerol c) })
(λ (n : Nat) (iH : n * (b + c) = n * b + n * c),
calc (n + 1) * (b + c) = n * (b + c) + (b + c) : mul::succl 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 : add::assoc (n * b + n * c) b c
... = n * b + (n * c + b) + c : { symm (add::assoc (n * b) (n * c) b) }
... = n * b + (b + n * c) + c : { add::comm (n * c) b }
... = n * b + b + n * c + c : { add::assoc (n * b) b (n * c) }
... = (n + 1) * b + n * c + c : { symm (mul::succl n b) }
... = (n + 1) * b + (n * c + c) : symm (add::assoc ((n + 1) * b) (n * c) c)
... = (n + 1) * b + (n + 1) * c : { symm (mul::succl n c) })
... = n * b + n * c + b + c : add_assoc (n * b + n * c) b c
... = n * b + (n * c + b) + c : { symm (add_assoc (n * b) (n * c) b) }
... = n * b + (b + n * c) + c : { add_comm (n * c) b }
... = n * b + b + n * c + c : { add_assoc (n * b) b (n * c) }
... = (n + 1) * b + n * c + c : { symm (mul_succl n b) }
... = (n + 1) * b + (n * c + c) : symm (add_assoc ((n + 1) * b) (n * c) c)
... = (n + 1) * b + (n + 1) * c : { symm (mul_succl n c) })
theorem distributel (a b c : Nat) : (a + b) * c = a * c + b * c
:= calc (a + b) * c = c * (a + b) : mul::comm (a + b) c
:= calc (a + b) * c = c * (a + b) : mul_comm (a + b) c
... = c * a + c * b : distributer c a b
... = a * c + c * b : { mul::comm c a }
... = a * c + b * c : { mul::comm c b }
... = a * c + c * b : { mul_comm c a }
... = a * c + b * c : { mul_comm c b }
theorem mul::assoc (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
(calc 0 * (b * c) = 0 : mul::zerol (b * c)
... = 0 * c : symm (mul::zerol c)
... = (0 * b) * c : { symm (mul::zerol b) })
(calc 0 * (b * c) = 0 : mul_zerol (b * c)
... = 0 * c : symm (mul_zerol c)
... = (0 * b) * c : { symm (mul_zerol b) })
(λ (n : Nat) (iH : n * (b * c) = n * b * c),
calc (n + 1) * (b * c) = n * (b * c) + (b * c) : mul::succl 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 + b) * c : symm (distributel (n * b) b c)
... = (n + 1) * b * c : { symm (mul::succl n b) })
... = (n + 1) * b * c : { symm (mul_succl n b) })
theorem add::inj {a b c : Nat} : a + b = a + c → b = c
theorem add_inj {a b c : Nat} : a + b = a + c → b = c
:= induction a
(λ H : 0 + b = 0 + c,
calc b = 0 + b : symm (add::zerol b)
calc b = 0 + b : symm (add_zerol b)
... = 0 + c : H
... = c : add::zerol c)
... = c : add_zerol c)
(λ (n : Nat) (iH : n + b = n + c → b = c) (H : n + 1 + b = n + 1 + c),
let L1 : n + b + 1 = n + c + 1
:= (calc n + b + 1 = n + (b + 1) : symm (add::assoc n b 1)
... = n + (1 + b) : { add::comm b 1 }
... = n + 1 + b : add::assoc n 1 b
:= (calc n + b + 1 = n + (b + 1) : symm (add_assoc n b 1)
... = n + (1 + b) : { add_comm b 1 }
... = n + 1 + b : add_assoc n 1 b
... = n + 1 + c : H
... = n + (1 + c) : symm (add::assoc n 1 c)
... = n + (c + 1) : { add::comm 1 c }
... = n + c + 1 : add::assoc n c 1),
L2 : n + b = n + c := succ::inj L1
... = n + (1 + c) : symm (add_assoc n 1 c)
... = n + (c + 1) : { add_comm 1 c }
... = n + c + 1 : add_assoc n c 1),
L2 : n + b = n + c := succ_inj L1
in iH L2)
theorem add::eqz {a b : Nat} (H : a + b = 0) : a = 0
theorem add_eqz {a b : Nat} (H : a + b = 0) : a = 0
:= discriminate
(λ H1 : a = 0, H1)
(λ (n : Nat) (H1 : a = n + 1),
absurd::elim (a = 0)
absurd_elim (a = 0)
H (calc a + b = n + 1 + b : { H1 }
... = n + (1 + b) : symm (add::assoc n 1 b)
... = n + (b + 1) : { add::comm 1 b }
... = n + b + 1 : add::assoc n b 1
... ≠ 0 : succ::nz (n + b)))
... = n + (1 + b) : symm (add_assoc n 1 b)
... = n + (b + 1) : { add_comm 1 b }
... = n + b + 1 : add_assoc n b 1
... ≠ 0 : succ_nz (n + b)))
theorem le::intro {a b c : Nat} (H : a + c = b) : a ≤ b
:= (symm (le::def a b)) ◂ (have (∃ x, a + x = b) : exists::intro c H)
theorem le_intro {a b c : Nat} (H : a + c = b) : a ≤ b
:= (symm (le_def a b)) ◂ (have (∃ x, a + x = b) : exists_intro c H)
theorem le::elim {a b : Nat} (H : a ≤ b) : ∃ x, a + x = b
:= (le::def a b) ◂ H
theorem le_elim {a b : Nat} (H : a ≤ b) : ∃ x, a + x = b
:= (le_def a b) ◂ H
theorem le::refl (a : Nat) : a ≤ a := le::intro (add::zeror a)
theorem le_refl (a : Nat) : a ≤ a := le_intro (add_zeror a)
theorem le::zero (a : Nat) : 0 ≤ a := le::intro (add::zerol a)
theorem le_zero (a : Nat) : 0 ≤ a := le_intro (add_zerol a)
theorem le::trans {a b c : Nat} (H1 : a ≤ b) (H2 : b ≤ c) : a ≤ c
:= obtain (w1 : Nat) (Hw1 : a + w1 = b), from (le::elim H1),
obtain (w2 : Nat) (Hw2 : b + w2 = c), from (le::elim H2),
le::intro (calc a + (w1 + w2) = a + w1 + w2 : add::assoc a w1 w2
theorem le_trans {a b c : Nat} (H1 : a ≤ b) (H2 : b ≤ c) : a ≤ c
:= obtain (w1 : Nat) (Hw1 : a + w1 = b), from (le_elim H1),
obtain (w2 : Nat) (Hw2 : b + w2 = c), from (le_elim H2),
le_intro (calc a + (w1 + w2) = a + w1 + w2 : add_assoc a w1 w2
... = b + w2 : { Hw1 }
... = c : Hw2)
theorem le::add {a b : Nat} (H : a ≤ b) (c : Nat) : a + c ≤ b + c
:= obtain (w : Nat) (Hw : a + w = b), from (le::elim H),
le::intro (calc a + c + w = a + (c + w) : symm (add::assoc a c w)
... = a + (w + c) : { add::comm c w }
... = a + w + c : add::assoc a w c
theorem le_add {a b : Nat} (H : a ≤ b) (c : Nat) : a + c ≤ b + c
:= obtain (w : Nat) (Hw : a + w = b), from (le_elim H),
le_intro (calc a + c + w = a + (c + w) : symm (add_assoc a c w)
... = a + (w + c) : { add_comm c w }
... = a + w + c : add_assoc a w c
... = b + c : { Hw })
theorem le::antisym {a b : Nat} (H1 : a ≤ b) (H2 : b ≤ a) : a = b
:= obtain (w1 : Nat) (Hw1 : a + w1 = b), from (le::elim H1),
obtain (w2 : Nat) (Hw2 : b + w2 = a), from (le::elim H2),
theorem le_antisym {a b : Nat} (H1 : a ≤ b) (H2 : b ≤ a) : a = b
:= obtain (w1 : Nat) (Hw1 : a + w1 = b), from (le_elim H1),
obtain (w2 : Nat) (Hw2 : b + w2 = a), from (le_elim H2),
let L1 : w1 + w2 = 0
:= add::inj (calc a + (w1 + w2) = a + w1 + w2 : { add::assoc a w1 w2 }
:= add_inj (calc a + (w1 + w2) = a + w1 + w2 : { add_assoc a w1 w2 }
... = b + w2 : { Hw1 }
... = a : Hw2
... = a + 0 : symm (add::zeror a)),
L2 : w1 = 0 := add::eqz L1
in calc a = a + 0 : symm (add::zeror a)
... = a + 0 : symm (add_zeror a)),
L2 : w1 = 0 := add_eqz L1
in calc a = a + 0 : symm (add_zeror a)
... = a + w1 : { symm L2 }
... = b : Hw1
set::opaque add true
set::opaque mul true
set::opaque le true
set::opaque id true
set::opaque ge true
set::opaque lt true
set::opaque gt true
set::opaque id true
set_opaque add true
set_opaque mul true
set_opaque le true
set_opaque id true
set_opaque ge true
set_opaque lt true
set_opaque gt true
set_opaque id true
end

21
src/builtin/cast.lean
View file

@ -8,7 +8,7 @@ universe U >= M + 1
definition TypeM := (Type M)
-- Type equality axiom, if two values are equal, then their types are equal
theorem type::eq {A B : TypeM} {a : A} {b : B} (H : a == b) : A == B
theorem type_eq {A B : TypeM} {a : A} {b : B} (H : a == b) : A == B
:= hsubst (λ (T : TypeU) (x : T), A == T) (refl A) H
-- Heterogenous symmetry
@ -24,10 +24,10 @@ theorem htrans {A B C : TypeU} {a : A} {b : B} {c : C} (H1 : a == b) (H2 : b ==
variable cast {A B : TypeU} : A == B → A → B
-- The CastEq axiom states that for any cast of x is equal to x.
axiom cast::eq {A B : TypeU} (H : A == B) (x : A) : x == cast H x
axiom cast_eq {A B : TypeU} (H : A == B) (x : A) : x == cast H x
-- The CastApp axiom "propagates" the cast over application
axiom cast::app {A A' : TypeU} {B : A → TypeU} {B' : A' → TypeU}
axiom cast_app {A A' : TypeU} {B : A → TypeU} {B' : A' → TypeU}
(H1 : (∀ x : A, B x) == (∀ x : A', B' x)) (H2 : A == A')
(f : ∀ x : A, B x) (x : A) :
cast H1 f (cast H2 x) == f x
@ -39,19 +39,19 @@ theorem hcongr
(H1 : f == g)
(H2 : a == b)
: f a == g b
:= let L1 : A == A' := type::eq H2,
:= let L1 : A == A' := type_eq H2,
L2 : A' == A := symm L1,
b' : A := cast L2 b,
L3 : b == b' := cast::eq L2 b,
L3 : b == b' := cast_eq L2 b,
L4 : a == b' := htrans H2 L3,
L5 : f a == f b' := congr2 f L4,
S1 : (∀ x : A', B' x) == (∀ x : A, B x) := symm (type::eq H1),
S1 : (∀ x : A', B' x) == (∀ x : A, B x) := symm (type_eq H1),
g' : (∀ x : A, B x) := cast S1 g,
L6 : g == g' := cast::eq S1 g,
L6 : g == g' := cast_eq S1 g,
L7 : f == g' := htrans H1 L6,
L8 : f b' == g' b' := congr1 b' L7,
L9 : f a == g' b' := htrans L5 L8,
L10 : g' b' == g b := cast::app S1 L2 g b
L10 : g' b' == g b := cast_app S1 L2 g b
in htrans L9 L10
exit -- Stop here, the following axiom is not sound
@ -72,9 +72,8 @@ theorem unsat : false :=
let L1 : (∀ x : true, true) := (λ x : true, trivial),
L2 : (∀ x : false, true) := (λ x : false, trivial),
-- When we keep Pi/forall as different things, the following two steps can't be used
L3 : (∀ x : true, true) = true := eqt::intro L1,
L4 : (∀ x : false, true) = true := eqt::intro L2,
L3 : (∀ x : true, true) = true := eqt_intro L1,
L4 : (∀ x : false, true) = true := eqt_intro L2,
L5 : (∀ x : true, true) = (∀ x : false, true) := trans L3 (symm L4),
L6 : true = false := dominj L5
in L6

248
src/builtin/kernel.lean
View file

@ -83,23 +83,23 @@ infixl 100 ◂ : eqmp
theorem boolcomplete (a : Bool) : a == true ∨ a == false
:= case (λ x, x == true ∨ x == false) trivial trivial a
theorem false::elim (a : Bool) (H : false) : a
theorem false_elim (a : Bool) (H : false) : a
:= case (λ x, x) trivial H a
theorem imp::trans {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
:= λ Ha, H2 (H1 Ha)
theorem imp::eq::trans {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
:= λ Ha, H2 ◂ (H1 Ha)
theorem eq::imp::trans {a b c : Bool} (H1 : a == b) (H2 : b → c) : a → c
theorem eq_imp_trans {a b c : Bool} (H1 : a == b) (H2 : b → c) : a → c
:= λ Ha, H2 (H1 ◂ Ha)
theorem not::not::eq (a : Bool) : (¬ ¬ a) == a
theorem not_not_eq (a : Bool) : (¬ ¬ a) == a
:= case (λ x, (¬ ¬ x) == x) trivial trivial a
theorem not::not::elim {a : Bool} (H : ¬ ¬ a) : a
:= (not::not::eq a) ◂ H
theorem not_not_elim {a : Bool} (H : ¬ ¬ a) : a
:= (not_not_eq a) ◂ H
theorem mt {a b : Bool} (H1 : a → b) (H2 : ¬ b) : ¬ a
:= λ Ha, absurd (H1 Ha) H2
@ -107,16 +107,16 @@ theorem mt {a b : Bool} (H1 : a → b) (H2 : ¬ b) : ¬ a
theorem contrapos {a b : Bool} (H : a → b) : ¬ b → ¬ a
:= λ Hnb : ¬ b, mt H Hnb
theorem absurd::elim {a : Bool} (b : Bool) (H1 : a) (H2 : ¬ a) : b
:= false::elim b (absurd H1 H2)
theorem absurd_elim {a : Bool} (b : Bool) (H1 : a) (H2 : ¬ a) : b
:= false_elim b (absurd H1 H2)
theorem not::imp::eliml {a b : Bool} (Hnab : ¬ (a → b)) : a
:= not::not::elim
theorem not_imp_eliml {a b : Bool} (Hnab : ¬ (a → b)) : a
:= not_not_elim
(have ¬ ¬ a :
λ Hna : ¬ a, absurd (have a → b : λ Ha : a, absurd::elim b Ha Hna)
λ Hna : ¬ a, absurd (have a → b : λ Ha : a, absurd_elim b Ha Hna)
Hnab)
theorem not::imp::elimr {a b : Bool} (H : ¬ (a → b)) : ¬ b
theorem not_imp_elimr {a b : Bool} (H : ¬ (a → b)) : ¬ b
:= λ Hb : b, absurd (have a → b : λ Ha : a, Hb)
(have ¬ (a → b) : H)
@ -124,30 +124,30 @@ theorem resolve1 {a b : Bool} (H1 : a ∨ b) (H2 : ¬ a) : b
:= H1 H2
-- Recall that and is defined as ¬ (a → ¬ b)
theorem and::intro {a b : Bool} (H1 : a) (H2 : b) : a ∧ b
theorem and_intro {a b : Bool} (H1 : a) (H2 : b) : a ∧ b
:= λ H : a → ¬ b, absurd H2 (H H1)
theorem and::eliml {a b : Bool} (H : a ∧ b) : a
:= not::imp::eliml H
theorem and_eliml {a b : Bool} (H : a ∧ b) : a
:= not_imp_eliml H
theorem and::elimr {a b : Bool} (H : a ∧ b) : b
:= not::not::elim (not::imp::elimr H)
theorem and_elimr {a b : Bool} (H : a ∧ b) : b
:= not_not_elim (not_imp_elimr H)
-- Recall that or is defined as ¬ a → b
theorem or::introl {a : Bool} (H : a) (b : Bool) : a ∨ b
:= λ H1 : ¬ a, absurd::elim b H H1
theorem or_introl {a : Bool} (H : a) (b : Bool) : a ∨ b
:= λ H1 : ¬ a, absurd_elim b H H1
theorem or::intror {b : Bool} (a : Bool) (H : b) : a ∨ b
theorem or_intror {b : Bool} (a : Bool) (H : b) : a ∨ b
:= λ H1 : ¬ a, H
theorem or::elim {a b c : Bool} (H1 : a ∨ b) (H2 : a → c) (H3 : b → c) : c
:= not::not::elim
theorem or_elim {a b c : Bool} (H1 : a ∨ b) (H2 : a → c) (H3 : b → c) : c
:= not_not_elim
(λ H : ¬ c,
absurd (have c : H3 (have b : resolve1 H1 (have ¬ a : (mt (λ Ha : a, H2 Ha) H))))
H)
theorem refute {a : Bool} (H : ¬ a → false) : a
:= or::elim (em a) (λ H1 : a, H1) (λ H1 : ¬ a, false::elim 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
:= subst (refl a) H
@ -157,16 +157,16 @@ theorem trans {A : TypeU} {a b c : A} (H1 : a == b) (H2 : b == c) : a == c
infixl 100 ⋈ : trans
theorem ne::symm {A : TypeU} {a b : A} (H : a ≠ b) : b ≠ a
theorem ne_symm {A : TypeU} {a b : A} (H : a ≠ b) : b ≠ a
:= λ H1 : b = a, H (symm H1)
theorem eq::ne::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 H2 (symm H1)
theorem ne::eq::trans {A : TypeU} {a b c : A} (H1 : a ≠ b) (H2 : b = c) : a ≠ c
theorem ne_eq_trans {A : TypeU} {a b c : A} (H1 : a ≠ b) (H2 : b = c) : a ≠ c
:= subst H1 H2
theorem eqt::elim {a : Bool} (H : a == true) : a
theorem eqt_elim {a : Bool} (H : a == true) : a
:= (symm H) ◂ trivial
theorem congr1 {A : TypeU} {B : A → TypeU} {f g : ∀ x : A, B x} (a : A) (H : f == g) : f a == g a
@ -179,176 +179,176 @@ theorem congr {A : TypeU} {B : A → TypeU} {f g : ∀ x : A, B x} {a b : A} (H1
:= subst (congr2 f H2) (congr1 b H1)
-- Recall that exists is defined as ¬ ∀ x : A, ¬ P x
theorem exists::elim {A : TypeU} {P : A → Bool} {B : Bool} (H1 : Exists A P) (H2 : ∀ (a : A) (H : P a), B) : B
theorem exists_elim {A : TypeU} {P : A → Bool} {B : Bool} (H1 : Exists A P) (H2 : ∀ (a : A) (H : P a), B) : B
:= refute (λ R : ¬ B,
absurd (λ a : A, mt (λ H : P a, H2 a H) R)
H1)
theorem exists::intro {A : TypeU} {P : A → Bool} (a : A) (H : P a) : Exists A P
theorem exists_intro {A : TypeU} {P : A → Bool} (a : A) (H : P a) : Exists A P
:= λ H1 : (∀ x : A, ¬ P x),
absurd H (H1 a)
theorem boolext {a b : Bool} (Hab : a → b) (Hba : b → a) : a == b
:= or::elim (boolcomplete a)
(λ Hat : a == true, or::elim (boolcomplete b)
:= or_elim (boolcomplete a)
(λ Hat : a == true, or_elim (boolcomplete b)
(λ Hbt : b == true, trans Hat (symm Hbt))
(λ Hbf : b == false, false::elim (a == b) (subst (Hab (eqt::elim Hat)) Hbf)))
(λ Haf : a == false, or::elim (boolcomplete b)
(λ Hbt : b == true, false::elim (a == b) (subst (Hba (eqt::elim Hbt)) Haf))
(λ Hbf : b == false, false_elim (a == b) (subst (Hab (eqt_elim Hat)) Hbf)))
(λ Haf : a == false, or_elim (boolcomplete b)
(λ Hbt : b == true, false_elim (a == b) (subst (Hba (eqt_elim Hbt)) Haf))
(λ Hbf : b == false, trans Haf (symm Hbf)))
definition iff::intro {a b : Bool} (Hab : a → b) (Hba : b → a) := boolext Hab Hba
definition iff_intro {a b : Bool} (Hab : a → b) (Hba : b → a) := boolext Hab Hba
theorem eqt::intro {a : Bool} (H : a) : a == true
theorem eqt_intro {a : Bool} (H : a) : a == true
:= boolext (λ H1 : a, trivial)
(λ H2 : true, H)
theorem or::comm (a b : Bool) : (a ∨ b) == (b ∨ a)
:= boolext (λ H, or::elim H (λ H1, or::intror b H1) (λ H2, or::introl H2 a))
(λ H, or::elim H (λ H1, or::intror a H1) (λ H2, or::introl H2 b))
theorem or_comm (a b : Bool) : (a ∨ b) == (b ∨ a)
:= boolext (λ H, or_elim H (λ H1, or_intror b H1) (λ H2, or_introl H2 a))
(λ H, or_elim H (λ H1, or_intror a H1) (λ H2, or_introl H2 b))
theorem or::assoc (a b c : Bool) : ((a ∨ b) ∨ c) == (a ∨ (b ∨ c))
theorem or_assoc (a b c : Bool) : ((a ∨ b) ∨ c) == (a ∨ (b ∨ c))
:= boolext (λ 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)))
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)))
(λ 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)))
or_elim H (λ Ha : a, (or_introl (or_introl Ha b) c))
(λ H1 : b ∨ c, or_elim H1 (λ Hb : b, or_introl (or_intror a Hb) c)
(λ Hc : c, or_intror (a ∨ b) Hc)))
theorem or::id (a : Bool) : (a ∨ a) == a
:= boolext (λ H, or::elim H (λ H1, H1) (λ H2, H2))
(λ H, or::introl H a)
theorem or_id (a : Bool) : (a ∨ a) == a
:= boolext (λ H, or_elim H (λ H1, H1) (λ H2, H2))
(λ H, or_introl H a)
theorem or::falsel (a : Bool) : (a ∨ false) == a
:= boolext (λ H, or::elim H (λ H1, H1) (λ H2, false::elim a H2))
(λ H, or::introl H false)
theorem or_falsel (a : Bool) : (a ∨ false) == a
:= boolext (λ H, or_elim H (λ H1, H1) (λ H2, false_elim a H2))
(λ H, or_introl H false)
theorem or::falser (a : Bool) : (false ∨ a) == a
:= (or::comm false a) ⋈ (or::falsel a)
theorem or_falser (a : Bool) : (false ∨ a) == a
:= (or_comm false a) ⋈ (or_falsel a)
theorem or::truel (a : Bool) : (true ∨ a) == true
:= eqt::intro (case (λ x : Bool, true ∨ x) trivial trivial a)
theorem or_truel (a : Bool) : (true ∨ a) == true
:= eqt_intro (case (λ x : Bool, true ∨ x) trivial trivial a)
theorem or::truer (a : Bool) : (a ∨ true) == true
:= (or::comm a true) ⋈ (or::truel a)
theorem or_truer (a : Bool) : (a ∨ true) == true
:= (or_comm a true) ⋈ (or_truel a)
theorem or::tauto (a : Bool) : (a ∨ ¬ a) == true
:= eqt::intro (em a)
theorem or_tauto (a : Bool) : (a ∨ ¬ a) == true
:= eqt_intro (em a)
theorem and::comm (a b : Bool) : (a ∧ b) == (b ∧ a)
:= boolext (λ H, and::intro (and::elimr H) (and::eliml H))
(λ H, and::intro (and::elimr H) (and::eliml H))
theorem and_comm (a b : Bool) : (a ∧ b) == (b ∧ a)
:= boolext (λ H, and_intro (and_elimr H) (and_eliml H))
(λ H, and_intro (and_elimr H) (and_eliml H))
theorem and::id (a : Bool) : (a ∧ a) == a
:= boolext (λ H, and::eliml H)
(λ H, and::intro H H)
theorem and_id (a : Bool) : (a ∧ a) == a
:= boolext (λ H, and_eliml H)
(λ H, and_intro H H)
theorem and::assoc (a b c : Bool) : ((a ∧ b) ∧ c) == (a ∧ (b ∧ c))
:= boolext (λ H, and::intro (and::eliml (and::eliml H)) (and::intro (and::elimr (and::eliml H)) (and::elimr H)))
(λ H, and::intro (and::intro (and::eliml H) (and::eliml (and::elimr H))) (and::elimr (and::elimr H)))
theorem and_assoc (a b c : Bool) : ((a ∧ b) ∧ c) == (a ∧ (b ∧ c))
:= boolext (λ H, and_intro (and_eliml (and_eliml H)) (and_intro (and_elimr (and_eliml H)) (and_elimr H)))
(λ H, and_intro (and_intro (and_eliml H) (and_eliml (and_elimr H))) (and_elimr (and_elimr H)))
theorem and::truer (a : Bool) : (a ∧ true) == a
:= boolext (λ H : a ∧ true, and::eliml H)
(λ H : a, and::intro H trivial)
theorem and_truer (a : Bool) : (a ∧ true) == a
:= boolext (λ H : a ∧ true, and_eliml H)
(λ H : a, and_intro H trivial)
theorem and::truel (a : Bool) : (true ∧ a) == a
:= trans (and::comm true a) (and::truer a)
theorem and_truel (a : Bool) : (true ∧ a) == a
:= trans (and_comm true a) (and_truer a)
theorem and::falsel (a : Bool) : (a ∧ false) == false
:= boolext (λ H, and::elimr H)
(λ H, false::elim (a ∧ false) H)
theorem and_falsel (a : Bool) : (a ∧ false) == false
:= boolext (λ H, and_elimr H)
(λ H, false_elim (a ∧ false) H)
theorem and::falser (a : Bool) : (false ∧ a) == false
:= (and::comm false a) ⋈ (and::falsel a)
theorem and_falser (a : Bool) : (false ∧ a) == false
:= (and_comm false a) ⋈ (and_falsel a)
theorem and::absurd (a : Bool) : (a ∧ ¬ a) == false
:= boolext (λ H, absurd (and::eliml H) (and::elimr H))
(λ H, false::elim (a ∧ ¬ a) H)
theorem and_absurd (a : Bool) : (a ∧ ¬ a) == false
:= boolext (λ H, absurd (and_eliml H) (and_elimr H))
(λ H, false_elim (a ∧ ¬ a) H)
theorem not::true : (¬ true) == false
theorem not_true : (¬ true) == false
:= trivial
theorem not::false : (¬ false) == true
theorem not_false : (¬ false) == true
:= trivial
theorem not::and (a b : Bool) : (¬ (a ∧ b)) == (¬ a ∨ ¬ b)
theorem not_and (a b : Bool) : (¬ (a ∧ b)) == (¬ a ∨ ¬ b)
:= case (λ x, (¬ (x ∧ b)) == (¬ x ∨ ¬ b))
(case (λ y, (¬ (true ∧ y)) == (¬ true ∨ ¬ y)) trivial trivial b)
(case (λ y, (¬ (false ∧ y)) == (¬ false ∨ ¬ y)) trivial trivial b)
a
theorem not::and::elim {a b : Bool} (H : ¬ (a ∧ b)) : ¬ a ∨ ¬ b
:= (not::and a b) ◂ H
theorem not_and_elim {a b : Bool} (H : ¬ (a ∧ b)) : ¬ a ∨ ¬ b
:= (not_and a b) ◂ H
theorem not::or (a b : Bool) : (¬ (a ∨ b)) == (¬ a ∧ ¬ b)
theorem not_or (a b : Bool) : (¬ (a ∨ b)) == (¬ a ∧ ¬ b)
:= case (λ x, (¬ (x ∨ b)) == (¬ x ∧ ¬ b))
(case (λ y, (¬ (true ∨ y)) == (¬ true ∧ ¬ y)) trivial trivial b)
(case (λ y, (¬ (false ∨ y)) == (¬ false ∧ ¬ y)) trivial trivial b)
a
theorem not::or::elim {a b : Bool} (H : ¬ (a ∨ b)) : ¬ a ∧ ¬ b
:= (not::or a b) ◂ H
theorem not_or_elim {a b : Bool} (H : ¬ (a ∨ b)) : ¬ a ∧ ¬ b
:= (not_or a b) ◂ H
theorem not::iff (a b : Bool) : (¬ (a == b)) == ((¬ a) == b)
theorem not_iff (a b : Bool) : (¬ (a == b)) == ((¬ a) == b)
:= case (λ x, (¬ (x == b)) == ((¬ x) == b))
(case (λ y, (¬ (true == y)) == ((¬ true) == y)) trivial trivial b)
(case (λ y, (¬ (false == y)) == ((¬ false) == y)) trivial trivial b)
a
theorem not::iff::elim {a b : Bool} (H : ¬ (a == b)) : (¬ a) == b
:= (not::iff a b) ◂ H
theorem not_iff_elim {a b : Bool} (H : ¬ (a == b)) : (¬ a) == b
:= (not_iff a b) ◂ H
theorem not::implies (a b : Bool) : (¬ (a → b)) == (a ∧ ¬ b)
theorem not_implies (a b : Bool) : (¬ (a → b)) == (a ∧ ¬ b)
:= case (λ x, (¬ (x → b)) == (x ∧ ¬ b))
(case (λ y, (¬ (true → y)) == (true ∧ ¬ y)) trivial trivial b)
(case (λ y, (¬ (false → y)) == (false ∧ ¬ y)) trivial trivial b)
a
theorem not::implies::elim {a b : Bool} (H : ¬ (a → b)) : a ∧ ¬ b
:= (not::implies a b) ◂ H
theorem not_implies_elim {a b : Bool} (H : ¬ (a → b)) : a ∧ ¬ b
:= (not_implies a b) ◂ H
theorem not::congr {a b : Bool} (H : a == b) : (¬ a) == (¬ b)
theorem not_congr {a b : Bool} (H : a == b) : (¬ a) == (¬ b)
:= congr2 not H
theorem eq::exists::intro {A : (Type U)} {P Q : A → Bool} (H : ∀ x : A, P x == Q x) : (∃ x : A, P x) == (∃ x : A, Q x)
theorem eq_exists_intro {A : (Type U)} {P Q : A → Bool} (H : ∀ x : A, P x == Q x) : (∃ x : A, P x) == (∃ x : A, Q x)
:= congr2 (Exists A) (funext H)
theorem not::forall (A : (Type U)) (P : A → Bool) : (¬ (∀ x : A, P x)) == (∃ x : A, ¬ P x)
:= calc (¬ ∀ x : A, P x) = (¬ ∀ x : A, ¬ ¬ P x) : not::congr (allext (λ x : A, symm (not::not::eq (P x))))
theorem not_forall (A : (Type U)) (P : A → Bool) : (¬ (∀ x : A, P x)) == (∃ x : A, ¬ P x)
:= calc (¬ ∀ x : A, P x) = (¬ ∀ x : A, ¬ ¬ P x) : not_congr (allext (λ x : A, symm (not_not_eq (P x))))
... = (∃ x : A, ¬ P x) : refl (∃ x : A, ¬ P x)
theorem not::forall::elim {A : (Type U)} {P : A → Bool} (H : ¬ (∀ x : A, P x)) : ∃ x : A, ¬ P x
:= (not::forall A P) ◂ H
theorem not_forall_elim {A : (Type U)} {P : A → Bool} (H : ¬ (∀ x : A, P x)) : ∃ x : A, ¬ P x
:= (not_forall A P) ◂ H
theorem not::exists (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)
:= calc (¬ ∃ x : A, P x) = (¬ ¬ ∀ x : A, ¬ P x) : refl (¬ ∃ x : A, P x)
... = (∀ x : A, ¬ P x) : not::not::eq (∀ x : A, ¬ P x)
... = (∀ x : A, ¬ P x) : not_not_eq (∀ x : A, ¬ P x)
theorem not::exists::elim {A : (Type U)} {P : A → Bool} (H : ¬ ∃ x : A, P x) : ∀ x : A, ¬ P x
:= (not::exists A P) ◂ H
theorem not_exists_elim {A : (Type U)} {P : A → Bool} (H : ¬ ∃ x : A, P x) : ∀ x : A, ¬ P x
:= (not_exists A P) ◂ H
theorem exists::unfold1 {A : TypeU} {P : A → Bool} (a : A) (H : ∃ x : A, P x) : P a ∨ (∃ x : A, x ≠ a ∧ P x)
:= exists::elim H
theorem exists_unfold1 {A : TypeU} {P : A → Bool} (a : A) (H : ∃ x : A, P x) : P a ∨ (∃ x : A, x ≠ a ∧ P x)
:= exists_elim H
(λ (w : A) (H1 : P w),
or::elim (em (w = a))
(λ Heq : w = a, or::introl (subst H1 Heq) (∃ x : A, x ≠ a ∧ P x))
(λ Hne : w ≠ a, or::intror (P a) (exists::intro w (and::intro Hne H1))))
or_elim (em (w = a))
(λ Heq : w = a, or_introl (subst H1 Heq) (∃ x : A, x ≠ a ∧ P x))
(λ Hne : w ≠ a, or_intror (P a) (exists_intro w (and_intro Hne H1))))
theorem exists::unfold2 {A : TypeU} {P : A → Bool} (a : A) (H : P a ∨ (∃ x : A, x ≠ a ∧ P x)) : ∃ x : A, P x
:= or::elim H
(λ H1 : P a, exists::intro a H1)
theorem exists_unfold2 {A : TypeU} {P : A → Bool} (a : A) (H : P a ∨ (∃ x : A, x ≠ a ∧ P x)) : ∃ x : A, P x
:= or_elim H
(λ H1 : P a, exists_intro a H1)
(λ H2 : (∃ x : A, x ≠ a ∧ P x),
exists::elim H2
exists_elim H2
(λ (w : A) (Hw : w ≠ a ∧ P w),
exists::intro w (and::elimr Hw)))
exists_intro w (and_elimr Hw)))
theorem exists::unfold {A : TypeU} (P : A → Bool) (a : A) : (∃ x : A, P x) = (P a ∨ (∃ x : A, x ≠ a ∧ P x))
:= boolext (λ H : (∃ x : A, P x), exists::unfold1 a H)
(λ H : (P a ∨ (∃ x : A, x ≠ a ∧ P x)), exists::unfold2 a H)
theorem exists_unfold {A : TypeU} (P : A → Bool) (a : A) : (∃ x : A, P x) = (P a ∨ (∃ x : A, x ≠ a ∧ P x))
:= boolext (λ H : (∃ x : A, P x), exists_unfold1 a H)
(λ H : (P a ∨ (∃ x : A, x ≠ a ∧ P x)), exists_unfold2 a H)
set::opaque exists true
set::opaque not true
set::opaque or true
set::opaque and true
set::opaque implies true
set_opaque exists true
set_opaque not true
set_opaque or true
set_opaque and true
set_opaque implies true

2
src/builtin/macros.lua
View file

@ -92,7 +92,7 @@ macro("obtain", { macro_arg.Parameters, macro_arg.Comma, macro_arg.Id, macro_arg
if fromid ~= name("from") then
error("invalid 'obtain' expression, 'from' keyword expected, got '" .. tostring(fromid) .. "'")
end
local exElim = mk_constant({"exists", "elim"})
local exElim = mk_constant("exists_elim")
local H_name = bindings[n][1]
local H_type = bindings[n][2]
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);
}
static name g_eq_imp_trans({"eq", "imp", "trans"});
static name g_imp_eq_trans({"imp", "eq", "trans"});
static name g_imp_trans({"imp", "trans"});
static name g_eq_ne_trans({"eq", "ne", "trans"});
static name g_ne_eq_trans({"ne", "eq", "trans"});
static name g_eq_imp_trans("eq_imp_trans");
static name g_imp_eq_trans("imp_eq_trans");
static name g_imp_trans("imp_trans");
static name g_eq_ne_trans("eq_ne_trans");
static name g_ne_eq_trans("ne_eq_trans");
static name g_neq("neq");
calc_proof_parser::calc_proof_parser() {

6
src/frontends/lean/parser_cmds.cpp
View file

@ -37,8 +37,8 @@ static name g_infix_kwd("infix");
static name g_infixl_kwd("infixl");
static name g_infixr_kwd("infixr");
static name g_notation_kwd("notation");
static name g_set_option_kwd("set", "option");
static name g_set_opaque_kwd("set", "opaque");
static name g_set_option_kwd("set_option");
static name g_set_opaque_kwd("set_opaque");
static name g_options_kwd("options");
static name g_env_kwd("environment");
static name g_import_kwd("import");
@ -46,7 +46,7 @@ static name g_help_kwd("help");
static name g_coercion_kwd("coercion");
static name g_exit_kwd("exit");
static name g_print_kwd("print");
static name g_pop_kwd("pop", "scope");
static name g_pop_kwd("pop_scope");
static name g_scope_kwd("scope");
static name g_builtin_kwd("builtin");
static name g_namespace_kwd("namespace");

34
src/kernel/builtin.cpp
View file

@ -137,35 +137,35 @@ MK_CONSTANT(hsymm_fn, name("hsymm"));
MK_CONSTANT(eta_fn, name("eta"));
MK_CONSTANT(imp_antisym_fn, name("iffintro"));
MK_CONSTANT(trivial, name("trivial"));
MK_CONSTANT(false_elim_fn, name({"false", "elim"}));
MK_CONSTANT(false_elim_fn, name("false_elim"));
MK_CONSTANT(absurd_fn, name("absurd"));
MK_CONSTANT(em_fn, name("em"));
MK_CONSTANT(double_neg_fn, name("doubleneg"));
MK_CONSTANT(double_neg_elim_fn, name({"doubleneg", "elim"}));
MK_CONSTANT(double_neg_elim_fn, name("doubleneg_elim"));
MK_CONSTANT(mt_fn, name("mt"));
MK_CONSTANT(contrapos_fn, name("contrapos"));
MK_CONSTANT(absurd_elim_fn, name({"absurd", "elim"}));
MK_CONSTANT(absurd_elim_fn, name("absurd_elim"));
MK_CONSTANT(eq_mp_fn, name("eqmp"));
MK_CONSTANT(not_imp1_fn, name({"not", "imp", "eliml"}));
MK_CONSTANT(not_imp2_fn, name({"not", "imp", "elimr"}));
MK_CONSTANT(conj_fn, name({"and", "intro"}));
MK_CONSTANT(conjunct1_fn, name({"and", "eliml"}));
MK_CONSTANT(conjunct2_fn, name({"and", "elimr"}));
MK_CONSTANT(disj1_fn, name({"or", "introl"}));
MK_CONSTANT(disj2_fn, name({"or", "intror"}));
MK_CONSTANT(disj_cases_fn, name({"or", "elim"}));
MK_CONSTANT(not_imp1_fn, name("not_imp_eliml"));
MK_CONSTANT(not_imp2_fn, name("not_imp_elimr"));
MK_CONSTANT(conj_fn, name("and_intro"));
MK_CONSTANT(conjunct1_fn, name("and_eliml"));
MK_CONSTANT(conjunct2_fn, name("and_elimr"));
MK_CONSTANT(disj1_fn, name("or_introl"));
MK_CONSTANT(disj2_fn, name("or_intror"));
MK_CONSTANT(disj_cases_fn, name("or_elim"));
MK_CONSTANT(refute_fn, name("refute"));
MK_CONSTANT(symm_fn, name("symm"));
MK_CONSTANT(trans_fn, name("trans"));
MK_CONSTANT(congr1_fn, name("congr1"));
MK_CONSTANT(congr2_fn, name("congr2"));
MK_CONSTANT(congr_fn, name("congr"));
MK_CONSTANT(eqt_elim_fn, name({"eqt", "elim"}));
MK_CONSTANT(eqt_intro_fn, name({"eqt", "intro"}));
MK_CONSTANT(forall_elim_fn, name({"forall", "elim"}));
MK_CONSTANT(forall_intro_fn, name({"forall", "intro"}));
MK_CONSTANT(exists_elim_fn, name({"exists", "elim"}));
MK_CONSTANT(exists_intro_fn, name({"exists", "intro"}));
MK_CONSTANT(eqt_elim_fn, name("eqt_elim"));
MK_CONSTANT(eqt_intro_fn, name("eqt_intro"));
MK_CONSTANT(forall_elim_fn, name("forall_elim"));
MK_CONSTANT(forall_intro_fn, name("forall_intro"));
MK_CONSTANT(exists_elim_fn, name("exists_elim"));
MK_CONSTANT(exists_intro_fn, name("exists_intro"));
void import_kernel(environment const & env, io_state const & ios) {
env->import("kernel", ios);

2
src/kernel/environment.cpp
View file

@ -34,7 +34,7 @@ class set_opaque_command : public neutral_object_cell {
public:
set_opaque_command(name const & n, bool opaque):m_obj_name(n), m_opaque(opaque) {}
virtual ~set_opaque_command() {}
virtual char const * keyword() const { return "set::opaque"; }
virtual char const * keyword() const { return "set_opaque"; }
virtual void write(serializer & s) const { s << "Opa" << m_obj_name << m_opaque; }
name const & get_obj_name() const { return m_obj_name; }
bool get_flag() const { return m_opaque; }

10
src/tests/frontends/lean/parser.cpp
View file

@ -94,11 +94,11 @@ static void tst3() {
parse_error(env, ios, "check U");
parse(env, ios, "variable h : Real -> Real -> Real. notation 10 [ _ ; _ ] : h. check [ 10.3 ; 20.1 ].");
parse_error(env, ios, "variable h : Real -> Real -> Real. notation 10 [ _ ; _ ] : h. check [ 10.3 | 20.1 ].");
parse_error(env, ios, "set::option pp::indent true");
parse(env, ios, "set::option pp::indent 10");
parse_error(env, ios, "set::option pp::colors foo");
parse_error(env, ios, "set::option pp::colors \"foo\"");
parse(env, ios, "set::option pp::colors true");
parse_error(env, ios, "set_option pp::indent true");
parse(env, ios, "set_option pp::indent 10");
parse_error(env, ios, "set_option pp::colors foo");
parse_error(env, ios, "set_option pp::colors \"foo\"");
parse(env, ios, "set_option pp::colors true");
parse_error(env, ios, "notation 10 : Int::add");
parse_error(env, ios, "notation 10 _ : Int::add");
parse(env, ios, "notation 10 _ ++ _ : Int::add. eval 10 ++ 20.");

2
tests/lean/abst.lean
View file

@ -2,5 +2,5 @@ import Int.
axiom PlusComm(a b : Int) : a + b == b + a.
variable a : Int.
check (funext (fun x : Int, (PlusComm a x))).
set::option pp::implicit true.
set_option pp::implicit true.
check (funext (fun x : Int, (PlusComm a x))).

8
tests/lean/alias2.lean
View file

@ -3,14 +3,14 @@ scope
alias ℕℕ : Natural.
variable x : Natural.
print environment 1.
set::option pp::unicode false.
set_option pp::unicode false.
print environment 1.
set::option pp::unicode true.
set_option pp::unicode true.
print environment 1.
alias NN : Natural.
print environment 2.
alias ℕℕℕ : Natural.
print environment 3.
set::option pp::unicode false.
set_option pp::unicode false.
print environment 3.
pop::scope
pop_scope

4
tests/lean/arith1.lean
View file

@ -10,9 +10,9 @@ variable n : Nat
variable m : Nat
print n + m
print n + x + m
set::option lean::pp::coercion true
set_option lean::pp::coercion true
print n + x + m + 10
print x + n + m + 10
print n + m + 10 + x
set::option lean::pp::notation false
set_option lean::pp::notation false
print n + m + 10 + x

2
tests/lean/arith2.lean
View file

@ -7,7 +7,7 @@ variable x : Real
variable i : Int
variable n : Nat
print x + i + 1 + n
set::option lean::pp::coercion true
set_option lean::pp::coercion true
print x + i + 1 + n
print x * i + x
print x - i + x - x >= 0

2
tests/lean/arith3.lean
View file

@ -4,7 +4,7 @@ eval 8 div 4
eval 7 div 3
eval 7 mod 3
print -8 mod 3
set::option lean::pp::notation false
set_option lean::pp::notation false
print -8 mod 3
eval -8 mod 3
eval (-8 div 3)*3 + (-8 mod 3)

4
tests/lean/arith6.lean
View file

@ -1,5 +1,5 @@
import Int.
set::option pp::unicode false
set_option pp::unicode false
print 3 | 6
eval 3 | 6
eval 3 | 7
@ -9,5 +9,5 @@ variable x : Int
eval x | 3
eval 3 | x
eval 6 | 3
set::option pp::notation false
set_option pp::notation false
print 3 | x

2
tests/lean/arith7.lean
View file

@ -11,6 +11,6 @@ eval |x + 1| > 0
variable y : Int
eval |x + y|
print |x + y| > x
set::option pp::notation false
set_option pp::notation false
print |x + y| > x
print |x + y| + |y + x| > x

4
tests/lean/bad10.lean
View file

@ -1,5 +1,5 @@
set::option pp::implicit true.
set::option pp::colors false.
set_option pp::implicit true.
set_option pp::colors false.
variable N : Type.
definition T (a : N) (f : _ -> _) (H : f a == a) : f (f _) == f _ :=

4
tests/lean/bad2.lean
View file

@ -8,6 +8,6 @@ definition n3 : list Int := cons 10 nil
definition n4 : list Int := nil
definition n5 : _ := cons 10 nil
set::option pp::coercion true
set::option pp::implicit true
set_option pp::coercion true
set_option pp::implicit true
print environment 1.

4
tests/lean/bad9.lean
View file

@ -1,5 +1,5 @@
set::option pp::implicit true.
set::option pp::colors false.
set_option pp::implicit true.
set_option pp::colors false.
variable N : Type.
check

2
tests/lean/cast4.lean
View file

@ -1,5 +1,5 @@
import cast
set::option pp::colors false
set_option pp::colors false
check fun (A A': TypeM)
(B : A -> TypeM)

10
tests/lean/coercion2.lean
View file

@ -8,25 +8,25 @@ print g a a
variable b : R
print g a b
print g b a
set::option lean::pp::coercion true
set_option lean::pp::coercion true
print g a a
print g a b
print g b a
set::option lean::pp::coercion false
set_option lean::pp::coercion false
variable S : Type
variable s : S
variable r : S
variable h : S -> S -> S
infixl 10 ++ : g
infixl 10 ++ : h
set::option lean::pp::notation false
set_option lean::pp::notation false
print a ++ b ++ a
print r ++ s ++ r
check a ++ b ++ a
check r ++ s ++ r
set::option lean::pp::coercion true
set_option lean::pp::coercion true
print a ++ b ++ a
print r ++ s ++ r
set::option lean::pp::notation true
set_option lean::pp::notation true
print a ++ b ++ a
print r ++ s ++ r

6
tests/lean/config.lean
View file

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

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

@ -3,4 +3,4 @@
Imported 'tactic'
Proved: T1
Proved: T2
theorem T2 (a b : Bool) (H : a ∨ b) : b ∨ a := or::elim H (λ H : a, or::intror b H) (λ H : b, or::introl H a)
theorem T2 (a b : Bool) (H : a ∨ b) : b ∨ a := or_elim H (λ H : a, or_intror b H) (λ H : b, or_introl H a)

6
tests/lean/disjcases.lean
View file

@ -2,9 +2,9 @@
variables a b c : Bool
axiom H : a \/ b
theorem T (a b : Bool) : a \/ b → b \/ a.
apply (or::elim H).
apply or::intror.
apply (or_elim H).
apply or_intror.
exact.
apply or::introl.
apply or_introl.
exact.
done.

4
tests/lean/elab1.lean
View file

@ -15,13 +15,13 @@ check fun (A B : Type) (a : _) (b : _) (C : Type), my_eq C a b.
variable a : Bool
variable b : Bool
variable H : a /\ b
theorem t1 : b := (fun H1, and::intro H1 (and::eliml H)).
theorem t1 : b := (fun H1, and_intro H1 (and_eliml H)).
theorem t2 : a = b := trans (refl a) (refl b).
check f Bool Bool.
theorem pierce (a b : Bool) : ((a -> b) -> a) -> a :=
λ H, or::elim (EM a)
λ H, or_elim (EM a)
(λ H_a, H)
(λ H_na, NotImp1 (MT H H_na))

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

@ -54,4 +54,4 @@ Failed to solve
?M::0
Bool
Bool
Error (line: 25, pos: 19) unknown identifier 'EM'
Error (line: 25, pos: 18) unknown identifier 'EM'

2
tests/lean/elab4.lean
View file

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

2
tests/lean/elab5.lean
View file

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

2
tests/lean/elab7.lean
View file

@ -17,5 +17,5 @@ theorem T2 : (fun (x1 : A) (x2 : B), F1 x1 x2) = F2 := funext (fun a, (funext (f
theorem T3 : F1 = (fun (x1 : A) (x2 : B), F2 x1 x2) := funext (fun a, (funext (fun b, H a b)))
theorem T4 : (fun (x1 : A) (x2 : B), F1 x1 x2) = (fun (x1 : A) (x2 : B), F2 x1 x2) := funext (fun a, (funext (fun b, H a b)))
print environment 4
set::option pp::implicit true
set_option pp::implicit true
print environment 4

4
tests/lean/env_errors.lean
View file

@ -1,7 +1,6 @@
variable x : Nat
set::opaque x true.
set_opaque x true.
print "before import"
(*
@ -26,4 +25,3 @@ print "before load3"
local env = get_environment()
env:load("fake2.olean")
*)

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

@ -1,12 +1,12 @@
Set: pp::colors
Set: pp::unicode
Assumed: x
Error (line: 4, pos: 0) set_opaque failed, 'x' is not a definition
Error (line: 3, pos: 0) set_opaque failed, 'x' is not a definition
before import
Error (line: 12, pos: 0) file 'tstblafoo.lean' not found in the LEAN_PATH
Error (line: 11, pos: 0) file 'tstblafoo.lean' not found in the LEAN_PATH
before load1
Error (line: 18, pos: 0) failed to open file 'tstblafoo.lean'
Error (line: 17, pos: 0) failed to open file 'tstblafoo.lean'
before load2
Error (line: 24, pos: 0) corrupted binary file
Error (line: 23, pos: 0) corrupted binary file
before load3
Error (line: 30, pos: 0) file 'fake2.olean' does not seem to be a valid object Lean file
Error (line: 28, pos: 0) file 'fake2.olean' does not seem to be a valid object Lean file

2
tests/lean/eq1.lean
View file

@ -1,5 +1,5 @@
import Int.
variable i : Int
check i = 0
set::option pp::coercion true
set_option pp::coercion true
check i = 0

2
tests/lean/eq2.lean
View file

@ -4,5 +4,5 @@ variable nil {A : Type} : List A
variable cons {A : Type} (head : A) (tail : List A) : List A
variable l : List Int.
check l = nil.
set::option pp::implicit true
set_option pp::implicit true
check l = nil.

2
tests/lean/eq3.lean
View file

@ -7,5 +7,5 @@ variable v3 : Vector (0 + n)
axiom H1 : v1 == v2
axiom H2 : v2 == v3
check htrans H1 H2
set::option pp::implicit true
set_option pp::implicit true
check htrans H1 H2

10
tests/lean/ex2.lean
View file

@ -1,8 +1,8 @@
-- comment
print true
set::option lean::pp::notation false
set_option lean::pp::notation false
print true && false
set::option pp::unicode false
set_option pp::unicode false
print true && false
variable a : Bool
variable a : Bool
@ -12,7 +12,7 @@ variable A : Type
check a && A
print environment 1
print options
set::option lean::p::notation true
set::option lean::pp::notation 10
set::option lean::pp::notation true
set_option lean::p::notation true
set_option lean::pp::notation 10
set_option lean::pp::notation true
print a && b

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

@ -19,7 +19,7 @@ Arguments types:
A : Type
variable A : Type
(lean::pp::notation := false, pp::unicode := false, pp::colors := false)
Error (line: 15, pos: 12) unknown option 'lean::p::notation', type 'Help Options.' for list of available options
Error (line: 16, pos: 31) invalid option value, given option is not an integer
Error (line: 15, pos: 11) unknown option 'lean::p::notation', type 'Help Options.' for list of available options
Error (line: 16, pos: 30) invalid option value, given option is not an integer
Set: lean::pp::notation
a /\ b

2
tests/lean/ex3.lean
View file

@ -5,5 +5,5 @@ variable a : T
check myeq _ true a
variable myeq2 {A:Type} (a b : A) : Bool
infix 50 === : myeq2
set::option lean::pp::implicit true
set_option lean::pp::implicit true
check true === a

2
tests/lean/exists1.lean
View file

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

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

@ -5,4 +5,4 @@
Assumed: P
Assumed: H
Proved: T
theorem T : ∃ x : ℤ, P a a := exists::intro 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 H2 : P (f (g a) (g a)) (f (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) := exists::intro _ (exists::intro _ 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) := exists::intro _ 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 := exists::intro _ H2
theorem T6 : exists x y : Int, P x y := exists::intro _ (exists::intro _ 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 := exists::intro _ (exists::intro _ H3)
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)) := exists_intro _ H1
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) := exists_intro _ H2
theorem T5 : exists x : Int, P x x := exists_intro _ H2
theorem T6 : exists x y : Int, P x y := exists_intro _ (exists_intro _ 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 := exists_intro _ (exists_intro _ H3)
print environment 8.

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

@ -16,11 +16,11 @@
Proved: T6
Proved: T7
Proved: T8
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)) := exists::intro a H1
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) := exists::intro (g a) H2
theorem T5 : ∃ x : ℤ, P x x := exists::intro (f (g a) (g a)) H2
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 := exists::intro (g a) H3
theorem T8 : ∃ x y : ℤ, P (f x x) y := exists::intro (g a) (exists::intro (g a) H3)
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)) := exists_intro a H1
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) := exists_intro (g a) H2
theorem T5 : ∃ x : ℤ, P x x := exists_intro (f (g a) (g a)) H2
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 := exists_intro (g a) H3
theorem T8 : ∃ x y : ℤ, P (f x x) y := exists_intro (g a) (exists_intro (g a) H3)

12
tests/lean/exists3.lean
View file

@ -1,25 +1,25 @@
import Int.
variable P : Int -> Int -> Bool
set::opaque exists false.
set_opaque exists false.
theorem T1 (R1 : not (exists x y, P x y)) : forall x y, not (P x y) :=
fun a b,
not::not::elim (not::not::elim R1 a) b
not_not_elim (not_not_elim R1 a) b
axiom Ax : forall x, exists y, P x y
theorem T2 : exists x y, P x y :=
refute (fun R : not (exists x y, P x y),
let L1 : forall x y, not (P x y) := fun a b, (not::not::elim ((not::not::elim R) a)) b,
let L1 : forall x y, not (P x y) := fun a b, (not_not_elim ((not_not_elim R) a)) b,
L2 : exists y, P 0 y := Ax 0
in exists::elim L2 (fun (w : Int) (H : P 0 w),
in exists_elim L2 (fun (w : Int) (H : P 0 w),
absurd H (L1 0 w))).
theorem T3 (A : (Type U)) (P : A -> A -> Bool) (a : A) (H1 : forall x, exists y, P x y) : exists x y, P x y :=
refute (fun R : not (exists x y, P x y),
let L1 : forall x y, not (P x y) := fun a b,
(not::not::elim ((not::not::elim R) a)) b,
(not_not_elim ((not_not_elim R) a)) b,
L2 : exists y, P a y := H1 a
in exists::elim L2 (fun (w : A) (H : P a w),
in exists_elim L2 (fun (w : A) (H : P a w),
absurd H (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
axiom H3 : P a b c
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
(exists::@intro N _ b
(exists::@intro N (fun z : N, P a b z) c H3))
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
(@exists_intro N _ b
(@exists_intro N (fun z : N, P a b z) c H3))
theorem T2 : exists x y z : N, P x y z := exists::intro a (exists::intro b (exists::intro 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 := exists::intro _ (exists::intro _ (exists::intro _ 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 := exists::intro _ (exists::intro _ (exists::intro _ 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

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

@ -11,11 +11,11 @@
Proved: T3
Proved: T4
theorem T1 : ∃ x y z : N, P x y z :=
exists::@intro
@exists_intro
N
(λ x : N, ∃ y z : N, P x y z)
a
(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 := exists::intro a (exists::intro b (exists::intro 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 := exists::intro a (exists::intro a (exists::intro b H))
(@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 := exists_intro a (exists_intro b (exists_intro 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 := 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 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 := exists::intro _ (exists::intro _ (exists::intro _ 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.

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

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

2
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 Ax2 : forall x y z, not (P x y z)
theorem T : false :=
exists::elim Ax1 (fun a H1, exists::elim H1 (fun b H2, exists::elim H2 (fun (c : Int) (H3 : P a b c),
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) := Ax2 a b c
in absurd H3 notH3)))

8
tests/lean/exists7.lean
View file

@ -1,11 +1,11 @@
set::option pp::colors false
set_option pp::colors false
variable N : Type
variables a b c : N
variables P : N -> N -> N -> Bool
set::opaque exists false.
set::opaque not false.
set_opaque exists false.
set_opaque not false.
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))
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.

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

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

10
tests/lean/exists8.lean
View file

@ -3,22 +3,22 @@ variable P : Int -> Int -> Bool
theorem T1 (R1 : not (exists x y, P x y)) : forall x y, not (P x y) :=
fun a b,
(not::exists::elim (not::exists::elim R1 a)) b
(not_exists_elim (not_exists_elim R1 a)) b
axiom Ax : forall x, exists y, P x y
theorem T2 : exists x y, P x y :=
refute (fun R : not (exists x y, P x y),
let L1 : forall x y, not (P x y) := fun a b,
(not::exists::elim ((not::exists::elim R) a)) b,
(not_exists_elim ((not_exists_elim R) a)) b,
L2 : exists y, P 0 y := Ax 0
in exists::elim L2 (fun (w : Int) (H : P 0 w),
in exists_elim L2 (fun (w : Int) (H : P 0 w),
absurd H (L1 0 w))).
theorem T3 (A : (Type U)) (P : A -> A -> Bool) (a : A) (H1 : forall x, exists y, P x y) : exists x y, P x y :=
refute (fun R : not (exists x y, P x y),
let L1 : forall x y, not (P x y) := fun a b,
(not::exists::elim ((not::exists::elim R) a)) b,
(not_exists_elim ((not_exists_elim R) a)) b,
L2 : exists y, P a y := H1 a
in exists::elim L2 (fun (w : A) (H : P a w),
in exists_elim L2 (fun (w : A) (H : P a w),
absurd H ((L1 a) w))).

2
tests/lean/implicit1.lean
View file

@ -6,7 +6,7 @@ print forall a b, f a b > 0
variable g : Int -> Real -> Int
print forall a b, g a b > 0
print forall a b, g a (f a b) > 0
set::option pp::coercion true
set_option pp::coercion true
print forall a b, g a (f a b) > 0
print fun a, a + 1
print fun a b, a + b

2
tests/lean/implicit2.lean
View file

@ -8,6 +8,6 @@ check g 10 20 true
check let r : Real -> Real -> Real := g 10 20
in r
check g 10
set::option pp::implicit true
set_option pp::implicit true
check let r : Real -> Real -> Real := g 10 20
in r

4
tests/lean/implicit3.lean
View file

@ -5,7 +5,7 @@ variable f : Int -> Int -> Int
variable g : Int -> Int -> Int -> Int
notation 10 _ ++ _ : f
notation 10 _ ++ _ : g
set::option pp::implicit true
set::option pp::notation false
set_option pp::implicit true
set_option pp::notation false
print (10 ++ 20)
print (10 ++ 20) 10

4
tests/lean/implicit6.lean
View file

@ -4,8 +4,8 @@ infixl 65 + : f
print true + false
print 10 + 20
print 10 + (- 20)
set::option pp::notation false
set::option pp::coercion true
set_option pp::notation false
set_option pp::coercion true
print true + false
print 10 + 20
print 10 + (- 20)

4
tests/lean/implicit7.lean
View file

@ -4,9 +4,9 @@ notation 100 _ ; _ ; _ : f
notation 100 _ ; _ ; _ : g
check 10 ; true ; false
check 10 ; 10 ; true
set::option pp::notation false
set_option pp::notation false
check 10 ; true ; false
check 10 ; 10 ; true
set::option pp::implicit true
set_option pp::implicit true
check 10 ; true ; false
check 10 ; 10 ; true

16
tests/lean/induction1.lean
View file

@ -10,14 +10,14 @@ theorem Comm1 : ∀ n m, n + m = m + n
:= Induction
_ -- I use a placeholder because I do not want to write the P
(λ m, -- Base case
calc 0 + m = m : add::zerol m
... = m + 0 : symm (add::zeror m))
calc 0 + m = m : add_zerol m
... = m + 0 : symm (add_zeror m))
(λ n, -- Inductive case
λ (iH : ∀ m, n + m = m + n),
λ m,
calc n + 1 + m = (n + m) + 1 : add::succl n m
calc n + 1 + m = (n + m) + 1 : add_succl n m
... = (m + n) + 1 : { iH m }
... = m + (n + 1) : symm (add::succr m n))
... = m + (n + 1) : symm (add_succr m n))
-- indunction on m
@ -25,13 +25,13 @@ theorem Comm2 : ∀ n m, n + m = m + n
:= λ n,
Induction
_
(calc n + 0 = n : add::zeror n
... = 0 + n : symm (add::zerol n))
(calc n + 0 = n : add_zeror n
... = 0 + n : symm (add_zerol n))
(λ m,
λ (iH : n + m = m + n),
calc n + (m + 1) = (n + m) + 1 : add::succr n m
calc n + (m + 1) = (n + m) + 1 : add_succr n m
... = (m + n) + 1 : { iH }
... = (m + 1) + n : symm (add::succl m n))
... = (m + 1) + n : symm (add_succl m n))
print environment 1

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

@ -9,6 +9,6 @@ theorem Comm2 : ∀ n m : ℕ, n + m = m + n :=
λ n : ℕ,
Induction
(λ x : ℕ, n + x == x + n)
(Nat::add::zeror n ⋈ symm (Nat::add::zerol n))
(Nat::add_zeror n ⋈ symm (Nat::add_zerol n))
(λ (m : ℕ) (iH : n + m = m + n),
Nat::add::succr n m ⋈ subst (refl (n + m + 1)) iH ⋈ symm (Nat::add::succl m n))
Nat::add_succr n m ⋈ subst (refl (n + m + 1)) iH ⋈ symm (Nat::add_succl m n))

8
tests/lean/induction2.lean
View file

@ -10,9 +10,9 @@ theorem Comm1 : ∀ n m, n + m = m + n
:= Induction
_ -- I use a placeholder because I do not want to write the P
(λ m, -- Base case
calc 0 + m = m : add::zerol m
... = m + 0 : symm (add::zeror m))
calc 0 + m = m : add_zerol m
... = m + 0 : symm (add_zeror m))
(λ n iH m, -- Inductive case
calc n + 1 + m = (n + m) + 1 : add::succl n m
calc n + 1 + m = (n + m) + 1 : add_succl n m
... = (m + n) + 1 : { iH } -- Error is here
... = m + (n + 1) : symm (add::succr m n))
... = m + (n + 1) : symm (add_succr m n))

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

@ -9,6 +9,6 @@ Failed to solve
Induction
with arguments:
?M::3
λ m : ℕ, Nat::add::zerol m ⋈ symm (Nat::add::zeror m)
λ m : ℕ, Nat::add_zerol m ⋈ symm (Nat::add_zeror m)
λ (n : ℕ) (iH : ?M::3 n) (m : ℕ),
Nat::add::succl n m ⋈ subst (refl (n + m + 1)) iH ⋈ symm (Nat::add::succr m n)
Nat::add_succl n m ⋈ subst (refl (n + m + 1)) iH ⋈ symm (Nat::add_succr m n)

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

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

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

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

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

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

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

@ -2,5 +2,5 @@
Set: pp::unicode
Proved: T1
theorem T1 (A B : Bool) (assumption : A ∧ B) : B ∧ A :=
let lemma1 := and::eliml assumption, lemma2 := and::elimr assumption in and::intro 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

@ -12,5 +12,5 @@ a : Bool, b : Bool, H : b ⊢ b
## Proof state:
no goals
## Proved: T2
# theorem T2 (a b : Bool) (H : b) : a ∨ b := or::intror a H
# theorem T2 (a b : Bool) (H : b) : a ∨ b := or_intror a H
#

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

@ -1,5 +1,5 @@
(* import("tactic.lua") *)
theorem T1 (a b : Bool) : a → b → a /\ b.
apply and::intro.
apply and_intro.
exact.
done.

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

@ -1,6 +1,6 @@
(* import("tactic.lua") *)
set::option tactic::proof_state::goal_names true.
set_option tactic::proof_state::goal_names true.
theorem T (a : Bool) : a → a /\ a.
apply and::intro.
apply and_intro.
exact.
done.

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

@ -12,7 +12,7 @@ theorem T1 (A B : Bool) : A /\ B → B /\ A :=
conj_hyp.
exact.
done.
apply and::intro.
apply and_intro.
exact.
done.

2
tests/lean/let1.lean
View file

@ -6,5 +6,5 @@ check let a : Nat := 10 in a + 1
eval let a : Nat := 20 in a + 10
eval let a := 20 in a + 10
check let a : Int := 20 in a + 10
set::option pp::coercion true
set_option pp::coercion true
print let a : Int := 20 in a + 10

4
tests/lean/let2.lean
View file

@ -2,8 +2,8 @@
theorem simple (p q r : Bool) : (p → q) ∧ (q → r) → p → r :=
λ H_pq_qr H_p,
let P_pq : (p → q) := and::eliml H_pq_qr,
P_qr : (q → r) := and::elimr H_pq_qr,
let P_pq : (p → q) := and_eliml H_pq_qr,
P_qr : (q → r) := and_elimr H_pq_qr,
P_q : q := P_pq H_p
in P_qr P_q

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

@ -2,4 +2,4 @@
Set: pp::unicode
Proved: simple
theorem simple (p q r : Bool) (H_pq_qr : (p → q) ∧ (q → r)) (H_p : p) : r :=
let P_pq : p → q := and::eliml H_pq_qr, P_qr : q → r := and::elimr H_pq_qr, P_q : q := P_pq H_p in P_qr P_q
let P_pq : p → q := and_eliml H_pq_qr, P_qr : q → r := and_elimr H_pq_qr, P_q : q := P_pq H_p in P_qr P_q

4
tests/lean/let3.lean
View file

@ -2,8 +2,8 @@ import Int.
variable magic : forall (H : Bool), H
set::option pp::notation false
set::option pp::coercion true
set_option pp::notation false
set_option pp::coercion true
print let a : Int := 1,
H : a > 0 := magic (a > 0)
in H

2
tests/lean/let4.lean
View file

@ -41,7 +41,7 @@ let a := 10,
v2 : vector Int a := v1
in v2
set::option pp::coercion true
set_option pp::coercion true
print
let a := 10,

2
tests/lean/lua6.lean
View file

@ -1,6 +1,6 @@
import Int.
variable x : Int
set::option pp::notation false
set_option pp::notation false
(*
print(get_options())
*)

8
tests/lean/norm_bug1.lean
View file

@ -1,12 +1,12 @@
import cast
set::option pp::colors false
set_option pp::colors false
check fun (A A': TypeM)
(a : A)
(b : A')
(L2 : A' == A),
let b' : A := cast L2 b,
L3 : b == b' := cast::eq L2 b
L3 : b == b' := cast_eq L2 b
in L3
check fun (A A': TypeM)
@ -18,10 +18,10 @@ check fun (A A': TypeM)
(b : A')
(H2 : f == g)
(H3 : a == b),
let L1 : A == A' := type::eq H3,
let L1 : A == A' := type_eq H3,
L2 : A' == A := symm L1,
b' : A := cast L2 b,
L3 : b == b' := cast::eq L2 b,
L3 : b == b' := cast_eq L2 b,
L4 : a == b' := htrans H3 L3,
L5 : f a == f b' := congr2 f L4
in L5

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

@ -2,7 +2,7 @@
Set: pp::unicode
Imported 'cast'
Set: pp::colors
λ (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), let b' : A := cast L2 b, L3 : b == b' := cast::eq L2 b in L3 :
λ (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), 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)
(B : A → TypeM)
@ -13,10 +13,10 @@
(b : A')
(H2 : f == g)
(H3 : a == b),
let L1 : A == A' := type::eq H3,
let L1 : A == A' := type_eq H3,
L2 : A' == A := symm L1,
b' : A := cast L2 b,
L3 : b == b' := cast::eq L2 b,
L3 : b == b' := cast_eq L2 b,
L4 : a == b' := htrans H3 L3,
L5 : f a == f b' := congr2 f L4
in L5 :
@ -29,4 +29,4 @@
(b : A')
(H2 : f == g)
(H3 : a == b),
f a == f (cast (symm (type::eq H3)) b)
f a == f (cast (symm (type_eq H3)) b)

6
tests/lean/norm_tac.lean
View file

@ -1,8 +1,8 @@
import Int
import tactic
set::option pp::implicit true
set::option pp::coercion true
set::option pp::notation false
set_option pp::implicit true
set_option pp::coercion true
set_option pp::notation false
variable vector (A : Type) (sz : Nat) : Type
variable read {A : Type} {sz : Nat} (v : vector A sz) (i : Nat) (H : i < sz) : A
variable V1 : vector Int 10

2
tests/lean/overload1.lean
View file

@ -4,7 +4,7 @@ variable g : N -> N -> N
infixl 10 ++ : f
infixl 10 ++ : g
print true ++ false ++ true
set::option lean::pp::notation false
set_option lean::pp::notation false
print true ++ false ++ true
variable a : N
variable b : N

4
tests/lean/overload2.lean
View file

@ -10,8 +10,8 @@ coercion t2r
variable f : T -> R -> T
variable a : T
variable b : R
set::option lean::pp::coercion true
set::option lean::pp::notation false
set_option lean::pp::coercion true
set_option lean::pp::notation false
print f a b
print f b a
variable g : R -> T -> R

6
tests/lean/push.lean
View file

@ -6,7 +6,7 @@ scope
variables a b c : Int
variable f : Int -> Int
eval f a
pop::scope
pop_scope
eval f a -- should produce an error
@ -15,8 +15,8 @@ print environment 1
scope
infixl 100 ++ : Int::add
check 10 ++ 20
pop::scope
pop_scope
check 10 ++ 20 -- should produce an error
pop::scope -- should produce an error
pop_scope -- should produce an error

2
tests/lean/refute1.lean
View file

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

2
tests/lean/showenv.l
View file

@ -1,3 +1,3 @@
set::option pp::colors false
set_option pp::colors false
print "===BEGIN ENVIRONMENT==="
print environment

6
tests/lean/slow/config.lean
View file

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

4
tests/lean/slow/deep.lean
View file

@ -3,6 +3,6 @@ definition f1 (f : Int -> Int) (x : Int) : Int := f (f (f (f x)))
definition f2 (f : Int -> Int) (x : Int) : Int := f1 (f1 (f1 (f1 f))) x
definition f3 (f : Int -> Int) (x : Int) : Int := f1 (f2 (f2 f)) x
variable f : Int -> Int.
set::option pp::width 80.
set::option lean::pp::max_depth 2000.
set_option pp::width 80.
set_option lean::pp::max_depth 2000.
eval f3 f 0.

6
tests/lean/subst.lean
View file

@ -4,7 +4,7 @@ variable n : Nat
axiom H1 : a + a + a = 10
axiom H2 : a = n
theorem T : a + n + a = 10 := subst H1 H2
set::option pp::coercion true
set::option pp::notation false
set::option pp::implicit true
set_option pp::coercion true
set_option pp::notation false
set_option pp::implicit true
print environment 1.

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

@ -3,4 +3,4 @@
Assumed: p
Assumed: q
Assumed: r
theorem T1 (H : p) (H::1 : q) : p ∧ q := and::intro H H::1
theorem T1 (H : p) (H::1 : q) : p ∧ q := and_intro H H::1

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