Skip to content

Commit 49735fe

Browse files
jmougeotjmougeot
committed
2
1 parent fde1991 commit 49735fe

File tree

1 file changed

+69
-77
lines changed

1 file changed

+69
-77
lines changed

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

Lines changed: 69 additions & 77 deletions
Original file line numberDiff line numberDiff line change
@@ -1,24 +1,19 @@
11
module Relation.Binary.Domain.Definitions where
22

3-
open import Relation.Binary.Core
4-
open import Relation.Binary.Bundles
5-
open import Relation.Binary.Structures
6-
open import Relation.Binary.Lattice.Bundles
7-
open import Relation.Binary.Lattice.Structures
8-
open import Level using (Level; _⊔_; suc; Lift; lift)
3+
open import Relation.Binary.Bundles using (Poset)
4+
open import Level using (Level; _⊔_; suc; Lift; lift; lower)
95
open import Function using (_∘_; id)
106
open import Data.Product using (∃-syntax; _×_; _,_; proj₁; proj₂)
117
open import Relation.Unary using (Pred)
12-
open import Relation.Nullary using (¬_)
138
open import Relation.Binary.PropositionalEquality using (_≡_)
149
open import Relation.Binary.Reasoning.PartialOrder
15-
open import Data.Bool using (Bool; true; false)
10+
open import Data.Bool using (Bool; true; false; if_then_else_)
11+
open import Relation.Binary.Morphism.Structures
1612

1713
private variable
1814
o ℓ ℓ' ℓ₂ : Level
1915
Ix A B : Set o
2016

21-
2217
module _ {c ℓ₁ ℓ₂ : Level} (P : Poset c ℓ₁ ℓ₂) where
2318
open Poset P
2419

@@ -49,14 +44,11 @@ module _ {c ℓ₁ ℓ₂ : Level} {P : Poset c ℓ₁ ℓ₂} {Q : Poset c ℓ
4944
private
5045
module P = Poset P
5146
module Q = Poset Q
52-
53-
record is-monotone (f : P.Carrier → Q.Carrier) : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where
54-
field
55-
monotone : ∀ {x y} → x P.≤ y → f x Q.≤ f y
47+
48+
open IsOrderHomomorphism {_≈₁_ = P._≈_} {_≈₂_ = Q._≈_} {_≲₁_ = P._≤_} {_≲₂_ = Q._≤_}
5649

5750
record is-scott-continuous (f : P.Carrier → Q.Carrier) : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
5851
field
59-
monotone : is-monotone f
6052
preserve-lub : ∀ {Ix : Set c} {g : Ix → P.Carrier}
6153
→ (df : is-directed-family P g)
6254
→ (dlub : ∃[ lub ] ((∀ i → g i P.≤ lub) × ∀ y → (∀ i → g i P.≤ y) → lub P.≤ y))
@@ -65,72 +57,72 @@ module _ {c ℓ₁ ℓ₂ : Level} {P : Poset c ℓ₁ ℓ₂} {Q : Poset c ℓ
6557
dcpo+scott→monotone : (P-dcpo : is-dcpo P)
6658
→ (f : P.Carrier → Q.Carrier)
6759
→ (scott : is-scott-continuous f)
68-
→ ∀ {x y} → x P.≤ y → f x Q.≤ f y
69-
60+
→ ∀ {x y} → x P.≤ y → f x Q.≤ f y
7061
dcpo+scott→monotone P-dcpo f scott {x} {y} p =
71-
Q.trans (ub-proof (lift true)) (least-proof (f y) upper-bound-proof)
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 ))
7264
where
65+
-- The directed family indexed by Lift c Bool: s (lift true) = x, s (lift false) = y
7366
s : Lift c Bool → P.Carrier
74-
s (lift true) = x
75-
s (lift false) = y
76-
77-
s-directed : is-directed-family P s
78-
s-directed .is-directed-family.elt = lift true
79-
s-directed .is-directed-family.semidirected i j =
80-
lift false , p' i , p' j
81-
where
82-
p' : (i : Lift c Bool) → s i P.≤ s (lift false)
83-
p' (lift true) = p
84-
p' (lift false) = P.refl
85-
86-
s-lub = is-dcpo.has-directed-lub P-dcpo s-directed
87-
q-lub = is-scott-continuous.preserve-lub scott s-directed s-lub
88-
89-
ub-proof : ∀ i → f (s i) Q.≤ proj₁ q-lub
90-
ub-proof = proj₁ (proj₂ q-lub)
91-
92-
least-proof : ∀ y → (∀ i → f (s i) Q.≤ y) → proj₁ q-lub Q.≤ y
93-
least-proof = proj₂ (proj₂ q-lub)
94-
95-
upper-bound-proof : ∀ i → f (s i) Q.≤ f y
96-
upper-bound-proof (lift true) = is-monotone.monotone (is-scott-continuous.monotone scott) p
97-
upper-bound-proof (lift false) = Q.refl
98-
99-
monotone∘directed : ∀ {Ix : Set c} → {s : Ix → P.Carrier}
100-
→ (f : P.Carrier → Q.Carrier)
101-
→ (mon : is-monotone f)
102-
→ is-directed-family P s
103-
→ is-directed-family Q (f ∘ s)
104-
monotone∘directed f mon dir .is-directed-family.elt = dir .is-directed-family.elt
105-
monotone∘directed f mon dir .is-directed-family.semidirected i j =
106-
let k , p = dir .is-directed-family.semidirected i j
107-
in k , mon .is-monotone.monotone (proj₁ p) , mon .is-monotone.monotone (proj₂ p)
108-
67+
s (lift b) = if b then x else y
10968

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
11074

111-
{-module _ where
112-
open import Relation.Binary.Bundles using (Poset)
113-
open import Function using (_∘_)
114-
115-
private
116-
module P {o ℓ₁ ℓ₂} (P : Poset o ℓ₁ ℓ₂) = Poset P
117-
module Q {o ℓ₁ ℓ₂} (Q : Poset o ℓ₁ ℓ₂) = Poset Q
118-
module R {o ℓ₁ ℓ₂} (R : Poset o ℓ₁ ℓ₂) = Poset R
119-
120-
scott-id : ∀ {o ℓ₁ ℓ₂} {P : Poset o ℓ₁ ℓ₂}
121-
→ is-scott-continuous (id {A = Poset.Carrier P})
122-
scott-id = record
123-
{ monotone = record { monotone = λ {x} {y} z → x }
124-
; preserve-lub = λ {Ix} {g} df dlub → dlub
125-
}
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+
-- }
126118

127-
scott-∘
128-
: ∀ {o ℓ₁ ℓ₂} {P Q R : Poset o ℓ₁ ℓ₂}
129-
→ (f : Q.Carrier Q → R.Carrier R) (g : P.Carrier P → Q.Carrier Q)
130-
→ is-scott-continuous f → is-scott-continuous g
131-
→ is-scott-continuous (f ∘ g)
132-
scott-∘ {P = P} {Q} {R} f g f-scott g-scott s dir x lub =
133-
f-scott (g ∘ s)
134-
(monotone∘directed g (is-scott-continuous.monotone g-scott) dir)
135-
(g x)
136-
(g-scott s dir x lub)-}
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)

0 commit comments

Comments
 (0)