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

chore(examples/lean): remove old examples

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-15 16:06:42 -07:00
parent 391b2fe739
commit 847d8b8c47
20 changed files with 0 additions and 1809 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

145
examples/lean/abelian.lean
View file

@ -1,145 +0,0 @@
import macros
definition associative {A : (Type U)} (f : A → A → A) := ∀ x y z, f (f x y) z = f x (f y z)
definition is_identity {A : (Type U)} (f : A → A → A) (id : A) := ∀ x, f x id = x
definition inverse_ex {A : (Type U)} (f : A → A → A) (id : A) := ∀ x, ∃ y, f x y = id
universe s ≥ 1
definition group := sig A : (Type s), sig mul : A → A → A, sig one : A, (associative mul) # (is_identity mul one) # (inverse_ex mul one)
definition to_group (A : (Type s)) (mul : A → A → A) (one : A) (H1 : associative mul) (H2 : is_identity mul one) (H3 : inverse_ex mul one) : group
:= pair A (pair mul (pair one (pair H1 (pair H2 H3))))
-- The following definitions can be generated automatically.
definition carrier (g : group) := proj1 g
definition G_mul {g : group} : carrier g → carrier g → carrier g
:= proj1 (proj2 g)
infixl 70 * : G_mul
definition one {g : group} : carrier g
:= proj1 (proj2 (proj2 g))
theorem G_assoc {g : group} (x y z : carrier g) : (x * y) * z = x * (y * z)
:= (proj1 (proj2 (proj2 (proj2 g)))) x y z
theorem G_id {g : group} (x : carrier g) : x * one = x
:= (proj1 (proj2 (proj2 (proj2 (proj2 g))))) x
theorem G_inv {g : group} (x : carrier g) : ∃ y, x * y = one
:= (proj2 (proj2 (proj2 (proj2 (proj2 g))))) x
set_opaque group true
set_opaque carrier true
set_opaque G_mul true
set_opaque one true
-- First example: the pairwise product of two groups is a group
definition product (g1 g2 : group) : group
:= let S := carrier g1 # carrier g2,
-- It would be nice to be able to define local notation, and write _*_ instead of f
f := λ x y, pair (proj1 x * proj1 y) (proj2 x * proj2 y),
o := pair one one -- this is actually (pair (@one g1) (@one g2))
in have assoc : associative f,
-- The elaborator failed to infer the type of the pairs.
-- I had to annotate the pairs with their types.
from take x y z : S, -- We don't really need to provide S, but it will make the elaborator to work much harder
-- since * is an overloaded operator, we also have * as notation for Nat::mul in the context.
calc f (f x y) z = (pair ((proj1 x * proj1 y) * proj1 z) ((proj2 x * proj2 y) * proj2 z) : S) : refl (f (f x y) z)
... = (pair (proj1 x * (proj1 y * proj1 z)) ((proj2 x * proj2 y) * proj2 z) : S) : { G_assoc (proj1 x) (proj1 y) (proj1 z) }
... = (pair (proj1 x * (proj1 y * proj1 z)) (proj2 x * (proj2 y * proj2 z)) : S) : { G_assoc (proj2 x) (proj2 y) (proj2 z) }
... = f x (f y z) : refl (f x (f y z)),
have id : is_identity f o,
from take x : S,
calc f x o = (pair (proj1 x * one) (proj2 x * one) : S) : refl (f x o)
... = (pair (proj1 x) (proj2 x * one) : S) : { G_id (proj1 x) }
... = (pair (proj1 x) (proj2 x) : S) : { G_id (proj2 x) }
... = x : pair_proj_eq x,
have inv : inverse_ex f o,
from take x : S,
obtain (y1 : carrier g1) (Hy1 : proj1 x * y1 = one), from G_inv (proj1 x),
obtain (y2 : carrier g2) (Hy2 : proj2 x * y2 = one), from G_inv (proj2 x),
show ∃ y, f x y = o,
from exists_intro (pair y1 y2 : S)
(calc f x (pair y1 y2 : S) = (pair (proj1 x * y1) (proj2 x * y2) : S) : refl (f x (pair y1 y2 : S))
... = (pair one (proj2 x * y2) : S) : { Hy1 }
... = (pair one one : S) : { Hy2 }
... = o : refl o),
to_group S f o assoc id inv
set_opaque product true
-- It would be nice to be able to write x.first and x.second instead of (proj1 x) and (proj2 x)
-- Remark: * is overloaded since Lean loads Nat.lean by default.
-- The type errors related to * are quite cryptic because of that
-- Use 'star' for creating products
infixr 50 ⋆ : product
-- It would be nice to be able to write (p1 p2 : g1 ⋆ g2 ⋆ g3)
check λ (g1 g2 g3 : group) (p1 p2 : carrier (g1 ⋆ g2 ⋆ g3)), p1 * p2 = p2 * p1
theorem group_inhab (g : group) : inhabited (carrier g)
:= inhabited_intro (@one g)
definition inv {g : group} (a : carrier g) : carrier g
:= ε (group_inhab g) (λ x : carrier g, a * x = one)
theorem G_idl {g : group} (x : carrier g) : x * one = x
:= G_id x
theorem G_invl {g : group} (x : carrier g) : x * inv x = one
:= obtain (y : carrier g) (Hy : x * y = one), from G_inv x,
eps_ax (group_inhab g) y Hy
set_opaque inv true
theorem G_inv_aux {g : group} (x : carrier g) : inv x = (inv x * x) * inv x
:= symm (calc (inv x * x) * inv x = inv x * (x * inv x) : G_assoc (inv x) x (inv x)
... = inv x * one : { G_invl x }
... = inv x : G_idl (inv x))
theorem G_invr {g : group} (x : carrier g) : inv x * x = one
:= calc inv x * x = (inv x * x) * one : symm (G_idl (inv x * x))
... = (inv x * x) * (inv x * inv (inv x)) : { symm (G_invl (inv x)) }
... = ((inv x * x) * inv x) * inv (inv x) : symm (G_assoc (inv x * x) (inv x) (inv (inv x)))
... = (inv x * (x * inv x)) * inv (inv x) : { G_assoc (inv x) x (inv x) }
... = (inv x * one) * inv (inv x) : { G_invl x }
... = (inv x) * inv (inv x) : { G_idl (inv x) }
... = one : G_invl (inv x)
theorem G_idr {g : group} (x : carrier g) : one * x = x
:= calc one * x = (x * inv x) * x : { symm (G_invl x) }
... = x * (inv x * x) : G_assoc x (inv x) x
... = x * one : { G_invr x }
... = x : G_idl x
theorem G_inv_inv {g : group} (x : carrier g) : inv (inv x) = x
:= calc inv (inv x) = inv (inv x) * one : symm (G_idl (inv (inv x)))
... = inv (inv x) * (inv x * x) : { symm (G_invr x) }
... = (inv (inv x) * inv x) * x : symm (G_assoc (inv (inv x)) (inv x) x)
... = one * x : { G_invr (inv x) }
... = x : G_idr x
definition commutative {A : (Type U)} (f : A → A → A) := ∀ x y, f x y = f y x
definition abelian_group := sig g : group, commutative (@G_mul g)
definition ab_to_g (ag : abelian_group) : group
:= proj1 ag
-- Coercions currently only work with opaque types
-- We must first define "extract" the information we want, and then
-- mark abelian_group as opaque
definition AG_comm {g : abelian_group} (x y : carrier (ab_to_g g)) : x * y = y * x
:= (proj2 g) x y
set_opaque abelian_group true
set_opaque ab_to_g true
set_opaque AG_comm true
coercion ab_to_g
-- Now, we can use abelian groups where groups are expected.
theorem AG_left_comm {g : abelian_group} (x y z : carrier g) : x * (y * z) = y * (x * z)
:= calc x * (y * z) = (x * y) * z : symm (G_assoc x y z)
... = (y * x) * z : { AG_comm x y }
... = y * (x * z) : G_assoc y x z

83
examples/lean/alg.lean
View file

@ -1,83 +0,0 @@
import macros
definition associative {A : (Type U)} (f : A → A → A) := ∀ x y z, f (f x y) z = f x (f y z)
definition commutative {A : (Type U)} (f : A → A → A) := ∀ x y, f x y = f y x
definition is_identity {A : (Type U)} (f : A → A → A) (id : A) := ∀ x, f x id = x
definition inverse_ex {A : (Type U)} (f : A → A → A) (id : A) := ∀ x, ∃ y, f x y = id
definition struct := Type
definition carrier (s : struct) := s
definition mul_struct
:= sig s : struct, carrier s → carrier s → carrier s
definition mul_to_s (m : mul_struct) : struct := proj1 m
coercion mul_to_s
definition mul {m : mul_struct} : carrier m → carrier m → carrier m
:= proj2 m
infixl 70 * : mul
definition semi_group
:= sig m : mul_struct, associative (@mul m)
definition sg_to_mul (sg : semi_group) : mul_struct := proj1 sg
definition sg_to_s (sg : semi_group) : struct := mul_to_s (sg_to_mul sg)
coercion sg_to_s
coercion sg_to_mul
theorem sg_assoc {m : semi_group} (x y z : carrier m) : (x * y) * z = x * (y * z)
:= proj2 m x y z
definition monoid
:= sig sg : semi_group, sig id : carrier sg, is_identity (@mul sg) id
definition monoid_to_sg (m : monoid) : semi_group := proj1 m
definition monoid_to_mul (m : monoid) : mul_struct := sg_to_mul (monoid_to_sg m)
definition monoid_to_s (m : monoid) : struct := mul_to_s (monoid_to_mul m)
coercion monoid_to_sg
coercion monoid_to_mul
coercion monoid_to_s
definition one {m : monoid} : carrier m
:= proj1 (proj2 m)
theorem monoid_id {m : monoid} (x : carrier m) : x * one = x
:= proj2 (proj2 m) x
definition group
:= sig m : monoid, inverse_ex (@mul m) (@one m)
definition group_to_monoid (g : group) : monoid := proj1 g
definition group_to_sg (g : group) : semi_group := monoid_to_sg (group_to_monoid g)
definition group_to_mul (g : group) : mul_struct := sg_to_mul (group_to_sg g)
definition group_to_s (g : group) : struct := mul_to_s (group_to_mul g)
coercion group_to_monoid
coercion group_to_sg
coercion group_to_mul
coercion group_to_s
theorem group_inv {g : group} (x : carrier g) : ∃ y, x * y = one
:= proj2 g x
definition abelian_group
:= sig g : group, commutative (@mul g)
definition abelian_to_group (ag : abelian_group) : group := proj1 ag
definition abelian_to_monoid (ag : abelian_group) : monoid := group_to_monoid (abelian_to_group ag)
definition abelian_to_sg (ag : abelian_group) : semi_group := monoid_to_sg (abelian_to_monoid ag)
definition abelian_to_mul (ag : abelian_group) : mul_struct := sg_to_mul (abelian_to_sg ag)
definition abelian_to_s (ag : abelian_group) : struct := mul_to_s (abelian_to_mul ag)
coercion abelian_to_group
coercion abelian_to_monoid
coercion abelian_to_sg
coercion abelian_to_mul
coercion abelian_to_s
theorem abelian_comm {ag : abelian_group} (x y : carrier ag) : x * y = y * x
:= proj2 ag x y
theorem abelian_left_comm {ag : abelian_group} (x y z : carrier ag) : x * (y * z) = y * (x * z)
:= calc x * (y * z) = (x * y) * z : symm (sg_assoc x y z)
... = (y * x) * z : { abelian_comm x y }
... = y * (x * z) : sg_assoc y x z

99
examples/lean/dep_if.lean
View file

@ -1,99 +0,0 @@
import macros
import tactic
-- "Dependent" if-then-else (dep_if c t e)
-- The then-branch t gets a proof for c, and the else-branch e gets a proof for ¬ c
-- We also prove that
-- 1) given H : c, (dep_if c t e) = t H
-- 2) given H : ¬ c, (dep_if c t e) = e H
-- We define the "dependent" if-then-else using Hilbert's choice operator ε.
-- Note that ε is only applicable to non-empty types. Thus, we first
-- prove the following auxiliary theorem.
theorem inhabited_resolve {A : (Type U)} {c : Bool} (t : c → A) (e : ¬ c → A) : inhabited A
:= or_elim (em c)
(λ Hc, inhabited_range (inhabited_intro t) Hc)
(λ Hnc, inhabited_range (inhabited_intro e) Hnc)
-- The actual definition
definition dep_if {A : (Type U)} (c : Bool) (t : c → A) (e : ¬ c → A) : A
:= ε (inhabited_resolve t e) (λ r, (∀ Hc : c, r = t Hc) ∧ (∀ Hnc : ¬ c, r = e Hnc))
theorem then_simp (A : (Type U)) (c : Bool) (r : A) (t : c → A) (e : ¬ c → A) (H : c)
: (∀ Hc : c, r = t Hc) ∧ (∀ Hnc : ¬ c, r = e Hnc) ↔ r = t H
:= let s1 : (∀ Hc : c, r = t Hc) ↔ r = t H
:= iff_intro
(assume Hl : (∀ Hc : c, r = t Hc),
Hl H)
(assume Hr : r = t H,
λ Hc : c, subst Hr (proof_irrel H Hc)),
s2 : (∀ Hnc : ¬ c, r = e Hnc) ↔ true
:= eqt_intro (λ Hnc : ¬ c, absurd_elim (r = e Hnc) H Hnc)
in by simp
-- Given H : c, (dep_if c t e) = t H
theorem dep_if_elim_then {A : (Type U)} (c : Bool) (t : c → A) (e : ¬ c → A) (H : c) : dep_if c t e = t H
:= let s1 : (λ r, (∀ Hc : c, r = t Hc) ∧ (∀ Hnc : ¬ c, r = e Hnc)) = (λ r, r = t H)
:= funext (λ r, then_simp A c r t e H)
in calc dep_if c t e = ε (inhabited_resolve t e) (λ r, (∀ Hc : c, r = t Hc) ∧ (∀ Hnc : ¬ c, r = e Hnc)) : refl (dep_if c t e)
... = ε (inhabited_resolve t e) (λ r, r = t H) : { s1 }
... = t H : eps_singleton (inhabited_resolve t e) (t H)
theorem dep_if_true {A : (Type U)} (t : true → A) (e : ¬ true → A) : dep_if true t e = t trivial
:= dep_if_elim_then true t e trivial
theorem else_simp (A : (Type U)) (c : Bool) (r : A) (t : c → A) (e : ¬ c → A) (H : ¬ c)
: (∀ Hc : c, r = t Hc) ∧ (∀ Hnc : ¬ c, r = e Hnc) ↔ r = e H
:= let s1 : (∀ Hc : c, r = t Hc) ↔ true
:= eqt_intro (λ Hc : c, absurd_elim (r = t Hc) Hc H),
s2 : (∀ Hnc : ¬ c, r = e Hnc) ↔ r = e H
:= iff_intro
(assume Hl : (∀ Hnc : ¬ c, r = e Hnc),
Hl H)
(assume Hr : r = e H,
λ Hnc : ¬ c, subst Hr (proof_irrel H Hnc))
in by simp
-- Given H : ¬ c, (dep_if c t e) = e H
theorem dep_if_elim_else {A : (Type U)} (c : Bool) (t : c → A) (e : ¬ c → A) (H : ¬ c) : dep_if c t e = e H
:= let s1 : (λ r, (∀ Hc : c, r = t Hc) ∧ (∀ Hnc : ¬ c, r = e Hnc)) = (λ r, r = e H)
:= funext (λ r, else_simp A c r t e H)
in calc dep_if c t e = ε (inhabited_resolve t e) (λ r, (∀ Hc : c, r = t Hc) ∧ (∀ Hnc : ¬ c, r = e Hnc)) : refl (dep_if c t e)
... = ε (inhabited_resolve t e) (λ r, r = e H) : { s1 }
... = e H : eps_singleton (inhabited_resolve t e) (e H)
theorem dep_if_false {A : (Type U)} (t : false → A) (e : ¬ false → A) : dep_if false t e = e not_false_trivial
:= dep_if_elim_else false t e not_false_trivial
set_option simplifier::heq true -- enable heterogeneous equality support
universe M >= 1
theorem dep_if_congr {A : (Type M)} (c1 c2 : Bool)
(t1 : c1 → A) (t2 : c2 → A)
(e1 : ¬ c1 → A) (e2 : ¬ c2 → A)
(Hc : c1 = c2)
(Ht : t1 = cast (by simp) t2)
(He : e1 = cast (by simp) e2)
: dep_if c1 t1 e1 = dep_if c2 t2 e2
:= by simp
scope
-- Here is an example where dep_if is useful
-- Suppose we have a (div s t H) where H is a proof for t ≠ 0
variable div (s : Nat) (t : Nat) (H : t ≠ 0) : Nat
-- Now, we want to define a function that
-- returns 0 if x = 0
-- and div 10 x _ otherwise
-- We can't use the standard if-the-else, because we don't have a way to synthesize the proof for x ≠ 0
check λ x, dep_if (x = 0) (λ H, 0) (λ H : ¬ x = 0, div 10 x H)
pop_scope
-- If the dependent then/else branches do not use the proofs Hc : c and Hn : ¬ c, then we
-- can reduce the dependent-if to a regular if
theorem dep_if_if {A : (Type U)} (c : Bool) (t e : A) : dep_if c (λ Hc, t) (λ Hn, e) = if c then t else e
:= or_elim (em c)
(assume Hc : c, calc dep_if c (λ Hc, t) (λ Hn, e) = (λ Hc, t) Hc : dep_if_elim_then _ _ _ Hc
... = if c then t else e : by simp)
(assume Hn : ¬ c, calc dep_if c (λ Hc, t) (λ Hn, e) = (λ Hn, e) Hn : dep_if_elim_else _ _ _ Hn
... = if c then t else e : by simp)

72
examples/lean/even.lean
View file

@ -1,72 +0,0 @@
import macros
using Nat
-- In this example, we prove two simple theorems about even/odd numbers.
-- First, we define the predicates even and odd.
definition even (a : Nat) := ∃ b, a = 2*b
definition odd (a : Nat) := ∃ b, a = 2*b + 1
-- Prove that the sum of two even numbers is even.
--
-- Notes: we use the macro
-- obtain [bindings] ',' 'from' [expr]_1 ',' [expr]_2
--
-- It is syntax sugar for existential elimination.
-- It expands to
--
-- exists_elim [expr]_1 (fun [binding], [expr]_2)
--
-- It is defined in the file macros.lua.
--
-- We also use the calculational proof style.
-- See doc/lean/calc.md for more information.
--
-- We use the first two obtain-expressions to extract the
-- 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
-- fact that 'a' and 'b' are even.
--
-- We use a calculational proof 'calc' expression to derive
-- 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)
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)
(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.
-- Lean can infer them automatically.
--
-- refl is the reflexivity proof. (refl a) is a proof that two
-- definitionally equal terms are indeed equal.
-- "definitionally equal" means that they have the same normal form.
-- We can also view it as "Proof by computation".
-- The normal form of (1+1), and 2*1 is 2.
--
-- Another remark: '2*w + 1 + 1' is not definitionally equal to '2*w + 2*1'.
-- The gotcha is that '2*w + 1 + 1' is actually '(2*w + 1) + 1' since +
-- is left associative. Moreover, Lean normalizer does not use
-- 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)
(calc a + 1 = 2*w + 1 + 1 : { Hw }
... = 2*w + (1 + 1) : add_assoc _ _ _
... = 2*w + 2*1 : refl _
... = 2*(w + 1) : symm (distributer _ _ _))
-- The following command displays the proof object produced by Lean after
-- expanding macros, and infering implicit/missing arguments.
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
print environment 2
-- As an exercise, prove that the sum of two odd numbers is even,
-- and other similar theorems.

35
examples/lean/ex1.lean
View file

@ -1,35 +0,0 @@
variable N : Type
variable h : N -> N -> N
-- 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) :=
congr (congr (refl h) H1) H2
-- Declare some variables
variable a : N
variable b : N
variable c : N
variable d : N
variable e : N
-- Add axioms stating facts about these variables
axiom H1 : (a = b ∧ b = c) ∨ (d = c ∧ a = d)
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 (trans (and_eliml C1) (and_elimr C1)) H2)
(λ C2, congrh (trans (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)) :=
congrh (refl a) T1
-- Display the last two objects (i.e., theorems) added to the environment
print environment 2
-- print implicit arguments
set_option lean::pp::implicit true
set_option pp::width 150
print environment 2

16
examples/lean/ex2.lean
View file

@ -1,16 +0,0 @@
import macros.
theorem simple (p q r : Bool) : (p → q) ∧ (q → r) → p → r
:= assume H_pq_qr H_p,
let P_pq := and_eliml H_pq_qr,
P_qr := and_elimr H_pq_qr
in P_qr (P_pq H_p)
set_option pp::implicit true.
print environment 1.
theorem simple2 (a b c : Bool) : (a → b → c) → (a → b) → a → c
:= assume H_abc H_ab H_a,
(H_abc H_a) (H_ab H_a)
print environment 1.

28
examples/lean/ex3.lean
View file

@ -1,28 +0,0 @@
import macros.
theorem my_and_comm (a b : Bool) : (a ∧ b) → (b ∧ a)
:= assume H_ab, and_intro (and_elimr H_ab) (and_eliml H_ab).
theorem my_or_comm (a b : Bool) : (a ∨ b) → (b ∨ a)
:= assume H_ab,
or_elim H_ab
(λ H_a, or_intror b H_a)
(λ H_b, or_introl H_b a).
-- (em a) is the excluded middle a ∨ ¬a
-- (mt H H_na) is Modus Tollens with
-- H : (a → b) → a)
-- H_na : ¬a
-- produces
-- ¬(a → b)
--
-- not_imp_eliml applied to
-- (MT H H_na) : ¬(a → b)
-- produces
-- a
theorem pierce (a b : Bool) : ((a → b) → a) → a
:= assume H, or_elim (em a)
(λ H_a, H_a)
(λ H_na, not_imp_eliml (mt H H_na)).
print environment 3.

5
examples/lean/ex4.lean
View file

@ -1,5 +0,0 @@
import Int
import tactic
set_option simplifier::unfold true -- allow the simplifier to unfold definitions
definition a : Nat := 10
theorem T1 : a > 0 := (by simp)

34
examples/lean/ex5.lean
View file

@ -1,34 +0,0 @@
import macros
scope
theorem ReflIf (A : Type)
(R : A → A → Bool)
(Symm : ∀ x y, R x y → R y x)
(Trans : ∀ x y z, R x y → R y z → R x z)
(Linked : ∀ x, ∃ y, R x y)
:
∀ x, R x x :=
take x,
obtain (w : A) (H : R x w), from (Linked x),
let L1 : R w x := Symm x w H
in Trans x w x H L1
pop_scope
scope
-- Same example again.
variable A : Type
variable R : A → A → Bool
axiom Symm {x y : A} : R x y → R y x
axiom Trans {x y z : A} : R x y → R y z → R x z
axiom Linked (x : A) : ∃ y, R x y
theorem ReflIf (x : A) : R x x :=
obtain (w : A) (H : R x w), from (Linked x),
let L1 : R w x := Symm H
in Trans H L1
end
-- Display the last two theorems
print environment 2

111
examples/lean/group.lean
View file

@ -1,111 +0,0 @@
import macros
definition associative {A : (Type U)} (f : A → A → A) := ∀ x y z, f (f x y) z = f x (f y z)
definition is_identity {A : (Type U)} (f : A → A → A) (id : A) := ∀ x, f x id = x
definition inverse_ex {A : (Type U)} (f : A → A → A) (id : A) := ∀ x, ∃ y, f x y = id
universe s ≥ 1
definition group := sig A : (Type s), sig mul : A → A → A, sig one : A, (associative mul) # (is_identity mul one) # (inverse_ex mul one)
definition to_group (A : (Type s)) (mul : A → A → A) (one : A) (H1 : associative mul) (H2 : is_identity mul one) (H3 : inverse_ex mul one) : group
:= pair A (pair mul (pair one (pair H1 (pair H2 H3))))
-- The following definitions can be generated automatically.
definition carrier (g : group) := proj1 g
definition G_mul {g : group} : carrier g → carrier g → carrier g
:= proj1 (proj2 g)
infixl 70 * : G_mul
definition one {g : group} : carrier g
:= proj1 (proj2 (proj2 g))
theorem G_assoc {g : group} (x y z : carrier g) : (x * y) * z = x * (y * z)
:= (proj1 (proj2 (proj2 (proj2 g)))) x y z
theorem G_id {g : group} (x : carrier g) : x * one = x
:= (proj1 (proj2 (proj2 (proj2 (proj2 g))))) x
theorem G_inv {g : group} (x : carrier g) : ∃ y, x * y = one
:= (proj2 (proj2 (proj2 (proj2 (proj2 g))))) x
-- First example: the pairwise product of two groups is a group
definition product (g1 g2 : group) : group
:= let S := carrier g1 # carrier g2,
-- It would be nice to be able to define local notation, and write _*_ instead of f
f := λ x y, pair (proj1 x * proj1 y) (proj2 x * proj2 y),
o := pair one one -- this is actually (pair (@one g1) (@one g2))
in have assoc : associative f,
-- The elaborator failed to infer the type of the pairs.
-- I had to annotate the pairs with their types.
from take x y z : S, -- We don't really need to provide S, but it will make the elaborator to work much harder
-- since * is an overloaded operator, we also have * as notation for Nat::mul in the context.
calc f (f x y) z = (pair ((proj1 x * proj1 y) * proj1 z) ((proj2 x * proj2 y) * proj2 z) : S) : refl (f (f x y) z)
... = (pair (proj1 x * (proj1 y * proj1 z)) ((proj2 x * proj2 y) * proj2 z) : S) : { G_assoc (proj1 x) (proj1 y) (proj1 z) }
... = (pair (proj1 x * (proj1 y * proj1 z)) (proj2 x * (proj2 y * proj2 z)) : S) : { G_assoc (proj2 x) (proj2 y) (proj2 z) }
... = f x (f y z) : refl (f x (f y z)),
have id : is_identity f o,
from take x : S,
calc f x o = (pair (proj1 x * one) (proj2 x * one) : S) : refl (f x o)
... = (pair (proj1 x) (proj2 x * one) : S) : { G_id (proj1 x) }
... = (pair (proj1 x) (proj2 x) : S) : { G_id (proj2 x) }
... = x : pair_proj_eq x,
have inv : inverse_ex f o,
from take x : S,
obtain (y1 : carrier g1) (Hy1 : proj1 x * y1 = one), from G_inv (proj1 x),
obtain (y2 : carrier g2) (Hy2 : proj2 x * y2 = one), from G_inv (proj2 x),
show ∃ y, f x y = o,
from exists_intro (pair y1 y2 : S)
(calc f x (pair y1 y2 : S) = (pair (proj1 x * y1) (proj2 x * y2) : S) : refl (f x (pair y1 y2 : S))
... = (pair one (proj2 x * y2) : S) : { Hy1 }
... = (pair one one : S) : { Hy2 }
... = o : refl o),
to_group S f o assoc id inv
-- It would be nice to be able to write x.first and x.second instead of (proj1 x) and (proj2 x)
-- Remark: * is overloaded since Lean loads Nat.lean by default.
-- The type errors related to * are quite cryptic because of that
-- Use 'star' for creating products
infixr 50 ⋆ : product
-- It would be nice to be able to write (p1 p2 : g1 ⋆ g2 ⋆ g3)
check λ (g1 g2 g3 : group) (p1 p2 : carrier (g1 ⋆ g2 ⋆ g3)), p1 * p2 = p2 * p1
theorem group_inhab (g : group) : inhabited (carrier g)
:= inhabited_intro (@one g)
definition inv {g : group} (a : carrier g) : carrier g
:= ε (group_inhab g) (λ x : carrier g, a * x = one)
theorem G_idl {g : group} (x : carrier g) : x * one = x
:= G_id x
theorem G_invl {g : group} (x : carrier g) : x * inv x = one
:= obtain (y : carrier g) (Hy : x * y = one), from G_inv x,
eps_ax (group_inhab g) y Hy
theorem G_inv_aux {g : group} (x : carrier g) : inv x = (inv x * x) * inv x
:= symm (calc (inv x * x) * inv x = inv x * (x * inv x) : G_assoc (inv x) x (inv x)
... = inv x * one : { G_invl x }
... = inv x : G_idl (inv x))
theorem G_invr {g : group} (x : carrier g) : inv x * x = one
:= calc inv x * x = (inv x * x) * one : symm (G_idl (inv x * x))
... = (inv x * x) * (inv x * inv (inv x)) : { symm (G_invl (inv x)) }
... = ((inv x * x) * inv x) * inv (inv x) : symm (G_assoc (inv x * x) (inv x) (inv (inv x)))
... = (inv x * (x * inv x)) * inv (inv x) : { G_assoc (inv x) x (inv x) }
... = (inv x * one) * inv (inv x) : { G_invl x }
... = (inv x) * inv (inv x) : { G_idl (inv x) }
... = one : G_invl (inv x)
theorem G_idr {g : group} (x : carrier g) : one * x = x
:= calc one * x = (x * inv x) * x : { symm (G_invl x) }
... = x * (inv x * x) : G_assoc x (inv x) x
... = x * one : { G_invr x }
... = x : G_idl x
theorem G_inv_inv {g : group} (x : carrier g) : inv (inv x) = x
:= calc inv (inv x) = inv (inv x) * one : symm (G_idl (inv (inv x)))
... = inv (inv x) * (inv x * x) : { symm (G_invr x) }
... = (inv (inv x) * inv x) * x : symm (G_assoc (inv (inv x)) (inv x) x)
... = one * x : { G_invr (inv x) }
... = x : G_idr x

106
examples/lean/opaque_pairs.lean
View file

@ -1,106 +0,0 @@
import macros tactic
variable Sigma {A : (Type 1)} (B : A → (Type 1)) : (Type 1)
variable Pair {A : (Type 1)} {B : A → (Type 1)} (a : A) (b : B a) : Sigma B
variable Fst {A : (Type 1)} {B : A → (Type 1)} (p : Sigma B) : A
variable Snd {A : (Type 1)} {B : A → (Type 1)} (p : Sigma B) : B (Fst p)
axiom FstAx {A : (Type 1)} {B : A → (Type 1)} (a : A) (b : B a) : @Fst A B (Pair a b) = a
axiom SndAx {A : (Type 1)} {B : A → (Type 1)} (a : A) (b : B a) : @Snd A B (Pair a b) == b
scope
-- Remark: A1 a1 A2 a2 A3 a3 A3 a4 are parameters for the definitions and theorems in this scope.
variable A1 : (Type 1)
variable a1 : A1
variable A2 : A1 → (Type 1)
variable a2 : A2 a1
variable A3 : ∀ a1 : A1, A2 a1 → (Type 1)
variable a3 : A3 a1 a2
variable A4 : ∀ (a1 : A1) (a2 : A2 a1), A3 a1 a2 → (Type 1)
variable a4 : A4 a1 a2 a3
-- Pair type parameterized by a1 and a2
definition A1A2_tuple_ty (a1 : A1) (a2 : A2 a1) : (Type 1)
:= @Sigma (A3 a1 a2) (A4 a1 a2)
-- Pair a3 a4
definition tuple_34 : A1A2_tuple_ty a1 a2
:= @Pair (A3 a1 a2) (A4 a1 a2) a3 a4
-- Triple type parameterized by a1 a2 a3
definition A1_tuple_ty (a1 : A1) : (Type 1)
:= @Sigma (A2 a1) (A1A2_tuple_ty a1)
-- Triple a2 a3 a4
definition tuple_234 : A1_tuple_ty a1
:= @Pair (A2 a1) (A1A2_tuple_ty a1) a2 tuple_34
-- Quadruple type
definition tuple_ty : (Type 1)
:= @Sigma A1 A1_tuple_ty
-- Quadruple a1 a2 a3 a4
definition tuple_1234 : tuple_ty
:= @Pair A1 A1_tuple_ty a1 tuple_234
-- First element of the quadruple
definition f_1234 : A1
:= @Fst A1 A1_tuple_ty tuple_1234
-- Rest of the quadruple (i.e., a triple)
definition s_1234 : A1_tuple_ty f_1234
:= @Snd A1 A1_tuple_ty tuple_1234
theorem H_eq_a1 : f_1234 = a1
:= @FstAx A1 A1_tuple_ty a1 tuple_234
theorem H_eq_triple : s_1234 == tuple_234
:= @SndAx A1 A1_tuple_ty a1 tuple_234
-- Second element of the quadruple
definition fs_1234 : A2 f_1234
:= @Fst (A2 f_1234) (A1A2_tuple_ty f_1234) s_1234
-- Rest of the triple (i.e., a pair)
definition ss_1234 : A1A2_tuple_ty f_1234 fs_1234
:= @Snd (A2 f_1234) (A1A2_tuple_ty f_1234) s_1234
theorem H_eq_a2 : fs_1234 == a2
:= have H1 : @Fst (A2 f_1234) (A1A2_tuple_ty f_1234) s_1234 == @Fst (A2 a1) (A1A2_tuple_ty a1) tuple_234,
from hcongr (hcongr (hrefl (λ x, @Fst (A2 x) (A1A2_tuple_ty x))) (to_heq H_eq_a1)) H_eq_triple,
have H2 : @Fst (A2 a1) (A1A2_tuple_ty a1) tuple_234 = a2,
from FstAx _ _,
htrans H1 (to_heq H2)
theorem H_eq_pair : ss_1234 == tuple_34
:= have H1 : @Snd (A2 f_1234) (A1A2_tuple_ty f_1234) s_1234 == @Snd (A2 a1) (A1A2_tuple_ty a1) tuple_234,
from hcongr (hcongr (hrefl (λ x, @Snd (A2 x) (A1A2_tuple_ty x))) (to_heq H_eq_a1)) H_eq_triple,
have H2 : @Snd (A2 a1) (A1A2_tuple_ty a1) tuple_234 == tuple_34,
from SndAx _ _,
htrans H1 H2
-- Third element of the quadruple
definition fss_1234 : A3 f_1234 fs_1234
:= @Fst (A3 f_1234 fs_1234) (A4 f_1234 fs_1234) ss_1234
-- Fourth element of the quadruple
definition sss_1234 : A4 f_1234 fs_1234 fss_1234
:= @Snd (A3 f_1234 fs_1234) (A4 f_1234 fs_1234) ss_1234
theorem H_eq_a3 : fss_1234 == a3
:= have H1 : @Fst (A3 f_1234 fs_1234) (A4 f_1234 fs_1234) ss_1234 == @Fst (A3 a1 a2) (A4 a1 a2) tuple_34,
from hcongr (hcongr (hcongr (hrefl (λ x y z, @Fst (A3 x y) (A4 x y) z)) (to_heq H_eq_a1)) H_eq_a2) H_eq_pair,
have H2 : @Fst (A3 a1 a2) (A4 a1 a2) tuple_34 = a3,
from FstAx _ _,
htrans H1 (to_heq H2)
theorem H_eq_a4 : sss_1234 == a4
:= have H1 : @Snd (A3 f_1234 fs_1234) (A4 f_1234 fs_1234) ss_1234 == @Snd (A3 a1 a2) (A4 a1 a2) tuple_34,
from hcongr (hcongr (hcongr (hrefl (λ x y z, @Snd (A3 x y) (A4 x y) z)) (to_heq H_eq_a1)) H_eq_a2) H_eq_pair,
have H2 : @Snd (A3 a1 a2) (A4 a1 a2) tuple_34 == a4,
from SndAx _ _,
htrans H1 H2
eval tuple_1234
eval f_1234
eval fs_1234
eval fss_1234
eval sss_1234
check H_eq_a1
check H_eq_a2
check H_eq_a3
check H_eq_a4
theorem f_quadruple : Fst (Pair a1 (Pair a2 (Pair a3 a4))) = a1
:= H_eq_a1
theorem fs_quadruple : Fst (Snd (Pair a1 (Pair a2 (Pair a3 a4)))) == a2
:= H_eq_a2
theorem fss_quadruple : Fst (Snd (Snd (Pair a1 (Pair a2 (Pair a3 a4))))) == a3
:= H_eq_a3
theorem sss_quadruple : Snd (Snd (Snd (Pair a1 (Pair a2 (Pair a3 a4))))) == a4
:= H_eq_a4
end
-- Show the theorems with their parameters
check f_quadruple
check fs_quadruple
check fss_quadruple
check sss_quadruple
exit

542
examples/lean/primes.lean
View file

@ -1,542 +0,0 @@
----------------------------------------------------------------------------------------------------
--
-- theory primes.lean
-- author: Jeremy Avigad
--
-- Experimenting with Lean.
--
----------------------------------------------------------------------------------------------------
import macros
import tactic
using Nat
--
-- fundamental properties of Nat
--
theorem cases_on {P : Nat → Bool} (a : Nat) (H1 : P 0) (H2 : ∀ (n : Nat), P (n + 1)) : P a
:= induction_on a H1 (take n : Nat, assume ih : P n, H2 n)
theorem strong_induction_on {P : Nat → Bool} (a : Nat) (H : ∀ n, (∀ m, m < n → P m) → P n) : P a
:= @strong_induction P H a
-- in hindsight, now I know I don't need these
theorem one_ne_zero : 1 ≠ 0 := succ_nz 0
theorem two_ne_zero : 2 ≠ 0 := succ_nz 1
--
-- observation: the proof of lt_le_trans in Nat is not needed
--
theorem lt_le_trans2 {a b c : Nat} (H1 : a < b) (H2 : b ≤ c) : a < c
:= le_trans H1 H2
--
-- also, contrapos and mt are the same theorem
--
theorem contrapos2 {a b : Bool} (H : a → b) : ¬ b → ¬ a
:= mt H
--
-- properties of lt and le
--
theorem succ_le_succ {a b : Nat} (H : a + 1 ≤ b + 1) : a ≤ b
:=
obtain (x : Nat) (Hx : a + 1 + x = b + 1), from lt_elim H,
have H2 : a + x + 1 = b + 1, from (calc
a + x + 1 = a + (x + 1) : add_assoc _ _ _
... = a + (1 + x) : { add_comm x 1 }
... = a + 1 + x : symm (add_assoc _ _ _)
... = b + 1 : Hx),
have H3 : a + x = b, from (succ_inj H2),
show a ≤ b, from (le_intro H3)
-- should we keep this duplication or < and <=?
theorem lt_succ {a b : Nat} (H : a < b + 1) : a ≤ b
:= succ_le_succ H
theorem succ_le_succ_eq (a b : Nat) : a + 1 ≤ b + 1 ↔ a ≤ b
:= iff_intro succ_le_succ (assume H : a ≤ b, le_add H 1)
theorem lt_succ_eq (a b : Nat) : a < b + 1 ↔ a ≤ b
:= succ_le_succ_eq a b
theorem le_or_lt (a : Nat) : ∀ b : Nat, a ≤ b ∨ b < a
:=
induction_on a (
show ∀b, 0 ≤ b ∨ b < 0,
from take b, or_introl (le_zero b) _
) (
take a,
assume ih : ∀b, a ≤ b ∨ b < a,
show ∀b, a + 1 ≤ b ∨ b < a + 1,
from
take b,
cases_on b (
show a + 1 ≤ 0 ∨ 0 < a + 1,
from or_intror _ (le_add (le_zero a) 1)
) (
take b,
have H : a ≤ b ∨ b < a, from ih b,
show a + 1 ≤ b + 1 ∨ b + 1 < a + 1,
from or_elim H (
assume H1 : a ≤ b,
or_introl (le_add H1 1) (b + 1 < a + 1)
) (
assume H2 : b < a,
or_intror (a + 1 ≤ b + 1) (le_add H2 1)
)
)
)
theorem not_le_lt {a b : Nat} : ¬ a ≤ b → b < a
:= (or_imp _ _) ◂ le_or_lt a b
theorem not_lt_le {a b : Nat} : ¬ a < b → b ≤ a
:= (or_imp _ _) ◂ (or_comm _ _ ◂ le_or_lt b a)
theorem lt_not_le {a b : Nat} (H : a < b) : ¬ b ≤ a
:= not_intro (take H1 : b ≤ a, absurd (lt_le_trans H H1) (lt_nrefl a))
theorem le_not_lt {a b : Nat} (H : a ≤ b) : ¬ b < a
:= not_intro (take H1 : b < a, absurd H (lt_not_le H1))
theorem not_le_iff {a b : Nat} : ¬ a ≤ b ↔ b < a
:= iff_intro (@not_le_lt a b) (@lt_not_le b a)
theorem not_lt_iff {a b : Nat} : ¬ a < b ↔ b ≤ a
:= iff_intro (@not_lt_le a b) (@le_not_lt b a)
theorem le_iff {a b : Nat} : a ≤ b ↔ a < b ∨ a = b
:=
iff_intro (
assume H : a ≤ b,
show a < b ∨ a = b,
from or_elim (em (a = b)) (
take H1 : a = b,
show a < b ∨ a = b, from or_intror _ H1
) (
take H2 : a ≠ b,
have H3 : ¬ b ≤ a,
from not_intro (take H4: b ≤ a, absurd (le_antisym H H4) H2),
have H4 : a < b, from resolve1 (le_or_lt b a) H3,
show a < b ∨ a = b, from or_introl H4 _
)
)(
assume H : a < b ∨ a = b,
show a ≤ b,
from or_elim H (
take H1 : a < b, lt_le H1
) (
take H1 : a = b, subst (le_refl a) H1
)
)
theorem ne_symm_iff {A : (Type U)} (a b : A) : a ≠ b ↔ b ≠ a
:= iff_intro ne_symm ne_symm
theorem lt_iff (a b : Nat) : a < b ↔ a ≤ b ∧ a ≠ b
:=
calc
a < b = ¬ b ≤ a : symm (not_le_iff)
... = ¬ (b < a ∨ b = a) : { le_iff }
... = ¬ b < a ∧ b ≠ a : not_or _ _
... = a ≤ b ∧ b ≠ a : { not_lt_iff }
... = a ≤ b ∧ a ≠ b : { ne_symm_iff _ _ }
theorem ne_zero_ge_one {x : Nat} (H : x ≠ 0) : x ≥ 1
:= resolve2 (le_iff ◂ (le_zero x)) (ne_symm H)
theorem ne_zero_one_ge_two {x : Nat} (H0 : x ≠ 0) (H1 : x ≠ 1) : x ≥ 2
:= resolve2 (le_iff ◂ (ne_zero_ge_one H0)) (ne_symm H1)
-- the forward direction can be replaced by ne_zero_ge_one, but
-- note the comments below
theorem ne_zero_iff (n : Nat) : n ≠ 0 ↔ n > 0
:=
iff_intro (
assume H : n ≠ 0,
by_contradiction (
assume H1 : ¬ n > 0,
-- curious: if you make the arguments implicit in the next line,
-- it fails (the evaluator is getting in the way, I think)
have H2 : n = 0, from le_antisym (@not_lt_le 0 n H1) (le_zero n),
absurd H2 H
)
) (
-- here too
assume H : n > 0, ne_symm (@lt_ne 0 n H)
)
-- Note: this differs from Leo's naming conventions
theorem mul_right_mono {x y : Nat} (H : x ≤ y) (z : Nat) : x * z ≤ y * z
:=
obtain (w : Nat) (Hw : x + w = y),
from le_elim H,
le_intro (
show x * z + w * z = y * z,
from calc
x * z + w * z = (x + w) * z : symm (distributel x w z)
... = y * z : { Hw }
)
theorem mul_left_mono (x : Nat) {y z : Nat} (H : y ≤ z) : x * y ≤ x * z
:= subst (subst (mul_right_mono H x) (mul_comm y x)) (mul_comm z x)
theorem le_addr (a b : Nat) : a ≤ a + b
:= le_intro (refl (a + b))
theorem le_addl (a b : Nat) : a ≤ b + a
:= subst (le_addr a b) (add_comm a b)
theorem add_left_mono {a b : Nat} (c : Nat) (H : a ≤ b) : c + a ≤ c + b
:= subst (subst (le_add H c) (add_comm a c)) (add_comm b c)
theorem mul_right_strict_mono {x y z : Nat} (H : x < y) (znez : z ≠ 0) : x * z < y * z
:=
obtain (w : Nat) (Hw : x + 1 + w = y),
from le_elim H,
have H1 : y * z = x * z + w * z + z,
from calc
y * z = (x + 1 + w) * z : { symm Hw }
... = (x + (1 + w)) * z : { add_assoc _ _ _ }
... = (x + (w + 1)) * z : { add_comm _ _ }
... = (x + w + 1) * z : { symm (add_assoc _ _ _) }
... = (x + w) * z + 1 * z : distributel _ _ _
... = (x + w) * z + z : { mul_onel _ }
... = x * z + w * z + z : { distributel _ _ _ },
have H2 : x * z ≤ x * z + w * z, from le_addr _ _,
have H3 : x * z + w * z < x * z + w * z + z, from add_left_mono _ (ne_zero_ge_one znez),
show x * z < y * z, from subst (le_lt_trans H2 H3) (symm H1)
theorem mul_left_strict_mono {x y z : Nat} (H : x < y) (znez : z ≠ 0) : z * x < z * y
:= subst (subst (mul_right_strict_mono H znez) (mul_comm x z)) (mul_comm y z)
theorem mul_left_le_cancel {a b c : Nat} (H : a * b ≤ a * c) (anez : a ≠ 0) : b ≤ c
:=
by_contradiction (
assume H1 : ¬ b ≤ c,
have H2 : a * c < a * b, from mul_left_strict_mono (not_le_lt H1) anez,
show false, from absurd H (lt_not_le H2)
)
theorem mul_right_le_cancel {a b c : Nat} (H : b * a ≤ c * a) (anez : a ≠ 0) : b ≤ c
:= mul_left_le_cancel (subst (subst H (mul_comm b a)) (mul_comm c a)) anez
theorem mul_left_lt_cancel {a b c : Nat} (H : a * b < a * c) : b < c
:=
by_contradiction (
assume H1 : ¬ b < c,
have H2 : a * c ≤ a * b, from mul_left_mono a (not_lt_le H1),
show false, from absurd H (le_not_lt H2)
)
theorem mul_right_lt_cancel {a b c : Nat} (H : b * a < c * a) : b < c
:= mul_left_lt_cancel (subst (subst H (mul_comm b a)) (mul_comm c a))
theorem add_right_comm (a b c : Nat) : a + b + c = a + c + b
:=
calc
a + b + c = a + (b + c) : add_assoc _ _ _
... = a + (c + b) : { add_comm b c }
... = a + c + b : symm (add_assoc _ _ _)
theorem add_left_le_cancel {a b c : Nat} (H : a + c ≤ b + c) : a ≤ b
:=
obtain (d : Nat) (Hd : a + c + d = b + c), from le_elim H,
le_intro (add_injl (subst Hd (add_right_comm a c d)))
theorem add_right_le_cancel {a b c : Nat} (H : c + a ≤ c + b) : a ≤ b
:= add_left_le_cancel (subst (subst H (add_comm c a)) (add_comm c b))
--
-- more properties of multiplication
--
theorem mul_left_cancel {a b c : Nat} (H : a * b = a * c) (anez : a ≠ 0) : b = c
:=
have H1 : a * b ≤ a * c, from subst (le_refl _) H,
have H2 : a * c ≤ a * b, from subst (le_refl _) H,
le_antisym (mul_left_le_cancel H1 anez) (mul_left_le_cancel H2 anez)
theorem mul_right_cancel {a b c : Nat} (H : b * a = c * a) (anez : a ≠ 0) : b = c
:= mul_left_cancel (subst (subst H (mul_comm b a)) (mul_comm c a)) anez
--
-- divisibility
--
definition dvd (a b : Nat) : Bool := ∃ c, a * c = b
infix 50 | : dvd
theorem dvd_intro {a b c : Nat} (H : a * c = b) : a | b
:= exists_intro c H
theorem dvd_elim {a b : Nat} (H : a | b) : ∃ c, a * c = b
:= H
theorem dvd_self (n : Nat) : n | n := dvd_intro (mul_oner n)
theorem one_dvd (a : Nat) : 1 | a
:= dvd_intro (mul_onel a)
theorem zero_dvd {a : Nat} (H: 0 | a) : a = 0
:=
obtain (w : Nat) (H1 : 0 * w = a), from H,
subst (symm H1) (mul_zerol _)
theorem dvd_zero (a : Nat) : a | 0
:= exists_intro 0 (mul_zeror _)
theorem dvd_trans {a b c} (H1 : a | b) (H2 : b | c) : a | c
:=
obtain (w1 : Nat) (Hw1 : a * w1 = b), from H1,
obtain (w2 : Nat) (Hw2 : b * w2 = c), from H2,
exists_intro (w1 * w2)
calc a * (w1 * w2) = a * w1 * w2 : symm (mul_assoc a w1 w2)
... = b * w2 : { Hw1 }
... = c : Hw2
theorem dvd_le {x y : Nat} (H : x | y) (ynez : y ≠ 0) : x ≤ y
:=
obtain (w : Nat) (Hw : x * w = y), from H,
have wnez : w ≠ 0, from
not_intro (take H1 : w = 0, absurd (
calc y = x * w : symm Hw
... = x * 0 : { H1 }
... = 0 : mul_zeror x
) ynez),
have H2 : x * 1 ≤ x * w, from mul_left_mono x (ne_zero_ge_one wnez),
show x ≤ y, from subst (subst H2 (mul_oner x)) Hw
theorem dvd_mul_right {a b : Nat} (H : a | b) (c : Nat) : a | b * c
:=
obtain (d : Nat) (Hd : a * d = b), from dvd_elim H,
dvd_intro (
calc
a * (d * c) = (a * d) * c : symm (mul_assoc _ _ _)
... = b * c : { Hd }
)
theorem dvd_mul_left {a b : Nat} (H : a | b) (c : Nat) : a | c * b
:= subst (dvd_mul_right H c) (mul_comm b c)
theorem dvd_add {a b c : Nat} (H1 : a | b) (H2 : a | c) : a | b + c
:=
obtain (w1 : Nat) (Hw1 : a * w1 = b), from H1,
obtain (w2 : Nat) (Hw2 : a * w2 = c), from H2,
exists_intro (w1 + w2)
calc a * (w1 + w2) = a * w1 + a * w2 : distributer _ _ _
... = b + a * w2 : { Hw1 }
... = b + c : { Hw2 }
theorem dvd_add_cancel {a b c : Nat} (H1 : a | b + c) (H2 : a | b) : a | c
:=
or_elim (em (a = 0)) (
assume az : a = 0,
have H3 : c = 0, from
calc c = 0 + c : symm (add_zerol _)
... = b + c : { symm (zero_dvd (subst H2 az)) }
... = 0 : zero_dvd (subst H1 az),
show a | c, from subst (dvd_zero a) (symm H3)
) (
assume anz : a ≠ 0,
obtain (w1 : Nat) (Hw1 : a * w1 = b + c), from H1,
obtain (w2 : Nat) (Hw2 : a * w2 = b), from H2,
have H3 : a * w1 = a * w2 + c, from subst Hw1 (symm Hw2),
have H4 : a * w2 ≤ a * w1, from le_intro (symm H3),
have H5 : w2 ≤ w1, from mul_left_le_cancel H4 anz,
obtain (w3 : Nat) (Hw3 : w2 + w3 = w1), from le_elim H5,
have H6 : b + a * w3 = b + c, from
calc
b + a * w3 = a * w2 + a * w3 : { symm Hw2 }
... = a * (w2 + w3) : symm (distributer _ _ _)
... = a * w1 : { Hw3 }
... = b + c : Hw1,
have H7 : a * w3 = c, from add_injr H6,
show a | c, from dvd_intro H7
)
--
-- primes
--
definition prime p := p ≥ 2 ∧ forall m, m | p → m = 1 ∨ m = p
theorem not_prime_has_divisor {n : Nat} (H1 : n ≥ 2) (H2 : ¬ prime n) : ∃ m, m | n ∧ m ≠ 1 ∧ m ≠ n
:=
have H3 : ¬ n ≥ 2 ∨ ¬ (∀ m : Nat, m | n → m = 1 ∨ m = n),
from not_and _ _ ◂ H2,
have H4 : ¬ ¬ n ≥ 2,
from (symm (not_not_eq _)) ◂ H1,
obtain (m : Nat) (H5 : ¬ (m | n → m = 1 ∨ m = n)),
from not_forall_elim (resolve1 H3 H4),
have H6 : m | n ∧ ¬ (m = 1 ∨ m = n),
from (not_implies _ _) ◂ H5,
have H7 : ¬ (m = 1 ∨ m = n) ↔ (m ≠ 1 ∧ m ≠ n),
from not_or (m = 1) (m = n),
have H8 : m | n ∧ m ≠ 1 ∧ m ≠ n,
from subst H6 H7,
show ∃ m, m | n ∧ m ≠ 1 ∧ m ≠ n,
from exists_intro m H8
theorem not_prime_has_divisor2 {n : Nat} (H1 : n ≥ 2) (H2 : ¬ prime n) :
∃ m, m | n ∧ m ≥ 2 ∧ m < n
:=
have n_ne_0 : n ≠ 0, from
not_intro (take n0 : n = 0, substp (fun n, n ≥ 2) H1 n0),
obtain (m : Nat) (Hm : m | n ∧ m ≠ 1 ∧ m ≠ n),
from not_prime_has_divisor H1 H2,
let m_dvd_n := and_eliml Hm in
let m_ne_1 := and_eliml (and_elimr Hm) in
let m_ne_n := and_elimr (and_elimr Hm) in
have m_ne_0 : m ≠ 0, from
not_intro (
take m0 : m = 0,
have n0 : n = 0, from zero_dvd (subst m_dvd_n m0),
absurd n0 n_ne_0
),
exists_intro m (
and_intro m_dvd_n (
and_intro (
show m ≥ 2, from ne_zero_one_ge_two m_ne_0 m_ne_1
) (
have m_le_n : m ≤ n, from dvd_le m_dvd_n n_ne_0,
show m < n, from resolve2 (le_iff ◂ m_le_n) m_ne_n
)
)
)
theorem has_prime_divisor {n : Nat} : n ≥ 2 → ∃ p, prime p ∧ p | n
:=
strong_induction_on n (
take n,
assume ih : ∀ m, m < n → m ≥ 2 → ∃ p, prime p ∧ p | m,
assume n_ge_2 : n ≥ 2,
show ∃ p, prime p ∧ p | n, from
or_elim (em (prime n)) (
assume H : prime n,
exists_intro n (and_intro H (dvd_self n))
) (
assume H : ¬ prime n,
obtain (m : Nat) (Hm : m | n ∧ m ≥ 2 ∧ m < n),
from not_prime_has_divisor2 n_ge_2 H,
obtain (p : Nat) (Hp : prime p ∧ p | m),
from ih m (and_elimr (and_elimr Hm)) (and_eliml (and_elimr Hm)),
have p_dvd_n : p | n, from dvd_trans (and_elimr Hp) (and_eliml Hm),
exists_intro p (and_intro (and_eliml Hp) p_dvd_n)
)
)
--
-- factorial
--
variable fact : Nat → Nat
axiom fact_0 : fact 0 = 1
axiom fact_succ : ∀ n, fact (n + 1) = (n + 1) * fact n
-- can the simplifier do this?
theorem fact_1 : fact 1 = 1
:=
calc
fact 1 = fact (0 + 1) : { symm (add_zerol 1) }
... = (0 + 1) * fact 0 : fact_succ _
... = 1 * fact 0 : { add_zerol 1 }
... = 1 * 1 : { fact_0 }
... = 1 : mul_oner _
theorem fact_ne_0 (n : Nat) : fact n ≠ 0
:=
induction_on n (
not_intro (
assume H : fact 0 = 0,
have H1 : 1 = 0, from (subst H fact_0),
absurd H1 one_ne_zero
)
) (
take n,
assume ih : fact n ≠ 0,
not_intro (
assume H : fact (n + 1) = 0,
have H1 : n + 1 = 0, from
mul_right_cancel (
calc
(n + 1) * fact n = fact (n + 1) : symm (fact_succ n)
... = 0 : H
... = 0 * fact n : symm (mul_zerol _)
) ih,
absurd H1 (succ_nz _)
)
)
theorem dvd_fact {m n : Nat} (m_gt_0 : m > 0) (m_le_n : m ≤ n) : m | fact n
:=
obtain (m' : Nat) (Hm' : 1 + m' = m), from le_elim m_gt_0,
obtain (n' : Nat) (Hn' : 1 + n' = n), from le_elim (le_trans m_gt_0 m_le_n),
have m'_le_n' : m' ≤ n',
from add_right_le_cancel (subst (subst m_le_n (symm Hm')) (symm Hn')),
have H : ∀ n' m', m' ≤ n' → m' + 1 | fact (n' + 1), from
induction (
take m' ,
assume m'_le_0 : m' ≤ 0,
have Hm' : m' + 1 = 1,
from calc
m' + 1 = 0 + 1 : { le_antisym m'_le_0 (le_zero m') }
... = 1 : add_zerol _,
show m' + 1 | fact (0 + 1), from subst (one_dvd _) (symm Hm')
) (
take n',
assume ih : ∀m', m' ≤ n' → m' + 1 | fact (n' + 1),
take m',
assume Hm' : m' ≤ n' + 1,
have H1 : m' < n' + 1 ∨ m' = n' + 1, from le_iff ◂ Hm',
or_elim H1 (
assume H2 : m' < n' + 1,
have H3 : m' ≤ n', from lt_succ H2,
have H4 : m' + 1 | fact (n' + 1), from ih _ H3,
have H5 : m' + 1 | (n' + 1 + 1) * fact (n' + 1), from dvd_mul_left H4 _,
show m' + 1 | fact (n' + 1 + 1), from subst H5 (symm (fact_succ _))
) (
assume H2 : m' = n' + 1,
have H3 : m' + 1 | n' + 1 + 1, from subst (dvd_self _) H2,
have H4 : m' + 1 | (n' + 1 + 1) * fact (n' + 1), from dvd_mul_right H3 _,
show m' + 1 | fact (n' + 1 + 1), from subst H4 (symm (fact_succ _))
)
),
have H1 : m' + 1 | fact (n' + 1), from H _ _ m'_le_n',
show m | fact n,
from (subst (subst (subst (subst H1 (add_comm m' 1)) Hm') (add_comm n' 1)) Hn')
theorem primes_infinite (n : Nat) : ∃ p, p ≥ n ∧ prime p
:=
let m := fact (n + 1) in
have Hn1 : n + 1 ≥ 1, from le_addl _ _,
have m_ge_1 : m ≥ 1, from ne_zero_ge_one (fact_ne_0 _),
have m1_ge_2 : m + 1 ≥ 2, from le_add m_ge_1 1,
obtain (p : Nat) (Hp : prime p ∧ p | m + 1), from has_prime_divisor m1_ge_2,
let prime_p := and_eliml Hp in
let p_dvd_m1 := and_elimr Hp in
have p_ge_2 : p ≥ 2, from and_eliml prime_p,
have two_gt_0 : 2 > 0, from (ne_zero_iff 2) ◂ (succ_nz 1),
-- fails if arguments are left implicit
have p_gt_0 : p > 0, from @lt_le_trans 0 2 p two_gt_0 p_ge_2,
have p_ge_n : p ≥ n, from
by_contradiction (
assume H1 : ¬ p ≥ n,
have H2 : p < n, from not_le_lt H1,
have H3 : p ≤ n + 1, from lt_le (lt_le_trans H2 (le_addr n 1)),
have H4 : p | m, from dvd_fact p_gt_0 H3,
have H5 : p | 1, from dvd_add_cancel p_dvd_m1 H4,
have H6 : p ≤ 1, from dvd_le H5 (succ_nz 0),
have H7 : 2 ≤ 1, from le_trans p_ge_2 H6,
absurd H7 (lt_nrefl 1)
),
exists_intro p (and_intro p_ge_n prime_p)

25
examples/lean/set.lean
View file

@ -1,25 +0,0 @@
import macros
definition Set (A : Type) : Type := A → Bool
definition element {A : Type} (x : A) (s : Set A) := s x
infix 60 ∈ : element
definition subset {A : Type} (s1 : Set A) (s2 : Set A) := ∀ x, x ∈ s1 → x ∈ s2
infix 50 ⊆ : subset
theorem subset_trans {A : Type} {s1 s2 s3 : Set A} (H1 : s1 ⊆ s2) (H2 : s2 ⊆ s3) : s1 ⊆ s3
:= take x : A,
assume Hin : x ∈ s1,
show x ∈ s3, from
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
:= funext H
theorem subset_antisym {A : Type} {s1 s2 : Set A} (H1 : s1 ⊆ s2) (H2 : s2 ⊆ s1) : s1 = s2
:= subset_ext (show (∀ x, x ∈ s1 = x ∈ s2), from
take x, show x ∈ s1 = x ∈ s2, from
boolext (show x ∈ s1 → x ∈ s2, from H1 x)
(show x ∈ s2 → x ∈ s1, from H2 x))

70
examples/lean/setoid.lean
View file

@ -1,70 +0,0 @@
-- Setoid example/test
import macros
definition reflexive {A : (Type U)} (r : A → A → Bool) := ∀ x, r x x
definition symmetric {A : (Type U)} (r : A → A → Bool) := ∀ x y, r x y → r y x
definition transitive {A : (Type U)} (r : A → A → Bool) := ∀ x y z, r x y → r y z → r x z
-- We need to create a universe smaller than U for defining setoids.
-- If we use (Type U) in the definition of setoid, then we will not be
-- able to write s1 = s2 given s1 s2 : setoid.
-- Writing the universes explicitily is really annoying. We should try to hide them.
universe s ≥ 1
-- We currently don't have records. So, we use sigma types.
definition setoid := sig A : (Type s), sig eq : A → A → Bool, (reflexive eq) # (symmetric eq) # (transitive eq)
definition to_setoid (S : (Type s)) (eq : S → S → Bool) (Hrefl : reflexive eq) (Hsymm : symmetric eq) (Htrans : transitive eq) : setoid
:= pair S (pair eq (pair Hrefl (pair Hsymm Htrans)))
-- The following definitions can be generated automatically.
definition carrier (s : setoid) := proj1 s
definition S_eq {s : setoid} : carrier s → carrier s → Bool
:= proj1 (proj2 s)
infix 50 ≈ : S_eq
definition S_refl {s : setoid} : ∀ x, x ≈ x
:= proj1 (proj2 (proj2 s))
definition S_symm {s : setoid} {x y : carrier s} : x ≈ y → y ≈ x
:= proj1 (proj2 (proj2 (proj2 s))) x y
definition S_trans {s : setoid} {x y z : carrier s} : x ≈ y → y ≈ z → x ≈ z
:= proj2 (proj2 (proj2 (proj2 s))) x y z
-- First example: the cross-product of two setoids is a setoid
definition product (s1 s2 : setoid) : setoid
:= to_setoid
(carrier s1 # carrier s2)
(λ x y, proj1 x ≈ proj1 y ∧ proj2 x ≈ proj2 y)
(take x, and_intro (S_refl (proj1 x)) (S_refl (proj2 x)))
(take x y,
assume H : proj1 x ≈ proj1 y ∧ proj2 x ≈ proj2 y,
and_intro (S_symm (and_eliml H)) (S_symm (and_elimr H)))
(take x y z,
assume H1 : proj1 x ≈ proj1 y ∧ proj2 x ≈ proj2 y,
assume H2 : proj1 y ≈ proj1 z ∧ proj2 y ≈ proj2 z,
and_intro (S_trans (and_eliml H1) (and_eliml H2))
(S_trans (and_elimr H1) (and_elimr H2)))
scope
-- We need to extend the elaborator to be able to write
-- p1 p2 : product s1 s2
set_option pp::implicit true
check λ (s1 s2 : setoid) (p1 p2 : carrier (product s1 s2)), p1 ≈ p2
end
definition morphism (s1 s2 : setoid) := sig f : carrier s1 → carrier s2, ∀ x y, x ≈ y → f x ≈ f y
definition morphism_intro {s1 s2 : setoid} (f : carrier s1 → carrier s2) (H : ∀ x y, x ≈ y → f x ≈ f y) : morphism s1 s2
:= pair f H
definition f {s1 s2 : setoid} (m : morphism s1 s2) : carrier s1 → carrier s2
:= proj1 m
-- It would be nice to support (m.f x) as syntax sugar for (f m x)
definition is_compat {s1 s2 : setoid} (m : morphism s1 s2) {x y : carrier s1} : x ≈ y → f m x ≈ f m y
:= proj2 m x y
-- Second example: the composition of two morphism is a morphism
definition compose {s1 s2 s3 : setoid} (m1 : morphism s1 s2) (m2 : morphism s2 s3) : morphism s1 s3
:= morphism_intro
(λ x, f m2 (f m1 x))
(take x y, assume Hxy : x ≈ y,
have Hfxy : f m1 x ≈ f m1 y,
from is_compat m1 Hxy,
show f m2 (f m1 x) ≈ f m2 (f m1 y),
from is_compat m2 Hfxy)

113
examples/lean/setoid2.lean
View file

@ -1,113 +0,0 @@
-- Setoid example/test
import macros
import tactic
variable first {A : (Type U)} {B : A → (Type U)} (p : sig x : A, B x) : A
variable second {A : (Type U)} {B : A → (Type U)} (p : sig x : A, B x) : B (first p)
definition reflexive {A : (Type U)} (r : A → A → Bool) := ∀ x, r x x
definition symmetric {A : (Type U)} (r : A → A → Bool) := ∀ x y, r x y → r y x
definition transitive {A : (Type U)} (r : A → A → Bool) := ∀ x y z, r x y → r y z → r x z
-- We need to create a universe smaller than U for defining setoids.
-- If we use (Type U) in the definition of setoid, then we will not be
-- able to write s1 = s2 given s1 s2 : setoid.
-- Writing the universes explicitily is really annoying. We should try to hide them.
universe M ≥ 1
-- We currently don't have records. So, we use sigma types.
definition setoid := sig A : (Type M), sig eq : A → A → Bool, (reflexive eq) # (symmetric eq) # (transitive eq)
definition to_setoid (S : (Type M)) (eq : S → S → Bool) (Hrefl : reflexive eq) (Hsymm : symmetric eq) (Htrans : transitive eq) : setoid
:= pair S (pair eq (pair Hrefl (pair Hsymm Htrans)))
-- The following definitions can be generated automatically.
definition carrier (s : setoid)
:= @first
(Type M)
(λ A : (Type M), sig eq : A → A → Bool, (reflexive eq) # (symmetric eq) # (transitive eq))
s
definition setoid_unfold1 (s : setoid) : sig eq : carrier s → carrier s → Bool, (reflexive eq) # (symmetric eq) # (transitive eq)
:= (@second (Type M)
(λ A : (Type M), sig eq : A → A → Bool, (reflexive eq) # (symmetric eq) # (transitive eq))
s)
definition S_eq {s : setoid} : carrier s → carrier s → Bool
:= (@first (carrier s → carrier s → Bool)
(λ eq : carrier s → carrier s → Bool, (reflexive eq) # (symmetric eq) # (transitive eq))
(setoid_unfold1 s))
infix 50 ≈ : S_eq
definition setoid_unfold2 (s : setoid) : (reflexive (@S_eq s)) # (symmetric (@S_eq s)) # (transitive (@S_eq s))
:= (@second (carrier s → carrier s → Bool)
(λ eq : carrier s → carrier s → Bool, (reflexive eq) # (symmetric eq) # (transitive eq))
(setoid_unfold1 s))
definition S_refl {s : setoid} : ∀ x : carrier s, x ≈ x
:= (@first (reflexive (@S_eq s))
(λ x : reflexive (@S_eq s), (symmetric (@S_eq s)) # (transitive (@S_eq s)))
(setoid_unfold2 s))
definition setoid_unfold3 (s : setoid) : (symmetric (@S_eq s)) # (transitive (@S_eq s))
:= (@second (reflexive (@S_eq s))
(λ x : reflexive (@S_eq s), (symmetric (@S_eq s)) # (transitive (@S_eq s)))
(setoid_unfold2 s))
definition S_symm {s : setoid} {x y : carrier s} : x ≈ y → y ≈ x
:= (@first (symmetric (@S_eq s))
(λ x : symmetric (@S_eq s), (transitive (@S_eq s)))
(setoid_unfold3 s))
x y
definition S_trans {s : setoid} {x y z : carrier s} : x ≈ y → y ≈ z → x ≈ z
:= (@second (symmetric (@S_eq s))
(λ x : symmetric (@S_eq s), (transitive (@S_eq s)))
(setoid_unfold3 s))
x y z
set_opaque carrier true
set_opaque S_eq true
set_opaque S_refl true
set_opaque S_symm true
set_opaque S_trans true
-- First example: the cross-product of two setoids is a setoid
definition product (s1 s2 : setoid) : setoid
:= to_setoid
(carrier s1 # carrier s2)
(λ x y, proj1 x ≈ proj1 y ∧ proj2 x ≈ proj2 y)
(take x, and_intro (S_refl (proj1 x)) (S_refl (proj2 x)))
(take x y,
assume H : proj1 x ≈ proj1 y ∧ proj2 x ≈ proj2 y,
and_intro (S_symm (and_eliml H)) (S_symm (and_elimr H)))
(take x y z,
assume H1 : proj1 x ≈ proj1 y ∧ proj2 x ≈ proj2 y,
assume H2 : proj1 y ≈ proj1 z ∧ proj2 y ≈ proj2 z,
and_intro (S_trans (and_eliml H1) (and_eliml H2))
(S_trans (and_elimr H1) (and_elimr H2)))
scope
-- We need to extend the elaborator to be able to write
-- p1 p2 : product s1 s2
set_option pp::implicit true
check λ (s1 s2 : setoid) (p1 p2 : carrier (product s1 s2)), p1 ≈ p2
end
definition morphism (s1 s2 : setoid) := sig f : carrier s1 → carrier s2, ∀ x y, x ≈ y → f x ≈ f y
definition morphism_intro {s1 s2 : setoid} (f : carrier s1 → carrier s2) (H : ∀ x y, x ≈ y → f x ≈ f y) : morphism s1 s2
:= pair f H
definition f {s1 s2 : setoid} (m : morphism s1 s2) : carrier s1 → carrier s2
:= proj1 m
-- It would be nice to support (m.f x) as syntax sugar for (f m x)
definition is_compat {s1 s2 : setoid} (m : morphism s1 s2) {x y : carrier s1} : x ≈ y → f m x ≈ f m y
:= proj2 m x y
-- Second example: the composition of two morphism is a morphism
definition compose {s1 s2 s3 : setoid} (m1 : morphism s1 s2) (m2 : morphism s2 s3) : morphism s1 s3
:= morphism_intro
(λ x, f m2 (f m1 x))
(take x y, assume Hxy : x ≈ y,
have Hfxy : f m1 x ≈ f m1 y,
from is_compat m1 Hxy,
show f m2 (f m1 x) ≈ f m2 (f m1 y),
from is_compat m2 Hfxy)

57
examples/lean/tactic1.lean
View file

@ -1,57 +0,0 @@
-- This example demonstrates how to specify a proof skeleton that contains
-- "holes" that must be filled using user-defined tactics.
import tactic
(*
-- Define a simple tactic using Lua
auto = Repeat(OrElse(assumption_tac(), conj_tac(), conj_hyp_tac()))
conj_hyp = conj_hyp_tac()
conj = conj_tac()
*)
-- The (by [tactic]) expression is essentially creating a "hole" and associating a "hint" to it.
-- The "hint" is a tactic that should be used to fill the "hole".
-- In the following example, we use the tactic "auto" defined by the Lua code above.
--
-- The (show [expr], by [tactic]) expression is also creating a "hole" and associating a "hint" to it.
-- The expression [expr] after the shows is fixing the type of the "hole"
theorem T1 (A B : Bool) : A /\ B -> B /\ A :=
fun assumption : A /\ B,
let lemma1 : A := (by auto),
lemma2 : B := (by auto)
in (show B /\ A, by auto)
print environment 1. -- print proof for the previous theorem
-- When hints are not provided, the user must fill the (remaining) holes using tactic command sequences.
-- Each hole must be filled with a tactic command sequence that terminates with the command 'done' and
-- successfully produces a proof term for filling the hole. Here is the same example without hints
-- This style is more convenient for interactive proofs
theorem T2 (A B : Bool) : A /\ B -> B /\ A :=
fun assumption : A /\ B,
let lemma1 : A := _, -- first hole
lemma2 : B := _ -- second hole
in _. -- third hole
auto. done. -- tactic command sequence for the first hole
auto. done. -- tactic command sequence for the second hole
auto. done. -- tactic command sequence for the third hole
-- In the following example, instead of using the "auto" tactic, we apply a sequence of even simpler tactics.
theorem T3 (A B : Bool) : A /\ B -> B /\ A :=
fun assumption : A /\ B,
let lemma1 : A := _, -- first hole
lemma2 : B := _ -- second hole
in _. -- third hole
conj_hyp. exact. done. -- tactic command sequence for the first hole
conj_hyp. exact. done. -- tactic command sequence for the second hole
conj. exact. done. -- tactic command sequence for the third hole
-- We can also mix the two styles (hints and command sequences)
theorem T4 (A B : Bool) : A /\ B -> B /\ A :=
fun assumption : A /\ B,
let lemma1 : A := _, -- first hole
lemma2 : B := _ -- second hole
in (show B /\ A, by auto).
auto. done. -- tactic command sequence for the first hole
auto. done. -- tactic command sequence for the second hole

72
examples/lean/tactic_in_lua.lean
View file

@ -1,72 +0,0 @@
(*
-- This example demonstrates how to create a new tactic using Lua.
-- The basic idea is to reimplement the tactic conj_tactic in Lua.
-- Tactic for splitting goals of the form
-- n : Hs |- A /\ B
-- into
-- n::1 : Hs |- A
-- n::2 : Hs |- B
function conj_fn(env, ios, s)
local gs = s:goals()
-- We store the information needed by the proof_builder in the
-- array proof_info.
-- proof_info has the format {{name_1, expr_1}, ... {name_k, expr_k}}
-- where name_i is a goal splitted by this tactic, and expr_i
-- is the conclusion of the theorem, that is, an expression of the form
-- A /\ B
local proof_info = {}
-- We store the new goals into the Lua array new_gs.
-- new_gs has the format {{name_1, goal_1}, ..., {name_n, goal_n}}
local new_gs = {}
local found = false
for n, g in gs:pairs() do
yield() -- Give a chance to other tactics to run
local c = g:conclusion()
if c:is_and() then
-- Goal g is of the form Hs |- A /\ B
found = true -- The tactic managed to split at least one goal
local Hs = g:hypotheses()
local A = c:arg(1)
local B = c:arg(2)
proof_info[#proof_info + 1] = {n, c} -- Save information for implementing the proof builder
new_gs[#new_gs + 1] = {name(n, 1), goal(Hs, A)} -- Add goal n::1 : Hs |- A
new_gs[#new_gs + 1] = {name(n, 2), goal(Hs, B)} -- Add goal n::1 : Hs |- B
else
new_gs[#new_gs + 1] = {n, g} -- Keep the goal
end
end
if not found then
return nil -- Tactic is not applicable
end
local pb = s:proof_builder()
local new_pb =
function(m, a)
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
local c = p[2] -- c is the conclusion of the goal splitted by this tactic
assert(c:is_and()) -- c is of the form A /\ B
-- The proof for goal n is
-- Conj(A, B, H1, H2)
-- where H1 and H2 are the proofs for goals n::1 and n::2
new_m:insert(n, Conj(c:arg(1), c:arg(2), m:find(name(n, 1)), m:find(name(n, 2))))
-- We don't need the proofs for n::1 and n::2 anymore
new_m:erase(name(n, 1))
new_m:erase(name(n, 2))
end
return pb(new_m, a) -- Apply the proof builder for the original state
end
return proof_state(s, goals(new_gs), proof_builder(new_pb))
end
conj_in_lua = tactic(conj_fn) -- Create a new tactic object using the Lua function conj_fn
-- Now, the tactic conj_in_lua can be used when proving theorems in Lean.
*)
theorem T (a b : Bool) : a -> b -> a /\ b := _.
(* Then(conj_in_lua, assumption_tac()) *)
done
-- print proof created using our script
print environment 1.

38
examples/lean/tc.lean
View file

@ -1,38 +0,0 @@
import macros
definition reflexive {A : TypeU} (R : A → A → Bool) := ∀ x, R x x
definition transitive {A : TypeU} (R : A → A → Bool) := ∀ x y z, R x y → R y z → R x z
definition subrelation {A : TypeU} (R1 : A → A → Bool) (R2 : A → A → Bool) := ∀ x y, R1 x y → R2 x y
infix 50 ⊆ : subrelation
-- (tcls R) is the transitive closure of relation R
-- We define it as the intersection of all transitive relations containing R
definition tcls {A : TypeU} (R : A → A → Bool) (a b : A)
:= ∀ P, (reflexive P) → (transitive P) → (R ⊆ P) → P a b
notation 65 _⁺ : tcls -- use superscript + as notation for transitive closure
theorem tcls_trans {A : TypeU} {R : A → A → Bool} {a b c : A} (Hab : R⁺ a b) (Hbc : R⁺ b c) : R⁺ a c
:= take P, assume Hrefl Htrans Hsub,
let Pab : P a b := Hab P Hrefl Htrans Hsub,
Pbc : P b c := Hbc P Hrefl Htrans Hsub
in Htrans a b c Pab Pbc
theorem tcls_refl {A : TypeU} (R : A → A → Bool) : ∀ a, R⁺ a a
:= take a P, assume Hrefl Htrans Hsub,
Hrefl a
theorem tcls_sub {A : TypeU} (R : A → A → Bool) : R ⊆ R⁺
:= take a b,
assume Hab : R a b,
show R⁺ a b, from
take P, assume Hrefl Htrans Hsub,
Hsub a b Hab
theorem tcls_step {A : TypeU} {R : A → A → Bool} {a b c : A} (H1 : R a b) (H2 : R⁺ b c) : R⁺ a c
:= take P, assume Hrefl Htrans Hsub,
Htrans a b c (Hsub a b H1) (H2 P Hrefl Htrans Hsub)
theorem tcls_smallest {A : TypeU} (R : A → A → Bool) : ∀ P, (reflexive P) → (transitive P) → (R ⊆ P) → (R⁺ ⊆ P)
:= take P, assume Hrefl Htrans Hsub,
take a b, assume H : R⁺ a b,
show P a b, from H P Hrefl Htrans Hsub

108
examples/lean/test_algebra.lean
View file

@ -1,108 +0,0 @@
import macros
---
--- Classes of structures, and axiomatic classes of structures
---
--- A "structure" consists of a carrier, and some data (whose type depends on the carrier)
definition StructClass : (Type 1) := Type → Type -- the type of the data
definition structure (S : StructClass) : (Type 1)
:= sig T : Type, S T
definition carrier {S : StructClass} (M : structure S) : Type
:= proj1 M
definition data {S : StructClass} (M : structure S) : S (carrier M)
:= proj2 M
--- An "axiomatic class" is a class of structures satisfying some predicate (the "axioms")
definition AxClass : (Type 1)
:= sig S : StructClass, structure S → Bool
-- Coercion from AxClass to StructClass
definition struct_class (C : AxClass) : StructClass
:= proj1 C
definition axioms {C : AxClass} (M : structure (struct_class C))
:= proj2 C M
definition instance (C : AxClass) : (Type 1)
:= sig M : structure (struct_class C), axioms M
definition struct {C : AxClass} (M : instance C)
:= proj1 M
definition hyps {C : AxClass} (M : instance C) : axioms (struct M)
:= proj2 M
---
--- Examples
---
--- multiplication (for overloading *)
definition MulStruct : StructClass
:= λ T, T → T → T
definition mul {M : structure MulStruct} (x y : carrier M) : carrier M
:= data M x y
infixl 70 * : mul
definition mul_is_assoc (M : structure MulStruct) : Bool
:= ∀ x y z : carrier M, (x * y) * z = x * (y * z)
definition mul_is_comm (M : structure MulStruct) : Bool
:= ∀ x y z : carrier M, x * y = y * x
--- semigroups
definition Semigroup : AxClass
:= pair MulStruct mul_is_assoc
--- to fill the hole above automatically
theorem semigroup_mul_is_assoc (M : instance Semigroup) : mul_is_assoc (struct M)
:= hyps M
definition OneStruct : StructClass
:= λ T, T
definition one {M : structure OneStruct} : carrier M
:= data M
-- structures with mult and one
definition MonoidStruct : StructClass
:= λ T, OneStruct T # MulStruct T
definition MonoidStruct_to_OneStruct (M : structure MonoidStruct) : (structure OneStruct)
:= pair (carrier M) (proj1 (data M))
definition MonoidStruct_to_MulStruct (M : structure MonoidStruct) : (structure MulStruct)
:= pair (carrier M) (proj2 (data M))
variable M : structure MonoidStruct
check carrier M = carrier (MonoidStruct_to_OneStruct M)
theorem test1 (M : structure MonoidStruct) : carrier M = carrier (MonoidStruct_to_OneStruct M)
:= refl (carrier M)
definition is_mul_right_id (M : structure MonoidStruct) : Bool
:= let m : carrier M → carrier M → carrier M := @mul (MonoidStruct_to_MulStruct M),
o : carrier M := @one (MonoidStruct_to_OneStruct M)
in ∀ x : carrier M, m x o = x
definition is_monoid (M : structure MonoidStruct) : Bool
:= mul_is_assoc (MonoidStruct_to_MulStruct M) ∧ is_mul_right_id M
definition Monoid : AxClass
:= pair MonoidStruct is_monoid
theorem monoid_is_mul_right_id (M : instance Monoid) : is_mul_right_id (struct M)
:= and_elimr (proj2 M)
theorem monoid_mul_is_assoc (M : instance Monoid) : mul_is_assoc (MonoidStruct_to_MulStruct (struct M))
:= and_eliml (proj2 M)

50
examples/lean/wf.lean
View file

@ -1,50 +0,0 @@
import macros
-- Well-founded relation definition
-- We are essentially saying that a relation R is well-founded
-- if every non-empty "set" P, has a R-minimal element
definition wf {A : (Type U)} (R : A → A → Bool) : Bool
:= ∀ P, (∃ w, P w) → ∃ min, P min ∧ ∀ b, R b min → ¬ P b
-- Well-founded induction theorem
theorem wf_induction {A : (Type U)} {R : A → A → Bool} {P : A → Bool} (Hwf : wf R) (iH : ∀ x, (∀ y, R y x → P y) → P x)
: ∀ x, P x
:= by_contradiction (assume N : ¬ ∀ x, P x,
obtain (w : A) (Hw : ¬ P w), from not_forall_elim N,
-- The main "trick" is to define Q x as ¬ P x.
-- Since R is well-founded, there must be a R-minimal element r s.t. Q r (which is ¬ P r)
let Q : A → Bool := λ x, ¬ P x in
have Qw : ∃ w, Q w,
from exists_intro w Hw,
have Qwf : ∃ min, Q min ∧ ∀ b, R b min → ¬ Q b,
from Hwf Q Qw,
obtain (r : A) (Hr : Q r ∧ ∀ b, R b r → ¬ Q b),
from Qwf,
-- Using the inductive hypothesis iH and Hr, we show P r, and derive the contradiction.
have s1 : ∀ b, R b r → P b,
from take b : A, assume H : R b r,
-- We are using Hr to derive ¬ ¬ P b
not_not_elim (and_elimr Hr b H),
have s2 : P r,
from iH r s1,
have s3 : ¬ P r,
from and_eliml Hr,
show false,
from absurd s2 s3)
-- More compact proof
theorem wf_induction2 {A : (Type U)} {R : A → A → Bool} {P : A → Bool} (Hwf : wf R) (iH : ∀ x, (∀ y, R y x → P y) → P x)
: ∀ x, P x
:= by_contradiction (assume N : ¬ ∀ x, P x,
obtain (w : A) (Hw : ¬ P w), from not_forall_elim N,
-- The main "trick" is to define Q x as ¬ P x.
-- Since R is well-founded, there must be a R-minimal element r s.t. Q r (which is ¬ P r)
let Q : A → Bool := λ x, ¬ P x in
obtain (r : A) (Hr : Q r ∧ ∀ b, R b r → ¬ Q b),
from Hwf Q (exists_intro w Hw),
-- Using the inductive hypothesis iH and Hr, we show P r, and derive the contradiction.
have s1 : ∀ b, R b r → P b,
from take b : A, assume H : R b r,
-- We are using Hr to derive ¬ ¬ P b
not_not_elim (and_elimr Hr b H),
absurd (iH r s1) (and_eliml Hr))