diff --git a/Equivalence.agda b/Equivalence.agda new file mode 100644 index 0000000..327b9bd --- /dev/null +++ b/Equivalence.agda @@ -0,0 +1,78 @@ +module Equivalence where + +open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂) +open import Relation.Binary.Definitions +open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym) + +record IsEquivalence {a} (A : Set a) (_≈_ : A → A → Set a) : Set a where + field + ≈-refl : {a : A} → a ≈ a + ≈-sym : {a b : A} → a ≈ b → b ≈ a + ≈-trans : {a b c : A} → a ≈ b → b ≈ c → a ≈ c + +module IsEquivalenceInstances where + module ForProd {a} {A B : Set a} + (_≈₁_ : A → A → Set a) (_≈₂_ : B → B → Set a) + (eA : IsEquivalence A _≈₁_) (eB : IsEquivalence B _≈₂_) where + + infix 4 _≈_ + + _≈_ : A × B → A × B → Set a + (a₁ , b₁) ≈ (a₂ , b₂) = (a₁ ≈₁ a₂) × (b₁ ≈₂ b₂) + + ProdEquivalence : IsEquivalence (A × B) _≈_ + ProdEquivalence = record + { ≈-refl = λ {p} → + ( IsEquivalence.≈-refl eA + , IsEquivalence.≈-refl eB + ) + ; ≈-sym = λ {p₁} {p₂} (a₁≈a₂ , b₁≈b₂) → + ( IsEquivalence.≈-sym eA a₁≈a₂ + , IsEquivalence.≈-sym eB b₁≈b₂ + ) + ; ≈-trans = λ {p₁} {p₂} {p₃} (a₁≈a₂ , b₁≈b₂) (a₂≈a₃ , b₂≈b₃) → + ( IsEquivalence.≈-trans eA a₁≈a₂ a₂≈a₃ + , IsEquivalence.≈-trans eB b₁≈b₂ b₂≈b₃ + ) + } + + module ForMap {a b} (A : Set a) (B : Set b) + (≡-dec-A : Decidable (_≡_ {a} {A})) + (_≈₂_ : B → B → Set b) + (eB : IsEquivalence B _≈₂_) where + + open import Map A B ≡-dec-A using (Map; lift; subset) + open import Data.List using (_∷_; []) -- TODO: re-export these with nicer names from map + + open IsEquivalence eB renaming + ( ≈-refl to ≈₂-refl + ; ≈-sym to ≈₂-sym + ; ≈-trans to ≈₂-trans + ) + + _≈_ : Map → Map → Set (Agda.Primitive._⊔_ a b) + _≈_ = lift _≈₂_ + + _⊆_ : Map → Map → Set (Agda.Primitive._⊔_ a b) + _⊆_ = subset _≈₂_ + + private + ⊆-refl : (m : Map) → m ⊆ m + ⊆-refl _ k v k,v∈m = (v , (≈₂-refl , k,v∈m)) + + ⊆-trans : (m₁ m₂ m₃ : Map) → m₁ ⊆ m₂ → m₂ ⊆ m₃ → m₁ ⊆ m₃ + ⊆-trans _ _ _ m₁⊆m₂ m₂⊆m₃ k v k,v∈m₁ = + let + (v' , (v≈v' , k,v'∈m₂)) = m₁⊆m₂ k v k,v∈m₁ + (v'' , (v'≈v'' , k,v''∈m₃)) = m₂⊆m₃ k v' k,v'∈m₂ + in (v'' , (≈₂-trans v≈v' v'≈v'' , k,v''∈m₃)) + + LiftEquivalence : IsEquivalence Map _≈_ + LiftEquivalence = record + { ≈-refl = λ {m} → (⊆-refl m , ⊆-refl m) + ; ≈-sym = λ {m₁} {m₂} (m₁⊆m₂ , m₂⊆m₁) → (m₂⊆m₁ , m₁⊆m₂) + ; ≈-trans = λ {m₁} {m₂} {m₃} (m₁⊆m₂ , m₂⊆m₁) (m₂⊆m₃ , m₃⊆m₂) → + ( ⊆-trans m₁ m₂ m₃ m₁⊆m₂ m₂⊆m₃ + , ⊆-trans m₃ m₂ m₁ m₃⊆m₂ m₂⊆m₁ + ) + } diff --git a/Lattice.agda b/Lattice.agda index 229caed..d50664b 100644 --- a/Lattice.agda +++ b/Lattice.agda @@ -1,5 +1,8 @@ module Lattice where +open import Chain using (Chain; Height; done; step; concat) +open import Equivalence + import Data.Nat.Properties as NatProps open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym) open import Relation.Binary.Definitions @@ -8,15 +11,8 @@ open import Data.Nat as Nat using (ℕ; _≤_; _+_) open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂) open import Data.Sum using (_⊎_; inj₁; inj₂) open import Agda.Primitive using (lsuc; Level) renaming (_⊔_ to _⊔ℓ_) -open import Chain using (Chain; Height; done; step; concat) open import Function.Definitions using (Injective) -record IsEquivalence {a} (A : Set a) (_≈_ : A → A → Set a) : Set a where - field - ≈-refl : {a : A} → a ≈ a - ≈-sym : {a b : A} → a ≈ b → b ≈ a - ≈-trans : {a b c : A} → a ≈ b → b ≈ c → a ≈ c - record IsDecidable {a} (A : Set a) (R : A → A → Set a) : Set a where field R-dec : ∀ (a₁ a₂ : A) → Dec (R a₁ a₂) @@ -118,73 +114,6 @@ record Lattice {a} (A : Set a) : Set (lsuc a) where open IsLattice isLattice public -module IsEquivalenceInstances where - module ForProd {a} {A B : Set a} - (_≈₁_ : A → A → Set a) (_≈₂_ : B → B → Set a) - (eA : IsEquivalence A _≈₁_) (eB : IsEquivalence B _≈₂_) where - - infix 4 _≈_ - - _≈_ : A × B → A × B → Set a - (a₁ , b₁) ≈ (a₂ , b₂) = (a₁ ≈₁ a₂) × (b₁ ≈₂ b₂) - - ProdEquivalence : IsEquivalence (A × B) _≈_ - ProdEquivalence = record - { ≈-refl = λ {p} → - ( IsEquivalence.≈-refl eA - , IsEquivalence.≈-refl eB - ) - ; ≈-sym = λ {p₁} {p₂} (a₁≈a₂ , b₁≈b₂) → - ( IsEquivalence.≈-sym eA a₁≈a₂ - , IsEquivalence.≈-sym eB b₁≈b₂ - ) - ; ≈-trans = λ {p₁} {p₂} {p₃} (a₁≈a₂ , b₁≈b₂) (a₂≈a₃ , b₂≈b₃) → - ( IsEquivalence.≈-trans eA a₁≈a₂ a₂≈a₃ - , IsEquivalence.≈-trans eB b₁≈b₂ b₂≈b₃ - ) - } - - module ForMap {a b} (A : Set a) (B : Set b) - (≡-dec-A : Decidable (_≡_ {a} {A})) - (_≈₂_ : B → B → Set b) - (eB : IsEquivalence B _≈₂_) where - - open import Map A B ≡-dec-A using (Map; lift; subset) - open import Data.List using (_∷_; []) -- TODO: re-export these with nicer names from map - - open IsEquivalence eB renaming - ( ≈-refl to ≈₂-refl - ; ≈-sym to ≈₂-sym - ; ≈-trans to ≈₂-trans - ) - - _≈_ : Map → Map → Set (Agda.Primitive._⊔_ a b) - _≈_ = lift _≈₂_ - - _⊆_ : Map → Map → Set (Agda.Primitive._⊔_ a b) - _⊆_ = subset _≈₂_ - - private - ⊆-refl : (m : Map) → m ⊆ m - ⊆-refl _ k v k,v∈m = (v , (≈₂-refl , k,v∈m)) - - ⊆-trans : (m₁ m₂ m₃ : Map) → m₁ ⊆ m₂ → m₂ ⊆ m₃ → m₁ ⊆ m₃ - ⊆-trans _ _ _ m₁⊆m₂ m₂⊆m₃ k v k,v∈m₁ = - let - (v' , (v≈v' , k,v'∈m₂)) = m₁⊆m₂ k v k,v∈m₁ - (v'' , (v'≈v'' , k,v''∈m₃)) = m₂⊆m₃ k v' k,v'∈m₂ - in (v'' , (≈₂-trans v≈v' v'≈v'' , k,v''∈m₃)) - - LiftEquivalence : IsEquivalence Map _≈_ - LiftEquivalence = record - { ≈-refl = λ {m} → (⊆-refl m , ⊆-refl m) - ; ≈-sym = λ {m₁} {m₂} (m₁⊆m₂ , m₂⊆m₁) → (m₂⊆m₁ , m₁⊆m₂) - ; ≈-trans = λ {m₁} {m₂} {m₃} (m₁⊆m₂ , m₂⊆m₁) (m₂⊆m₃ , m₃⊆m₂) → - ( ⊆-trans m₁ m₂ m₃ m₁⊆m₂ m₂⊆m₃ - , ⊆-trans m₃ m₂ m₁ m₃⊆m₂ m₂⊆m₁ - ) - } - module IsSemilatticeInstances where module ForNat where open Nat