Compare commits

..

9 Commits

Author SHA1 Message Date
b1c6b4c99a Expose bundles from Unit
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-02-11 21:20:05 -08:00
5420bb808e Expose bundles from 'Prod'
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-02-11 21:16:41 -08:00
4c0860f4c7 Expose bundle form MapSet
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-02-11 21:14:49 -08:00
e89418d600 Expose bundle form 'Map'
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-02-11 21:12:49 -08:00
bfb32092c2 Expose bundles and apply so renames to IterProd
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-02-11 21:10:51 -08:00
6e26aa1580 Add a bundle to FiniteMap
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-02-11 21:02:43 -08:00
27f40bd42e Add bundles to 'AboveBelow'
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-02-11 21:00:28 -08:00
08f3f49640 Rename some definitions in Nat and expose bundle
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-02-11 20:56:21 -08:00
a920608bef Tweak IterProd to expose more (including a bundle)
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-02-11 20:45:14 -08:00
8 changed files with 110 additions and 31 deletions

View File

@ -279,6 +279,14 @@ module Plain where
; absorb-⊓-⊔ = absorb-⊓-⊔ ; absorb-⊓-⊔ = absorb-⊓-⊔
} }
lattice : Lattice AboveBelow
lattice = record
{ _≈_ = _≈_
; _⊔_ = _⊔_
; _⊓_ = _⊓_
; isLattice = isLattice
}
open IsLattice isLattice using (_≼_; _≺_) open IsLattice isLattice using (_≼_; _≺_)
⊥≺[x] : (x : A) [ x ] ⊥≺[x] : (x : A) [ x ]
@ -329,3 +337,12 @@ module Plain where
{ isLattice = isLattice { isLattice = isLattice
; fixedHeight = ((( , ) , longestChain) , isLongest) ; fixedHeight = ((( , ) , longestChain) , isLongest)
} }
finiteHeightLattice : FiniteHeightLattice AboveBelow
finiteHeightLattice = record
{ height = 2
; _≈_ = _≈_
; _⊔_ = _⊔_
; _⊓_ = _⊓_
; isFiniteHeightLattice = isFiniteHeightLattice
}

View File

@ -76,3 +76,11 @@ module _ (ks : List A) where
; absorb-⊔-⊓ = λ (m₁ , _) (m₂ , _) absorb-⊔ᵐ-⊓ᵐ m₁ m₂ ; absorb-⊔-⊓ = λ (m₁ , _) (m₂ , _) absorb-⊔ᵐ-⊓ᵐ m₁ m₂
; absorb-⊓-⊔ = λ (m₁ , _) (m₂ , _) absorb-⊓ᵐ-⊔ᵐ m₁ m₂ ; absorb-⊓-⊔ = λ (m₁ , _) (m₂ , _) absorb-⊓ᵐ-⊔ᵐ m₁ m₂
} }
lattice : Lattice FiniteMap
lattice = record
{ _≈_ = _≈_
; _⊔_ = _⊔_
; _⊓_ = _⊓_
; isLattice = isLattice
}

View File

@ -21,17 +21,14 @@ IterProd k = iterate k (λ t → A × t) B
-- records, perform the recursion, and unpackage. -- records, perform the recursion, and unpackage.
private module _ where private module _ where
BLattice : Lattice B lattice : {k : } Lattice (IterProd k)
BLattice = record lattice {0} = record
{ _≈_ = _≈₂_ { _≈_ = _≈₂_
; _⊔_ = _⊔₂_ ; _⊔_ = _⊔₂_
; _⊓_ = _⊓₂_ ; _⊓_ = _⊓₂_
; isLattice = lB ; isLattice = lB
} }
lattice {suc k'} = record
IterProdLattice : {k : } Lattice (IterProd k)
IterProdLattice {0} = BLattice
IterProdLattice {suc k'} = record
{ _≈_ = _≈_ { _≈_ = _≈_
; _⊔_ = _⊔_ ; _⊔_ = _⊔_
; _⊓_ = _⊓_ ; _⊓_ = _⊓_
@ -39,7 +36,7 @@ private module _ where
} }
where where
Right : Lattice (IterProd k') Right : Lattice (IterProd k')
Right = IterProdLattice {k'} Right = lattice {k'}
open import Lattice.Prod open import Lattice.Prod
_≈₁_ (Lattice._≈_ Right) _≈₁_ (Lattice._≈_ Right)
@ -47,6 +44,9 @@ private module _ where
_⊓₁_ (Lattice._⊓_ Right) _⊓₁_ (Lattice._⊓_ Right)
lA (Lattice.isLattice Right) lA (Lattice.isLattice Right)
module _ (k : ) where
open Lattice.Lattice (lattice {k}) public
module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_) module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
(h₁ h₂ : ) (h₁ h₂ : )
(fhA : FixedHeight₁ h₁) (fhB : FixedHeight₂ h₂) where (fhA : FixedHeight₁ h₁) (fhB : FixedHeight₂ h₂) where
@ -64,8 +64,8 @@ module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
open IsFiniteHeightLattice isFiniteHeightLattice public open IsFiniteHeightLattice isFiniteHeightLattice public
BFiniteHeightLattice : FiniteHeightAndDecEq B finiteHeightAndDec : {k : } FiniteHeightAndDecEq (IterProd k)
BFiniteHeightLattice = record finiteHeightAndDec {0} = record
{ height = h₂ { height = h₂
; _≈_ = _≈₂_ ; _≈_ = _≈₂_
; _⊔_ = _⊔₂_ ; _⊔_ = _⊔₂_
@ -76,14 +76,11 @@ module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
} }
; ≈-dec = ≈₂-dec ; ≈-dec = ≈₂-dec
} }
finiteHeightAndDec {suc k'} = record
IterProdFiniteHeightLattice : {k : } FiniteHeightAndDecEq (IterProd k)
IterProdFiniteHeightLattice {0} = BFiniteHeightLattice
IterProdFiniteHeightLattice {suc k'} = record
{ height = h₁ + FiniteHeightAndDecEq.height Right { height = h₁ + FiniteHeightAndDecEq.height Right
; _≈_ = _≈_ ; _≈_ = P._≈_
; _⊔_ = _⊔_ ; _⊔_ = P._⊔_
; _⊓_ = _⊓_ ; _⊓_ = P._⊓_
; isFiniteHeightLattice = isFiniteHeightLattice ; isFiniteHeightLattice = isFiniteHeightLattice
≈₁-dec (FiniteHeightAndDecEq.≈-dec Right) ≈₁-dec (FiniteHeightAndDecEq.≈-dec Right)
h₁ (FiniteHeightAndDecEq.height Right) h₁ (FiniteHeightAndDecEq.height Right)
@ -91,17 +88,25 @@ module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
; ≈-dec = ≈-dec ≈₁-dec (FiniteHeightAndDecEq.≈-dec Right) ; ≈-dec = ≈-dec ≈₁-dec (FiniteHeightAndDecEq.≈-dec Right)
} }
where where
Right = IterProdFiniteHeightLattice {k'} Right = finiteHeightAndDec {k'}
open import Lattice.Prod open import Lattice.Prod
_≈₁_ (FiniteHeightAndDecEq._≈_ Right) _≈₁_ (FiniteHeightAndDecEq._≈_ Right)
_⊔₁_ (FiniteHeightAndDecEq._⊔_ Right) _⊔₁_ (FiniteHeightAndDecEq._⊔_ Right)
_⊓₁_ (FiniteHeightAndDecEq._⊓_ Right) _⊓₁_ (FiniteHeightAndDecEq._⊓_ Right)
lA (FiniteHeightAndDecEq.isLattice Right) lA (FiniteHeightAndDecEq.isLattice Right) as P
module _ (k : ) where module _ (k : ) where
open FiniteHeightAndDecEq (IterProdFiniteHeightLattice {k}) using (fixedHeight) public open FiniteHeightAndDecEq (finiteHeightAndDec {k}) using (isFiniteHeightLattice) public
-- Expose the computed definition in public. private
module _ (k : ) where FHD = finiteHeightAndDec {k}
open Lattice.Lattice (IterProdLattice {k}) public
finiteHeightLattice : FiniteHeightLattice (IterProd k)
finiteHeightLattice = record
{ height = FiniteHeightAndDecEq.height FHD
; _≈_ = FiniteHeightAndDecEq._≈_ FHD
; _⊔_ = FiniteHeightAndDecEq._⊔_ FHD
; _⊓_ = FiniteHeightAndDecEq._⊓_ FHD
; isFiniteHeightLattice = isFiniteHeightLattice
}

View File

@ -882,6 +882,14 @@ isLattice = record
; absorb-⊓-⊔ = absorb-⊓-⊔ ; absorb-⊓-⊔ = absorb-⊓-⊔
} }
lattice : Lattice Map
lattice = record
{ _≈_ = _≈_
; _⊔_ = _⊔_
; _⊓_ = _⊓_
; isLattice = isLattice
}
⊔-equal-keys : {m₁ m₂ : Map} keys m₁ keys m₂ keys m₁ keys (m₁ m₂) ⊔-equal-keys : {m₁ m₂ : Map} keys m₁ keys m₂ keys m₁ keys (m₁ m₂)
⊔-equal-keys km₁≡km₂ = union-equal-keys km₁≡km₂ ⊔-equal-keys km₁≡km₂ = union-equal-keys km₁≡km₂

View File

@ -12,7 +12,7 @@ private module UnitMap = Lattice.Map A _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A
open UnitMap using (Map) open UnitMap using (Map)
open UnitMap using open UnitMap using
( _⊆_; _≈_; ≈-equiv; _⊔_; _⊓_ ( _⊆_; _≈_; ≈-equiv; _⊔_; _⊓_
; isUnionSemilattice; isIntersectSemilattice; isLattice ; isUnionSemilattice; isIntersectSemilattice; isLattice; lattice
) public ) public
MapSet : Set a MapSet : Set a

View File

@ -18,8 +18,8 @@ private
≡-⊓-cong : {a₁ a₂ a₃ a₄} a₁ a₂ a₃ a₄ (a₁ a₃) (a₂ a₄) ≡-⊓-cong : {a₁ a₂ a₃ a₄} a₁ a₂ a₃ a₄ (a₁ a₃) (a₂ a₄)
≡-⊓-cong a₁≡a₂ a₃≡a₄ rewrite a₁≡a₂ rewrite a₃≡a₄ = refl ≡-⊓-cong a₁≡a₂ a₃≡a₄ rewrite a₁≡a₂ rewrite a₃≡a₄ = refl
NatIsMaxSemilattice : IsSemilattice _≡_ _⊔_ isMaxSemilattice : IsSemilattice _≡_ _⊔_
NatIsMaxSemilattice = record isMaxSemilattice = record
{ ≈-equiv = record { ≈-equiv = record
{ ≈-refl = refl { ≈-refl = refl
; ≈-sym = sym ; ≈-sym = sym
@ -31,8 +31,8 @@ NatIsMaxSemilattice = record
; ⊔-idemp = ⊔-idem ; ⊔-idemp = ⊔-idem
} }
NatIsMinSemilattice : IsSemilattice _≡_ _⊓_ isMinSemilattice : IsSemilattice _≡_ _⊓_
NatIsMinSemilattice = record isMinSemilattice = record
{ ≈-equiv = record { ≈-equiv = record
{ ≈-refl = refl { ≈-refl = refl
; ≈-sym = sym ; ≈-sym = sym
@ -74,10 +74,18 @@ private
helper : x (x y) x x x x x x (x y) x helper : x (x y) x x x x x x (x y) x
helper x⊔x⊓y≤x⊔x x⊔x≡x rewrite x⊔x≡x = x⊔x⊓y≤x⊔x helper x⊔x⊓y≤x⊔x x⊔x≡x rewrite x⊔x≡x = x⊔x⊓y≤x⊔x
NatIsLattice : IsLattice _≡_ _⊔_ _⊓_ isLattice : IsLattice _≡_ _⊔_ _⊓_
NatIsLattice = record isLattice = record
{ joinSemilattice = NatIsMaxSemilattice { joinSemilattice = isMaxSemilattice
; meetSemilattice = NatIsMinSemilattice ; meetSemilattice = isMinSemilattice
; absorb-⊔-⊓ = λ x y maxmin-absorb {x} {y} ; absorb-⊔-⊓ = λ x y maxmin-absorb {x} {y}
; absorb-⊓-⊔ = λ x y minmax-absorb {x} {y} ; absorb-⊓-⊔ = λ x y minmax-absorb {x} {y}
} }
lattice : Lattice
lattice = record
{ _≈_ = _≡_
; _⊔_ = _⊔_
; _⊓_ = _⊓_
; isLattice = isLattice
}

View File

@ -94,6 +94,13 @@ isLattice = record
) )
} }
lattice : Lattice (A × B)
lattice = record
{ _≈_ = _≈_
; _⊔_ = _⊔_
; _⊓_ = _⊓_
; isLattice = isLattice
}
module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_) where module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_) where
≈-dec : IsDecidable _≈_ ≈-dec : IsDecidable _≈_
@ -176,3 +183,12 @@ module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
in ≤-trans n≤n₁+n₂ (+-mono-≤ (proj₂ fhA a₁a₂) (proj₂ fhB b₁b₂)) in ≤-trans n≤n₁+n₂ (+-mono-≤ (proj₂ fhA a₁a₂) (proj₂ fhB b₁b₂))
) )
} }
finiteHeightLattice : FiniteHeightLattice (A × B)
finiteHeightLattice = record
{ height = h₁ + h₂
; _≈_ = _≈_
; _⊔_ = _⊔_
; _⊓_ = _⊓_
; isFiniteHeightLattice = isFiniteHeightLattice
}

View File

@ -89,6 +89,14 @@ isLattice = record
; absorb-⊓-⊔ = absorb-⊓-⊔ ; absorb-⊓-⊔ = absorb-⊓-⊔
} }
lattice : Lattice
lattice = record
{ _≈_ = _≈_
; _⊔_ = _⊔_
; _⊓_ = _⊓_
; isLattice = isLattice
}
open Chain _≈_ ≈-equiv (IsLattice._≺_ isLattice) (IsLattice.≺-cong isLattice) open Chain _≈_ ≈-equiv (IsLattice._≺_ isLattice) (IsLattice.≺-cong isLattice)
private private
@ -104,3 +112,12 @@ isFiniteHeightLattice = record
{ isLattice = isLattice { isLattice = isLattice
; fixedHeight = (((tt , tt) , longestChain) , isLongest) ; fixedHeight = (((tt , tt) , longestChain) , isLongest)
} }
finiteHeightLattice : FiniteHeightLattice
finiteHeightLattice = record
{ height = 0
; _≈_ = _≈_
; _⊔_ = _⊔_
; _⊓_ = _⊓_
; isFiniteHeightLattice = isFiniteHeightLattice
}