agda-spa/Lattice.agda

307 lines
12 KiB
Agda
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

module Lattice where
import Data.Nat.Properties as NatProps
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym)
open import Relation.Binary.Definitions
open import Data.Nat as Nat using (; _≤_)
open import Data.Product using (_×_; _,_)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Agda.Primitive using (lsuc; Level)
open import NatMap using (NatMap)
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 IsSemilattice {a} (A : Set a)
(_≈_ : A A Set a)
(_⊔_ : A A A) : Set a where
field
≈-equiv : IsEquivalence A _≈_
⊔-assoc : (x y z : A) ((x y) z) (x (y z))
⊔-comm : (x y : A) (x y) (y x)
⊔-idemp : (x : A) (x x) x
open IsEquivalence ≈-equiv public
record IsLattice {a} (A : Set a)
(_≈_ : A A Set a)
(_⊔_ : A A A)
(_⊓_ : A A A) : Set a where
field
joinSemilattice : IsSemilattice A _≈_ _⊔_
meetSemilattice : IsSemilattice A _≈_ _⊓_
absorb-⊔-⊓ : (x y : A) (x (x y)) x
absorb-⊓-⊔ : (x y : A) (x (x y)) x
open IsSemilattice joinSemilattice public
open IsSemilattice meetSemilattice public renaming
( ⊔-assoc to ⊓-assoc
; ⊔-comm to ⊓-comm
; ⊔-idemp to ⊓-idemp
)
record Semilattice {a} (A : Set a) : Set (lsuc a) where
field
_≈_ : A A Set a
_⊔_ : A A A
isSemilattice : IsSemilattice A _≈_ _⊔_
open IsSemilattice isSemilattice public
record Lattice {a} (A : Set a) : Set (lsuc a) where
field
_≈_ : A A Set a
_⊔_ : A A A
_⊓_ : A A A
isLattice : IsLattice A _≈_ _⊔_ _⊓_
open IsLattice isLattice public
module IsEquivalenceInstances where
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; insert)
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
)
private
_≈_ : Map Map Set (Agda.Primitive._⊔_ a b)
_≈_ = lift _≈₂_
_⊆_ : Map Map Set (Agda.Primitive._⊔_ a b)
_⊆_ = subset _≈₂_
⊆-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₃))
≈-refl : {m : Map} m m
≈-refl {m} = (⊆-refl , ⊆-refl)
≈-sym : {m₁ m₂ : Map} m₁ m₂ m₂ m₁
≈-sym (m₁⊆m₂ , m₂⊆m₁) = (m₂⊆m₁ , m₁⊆m₂)
≈-trans : {m₁ m₂ m₃ : Map} m₁ m₂ m₂ m₃ m₁ m₃
≈-trans (m₁⊆m₂ , m₂⊆m₁) (m₂⊆m₃ , m₃⊆m₂) = (⊆-trans m₁⊆m₂ m₂⊆m₃ , ⊆-trans m₃⊆m₂ m₂⊆m₁)
LiftEquivalence : IsEquivalence Map _≈_
LiftEquivalence = record
{ ≈-refl = ≈-refl
; ≈-sym = ≈-sym
; ≈-trans = ≈-trans
}
module IsSemilatticeInstances where
module ForNat where
open Nat
open NatProps
open Eq
NatIsMaxSemilattice : IsSemilattice _≡_ _⊔_
NatIsMaxSemilattice = record
{ ≈-equiv = record
{ ≈-refl = refl
; ≈-sym = sym
; ≈-trans = trans
}
; ⊔-assoc = ⊔-assoc
; ⊔-comm = ⊔-comm
; ⊔-idemp = ⊔-idem
}
NatIsMinSemilattice : IsSemilattice _≡_ _⊓_
NatIsMinSemilattice = record
{ ≈-equiv = record
{ ≈-refl = refl
; ≈-sym = sym
; ≈-trans = trans
}
; ⊔-assoc = ⊓-assoc
; ⊔-comm = ⊓-comm
; ⊔-idemp = ⊓-idem
}
module ForProd {a} {A B : Set a}
(_≈₁_ : A A Set a) (_≈₂_ : B B Set a)
(_⊔₁_ : A A A) (_⊔₂_ : B B B)
(sA : IsSemilattice A _≈₁_ _⊔₁_) (sB : IsSemilattice B _≈₂_ _⊔₂_) where
open Eq
open Data.Product
private
infix 4 _≈_
infixl 20 _⊔_
_≈_ : A × B A × B Set a
(a₁ , b₁) (a₂ , b₂) = (a₁ ≈₁ a₂) × (b₁ ≈₂ b₂)
_⊔_ : A × B A × B A × B
(a₁ , b₁) (a₂ , b₂) = (a₁ ⊔₁ a₂ , b₁ ⊔₂ b₂)
⊔-assoc : (p₁ p₂ p₃ : A × B) (p₁ p₂) p₃ p₁ (p₂ p₃)
⊔-assoc (a₁ , b₁) (a₂ , b₂) (a₃ , b₃) =
( IsSemilattice.⊔-assoc sA a₁ a₂ a₃
, IsSemilattice.⊔-assoc sB b₁ b₂ b₃
)
⊔-comm : (p₁ p₂ : A × B) p₁ p₂ p₂ p₁
⊔-comm (a₁ , b₁) (a₂ , b₂) =
( IsSemilattice.⊔-comm sA a₁ a₂
, IsSemilattice.⊔-comm sB b₁ b₂
)
⊔-idemp : (p : A × B) p p p
⊔-idemp (a , b) =
( IsSemilattice.⊔-idemp sA a
, IsSemilattice.⊔-idemp sB b
)
≈-refl : {p : A × B} p p
≈-refl =
( IsSemilattice.≈-refl sA
, IsSemilattice.≈-refl sB
)
≈-sym : {p₁ p₂ : A × B} p₁ p₂ p₂ p₁
≈-sym (a₁≈a₂ , b₁≈b₂) =
( IsSemilattice.≈-sym sA a₁≈a₂
, IsSemilattice.≈-sym sB b₁≈b₂
)
≈-trans : {p₁ p₂ p₃ : A × B} p₁ p₂ p₂ p₃ p₁ p₃
≈-trans (a₁≈a₂ , b₁≈b₂) (a₂≈a₃ , b₂≈b₃) =
( IsSemilattice.≈-trans sA a₁≈a₂ a₂≈a₃
, IsSemilattice.≈-trans sB b₁≈b₂ b₂≈b₃
)
ProdIsSemilattice : IsSemilattice (A × B) _≈_ _⊔_
ProdIsSemilattice = record
{ ≈-equiv = record
{ ≈-refl = ≈-refl
; ≈-sym = ≈-sym
; ≈-trans = ≈-trans
}
; ⊔-assoc = ⊔-assoc
; ⊔-comm = ⊔-comm
; ⊔-idemp = ⊔-idemp
}
module IsLatticeInstances where
module ForNat where
open Nat
open NatProps
open Eq
open IsSemilatticeInstances.ForNat
open Data.Product
private
max-bound₁ : {x y z : } x y z x z
max-bound₁ {x} {y} {z} x⊔y≡z
rewrite sym x⊔y≡z
rewrite ⊔-comm x y = m≤n⇒m≤o⊔n y (≤-refl)
min-bound₁ : {x y z : } x y z z x
min-bound₁ {x} {y} {z} x⊓y≡z
rewrite sym x⊓y≡z = m≤n⇒m⊓o≤n y (≤-refl)
minmax-absorb : {x y : } x (x y) x
minmax-absorb {x} {y} = ≤-antisym x⊓x⊔y≤x (helper x⊓x≤x⊓x⊔y (⊓-idem x))
where
x⊓x⊔y≤x = min-bound₁ {x} {x y} {x (x y)} refl
x⊓x≤x⊓x⊔y = ⊓-mono-≤ {x} {x} ≤-refl (max-bound₁ {x} {y} {x y} refl)
-- >:(
helper : x x x (x y) x x x x x (x y)
helper x⊓x≤x⊓x⊔y x⊓x≡x rewrite x⊓x≡x = x⊓x≤x⊓x⊔y
maxmin-absorb : {x y : } x (x y) x
maxmin-absorb {x} {y} = ≤-antisym (helper x⊔x⊓y≤x⊔x (⊔-idem x)) x≤x⊔x⊓y
where
x≤x⊔x⊓y = max-bound₁ {x} {x y} {x (x y)} refl
x⊔x⊓y≤x⊔x = ⊔-mono-≤ {x} {x} ≤-refl (min-bound₁ {x} {y} {x y} refl)
-- >:(
helper : x (x y) x x x x x x (x y) x
helper x⊔x⊓y≤x⊔x x⊔x≡x rewrite x⊔x≡x = x⊔x⊓y≤x⊔x
NatIsLattice : IsLattice _≡_ _⊔_ _⊓_
NatIsLattice = record
{ joinSemilattice = NatIsMaxSemilattice
; meetSemilattice = NatIsMinSemilattice
; absorb-⊔-⊓ = λ x y maxmin-absorb {x} {y}
; absorb-⊓-⊔ = λ x y minmax-absorb {x} {y}
}
module ForProd {a} {A B : Set a}
(_≈₁_ : A A Set a) (_≈₂_ : B B Set a)
(_⊔₁_ : A A A) (_⊓₁_ : A A A)
(_⊔₂_ : B B B) (_⊓₂_ : B B B)
(lA : IsLattice A _≈₁_ _⊔₁_ _⊓₁_) (lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where
private
module ProdJoin = IsSemilatticeInstances.ForProd _≈₁_ _≈₂_ _⊔₁_ _⊔₂_ (IsLattice.joinSemilattice lA) (IsLattice.joinSemilattice lB)
module ProdMeet = IsSemilatticeInstances.ForProd _≈₁_ _≈₂_ _⊓₁_ _⊓₂_ (IsLattice.meetSemilattice lA) (IsLattice.meetSemilattice lB)
infix 4 _≈_
infixl 20 _⊔_
_≈_ : (A × B) (A × B) Set a
(a₁ , b₁) (a₂ , b₂) = (a₁ ≈₁ a₂) × (b₁ ≈₂ b₂)
_⊔_ : (A × B) (A × B) (A × B)
(a₁ , b₁) (a₂ , b₂) = (a₁ ⊔₁ a₂ , b₁ ⊔₂ b₂)
_⊓_ : (A × B) (A × B) (A × B)
(a₁ , b₁) (a₂ , b₂) = (a₁ ⊓₁ a₂ , b₁ ⊓₂ b₂)
open Eq
open Data.Product
private
absorb-⊔-⊓ : (p₁ p₂ : A × B) p₁ (p₁ p₂) p₁
absorb-⊔-⊓ (a₁ , b₁) (a₂ , b₂) =
( IsLattice.absorb-⊔-⊓ lA a₁ a₂
, IsLattice.absorb-⊔-⊓ lB b₁ b₂
)
absorb-⊓-⊔ : (p₁ p₂ : A × B) p₁ (p₁ p₂) p₁
absorb-⊓-⊔ (a₁ , b₁) (a₂ , b₂) =
( IsLattice.absorb-⊓-⊔ lA a₁ a₂
, IsLattice.absorb-⊓-⊔ lB b₁ b₂
)
ProdIsLattice : IsLattice (A × B) _≈_ _⊔_ _⊓_
ProdIsLattice = record
{ joinSemilattice = ProdJoin.ProdIsSemilattice
; meetSemilattice = ProdMeet.ProdIsSemilattice
; absorb-⊔-⊓ = absorb-⊔-⊓
; absorb-⊓-⊔ = absorb-⊓-⊔
}