DanilaFe/agda-spa
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Add congruence instances for < and <= on semilattices

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2023-09-03 19:33:04 -07:00
parent c9ec50c0ca
commit 67e96b27cf
1 changed files with 15 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

20
Lattice.agda
View File

@ -1,7 +1,7 @@
module Lattice where module Lattice where
open import Chain using (Chain; Height; done; step; concat)
open import Equivalence open import Equivalence
open import Chain
import Data.Nat.Properties as NatProps import Data.Nat.Properties as NatProps
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym) open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym)
@ -35,10 +35,19 @@ record IsSemilattice {a} (A : Set a)
⊔-comm : (x y : A) → (x ⊔ y) ≈ (y ⊔ x) ⊔-comm : (x y : A) → (x ⊔ y) ≈ (y ⊔ x)
⊔-idemp : (x : A) → (x ⊔ x) ≈ x ⊔-idemp : (x : A) → (x ⊔ x) ≈ x
open IsEquivalence ≈-equiv public
≼-refl : ∀ (a : A) → a ≼ a ≼-refl : ∀ (a : A) → a ≼ a
≼-refl a = (a , ⊔-idemp a) ≼-refl a = (a , ⊔-idemp a)
open IsEquivalence ≈-equiv public ≼-cong : ∀ {a₁ a₂ a₃ a₄ : A} → a₁ ≈ a₂ → a₃ ≈ a₄ → a₁ ≼ a₃ → a₂ ≼ a₄
≼-cong a₁≈a₂ a₃≈a₄ (c₁ , a₁⊔c₁≈a₃) = (c₁ , ≈-trans (≈-⊔-cong (≈-sym a₁≈a₂) ≈-refl) (≈-trans a₁⊔c₁≈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₄)))
)
record IsLattice {a} (A : Set a) record IsLattice {a} (A : Set a)
(_≈_ : A → A → Set a) (_≈_ : A → A → Set a)
@ -71,10 +80,11 @@ record IsFiniteHeightLattice {a} (A : Set a)
field field
isLattice : IsLattice A _≈_ _⊔_ _⊓_ isLattice : IsLattice A _≈_ _⊔_ _⊓_
fixedHeight : Height (IsLattice._≺_ isLattice) h fixedHeight : Chain.Height (IsLattice._≺_ isLattice) h
open IsLattice isLattice public open IsLattice isLattice public
module _ {a b} {A : Set a} {B : Set b} module _ {a b} {A : Set a} {B : Set b}
(_≼₁_ : A → A → Set a) (_≼₂_ : B → B → Set b) where (_≼₁_ : A → A → Set a) (_≼₂_ : B → B → Set b) where
@ -86,8 +96,8 @@ module ChainMapping {a b} {A : Set a} {B : Set b}
{_⊔₁_ : A → A → A} {_⊔₂_ : B → B → B} {_⊔₁_ : A → A → A} {_⊔₂_ : B → B → B}
(slA : IsSemilattice A _≈₁_ _⊔₁_) (slB : IsSemilattice B _≈₂_ _⊔₂_) where (slA : IsSemilattice A _≈₁_ _⊔₁_) (slB : IsSemilattice B _≈₂_ _⊔₂_) where
open IsSemilattice slA renaming (_≼_ to _≼₁_; _≺_ to _≺₁_) open IsSemilattice slA renaming (_≼_ to _≼₁_; _≺_ to _≺₁_; ≈-equiv to ≈₁-equiv)
open IsSemilattice slB renaming (_≼_ to _≼₂_; _≺_ to _≺₂_) open IsSemilattice slB renaming (_≼_ to _≼₂_; _≺_ to _≺₂_; ≈-equiv to ≈₂-equiv)
Chain-map : ∀ (f : A → B) → Monotonic _≼₁_ _≼₂_ f → Injective _≈₁_ _≈₂_ f → Chain-map : ∀ (f : A → B) → Monotonic _≼₁_ _≼₂_ f → Injective _≈₁_ _≈₂_ f →
∀ {a₁ a₂ : A} {n : ℕ} → Chain _≺₁_ a₁ a₂ n → Chain _≺₂_ (f a₁) (f a₂) n ∀ {a₁ a₂ : A} {n : ℕ} → Chain _≺₁_ a₁ a₂ n → Chain _≺₂_ (f a₁) (f a₂) n