aboutsummaryrefslogtreecommitdiff
path: root/Data/Hypergraph
diff options
context:
space:
mode:
Diffstat (limited to 'Data/Hypergraph')
-rw-r--r--Data/Hypergraph/Base.agda179
1 files changed, 171 insertions, 8 deletions
diff --git a/Data/Hypergraph/Base.agda b/Data/Hypergraph/Base.agda
index a2157fb..f54468d 100644
--- a/Data/Hypergraph/Base.agda
+++ b/Data/Hypergraph/Base.agda
@@ -3,29 +3,57 @@
module Data.Hypergraph.Base where
open import Data.Castable using (IsCastable)
-open import Data.Nat.Base using (ℕ)
open import Data.Fin using (Fin)
+open import Relation.Binary
+ using
+ ( Rel
+ ; IsDecTotalOrder
+ ; IsStrictTotalOrder
+ ; Tri
+ ; Trichotomous
+ ; _Respectsˡ_
+ ; _Respectsʳ_
+ ; _Respects_
+ )
+open import Relation.Binary.Bundles using (DecTotalOrder; StrictTotalOrder)
+open import Relation.Nullary using (¬_)
+open import Data.Nat.Base using (ℕ; _<_)
+open import Data.Product.Base using (_×_; _,_; proj₁; proj₂)
+open import Data.Nat.Properties using (<-irrefl; <-trans; <-resp₂-≡; <-cmp)
+open import Level using (Level; suc; _⊔_)
+
import Data.Vec.Base as VecBase
import Data.Vec.Relation.Binary.Equality.Cast as VecCast
import Relation.Binary.PropositionalEquality as ≡
-
-open import Relation.Binary using (Rel; IsDecTotalOrder)
-open import Data.Nat.Base using (ℕ)
-open import Level using (Level; suc; _⊔_)
+import Relation.Binary.Properties.DecTotalOrder as DTOP
record HypergraphLabel {ℓ : Level} : Set (suc ℓ) where
field
Label : ℕ → Set ℓ
isCastable : IsCastable Label
- _[_≈_] : (n : ℕ) → Rel (Label n) ℓ
+ -- _[_≈_] : (n : ℕ) → Rel (Label n) ℓ
_[_≤_] : (n : ℕ) → Rel (Label n) ℓ
- decTotalOrder : (n : ℕ) → IsDecTotalOrder (n [_≈_]) (n [_≤_])
+ isDecTotalOrder : (n : ℕ) → IsDecTotalOrder ≡._≡_ (n [_≤_])
+ decTotalOrder : (n : ℕ) → DecTotalOrder ℓ ℓ ℓ
+ decTotalOrder n = record
+ { Carrier = Label n
+ ; _≈_ = ≡._≡_
+ ; _≤_ = n [_≤_]
+ ; isDecTotalOrder = isDecTotalOrder n
+ }
+
+ open DTOP using (<-strictTotalOrder) renaming (_<_ to <)
+ _[_<_] : (n : ℕ) → Rel (Label n) ℓ
+ _[_<_] n = < (decTotalOrder n)
+ strictTotalOrder : (n : ℕ) → StrictTotalOrder ℓ ℓ ℓ
+ strictTotalOrder n = <-strictTotalOrder (decTotalOrder n)
open IsCastable isCastable public
module Edge (HL : HypergraphLabel) where
- open HypergraphLabel HL using (Label; cast)
+ module HL = HypergraphLabel HL
+ open HL using (Label; cast; cast-is-id; cast-trans)
open VecBase using (Vec)
record Edge (v : ℕ) : Set where
@@ -38,6 +66,7 @@ module Edge (HL : HypergraphLabel) where
open VecCast using (_≈[_]_)
record ≈-Edge {n : ℕ} (E E′ : Edge n) : Set where
+ eta-equality
module E = Edge E
module E′ = Edge E′
field
@@ -45,6 +74,140 @@ module Edge (HL : HypergraphLabel) where
≡label : cast ≡arity E.label ≡ E′.label
≡ports : E.ports ≈[ ≡arity ] E′.ports
+ ≈-Edge-refl : {v : ℕ} {x : Edge v} → ≈-Edge x x
+ ≈-Edge-refl {_} {x} = record
+ { ≡arity = ≡.refl
+ ; ≡label = HL.≈-reflexive ≡.refl
+ ; ≡ports = VecCast.≈-reflexive ≡.refl
+ }
+ where
+ open Edge x using (arity; label)
+ open DecTotalOrder (HL.decTotalOrder arity) using (module Eq)
+
+ ≈-Edge-sym : {v : ℕ} {x y : Edge v} → ≈-Edge x y → ≈-Edge y x
+ ≈-Edge-sym {_} {x} {y} x≈y = record
+ { ≡arity = ≡.sym ≡arity
+ ; ≡label = HL.≈-sym ≡label
+ ; ≡ports = VecCast.≈-sym ≡ports
+ }
+ where
+ open ≈-Edge x≈y
+ open DecTotalOrder (HL.decTotalOrder E.arity) using (module Eq)
+
+ ≈-Edge-trans : {v : ℕ} {i j k : Edge v} → ≈-Edge i j → ≈-Edge j k → ≈-Edge i k
+ ≈-Edge-trans {_} {i} {j} {k} i≈j j≈k = record
+ { ≡arity = ≡.trans i≈j.≡arity j≈k.≡arity
+ ; ≡label = HL.≈-trans i≈j.≡label j≈k.≡label
+ ; ≡ports = VecCast.≈-trans i≈j.≡ports j≈k.≡ports
+ }
+ where
+ module i≈j = ≈-Edge i≈j
+ module j≈k = ≈-Edge j≈k
+
+ open HL using (_[_<_])
+ data <-Edge {v : ℕ} : Edge v → Edge v → Set where
+ <-arity
+ : {x y : Edge v}
+ → Edge.arity x < Edge.arity y
+ → <-Edge x y
+ <-label
+ : {x y : Edge v}
+ (≡a : Edge.arity x ≡ Edge.arity y)
+ → Edge.arity y [ cast ≡a (Edge.label x) < Edge.label y ]
+ → <-Edge x y
+
+ <-Edge-irrefl : {v : ℕ} {x y : Edge v} → ≈-Edge x y → ¬ <-Edge x y
+ <-Edge-irrefl record { ≡arity = ≡a } (<-arity n<m) = <-irrefl ≡a n<m
+ <-Edge-irrefl record { ≡label = ≡l } (<-label _ (_ , x≉y)) = x≉y ≡l
+
+ <-Edge-trans : {v : ℕ} {i j k : Edge v} → <-Edge i j → <-Edge j k → <-Edge i k
+ <-Edge-trans (<-arity i<j) (<-arity j<k) = <-arity (<-trans i<j j<k)
+ <-Edge-trans (<-arity i<j) (<-label ≡.refl j<k) = <-arity i<j
+ <-Edge-trans (<-label ≡.refl i<j) (<-arity j<k) = <-arity j<k
+ <-Edge-trans {_} {i} (<-label ≡.refl i<j) (<-label ≡.refl j<k)
+ = <-label ≡.refl (<-label-trans i<j (<-respˡ-≈ (HL.≈-reflexive ≡.refl) j<k))
+ where
+ open DTOP (HL.decTotalOrder (Edge.arity i)) using (<-respˡ-≈) renaming (<-trans to <-label-trans)
+
+ <-Edge-respˡ-≈ : {v : ℕ} {y : Edge v} → (λ x → <-Edge x y) Respects ≈-Edge
+ <-Edge-respˡ-≈ ≈x (<-arity x₁<y) = <-arity (proj₂ <-resp₂-≡ ≡arity x₁<y)
+ where
+ open ≈-Edge ≈x using (≡arity)
+ <-Edge-respˡ-≈ {_} {y} record { ≡arity = ≡.refl ; ≡label = ≡.refl } (<-label ≡.refl x₁<y)
+ = <-label ≡.refl (<-respˡ-≈ (≡.sym (HL.≈-reflexive ≡.refl)) x₁<y)
+ where
+ module y = Edge y
+ open DTOP (HL.decTotalOrder y.arity) using (<-respˡ-≈)
+ <-Edge-respʳ-≈ : {v : ℕ} {x : Edge v} → <-Edge x Respects ≈-Edge
+ <-Edge-respʳ-≈ record { ≡arity = ≡a } (<-arity x<y₁) = <-arity (proj₁ <-resp₂-≡ ≡a x<y₁)
+ <-Edge-respʳ-≈ {_} {x} record { ≡arity = ≡.refl ; ≡label = ≡.refl } (<-label ≡.refl x<y₁)
+ = <-label ≡.refl (<-respʳ-≈ (≡.sym (HL.≈-reflexive ≡.refl)) x<y₁)
+ where
+ module x = Edge x
+ open DTOP (HL.decTotalOrder x.arity) using (<-respʳ-≈)
+
+ open Tri
+ open ≈-Edge
+ tri : {v : ℕ} → Trichotomous (≈-Edge {v}) (<-Edge {v})
+ tri x y with <-cmp x.arity y.arity
+ where
+ module x = Edge x
+ module y = Edge y
+ tri x y | tri< x<y x≢y y≮x = tri< (<-arity x<y) (λ x≡y → x≢y (≡arity x≡y)) ¬y<x
+ where
+ ¬y<x : ¬ <-Edge y x
+ ¬y<x (<-arity y<x) = y≮x y<x
+ ¬y<x (<-label ≡a y<x) = x≢y (≡.sym ≡a)
+ tri x y | tri≈ x≮y ≡.refl y≮x = compare-label
+ where
+ module x = Edge x
+ module y = Edge y
+ open StrictTotalOrder (HL.strictTotalOrder x.arity) using (compare)
+ import Relation.Binary.Properties.DecTotalOrder
+ open DTOP (HL.decTotalOrder x.arity) using (<-respˡ-≈)
+ compare-label : Tri (<-Edge x y) (≈-Edge x y) (<-Edge y x)
+ compare-label with compare x.label y.label
+ ... | tri< x<y x≢y y≮x′ = tri<
+ (<-label ≡.refl (<-respˡ-≈ (≡.sym (HL.≈-reflexive ≡.refl)) x<y))
+ (λ x≡y → x≢y (≡.trans (≡.sym (HL.≈-reflexive ≡.refl)) (≡label x≡y)))
+ ¬y<x
+ where
+ ¬y<x : ¬ <-Edge y x
+ ¬y<x (<-arity y<x) = y≮x y<x
+ ¬y<x (<-label ≡a y<x) = y≮x′ (<-respˡ-≈ (HL.≈-reflexive ≡.refl) y<x)
+ ... | tri≈ x≮y x≡y y≮x = compare-ports
+ where
+ compare-ports : Tri (<-Edge x y) (≈-Edge x y) (<-Edge y x)
+ compare-ports = ?
+ ... | tri> x≮y′ x≢y y<x = tri>
+ ¬x<y
+ (λ x≡y → x≢y (≡.trans (≡.sym (HL.≈-reflexive ≡.refl)) (≡label x≡y)))
+ (<-label ≡.refl (<-respˡ-≈ (≡.sym (HL.≈-reflexive ≡.refl)) y<x))
+ where
+ ¬x<y : ¬ <-Edge x y
+ ¬x<y (<-arity x<y) = x≮y x<y
+ ¬x<y (<-label ≡a x<y) = x≮y′ (<-respˡ-≈ (HL.≈-reflexive ≡.refl) x<y)
+ tri x y | tri> x≮y x≢y y<x = tri> ¬x<y (λ x≡y → x≢y (≡arity x≡y)) (<-arity y<x)
+ where
+ ¬x<y : ¬ <-Edge x y
+ ¬x<y (<-arity x<y) = x≮y x<y
+ ¬x<y (<-label ≡a x<y) = x≢y ≡a
+
+ isStrictTotalOrder : {v : ℕ} → IsStrictTotalOrder (≈-Edge {v}) (<-Edge {v})
+ isStrictTotalOrder = record
+ { isStrictPartialOrder = record
+ { isEquivalence = record
+ { refl = ≈-Edge-refl
+ ; sym = ≈-Edge-sym
+ ; trans = ≈-Edge-trans
+ }
+ ; irrefl = <-Edge-irrefl
+ ; trans = <-Edge-trans
+ ; <-resp-≈ = <-Edge-respʳ-≈ , <-Edge-respˡ-≈
+ }
+ ; compare = tri
+ }
+
module HypergraphList (HL : HypergraphLabel) where
open import Data.List.Base using (List)