Compare commits
No commits in common. "b1c6b4c99a0c14353cc56054b5dee5d5913da05a" and "45f2babfa390ad860d7ecd11bd5bf9de85dd79cd" have entirely different histories.
b1c6b4c99a
...
45f2babfa3
@ -279,14 +279,6 @@ 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 ]
|
||||||
@ -337,12 +329,3 @@ module Plain where
|
|||||||
{ isLattice = isLattice
|
{ isLattice = isLattice
|
||||||
; fixedHeight = (((⊥ , ⊤) , longestChain) , isLongest)
|
; fixedHeight = (((⊥ , ⊤) , longestChain) , isLongest)
|
||||||
}
|
}
|
||||||
|
|
||||||
finiteHeightLattice : FiniteHeightLattice AboveBelow
|
|
||||||
finiteHeightLattice = record
|
|
||||||
{ height = 2
|
|
||||||
; _≈_ = _≈_
|
|
||||||
; _⊔_ = _⊔_
|
|
||||||
; _⊓_ = _⊓_
|
|
||||||
; isFiniteHeightLattice = isFiniteHeightLattice
|
|
||||||
}
|
|
||||||
|
@ -76,11 +76,3 @@ 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
|
|
||||||
}
|
|
||||||
|
@ -21,14 +21,17 @@ 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
|
||||||
lattice : ∀ {k : ℕ} → Lattice (IterProd k)
|
BLattice : Lattice B
|
||||||
lattice {0} = record
|
BLattice = record
|
||||||
{ _≈_ = _≈₂_
|
{ _≈_ = _≈₂_
|
||||||
; _⊔_ = _⊔₂_
|
; _⊔_ = _⊔₂_
|
||||||
; _⊓_ = _⊓₂_
|
; _⊓_ = _⊓₂_
|
||||||
; isLattice = lB
|
; isLattice = lB
|
||||||
}
|
}
|
||||||
lattice {suc k'} = record
|
|
||||||
|
IterProdLattice : ∀ {k : ℕ} → Lattice (IterProd k)
|
||||||
|
IterProdLattice {0} = BLattice
|
||||||
|
IterProdLattice {suc k'} = record
|
||||||
{ _≈_ = _≈_
|
{ _≈_ = _≈_
|
||||||
; _⊔_ = _⊔_
|
; _⊔_ = _⊔_
|
||||||
; _⊓_ = _⊓_
|
; _⊓_ = _⊓_
|
||||||
@ -36,7 +39,7 @@ private module _ where
|
|||||||
}
|
}
|
||||||
where
|
where
|
||||||
Right : Lattice (IterProd k')
|
Right : Lattice (IterProd k')
|
||||||
Right = lattice {k'}
|
Right = IterProdLattice {k'}
|
||||||
|
|
||||||
open import Lattice.Prod
|
open import Lattice.Prod
|
||||||
_≈₁_ (Lattice._≈_ Right)
|
_≈₁_ (Lattice._≈_ Right)
|
||||||
@ -44,9 +47,6 @@ 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
|
||||||
|
|
||||||
finiteHeightAndDec : ∀ {k : ℕ} → FiniteHeightAndDecEq (IterProd k)
|
BFiniteHeightLattice : FiniteHeightAndDecEq B
|
||||||
finiteHeightAndDec {0} = record
|
BFiniteHeightLattice = record
|
||||||
{ height = h₂
|
{ height = h₂
|
||||||
; _≈_ = _≈₂_
|
; _≈_ = _≈₂_
|
||||||
; _⊔_ = _⊔₂_
|
; _⊔_ = _⊔₂_
|
||||||
@ -76,11 +76,14 @@ 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)
|
||||||
@ -88,25 +91,17 @@ module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
|
|||||||
; ≈-dec = ≈-dec ≈₁-dec (FiniteHeightAndDecEq.≈-dec Right)
|
; ≈-dec = ≈-dec ≈₁-dec (FiniteHeightAndDecEq.≈-dec Right)
|
||||||
}
|
}
|
||||||
where
|
where
|
||||||
Right = finiteHeightAndDec {k'}
|
Right = IterProdFiniteHeightLattice {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) as P
|
lA (FiniteHeightAndDecEq.isLattice Right)
|
||||||
|
|
||||||
module _ (k : ℕ) where
|
module _ (k : ℕ) where
|
||||||
open FiniteHeightAndDecEq (finiteHeightAndDec {k}) using (isFiniteHeightLattice) public
|
open FiniteHeightAndDecEq (IterProdFiniteHeightLattice {k}) using (fixedHeight) public
|
||||||
|
|
||||||
private
|
-- Expose the computed definition in public.
|
||||||
FHD = finiteHeightAndDec {k}
|
module _ (k : ℕ) where
|
||||||
|
open Lattice.Lattice (IterProdLattice {k}) public
|
||||||
finiteHeightLattice : FiniteHeightLattice (IterProd k)
|
|
||||||
finiteHeightLattice = record
|
|
||||||
{ height = FiniteHeightAndDecEq.height FHD
|
|
||||||
; _≈_ = FiniteHeightAndDecEq._≈_ FHD
|
|
||||||
; _⊔_ = FiniteHeightAndDecEq._⊔_ FHD
|
|
||||||
; _⊓_ = FiniteHeightAndDecEq._⊓_ FHD
|
|
||||||
; isFiniteHeightLattice = isFiniteHeightLattice
|
|
||||||
}
|
|
||||||
|
@ -882,14 +882,6 @@ 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₂
|
||||||
|
|
||||||
|
@ -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; lattice
|
; isUnionSemilattice; isIntersectSemilattice; isLattice
|
||||||
) public
|
) public
|
||||||
|
|
||||||
MapSet : Set a
|
MapSet : Set a
|
||||||
|
@ -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
|
||||||
|
|
||||||
isMaxSemilattice : IsSemilattice ℕ _≡_ _⊔_
|
NatIsMaxSemilattice : IsSemilattice ℕ _≡_ _⊔_
|
||||||
isMaxSemilattice = record
|
NatIsMaxSemilattice = record
|
||||||
{ ≈-equiv = record
|
{ ≈-equiv = record
|
||||||
{ ≈-refl = refl
|
{ ≈-refl = refl
|
||||||
; ≈-sym = sym
|
; ≈-sym = sym
|
||||||
@ -31,8 +31,8 @@ isMaxSemilattice = record
|
|||||||
; ⊔-idemp = ⊔-idem
|
; ⊔-idemp = ⊔-idem
|
||||||
}
|
}
|
||||||
|
|
||||||
isMinSemilattice : IsSemilattice ℕ _≡_ _⊓_
|
NatIsMinSemilattice : IsSemilattice ℕ _≡_ _⊓_
|
||||||
isMinSemilattice = record
|
NatIsMinSemilattice = record
|
||||||
{ ≈-equiv = record
|
{ ≈-equiv = record
|
||||||
{ ≈-refl = refl
|
{ ≈-refl = refl
|
||||||
; ≈-sym = sym
|
; ≈-sym = sym
|
||||||
@ -74,18 +74,10 @@ 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
|
||||||
|
|
||||||
isLattice : IsLattice ℕ _≡_ _⊔_ _⊓_
|
NatIsLattice : IsLattice ℕ _≡_ _⊔_ _⊓_
|
||||||
isLattice = record
|
NatIsLattice = record
|
||||||
{ joinSemilattice = isMaxSemilattice
|
{ joinSemilattice = NatIsMaxSemilattice
|
||||||
; meetSemilattice = isMinSemilattice
|
; meetSemilattice = NatIsMinSemilattice
|
||||||
; 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
|
|
||||||
}
|
|
||||||
|
@ -94,13 +94,6 @@ 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 _≈_
|
||||||
@ -183,12 +176,3 @@ 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
|
|
||||||
}
|
|
||||||
|
@ -89,14 +89,6 @@ 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
|
||||||
@ -112,12 +104,3 @@ isFiniteHeightLattice = record
|
|||||||
{ isLattice = isLattice
|
{ isLattice = isLattice
|
||||||
; fixedHeight = (((tt , tt) , longestChain) , isLongest)
|
; fixedHeight = (((tt , tt) , longestChain) , isLongest)
|
||||||
}
|
}
|
||||||
|
|
||||||
finiteHeightLattice : FiniteHeightLattice ⊤
|
|
||||||
finiteHeightLattice = record
|
|
||||||
{ height = 0
|
|
||||||
; _≈_ = _≈_
|
|
||||||
; _⊔_ = _⊔_
|
|
||||||
; _⊓_ = _⊓_
|
|
||||||
; isFiniteHeightLattice = isFiniteHeightLattice
|
|
||||||
}
|
|
||||||
|
Loading…
Reference in New Issue
Block a user