doc(examples/lean): proof of concept
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura
parent
56ad1c1728
commit
1796c2b992
1 changed files with 113 additions and 0 deletions
113
examples/lean/setoid2.lean
Normal file
113
examples/lean/setoid2.lean
Normal file
|
|
@ -0,0 +1,113 @@
|
|||
-- 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)
|
||||
Loading…
Reference in a new issue