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

Make 'IsDecidable' into a record to aid instance search

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin
2025-01-04 18:58:56 -08:00
parent 8abf6f8670
commit b0488c9cc6
14 changed files with 146 additions and 115 deletions
Download Patch File Download Diff File Expand all files Collapse all files

10
Lattice/AboveBelow.agda
View File

@@ -5,13 +5,14 @@ open import Relation.Nullary using (Dec; ¬_; yes; no)
module Lattice.AboveBelow {a} (A : Set a)
(_≈₁_ : A → A → Set a)
(≈₁-equiv : IsEquivalence A _≈₁_)
(≈₁-dec : IsDecidable _≈₁_) where
(≈₁-Decidable : IsDecidable _≈₁_) where
open import Data.Empty using (⊥-elim)
open import Data.Product using (_,_)
open import Data.Nat using (_≤_; ℕ; z≤n; s≤s; suc)
open import Function using (_∘_)
open import Showable using (Showable; show)
open import Relation.Binary.Definitions using (Decidable)
open import Relation.Binary.PropositionalEquality as Eq
using (_≡_; sym; subst; refl)
@@ -20,6 +21,8 @@ import Chain
open IsEquivalence ≈₁-equiv using ()
renaming (≈-refl to ≈₁-refl; ≈-sym to ≈₁-sym; ≈-trans to ≈₁-trans)
open IsDecidable ≈₁-Decidable using () renaming (R-dec to ≈₁-dec)
data AboveBelow : Set a where
⊥ : AboveBelow
⊤ : AboveBelow
@@ -62,7 +65,7 @@ data _≈_ : AboveBelow → AboveBelow → Set a where
; ≈-trans = ≈-trans
}
≈-dec : IsDecidable _≈_
≈-dec : Decidable _≈_
≈-dec ⊥ ⊥ = yes ≈-⊥-⊥
≈-dec ⊤ ⊤ = yes ≈-⊤-⊤
≈-dec [ x ] [ y ]
@@ -76,6 +79,9 @@ data _≈_ : AboveBelow → AboveBelow → Set a where
≈-dec [ x ] ⊥ = no λ ()
≈-dec [ x ] ⊤ = no λ ()
≈-Decidable : IsDecidable _≈_
≈-Decidable = record { R-dec = ≈-dec }
-- Any object can be wrapped in an 'above below' to make it a lattice,
-- since ⊤ and ⊥ are the largest and least elements, and the rest are left
-- unordered. That's what this module does.

18
Lattice/FiniteMap.agda
View File

@@ -39,7 +39,7 @@ open import Lattice.Map ≡-dec-A lB as Map
; ⊓-idemp to ⊓ᵐ-idemp
; absorb-⊔-⊓ to absorb-⊔ᵐ-⊓ᵐ
; absorb-⊓-⊔ to absorb-⊓ᵐ-⊔ᵐ
; ≈-dec to ≈ᵐ-dec
; ≈-Decidable to ≈ᵐ-Decidable
; _[_] to _[_]ᵐ
; []-∈ to []ᵐ-∈
; m₁≼m₂⇒m₁[k]≼m₂[k] to m₁≼m₂⇒m₁[k]ᵐ≼m₂[k]ᵐ
@@ -67,7 +67,6 @@ open import Data.Nat using (ℕ)
open import Data.Product using (_×_; _,_; Σ; proj₁; proj₂)
open import Equivalence
open import Function using (_∘_)
open import Relation.Binary.Definitions using (Decidable)
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Utils using (Pairwise; _∷_; []; Unique; push; empty; All¬-¬Any)
open import Showable using (Showable; show)
@@ -86,8 +85,11 @@ module WithKeys (ks : List A) where
_≈_ : FiniteMap → FiniteMap → Set
_≈_ (m₁ , _) (m₂ , _) = m₁ ≈ᵐ m₂
≈₂-dec⇒≈-dec : IsDecidable _≈₂_ → IsDecidable _≈_
≈₂-dec⇒≈-dec ≈₂-dec fm₁ fm₂ = ≈ᵐ-dec ≈₂-dec (proj₁ fm₁) (proj₁ fm₂)
≈₂-Decidable⇒≈-Decidable : IsDecidable _≈₂_ → IsDecidable _≈_
≈₂-Decidable⇒≈-Decidable ≈₂-Decidable = record
{ R-dec = λ fm₁ fm₂ → IsDecidable.R-dec (≈ᵐ-Decidable ≈₂-Decidable)
(proj₁ fm₁) (proj₁ fm₂)
}
_⊔_ : FiniteMap → FiniteMap → FiniteMap
_⊔_ (m₁ , km₁≡ks) (m₂ , km₂≡ks) =
@@ -257,7 +259,7 @@ module IterProdIsomorphism where
( _≈_ to _≈ᵘ_
; _⊔_ to _⊔ᵘ_
; _⊓_ to _⊓ᵘ_
; ≈-dec to ≈ᵘ-dec
; ≈-Decidable to ≈ᵘ-Decidable
; isLattice to isLatticeᵘ
; ≈-equiv to ≈ᵘ-equiv
; fixedHeight to fixedHeightᵘ
@@ -608,10 +610,10 @@ module IterProdIsomorphism where
in
(v' , (v₁⊔v₂≈v' , there v'∈fm'))
module WithUniqueKeysAndFixedHeight {ks : List A} (uks : Unique ks) (≈₂-dec : Decidable _≈₂_) (h₂ : ℕ) (fhB : FixedHeight₂ h₂) where
module WithUniqueKeysAndFixedHeight {ks : List A} (uks : Unique ks) (≈₂-Decidable : IsDecidable _≈₂_) (h₂ : ℕ) (fhB : FixedHeight₂ h₂) where
import Isomorphism
open Isomorphism.TransportFiniteHeight
(IP.isFiniteHeightLattice (length ks) ≈₂-dec ≈ᵘ-dec h₂ 0 fhB fixedHeightᵘ) (isLattice ks)
(IP.isFiniteHeightLattice (length ks) ≈₂-Decidable ≈ᵘ-Decidable h₂ 0 fhB fixedHeightᵘ) (isLattice ks)
{f = to uks} {g = from {ks}}
(to-preserves-≈ uks) (from-preserves-≈ {ks})
(to-⊔-distr uks) (from-⊔-distr {ks})
@@ -624,5 +626,5 @@ module IterProdIsomorphism where
⊥-contains-bottoms : ∀ {k : A} {v : B} → (k , v) ∈ᵐ ⊥ → v ≡ (Height.⊥ fhB)
⊥-contains-bottoms {k} {v} k,v∈⊥
rewrite IP.⊥-built (length ks) ≈₂-dec ≈ᵘ-dec h₂ 0 fhB fixedHeightᵘ =
rewrite IP.⊥-built (length ks) ≈₂-Decidable ≈ᵘ-Decidable h₂ 0 fhB fixedHeightᵘ =
to-build uks k v k,v∈⊥

18
Lattice/IterProd.agda
View File

@@ -39,8 +39,8 @@ build a b (suc s) = (a , build a b s)
private
record RequiredForFixedHeight : Set (lsuc a) where
field
≈₁-dec : IsDecidable _≈₁_
≈₂-dec : IsDecidable _≈₂_
≈₁-Decidable : IsDecidable _≈₁_
≈₂-Decidable : IsDecidable _≈₂_
h₁ h₂ : ℕ
fhA : FixedHeight₁ h₁
fhB : FixedHeight₂ h₂
@@ -58,7 +58,7 @@ private
field
height : ℕ
fixedHeight : IsLattice.FixedHeight isLattice height
≈-dec : IsDecidable _≈_
≈-Decidable : IsDecidable _≈_
⊥-correct : Height.⊥ fixedHeight ≡ ⊥
@@ -84,7 +84,7 @@ private
; isFiniteHeightIfSupported = λ req → record
{ height = RequiredForFixedHeight.h₂ req
; fixedHeight = RequiredForFixedHeight.fhB req
; ≈-dec = RequiredForFixedHeight.≈₂-dec req
; ≈-Decidable = RequiredForFixedHeight.≈₂-Decidable req
; ⊥-correct = refl
}
}
@@ -101,10 +101,10 @@ private
{ height = (RequiredForFixedHeight.h₁ req) + IsFiniteHeightWithBotAndDecEq.height fhlRest
; fixedHeight =
P.fixedHeight
(RequiredForFixedHeight.≈₁-dec req) (IsFiniteHeightWithBotAndDecEq.≈-dec fhlRest)
(RequiredForFixedHeight.≈₁-Decidable req) (IsFiniteHeightWithBotAndDecEq.≈-Decidable fhlRest)
(RequiredForFixedHeight.h₁ req) (IsFiniteHeightWithBotAndDecEq.height fhlRest)
(RequiredForFixedHeight.fhA req) (IsFiniteHeightWithBotAndDecEq.fixedHeight fhlRest)
; ≈-dec = P.≈-dec (RequiredForFixedHeight.≈₁-dec req) (IsFiniteHeightWithBotAndDecEq.≈-dec fhlRest)
; ≈-Decidable = P.≈-Decidable (RequiredForFixedHeight.≈₁-Decidable req) (IsFiniteHeightWithBotAndDecEq.≈-Decidable fhlRest)
; ⊥-correct =
cong ((Height.⊥ (RequiredForFixedHeight.fhA req)) ,_)
(IsFiniteHeightWithBotAndDecEq.⊥-correct fhlRest)
@@ -131,15 +131,15 @@ module _ (k : ℕ) where
; isLattice = isLattice
}
module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
module _ (≈₁-Decidable : IsDecidable _≈₁_) (≈₂-Decidable : IsDecidable _≈₂_)
(h₁ h₂ : ℕ)
(fhA : FixedHeight₁ h₁) (fhB : FixedHeight₂ h₂) where
private
required : RequiredForFixedHeight
required = record
{ ≈₁-dec = ≈₁-dec
; ≈₂-dec = ≈₂-dec
{ ≈₁-Decidable = ≈₁-Decidable
; ≈₂-Decidable = ≈₂-Decidable
; h₁ = h₁
; h₂ = h₂
; fhA = fhA

11
Lattice/Map.agda
View File

@@ -1,12 +1,11 @@
open import Lattice
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym; trans; cong; subst)
open import Relation.Binary.Definitions using (Decidable)
open import Agda.Primitive using (Level) renaming (_⊔_ to _⊔ℓ_)
module Lattice.Map {a b : Level} {A : Set a} {B : Set b}
{_≈₂_ : B → B → Set b}
{_⊔₂_ : B → B → B} {_⊓₂_ : B → B → B}
(≡-dec-A : Decidable (_≡_ {a} {A}))
(≡-Decidable-A : IsDecidable {a} {A} _≡_)
(lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where
open import Data.List.Membership.Propositional as MemProp using () renaming (_∈_ to _∈ˡ_)
@@ -23,6 +22,8 @@ open import Utils using (Unique; push; Unique-append; All¬-¬Any; All-x∈xs)
open import Data.String using () renaming (_++_ to _++ˢ_)
open import Showable using (Showable; show)
open IsDecidable ≡-Decidable-A using () renaming (R-dec to ≡-dec-A)
open IsLattice lB using () renaming
( ≈-refl to ≈₂-refl; ≈-sym to ≈₂-sym; ≈-trans to ≈₂-trans
; ≈-⊔-cong to ≈₂-⊔₂-cong; ≈-⊓-cong to ≈₂-⊓₂-cong
@@ -625,7 +626,8 @@ Expr-Provenance-≡ {k} {v} e k,v∈e
with (v' , (p , k,v'∈e)) ← Expr-Provenance k e (forget k,v∈e)
rewrite Map-functional {m = ⟦ e ⟧} k,v∈e k,v'∈e = p
module _ (≈₂-dec : IsDecidable _≈₂_) where
module _ (≈₂-Decidable : IsDecidable _≈₂_) where
open IsDecidable ≈₂-Decidable using () renaming (R-dec to ≈₂-dec)
private module _ where
data SubsetInfo (m₁ m₂ : Map) : Set (a ⊔ℓ b) where
extra : (k : A) → k ∈k m₁ → ¬ k ∈k m₂ → SubsetInfo m₁ m₂
@@ -676,6 +678,9 @@ module _ (≈₂-dec : IsDecidable _≈₂_) where
... | _ | no m₂̷⊆m₁ = no (λ (_ , m₂⊆m₁) → m₂̷⊆m₁ m₂⊆m₁)
... | no m₁̷⊆m₂ | _ = no (λ (m₁⊆m₂ , _) → m₁̷⊆m₂ m₁⊆m₂)
≈-Decidable : IsDecidable _≈_
≈-Decidable = record { R-dec = ≈-dec }
private module I⊔ = ImplInsert _⊔₂_
private module I⊓ = ImplInsert _⊓₂_

5
Lattice/MapSet.agda
View File

@@ -1,9 +1,8 @@
open import Lattice
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym; trans; cong; subst)
open import Relation.Binary.Definitions using (Decidable)
open import Agda.Primitive using (Level) renaming (_⊔_ to _⊔ℓ_)
module Lattice.MapSet {a : Level} {A : Set a} (≡-dec-A : Decidable (_≡_ {a} {A})) where
module Lattice.MapSet {a : Level} {A : Set a} (≡-Decidable-A : IsDecidable (_≡_ {a} {A})) where
open import Data.List using (List; map)
open import Data.Product using (_,_; proj₁)
@@ -12,7 +11,7 @@ open import Function using (_∘_)
open import Lattice.Unit using (⊤; tt) renaming (_≈_ to _≈₂_; _⊔_ to _⊔₂_; _⊓_ to _⊓₂_; isLattice to ⊤-isLattice)
import Lattice.Map
private module UnitMap = Lattice.Map ≡-dec-A ⊤-isLattice
private module UnitMap = Lattice.Map ≡-Decidable-A ⊤-isLattice
open UnitMap
using (Map; Expr; ⟦_⟧)
renaming

133
Lattice/Prod.agda
View File

@@ -12,6 +12,7 @@ open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂)
open import Data.Empty using (⊥-elim)
open import Relation.Binary.Core using (_Preserves_⟶_ )
open import Relation.Binary.PropositionalEquality using (sym; subst)
open import Relation.Binary.Definitions using (Decidable)
open import Relation.Nullary using (¬_; yes; no)
open import Equivalence
import Chain
@@ -103,88 +104,92 @@ lattice = record
; isLattice = isLattice
}
module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_) where
≈-dec : IsDecidable _≈_
module _ (≈₁-Decidable : IsDecidable _≈₁_) (≈₂-Decidable : IsDecidable _≈₂_) where
open IsDecidable ≈₁-Decidable using () renaming (R-dec to ≈₁-dec)
open IsDecidable ≈₂-Decidable using () renaming (R-dec to ≈₂-dec)
≈-dec : Decidable _≈_
≈-dec (a₁ , b₁) (a₂ , b₂)
with ≈₁-dec a₁ a₂ | ≈₂-dec b₁ b₂
... | yes a₁≈a₂ | yes b₁≈b₂ = yes (a₁≈a₂ , b₁≈b₂)
... | no a₁̷≈a₂ | _ = no (λ (a₁≈a₂ , _) → a₁̷≈a₂ a₁≈a₂)
... | _ | no b₁̷≈b₂ = no (λ (_ , b₁≈b₂) → b₁̷≈b₂ b₁≈b₂)
≈-Decidable : IsDecidable _≈_
≈-Decidable = record { R-dec = ≈-dec }
module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
(h₁ h₂ : ℕ)
(fhA : FixedHeight₁ h₁) (fhB : FixedHeight₂ h₂) where
module _ (h₁ h₂ : ℕ)
(fhA : FixedHeight₁ h₁) (fhB : FixedHeight₂ h₂) where
open import Data.Nat.Properties
open IsLattice isLattice using (_≼_; _≺_; ≺-cong)
open import Data.Nat.Properties
open IsLattice isLattice using (_≼_; _≺_; ≺-cong)
module ChainMapping₁ = ChainMapping joinSemilattice₁ isJoinSemilattice
module ChainMapping₂ = ChainMapping joinSemilattice₂ isJoinSemilattice
module ChainMapping₁ = ChainMapping joinSemilattice₁ isJoinSemilattice
module ChainMapping₂ = ChainMapping joinSemilattice₂ isJoinSemilattice
module ChainA = Chain _≈₁_ ≈₁-equiv _≺₁_ ≺₁-cong
module ChainB = Chain _≈₂_ ≈₂-equiv _≺₂_ ≺₂-cong
module ProdChain = Chain _≈_ ≈-equiv _≺_ ≺-cong
module ChainA = Chain _≈₁_ ≈₁-equiv _≺₁_ ≺₁-cong
module ChainB = Chain _≈₂_ ≈₂-equiv _≺₂_ ≺₂-cong
module ProdChain = Chain _≈_ ≈-equiv _≺_ ≺-cong
open ChainA using () renaming (Chain to Chain₁; done to done₁; step to step₁; Chain-≈-cong₁ to Chain₁-≈-cong₁)
open ChainB using () renaming (Chain to Chain₂; done to done₂; step to step₂; Chain-≈-cong₁ to Chain₂-≈-cong₁)
open ProdChain using (Chain; concat; done; step)
open ChainA using () renaming (Chain to Chain₁; done to done₁; step to step₁; Chain-≈-cong₁ to Chain₁-≈-cong₁)
open ChainB using () renaming (Chain to Chain₂; done to done₂; step to step₂; Chain-≈-cong₁ to Chain₂-≈-cong₁)
open ProdChain using (Chain; concat; done; step)
private
a,∙-Monotonic : ∀ (a : A) → Monotonic _≼₂_ _≼_ (λ b → (a , b))
a,∙-Monotonic a {b₁} {b₂} b₁⊔b₂≈b₂ = (⊔₁-idemp a , b₁⊔b₂≈b₂)
private
a,∙-Monotonic : ∀ (a : A) → Monotonic _≼₂_ _≼_ (λ b → (a , b))
a,∙-Monotonic a {b₁} {b₂} b₁⊔b₂≈b₂ = (⊔₁-idemp a , b₁⊔b₂≈b₂)
a,∙-Preserves-≈₂ : ∀ (a : A) → (λ b → (a , b)) Preserves _≈₂_ ⟶ _≈_
a,∙-Preserves-≈₂ a {b₁} {b₂} b₁≈b₂ = (≈₁-refl , b₁≈b₂)
a,∙-Preserves-≈₂ : ∀ (a : A) → (λ b → (a , b)) Preserves _≈₂_ ⟶ _≈_
a,∙-Preserves-≈₂ a {b₁} {b₂} b₁≈b₂ = (≈₁-refl , b₁≈b₂)
∙,b-Monotonic : ∀ (b : B) → Monotonic _≼₁_ _≼_ (λ a → (a , b))
∙,b-Monotonic b {a₁} {a₂} a₁⊔a₂≈a₂ = (a₁⊔a₂≈a₂ , ⊔₂-idemp b)
∙,b-Monotonic : ∀ (b : B) → Monotonic _≼₁_ _≼_ (λ a → (a , b))
∙,b-Monotonic b {a₁} {a₂} a₁⊔a₂≈a₂ = (a₁⊔a₂≈a₂ , ⊔₂-idemp b)
∙,b-Preserves-≈₁ : ∀ (b : B) → (λ a → (a , b)) Preserves _≈₁_ ⟶ _≈_
∙,b-Preserves-≈₁ b {a₁} {a₂} a₁≈a₂ = (a₁≈a₂ , ≈₂-refl)
∙,b-Preserves-≈₁ : ∀ (b : B) → (λ a → (a , b)) Preserves _≈₁_ ⟶ _≈_
∙,b-Preserves-≈₁ b {a₁} {a₂} a₁≈a₂ = (a₁≈a₂ , ≈₂-refl)
open ChainA.Height fhA using () renaming (⊥ to ⊥₁; ⊤ to ⊤₁; longestChain to longestChain₁; bounded to bounded₁)
open ChainB.Height fhB using () renaming (⊥ to ⊥₂; ⊤ to ⊤₂; longestChain to longestChain₂; bounded to bounded₂)
open ChainA.Height fhA using () renaming (⊥ to ⊥₁; ⊤ to ⊤₁; longestChain to longestChain₁; bounded to bounded₁)
open ChainB.Height fhB using () renaming (⊥ to ⊥₂; ⊤ to ⊤₂; longestChain to longestChain₂; bounded to bounded₂)
unzip : ∀ {a₁ a₂ : A} {b₁ b₂ : B} {n : ℕ} → Chain (a₁ , b₁) (a₂ , b₂) n → Σ (ℕ × ℕ) (λ (n₁ , n₂) → ((Chain₁ a₁ a₂ n₁ × Chain₂ b₁ b₂ n₂) × (n ≤ n₁ + n₂)))
unzip (done (a₁≈a₂ , b₁≈b₂)) = ((0 , 0) , ((done₁ a₁≈a₂ , done₂ b₁≈b₂) , ≤-refl))
unzip {a₁} {a₂} {b₁} {b₂} {n} (step {(a₁ , b₁)} {(a , b)} ((a₁≼a , b₁≼b) , a₁b₁̷≈ab) (a≈a' , b≈b') a'b'a₂b₂)
with ≈₁-dec a₁ a | ≈₂-dec b₁ b | unzip a'b'a₂b₂
... | yes a₁≈a | yes b₁≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) = ⊥-elim (a₁b₁̷≈ab (a₁≈a , b₁≈b))
... | no a₁̷≈a | yes b₁≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) =
((suc n₁ , n₂) , ((step₁ (a₁≼a , a₁̷≈a) a≈a' c₁ , Chain₂-≈-cong₁ (≈₂-sym (≈₂-trans b₁≈b b≈b')) c₂), +-monoʳ-≤ 1 (n≤n₁+n₂)))
... | yes a₁≈a | no b₁̷≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) =
((n₁ , suc n₂) , ( (Chain₁-≈-cong₁ (≈₁-sym (≈₁-trans a₁≈a a≈a')) c₁ , step₂ (b₁≼b , b₁̷≈b) b≈b' c₂)
, subst (n ≤_) (sym (+-suc n₁ n₂)) (+-monoʳ-≤ 1 n≤n₁+n₂)
))
... | no a₁̷≈a | no b₁̷≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) =
((suc n₁ , suc n₂) , ( (step₁ (a₁≼a , a₁̷≈a) a≈a' c₁ , step₂ (b₁≼b , b₁̷≈b) b≈b' c₂)
, m≤n⇒m≤o+n 1 (subst (n ≤_) (sym (+-suc n₁ n₂)) (+-monoʳ-≤ 1 n≤n₁+n₂))
unzip : ∀ {a₁ a₂ : A} {b₁ b₂ : B} {n : ℕ} → Chain (a₁ , b₁) (a₂ , b₂) n → Σ (ℕ × ℕ) (λ (n₁ , n₂) → ((Chain₁ a₁ a₂ n₁ × Chain₂ b₁ b₂ n₂) × (n ≤ n₁ + n₂)))
unzip (done (a₁≈a₂ , b₁≈b₂)) = ((0 , 0) , ((done₁ a₁≈a₂ , done₂ b₁≈b₂) , ≤-refl))
unzip {a₁} {a₂} {b₁} {b₂} {n} (step {(a₁ , b₁)} {(a , b)} ((a₁≼a , b₁≼b) , a₁b₁̷≈ab) (a≈a' , b≈b') a'b'a₂b₂)
with ≈₁-dec a₁ a | ≈₂-dec b₁ b | unzip a'b'a₂b₂
... | yes a₁≈a | yes b₁≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) = ⊥-elim (a₁b₁̷≈ab (a₁≈a , b₁≈b))
... | no a₁̷≈a | yes b₁≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) =
((suc n₁ , n₂) , ((step₁ (a₁≼a , a₁̷≈a) a≈a' c₁ , Chain₂-≈-cong₁ (≈₂-sym (≈₂-trans b₁≈b b≈b')) c₂), +-monoʳ-≤ 1 (n≤n₁+n₂)))
... | yes a₁≈a | no b₁̷≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) =
((n₁ , suc n₂) , ( (Chain₁-≈-cong₁ (≈₁-sym (≈₁-trans a₁≈a a≈a')) c₁ , step₂ (b₁≼b , b₁̷≈b) b≈b' c₂)
, subst (n ≤_) (sym (+-suc n₁ n₂)) (+-monoʳ-≤ 1 n≤n₁+n₂)
))
... | no a₁̷≈a | no b₁̷≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) =
((suc n₁ , suc n₂) , ( (step₁ (a₁≼a , a₁̷≈a) a≈a' c₁ , step₂ (b₁≼b , b₁̷≈b) b≈b' c₂)
, m≤n⇒m≤o+n 1 (subst (n ≤_) (sym (+-suc n₁ n₂)) (+-monoʳ-≤ 1 n≤n₁+n₂))
))
fixedHeight : IsLattice.FixedHeight isLattice (h₁ + h₂)
fixedHeight = record
{ ⊥ = (⊥₁ , ⊥₂)
; ⊤ = (⊤₁ , ⊤₂)
; longestChain = concat
(ChainMapping₁.Chain-map (λ a → (a , ⊥₂)) (∙,b-Monotonic _) proj₁ (∙,b-Preserves-≈₁ _) longestChain₁)
(ChainMapping₂.Chain-map (λ b → (⊤₁ , b)) (a,∙-Monotonic _) proj₂ (a,∙-Preserves-≈₂ _) longestChain₂)
; bounded = λ a₁b₁a₂b₂ →
let ((n₁ , n₂) , ((a₁a₂ , b₁b₂) , n≤n₁+n₂)) = unzip a₁b₁a₂b₂
in ≤-trans n≤n₁+n₂ (+-mono-≤ (bounded₁ a₁a₂) (bounded₂ b₁b₂))
}
fixedHeight : IsLattice.FixedHeight isLattice (h₁ + h₂)
fixedHeight = record
{ ⊥ = (⊥₁ , ⊥₂)
; ⊤ = (⊤₁ , ⊤₂)
; longestChain = concat
(ChainMapping₁.Chain-map (λ a → (a , ⊥₂)) (∙,b-Monotonic _) proj₁ (∙,b-Preserves-≈₁ _) longestChain₁)
(ChainMapping₂.Chain-map (λ b → (⊤₁ , b)) (a,∙-Monotonic _) proj₂ (a,∙-Preserves-≈₂ _) longestChain₂)
; bounded = λ a₁b₁a₂b₂ →
let ((n₁ , n₂) , ((a₁a₂ , b₁b₂) , n≤n₁+n₂)) = unzip a₁b₁a₂b₂
in ≤-trans n≤n₁+n₂ (+-mono-≤ (bounded₁ a₁a₂) (bounded₂ b₁b₂))
}
isFiniteHeightLattice : IsFiniteHeightLattice (A × B) (h₁ + h₂) _≈_ _⊔_ _⊓_
isFiniteHeightLattice = record
{ isLattice = isLattice
; fixedHeight = fixedHeight
}
isFiniteHeightLattice : IsFiniteHeightLattice (A × B) (h₁ + h₂) _≈_ _⊔_ _⊓_
isFiniteHeightLattice = record
{ isLattice = isLattice
; fixedHeight = fixedHeight
}
finiteHeightLattice : FiniteHeightLattice (A × B)
finiteHeightLattice = record
{ height = h₁ + h₂
; _≈_ = _≈_
; _⊔_ = _⊔_
; _⊓_ = _⊓_
; isFiniteHeightLattice = isFiniteHeightLattice
}
finiteHeightLattice : FiniteHeightLattice (A × B)
finiteHeightLattice = record
{ height = h₁ + h₂
; _≈_ = _≈_
; _⊔_ = _⊔_
; _⊓_ = _⊓_
; isFiniteHeightLattice = isFiniteHeightLattice
}

6
Lattice/Unit.agda
View File

@@ -7,6 +7,7 @@ open import Data.Unit using (⊤; tt) public
open import Data.Unit.Properties using (_≟_; ≡-setoid)
open import Relation.Binary using (Setoid)
open import Relation.Binary.PropositionalEquality as Eq using (_≡_)
open import Relation.Binary.Definitions using (Decidable)
open import Relation.Nullary using (Dec; ¬_; yes; no)
open import Equivalence
open import Lattice
@@ -24,9 +25,12 @@ _≈_ = _≡_
; ≈-trans = trans
}
≈-dec : IsDecidable _≈_
≈-dec : Decidable _≈_
≈-dec = _≟_
≈-Decidable : IsDecidable _≈_
≈-Decidable = record { R-dec = ≈-dec }
_⊔_ : ⊤ → ⊤ → ⊤
tt ⊔ tt = tt