diff options
Diffstat (limited to 'Data/Hypergraph/Base.agda')
| -rw-r--r-- | Data/Hypergraph/Base.agda | 179 |
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) |