[Add] Initial files for Domain theory

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 `DirectedCompletePartialOrder`, `Lub`, and `ScottContinuous`.
+  - All files for domain theory are now available in `src/Relation/Binary/Domain/`.
+
 Additions to existing modules
 -----------------------------
 

src/Padrightpropertiesdraft.agda

@@ -0,0 +1,105 @@
+------------------------------------------------------------------------
+-- 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)
+

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

src/Relation/Binary/Domain/Bundles.agda

@@ -0,0 +1,63 @@
+------------------------------------------------------------------------
+-- 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
+
+------------------------------------------------------------------------
+-- Directed Complete Partial Orders
+------------------------------------------------------------------------
+
+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
+  field
+    poset                             : Poset c ℓ₁ ℓ₂
+    isDirectedCompletePartialOrder    : IsDirectedCompletePartialOrder poset
+
+  open Poset poset public
+  open IsDirectedCompletePartialOrder isDirectedCompletePartialOrder public
+
+------------------------------------------------------------------------
+-- Scott-continuous functions
+------------------------------------------------------------------------
+
+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 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
+  open Poset P
+  field
+    lub   : Carrier
+    isLub : IsLub P f lub

src/Relation/Binary/Domain/Definitions.agda

@@ -0,0 +1,38 @@
+------------------------------------------------------------------------
+-- 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.Core using (Rel)
+
+private
+  variable
+    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))
+
+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)

src/Relation/Binary/Domain/Structures.agda

@@ -0,0 +1,79 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Structures for domain theory
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Relation.Binary.Domain.Structures where
+
+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
+
+private variable
+  a b c ℓ ℓ₁ ℓ₂ : Level
+  A B : Set a
+
+
+module _ {c ℓ₁ ℓ₂ : Level} (P : Poset c ℓ₁ ℓ₂) where
+  open Poset P
+
+  record IsLub {b : Level} {B : Set b} (f : B → Carrier)
+               (lub : Carrier) : Set (b ⊔ 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 = proj₂ isLeastUpperBound
+
+  record IsDirectedFamily {b : Level} {B : Set b} (f : B → Carrier)
+    : Set (b ⊔ c ⊔ ℓ₁ ⊔ ℓ₂) where
+    no-eta-equality
+    field
+      elt           : B
+      isSemidirected : semidirected _≤_ B f
+
+  record IsDirectedCompletePartialOrder : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+    field
+      ⋁ : ∀ {B : Set c}
+        → (f : B → Carrier)
+        → IsDirectedFamily f
+        → Carrier
+      ⋁-isLub : ∀ {B : Set c}
+        → (f : B → Carrier)
+        → (dir : IsDirectedFamily f)
+        → IsLub f (⋁ f dir)
+
+    module _ {B : Set c} {f : B → Carrier} {dir : IsDirectedFamily f} where
+      open IsLub (⋁-isLub f dir)
+        renaming (isUpperBound to ⋁-≤; isLeast to ⋁-least)
+        public
+
+------------------------------------------------------------------------
+-- 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₁ ⊔ ℓ₁₁ ⊔ ℓ₁₂ ⊔ c₂ ⊔ ℓ₂₁ ⊔ ℓ₂₂)) where
+    field
+      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