doc(examples/lean): setoid and group examples
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura
parent
11a2b3016f
commit
acd04d3c2b
2 changed files with 140 additions and 0 deletions
70
examples/lean/group.lean
Normal file
70
examples/lean/group.lean
Normal file
|
|
@ -0,0 +1,70 @@
|
|||
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
|
||||
|
||||
70
examples/lean/setoid.lean
Normal file
70
examples/lean/setoid.lean
Normal file
|
|
@ -0,0 +1,70 @@
|
|||
-- 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)
|
||||
|
||||
Loading…
Reference in a new issue