279 lines
12 KiB
Agda
279 lines
12 KiB
Agda
module Lattice where
|
||
|
||
open import Equivalence
|
||
import Chain
|
||
|
||
open import Relation.Binary.Core using (_Preserves_⟶_ )
|
||
open import Relation.Nullary using (Dec; ¬_)
|
||
open import Data.Nat as Nat using (ℕ)
|
||
open import Data.Product using (_×_; Σ; _,_)
|
||
open import Data.Sum using (_⊎_; inj₁; inj₂)
|
||
open import Agda.Primitive using (lsuc; Level) renaming (_⊔_ to _⊔ℓ_)
|
||
open import Function.Definitions using (Injective)
|
||
|
||
IsDecidable : ∀ {a} {A : Set a} (R : A → A → Set a) → Set a
|
||
IsDecidable {a} {A} R = ∀ (a₁ a₂ : A) → Dec (R a₁ a₂)
|
||
|
||
module _ {a b} {A : Set a} {B : Set b}
|
||
(_≼₁_ : A → A → Set a) (_≼₂_ : B → B → Set b) where
|
||
|
||
Monotonic : (A → B) → Set (a ⊔ℓ b)
|
||
Monotonic f = ∀ {a₁ a₂ : A} → a₁ ≼₁ a₂ → f a₁ ≼₂ f a₂
|
||
|
||
record IsSemilattice {a} (A : Set a)
|
||
(_≈_ : A → A → Set a)
|
||
(_⊔_ : A → A → A) : Set a where
|
||
|
||
_≼_ : A → A → Set a
|
||
a ≼ b = (a ⊔ b) ≈ b
|
||
|
||
_≺_ : A → A → Set a
|
||
a ≺ b = (a ≼ b) × (¬ a ≈ b)
|
||
|
||
field
|
||
≈-equiv : IsEquivalence A _≈_
|
||
≈-⊔-cong : ∀ {a₁ a₂ a₃ a₄} → a₁ ≈ a₂ → a₃ ≈ a₄ → (a₁ ⊔ a₃) ≈ (a₂ ⊔ a₄)
|
||
|
||
⊔-assoc : (x y z : A) → ((x ⊔ y) ⊔ z) ≈ (x ⊔ (y ⊔ z))
|
||
⊔-comm : (x y : A) → (x ⊔ y) ≈ (y ⊔ x)
|
||
⊔-idemp : (x : A) → (x ⊔ x) ≈ x
|
||
|
||
open IsEquivalence ≈-equiv public
|
||
|
||
open import Relation.Binary.Reasoning.Base.Single _≈_ ≈-refl ≈-trans
|
||
|
||
⊔-Monotonicˡ : ∀ (a₁ : A) → Monotonic _≼_ _≼_ (λ a₂ → a₁ ⊔ a₂)
|
||
⊔-Monotonicˡ a {a₁} {a₂} a₁≼a₂ = ≈-trans (≈-sym lhs) (≈-⊔-cong (≈-refl {a}) a₁≼a₂)
|
||
where
|
||
lhs =
|
||
begin
|
||
a ⊔ (a₁ ⊔ a₂)
|
||
∼⟨ ≈-⊔-cong (≈-sym (⊔-idemp _)) ≈-refl ⟩
|
||
(a ⊔ a) ⊔ (a₁ ⊔ a₂)
|
||
∼⟨ ⊔-assoc _ _ _ ⟩
|
||
a ⊔ (a ⊔ (a₁ ⊔ a₂))
|
||
∼⟨ ≈-⊔-cong ≈-refl (≈-sym (⊔-assoc _ _ _)) ⟩
|
||
a ⊔ ((a ⊔ a₁) ⊔ a₂)
|
||
∼⟨ ≈-⊔-cong ≈-refl (≈-⊔-cong (⊔-comm _ _) ≈-refl) ⟩
|
||
a ⊔ ((a₁ ⊔ a) ⊔ a₂)
|
||
∼⟨ ≈-⊔-cong ≈-refl (⊔-assoc _ _ _) ⟩
|
||
a ⊔ (a₁ ⊔ (a ⊔ a₂))
|
||
∼⟨ ≈-sym (⊔-assoc _ _ _) ⟩
|
||
(a ⊔ a₁) ⊔ (a ⊔ a₂)
|
||
∎
|
||
|
||
⊔-Monotonicʳ : ∀ (a₂ : A) → Monotonic _≼_ _≼_ (λ a₁ → a₁ ⊔ a₂)
|
||
⊔-Monotonicʳ a {a₁} {a₂} a₁≼a₂ = ≈-trans (≈-sym lhs) (≈-⊔-cong a₁≼a₂ (≈-refl {a}))
|
||
where
|
||
lhs =
|
||
begin
|
||
(a₁ ⊔ a₂) ⊔ a
|
||
∼⟨ ≈-⊔-cong ≈-refl (≈-sym (⊔-idemp _)) ⟩
|
||
(a₁ ⊔ a₂) ⊔ (a ⊔ a)
|
||
∼⟨ ≈-sym (⊔-assoc _ _ _) ⟩
|
||
((a₁ ⊔ a₂) ⊔ a) ⊔ a
|
||
∼⟨ ≈-⊔-cong (⊔-assoc _ _ _) ≈-refl ⟩
|
||
(a₁ ⊔ (a₂ ⊔ a)) ⊔ a
|
||
∼⟨ ≈-⊔-cong (≈-⊔-cong ≈-refl (⊔-comm _ _)) ≈-refl ⟩
|
||
(a₁ ⊔ (a ⊔ a₂)) ⊔ a
|
||
∼⟨ ≈-⊔-cong (≈-sym (⊔-assoc _ _ _)) ≈-refl ⟩
|
||
((a₁ ⊔ a) ⊔ a₂) ⊔ a
|
||
∼⟨ ⊔-assoc _ _ _ ⟩
|
||
(a₁ ⊔ a) ⊔ (a₂ ⊔ a)
|
||
∎
|
||
|
||
≼-refl : ∀ (a : A) → a ≼ a
|
||
≼-refl a = ⊔-idemp a
|
||
|
||
≼-trans : ∀ {a₁ a₂ a₃ : A} → a₁ ≼ a₂ → a₂ ≼ a₃ → a₁ ≼ a₃
|
||
≼-trans {a₁} {a₂} {a₃} a₁≼a₂ a₂≼a₃ =
|
||
begin
|
||
a₁ ⊔ a₃
|
||
∼⟨ ≈-⊔-cong ≈-refl (≈-sym a₂≼a₃) ⟩
|
||
a₁ ⊔ (a₂ ⊔ a₃)
|
||
∼⟨ ≈-sym (⊔-assoc _ _ _) ⟩
|
||
(a₁ ⊔ a₂) ⊔ a₃
|
||
∼⟨ ≈-⊔-cong a₁≼a₂ ≈-refl ⟩
|
||
a₂ ⊔ a₃
|
||
∼⟨ a₂≼a₃ ⟩
|
||
a₃
|
||
∎
|
||
|
||
≼-cong : ∀ {a₁ a₂ a₃ a₄ : A} → a₁ ≈ a₂ → a₃ ≈ a₄ → a₁ ≼ a₃ → a₂ ≼ a₄
|
||
≼-cong {a₁} {a₂} {a₃} {a₄} a₁≈a₂ a₃≈a₄ a₁⊔a₃≈a₃ =
|
||
begin
|
||
a₂ ⊔ a₄
|
||
∼⟨ ≈-⊔-cong (≈-sym a₁≈a₂) (≈-sym a₃≈a₄) ⟩
|
||
a₁ ⊔ a₃
|
||
∼⟨ a₁⊔a₃≈a₃ ⟩
|
||
a₃
|
||
∼⟨ a₃≈a₄ ⟩
|
||
a₄
|
||
∎
|
||
|
||
≺-cong : ∀ {a₁ a₂ a₃ a₄ : A} → a₁ ≈ a₂ → a₃ ≈ a₄ → a₁ ≺ a₃ → a₂ ≺ a₄
|
||
≺-cong a₁≈a₂ a₃≈a₄ (a₁≼a₃ , a₁̷≈a₃) =
|
||
( ≼-cong a₁≈a₂ a₃≈a₄ a₁≼a₃
|
||
, λ a₂≈a₄ → a₁̷≈a₃ (≈-trans a₁≈a₂ (≈-trans a₂≈a₄ (≈-sym a₃≈a₄)))
|
||
)
|
||
|
||
module _ {a} {A : Set a}
|
||
{_≈_ : A → A → Set a} {_⊔_ : A → A → A}
|
||
(lA : IsSemilattice A _≈_ _⊔_) where
|
||
|
||
open IsSemilattice lA using (_≼_)
|
||
|
||
id-Mono : Monotonic _≼_ _≼_ (λ x → x)
|
||
id-Mono {a₁} {a₂} a₁≼a₂ = a₁≼a₂
|
||
|
||
module _ {a b} {A : Set a} {B : Set b}
|
||
{_≈₁_ : A → A → Set a} {_⊔₁_ : A → A → A}
|
||
{_≈₂_ : B → B → Set b} {_⊔₂_ : B → B → B}
|
||
(lA : IsSemilattice A _≈₁_ _⊔₁_) (lB : IsSemilattice B _≈₂_ _⊔₂_) where
|
||
|
||
open IsSemilattice lA using () renaming (_≼_ to _≼₁_)
|
||
open IsSemilattice lB using () renaming (_≼_ to _≼₂_; ⊔-idemp to ⊔₂-idemp; ≼-trans to ≼₂-trans)
|
||
|
||
const-Mono : ∀ (x : B) → Monotonic _≼₁_ _≼₂_ (λ _ → x)
|
||
const-Mono x _ = ⊔₂-idemp x
|
||
|
||
open import Data.List as List using (List; foldr; foldl; _∷_)
|
||
open import Utils using (Pairwise; _∷_)
|
||
|
||
foldr-Mono : ∀ (l₁ l₂ : List A) (f : A → B → B) (b₁ b₂ : B) →
|
||
Pairwise _≼₁_ l₁ l₂ → b₁ ≼₂ b₂ →
|
||
(∀ b → Monotonic _≼₁_ _≼₂_ (λ a → f a b)) →
|
||
(∀ a → Monotonic _≼₂_ _≼₂_ (f a)) →
|
||
foldr f b₁ l₁ ≼₂ foldr f b₂ l₂
|
||
foldr-Mono List.[] List.[] f b₁ b₂ _ b₁≼b₂ _ _ = b₁≼b₂
|
||
foldr-Mono (x ∷ xs) (y ∷ ys) f b₁ b₂ (x≼y ∷ xs≼ys) b₁≼b₂ f-Mono₁ f-Mono₂ =
|
||
≼₂-trans (f-Mono₁ (foldr f b₁ xs) x≼y)
|
||
(f-Mono₂ y (foldr-Mono xs ys f b₁ b₂ xs≼ys b₁≼b₂ f-Mono₁ f-Mono₂))
|
||
|
||
foldl-Mono : ∀ (l₁ l₂ : List A) (f : B → A → B) (b₁ b₂ : B) →
|
||
Pairwise _≼₁_ l₁ l₂ → b₁ ≼₂ b₂ →
|
||
(∀ a → Monotonic _≼₂_ _≼₂_ (λ b → f b a)) →
|
||
(∀ b → Monotonic _≼₁_ _≼₂_ (f b)) →
|
||
foldl f b₁ l₁ ≼₂ foldl f b₂ l₂
|
||
foldl-Mono List.[] List.[] f b₁ b₂ _ b₁≼b₂ _ _ = b₁≼b₂
|
||
foldl-Mono (x ∷ xs) (y ∷ ys) f b₁ b₂ (x≼y ∷ xs≼ys) b₁≼b₂ f-Mono₁ f-Mono₂ =
|
||
foldl-Mono xs ys f (f b₁ x) (f b₂ y) xs≼ys (≼₂-trans (f-Mono₁ x b₁≼b₂) (f-Mono₂ b₂ x≼y)) f-Mono₁ f-Mono₂
|
||
|
||
module _ {a b} {A : Set a} {B : Set b}
|
||
{_≈₂_ : B → B → Set b} {_⊔₂_ : B → B → B}
|
||
(lB : IsSemilattice B _≈₂_ _⊔₂_) where
|
||
|
||
open IsSemilattice lB using () renaming (_≼_ to _≼₂_; ⊔-idemp to ⊔₂-idemp; ≼-trans to ≼₂-trans)
|
||
|
||
open import Data.List as List using (List; foldr; foldl; _∷_)
|
||
open import Utils using (Pairwise; _∷_)
|
||
|
||
foldr-Mono' : ∀ (l : List A) (f : A → B → B) →
|
||
(∀ a → Monotonic _≼₂_ _≼₂_ (f a)) →
|
||
Monotonic _≼₂_ _≼₂_ (λ b → foldr f b l)
|
||
foldr-Mono' List.[] f _ b₁≼b₂ = b₁≼b₂
|
||
foldr-Mono' (x ∷ xs) f f-Mono₂ b₁≼b₂ = f-Mono₂ x (foldr-Mono' xs f f-Mono₂ b₁≼b₂)
|
||
|
||
foldl-Mono' : ∀ (l : List A) (f : B → A → B) →
|
||
(∀ b → Monotonic _≼₂_ _≼₂_ (λ a → f a b)) →
|
||
Monotonic _≼₂_ _≼₂_ (λ b → foldl f b l)
|
||
foldl-Mono' List.[] f _ b₁≼b₂ = b₁≼b₂
|
||
foldl-Mono' (x ∷ xs) f f-Mono₁ b₁≼b₂ = foldl-Mono' xs f f-Mono₁ (f-Mono₁ x b₁≼b₂)
|
||
|
||
record IsLattice {a} (A : Set a)
|
||
(_≈_ : A → A → Set a)
|
||
(_⊔_ : A → A → A)
|
||
(_⊓_ : A → A → A) : Set a where
|
||
|
||
field
|
||
joinSemilattice : IsSemilattice A _≈_ _⊔_
|
||
meetSemilattice : IsSemilattice A _≈_ _⊓_
|
||
|
||
absorb-⊔-⊓ : (x y : A) → (x ⊔ (x ⊓ y)) ≈ x
|
||
absorb-⊓-⊔ : (x y : A) → (x ⊓ (x ⊔ y)) ≈ x
|
||
|
||
open IsSemilattice joinSemilattice public
|
||
open IsSemilattice meetSemilattice public using () renaming
|
||
( ⊔-assoc to ⊓-assoc
|
||
; ⊔-comm to ⊓-comm
|
||
; ⊔-idemp to ⊓-idemp
|
||
; ⊔-Monotonicˡ to ⊓-Monotonicˡ
|
||
; ⊔-Monotonicʳ to ⊓-Monotonicʳ
|
||
; ≈-⊔-cong to ≈-⊓-cong
|
||
; _≼_ to _≽_
|
||
; _≺_ to _≻_
|
||
; ≼-refl to ≽-refl
|
||
; ≼-trans to ≽-trans
|
||
)
|
||
|
||
FixedHeight : ∀ (h : ℕ) → Set a
|
||
FixedHeight h = Chain.Height (_≈_) ≈-equiv _≺_ ≺-cong h
|
||
|
||
record IsFiniteHeightLattice {a} (A : Set a)
|
||
(h : ℕ)
|
||
(_≈_ : A → A → Set a)
|
||
(_⊔_ : A → A → A)
|
||
(_⊓_ : A → A → A) : Set (lsuc a) where
|
||
|
||
field
|
||
isLattice : IsLattice A _≈_ _⊔_ _⊓_
|
||
|
||
open IsLattice isLattice public
|
||
|
||
field
|
||
fixedHeight : FixedHeight h
|
||
|
||
module ChainMapping {a b} {A : Set a} {B : Set b}
|
||
{_≈₁_ : A → A → Set a} {_≈₂_ : B → B → Set b}
|
||
{_⊔₁_ : A → A → A} {_⊔₂_ : B → B → B}
|
||
(slA : IsSemilattice A _≈₁_ _⊔₁_) (slB : IsSemilattice B _≈₂_ _⊔₂_) where
|
||
|
||
open IsSemilattice slA renaming (_≼_ to _≼₁_; _≺_ to _≺₁_; ≈-equiv to ≈₁-equiv; ≺-cong to ≺₁-cong)
|
||
open IsSemilattice slB renaming (_≼_ to _≼₂_; _≺_ to _≺₂_; ≈-equiv to ≈₂-equiv; ≺-cong to ≺₂-cong)
|
||
|
||
open Chain _≈₁_ ≈₁-equiv _≺₁_ ≺₁-cong using () renaming (Chain to Chain₁; step to step₁; done to done₁)
|
||
open Chain _≈₂_ ≈₂-equiv _≺₂_ ≺₂-cong using () renaming (Chain to Chain₂; step to step₂; done to done₂)
|
||
|
||
Chain-map : ∀ (f : A → B) →
|
||
Monotonic _≼₁_ _≼₂_ f →
|
||
Injective _≈₁_ _≈₂_ f →
|
||
f Preserves _≈₁_ ⟶ _≈₂_ →
|
||
∀ {a₁ a₂ : A} {n : ℕ} → Chain₁ a₁ a₂ n → Chain₂ (f a₁) (f a₂) n
|
||
Chain-map f Monotonicᶠ Injectiveᶠ Preservesᶠ (done₁ a₁≈a₂) =
|
||
done₂ (Preservesᶠ a₁≈a₂)
|
||
Chain-map f Monotonicᶠ Injectiveᶠ Preservesᶠ (step₁ (a₁≼₁a , a₁̷≈₁a) a≈₁a' a'a₂) =
|
||
let fa₁≺₂fa = (Monotonicᶠ a₁≼₁a , λ fa₁≈₂fa → a₁̷≈₁a (Injectiveᶠ fa₁≈₂fa))
|
||
fa≈fa' = Preservesᶠ a≈₁a'
|
||
in step₂ fa₁≺₂fa fa≈fa' (Chain-map f Monotonicᶠ Injectiveᶠ Preservesᶠ a'a₂)
|
||
|
||
record Semilattice {a} (A : Set a) : Set (lsuc a) where
|
||
field
|
||
_≈_ : A → A → Set a
|
||
_⊔_ : A → A → A
|
||
|
||
isSemilattice : IsSemilattice A _≈_ _⊔_
|
||
|
||
open IsSemilattice isSemilattice public
|
||
|
||
|
||
record Lattice {a} (A : Set a) : Set (lsuc a) where
|
||
field
|
||
_≈_ : A → A → Set a
|
||
_⊔_ : A → A → A
|
||
_⊓_ : A → A → A
|
||
|
||
isLattice : IsLattice A _≈_ _⊔_ _⊓_
|
||
|
||
open IsLattice isLattice public
|
||
|
||
record FiniteHeightLattice {a} (A : Set a) : Set (lsuc a) where
|
||
field
|
||
height : ℕ
|
||
_≈_ : A → A → Set a
|
||
_⊔_ : A → A → A
|
||
_⊓_ : A → A → A
|
||
|
||
isFiniteHeightLattice : IsFiniteHeightLattice A height _≈_ _⊔_ _⊓_
|
||
|
||
open IsFiniteHeightLattice isFiniteHeightLattice public
|