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

Add a congruence requirement on Lattice.

Browse Source
This commit is contained in:
Danila Fedorin 2023-09-03 17:08:37 -07:00
parent eee814ae3c
commit c9ec50c0ca
1 changed files with 18 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

19
Lattice.agda
View File

@ -29,6 +29,7 @@ record IsSemilattice {a} (A : Set a)
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)
@ -56,6 +57,7 @@ record IsLattice {a} (A : Set a)
( ⊔-assoc to ⊓-assoc
; ⊔-comm to ⊓-comm
; ⊔-idemp to ⊓-idemp
; ≈-⊔-cong to ≈-⊓-cong
; _≼_ to _≽_
; _≺_ to _≻_
; ≼-refl to ≽-refl
@ -120,6 +122,13 @@ module IsSemilatticeInstances where
open NatProps
open Eq
private
≡-⊔-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₄} → a₁ ≡ a₂ → a₃ ≡ a₄ → (a₁ ⊓ a₃) ≡ (a₂ ⊓ a₄)
≡-⊓-cong a₁≡a₂ a₃≡a₄ rewrite a₁≡a₂ rewrite a₃≡a₄ = refl
NatIsMaxSemilattice : IsSemilattice ℕ _≡_ _⊔_
NatIsMaxSemilattice = record
{ ≈-equiv = record
@ -127,6 +136,7 @@ module IsSemilatticeInstances where
; ≈-sym = sym
; ≈-trans = trans
}
; ≈-⊔-cong = ≡-⊔-cong
; ⊔-assoc = ⊔-assoc
; ⊔-comm = ⊔-comm
; ⊔-idemp = ⊔-idem
@ -139,6 +149,7 @@ module IsSemilatticeInstances where
; ≈-sym = sym
; ≈-trans = trans
}
; ≈-⊔-cong = ≡-⊓-cong
; ⊔-assoc = ⊓-assoc
; ⊔-comm = ⊓-comm
; ⊔-idemp = ⊓-idem
@ -163,6 +174,10 @@ module IsSemilatticeInstances where
ProdIsSemilattice : IsSemilattice (A × B) _≈_ _⊔_
ProdIsSemilattice = record
{ ≈-equiv = ProdEquiv.ProdEquivalence
; ≈-⊔-cong = λ (a₁≈a₂ , b₁≈b₂) (a₃≈a₄ , b₃≈b₄) →
( IsSemilattice.≈-⊔-cong sA a₁≈a₂ a₃≈a₄
, IsSemilattice.≈-⊔-cong sB b₁≈b₂ b₃≈b₄
)
; ⊔-assoc = λ (a₁ , b₁) (a₂ , b₂) (a₃ , b₃) →
( IsSemilattice.⊔-assoc sA a₁ a₂ a₃
, IsSemilattice.⊔-assoc sB b₁ b₂ b₃
@ -185,7 +200,7 @@ module IsSemilatticeInstances where
open import Map A B ≡-dec-A
open IsSemilattice sB renaming
( ≈-refl to ≈₂-refl; ≈-sym to ≈₂-sym
( ≈-refl to ≈₂-refl; ≈-sym to ≈₂-sym; ≈-⊔-cong to ≈₂-⊔₂-cong
; ⊔-assoc to ⊔₂-assoc; ⊔-comm to ⊔₂-comm; ⊔-idemp to ⊔₂-idemp
)
@ -204,6 +219,7 @@ module IsSemilatticeInstances where
MapIsUnionSemilattice : IsSemilattice Map _≈_ _⊔_
MapIsUnionSemilattice = record
{ ≈-equiv = MapEquiv.LiftEquivalence
; ≈-⊔-cong = λ {m₁} {m₂} {m₃} {m₄} → union-cong _≈₂_ _⊔₂_ ≈₂-⊔₂-cong {m₁} {m₂} {m₃} {m₄}
; ⊔-assoc = union-assoc _≈₂_ ≈₂-refl ≈₂-sym _⊔₂_ ⊔₂-assoc
; ⊔-comm = union-comm _≈₂_ ≈₂-refl ≈₂-sym _⊔₂_ ⊔₂-comm
; ⊔-idemp = union-idemp _≈₂_ ≈₂-refl ≈₂-sym _⊔₂_ ⊔₂-idemp
@ -212,6 +228,7 @@ module IsSemilatticeInstances where
MapIsIntersectSemilattice : IsSemilattice Map _≈_ _⊓_
MapIsIntersectSemilattice = record
{ ≈-equiv = MapEquiv.LiftEquivalence
; ≈-⊔-cong = λ {m₁} {m₂} {m₃} {m₄} → intersect-cong _≈₂_ _⊔₂_ ≈₂-⊔₂-cong {m₁} {m₂} {m₃} {m₄}
; ⊔-assoc = intersect-assoc _≈₂_ ≈₂-refl ≈₂-sym _⊔₂_ ⊔₂-assoc
; ⊔-comm = intersect-comm _≈₂_ ≈₂-refl ≈₂-sym _⊔₂_ ⊔₂-comm
; ⊔-idemp = intersect-idemp _≈₂_ ≈₂-refl ≈₂-sym _⊔₂_ ⊔₂-idemp