From 4486fd0108d05cceb9636d4e9a72d72ddfa67cf6 Mon Sep 17 00:00:00 2001 From: Jacques Date: Mon, 26 May 2025 19:07:22 -0400 Subject: [PATCH 01/12] Definitons of domain theory --- CHANGELOG.md | 4 ++ src/Relation/Binary/Domain.agda | 16 +++++ src/Relation/Binary/Domain/Bundles.agda | 53 +++++++++++++++++ src/Relation/Binary/Domain/Definitions.agda | 28 +++++++++ src/Relation/Binary/Domain/Structures.agda | 66 +++++++++++++++++++++ 5 files changed, 167 insertions(+) create mode 100644 src/Relation/Binary/Domain.agda create mode 100644 src/Relation/Binary/Domain/Bundles.agda create mode 100644 src/Relation/Binary/Domain/Definitions.agda create mode 100644 src/Relation/Binary/Domain/Structures.agda diff --git a/CHANGELOG.md b/CHANGELOG.md index 2959d3d6ce..4722c81ba2 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -123,6 +123,10 @@ New modules * `Data.Sign.Show` to show a sign +* Added a new domain theory section to the library under `Relation.Binary.Domain.*`: + - Introduced new modules and bundles for domain theory, including `DCPO`, `Lub`, and `ScottContinuous`. + - All files for domain theory are now available in `src/Relation/Binary/Domain/`. + Additions to existing modules ----------------------------- diff --git a/src/Relation/Binary/Domain.agda b/src/Relation/Binary/Domain.agda new file mode 100644 index 0000000000..812e74a601 --- /dev/null +++ b/src/Relation/Binary/Domain.agda @@ -0,0 +1,16 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Order-theoretic Domains +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Relation.Binary.Domain where + +------------------------------------------------------------------------ +-- Re-export various components of the Domain hierarchy + +open import Relation.Binary.Domain.Definitions public +open import Relation.Binary.Domain.Structures public +open import Relation.Binary.Domain.Bundles public diff --git a/src/Relation/Binary/Domain/Bundles.agda b/src/Relation/Binary/Domain/Bundles.agda new file mode 100644 index 0000000000..7b84781ee6 --- /dev/null +++ b/src/Relation/Binary/Domain/Bundles.agda @@ -0,0 +1,53 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Bundles for domain theory +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Relation.Binary.Domain.Bundles where + +open import Level using (Level; _⊔_; suc) +open import Relation.Binary.Bundles using (Poset) +open import Relation.Binary.Domain.Structures +open import Relation.Binary.Domain.Definitions + +private + variable + o ℓ e o' ℓ' e' ℓ₂ : Level + Ix A B : Set o + +------------------------------------------------------------------------ +-- DCPOs +------------------------------------------------------------------------ + +record DCPO (c ℓ₁ ℓ₂ : Level) : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where + field + poset : Poset c ℓ₁ ℓ₂ + DcpoStr : IsDCPO poset + + open Poset poset public + open IsDCPO DcpoStr public + +------------------------------------------------------------------------ +-- Scott-continuous functions +------------------------------------------------------------------------ + +record ScottContinuous {c ℓ₁ ℓ₂ : Level} {P : Poset c ℓ₁ ℓ₂} {Q : Poset c ℓ₁ ℓ₂} : + Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where + field + f : Poset.Carrier P → Poset.Carrier Q + Scottfunction : IsScottContinuous {P = P} {Q = Q} f + +------------------------------------------------------------------------ +-- Lubs +------------------------------------------------------------------------ + +record Lub {c ℓ₁ ℓ₂ : Level} {P : Poset c ℓ₁ ℓ₂} {Ix : Set c} (s : Ix → Poset.Carrier P) : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where + private + module P = Poset P + field + lub : P.Carrier + is-upperbound : ∀ i → P._≤_ (s i) lub + is-least : ∀ y → (∀ i → P._≤_ (s i) y) → P._≤_ lub y diff --git a/src/Relation/Binary/Domain/Definitions.agda b/src/Relation/Binary/Domain/Definitions.agda new file mode 100644 index 0000000000..828553b6af --- /dev/null +++ b/src/Relation/Binary/Domain/Definitions.agda @@ -0,0 +1,28 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Definitions for domain theory +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Relation.Binary.Domain.Definitions where + +open import Data.Product using (∃-syntax; _×_; _,_) +open import Level using (Level; _⊔_) +open import Relation.Binary.Bundles using (Poset) +open import Relation.Binary.Morphism.Structures using (IsOrderHomomorphism) + +private + variable + c o ℓ e o' ℓ' e' ℓ₁ ℓ₂ : Level + Ix A B : Set o + P : Poset c ℓ e + +------------------------------------------------------------------------ +-- Directed families +------------------------------------------------------------------------ + +IsSemidirectedFamily : (P : Poset c ℓ₁ ℓ₂) → ∀ {Ix : Set c} → (s : Ix → Poset.Carrier P) → Set _ +IsSemidirectedFamily P {Ix} s = ∀ i j → ∃[ k ] (Poset._≤_ P (s i) (s k) × Poset._≤_ P (s j) (s k)) + diff --git a/src/Relation/Binary/Domain/Structures.agda b/src/Relation/Binary/Domain/Structures.agda new file mode 100644 index 0000000000..5d6d397181 --- /dev/null +++ b/src/Relation/Binary/Domain/Structures.agda @@ -0,0 +1,66 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Structures for domain theory +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Relation.Binary.Domain.Structures where + +open import Data.Product using (_×_; _,_) +open import Data.Nat.Properties using (≤-trans) +open import Function using (_∘_) +open import Level using (Level; _⊔_; suc) +open import Relation.Binary.Bundles using (Poset) +open import Relation.Binary.Domain.Definitions +open import Relation.Binary.Morphism.Structures using (IsOrderHomomorphism) + +private variable + o ℓ e o' ℓ' e' ℓ₂ : Level + Ix A B : Set o + +module _ {c ℓ₁ ℓ₂ : Level} (P : Poset c ℓ₁ ℓ₂) where + open Poset P + + record IsDirectedFamily {Ix : Set c} (s : Ix → Carrier) : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where + no-eta-equality + field + elt : Ix + SemiDirected : IsSemidirectedFamily P s + + record IsLub {Ix : Set c} (s : Ix → Carrier) (lub : Carrier) : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where + field + is-upperbound : ∀ i → s i ≤ lub + is-least : ∀ y → (∀ i → s i ≤ y) → lub ≤ y + + record IsDCPO : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where + field + ⋁ : ∀ {Ix : Set c} + → (s : Ix → Carrier) + → IsDirectedFamily s + → Carrier + ⋁-isLub : ∀ {Ix : Set c} + → (s : Ix → Carrier) + → (dir : IsDirectedFamily s) + → IsLub s (⋁ s dir) + + module _ {Ix : Set c} {s : Ix → Carrier} {dir : IsDirectedFamily s} where + open IsLub (⋁-isLub s dir) + renaming (is-upperbound to ⋁-≤; is-least to ⋁-least) + public + +module _ {c ℓ₁ ℓ₂ : Level} {P : Poset c ℓ₁ ℓ₂} {Q : Poset c ℓ₁ ℓ₂} where + + private + module P = Poset P + module Q = Poset Q + + record IsScottContinuous (f : P.Carrier → Q.Carrier) : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where + field + PreserveLub : ∀ {Ix : Set c} {s : Ix → P.Carrier} + → (dir : IsDirectedFamily P s) + → (lub : P.Carrier) + → IsLub P s lub + → IsLub Q (f ∘ s) (f lub) + PreserveEquality : ∀ {x y} → x P.≈ y → f x Q.≈ f y From 872997511e1904fe9e85abbfaca010d088e6eb30 Mon Sep 17 00:00:00 2001 From: Jacques Date: Mon, 26 May 2025 19:14:37 -0400 Subject: [PATCH 02/12] add domain properties --- src/Relation/Binary/Properties/Domain.agda | 180 +++++++++++++++++++++ 1 file changed, 180 insertions(+) create mode 100644 src/Relation/Binary/Properties/Domain.agda diff --git a/src/Relation/Binary/Properties/Domain.agda b/src/Relation/Binary/Properties/Domain.agda new file mode 100644 index 0000000000..adb09a12ee --- /dev/null +++ b/src/Relation/Binary/Properties/Domain.agda @@ -0,0 +1,180 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Properties satisfied by directed complete partial orders (DCPOs) +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Relation.Binary.Properties.Domain where + +open import Relation.Binary.Bundles using (Poset) +open import Level using (Level; Lift; lift) +open import Function using (_∘_; id) +open import Data.Product using (_,_) +open import Data.Bool using (Bool; true; false; if_then_else_) +open import Relation.Binary.Domain.Bundles using (DCPO) +open import Relation.Binary.Domain.Structures + using (IsDirectedFamily; IsDCPO; IsLub; IsScottContinuous) +open import Relation.Binary.Morphism.Structures using (IsOrderHomomorphism) + +private variable + c ℓ₁ ℓ₂ o ℓ : Level + Ix A B : Set o + +module _ {c ℓ₁ ℓ₂} {P : Poset c ℓ₁ ℓ₂} {D : DCPO c ℓ₁ ℓ₂ } where + private + module D = DCPO D + + uniqueLub : ∀ {Ix} {s : Ix → D.Carrier} + → (x y : D.Carrier) → IsLub D.poset s x → IsLub D.poset s y + → x D.≈ y + uniqueLub x y x-lub y-lub = D.antisym + (IsLub.is-least x-lub y (IsLub.is-upperbound y-lub)) + (IsLub.is-least y-lub x (IsLub.is-upperbound x-lub)) + + is-lub-cong : ∀ {Ix} {s : Ix → D.Carrier} + → (x y : D.Carrier) + → x D.≈ y + → IsLub D.poset s x → IsLub D.poset s y + is-lub-cong x y x≈y x-lub = record + { is-upperbound = λ i → D.trans (IsLub.is-upperbound x-lub i) (D.reflexive x≈y) + ; is-least = λ z ub → D.trans (D.reflexive (D.Eq.sym x≈y)) + (IsLub.is-least x-lub z (λ i → D.trans (ub i) (D.reflexive D.Eq.refl))) + } + +module _ {c ℓ₁ ℓ₂ : Level} {P : Poset c ℓ₁ ℓ₂} {Q : Poset c ℓ₁ ℓ₂} where + + private + module P = Poset P + module Q = Poset Q + + dcpo+scott→monotone : (P-dcpo : IsDCPO P) + → (f : P.Carrier → Q.Carrier) + → (scott : IsScottContinuous f) + → IsOrderHomomorphism (Poset._≈_ P) (Poset._≈_ Q) (Poset._≤_ P) (Poset._≤_ Q) f + dcpo+scott→monotone P-dcpo f scott = record + { cong = λ {x} {y} x≈y → IsScottContinuous.PreserveEquality scott x≈y + ; mono = λ {x} {y} x≤y → mono-proof x y x≤y + } + where + mono-proof : ∀ x y → x P.≤ y → f x Q.≤ f y + mono-proof x y x≤y = IsLub.is-upperbound fs-lub (lift true) + where + s : Lift c Bool → P.Carrier + s (lift b) = if b then x else y + + sx≤sfalse : ∀ b → s b P.≤ s (lift false) + sx≤sfalse (lift true) = x≤y + sx≤sfalse (lift false) = P.refl + + s-directed : IsDirectedFamily P s + s-directed = record + { elt = lift true + ; SemiDirected = λ i j → (lift false , sx≤sfalse i , sx≤sfalse j) + } + + s-lub : IsLub P s y + s-lub = record + { is-upperbound = sx≤sfalse + ; is-least = λ z proof → proof (lift false) + } + + fs-lub : IsLub Q (f ∘ s) (f y) + fs-lub = IsScottContinuous.PreserveLub scott s-directed y s-lub + + monotone∘directed : ∀ {Ix : Set c} {s : Ix → P.Carrier} + → (f : P.Carrier → Q.Carrier) + → IsOrderHomomorphism (Poset._≈_ P) (Poset._≈_ Q) (Poset._≤_ P) (Poset._≤_ Q) f + → IsDirectedFamily P s + → IsDirectedFamily Q (f ∘ s) + monotone∘directed f ismonotone dir = record + { elt = IsDirectedFamily.elt dir + ; SemiDirected = λ i j → + let (k , s[i]≤s[k] , s[j]≤s[k]) = IsDirectedFamily.SemiDirected dir i j + in k , IsOrderHomomorphism.mono ismonotone s[i]≤s[k] , IsOrderHomomorphism.mono ismonotone s[j]≤s[k] + } + +module _ where + + ScottId : ∀ {c ℓ₁ ℓ₂} {P : Poset c ℓ₁ ℓ₂} → IsScottContinuous {P = P} {Q = P} id + ScottId = record + { PreserveLub = λ dir lub z → z + ; PreserveEquality = λ z → z } + + scott-∘ : ∀ {c ℓ₁ ℓ₂} {P Q R : Poset c ℓ₁ ℓ₂} + → (f : Poset.Carrier R → Poset.Carrier Q) (g : Poset.Carrier P → Poset.Carrier R) + → IsScottContinuous {P = R} {Q = Q} f → IsScottContinuous {P = P} {Q = R} g + → IsOrderHomomorphism (Poset._≈_ P) (Poset._≈_ R) (Poset._≤_ P) (Poset._≤_ R) g + → IsScottContinuous {P = P} {Q = Q} (f ∘ g) + scott-∘ f g scottf scottg monog = record + { PreserveLub = λ dir lub z → f.PreserveLub + (monotone∘directed g monog dir) + (g lub) + (g.PreserveLub dir lub z) + ; PreserveEquality = λ {x} {y} z → + f.PreserveEquality (g.PreserveEquality z) + } + where + module f = IsScottContinuous scottf + module g = IsScottContinuous scottg + +module _ {c ℓ₁ ℓ₂} {P : Poset c ℓ₁ ℓ₂} (D : DCPO c ℓ₁ ℓ₂) where + private + module D = DCPO D + + open import Relation.Binary.Reasoning.PartialOrder D.poset + + ⋃-pointwise : ∀ {Ix} {s s' : Ix → D.Carrier} + → {fam : IsDirectedFamily D.poset s} {fam' : IsDirectedFamily D.poset s'} + → (∀ ix → s ix D.≤ s' ix) + → D.⋁ s fam D.≤ D.⋁ s' fam' + ⋃-pointwise {s = s} {s'} {fam} {fam'} p = + D.⋁-least (D.⋁ s' fam') λ i → D.trans (p i) (D.⋁-≤ i) + +module Scott + {c ℓ₁ ℓ₂} + {P : Poset c ℓ₁ ℓ₂} + {D E : DCPO c ℓ₁ ℓ₂} + (let module D = DCPO D) + (let module E = DCPO E) + (f : D.Carrier → E.Carrier) + (isScott : IsScottContinuous {P = D.poset} {Q = E.poset} f) + (mono : IsOrderHomomorphism (Poset._≈_ D.poset) (Poset._≈_ E.poset) + (Poset._≤_ D.poset) (Poset._≤_ E.poset) f) + where + + open DCPO D + open DCPO E + + pres-⋁ + : ∀ {Ix} (s : Ix → D.Carrier) → (dir : IsDirectedFamily D.poset s) + → f (D.⋁ s dir) E.≈ E.⋁ (f ∘ s) (monotone∘directed f mono dir) + pres-⋁ s dir = E.antisym + (IsLub.is-least + (IsScottContinuous.PreserveLub isScott dir (D.⋁ s dir) (D.⋁-isLub s dir)) + (E.⋁ (f ∘ s) (monotone∘directed f mono dir)) + E.⋁-≤ + ) + (IsLub.is-least + (E.⋁-isLub (f ∘ s) (monotone∘directed f mono dir)) + (f (D.⋁ s dir)) + (λ i → IsOrderHomomorphism.mono mono (D.⋁-≤ i)) + ) + +module _ {c ℓ₁ ℓ₂} {P : Poset c ℓ₁ ℓ₂} {D E : DCPO c ℓ₁ ℓ₂} where + private + module D = DCPO D + module E = DCPO E + + to-scott : (f : D.Carrier → E.Carrier) + → IsOrderHomomorphism (Poset._≈_ D.poset) (Poset._≈_ E.poset) + (Poset._≤_ D.poset) (Poset._≤_ E.poset) f + → (∀ {Ix} (s : Ix → D.Carrier) (dir : IsDirectedFamily D.poset s) + → IsLub E.poset (f ∘ s) (f (D.⋁ s dir))) + → IsScottContinuous {P = D.poset} {Q = E.poset} f + to-scott f mono pres-⋁ = record + { PreserveLub = λ dir lub x → is-lub-cong {P = E.poset} {D = E} (f (D.⋁ _ dir)) (f lub) + (IsOrderHomomorphism.cong mono (uniqueLub {P = E.poset} {D = D} (D.⋁ _ dir) lub (D.⋁-isLub _ dir) x)) + (pres-⋁ _ dir) + ; PreserveEquality = IsOrderHomomorphism.cong mono } From 34be6b0cba4904ef0bca2d06bd678c08c2a1bf98 Mon Sep 17 00:00:00 2001 From: Jacques Date: Tue, 3 Jun 2025 14:14:03 -0400 Subject: [PATCH 03/12] 1st review --- CHANGELOG.md | 2 +- src/Padrightpropertiesdraft.agda | 109 ++++++++++++++++++++ src/Relation/Binary/Domain/Bundles.agda | 30 +++--- src/Relation/Binary/Domain/Definitions.agda | 24 +++-- src/Relation/Binary/Domain/Structures.agda | 60 ++++++----- 5 files changed, 176 insertions(+), 49 deletions(-) create mode 100644 src/Padrightpropertiesdraft.agda diff --git a/CHANGELOG.md b/CHANGELOG.md index 4722c81ba2..055fbf6250 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -124,7 +124,7 @@ New modules * `Data.Sign.Show` to show a sign * Added a new domain theory section to the library under `Relation.Binary.Domain.*`: - - Introduced new modules and bundles for domain theory, including `DCPO`, `Lub`, and `ScottContinuous`. + - Introduced new modules and bundles for domain theory, including `DirectedCompletePartialOrder`, `Lub`, and `ScottContinuous`. - All files for domain theory are now available in `src/Relation/Binary/Domain/`. Additions to existing modules diff --git a/src/Padrightpropertiesdraft.agda b/src/Padrightpropertiesdraft.agda new file mode 100644 index 0000000000..b7649b48d8 --- /dev/null +++ b/src/Padrightpropertiesdraft.agda @@ -0,0 +1,109 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Properties of padRight for Vec +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Padrightpropertiesdraft where + +open import Data.Fin.Base using (Fin; zero; suc; inject≤) +open import Data.Nat.Base using (ℕ; zero; suc; _+_; _≤_; z≤n; s≤s; _∸_) +open import Data.Nat.Properties using (≤-refl; ≤-trans; m≤m+n; m+n∸m≡n) +open import Data.Vec.Base +open import Data.Vec.Properties using (map-replicate; zipWith-replicate; padRight-trans) +open import Function.Base using (_∘_; _$_) +open import Level using (Level) +open import Relation.Binary.PropositionalEquality.Core + using (_≡_; refl; cong; sym; trans; subst) +open import Relation.Binary.PropositionalEquality.Properties + using (module ≡-Reasoning) + +private + variable + a b c : Level + A : Set a + B : Set b + C : Set c + m n p : ℕ + + +------------------------------------------------------------------------ +-- Interaction with map + +padRight-map : ∀ (f : A → B) (m≤n : m ≤ n) (a : A) (xs : Vec A m) → + map f (padRight m≤n a xs) ≡ padRight m≤n (f a) (map f xs) +padRight-map f z≤n a [] = map-replicate f a _ +padRight-map f (s≤s m≤n) a (x ∷ xs) = cong (f x ∷_) (padRight-map f m≤n a xs) + +------------------------------------------------------------------------ +-- Interaction with lookup + +padRight-lookup : ∀ (m≤n : m ≤ n) (a : A) (xs : Vec A m) (i : Fin m) → + lookup (padRight m≤n a xs) (inject≤ i m≤n) ≡ lookup xs i +padRight-lookup (s≤s m≤n) a (x ∷ xs) zero = refl +padRight-lookup (s≤s m≤n) a (x ∷ xs) (suc i) = padRight-lookup m≤n a xs i + +------------------------------------------------------------------------ +-- Interaction with zipWith + +-- When both vectors have the same original length +padRight-zipWith : ∀ (f : A → B → C) (m≤n : m ≤ n) (a : A) (b : B) + (xs : Vec A m) (ys : Vec B m) → + zipWith f (padRight m≤n a xs) (padRight m≤n b ys) ≡ + padRight m≤n (f a b) (zipWith f xs ys) +padRight-zipWith f z≤n a b [] [] = zipWith-replicate f a b +padRight-zipWith f (s≤s m≤n) a b (x ∷ xs) (y ∷ ys) = + cong (f x y ∷_) (padRight-zipWith f m≤n a b xs ys) + +-- When vectors have different original lengths +padRight-zipWith₁ : ∀ {p} (f : A → B → C) (m≤n : m ≤ n) (p≤m : p ≤ m) + (a : A) (b : B) (xs : Vec A m) (ys : Vec B p) → + zipWith f (padRight m≤n a xs) (padRight (≤-trans p≤m m≤n) b ys) ≡ + padRight m≤n (f a b) (zipWith f xs (padRight p≤m b ys)) +padRight-zipWith₁ {p} f m≤n p≤m a b xs ys = + trans (cong (zipWith f (padRight m≤n a xs)) (padRight-trans p≤m m≤n b ys)) + (padRight-zipWith f m≤n a b xs (padRight p≤m b ys)) + +------------------------------------------------------------------------ +-- Interaction with take and drop + +padRight-take : ∀ {p} (m≤n : m ≤ n) (a : A) (xs : Vec A m) (n≡m+p : n ≡ m + p) → + take m (subst (Vec A) n≡m+p (padRight m≤n a xs)) ≡ xs +padRight-take {m = zero} z≤n a [] refl = refl +padRight-take {m = suc m} {p = p} (s≤s m≤n) a (x ∷ xs) refl = + cong (x ∷_) (padRight-take {p = p} m≤n a xs refl) + +-- Helper lemma: commuting subst with drop +subst-drop : ∀ {m n p : ℕ} {A : Set} (eq : n ≡ m + p) (xs : Vec A n) → + drop m (subst (Vec A) eq xs) ≡ subst (Vec A) (cong (_∸ m) eq) (drop m xs) +subst-drop refl xs = refl + +-- Helper lemma: dropping from padded vector gives replicate +drop-padRight : ∀ {m n p} (m≤n : m ≤ n) (a : A) (xs : Vec A m) → + n ≡ m + p → drop m (padRight m≤n a xs) ≡ replicate p a +drop-padRight {m = zero} z≤n a [] refl = refl +drop-padRight {m = suc m} {p = p} (s≤s m≤n) a (x ∷ xs) refl = + drop-padRight {p = p} m≤n a xs refl + +padRight-drop : ∀ {p} (m≤n : m ≤ n) (a : A) (xs : Vec A m) (n≡m+p : n ≡ m + p) → + drop m (subst (Vec A) n≡m+p (padRight m≤n a xs)) ≡ replicate p a +padRight-drop {p = p} m≤n a xs n≡m+p = + trans (subst-drop n≡m+p (padRight m≤n a xs)) + (cong (subst (Vec A) (cong (_∸ _) n≡m+p)) (drop-padRight m≤n a xs n≡m+p)) + +------------------------------------------------------------------------ +-- Interaction with updateAt + +padRight-updateAt : ∀ (m≤n : m ≤ n) (xs : Vec A m) (f : A → A) (i : Fin m) (x : A) → + updateAt (padRight m≤n x xs) (inject≤ i m≤n) f ≡ + padRight m≤n x (updateAt xs i f) +padRight-updateAt (s≤s m≤n) (y ∷ xs) f zero x = refl +padRight-updateAt (s≤s m≤n) (y ∷ xs) f (suc i) x = + cong (y ∷_) (padRight-updateAt m≤n xs f i x) + + + + + diff --git a/src/Relation/Binary/Domain/Bundles.agda b/src/Relation/Binary/Domain/Bundles.agda index 7b84781ee6..6c103182d3 100644 --- a/src/Relation/Binary/Domain/Bundles.agda +++ b/src/Relation/Binary/Domain/Bundles.agda @@ -19,16 +19,22 @@ private Ix A B : Set o ------------------------------------------------------------------------ --- DCPOs +-- Directed Complete Partial Orders ------------------------------------------------------------------------ -record DCPO (c ℓ₁ ℓ₂ : Level) : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where +record DirectedFamily {c ℓ₁ ℓ₂ : Level} {P : Poset c ℓ₁ ℓ₂} {B : Set c} (f : B → Poset.Carrier P) : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where field - poset : Poset c ℓ₁ ℓ₂ - DcpoStr : IsDCPO poset + isDirectedFamily : IsDirectedFamily P f + + open IsDirectedFamily isDirectedFamily public + +record DirectedCompletePartialOrder (c ℓ₁ ℓ₂ : Level) : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where + field + poset : Poset c ℓ₁ ℓ₂ + isDirectedCompletePartialOrder : IsDirectedCompletePartialOrder poset open Poset poset public - open IsDCPO DcpoStr public + open IsDirectedCompletePartialOrder isDirectedCompletePartialOrder public ------------------------------------------------------------------------ -- Scott-continuous functions @@ -37,17 +43,15 @@ record DCPO (c ℓ₁ ℓ₂ : Level) : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) wher record ScottContinuous {c ℓ₁ ℓ₂ : Level} {P : Poset c ℓ₁ ℓ₂} {Q : Poset c ℓ₁ ℓ₂} : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where field - f : Poset.Carrier P → Poset.Carrier Q - Scottfunction : IsScottContinuous {P = P} {Q = Q} f + f : Poset.Carrier P → Poset.Carrier Q + isScottContinuous : IsScottContinuous {P = P} {Q = Q} f ------------------------------------------------------------------------ -- Lubs ------------------------------------------------------------------------ -record Lub {c ℓ₁ ℓ₂ : Level} {P : Poset c ℓ₁ ℓ₂} {Ix : Set c} (s : Ix → Poset.Carrier P) : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where - private - module P = Poset P +record Lub {c ℓ₁ ℓ₂ : Level} {P : Poset c ℓ₁ ℓ₂} {B : Set c} (f : B → Poset.Carrier P) : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where + open Poset P field - lub : P.Carrier - is-upperbound : ∀ i → P._≤_ (s i) lub - is-least : ∀ y → (∀ i → P._≤_ (s i) y) → P._≤_ lub y + lub : Carrier + isLub : IsLub P f lub diff --git a/src/Relation/Binary/Domain/Definitions.agda b/src/Relation/Binary/Domain/Definitions.agda index 828553b6af..a3322e87e0 100644 --- a/src/Relation/Binary/Domain/Definitions.agda +++ b/src/Relation/Binary/Domain/Definitions.agda @@ -4,25 +4,35 @@ -- Definitions for domain theory ------------------------------------------------------------------------ + + + {-# OPTIONS --cubical-compatible --safe #-} module Relation.Binary.Domain.Definitions where open import Data.Product using (∃-syntax; _×_; _,_) open import Level using (Level; _⊔_) -open import Relation.Binary.Bundles using (Poset) -open import Relation.Binary.Morphism.Structures using (IsOrderHomomorphism) +open import Relation.Binary.Core using (Rel) private variable - c o ℓ e o' ℓ' e' ℓ₁ ℓ₂ : Level - Ix A B : Set o - P : Poset c ℓ e + a b ℓ : Level + A B : Set a ------------------------------------------------------------------------ -- Directed families ------------------------------------------------------------------------ -IsSemidirectedFamily : (P : Poset c ℓ₁ ℓ₂) → ∀ {Ix : Set c} → (s : Ix → Poset.Carrier P) → Set _ -IsSemidirectedFamily P {Ix} s = ∀ i j → ∃[ k ] (Poset._≤_ P (s i) (s k) × Poset._≤_ P (s j) (s k)) +-- IsSemidirectedFamily : (P : Poset c ℓ₁ ℓ₂) → ∀ {Ix : Set c} → (s : Ix → Poset.Carrier P) → Set _ +-- IsSemidirectedFamily P {Ix} s = ∀ i j → ∃[ k ] (Poset._≤_ P (s i) (s k) × Poset._≤_ P (s j) (s k)) + +semidirected : {A : Set a} → Rel A ℓ → (B : Set b) → (B → A) → Set _ +semidirected _≤_ B f = ∀ i j → ∃[ k ] (f i ≤ f k × f j ≤ f k) + +------------------------------------------------------------------------ +-- Least upper bounds +------------------------------------------------------------------------ +leastupperbound : {A : Set a} → Rel A ℓ → (B : Set b) → (B → A) → A → Set _ +leastupperbound _≤_ B f lub = (∀ i → f i ≤ lub) × (∀ y → (∀ i → f i ≤ y) → lub ≤ y) diff --git a/src/Relation/Binary/Domain/Structures.agda b/src/Relation/Binary/Domain/Structures.agda index 5d6d397181..dfbe85f3c6 100644 --- a/src/Relation/Binary/Domain/Structures.agda +++ b/src/Relation/Binary/Domain/Structures.agda @@ -8,46 +8,50 @@ module Relation.Binary.Domain.Structures where -open import Data.Product using (_×_; _,_) -open import Data.Nat.Properties using (≤-trans) +open import Data.Product using (_×_; _,_; proj₁; proj₂) open import Function using (_∘_) open import Level using (Level; _⊔_; suc) open import Relation.Binary.Bundles using (Poset) open import Relation.Binary.Domain.Definitions -open import Relation.Binary.Morphism.Structures using (IsOrderHomomorphism) private variable - o ℓ e o' ℓ' e' ℓ₂ : Level - Ix A B : Set o + a b c ℓ ℓ₁ ℓ₂ : Level + A B : Set a + module _ {c ℓ₁ ℓ₂ : Level} (P : Poset c ℓ₁ ℓ₂) where open Poset P - record IsDirectedFamily {Ix : Set c} (s : Ix → Carrier) : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where - no-eta-equality + record IsLub {B : Set c} (f : B → Carrier) (lub : Carrier) : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where field - elt : Ix - SemiDirected : IsSemidirectedFamily P s + isLeastUpperBound : leastupperbound _≤_ B f lub + + isUpperBound : ∀ i → f i ≤ lub + isUpperBound = proj₁ isLeastUpperBound + + isLeast : ∀ y → (∀ i → f i ≤ y) → lub ≤ y + isLeast = proj₂ isLeastUpperBound - record IsLub {Ix : Set c} (s : Ix → Carrier) (lub : Carrier) : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where + record IsDirectedFamily {B : Set c} (f : B → Carrier) : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where + no-eta-equality field - is-upperbound : ∀ i → s i ≤ lub - is-least : ∀ y → (∀ i → s i ≤ y) → lub ≤ y + elt : B + isSemidirected : semidirected _≤_ B f - record IsDCPO : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where + record IsDirectedCompletePartialOrder : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where field - ⋁ : ∀ {Ix : Set c} - → (s : Ix → Carrier) - → IsDirectedFamily s + ⋁ : ∀ {B : Set c} + → (f : B → Carrier) + → IsDirectedFamily f → Carrier - ⋁-isLub : ∀ {Ix : Set c} - → (s : Ix → Carrier) - → (dir : IsDirectedFamily s) - → IsLub s (⋁ s dir) + ⋁-isLub : ∀ {B : Set c} + → (f : B → Carrier) + → (dir : IsDirectedFamily f) + → IsLub f (⋁ f dir) - module _ {Ix : Set c} {s : Ix → Carrier} {dir : IsDirectedFamily s} where - open IsLub (⋁-isLub s dir) - renaming (is-upperbound to ⋁-≤; is-least to ⋁-least) + module _ {B : Set c} {f : B → Carrier} {dir : IsDirectedFamily f} where + open IsLub (⋁-isLub f dir) + renaming (isUpperBound to ⋁-≤; isLeast to ⋁-least) public module _ {c ℓ₁ ℓ₂ : Level} {P : Poset c ℓ₁ ℓ₂} {Q : Poset c ℓ₁ ℓ₂} where @@ -58,9 +62,9 @@ module _ {c ℓ₁ ℓ₂ : Level} {P : Poset c ℓ₁ ℓ₂} {Q : Poset c ℓ record IsScottContinuous (f : P.Carrier → Q.Carrier) : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where field - PreserveLub : ∀ {Ix : Set c} {s : Ix → P.Carrier} - → (dir : IsDirectedFamily P s) + PreserveLub : ∀ {B : Set c} {g : B → P.Carrier} + → (dir : IsDirectedFamily P g) → (lub : P.Carrier) - → IsLub P s lub - → IsLub Q (f ∘ s) (f lub) - PreserveEquality : ∀ {x y} → x P.≈ y → f x Q.≈ f y + → IsLub P g lub + → IsLub Q (f ∘ g) (f lub) + PreserveEquality : ∀ {x y} → x P.≈ y → f x Q.≈ f y \ No newline at end of file From 502e288a5b39a7c3e7707718a0f3b33804b33ea1 Mon Sep 17 00:00:00 2001 From: Jacques Date: Tue, 3 Jun 2025 14:17:30 -0400 Subject: [PATCH 04/12] whitespaces --- src/Padrightpropertiesdraft.agda | 6 +----- src/Relation/Binary/Domain/Bundles.agda | 2 +- src/Relation/Binary/Domain/Structures.agda | 8 ++++---- 3 files changed, 6 insertions(+), 10 deletions(-) diff --git a/src/Padrightpropertiesdraft.agda b/src/Padrightpropertiesdraft.agda index b7649b48d8..8fbb9e9f36 100644 --- a/src/Padrightpropertiesdraft.agda +++ b/src/Padrightpropertiesdraft.agda @@ -80,7 +80,7 @@ subst-drop : ∀ {m n p : ℕ} {A : Set} (eq : n ≡ m + p) (xs : Vec A n) → drop m (subst (Vec A) eq xs) ≡ subst (Vec A) (cong (_∸ m) eq) (drop m xs) subst-drop refl xs = refl --- Helper lemma: dropping from padded vector gives replicate +-- Helper lemma: dropping from padded vector gives replicate drop-padRight : ∀ {m n p} (m≤n : m ≤ n) (a : A) (xs : Vec A m) → n ≡ m + p → drop m (padRight m≤n a xs) ≡ replicate p a drop-padRight {m = zero} z≤n a [] refl = refl @@ -103,7 +103,3 @@ padRight-updateAt (s≤s m≤n) (y ∷ xs) f zero x = refl padRight-updateAt (s≤s m≤n) (y ∷ xs) f (suc i) x = cong (y ∷_) (padRight-updateAt m≤n xs f i x) - - - - diff --git a/src/Relation/Binary/Domain/Bundles.agda b/src/Relation/Binary/Domain/Bundles.agda index 6c103182d3..0d255b11f4 100644 --- a/src/Relation/Binary/Domain/Bundles.agda +++ b/src/Relation/Binary/Domain/Bundles.agda @@ -25,7 +25,7 @@ private record DirectedFamily {c ℓ₁ ℓ₂ : Level} {P : Poset c ℓ₁ ℓ₂} {B : Set c} (f : B → Poset.Carrier P) : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where field isDirectedFamily : IsDirectedFamily P f - + open IsDirectedFamily isDirectedFamily public record DirectedCompletePartialOrder (c ℓ₁ ℓ₂ : Level) : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where diff --git a/src/Relation/Binary/Domain/Structures.agda b/src/Relation/Binary/Domain/Structures.agda index dfbe85f3c6..e6f73de0a6 100644 --- a/src/Relation/Binary/Domain/Structures.agda +++ b/src/Relation/Binary/Domain/Structures.agda @@ -25,11 +25,11 @@ module _ {c ℓ₁ ℓ₂ : Level} (P : Poset c ℓ₁ ℓ₂) where record IsLub {B : Set c} (f : B → Carrier) (lub : Carrier) : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where field isLeastUpperBound : leastupperbound _≤_ B f lub - + isUpperBound : ∀ i → f i ≤ lub isUpperBound = proj₁ isLeastUpperBound - - isLeast : ∀ y → (∀ i → f i ≤ y) → lub ≤ y + + isLeast : ∀ y → (∀ i → f i ≤ y) → lub ≤ y isLeast = proj₂ isLeastUpperBound record IsDirectedFamily {B : Set c} (f : B → Carrier) : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where @@ -67,4 +67,4 @@ module _ {c ℓ₁ ℓ₂ : Level} {P : Poset c ℓ₁ ℓ₂} {Q : Poset c ℓ → (lub : P.Carrier) → IsLub P g lub → IsLub Q (f ∘ g) (f lub) - PreserveEquality : ∀ {x y} → x P.≈ y → f x Q.≈ f y \ No newline at end of file + PreserveEquality : ∀ {x y} → x P.≈ y → f x Q.≈ f y From 63810b78d7f13bbd35fd4a5ed5c9c6b281314bba Mon Sep 17 00:00:00 2001 From: Jacques Date: Tue, 3 Jun 2025 15:27:34 -0400 Subject: [PATCH 05/12] @ review --- src/Relation/Binary/Domain/Bundles.agda | 14 +++++++++---- src/Relation/Binary/Domain/Structures.agda | 23 +++++++++++++++------- 2 files changed, 26 insertions(+), 11 deletions(-) diff --git a/src/Relation/Binary/Domain/Bundles.agda b/src/Relation/Binary/Domain/Bundles.agda index 0d255b11f4..d4557b000e 100644 --- a/src/Relation/Binary/Domain/Bundles.agda +++ b/src/Relation/Binary/Domain/Bundles.agda @@ -40,17 +40,23 @@ record DirectedCompletePartialOrder (c ℓ₁ ℓ₂ : Level) : Set (suc (c ⊔ -- Scott-continuous functions ------------------------------------------------------------------------ -record ScottContinuous {c ℓ₁ ℓ₂ : Level} {P : Poset c ℓ₁ ℓ₂} {Q : Poset c ℓ₁ ℓ₂} : - Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where +record ScottContinuous + {c₁ ℓ₁₁ ℓ₁₂ c₂ ℓ₂₁ ℓ₂₂ : Level} + (P : Poset c₁ ℓ₁₁ ℓ₁₂) + (Q : Poset c₂ ℓ₂₁ ℓ₂₂) + : Set (suc (c₁ ⊔ ℓ₁₁ ⊔ ℓ₁₂ ⊔ c₂ ⊔ ℓ₂₁ ⊔ ℓ₂₂)) where field f : Poset.Carrier P → Poset.Carrier Q - isScottContinuous : IsScottContinuous {P = P} {Q = Q} f + isScottContinuous : IsScottContinuous P Q f + + open IsScottContinuous isScottContinuous public ------------------------------------------------------------------------ -- Lubs ------------------------------------------------------------------------ -record Lub {c ℓ₁ ℓ₂ : Level} {P : Poset c ℓ₁ ℓ₂} {B : Set c} (f : B → Poset.Carrier P) : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where +record Lub {c ℓ₁ ℓ₂ : Level} {P : Poset c ℓ₁ ℓ₂} {B : Set c} + (f : B → Poset.Carrier P) : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where open Poset P field lub : Carrier diff --git a/src/Relation/Binary/Domain/Structures.agda b/src/Relation/Binary/Domain/Structures.agda index e6f73de0a6..36717e8189 100644 --- a/src/Relation/Binary/Domain/Structures.agda +++ b/src/Relation/Binary/Domain/Structures.agda @@ -22,7 +22,8 @@ private variable module _ {c ℓ₁ ℓ₂ : Level} (P : Poset c ℓ₁ ℓ₂) where open Poset P - record IsLub {B : Set c} (f : B → Carrier) (lub : Carrier) : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where + record IsLub {b : Level} {B : Set b} (f : B → Carrier) + (lub : Carrier) : Set (b ⊔ c ⊔ ℓ₁ ⊔ ℓ₂) where field isLeastUpperBound : leastupperbound _≤_ B f lub @@ -32,10 +33,11 @@ module _ {c ℓ₁ ℓ₂ : Level} (P : Poset c ℓ₁ ℓ₂) where isLeast : ∀ y → (∀ i → f i ≤ y) → lub ≤ y isLeast = proj₂ isLeastUpperBound - record IsDirectedFamily {B : Set c} (f : B → Carrier) : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where + record IsDirectedFamily {b : Level} {B : Set b} (f : B → Carrier) + : Set (b ⊔ c ⊔ ℓ₁ ⊔ ℓ₂) where no-eta-equality field - elt : B + elt : B isSemidirected : semidirected _≤_ B f record IsDirectedCompletePartialOrder : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where @@ -54,17 +56,24 @@ module _ {c ℓ₁ ℓ₂ : Level} (P : Poset c ℓ₁ ℓ₂) where renaming (isUpperBound to ⋁-≤; isLeast to ⋁-least) public -module _ {c ℓ₁ ℓ₂ : Level} {P : Poset c ℓ₁ ℓ₂} {Q : Poset c ℓ₁ ℓ₂} where +------------------------------------------------------------------------ +-- Scott‐continuous maps between two (possibly different‐universe) posets +------------------------------------------------------------------------ + +module _ {c₁ ℓ₁₁ ℓ₁₂ c₂ ℓ₂₁ ℓ₂₂ : Level} + (P : Poset c₁ ℓ₁₁ ℓ₁₂) + (Q : Poset c₂ ℓ₂₁ ℓ₂₂) where private module P = Poset P module Q = Poset Q - record IsScottContinuous (f : P.Carrier → Q.Carrier) : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where + record IsScottContinuous (f : P.Carrier → Q.Carrier) + : Set (suc (c₁ ⊔ ℓ₁₁ ⊔ ℓ₁₂ ⊔ c₂ ⊔ ℓ₂₁ ⊔ ℓ₂₂)) where field - PreserveLub : ∀ {B : Set c} {g : B → P.Carrier} + preserveLub : ∀ {B : Set c₁} {g : B → P.Carrier} → (dir : IsDirectedFamily P g) → (lub : P.Carrier) → IsLub P g lub → IsLub Q (f ∘ g) (f lub) - PreserveEquality : ∀ {x y} → x P.≈ y → f x Q.≈ f y + preserveEquality : ∀ {x y} → x P.≈ y → f x Q.≈ f y From 87d5f16ecf2276e1c7c68a02d66003b1871f4725 Mon Sep 17 00:00:00 2001 From: Jacques Date: Thu, 5 Jun 2025 16:15:02 -0400 Subject: [PATCH 06/12] remove the file Padrightdraft --- src/Padrightpropertiesdraft.agda | 105 ------------------------------- 1 file changed, 105 deletions(-) delete mode 100644 src/Padrightpropertiesdraft.agda diff --git a/src/Padrightpropertiesdraft.agda b/src/Padrightpropertiesdraft.agda deleted file mode 100644 index 8fbb9e9f36..0000000000 --- a/src/Padrightpropertiesdraft.agda +++ /dev/null @@ -1,105 +0,0 @@ ------------------------------------------------------------------------- --- The Agda standard library --- --- Properties of padRight for Vec ------------------------------------------------------------------------- - -{-# OPTIONS --cubical-compatible --safe #-} - -module Padrightpropertiesdraft where - -open import Data.Fin.Base using (Fin; zero; suc; inject≤) -open import Data.Nat.Base using (ℕ; zero; suc; _+_; _≤_; z≤n; s≤s; _∸_) -open import Data.Nat.Properties using (≤-refl; ≤-trans; m≤m+n; m+n∸m≡n) -open import Data.Vec.Base -open import Data.Vec.Properties using (map-replicate; zipWith-replicate; padRight-trans) -open import Function.Base using (_∘_; _$_) -open import Level using (Level) -open import Relation.Binary.PropositionalEquality.Core - using (_≡_; refl; cong; sym; trans; subst) -open import Relation.Binary.PropositionalEquality.Properties - using (module ≡-Reasoning) - -private - variable - a b c : Level - A : Set a - B : Set b - C : Set c - m n p : ℕ - - ------------------------------------------------------------------------- --- Interaction with map - -padRight-map : ∀ (f : A → B) (m≤n : m ≤ n) (a : A) (xs : Vec A m) → - map f (padRight m≤n a xs) ≡ padRight m≤n (f a) (map f xs) -padRight-map f z≤n a [] = map-replicate f a _ -padRight-map f (s≤s m≤n) a (x ∷ xs) = cong (f x ∷_) (padRight-map f m≤n a xs) - ------------------------------------------------------------------------- --- Interaction with lookup - -padRight-lookup : ∀ (m≤n : m ≤ n) (a : A) (xs : Vec A m) (i : Fin m) → - lookup (padRight m≤n a xs) (inject≤ i m≤n) ≡ lookup xs i -padRight-lookup (s≤s m≤n) a (x ∷ xs) zero = refl -padRight-lookup (s≤s m≤n) a (x ∷ xs) (suc i) = padRight-lookup m≤n a xs i - ------------------------------------------------------------------------- --- Interaction with zipWith - --- When both vectors have the same original length -padRight-zipWith : ∀ (f : A → B → C) (m≤n : m ≤ n) (a : A) (b : B) - (xs : Vec A m) (ys : Vec B m) → - zipWith f (padRight m≤n a xs) (padRight m≤n b ys) ≡ - padRight m≤n (f a b) (zipWith f xs ys) -padRight-zipWith f z≤n a b [] [] = zipWith-replicate f a b -padRight-zipWith f (s≤s m≤n) a b (x ∷ xs) (y ∷ ys) = - cong (f x y ∷_) (padRight-zipWith f m≤n a b xs ys) - --- When vectors have different original lengths -padRight-zipWith₁ : ∀ {p} (f : A → B → C) (m≤n : m ≤ n) (p≤m : p ≤ m) - (a : A) (b : B) (xs : Vec A m) (ys : Vec B p) → - zipWith f (padRight m≤n a xs) (padRight (≤-trans p≤m m≤n) b ys) ≡ - padRight m≤n (f a b) (zipWith f xs (padRight p≤m b ys)) -padRight-zipWith₁ {p} f m≤n p≤m a b xs ys = - trans (cong (zipWith f (padRight m≤n a xs)) (padRight-trans p≤m m≤n b ys)) - (padRight-zipWith f m≤n a b xs (padRight p≤m b ys)) - ------------------------------------------------------------------------- --- Interaction with take and drop - -padRight-take : ∀ {p} (m≤n : m ≤ n) (a : A) (xs : Vec A m) (n≡m+p : n ≡ m + p) → - take m (subst (Vec A) n≡m+p (padRight m≤n a xs)) ≡ xs -padRight-take {m = zero} z≤n a [] refl = refl -padRight-take {m = suc m} {p = p} (s≤s m≤n) a (x ∷ xs) refl = - cong (x ∷_) (padRight-take {p = p} m≤n a xs refl) - --- Helper lemma: commuting subst with drop -subst-drop : ∀ {m n p : ℕ} {A : Set} (eq : n ≡ m + p) (xs : Vec A n) → - drop m (subst (Vec A) eq xs) ≡ subst (Vec A) (cong (_∸ m) eq) (drop m xs) -subst-drop refl xs = refl - --- Helper lemma: dropping from padded vector gives replicate -drop-padRight : ∀ {m n p} (m≤n : m ≤ n) (a : A) (xs : Vec A m) → - n ≡ m + p → drop m (padRight m≤n a xs) ≡ replicate p a -drop-padRight {m = zero} z≤n a [] refl = refl -drop-padRight {m = suc m} {p = p} (s≤s m≤n) a (x ∷ xs) refl = - drop-padRight {p = p} m≤n a xs refl - -padRight-drop : ∀ {p} (m≤n : m ≤ n) (a : A) (xs : Vec A m) (n≡m+p : n ≡ m + p) → - drop m (subst (Vec A) n≡m+p (padRight m≤n a xs)) ≡ replicate p a -padRight-drop {p = p} m≤n a xs n≡m+p = - trans (subst-drop n≡m+p (padRight m≤n a xs)) - (cong (subst (Vec A) (cong (_∸ _) n≡m+p)) (drop-padRight m≤n a xs n≡m+p)) - ------------------------------------------------------------------------- --- Interaction with updateAt - -padRight-updateAt : ∀ (m≤n : m ≤ n) (xs : Vec A m) (f : A → A) (i : Fin m) (x : A) → - updateAt (padRight m≤n x xs) (inject≤ i m≤n) f ≡ - padRight m≤n x (updateAt xs i f) -padRight-updateAt (s≤s m≤n) (y ∷ xs) f zero x = refl -padRight-updateAt (s≤s m≤n) (y ∷ xs) f (suc i) x = - cong (y ∷_) (padRight-updateAt m≤n xs f i x) - From 5a1cafcffc8cfeee9413179dd510172e6d6c94f9 Mon Sep 17 00:00:00 2001 From: Jacques Date: Thu, 5 Jun 2025 18:32:30 -0400 Subject: [PATCH 07/12] waiting for part1 review --- src/Relation/Binary/Properties/Domain.agda | 136 ++++++++++++--------- 1 file changed, 76 insertions(+), 60 deletions(-) diff --git a/src/Relation/Binary/Properties/Domain.agda b/src/Relation/Binary/Properties/Domain.agda index adb09a12ee..e61860e629 100644 --- a/src/Relation/Binary/Properties/Domain.agda +++ b/src/Relation/Binary/Properties/Domain.agda @@ -1,7 +1,7 @@ ------------------------------------------------------------------------ -- The Agda standard library -- --- Properties satisfied by directed complete partial orders (DCPOs) +-- Properties satisfied by directed complete partial orders ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} @@ -13,53 +13,60 @@ open import Level using (Level; Lift; lift) open import Function using (_∘_; id) open import Data.Product using (_,_) open import Data.Bool using (Bool; true; false; if_then_else_) -open import Relation.Binary.Domain.Bundles using (DCPO) +open import Relation.Binary.Domain.Definitions +open import Relation.Binary.Domain.Bundles using (DirectedCompletePartialOrder) open import Relation.Binary.Domain.Structures - using (IsDirectedFamily; IsDCPO; IsLub; IsScottContinuous) + using (IsDirectedFamily; IsDirectedCompletePartialOrder; IsLub; IsScottContinuous) open import Relation.Binary.Morphism.Structures using (IsOrderHomomorphism) private variable c ℓ₁ ℓ₂ o ℓ : Level Ix A B : Set o -module _ {c ℓ₁ ℓ₂} {P : Poset c ℓ₁ ℓ₂} {D : DCPO c ℓ₁ ℓ₂ } where +------------------------------------------------------------------------ +-- Properties of least upper bounds + +module _ {c ℓ₁ ℓ₂} {D : DirectedCompletePartialOrder c ℓ₁ ℓ₂ } where private - module D = DCPO D + module D = DirectedCompletePartialOrder D uniqueLub : ∀ {Ix} {s : Ix → D.Carrier} → (x y : D.Carrier) → IsLub D.poset s x → IsLub D.poset s y → x D.≈ y uniqueLub x y x-lub y-lub = D.antisym - (IsLub.is-least x-lub y (IsLub.is-upperbound y-lub)) - (IsLub.is-least y-lub x (IsLub.is-upperbound x-lub)) + (IsLub.isLeast x-lub y (IsLub.isUpperBound y-lub)) + (IsLub.isLeast y-lub x (IsLub.isUpperBound x-lub)) - is-lub-cong : ∀ {Ix} {s : Ix → D.Carrier} + IsLub-cong : ∀ {Ix} {s : Ix → D.Carrier} → (x y : D.Carrier) → x D.≈ y → IsLub D.poset s x → IsLub D.poset s y - is-lub-cong x y x≈y x-lub = record - { is-upperbound = λ i → D.trans (IsLub.is-upperbound x-lub i) (D.reflexive x≈y) - ; is-least = λ z ub → D.trans (D.reflexive (D.Eq.sym x≈y)) - (IsLub.is-least x-lub z (λ i → D.trans (ub i) (D.reflexive D.Eq.refl))) + IsLub-cong x y x≈y x-lub = record + { isLeastUpperBound = (λ i → D.trans (IsLub.isUpperBound x-lub i) (D.reflexive x≈y)) , + (λ z ub → D.trans (D.reflexive (D.Eq.sym x≈y)) + (IsLub.isLeast x-lub z (λ i → D.trans (ub i) (D.reflexive D.Eq.refl)))) } +------------------------------------------------------------------------ +-- Scott continuity and monotonicity + module _ {c ℓ₁ ℓ₂ : Level} {P : Poset c ℓ₁ ℓ₂} {Q : Poset c ℓ₁ ℓ₂} where private module P = Poset P module Q = Poset Q - dcpo+scott→monotone : (P-dcpo : IsDCPO P) + DirectedCompletePartialOrder+scott→monotone : (P-DirectedCompletePartialOrder : IsDirectedCompletePartialOrder P) → (f : P.Carrier → Q.Carrier) → (scott : IsScottContinuous f) → IsOrderHomomorphism (Poset._≈_ P) (Poset._≈_ Q) (Poset._≤_ P) (Poset._≤_ Q) f - dcpo+scott→monotone P-dcpo f scott = record - { cong = λ {x} {y} x≈y → IsScottContinuous.PreserveEquality scott x≈y + DirectedCompletePartialOrder+scott→monotone P-DirectedCompletePartialOrder f scott = record + { cong = λ {x} {y} x≈y → IsScottContinuous.preserveEquality scott x≈y ; mono = λ {x} {y} x≤y → mono-proof x y x≤y } where mono-proof : ∀ x y → x P.≤ y → f x Q.≤ f y - mono-proof x y x≤y = IsLub.is-upperbound fs-lub (lift true) + mono-proof x y x≤y = IsLub.isUpperBound fs-lub (lift true) where s : Lift c Bool → P.Carrier s (lift b) = if b then x else y @@ -71,17 +78,16 @@ module _ {c ℓ₁ ℓ₂ : Level} {P : Poset c ℓ₁ ℓ₂} {Q : Poset c ℓ s-directed : IsDirectedFamily P s s-directed = record { elt = lift true - ; SemiDirected = λ i j → (lift false , sx≤sfalse i , sx≤sfalse j) + ; semidirected = λ i j → (lift false , sx≤sfalse i , sx≤sfalse j) } s-lub : IsLub P s y s-lub = record - { is-upperbound = sx≤sfalse - ; is-least = λ z proof → proof (lift false) + { isLeastUpperBound = sx≤sfalse , (λ z proof → proof (lift false)) } fs-lub : IsLub Q (f ∘ s) (f y) - fs-lub = IsScottContinuous.PreserveLub scott s-directed y s-lub + fs-lub = IsScottContinuous.preserveLub scott s-directed y s-lub monotone∘directed : ∀ {Ix : Set c} {s : Ix → P.Carrier} → (f : P.Carrier → Q.Carrier) @@ -90,38 +96,42 @@ module _ {c ℓ₁ ℓ₂ : Level} {P : Poset c ℓ₁ ℓ₂} {Q : Poset c ℓ → IsDirectedFamily Q (f ∘ s) monotone∘directed f ismonotone dir = record { elt = IsDirectedFamily.elt dir - ; SemiDirected = λ i j → - let (k , s[i]≤s[k] , s[j]≤s[k]) = IsDirectedFamily.SemiDirected dir i j + ; isSemidirected = λ i j → + let (k , s[i]≤s[k] , s[j]≤s[k]) = IsDirectedFamily.semidirected dir i j in k , IsOrderHomomorphism.mono ismonotone s[i]≤s[k] , IsOrderHomomorphism.mono ismonotone s[j]≤s[k] } -module _ where - - ScottId : ∀ {c ℓ₁ ℓ₂} {P : Poset c ℓ₁ ℓ₂} → IsScottContinuous {P = P} {Q = P} id - ScottId = record - { PreserveLub = λ dir lub z → z - ; PreserveEquality = λ z → z } - - scott-∘ : ∀ {c ℓ₁ ℓ₂} {P Q R : Poset c ℓ₁ ℓ₂} - → (f : Poset.Carrier R → Poset.Carrier Q) (g : Poset.Carrier P → Poset.Carrier R) - → IsScottContinuous {P = R} {Q = Q} f → IsScottContinuous {P = P} {Q = R} g - → IsOrderHomomorphism (Poset._≈_ P) (Poset._≈_ R) (Poset._≤_ P) (Poset._≤_ R) g - → IsScottContinuous {P = P} {Q = Q} (f ∘ g) - scott-∘ f g scottf scottg monog = record - { PreserveLub = λ dir lub z → f.PreserveLub - (monotone∘directed g monog dir) - (g lub) - (g.PreserveLub dir lub z) - ; PreserveEquality = λ {x} {y} z → - f.PreserveEquality (g.PreserveEquality z) - } - where - module f = IsScottContinuous scottf - module g = IsScottContinuous scottg +------------------------------------------------------------------------ +-- Scott continuous functions + +ScottId : ∀ {c ℓ₁ ℓ₂} {P : Poset c ℓ₁ ℓ₂} → IsScottContinuous {P = P} {Q = P} id +ScottId = record + { preserveLub = λ dir lub z → z + ; preserveEquality = λ z → z } + +scott-∘ : ∀ {c ℓ₁ ℓ₂} {P Q R : Poset c ℓ₁ ℓ₂} + → (f : Poset.Carrier R → Poset.Carrier Q) (g : Poset.Carrier P → Poset.Carrier R) + → IsScottContinuous {P = R} {Q = Q} f → IsScottContinuous {P = P} {Q = R} g + → IsOrderHomomorphism (Poset._≈_ P) (Poset._≈_ R) (Poset._≤_ P) (Poset._≤_ R) g + → IsScottContinuous {P = P} {Q = Q} (f ∘ g) +scott-∘ f g scottf scottg monog = record + { preserveLub = λ dir lub z → f.preserveLub + (monotone∘directed g monog dir) + (g lub) + (g.preserveLub dir lub z) + ; preserveEquality = λ {x} {y} z → + f.preserveEquality (g.preserveEquality z) + } + where + module f = IsScottContinuous scottf + module g = IsScottContinuous scottg + +------------------------------------------------------------------------ +-- Suprema and pointwise ordering -module _ {c ℓ₁ ℓ₂} {P : Poset c ℓ₁ ℓ₂} (D : DCPO c ℓ₁ ℓ₂) where +module _ {c ℓ₁ ℓ₂} {P : Poset c ℓ₁ ℓ₂} (D : DirectedCompletePartialOrder c ℓ₁ ℓ₂) where private - module D = DCPO D + module D = DirectedCompletePartialOrder D open import Relation.Binary.Reasoning.PartialOrder D.poset @@ -132,40 +142,46 @@ module _ {c ℓ₁ ℓ₂} {P : Poset c ℓ₁ ℓ₂} (D : DCPO c ℓ₁ ℓ₂ ⋃-pointwise {s = s} {s'} {fam} {fam'} p = D.⋁-least (D.⋁ s' fam') λ i → D.trans (p i) (D.⋁-≤ i) +------------------------------------------------------------------------ +-- Scott continuity module + module Scott {c ℓ₁ ℓ₂} {P : Poset c ℓ₁ ℓ₂} - {D E : DCPO c ℓ₁ ℓ₂} - (let module D = DCPO D) - (let module E = DCPO E) + {D E : DirectedCompletePartialOrder c ℓ₁ ℓ₂} + (let module D = DirectedCompletePartialOrder D) + (let module E = DirectedCompletePartialOrder E) (f : D.Carrier → E.Carrier) (isScott : IsScottContinuous {P = D.poset} {Q = E.poset} f) (mono : IsOrderHomomorphism (Poset._≈_ D.poset) (Poset._≈_ E.poset) (Poset._≤_ D.poset) (Poset._≤_ E.poset) f) where - open DCPO D - open DCPO E + open DirectedCompletePartialOrder D + open DirectedCompletePartialOrder E pres-⋁ : ∀ {Ix} (s : Ix → D.Carrier) → (dir : IsDirectedFamily D.poset s) → f (D.⋁ s dir) E.≈ E.⋁ (f ∘ s) (monotone∘directed f mono dir) pres-⋁ s dir = E.antisym - (IsLub.is-least - (IsScottContinuous.PreserveLub isScott dir (D.⋁ s dir) (D.⋁-isLub s dir)) + (IsLub.isLeast + (IsScottContinuous.preserveLub isScott dir (D.⋁ s dir) (D.⋁-isLub s dir)) (E.⋁ (f ∘ s) (monotone∘directed f mono dir)) E.⋁-≤ ) - (IsLub.is-least + (IsLub.isLeast (E.⋁-isLub (f ∘ s) (monotone∘directed f mono dir)) (f (D.⋁ s dir)) (λ i → IsOrderHomomorphism.mono mono (D.⋁-≤ i)) ) -module _ {c ℓ₁ ℓ₂} {P : Poset c ℓ₁ ℓ₂} {D E : DCPO c ℓ₁ ℓ₂} where +------------------------------------------------------------------------ +-- Converting to Scott continuity + +module _ {c ℓ₁ ℓ₂} {D E : DirectedCompletePartialOrder c ℓ₁ ℓ₂} where private - module D = DCPO D - module E = DCPO E + module D = DirectedCompletePartialOrder D + module E = DirectedCompletePartialOrder E to-scott : (f : D.Carrier → E.Carrier) → IsOrderHomomorphism (Poset._≈_ D.poset) (Poset._≈_ E.poset) @@ -174,7 +190,7 @@ module _ {c ℓ₁ ℓ₂} {P : Poset c ℓ₁ ℓ₂} {D E : DCPO c ℓ₁ ℓ → IsLub E.poset (f ∘ s) (f (D.⋁ s dir))) → IsScottContinuous {P = D.poset} {Q = E.poset} f to-scott f mono pres-⋁ = record - { PreserveLub = λ dir lub x → is-lub-cong {P = E.poset} {D = E} (f (D.⋁ _ dir)) (f lub) + { preserveLub = λ dir lub x → IsLub-cong {P = E.poset} {D = E} (f (D.⋁ _ dir)) (f lub) (IsOrderHomomorphism.cong mono (uniqueLub {P = E.poset} {D = D} (D.⋁ _ dir) lub (D.⋁-isLub _ dir) x)) (pres-⋁ _ dir) - ; PreserveEquality = IsOrderHomomorphism.cong mono } + ; preserveEquality = IsOrderHomomorphism.cong mono } From d4768c453b4682cbde4c419eb6c7f7f47dd02a73 Mon Sep 17 00:00:00 2001 From: Jacques Date: Wed, 11 Jun 2025 14:58:06 -0400 Subject: [PATCH 08/12] fix proof --- src/Relation/Binary/Properties/Domain.agda | 55 +++++++++++++--------- 1 file changed, 33 insertions(+), 22 deletions(-) diff --git a/src/Relation/Binary/Properties/Domain.agda b/src/Relation/Binary/Properties/Domain.agda index e61860e629..58358cc2e3 100644 --- a/src/Relation/Binary/Properties/Domain.agda +++ b/src/Relation/Binary/Properties/Domain.agda @@ -20,45 +20,44 @@ open import Relation.Binary.Domain.Structures open import Relation.Binary.Morphism.Structures using (IsOrderHomomorphism) private variable - c ℓ₁ ℓ₂ o ℓ : Level - Ix A B : Set o + c ℓ₁ ℓ₂ a ℓ : Level + Ix A B : Set a ------------------------------------------------------------------------ -- Properties of least upper bounds -module _ {c ℓ₁ ℓ₂} {D : DirectedCompletePartialOrder c ℓ₁ ℓ₂ } where +module _ {c ℓ₁ ℓ₂} (D : DirectedCompletePartialOrder c ℓ₁ ℓ₂) where private module D = DirectedCompletePartialOrder D - uniqueLub : ∀ {Ix} {s : Ix → D.Carrier} + uniqueLub : ∀ {s : Ix → D.Carrier} → (x y : D.Carrier) → IsLub D.poset s x → IsLub D.poset s y → x D.≈ y uniqueLub x y x-lub y-lub = D.antisym (IsLub.isLeast x-lub y (IsLub.isUpperBound y-lub)) (IsLub.isLeast y-lub x (IsLub.isUpperBound x-lub)) - IsLub-cong : ∀ {Ix} {s : Ix → D.Carrier} + IsLub-cong : ∀ {s : Ix → D.Carrier} → (x y : D.Carrier) → x D.≈ y → IsLub D.poset s x → IsLub D.poset s y IsLub-cong x y x≈y x-lub = record { isLeastUpperBound = (λ i → D.trans (IsLub.isUpperBound x-lub i) (D.reflexive x≈y)) , - (λ z ub → D.trans (D.reflexive (D.Eq.sym x≈y)) - (IsLub.isLeast x-lub z (λ i → D.trans (ub i) (D.reflexive D.Eq.refl)))) + (λ z ub → D.trans (D.reflexive (D.Eq.sym x≈y)) + (IsLub.isLeast x-lub z (λ i → D.trans (ub i) (D.reflexive D.Eq.refl)))) } ------------------------------------------------------------------------ -- Scott continuity and monotonicity -module _ {c ℓ₁ ℓ₂ : Level} {P : Poset c ℓ₁ ℓ₂} {Q : Poset c ℓ₁ ℓ₂} where - +module _ {c₁ ℓ₁₁ ℓ₁₂ c₂ ℓ₂₁ ℓ₂₂ : Level} {P : Poset c₁ ℓ₁₁ ℓ₁₂} {Q : Poset c₂ ℓ₂₁ ℓ₂₂} where private module P = Poset P module Q = Poset Q DirectedCompletePartialOrder+scott→monotone : (P-DirectedCompletePartialOrder : IsDirectedCompletePartialOrder P) → (f : P.Carrier → Q.Carrier) - → (scott : IsScottContinuous f) + → (scott : IsScottContinuous P Q f) → IsOrderHomomorphism (Poset._≈_ P) (Poset._≈_ Q) (Poset._≤_ P) (Poset._≤_ Q) f DirectedCompletePartialOrder+scott→monotone P-DirectedCompletePartialOrder f scott = record { cong = λ {x} {y} x≈y → IsScottContinuous.preserveEquality scott x≈y @@ -68,7 +67,7 @@ module _ {c ℓ₁ ℓ₂ : Level} {P : Poset c ℓ₁ ℓ₂} {Q : Poset c ℓ mono-proof : ∀ x y → x P.≤ y → f x Q.≤ f y mono-proof x y x≤y = IsLub.isUpperBound fs-lub (lift true) where - s : Lift c Bool → P.Carrier + s : Lift c₁ Bool → P.Carrier s (lift b) = if b then x else y sx≤sfalse : ∀ b → s b P.≤ s (lift false) @@ -78,7 +77,7 @@ module _ {c ℓ₁ ℓ₂ : Level} {P : Poset c ℓ₁ ℓ₂} {Q : Poset c ℓ s-directed : IsDirectedFamily P s s-directed = record { elt = lift true - ; semidirected = λ i j → (lift false , sx≤sfalse i , sx≤sfalse j) + ; isSemidirected = λ i j → (lift false , sx≤sfalse i , sx≤sfalse j) } s-lub : IsLub P s y @@ -97,23 +96,23 @@ module _ {c ℓ₁ ℓ₂ : Level} {P : Poset c ℓ₁ ℓ₂} {Q : Poset c ℓ monotone∘directed f ismonotone dir = record { elt = IsDirectedFamily.elt dir ; isSemidirected = λ i j → - let (k , s[i]≤s[k] , s[j]≤s[k]) = IsDirectedFamily.semidirected dir i j + let (k , s[i]≤s[k] , s[j]≤s[k]) = IsDirectedFamily.isSemidirected dir i j in k , IsOrderHomomorphism.mono ismonotone s[i]≤s[k] , IsOrderHomomorphism.mono ismonotone s[j]≤s[k] } ------------------------------------------------------------------------ -- Scott continuous functions -ScottId : ∀ {c ℓ₁ ℓ₂} {P : Poset c ℓ₁ ℓ₂} → IsScottContinuous {P = P} {Q = P} id +ScottId : ∀ {c ℓ₁ ℓ₂} {P : Poset c ℓ₁ ℓ₂} → IsScottContinuous P P id ScottId = record { preserveLub = λ dir lub z → z ; preserveEquality = λ z → z } scott-∘ : ∀ {c ℓ₁ ℓ₂} {P Q R : Poset c ℓ₁ ℓ₂} → (f : Poset.Carrier R → Poset.Carrier Q) (g : Poset.Carrier P → Poset.Carrier R) - → IsScottContinuous {P = R} {Q = Q} f → IsScottContinuous {P = P} {Q = R} g + → IsScottContinuous R Q f → IsScottContinuous P R g → IsOrderHomomorphism (Poset._≈_ P) (Poset._≈_ R) (Poset._≤_ P) (Poset._≤_ R) g - → IsScottContinuous {P = P} {Q = Q} (f ∘ g) + → IsScottContinuous P Q (f ∘ g) scott-∘ f g scottf scottg monog = record { preserveLub = λ dir lub z → f.preserveLub (monotone∘directed g monog dir) @@ -152,7 +151,7 @@ module Scott (let module D = DirectedCompletePartialOrder D) (let module E = DirectedCompletePartialOrder E) (f : D.Carrier → E.Carrier) - (isScott : IsScottContinuous {P = D.poset} {Q = E.poset} f) + (isScott : IsScottContinuous D.poset E.poset f) (mono : IsOrderHomomorphism (Poset._≈_ D.poset) (Poset._≈_ E.poset) (Poset._≤_ D.poset) (Poset._≤_ E.poset) f) where @@ -188,9 +187,21 @@ module _ {c ℓ₁ ℓ₂} {D E : DirectedCompletePartialOrder c ℓ₁ ℓ₂} (Poset._≤_ D.poset) (Poset._≤_ E.poset) f → (∀ {Ix} (s : Ix → D.Carrier) (dir : IsDirectedFamily D.poset s) → IsLub E.poset (f ∘ s) (f (D.⋁ s dir))) - → IsScottContinuous {P = D.poset} {Q = E.poset} f + → IsScottContinuous D.poset E.poset f to-scott f mono pres-⋁ = record - { preserveLub = λ dir lub x → IsLub-cong {P = E.poset} {D = E} (f (D.⋁ _ dir)) (f lub) - (IsOrderHomomorphism.cong mono (uniqueLub {P = E.poset} {D = D} (D.⋁ _ dir) lub (D.⋁-isLub _ dir) x)) - (pres-⋁ _ dir) - ; preserveEquality = IsOrderHomomorphism.cong mono } + { preserveLub = λ {_} {s} dir lub x → + IsLub-cong E (f (D.⋁ _ dir)) (f lub) + (f.cong (uniqueLub D (D.⋁ s dir) lub (D.⋁-isLub s dir) x)) + (pres-⋁ s dir) + ; preserveEquality = f.cong + } + where module f = IsOrderHomomorphism mono + + + -- { preserveLub = λ dir lub x → IsLub-cong {! D !} {! E !} {! !} (pres-⋁ {! !} dir) ; + -- preserveEquality = IsOrderHomomorphism.cong mono + -- } + -- { preserveLub = λ dir lub x → IsLub-cong ? E (f (D.⋁ _ dir)) (f lub) + -- (IsOrderHomomorphism.cong mono (uniqueLub {P = E.poset} {D = D} (D.⋁ _ dir) lub (D.⋁-isLub _ dir) x)) + -- (pres-⋁ _ dir) + -- ; preserveEquality = IsOrderHomomorphism.cong mono } From e268d4ed1361ea603f521fb3a8c719a35ce8e871 Mon Sep 17 00:00:00 2001 From: Jacques Date: Tue, 17 Jun 2025 15:19:12 -0400 Subject: [PATCH 09/12] refactoring --- src/Relation/Binary/Domain/Structures.agda | 2 +- src/Relation/Binary/Properties/Domain.agda | 207 +++++++++------------ 2 files changed, 87 insertions(+), 122 deletions(-) diff --git a/src/Relation/Binary/Domain/Structures.agda b/src/Relation/Binary/Domain/Structures.agda index 36717e8189..3bea876cc2 100644 --- a/src/Relation/Binary/Domain/Structures.agda +++ b/src/Relation/Binary/Domain/Structures.agda @@ -76,4 +76,4 @@ module _ {c₁ ℓ₁₁ ℓ₁₂ c₂ ℓ₂₁ ℓ₂₂ : Level} → (lub : P.Carrier) → IsLub P g lub → IsLub Q (f ∘ g) (f lub) - preserveEquality : ∀ {x y} → x P.≈ y → f x Q.≈ f y + cong : ∀ {x y} → x P.≈ y → f x Q.≈ f y diff --git a/src/Relation/Binary/Properties/Domain.agda b/src/Relation/Binary/Properties/Domain.agda index 58358cc2e3..ce71bc8825 100644 --- a/src/Relation/Binary/Properties/Domain.agda +++ b/src/Relation/Binary/Properties/Domain.agda @@ -20,52 +20,48 @@ open import Relation.Binary.Domain.Structures open import Relation.Binary.Morphism.Structures using (IsOrderHomomorphism) private variable - c ℓ₁ ℓ₂ a ℓ : Level + c₁ ℓ₁₁ ℓ₁₂ c₂ ℓ₂₁ ℓ₂₂ c ℓ₁ ℓ₂ a ℓ : Level Ix A B : Set a ------------------------------------------------------------------------ -- Properties of least upper bounds -module _ {c ℓ₁ ℓ₂} (D : DirectedCompletePartialOrder c ℓ₁ ℓ₂) where +module _ (D : DirectedCompletePartialOrder c ℓ₁ ℓ₂) where private module D = DirectedCompletePartialOrder D - uniqueLub : ∀ {s : Ix → D.Carrier} - → (x y : D.Carrier) → IsLub D.poset s x → IsLub D.poset s y - → x D.≈ y + uniqueLub : ∀ {s : Ix → D.Carrier} → (x y : D.Carrier) → + IsLub D.poset s x → IsLub D.poset s y → x D.≈ y uniqueLub x y x-lub y-lub = D.antisym (IsLub.isLeast x-lub y (IsLub.isUpperBound y-lub)) (IsLub.isLeast y-lub x (IsLub.isUpperBound x-lub)) - IsLub-cong : ∀ {s : Ix → D.Carrier} - → (x y : D.Carrier) - → x D.≈ y - → IsLub D.poset s x → IsLub D.poset s y - IsLub-cong x y x≈y x-lub = record - { isLeastUpperBound = (λ i → D.trans (IsLub.isUpperBound x-lub i) (D.reflexive x≈y)) , - (λ z ub → D.trans (D.reflexive (D.Eq.sym x≈y)) - (IsLub.isLeast x-lub z (λ i → D.trans (ub i) (D.reflexive D.Eq.refl)))) + IsLub-cong : ∀ {s : Ix → D.Carrier} → {x y : D.Carrier} → x D.≈ y → + IsLub D.poset s x → IsLub D.poset s y + IsLub-cong x≈y x-lub = record + { isLeastUpperBound = + (λ i → D.trans (IsLub.isUpperBound x-lub i) (D.reflexive x≈y)) + , (λ z ub → D.trans (D.reflexive (D.Eq.sym x≈y)) (IsLub.isLeast x-lub z (λ i → D.trans (ub i) (D.reflexive D.Eq.refl)))) } ------------------------------------------------------------------------ -- Scott continuity and monotonicity -module _ {c₁ ℓ₁₁ ℓ₁₂ c₂ ℓ₂₁ ℓ₂₂ : Level} {P : Poset c₁ ℓ₁₁ ℓ₁₂} {Q : Poset c₂ ℓ₂₁ ℓ₂₂} where +module _ {P : Poset c₁ ℓ₁₁ ℓ₁₂} {Q : Poset c₂ ℓ₂₁ ℓ₂₂} where private module P = Poset P module Q = Poset Q - - DirectedCompletePartialOrder+scott→monotone : (P-DirectedCompletePartialOrder : IsDirectedCompletePartialOrder P) - → (f : P.Carrier → Q.Carrier) - → (scott : IsScottContinuous P Q f) - → IsOrderHomomorphism (Poset._≈_ P) (Poset._≈_ Q) (Poset._≤_ P) (Poset._≤_ Q) f - DirectedCompletePartialOrder+scott→monotone P-DirectedCompletePartialOrder f scott = record - { cong = λ {x} {y} x≈y → IsScottContinuous.preserveEquality scott x≈y - ; mono = λ {x} {y} x≤y → mono-proof x y x≤y + + isMonotone : (P-DirectedCompletePartialOrder : IsDirectedCompletePartialOrder P) → + (f : P.Carrier → Q.Carrier) → (scott : IsScottContinuous P Q f) → + IsOrderHomomorphism P._≈_ Q._≈_ P._≤_ Q._≤_ f + isMonotone P-DirectedCompletePartialOrder f scott = record + { cong = IsScottContinuous.cong scott + ; mono = mono-proof } where - mono-proof : ∀ x y → x P.≤ y → f x Q.≤ f y - mono-proof x y x≤y = IsLub.isUpperBound fs-lub (lift true) + mono-proof : ∀ {x y} → x P.≤ y → f x Q.≤ f y + mono-proof {x} {y} x≤y = IsLub.isUpperBound fs-lub (lift true) where s : Lift c₁ Bool → P.Carrier s (lift b) = if b then x else y @@ -81,127 +77,96 @@ module _ {c₁ ℓ₁₁ ℓ₁₂ c₂ ℓ₂₁ ℓ₂₂ : Level} {P : Poset } s-lub : IsLub P s y - s-lub = record - { isLeastUpperBound = sx≤sfalse , (λ z proof → proof (lift false)) - } + s-lub = record { isLeastUpperBound = sx≤sfalse , (λ z proof → proof (lift false))} fs-lub : IsLub Q (f ∘ s) (f y) fs-lub = IsScottContinuous.preserveLub scott s-directed y s-lub - monotone∘directed : ∀ {Ix : Set c} {s : Ix → P.Carrier} - → (f : P.Carrier → Q.Carrier) - → IsOrderHomomorphism (Poset._≈_ P) (Poset._≈_ Q) (Poset._≤_ P) (Poset._≤_ Q) f - → IsDirectedFamily P s - → IsDirectedFamily Q (f ∘ s) - monotone∘directed f ismonotone dir = record + map-directed : {s : Ix → P.Carrier} → (f : P.Carrier → Q.Carrier)→ + IsOrderHomomorphism P._≈_ Q._≈_ P._≤_ Q._≤_ f → + IsDirectedFamily P s → IsDirectedFamily Q (f ∘ s) + map-directed f ismonotone dir = record { elt = IsDirectedFamily.elt dir - ; isSemidirected = λ i j → - let (k , s[i]≤s[k] , s[j]≤s[k]) = IsDirectedFamily.isSemidirected dir i j - in k , IsOrderHomomorphism.mono ismonotone s[i]≤s[k] , IsOrderHomomorphism.mono ismonotone s[j]≤s[k] + ; isSemidirected = λ i j → let (k , s[i]≤s[k] , s[j]≤s[k]) = IsDirectedFamily.isSemidirected dir i j + in k , f.mono s[i]≤s[k] , f.mono s[j]≤s[k] } + where module f = IsOrderHomomorphism ismonotone ------------------------------------------------------------------------ -- Scott continuous functions -ScottId : ∀ {c ℓ₁ ℓ₂} {P : Poset c ℓ₁ ℓ₂} → IsScottContinuous P P id -ScottId = record - { preserveLub = λ dir lub z → z - ; preserveEquality = λ z → z } - -scott-∘ : ∀ {c ℓ₁ ℓ₂} {P Q R : Poset c ℓ₁ ℓ₂} - → (f : Poset.Carrier R → Poset.Carrier Q) (g : Poset.Carrier P → Poset.Carrier R) - → IsScottContinuous R Q f → IsScottContinuous P R g - → IsOrderHomomorphism (Poset._≈_ P) (Poset._≈_ R) (Poset._≤_ P) (Poset._≤_ R) g - → IsScottContinuous P Q (f ∘ g) -scott-∘ f g scottf scottg monog = record - { preserveLub = λ dir lub z → f.preserveLub - (monotone∘directed g monog dir) - (g lub) - (g.preserveLub dir lub z) - ; preserveEquality = λ {x} {y} z → - f.preserveEquality (g.preserveEquality z) - } - where - module f = IsScottContinuous scottf - module g = IsScottContinuous scottg +module _ {P Q R : Poset c ℓ₁ ℓ₂} where + private + module P = Poset P + module Q = Poset Q + module R = Poset R + + ScottId : {P : Poset c ℓ₁ ℓ₂} → IsScottContinuous P P id + ScottId = record + { preserveLub = λ _ _ → id + ; cong = id } + + scott-cong : (f : R.Carrier → Q.Carrier) (g : P.Carrier → R.Carrier) → + IsScottContinuous R Q f → IsScottContinuous P R g → + IsOrderHomomorphism P._≈_ R._≈_ P._≤_ R._≤_ g → IsScottContinuous P Q (f ∘ g) + scott-cong f g scottf scottg monog = record + { preserveLub = λ dir lub → f.preserveLub (map-directed g monog dir) (g lub) ∘ g.preserveLub dir lub + ; cong = f.cong ∘ g.cong + } + where + module f = IsScottContinuous scottf + module g = IsScottContinuous scottg ------------------------------------------------------------------------ -- Suprema and pointwise ordering -module _ {c ℓ₁ ℓ₂} {P : Poset c ℓ₁ ℓ₂} (D : DirectedCompletePartialOrder c ℓ₁ ℓ₂) where +module _ {P : Poset c ℓ₁ ℓ₂} (D : DirectedCompletePartialOrder c ℓ₁ ℓ₂) where private module D = DirectedCompletePartialOrder D + DP = D.poset - open import Relation.Binary.Reasoning.PartialOrder D.poset - - ⋃-pointwise : ∀ {Ix} {s s' : Ix → D.Carrier} - → {fam : IsDirectedFamily D.poset s} {fam' : IsDirectedFamily D.poset s'} - → (∀ ix → s ix D.≤ s' ix) - → D.⋁ s fam D.≤ D.⋁ s' fam' - ⋃-pointwise {s = s} {s'} {fam} {fam'} p = - D.⋁-least (D.⋁ s' fam') λ i → D.trans (p i) (D.⋁-≤ i) + lub-monotone : {s s' : Ix → D.Carrier} → + {fam : IsDirectedFamily DP s} {fam' : IsDirectedFamily DP s'} → + (∀ i → s i D.≤ s' i) → D.⋁ s fam D.≤ D.⋁ s' fam' + lub-monotone {s' = s'} {fam' = fam'} p = D.⋁-least (D.⋁ s' fam') λ i → D.trans (p i) (D.⋁-≤ i) ------------------------------------------------------------------------ -- Scott continuity module module Scott - {c ℓ₁ ℓ₂} - {P : Poset c ℓ₁ ℓ₂} - {D E : DirectedCompletePartialOrder c ℓ₁ ℓ₂} - (let module D = DirectedCompletePartialOrder D) - (let module E = DirectedCompletePartialOrder E) - (f : D.Carrier → E.Carrier) - (isScott : IsScottContinuous D.poset E.poset f) - (mono : IsOrderHomomorphism (Poset._≈_ D.poset) (Poset._≈_ E.poset) - (Poset._≤_ D.poset) (Poset._≤_ E.poset) f) + (D E : DirectedCompletePartialOrder c ℓ₁ ℓ₂) where - - open DirectedCompletePartialOrder D - open DirectedCompletePartialOrder E - - pres-⋁ - : ∀ {Ix} (s : Ix → D.Carrier) → (dir : IsDirectedFamily D.poset s) - → f (D.⋁ s dir) E.≈ E.⋁ (f ∘ s) (monotone∘directed f mono dir) - pres-⋁ s dir = E.antisym - (IsLub.isLeast - (IsScottContinuous.preserveLub isScott dir (D.⋁ s dir) (D.⋁-isLub s dir)) - (E.⋁ (f ∘ s) (monotone∘directed f mono dir)) - E.⋁-≤ - ) - (IsLub.isLeast - (E.⋁-isLub (f ∘ s) (monotone∘directed f mono dir)) - (f (D.⋁ s dir)) - (λ i → IsOrderHomomorphism.mono mono (D.⋁-≤ i)) - ) - ------------------------------------------------------------------------- --- Converting to Scott continuity - -module _ {c ℓ₁ ℓ₂} {D E : DirectedCompletePartialOrder c ℓ₁ ℓ₂} where private module D = DirectedCompletePartialOrder D module E = DirectedCompletePartialOrder E + DP = D.poset + EP = E.poset - to-scott : (f : D.Carrier → E.Carrier) - → IsOrderHomomorphism (Poset._≈_ D.poset) (Poset._≈_ E.poset) - (Poset._≤_ D.poset) (Poset._≤_ E.poset) f - → (∀ {Ix} (s : Ix → D.Carrier) (dir : IsDirectedFamily D.poset s) - → IsLub E.poset (f ∘ s) (f (D.⋁ s dir))) - → IsScottContinuous D.poset E.poset f - to-scott f mono pres-⋁ = record - { preserveLub = λ {_} {s} dir lub x → - IsLub-cong E (f (D.⋁ _ dir)) (f lub) - (f.cong (uniqueLub D (D.⋁ s dir) lub (D.⋁-isLub s dir) x)) - (pres-⋁ s dir) - ; preserveEquality = f.cong - } - where module f = IsOrderHomomorphism mono - - - -- { preserveLub = λ dir lub x → IsLub-cong {! D !} {! E !} {! !} (pres-⋁ {! !} dir) ; - -- preserveEquality = IsOrderHomomorphism.cong mono - -- } - -- { preserveLub = λ dir lub x → IsLub-cong ? E (f (D.⋁ _ dir)) (f lub) - -- (IsOrderHomomorphism.cong mono (uniqueLub {P = E.poset} {D = D} (D.⋁ _ dir) lub (D.⋁-isLub _ dir) x)) - -- (pres-⋁ _ dir) - -- ; preserveEquality = IsOrderHomomorphism.cong mono } + module _ (f : D.Carrier → E.Carrier) + (isScott : IsScottContinuous DP EP f) + (mono : IsOrderHomomorphism D._≈_ E._≈_ D._≤_ E._≤_ f) + where + private module f = IsOrderHomomorphism mono + + pres-lub : (s : Ix → D.Carrier) → (dir : IsDirectedFamily DP s) → + f (D.⋁ s dir) E.≈ E.⋁ (f ∘ s) (map-directed f mono dir) + pres-lub s dir = E.antisym + (IsLub.isLeast + (IsScottContinuous.preserveLub isScott dir (D.⋁ s dir) (D.⋁-isLub s dir)) + (E.⋁ (f ∘ s) (map-directed f mono dir)) + E.⋁-≤ + ) + (IsLub.isLeast + (E.⋁-isLub (f ∘ s) (map-directed f mono dir)) + (f (D.⋁ s dir)) + (λ i → f.mono (D.⋁-≤ i)) + ) + + to-scott : (∀ {Ix} (s : Ix → D.Carrier) (dir : IsDirectedFamily DP s) → + IsLub E.poset (f ∘ s) (f (D.⋁ s dir))) → + IsScottContinuous DP EP f + to-scott pres-⋁ = record + { preserveLub = λ {_} {s} dir lub x → + IsLub-cong E (f.cong (uniqueLub D (D.⋁ s dir) lub (D.⋁-isLub s dir) x)) (pres-⋁ s dir) + ; cong = f.cong + } \ No newline at end of file From d98f028c7caab42e1fa14f3758852669ef3d7a93 Mon Sep 17 00:00:00 2001 From: Jacques Date: Tue, 17 Jun 2025 15:35:46 -0400 Subject: [PATCH 10/12] fix-whitespace --- src/Relation/Binary/Properties/Domain.agda | 26 +++++++++++----------- 1 file changed, 13 insertions(+), 13 deletions(-) diff --git a/src/Relation/Binary/Properties/Domain.agda b/src/Relation/Binary/Properties/Domain.agda index ce71bc8825..967b7ac1e6 100644 --- a/src/Relation/Binary/Properties/Domain.agda +++ b/src/Relation/Binary/Properties/Domain.agda @@ -30,17 +30,17 @@ module _ (D : DirectedCompletePartialOrder c ℓ₁ ℓ₂) where private module D = DirectedCompletePartialOrder D - uniqueLub : ∀ {s : Ix → D.Carrier} → (x y : D.Carrier) → + uniqueLub : ∀ {s : Ix → D.Carrier} → (x y : D.Carrier) → IsLub D.poset s x → IsLub D.poset s y → x D.≈ y uniqueLub x y x-lub y-lub = D.antisym (IsLub.isLeast x-lub y (IsLub.isUpperBound y-lub)) (IsLub.isLeast y-lub x (IsLub.isUpperBound x-lub)) - IsLub-cong : ∀ {s : Ix → D.Carrier} → {x y : D.Carrier} → x D.≈ y → + IsLub-cong : ∀ {s : Ix → D.Carrier} → {x y : D.Carrier} → x D.≈ y → IsLub D.poset s x → IsLub D.poset s y IsLub-cong x≈y x-lub = record - { isLeastUpperBound = - (λ i → D.trans (IsLub.isUpperBound x-lub i) (D.reflexive x≈y)) + { isLeastUpperBound = + (λ i → D.trans (IsLub.isUpperBound x-lub i) (D.reflexive x≈y)) , (λ z ub → D.trans (D.reflexive (D.Eq.sym x≈y)) (IsLub.isLeast x-lub z (λ i → D.trans (ub i) (D.reflexive D.Eq.refl)))) } @@ -51,8 +51,8 @@ module _ {P : Poset c₁ ℓ₁₁ ℓ₁₂} {Q : Poset c₂ ℓ₂₁ ℓ₂ private module P = Poset P module Q = Poset Q - - isMonotone : (P-DirectedCompletePartialOrder : IsDirectedCompletePartialOrder P) → + + isMonotone : (P-DirectedCompletePartialOrder : IsDirectedCompletePartialOrder P) → (f : P.Carrier → Q.Carrier) → (scott : IsScottContinuous P Q f) → IsOrderHomomorphism P._≈_ Q._≈_ P._≤_ Q._≤_ f isMonotone P-DirectedCompletePartialOrder f scott = record @@ -82,12 +82,12 @@ module _ {P : Poset c₁ ℓ₁₁ ℓ₁₂} {Q : Poset c₂ ℓ₂₁ ℓ₂ fs-lub : IsLub Q (f ∘ s) (f y) fs-lub = IsScottContinuous.preserveLub scott s-directed y s-lub - map-directed : {s : Ix → P.Carrier} → (f : P.Carrier → Q.Carrier)→ + map-directed : {s : Ix → P.Carrier} → (f : P.Carrier → Q.Carrier)→ IsOrderHomomorphism P._≈_ Q._≈_ P._≤_ Q._≤_ f → IsDirectedFamily P s → IsDirectedFamily Q (f ∘ s) map-directed f ismonotone dir = record { elt = IsDirectedFamily.elt dir - ; isSemidirected = λ i j → let (k , s[i]≤s[k] , s[j]≤s[k]) = IsDirectedFamily.isSemidirected dir i j + ; isSemidirected = λ i j → let (k , s[i]≤s[k] , s[j]≤s[k]) = IsDirectedFamily.isSemidirected dir i j in k , f.mono s[i]≤s[k] , f.mono s[j]≤s[k] } where module f = IsOrderHomomorphism ismonotone @@ -100,7 +100,7 @@ module _ {P Q R : Poset c ℓ₁ ℓ₂} where module P = Poset P module Q = Poset Q module R = Poset R - + ScottId : {P : Poset c ℓ₁ ℓ₂} → IsScottContinuous P P id ScottId = record { preserveLub = λ _ _ → id @@ -147,7 +147,7 @@ module Scott (mono : IsOrderHomomorphism D._≈_ E._≈_ D._≤_ E._≤_ f) where private module f = IsOrderHomomorphism mono - + pres-lub : (s : Ix → D.Carrier) → (dir : IsDirectedFamily DP s) → f (D.⋁ s dir) E.≈ E.⋁ (f ∘ s) (map-directed f mono dir) pres-lub s dir = E.antisym @@ -161,12 +161,12 @@ module Scott (f (D.⋁ s dir)) (λ i → f.mono (D.⋁-≤ i)) ) - + to-scott : (∀ {Ix} (s : Ix → D.Carrier) (dir : IsDirectedFamily DP s) → IsLub E.poset (f ∘ s) (f (D.⋁ s dir))) → IsScottContinuous DP EP f to-scott pres-⋁ = record - { preserveLub = λ {_} {s} dir lub x → + { preserveLub = λ {_} {s} dir lub x → IsLub-cong E (f.cong (uniqueLub D (D.⋁ s dir) lub (D.⋁-isLub s dir) x)) (pres-⋁ s dir) ; cong = f.cong - } \ No newline at end of file + } From 88d463a01081a96a0a10829e3d55b2de4c2afcd8 Mon Sep 17 00:00:00 2001 From: Jacques Date: Mon, 23 Jun 2025 15:49:57 -0400 Subject: [PATCH 11/12] review 2 --- src/Relation/Binary/Properties/Domain.agda | 35 ++++++++++++---------- 1 file changed, 19 insertions(+), 16 deletions(-) diff --git a/src/Relation/Binary/Properties/Domain.agda b/src/Relation/Binary/Properties/Domain.agda index 967b7ac1e6..9e39eddbe9 100644 --- a/src/Relation/Binary/Properties/Domain.agda +++ b/src/Relation/Binary/Properties/Domain.agda @@ -11,7 +11,7 @@ module Relation.Binary.Properties.Domain where open import Relation.Binary.Bundles using (Poset) open import Level using (Level; Lift; lift) open import Function using (_∘_; id) -open import Data.Product using (_,_) +open import Data.Product using (_,_; ∃) open import Data.Bool using (Bool; true; false; if_then_else_) open import Relation.Binary.Domain.Definitions open import Relation.Binary.Domain.Bundles using (DirectedCompletePartialOrder) @@ -53,10 +53,10 @@ module _ {P : Poset c₁ ℓ₁₁ ℓ₁₂} {Q : Poset c₂ ℓ₂₁ ℓ₂ module Q = Poset Q isMonotone : (P-DirectedCompletePartialOrder : IsDirectedCompletePartialOrder P) → - (f : P.Carrier → Q.Carrier) → (scott : IsScottContinuous P Q f) → + (f : P.Carrier → Q.Carrier) → (isCts : IsScottContinuous P Q f) → IsOrderHomomorphism P._≈_ Q._≈_ P._≤_ Q._≤_ f - isMonotone P-DirectedCompletePartialOrder f scott = record - { cong = IsScottContinuous.cong scott + isMonotone P-DirectedCompletePartialOrder f isCts = record + { cong = IsScottContinuous.cong isCts ; mono = mono-proof } where @@ -77,20 +77,23 @@ module _ {P : Poset c₁ ℓ₁₁ ℓ₁₂} {Q : Poset c₂ ℓ₂₁ ℓ₂ } s-lub : IsLub P s y - s-lub = record { isLeastUpperBound = sx≤sfalse , (λ z proof → proof (lift false))} + s-lub = record { isLeastUpperBound = sx≤sfalse , (λ _ proof → proof (lift false))} fs-lub : IsLub Q (f ∘ s) (f y) - fs-lub = IsScottContinuous.preserveLub scott s-directed y s-lub + fs-lub = IsScottContinuous.preserveLub isCts s-directed y s-lub map-directed : {s : Ix → P.Carrier} → (f : P.Carrier → Q.Carrier)→ IsOrderHomomorphism P._≈_ Q._≈_ P._≤_ Q._≤_ f → IsDirectedFamily P s → IsDirectedFamily Q (f ∘ s) map-directed f ismonotone dir = record { elt = IsDirectedFamily.elt dir - ; isSemidirected = λ i j → let (k , s[i]≤s[k] , s[j]≤s[k]) = IsDirectedFamily.isSemidirected dir i j - in k , f.mono s[i]≤s[k] , f.mono s[j]≤s[k] + ; isSemidirected = semi } - where module f = IsOrderHomomorphism ismonotone + where + module f = IsOrderHomomorphism ismonotone + + semi = λ i j → let (k , s[i]≤s[k] , s[j]≤s[k]) = IsDirectedFamily.isSemidirected dir i j + in k , f.mono s[i]≤s[k] , f.mono s[j]≤s[k] ------------------------------------------------------------------------ -- Scott continuous functions @@ -106,16 +109,16 @@ module _ {P Q R : Poset c ℓ₁ ℓ₂} where { preserveLub = λ _ _ → id ; cong = id } - scott-cong : (f : R.Carrier → Q.Carrier) (g : P.Carrier → R.Carrier) → + cts-cong : (f : R.Carrier → Q.Carrier) (g : P.Carrier → R.Carrier) → IsScottContinuous R Q f → IsScottContinuous P R g → IsOrderHomomorphism P._≈_ R._≈_ P._≤_ R._≤_ g → IsScottContinuous P Q (f ∘ g) - scott-cong f g scottf scottg monog = record + cts-cong f g isCtsf isCtsG monog = record { preserveLub = λ dir lub → f.preserveLub (map-directed g monog dir) (g lub) ∘ g.preserveLub dir lub ; cong = f.cong ∘ g.cong } where - module f = IsScottContinuous scottf - module g = IsScottContinuous scottg + module f = IsScottContinuous isCtsf + module g = IsScottContinuous isCtsG ------------------------------------------------------------------------ -- Suprema and pointwise ordering @@ -133,7 +136,7 @@ module _ {P : Poset c ℓ₁ ℓ₂} (D : DirectedCompletePartialOrder c ℓ₁ ------------------------------------------------------------------------ -- Scott continuity module -module Scott +module ScottContinuity (D E : DirectedCompletePartialOrder c ℓ₁ ℓ₂) where private @@ -162,10 +165,10 @@ module Scott (λ i → f.mono (D.⋁-≤ i)) ) - to-scott : (∀ {Ix} (s : Ix → D.Carrier) (dir : IsDirectedFamily DP s) → + isScottContinuous : (∀ {Ix} (s : Ix → D.Carrier) (dir : IsDirectedFamily DP s) → IsLub E.poset (f ∘ s) (f (D.⋁ s dir))) → IsScottContinuous DP EP f - to-scott pres-⋁ = record + isScottContinuous pres-⋁ = record { preserveLub = λ {_} {s} dir lub x → IsLub-cong E (f.cong (uniqueLub D (D.⋁ s dir) lub (D.⋁-isLub s dir) x)) (pres-⋁ s dir) ; cong = f.cong From 2199f7948f951fb752e20280b60acd569155241c Mon Sep 17 00:00:00 2001 From: Jacques Date: Mon, 23 Jun 2025 15:51:00 -0400 Subject: [PATCH 12/12] fix-whitespace --- src/Relation/Binary/Properties/Domain.agda | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Relation/Binary/Properties/Domain.agda b/src/Relation/Binary/Properties/Domain.agda index 9e39eddbe9..7e72e1a109 100644 --- a/src/Relation/Binary/Properties/Domain.agda +++ b/src/Relation/Binary/Properties/Domain.agda @@ -89,11 +89,11 @@ module _ {P : Poset c₁ ℓ₁₁ ℓ₁₂} {Q : Poset c₂ ℓ₂₁ ℓ₂ { elt = IsDirectedFamily.elt dir ; isSemidirected = semi } - where + where module f = IsOrderHomomorphism ismonotone - semi = λ i j → let (k , s[i]≤s[k] , s[j]≤s[k]) = IsDirectedFamily.isSemidirected dir i j - in k , f.mono s[i]≤s[k] , f.mono s[j]≤s[k] + semi = λ i j → let (k , s[i]≤s[k] , s[j]≤s[k]) = IsDirectedFamily.isSemidirected dir i j + in k , f.mono s[i]≤s[k] , f.mono s[j]≤s[k] ------------------------------------------------------------------------ -- Scott continuous functions