Danila Fedorin f84a1c923c Prove that the 'join' transformation is monotonic
`Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>`
2024-03-09 23:06:47 -08:00

#### 249 lines 10 KiB Agda Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

 ```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; _∷_) ``` ``` 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₂)) ``` ``` ``` ```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 ```