Extract the equivalence code into its own module
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
parent
b6292bf9bd
commit
29fb828ee2
78
Equivalence.agda
Normal file
78
Equivalence.agda
Normal file
|
|
@ -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₁
|
||||||
|
)
|
||||||
|
}
|
||||||
77
Lattice.agda
77
Lattice.agda
|
|
@ -1,5 +1,8 @@
|
||||||
module Lattice where
|
module Lattice where
|
||||||
|
|
||||||
|
open import Chain using (Chain; Height; done; step; concat)
|
||||||
|
open import Equivalence
|
||||||
|
|
||||||
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)
|
||||||
open import Relation.Binary.Definitions
|
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.Product using (_×_; Σ; _,_; proj₁; proj₂)
|
||||||
open import Data.Sum using (_⊎_; inj₁; inj₂)
|
open import Data.Sum using (_⊎_; inj₁; inj₂)
|
||||||
open import Agda.Primitive using (lsuc; Level) renaming (_⊔_ to _⊔ℓ_)
|
open import Agda.Primitive using (lsuc; Level) renaming (_⊔_ to _⊔ℓ_)
|
||||||
open import Chain using (Chain; Height; done; step; concat)
|
|
||||||
open import Function.Definitions using (Injective)
|
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
|
record IsDecidable {a} (A : Set a) (R : A → A → Set a) : Set a where
|
||||||
field
|
field
|
||||||
R-dec : ∀ (a₁ a₂ : A) → Dec (R a₁ a₂)
|
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
|
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 IsSemilatticeInstances where
|
||||||
module ForNat where
|
module ForNat where
|
||||||
open Nat
|
open Nat
|
||||||
|
|
|
||||||
Loading…
Reference in New Issue
Block a user