Skip to content

Commit ee5d9c1

Browse files
jmougeotjmougeot
committed
module ⋃
1 parent 49735fe commit ee5d9c1

File tree

1 file changed

+127
-91
lines changed

1 file changed

+127
-91
lines changed

‎src/Relation/Binary/Domain/Definitions.agda

Lines changed: 127 additions & 91 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
module Relation.Binary.Domain.Definitions where
22

33
open import Relation.Binary.Bundles using (Poset)
4+
open import Relation.Binary.Core using (Rel)
45
open import Level using (Level; _⊔_; suc; Lift; lift; lower)
56
open import Function using (_∘_; id)
67
open import Data.Product using (∃-syntax; _×_; _,_; proj₁; proj₂)
@@ -9,120 +10,155 @@ open import Relation.Binary.PropositionalEquality using (_≡_)
910
open import Relation.Binary.Reasoning.PartialOrder
1011
open import Data.Bool using (Bool; true; false; if_then_else_)
1112
open import Relation.Binary.Morphism.Structures
13+
open import Relation.Binary.Morphism.Structures using (IsOrderHomomorphism)
14+
open import Data.Nat.Properties using (≤-trans)
1215

1316
private variable
14-
o ℓ ℓ' ℓ₂ : Level
17+
o ℓ e o' ℓ' e' ℓ₂ : Level
1518
Ix A B : Set o
1619

20+
module _ where
21+
IsMonotone : (P : Poset o ℓ e) → (Q : Poset o' ℓ' e') → (f : Poset.Carrier P → Poset.Carrier Q) → Set (o ⊔ ℓ ⊔ e ⊔ ℓ' ⊔ e')
22+
IsMonotone P Q f = IsOrderHomomorphism (Poset._≈_ P) (Poset._≈_ Q) (Poset._≤_ P) (Poset._≤_ Q) f
23+
1724
module _ {c ℓ₁ ℓ₂ : Level} (P : Poset c ℓ₁ ℓ₂) where
1825
open Poset P
1926

20-
module PartialOrderReasoning = Relation.Binary.Reasoning.PartialOrder P
21-
22-
is-semidirected-family : ∀ {Ix : Set c} → (f : Ix → Carrier) → Set _
23-
is-semidirected-family f = ∀ i j → ∃[ k ] (f i ≤ f k × f j ≤ f k)
27+
IsSemidirectedFamily : ∀ {Ix : Set c} → (s : Ix → Carrier) → Set _
28+
IsSemidirectedFamily s = ∀ i j → ∃[ k ] (s i ≤ s k × s j ≤ s k)
2429

25-
record is-directed-family {Ix : Set c} (f : Ix → Carrier) : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where
30+
record IsDirectedFamily {Ix : Set c} (s : Ix → Carrier) : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where
2631
no-eta-equality
2732
field
2833
elt : Ix
29-
semidirected : is-semidirected-family f
34+
SemiDirected : IsSemidirectedFamily s
3035

31-
record is-dcpo : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
36+
record IsDCPO : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
3237
field
33-
has-directed-lub : ∀ {Ix : Set c} {f : Ix → Carrier}
34-
→ is-directed-family f
35-
→ ∃[ lub ] ((∀ i → f i ≤ lub) × ∀ y → (∀ i → f i ≤ y) → lub ≤ y)
38+
HasDirectedLub : ∀ {Ix : Set c} {s : Ix → Carrier}
39+
→ IsDirectedFamily s
40+
→ ∃[ lub ] ((∀ i → s i ≤ lub) × ∀ y → (∀ i → s i ≤ y) → lub ≤ y)
3641

37-
record DCPO : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
38-
field
39-
poset : Poset c ℓ₁ ℓ₂
40-
dcpo-str : is-dcpo
42+
record DCPO (c ℓ₁ ℓ₂ : Level) : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
43+
field
44+
poset : Poset c ℓ₁ ℓ₂
45+
DcpoStr : IsDCPO poset
4146

4247
module _ {c ℓ₁ ℓ₂ : Level} {P : Poset c ℓ₁ ℓ₂} {Q : Poset c ℓ₁ ℓ₂} where
4348

4449
private
4550
module P = Poset P
4651
module Q = Poset Q
4752

48-
open IsOrderHomomorphism {_≈₁_ = P._≈_} {_≈₂_ = Q._≈_} {_≲₁_ = P._≤_} {_≲₂_ = Q._≤_}
49-
50-
record is-scott-continuous (f : P.Carrier → Q.Carrier) : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
53+
record IsScottContinuous (f : P.Carrier → Q.Carrier) : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
5154
field
52-
preserve-lub : ∀ {Ix : Set c} {g : Ix → P.Carrier}
53-
→ (df : is-directed-family P g)
54-
→ (dlub : ∃[ lub ] ((∀ i → g i P.≤ lub) × ∀ y → (∀ i → g i P.≤ y) → lub P.≤ y))
55-
→ ∃[ qlub ] ((∀ i → f (g i) Q.≤ qlub) × ∀ y → (∀ i → f (g i) Q.≤ y) → qlub Q.≤ y)
55+
PreserveLub : ∀ {Ix : Set c} {s : Ix → P.Carrier}
56+
→ (dir-s : IsDirectedFamily P s)
57+
→ ∀ lub → ((∀ i → s i P.≤ lub) × ∀ y → (∀ i → s i P.≤ y) → lub P.≤ y)
58+
→ ((∀ i → f (s i) Q.≤ f lub) × ∀ y → (∀ i → f (s i) Q.≤ y) → f lub Q.≤ y)
59+
PreserveEquality : ∀ {x y} → x P.≈ y → f x Q.≈ f y
5660

57-
dcpo+scott→monotone : (P-dcpo : is-dcpo P)
61+
dcpo+scott→monotone : (P-dcpo : IsDCPO P)
5862
→ (f : P.Carrier → Q.Carrier)
59-
→ (scott : is-scott-continuous f)
60-
→ ∀ {x y} → x P.≤ y → f x Q.≤ f y
61-
dcpo+scott→monotone P-dcpo f scott {x} {y} p =
62-
-- f x ≤ f y follows by considering the directed family {x, y} and applying Scott-continuity.
63-
Q.trans (proj₁ (proj₂ f-lub) (lift true)) (Q.reflexive ( fy-is-lub ))
63+
→ (scott : IsScottContinuous f)
64+
→ IsMonotone P Q f
65+
dcpo+scott→monotone P-dcpo f scott = record
66+
{ cong = λ {x} {y} x≈y → IsScottContinuous.PreserveEquality scott x≈y
67+
; mono = λ {x} {y} x≤y → mono-proof x y x≤y
68+
}
6469
where
65-
-- The directed family indexed by Lift c Bool: s (lift true) = x, s (lift false) = y
66-
s : Lift c Bool → P.Carrier
67-
s (lift b) = if b then x else y
68-
69-
-- For any index k, s k ≤ s (lift false) (i.e., x ≤ y and y ≤ y)
70-
sx≤sfalse : ∀ k → s k P.≤ s (lift false)
71-
sx≤sfalse k with lower k
72-
... | true = p
73-
... | false = P.refl
74-
75-
-- s is a directed family: both elements are below y
76-
s-directed : is-directed-family P s
77-
s-directed = record
78-
{ elt = lift false ; semidirected = λ i j → lift false , (sx≤sfalse i , sx≤sfalse j)}
79-
80-
-- The least upper bound of s is y
81-
lub = is-dcpo.has-directed-lub P-dcpo s-directed
82-
83-
-- For any i, s i P.≤ y
84-
h′ : ∀ i → s i P.≤ y
85-
h′ i with lower i
86-
... | true = p
87-
... | false = P.refl
88-
89-
-- y is the least upper bound of s (in the poset sense)
90-
y-is-lub : proj₁ lub P.≈ y
91-
y-is-lub = P.antisym
92-
(proj₂ (proj₂ lub) y (λ i → h′ i))
93-
(proj₁ (proj₂ lub) (lift false))
94-
95-
-- f preserves the lub, so f-lub is the lub of the image family
96-
f-lub = is-scott-continuous.preserve-lub scott s-directed lub
97-
98-
-- f y is the least upper bound of the image family (in the codomain poset)
99-
fy-is-lub : proj₁ f-lub Q.≈ f y
100-
fy-is-lub = {! !}
101-
102-
103-
-- module _ where
104-
-- open import Relation.Binary.Bundles using (Poset)
105-
-- open import Function using (_∘_)
106-
107-
-- private
108-
-- module P {o ℓ₁ ℓ₂} (P : Poset o ℓ₁ ℓ₂) = Poset P
109-
-- module Q {o ℓ₁ ℓ₂} (Q : Poset o ℓ₁ ℓ₂) = Poset Q
110-
-- module R {o ℓ₁ ℓ₂} (R : Poset o ℓ₁ ℓ₂) = Poset R
111-
112-
-- scott-id : ∀ {o ℓ₁ ℓ₂} {P : Poset o ℓ₁ ℓ₂} → is-scott-continuous {P = P} {Q = P} id
113-
-- -- scott-id : ∀ {o ℓ₁ ℓ₂} {P : Poset o ℓ₁ ℓ₂} → is-scott-continuous (id {A = Poset.Carrier P})
114-
-- scott-id = record
115-
-- { monotone = record { monotone = λ {x} {y} p → p }
116-
-- ; preserve-lub = λ {Ix} {g} df dlub → dlub
117-
-- }
70+
mono-proof : ∀ x y → x P.≤ y → f x Q.≤ f y
71+
mono-proof x y x≤y = proj₁ fs-lub (lift true)
72+
where
73+
s : Lift c Bool → P.Carrier
74+
s (lift b) = if b then x else y
75+
76+
sx≤sfalse : ∀ b → s b P.≤ s (lift false)
77+
sx≤sfalse (lift true) = x≤y
78+
sx≤sfalse (lift false) = P.refl
79+
80+
s-directed : IsDirectedFamily P s
81+
s-directed = record
82+
{ elt = lift true
83+
; SemiDirected = λ i j → (lift false , sx≤sfalse i , sx≤sfalse j)
84+
}
85+
86+
s-lub : P.Carrier × ((∀ i → s i P.≤ y) × (∀ z → (∀ i → s i P.≤ z) → y P.≤ z))
87+
s-lub = y , (sx≤sfalse , λ z lt → lt (lift false))
88+
89+
fs-lub = IsScottContinuous.PreserveLub scott
90+
s-directed y (sx≤sfalse , λ z lt → lt (lift false))
91+
92+
monotone∘directed : ∀ {Ix : Set c} {s : Ix → P.Carrier}
93+
→ (f : P.Carrier → Q.Carrier)
94+
→ IsMonotone P Q f
95+
→ IsDirectedFamily P s
96+
→ IsDirectedFamily Q (f ∘ s)
97+
monotone∘directed f ismonotone dir = record
98+
{ elt = IsDirectedFamily.elt dir
99+
; SemiDirected = λ i j →
100+
let (k , s[i]≤s[k] , s[j]≤s[k]) = IsDirectedFamily.SemiDirected dir i j
101+
in k , IsOrderHomomorphism.mono ismonotone s[i]≤s[k] , IsOrderHomomorphism.mono ismonotone s[j]≤s[k]
102+
}
103+
104+
module _ where
105+
106+
ScottId : ∀ {c ℓ₁ ℓ₂} {P : Poset c ℓ₁ ℓ₂} → IsScottContinuous {P = P} {Q = P} id
107+
ScottId = record
108+
{ PreserveLub = λ dir-s lub z → z
109+
; PreserveEquality = λ z → z }
118110

119-
-- scott-∘
120-
-- : ∀ {o ℓ₁ ℓ₂} {P Q R : Poset o ℓ₁ ℓ₂}
121-
-- → (f : Q.Carrier Q → R.Carrier R) (g : P.Carrier P → Q.Carrier Q)
122-
-- → is-scott-continuous f → is-scott-continuous g
123-
-- → is-scott-continuous (f ∘ g)
124-
-- scott-∘ {P = P} {Q} {R} f g f-scott g-scott s dir x lub =
125-
-- f-scott (g ∘ s)
126-
-- (monotone∘directed g (is-scott-continuous.monotone g-scott) dir)
127-
-- (g x)
128-
-- (g-scott s dir x lub)
111+
scott-∘ : ∀ {c ℓ₁ ℓ₂} {P Q R : Poset c ℓ₁ ℓ₂}
112+
→ (f : Poset.Carrier R → Poset.Carrier Q) (g : Poset.Carrier P → Poset.Carrier R)
113+
→ IsScottContinuous {P = R} {Q = Q} f → IsScottContinuous {P = P} {Q = R} g
114+
→ IsMonotone R Q f → IsMonotone P R g
115+
→ IsScottContinuous {P = P} {Q = Q} (f ∘ g)
116+
scott-∘ f g scottf scottg monotonef monotoneg = record
117+
{ PreserveLub = λ dir-s lub z → IsScottContinuous.PreserveLub scottf
118+
(monotone∘directed g monotoneg dir-s)
119+
(g lub) ( IsScottContinuous.PreserveLub scottg dir-s lub z)
120+
; PreserveEquality = λ {x} {y} z → IsScottContinuous.PreserveEquality scottf
121+
(IsScottContinuous.PreserveEquality scottg z)
122+
}
123+
124+
-- Module for the DCPO record
125+
module _ {c ℓ₁ ℓ₂} (D : DCPO c ℓ₁ ℓ₂) where
126+
open DCPO D public
127+
128+
posetD : Poset c ℓ₁ ℓ₂
129+
posetD = poset
130+
131+
open Poset posetD
132+
open import Relation.Binary.Reasoning.PartialOrder posetD public
133+
134+
dcpoD : IsDCPO posetD
135+
dcpoD = DcpoStr
136+
137+
⋃ : ∀ {Ix : Set c} (s : Ix → Carrier) → (dir : IsDirectedFamily posetD s) → Carrier
138+
⋃ s dir = proj₁ (IsDCPO.HasDirectedLub dcpoD dir)
139+
140+
module ⋃ {Ix : Set c} (s : Ix → Carrier) (dir : IsDirectedFamily posetD s) where
141+
fam≤lub : ∀ ix → s ix ≤ ⋃ s dir
142+
fam≤lub ix = proj₁ (proj₂ (IsDCPO.HasDirectedLub dcpoD dir)) ix
143+
144+
least : ∀ ub → (∀ ix → s ix ≤ ub) → ⋃ s dir ≤ ub
145+
least ub p = proj₂ (proj₂ (IsDCPO.HasDirectedLub dcpoD dir)) ub p
146+
147+
⋃-pointwise : ∀ {Ix} {s s' : Ix → Carrier}
148+
→ {fam : IsDirectedFamily posetD s} {fam' : IsDirectedFamily posetD s'}
149+
→ (∀ ix → s ix ≤ s' ix)
150+
→ ⋃ s fam ≤ ⋃ s' fam'
151+
⋃-pointwise {s = s} {s'} {fam} {fam'} p = ⋃.least s fam (⋃ s' fam') λ ix →
152+
trans (p ix) (⋃.fam≤lub s' fam' ix)
153+
154+
module Scott {c} {ℓ₁} {ℓ₂} {D E : DCPO c ℓ₁ ℓ₂}
155+
(f : Poset.Carrier (DCPO.poset D) → Poset.Carrier (DCPO.poset E))
156+
(mono : IsMonotone (DCPO.poset D) (DCPO.poset E) f) where``
157+
158+
private
159+
module D = DCPO D
160+
module E = DCPO E
161+
162+
pres-directed-lub : ∀ {Ix} (s : Ix → Carrier) → is-directed-family D.poset s
163+
→ ∀ x → is-lub (D .fst) s x → is-lub (E .fst) (apply f ⊙ s) (f · x)
164+

0 commit comments

Comments
 (0)