diff options
| -rw-r--r-- | Data/Circuit.agda | 78 | ||||
| -rw-r--r-- | Data/Circuit/Convert.agda | 84 | ||||
| -rw-r--r-- | Data/Hypergraph.agda | 63 | ||||
| -rw-r--r-- | Data/Hypergraph/Base.agda | 25 | ||||
| -rw-r--r-- | Data/Hypergraph/Edge.agda | 368 | ||||
| -rw-r--r-- | Data/Hypergraph/Edge/Order.agda | 280 | ||||
| -rw-r--r-- | Data/Hypergraph/Setoid.agda | 59 | ||||
| -rw-r--r-- | Functor/Instance/Nat/Circ.agda | 2 | ||||
| -rw-r--r-- | Functor/Instance/Nat/Edge.agda | 11 |
9 files changed, 452 insertions, 518 deletions
diff --git a/Data/Circuit.agda b/Data/Circuit.agda index 09dfb2e..46c4e18 100644 --- a/Data/Circuit.agda +++ b/Data/Circuit.agda @@ -1,70 +1,38 @@ {-# OPTIONS --without-K --safe #-} -open import Level using (Level; _⊔_) +open import Level using (Level) module Data.Circuit {c ℓ : Level} where -import Data.List as List - open import Data.Circuit.Gate using (Gates) +import Data.List as List +import Data.Hypergraph {c} {ℓ} Gates as Hypergraph + open import Data.Fin using (Fin) -open import Data.Hypergraph {c} {ℓ} Gates - using - ( Hypergraph - ; Hypergraphₛ - ; mkHypergraphₛ - ; List∘Edgeₛ - ; module Edge - ; mkHypergraph - ; _≈_ - ; mk≈ - ) open import Data.Nat using (ℕ) -open import Relation.Binary using (Setoid) -open import Function.Bundles using (Func; _⟶ₛ_) - -open List using (List) -open Edge using (Edge; ≈-Edge⇒≡) - -Circuit : ℕ → Set c -Circuit = Hypergraph - -map : {n m : ℕ} → (Fin n → Fin m) → Circuit n → Circuit m -map f (mkHypergraph edges) = mkHypergraph (List.map (Edge.map f) edges) - -Circuitₛ : ℕ → Setoid c (c ⊔ ℓ) -Circuitₛ = Hypergraphₛ - -mkCircuitₛ : {n : ℕ} → List∘Edgeₛ n ⟶ₛ Circuitₛ n -mkCircuitₛ = mkHypergraphₛ +open import Function using (Func; _⟶ₛ_) +open import Data.List.Relation.Binary.Permutation.Propositional.Properties using (map⁺) open Func -open Edge.Sort using (sort) +open Hypergraph using (List∘Edgeₛ) +open Hypergraph + using (_≈_ ; mk≈ ; module Edge) + renaming + ( Hypergraph to Circuit + ; Hypergraphₛ to Circuitₛ + ; mkHypergraph to mkCircuit + ; mkHypergraphₛ to mkCircuitₛ + ) + public +open List using ([]) -open import Relation.Binary.PropositionalEquality as ≡ using (_≡_) -open import Data.List.Relation.Binary.Permutation.Propositional using (_↭_; ↭⇒↭ₛ′) -open import Data.List.Relation.Binary.Permutation.Propositional.Properties using (map⁺) -open import Data.List.Relation.Binary.Pointwise as PW using (Pointwise; Pointwise-≡⇒≡) -open import Data.List.Relation.Binary.Permutation.Homogeneous using (Permutation) +map : {n m : ℕ} → (Fin n → Fin m) → Circuit n → Circuit m +map f (mkCircuit edges) = mkCircuit (List.map (Edge.map f) edges) -import Data.Permutation.Sort as ↭-Sort +discrete : (n : ℕ) → Circuit n +discrete n = mkCircuit [] mapₛ : {n m : ℕ} → (Fin n → Fin m) → Circuitₛ n ⟶ₛ Circuitₛ m -mapₛ {n} {m} f .to = map f -mapₛ {n} {m} f .cong {mkHypergraph xs} {mkHypergraph ys} x≈y = mk≈ ≡-norm - where - open _≈_ x≈y using (↭-edges) - open ↭-Sort (Edge.decTotalOrder {m}) using (sorted-≋) - open import Function.Reasoning - xs′ ys′ : List (Edge m) - xs′ = List.map (Edge.map f) xs - ys′ = List.map (Edge.map f) ys - ≡-norm : mkHypergraph (sort xs′) ≡ mkHypergraph (sort ys′) - ≡-norm = ↭-edges ∶ xs ↭ ys - |> map⁺ (Edge.map f) ∶ xs′ ↭ ys′ - |> ↭⇒↭ₛ′ Edge.≈-Edge-IsEquivalence ∶ Permutation Edge.≈-Edge xs′ ys′ - |> sorted-≋ ∶ Pointwise Edge.≈-Edge (sort xs′) (sort ys′) - |> PW.map ≈-Edge⇒≡ ∶ Pointwise _≡_ (sort xs′) (sort ys′) - |> Pointwise-≡⇒≡ ∶ sort xs′ ≡ sort ys′ - |> ≡.cong mkHypergraph ∶ mkHypergraph (sort xs′) ≡ mkHypergraph (sort ys′) +mapₛ f .to = map f +mapₛ f .cong (mk≈ x≈y) = mk≈ (map⁺ (Edge.map f) x≈y) diff --git a/Data/Circuit/Convert.agda b/Data/Circuit/Convert.agda index 8562e92..d5abd35 100644 --- a/Data/Circuit/Convert.agda +++ b/Data/Circuit/Convert.agda @@ -4,50 +4,53 @@ module Data.Circuit.Convert where open import Level using (0ℓ) +import Data.Vec as Vec +import Data.Vec.Relation.Binary.Equality.Cast as VecCast +import Data.List.Relation.Binary.Permutation.Propositional as L +import Data.Vec.Functional.Relation.Binary.Permutation as V +import DecorationFunctor.Hypergraph.Labeled {0ℓ} {0ℓ} as LabeledHypergraph + open import Data.Nat.Base using (ℕ) open import Data.Circuit.Gate using (Gate; Gates; cast-gate; cast-gate-is-id; subst-is-cast-gate) +open import Data.Circuit {0ℓ} {0ℓ} using (Circuit; Circuitₛ; _≈_; mkCircuit; module Edge; mk≈) open import Data.Fin.Base using (Fin) -open import Data.Hypergraph.Edge Gates using (Edge) -open import Data.Hypergraph.Base {0ℓ} Gates using (Hypergraph; normalize; mkHypergraph) -open import Data.Hypergraph.Setoid {0ℓ} {0ℓ} Gates using (Hypergraphₛ; _≈_) +open import Data.Product.Base using (_,_) open import Data.Permutation using (fromList-↭; toList-↭) open import Data.List using (length) open import Data.Vec.Functional using (toVec; fromVec; toList; fromList) open import Function.Bundles using (Equivalence; _↔_) open import Function.Base using (_∘_; id) +open import Data.Vec.Properties using (tabulate-cong; tabulate-∘; map-cast) +open import Data.Fin.Base using () renaming (cast to fincast) +open import Data.Fin.Properties using () renaming (cast-trans to fincast-trans; cast-is-id to fincast-is-id) open import Data.List.Relation.Binary.Permutation.Homogeneous using (Permutation) open import Data.Product.Base using (proj₁; proj₂; _×_) open import Data.Fin.Permutation using (flip; _⟨$⟩ˡ_) open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_) -import Function.Reasoning as →-Reasoning -import Data.List.Relation.Binary.Permutation.Propositional as L -import Data.Vec.Functional.Relation.Binary.Permutation as V -import DecorationFunctor.Hypergraph.Labeled {0ℓ} {0ℓ} as LabeledHypergraph - open LabeledHypergraph using (Hypergraph-same) renaming (Hypergraph to Hypergraph′; Hypergraph-setoid to Hypergraph-Setoid′) -to : {v : ℕ} → Hypergraph v → Hypergraph′ v -to H = record +to : {v : ℕ} → Circuit v → Hypergraph′ v +to C = record { h = length edges ; a = arity ∘ fromList edges ; j = fromVec ∘ ports ∘ fromList edges ; l = label ∘ fromList edges } where - open Edge using (arity; ports; label) - open Hypergraph H + open Edge.Edge using (arity; ports; label) + open Circuit C -from : {v : ℕ} → Hypergraph′ v → Hypergraph v +from : {v : ℕ} → Hypergraph′ v → Circuit v from {v} H = record { edges = toList asEdge } where open Hypergraph′ H - asEdge : Fin h → Edge v + asEdge : Fin h → Edge.Edge v asEdge e = record { label = l e ; ports = toVec (j e) } -to-cong : {v : ℕ} {H H′ : Hypergraph v} → H ≈ H′ → Hypergraph-same (to H) (to H′) +to-cong : {v : ℕ} {H H′ : Circuit v} → H ≈ H′ → Hypergraph-same (to H) (to H′) to-cong {v} {H} {H′} ≈H = record { ↔h = flip ρ ; ≗a = ≗a @@ -55,7 +58,7 @@ to-cong {v} {H} {H′} ≈H = record ; ≗l = ≗l } where - open Edge using (arity; ports; label) + open Edge.Edge using (arity; ports; label) open _≈_ ≈H open import Data.Fin.Permutation using (_⟨$⟩ʳ_; _⟨$⟩ˡ_; Permutation′; inverseʳ) open import Data.Fin.Base using (cast) @@ -92,11 +95,6 @@ to-cong {v} {H} {H′} ≈H = record ≡.refl module _ {v : ℕ} where - open import Data.Hypergraph.Edge Gates using (decTotalOrder; ≈-Edge; ≈-Edge-IsEquivalence; ≈-Edge⇒≡) - open import Data.List.Sort (decTotalOrder {v}) using (sort; sort-↭) - open import Data.Permutation.Sort (decTotalOrder {v}) using (sorted-≋) - open import Data.List.Relation.Binary.Pointwise using (Pointwise; Pointwise-≡⇒≡; map) - open import Data.Product.Base using (_,_) open import Data.Hypergraph.Label using (HypergraphLabel) open HypergraphLabel Gates using (isCastable) open import Data.Castable using (IsCastable) @@ -105,15 +103,14 @@ module _ {v : ℕ} where : {H H′ : Hypergraph′ v} → Hypergraph-same H H′ → from H ≈ from H′ - from-cong {H} {H′} ≈H = record - { ≡-normalized = ≡-normalized - } + from-cong {H} {H′} ≈H = mk≈ (toList-↭ (flip ↔h , H∘ρ≗H′)) where + module H = Hypergraph′ H module H′ = Hypergraph′ H′ open Hypergraph′ open Hypergraph-same ≈H using (↔h; ≗a; ≗l; ≗j; inverseˡ) renaming (from to f; to to t) - asEdge : (H : Hypergraph′ v) → Fin (h H) → Edge v + asEdge : (H : Hypergraph′ v) → Fin (h H) → Edge.Edge v asEdge H e = record { label = l H e ; ports = toVec (j H e) } to-from : (e : Fin H′.h) → t (f e) ≡ e @@ -134,13 +131,6 @@ module _ {v : ℕ} where ≗l′ : (e : Fin H′.h) → cast-gate (≗a′ e) (H.l (f e)) ≡ H′.l e ≗l′ e = ≈-trans {H.a _} (l≗ (f e)) (l∘to-from e) - import Data.Vec.Relation.Binary.Equality.Cast as VecCast - open import Data.Vec using (cast) renaming (map to vecmap) - open import Data.Vec.Properties using (tabulate-cong; tabulate-∘; map-cast) - - open import Data.Fin.Base using () renaming (cast to fincast) - open import Data.Fin.Properties using () renaming (cast-trans to fincast-trans; cast-is-id to fincast-is-id) - j∘to-from : (e : Fin H′.h) (i : Fin (H′.a (t (f e)))) → H′.j (t (f e)) i @@ -161,40 +151,28 @@ module _ {v : ℕ} where {A : Set} (m≡n : m ≡ n) (f : Fin n → A) - → cast m≡n (toVec (f ∘ fincast m≡n)) ≡ toVec f + → Vec.cast m≡n (toVec (f ∘ fincast m≡n)) ≡ toVec f cast-toVec m≡n f rewrite m≡n = begin - cast _ (toVec (f ∘ (fincast _))) ≡⟨ VecCast.cast-is-id ≡.refl (toVec (f ∘ fincast ≡.refl)) ⟩ + Vec.cast _ (toVec (f ∘ (fincast _))) ≡⟨ VecCast.cast-is-id ≡.refl (toVec (f ∘ fincast ≡.refl)) ⟩ toVec (f ∘ fincast _) ≡⟨ tabulate-∘ f (fincast ≡.refl) ⟩ - vecmap f (toVec (fincast _)) ≡⟨ ≡.cong (vecmap f) (tabulate-cong (fincast-is-id ≡.refl)) ⟩ - vecmap f (toVec id) ≡⟨ tabulate-∘ f id ⟨ + Vec.map f (toVec (fincast _)) ≡⟨ ≡.cong (Vec.map f) (tabulate-cong (fincast-is-id ≡.refl)) ⟩ + Vec.map f (toVec id) ≡⟨ tabulate-∘ f id ⟨ toVec f ∎ - ≗p′ : (e : Fin H′.h) → cast (≗a′ e) (toVec (H.j (f e))) ≡ toVec (H′.j e) + ≗p′ : (e : Fin H′.h) → Vec.cast (≗a′ e) (toVec (H.j (f e))) ≡ toVec (H′.j e) ≗p′ e = begin - cast (≗a′ e) (toVec (H.j (f e))) ≡⟨ ≡.cong (cast (≗a′ e)) (tabulate-cong (≗j′ e)) ⟩ - cast _ (toVec (H′.j e ∘ fincast _)) ≡⟨ cast-toVec (≗a′ e) (H′.j e) ⟩ + Vec.cast (≗a′ e) (toVec (H.j (f e))) ≡⟨ ≡.cong (Vec.cast (≗a′ e)) (tabulate-cong (≗j′ e)) ⟩ + Vec.cast _ (toVec (H′.j e ∘ fincast _)) ≡⟨ cast-toVec (≗a′ e) (H′.j e) ⟩ toVec (H′.j e) ∎ H∘ρ≗H′ : (e : Fin H′.h) → asEdge H (↔h ⟨$⟩ˡ e) ≡ asEdge H′ e - H∘ρ≗H′ e = ≈-Edge⇒≡ record + H∘ρ≗H′ e = Edge.≈⇒≡ record { ≡arity = ≗a′ e ; ≡label = ≗l′ e ; ≡ports = ≗p′ e } - open Hypergraph using (edges) - open →-Reasoning - ≡-normalized : normalize (from H) ≡ normalize (from H′) - ≡-normalized = - flip ↔h , H∘ρ≗H′ ∶ asEdge H V.↭ asEdge H′ - |> toList-↭ ∶ toList (asEdge H) L.↭ toList (asEdge H′) - |> L.↭⇒↭ₛ′ ≈-Edge-IsEquivalence ∶ Permutation ≈-Edge (edges (from H)) (edges (from H′)) - |> sorted-≋ ∶ Pointwise ≈-Edge (sort (edges (from H))) (sort (edges (from H′))) - |> map ≈-Edge⇒≡ ∶ Pointwise _≡_ (sort (edges (from H))) (sort (edges (from H′))) - |> Pointwise-≡⇒≡ ∶ sort (edges (from H)) ≡ sort (edges (from H′)) - |> ≡.cong mkHypergraph ∶ normalize (from H) ≡ normalize (from H′) - -equiv : (v : ℕ) → Equivalence (Hypergraphₛ v) (Hypergraph-Setoid′ v) +equiv : (v : ℕ) → Equivalence (Circuitₛ v) (Hypergraph-Setoid′ v) equiv v = record { to = to ; from = from diff --git a/Data/Hypergraph.agda b/Data/Hypergraph.agda index 18a259b..ff92d0e 100644 --- a/Data/Hypergraph.agda +++ b/Data/Hypergraph.agda @@ -1,26 +1,71 @@ {-# OPTIONS --without-K --safe #-} -open import Level using (Level) - +open import Level using (Level; 0ℓ) open import Data.Hypergraph.Label using (HypergraphLabel) module Data.Hypergraph {c ℓ : Level} (HL : HypergraphLabel) where import Data.List.Relation.Binary.Pointwise as PW -import Data.Hypergraph.Edge HL as HypergraphEdge import Function.Reasoning as →-Reasoning import Relation.Binary.PropositionalEquality as ≡ +import Data.Hypergraph.Edge HL as Hyperedge +import Data.List.Relation.Binary.Permutation.Propositional as List-↭ -open import Data.Hypergraph.Base {c} HL public -open import Data.Hypergraph.Setoid {c} {ℓ} HL public +open import Data.List using (List; map) +open import Data.List.Relation.Binary.Permutation.Propositional using (_↭_; ↭-refl; ↭-sym; ↭-trans) open import Data.Nat using (ℕ) +open import Data.String using (String; unlines) open import Function using (_∘_; _⟶ₛ_; Func) -open import Level using (0ℓ) open import Relation.Binary using (Setoid) -module Edge = HypergraphEdge +module Edge = Hyperedge +open Edge using (Edge; Edgeₛ) + +-- A hypergraph is a list of edges +record Hypergraph (v : ℕ) : Set c where + constructor mkHypergraph + field + edges : List (Edge v) + +module _ {v : ℕ} where + + show : Hypergraph v → String + show (mkHypergraph e) = unlines (map Edge.show e) + + -- an equivalence relation on hypergraphs + record _≈_ (H H′ : Hypergraph v) : Set ℓ where + + constructor mk≈ + + module H = Hypergraph H + module H′ = Hypergraph H′ + + field + ↭-edges : H.edges ↭ H′.edges + + infixr 4 _≈_ + + ≈-refl : {H : Hypergraph v} → H ≈ H + ≈-refl = mk≈ ↭-refl + + ≈-sym : {H H′ : Hypergraph v} → H ≈ H′ → H′ ≈ H + ≈-sym (mk≈ ≡n) = mk≈ (↭-sym ≡n) + + ≈-trans : {H H′ H″ : Hypergraph v} → H ≈ H′ → H′ ≈ H″ → H ≈ H″ + ≈-trans (mk≈ ≡n₁) (mk≈ ≡n₂) = mk≈ (↭-trans ≡n₁ ≡n₂) + +-- The setoid of labeled hypergraphs with v nodes +Hypergraphₛ : ℕ → Setoid c ℓ +Hypergraphₛ v = record + { Carrier = Hypergraph v + ; _≈_ = _≈_ + ; isEquivalence = record + { refl = ≈-refl + ; sym = ≈-sym + ; trans = ≈-trans + } + } -open Edge using (Edgeₛ; ≈-Edge⇒≡) open Func List∘Edgeₛ : (n : ℕ) → Setoid 0ℓ 0ℓ @@ -29,7 +74,7 @@ List∘Edgeₛ = PW.setoid ∘ Edgeₛ mkHypergraphₛ : {n : ℕ} → List∘Edgeₛ n ⟶ₛ Hypergraphₛ n mkHypergraphₛ .to = mkHypergraph mkHypergraphₛ {n} .cong ≋-edges = ≋-edges - |> PW.map ≈-Edge⇒≡ + |> PW.map Edge.≈⇒≡ |> PW.Pointwise-≡⇒≡ |> ≡.cong mkHypergraph |> Setoid.reflexive (Hypergraphₛ n) diff --git a/Data/Hypergraph/Base.agda b/Data/Hypergraph/Base.agda deleted file mode 100644 index 0910e02..0000000 --- a/Data/Hypergraph/Base.agda +++ /dev/null @@ -1,25 +0,0 @@ -{-# OPTIONS --without-K --safe #-} - -open import Level using (Level) -open import Data.Hypergraph.Label using (HypergraphLabel) - -module Data.Hypergraph.Base {ℓ : Level} (HL : HypergraphLabel) where - -import Data.Hypergraph.Edge HL as Edge - -open import Data.List using (List; map) -open import Data.Nat.Base using (ℕ) -open import Data.String using (String; unlines) - -open Edge using (Edge) - -record Hypergraph (v : ℕ) : Set ℓ where - constructor mkHypergraph - field - edges : List (Edge v) - -normalize : {v : ℕ} → Hypergraph v → Hypergraph v -normalize (mkHypergraph e) = mkHypergraph (Edge.sort e) - -show : {v : ℕ} → Hypergraph v → String -show (mkHypergraph e) = unlines (map Edge.show e) diff --git a/Data/Hypergraph/Edge.agda b/Data/Hypergraph/Edge.agda index ee32393..1e24559 100644 --- a/Data/Hypergraph/Edge.agda +++ b/Data/Hypergraph/Edge.agda @@ -4,43 +4,32 @@ open import Data.Hypergraph.Label using (HypergraphLabel) module Data.Hypergraph.Edge (HL : HypergraphLabel) where -import Data.List.Sort as ListSort -import Data.Fin as Fin -import Data.Fin.Properties as FinProp import Data.Vec as Vec import Data.Vec.Relation.Binary.Equality.Cast as VecCast -import Data.Vec.Relation.Binary.Lex.Strict as Lex import Relation.Binary.PropositionalEquality as ≡ -import Relation.Binary.Properties.DecTotalOrder as DTOP -import Relation.Binary.Properties.StrictTotalOrder as STOP -open import Relation.Binary using (Rel; IsStrictTotalOrder; Tri; Trichotomous; _Respects_) -open import Data.Castable using (IsCastable) open import Data.Fin using (Fin) open import Data.Fin.Show using () renaming (show to showFin) -open import Data.Nat using (ℕ; _<_) -open import Data.Nat.Properties using (<-irrefl; <-trans; <-resp₂-≡; <-cmp) -open import Data.Product.Base using (_,_; proj₁; proj₂) +open import Data.Nat using (ℕ) open import Data.String using (String; _<+>_) -open import Data.Vec.Relation.Binary.Pointwise.Inductive using (≡⇒Pointwise-≡; Pointwise-≡⇒≡) open import Data.Vec.Show using () renaming (show to showVec) open import Level using (0ℓ) -open import Relation.Binary using (Setoid; DecTotalOrder; StrictTotalOrder; IsEquivalence) -open import Relation.Nullary using (¬_) - +open import Relation.Binary using (Setoid; IsEquivalence) module HL = HypergraphLabel HL + open HL using (Label; cast; cast-is-id) open Vec using (Vec) record Edge (v : ℕ) : Set where + constructor mkEdge field {arity} : ℕ label : Label arity ports : Vec (Fin v) arity map : {n m : ℕ} → (Fin n → Fin m) → Edge n → Edge m -map {n} {m} f edge = record +map f edge = record { label = label ; ports = Vec.map f ports } @@ -50,299 +39,58 @@ map {n} {m} f edge = record open ≡ using (_≡_) open VecCast using (_≈[_]_) -record ≈-Edge {n : ℕ} (E E′ : Edge n) : Set where - module E = Edge E - module E′ = Edge E′ - field - ≡arity : E.arity ≡ E′.arity - ≡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 - -≈-Edge-IsEquivalence : {v : ℕ} → IsEquivalence (≈-Edge {v}) -≈-Edge-IsEquivalence = record - { refl = ≈-Edge-refl - ; sym = ≈-Edge-sym - ; trans = ≈-Edge-trans - } - -open HL using (_[_<_]) -_<<_ : {v a : ℕ} → Rel (Vec (Fin v) a) 0ℓ -_<<_ {v} = Lex.Lex-< _≡_ (Fin._<_ {v}) -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 - <-ports - : {x y : Edge v} - (≡a : Edge.arity x ≡ Edge.arity y) - (≡l : Edge.label x HL.≈[ ≡a ] Edge.label y) - → Vec.cast ≡a (Edge.ports x) << Edge.ports 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-irrefl record { ≡ports = ≡p } (<-ports ≡.refl ≡l x<y) - = Lex.<-irrefl FinProp.<-irrefl (≡⇒Pointwise-≡ ≡p) x<y - -<-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 (<-arity i<j) (<-ports ≡.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-trans {k = k} (<-label ≡.refl i<j) (<-ports ≡.refl ≡.refl _) - = <-label ≡.refl (<-respʳ-≈ (≡.sym (HL.≈-reflexive ≡.refl)) i<j) - where - open DTOP (HL.decTotalOrder (Edge.arity k)) using (<-respʳ-≈) -<-Edge-trans (<-ports ≡.refl _ _) (<-arity j<k) = <-arity j<k -<-Edge-trans {k = k} (<-ports ≡.refl ≡.refl _) (<-label ≡.refl j<k) - = <-label ≡.refl (<-respˡ-≈ (≡.cong (cast _) (HL.≈-reflexive ≡.refl)) j<k) - where - open DTOP (HL.decTotalOrder (Edge.arity k)) using (<-respˡ-≈) -<-Edge-trans {j = j} (<-ports ≡.refl ≡l₁ i<j) (<-ports ≡.refl ≡l₂ j<k) - rewrite (VecCast.cast-is-id ≡.refl (Edge.ports j)) - = <-ports ≡.refl - (HL.≈-trans ≡l₁ ≡l₂) - (Lex.<-trans ≡-isPartialEquivalence FinProp.<-resp₂-≡ FinProp.<-trans i<j j<k) - where - open IsEquivalence ≡.isEquivalence using () renaming (isPartialEquivalence to ≡-isPartialEquivalence) - -<-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ˡ-≈ record { ≡arity = ≡.refl ; ≡label = ≡.refl; ≡ports = ≡.refl} (<-ports ≡.refl ≡.refl x₁<y) - = <-ports - ≡.refl - (≡.cong (cast _) (HL.≈-reflexive ≡.refl)) - (Lex.<-respectsˡ - ≡-isPartialEquivalence - FinProp.<-respˡ-≡ - (≡⇒Pointwise-≡ (≡.sym (VecCast.≈-reflexive ≡.refl))) - x₁<y) - where - open IsEquivalence ≡.isEquivalence using () renaming (isPartialEquivalence to ≡-isPartialEquivalence) - -<-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ʳ-≈) -<-Edge-respʳ-≈ record { ≡arity = ≡.refl ; ≡label = ≡.refl; ≡ports = ≡.refl} (<-ports ≡.refl ≡.refl x<y₁) - = <-ports - ≡.refl - (≡.cong (cast _) (≡.sym (HL.≈-reflexive ≡.refl))) - (Lex.<-respectsʳ - ≡-isPartialEquivalence - FinProp.<-respʳ-≡ - (≡⇒Pointwise-≡ (≡.sym (VecCast.≈-reflexive ≡.refl))) - x<y₁) - where - open IsEquivalence ≡.isEquivalence using () renaming (isPartialEquivalence to ≡-isPartialEquivalence) - -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 _) = x≢y (≡.sym ≡a) - ¬y<x (<-ports ≡a _ _) = 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 _ y<x) = y≮x′ (<-respˡ-≈ (HL.≈-reflexive ≡.refl) y<x) - ¬y<x (<-ports _ ≡l _) = x≢y (≡.trans (≡.sym ≡l) (cast-is-id ≡.refl y.label)) - ... | tri≈ x≮y′ x≡y′ y≮x′ = compare-ports - where - compare-ports : Tri (<-Edge x y) (≈-Edge x y) (<-Edge y x) - compare-ports with Lex.<-cmp ≡.sym FinProp.<-cmp x.ports y.ports - ... | tri< x<y x≢y y≮x″ = - tri< - (<-ports ≡.refl - (HL.≈-reflexive x≡y′) - (Lex.<-respectsˡ - ≡-isPartialEquivalence - FinProp.<-respˡ-≡ - (≡⇒Pointwise-≡ (≡.sym (VecCast.≈-reflexive ≡.refl))) - x<y)) - (λ x≡y → x≢y (≡⇒Pointwise-≡ (≡.trans (≡.sym (VecCast.≈-reflexive ≡.refl)) (≡ports x≡y)))) - ¬y<x - where - open IsEquivalence ≡.isEquivalence using () renaming (isPartialEquivalence to ≡-isPartialEquivalence) - ¬y<x : ¬ <-Edge y x - ¬y<x (<-arity y<x) = y≮x y<x - ¬y<x (<-label _ y<x) = y≮x′ (<-respˡ-≈ (HL.≈-reflexive ≡.refl) y<x) - ¬y<x (<-ports _ _ y<x) = - y≮x″ - (Lex.<-respectsˡ - ≡-isPartialEquivalence - FinProp.<-respˡ-≡ - (≡⇒Pointwise-≡ (VecCast.≈-reflexive ≡.refl)) - y<x) - ... | tri≈ x≮y″ x≡y″ y≮x″ = tri≈ - ¬x<y - (record { ≡arity = ≡.refl ; ≡label = HL.≈-reflexive x≡y′ ; ≡ports = VecCast.≈-reflexive (Pointwise-≡⇒≡ x≡y″) }) - ¬y<x - where - open IsEquivalence ≡.isEquivalence using () renaming (isPartialEquivalence to ≡-isPartialEquivalence) - ¬x<y : ¬ <-Edge x y - ¬x<y (<-arity x<y) = x≮y x<y - ¬x<y (<-label _ x<y) = x≮y′ (<-respˡ-≈ (HL.≈-reflexive ≡.refl) x<y) - ¬x<y (<-ports _ _ x<y) = - x≮y″ - (Lex.<-respectsˡ - ≡-isPartialEquivalence - FinProp.<-respˡ-≡ - (≡⇒Pointwise-≡ (VecCast.≈-reflexive ≡.refl)) - x<y) - ¬y<x : ¬ <-Edge y x - ¬y<x (<-arity y<x) = y≮x y<x - ¬y<x (<-label _ y<x) = y≮x′ (<-respˡ-≈ (HL.≈-reflexive ≡.refl) y<x) - ¬y<x (<-ports _ _ y<x) = - y≮x″ - (Lex.<-respectsˡ - ≡-isPartialEquivalence - FinProp.<-respˡ-≡ - (≡⇒Pointwise-≡ (VecCast.≈-reflexive ≡.refl)) - y<x) - - ... | tri> x≮y″ x≢y y<x = - tri> - ¬x<y - (λ x≡y → x≢y (≡⇒Pointwise-≡ (≡.trans (≡.sym (VecCast.≈-reflexive ≡.refl)) (≡ports x≡y)))) - (<-ports - ≡.refl - (HL.≈-sym (HL.≈-reflexive x≡y′)) - (Lex.<-respectsˡ - ≡-isPartialEquivalence - FinProp.<-respˡ-≡ - (≡⇒Pointwise-≡ (≡.sym (VecCast.≈-reflexive ≡.refl))) - y<x)) - where - open IsEquivalence ≡.isEquivalence using () renaming (isPartialEquivalence to ≡-isPartialEquivalence) - ¬x<y : ¬ <-Edge x y - ¬x<y (<-arity x<y) = x≮y x<y - ¬x<y (<-label _ x<y) = x≮y′ (<-respˡ-≈ (HL.≈-reflexive ≡.refl) x<y) - ¬x<y (<-ports _ _ x<y) = - x≮y″ - (Lex.<-respectsˡ - ≡-isPartialEquivalence - FinProp.<-respˡ-≡ - (≡⇒Pointwise-≡ (VecCast.≈-reflexive ≡.refl)) - x<y) - ... | 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) - ¬x<y (<-ports _ ≡l _) = x≢y (≡.trans (≡.sym (HL.≈-reflexive ≡.refl)) ≡l) -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 - ¬x<y (<-ports ≡a _ _) = x≢y ≡a - -isStrictTotalOrder : {v : ℕ} → IsStrictTotalOrder (≈-Edge {v}) (<-Edge {v}) -isStrictTotalOrder = record - { isStrictPartialOrder = record - { isEquivalence = ≈-Edge-IsEquivalence - ; irrefl = <-Edge-irrefl - ; trans = <-Edge-trans - ; <-resp-≈ = <-Edge-respʳ-≈ , <-Edge-respˡ-≈ - } - ; compare = tri - } - -strictTotalOrder : {v : ℕ} → StrictTotalOrder 0ℓ 0ℓ 0ℓ -strictTotalOrder {v} = record - { Carrier = Edge v - ; _≈_ = ≈-Edge {v} - ; _<_ = <-Edge {v} - ; isStrictTotalOrder = isStrictTotalOrder {v} - } - -show : {v : ℕ} → Edge v → String -show record { arity = a ; label = l ; ports = p} = HL.showLabel a l <+> showVec showFin p - -open module STOP′ {v} = STOP (strictTotalOrder {v}) using (decTotalOrder) public - -≈-Edge⇒≡ : {v : ℕ} {x y : Edge v} → ≈-Edge x y → x ≡ y -≈-Edge⇒≡ {v} {record { label = l ; ports = p }} record { ≡arity = ≡.refl ; ≡label = ≡.refl ; ≡ports = ≡.refl } - rewrite cast-is-id ≡.refl l - rewrite VecCast.cast-is-id ≡.refl p = ≡.refl - -module Sort {v} = ListSort (decTotalOrder {v}) -open Sort using (sort) public +module _ {v : ℕ} where + + -- an equivalence relation on edges with v nodes + record _≈_ (E E′ : Edge v) : Set where + constructor mk≈ + module E = Edge E + module E′ = Edge E′ + field + ≡arity : E.arity ≡ E′.arity + ≡label : cast ≡arity E.label ≡ E′.label + ≡ports : E.ports ≈[ ≡arity ] E′.ports + + ≈-refl : {x : Edge v} → x ≈ x + ≈-refl = record + { ≡arity = ≡.refl + ; ≡label = HL.≈-reflexive ≡.refl + ; ≡ports = VecCast.≈-reflexive ≡.refl + } + + ≈-sym : {x y : Edge v} → x ≈ y → y ≈ x + ≈-sym x≈y = record + { ≡arity = ≡.sym ≡arity + ; ≡label = HL.≈-sym ≡label + ; ≡ports = VecCast.≈-sym ≡ports + } + where + open _≈_ x≈y + + ≈-trans : {i j k : Edge v} → i ≈ j → j ≈ k → i ≈ k + ≈-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 = _≈_ i≈j + module j≈k = _≈_ j≈k + + ≈-IsEquivalence : IsEquivalence _≈_ + ≈-IsEquivalence = record + { refl = ≈-refl + ; sym = ≈-sym + ; trans = ≈-trans + } + + show : Edge v → String + show (mkEdge {a} l p) = HL.showLabel a l <+> showVec showFin p + + ≈⇒≡ : {x y : Edge v} → x ≈ y → x ≡ y + ≈⇒≡ {mkEdge l p} (mk≈ ≡.refl ≡.refl ≡.refl) + rewrite cast-is-id ≡.refl l + rewrite VecCast.cast-is-id ≡.refl p = ≡.refl Edgeₛ : (v : ℕ) → Setoid 0ℓ 0ℓ -Edgeₛ v = record { isEquivalence = ≈-Edge-IsEquivalence {v} } +Edgeₛ v = record { isEquivalence = ≈-IsEquivalence {v} } diff --git a/Data/Hypergraph/Edge/Order.agda b/Data/Hypergraph/Edge/Order.agda new file mode 100644 index 0000000..4b3c1e8 --- /dev/null +++ b/Data/Hypergraph/Edge/Order.agda @@ -0,0 +1,280 @@ +{-# OPTIONS --without-K --safe #-} + +open import Data.Hypergraph.Label using (HypergraphLabel) + +module Data.Hypergraph.Edge.Order (HL : HypergraphLabel) where + +import Data.List.Sort as ListSort +import Data.Fin as Fin +import Data.Fin.Properties as FinProp +import Data.Vec as Vec +import Data.Vec.Relation.Binary.Equality.Cast as VecCast +import Data.Vec.Relation.Binary.Lex.Strict as Lex +import Relation.Binary.PropositionalEquality as ≡ +import Relation.Binary.Properties.DecTotalOrder as DTOP +import Relation.Binary.Properties.StrictTotalOrder as STOP + +open import Data.Hypergraph.Edge HL using (Edge; ≈-Edge; ≈-Edge-IsEquivalence) +open import Data.Fin using (Fin) +open import Data.Nat using (ℕ; _<_) +open import Data.Nat.Properties using (<-irrefl; <-trans; <-resp₂-≡; <-cmp) +open import Data.Product.Base using (_,_; proj₁; proj₂) +open import Data.Vec.Relation.Binary.Pointwise.Inductive using (Pointwise-≡⇒≡) +open import Level using (0ℓ) +open import Relation.Binary + using + ( Rel + ; Tri ; Trichotomous + ; IsStrictTotalOrder ; IsEquivalence + ; _Respects_ + ; DecTotalOrder ; StrictTotalOrder + ) +open import Relation.Nullary using (¬_) + +module HL = HypergraphLabel HL +open HL using (Label; cast; cast-is-id) +open Vec using (Vec) + +open ≡ using (_≡_) + +open HL using (_[_<_]) +_<<_ : {v a : ℕ} → Rel (Vec (Fin v) a) 0ℓ +_<<_ {v} = Lex.Lex-< _≡_ (Fin._<_ {v}) + +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 + <-ports + : {x y : Edge v} + (≡a : Edge.arity x ≡ Edge.arity y) + (≡l : Edge.label x HL.≈[ ≡a ] Edge.label y) + → Vec.cast ≡a (Edge.ports x) << Edge.ports 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-irrefl record { ≡ports = ≡p } (<-ports ≡.refl ≡l x<y) + = Lex.<-irrefl FinProp.<-irrefl (≡⇒Pointwise-≡ ≡p) x<y + +<-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 (<-arity i<j) (<-ports ≡.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-trans {k = k} (<-label ≡.refl i<j) (<-ports ≡.refl ≡.refl _) + = <-label ≡.refl (<-respʳ-≈ (≡.sym (HL.≈-reflexive ≡.refl)) i<j) + where + open DTOP (HL.decTotalOrder (Edge.arity k)) using (<-respʳ-≈) +<-Edge-trans (<-ports ≡.refl _ _) (<-arity j<k) = <-arity j<k +<-Edge-trans {k = k} (<-ports ≡.refl ≡.refl _) (<-label ≡.refl j<k) + = <-label ≡.refl (<-respˡ-≈ (≡.cong (cast _) (HL.≈-reflexive ≡.refl)) j<k) + where + open DTOP (HL.decTotalOrder (Edge.arity k)) using (<-respˡ-≈) +<-Edge-trans {j = j} (<-ports ≡.refl ≡l₁ i<j) (<-ports ≡.refl ≡l₂ j<k) + rewrite (VecCast.cast-is-id ≡.refl (Edge.ports j)) + = <-ports ≡.refl + (HL.≈-trans ≡l₁ ≡l₂) + (Lex.<-trans ≡-isPartialEquivalence FinProp.<-resp₂-≡ FinProp.<-trans i<j j<k) + where + open IsEquivalence ≡.isEquivalence using () renaming (isPartialEquivalence to ≡-isPartialEquivalence) + +<-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ˡ-≈ record { ≡arity = ≡.refl ; ≡label = ≡.refl; ≡ports = ≡.refl} (<-ports ≡.refl ≡.refl x₁<y) + = <-ports + ≡.refl + (≡.cong (cast _) (HL.≈-reflexive ≡.refl)) + (Lex.<-respectsˡ + ≡-isPartialEquivalence + FinProp.<-respˡ-≡ + (≡⇒Pointwise-≡ (≡.sym (VecCast.≈-reflexive ≡.refl))) + x₁<y) + where + open IsEquivalence ≡.isEquivalence using () renaming (isPartialEquivalence to ≡-isPartialEquivalence) + +<-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ʳ-≈) +<-Edge-respʳ-≈ record { ≡arity = ≡.refl ; ≡label = ≡.refl; ≡ports = ≡.refl} (<-ports ≡.refl ≡.refl x<y₁) + = <-ports + ≡.refl + (≡.cong (cast _) (≡.sym (HL.≈-reflexive ≡.refl))) + (Lex.<-respectsʳ + ≡-isPartialEquivalence + FinProp.<-respʳ-≡ + (≡⇒Pointwise-≡ (≡.sym (VecCast.≈-reflexive ≡.refl))) + x<y₁) + where + open IsEquivalence ≡.isEquivalence using () renaming (isPartialEquivalence to ≡-isPartialEquivalence) + +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 _) = x≢y (≡.sym ≡a) + ¬y<x (<-ports ≡a _ _) = 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 _ y<x) = y≮x′ (<-respˡ-≈ (HL.≈-reflexive ≡.refl) y<x) + ¬y<x (<-ports _ ≡l _) = x≢y (≡.trans (≡.sym ≡l) (cast-is-id ≡.refl y.label)) + ... | tri≈ x≮y′ x≡y′ y≮x′ = compare-ports + where + compare-ports : Tri (<-Edge x y) (≈-Edge x y) (<-Edge y x) + compare-ports with Lex.<-cmp ≡.sym FinProp.<-cmp x.ports y.ports + ... | tri< x<y x≢y y≮x″ = + tri< + (<-ports ≡.refl + (HL.≈-reflexive x≡y′) + (Lex.<-respectsˡ + ≡-isPartialEquivalence + FinProp.<-respˡ-≡ + (≡⇒Pointwise-≡ (≡.sym (VecCast.≈-reflexive ≡.refl))) + x<y)) + (λ x≡y → x≢y (≡⇒Pointwise-≡ (≡.trans (≡.sym (VecCast.≈-reflexive ≡.refl)) (≡ports x≡y)))) + ¬y<x + where + open IsEquivalence ≡.isEquivalence using () renaming (isPartialEquivalence to ≡-isPartialEquivalence) + ¬y<x : ¬ <-Edge y x + ¬y<x (<-arity y<x) = y≮x y<x + ¬y<x (<-label _ y<x) = y≮x′ (<-respˡ-≈ (HL.≈-reflexive ≡.refl) y<x) + ¬y<x (<-ports _ _ y<x) = + y≮x″ + (Lex.<-respectsˡ + ≡-isPartialEquivalence + FinProp.<-respˡ-≡ + (≡⇒Pointwise-≡ (VecCast.≈-reflexive ≡.refl)) + y<x) + ... | tri≈ x≮y″ x≡y″ y≮x″ = tri≈ + ¬x<y + (record { ≡arity = ≡.refl ; ≡label = HL.≈-reflexive x≡y′ ; ≡ports = VecCast.≈-reflexive (Pointwise-≡⇒≡ x≡y″) }) + ¬y<x + where + open IsEquivalence ≡.isEquivalence using () renaming (isPartialEquivalence to ≡-isPartialEquivalence) + ¬x<y : ¬ <-Edge x y + ¬x<y (<-arity x<y) = x≮y x<y + ¬x<y (<-label _ x<y) = x≮y′ (<-respˡ-≈ (HL.≈-reflexive ≡.refl) x<y) + ¬x<y (<-ports _ _ x<y) = + x≮y″ + (Lex.<-respectsˡ + ≡-isPartialEquivalence + FinProp.<-respˡ-≡ + (≡⇒Pointwise-≡ (VecCast.≈-reflexive ≡.refl)) + x<y) + ¬y<x : ¬ <-Edge y x + ¬y<x (<-arity y<x) = y≮x y<x + ¬y<x (<-label _ y<x) = y≮x′ (<-respˡ-≈ (HL.≈-reflexive ≡.refl) y<x) + ¬y<x (<-ports _ _ y<x) = + y≮x″ + (Lex.<-respectsˡ + ≡-isPartialEquivalence + FinProp.<-respˡ-≡ + (≡⇒Pointwise-≡ (VecCast.≈-reflexive ≡.refl)) + y<x) + + ... | tri> x≮y″ x≢y y<x = + tri> + ¬x<y + (λ x≡y → x≢y (≡⇒Pointwise-≡ (≡.trans (≡.sym (VecCast.≈-reflexive ≡.refl)) (≡ports x≡y)))) + (<-ports + ≡.refl + (HL.≈-sym (HL.≈-reflexive x≡y′)) + (Lex.<-respectsˡ + ≡-isPartialEquivalence + FinProp.<-respˡ-≡ + (≡⇒Pointwise-≡ (≡.sym (VecCast.≈-reflexive ≡.refl))) + y<x)) + where + open IsEquivalence ≡.isEquivalence using () renaming (isPartialEquivalence to ≡-isPartialEquivalence) + ¬x<y : ¬ <-Edge x y + ¬x<y (<-arity x<y) = x≮y x<y + ¬x<y (<-label _ x<y) = x≮y′ (<-respˡ-≈ (HL.≈-reflexive ≡.refl) x<y) + ¬x<y (<-ports _ _ x<y) = + x≮y″ + (Lex.<-respectsˡ + ≡-isPartialEquivalence + FinProp.<-respˡ-≡ + (≡⇒Pointwise-≡ (VecCast.≈-reflexive ≡.refl)) + x<y) + ... | 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) + ¬x<y (<-ports _ ≡l _) = x≢y (≡.trans (≡.sym (HL.≈-reflexive ≡.refl)) ≡l) +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 + ¬x<y (<-ports ≡a _ _) = x≢y ≡a + +isStrictTotalOrder : {v : ℕ} → IsStrictTotalOrder (≈-Edge {v}) (<-Edge {v}) +isStrictTotalOrder = record + { isStrictPartialOrder = record + { isEquivalence = ≈-Edge-IsEquivalence + ; irrefl = <-Edge-irrefl + ; trans = <-Edge-trans + ; <-resp-≈ = <-Edge-respʳ-≈ , <-Edge-respˡ-≈ + } + ; compare = tri + } + +strictTotalOrder : {v : ℕ} → StrictTotalOrder 0ℓ 0ℓ 0ℓ +strictTotalOrder {v} = record + { Carrier = Edge v + ; _≈_ = ≈-Edge {v} + ; _<_ = <-Edge {v} + ; isStrictTotalOrder = isStrictTotalOrder {v} + } + +open module STOP′ {v} = STOP (strictTotalOrder {v}) using (decTotalOrder) public + +module Sort {v} = ListSort (decTotalOrder {v}) +open Sort using (sort) public diff --git a/Data/Hypergraph/Setoid.agda b/Data/Hypergraph/Setoid.agda deleted file mode 100644 index d9cc024..0000000 --- a/Data/Hypergraph/Setoid.agda +++ /dev/null @@ -1,59 +0,0 @@ -{-# OPTIONS --without-K --safe #-} - -open import Level using (Level; _⊔_) -open import Data.Hypergraph.Label using (HypergraphLabel) - -module Data.Hypergraph.Setoid {c ℓ : Level} (HL : HypergraphLabel) where - -import Data.List.Relation.Binary.Permutation.Propositional as List-↭ - -open import Data.Hypergraph.Edge HL using (module Sort) -open import Data.Hypergraph.Base {c} HL using (Hypergraph; normalize) -open import Data.Nat using (ℕ) -open import Relation.Binary using (Setoid) -open import Relation.Binary.PropositionalEquality as ≡ using (_≡_) - --- an equivalence relation on hypergraphs -record _≈_ {v : ℕ} (H H′ : Hypergraph v) : Set (c ⊔ ℓ) where - - constructor mk≈ - - module H = Hypergraph H - module H′ = Hypergraph H′ - - field - ≡-normalized : normalize H ≡ normalize H′ - - open Hypergraph using (edges) - - ≡-edges : edges (normalize H) ≡ edges (normalize H′) - ≡-edges = ≡.cong edges ≡-normalized - - open List-↭ using (_↭_; ↭-reflexive; ↭-sym; ↭-trans) - open Sort using (sort-↭) - - ↭-edges : H.edges ↭ H′.edges - ↭-edges = ↭-trans (↭-sym (sort-↭ H.edges)) (↭-trans (↭-reflexive ≡-edges) (sort-↭ H′.edges)) - -infixr 4 _≈_ - -≈-refl : {v : ℕ} {H : Hypergraph v} → H ≈ H -≈-refl = mk≈ ≡.refl - -≈-sym : {v : ℕ} {H H′ : Hypergraph v} → H ≈ H′ → H′ ≈ H -≈-sym (mk≈ ≡n) = mk≈ (≡.sym ≡n) - -≈-trans : {v : ℕ} {H H′ H″ : Hypergraph v} → H ≈ H′ → H′ ≈ H″ → H ≈ H″ -≈-trans (mk≈ ≡n₁) (mk≈ ≡n₂) = mk≈ (≡.trans ≡n₁ ≡n₂) - --- The setoid of labeled hypergraphs with v nodes -Hypergraphₛ : ℕ → Setoid c (c ⊔ ℓ) -Hypergraphₛ v = record - { Carrier = Hypergraph v - ; _≈_ = _≈_ - ; isEquivalence = record - { refl = ≈-refl - ; sym = ≈-sym - ; trans = ≈-trans - } - } diff --git a/Functor/Instance/Nat/Circ.agda b/Functor/Instance/Nat/Circ.agda index 0f18c4c..d5bcc9b 100644 --- a/Functor/Instance/Nat/Circ.agda +++ b/Functor/Instance/Nat/Circ.agda @@ -24,7 +24,7 @@ module List∘Edge = Functor List∘Edge open Func open Functor -Circ : Functor Nat (Setoids c (c ⊔ ℓ)) +Circ : Functor Nat (Setoids c ℓ) Circ .F₀ = Circuitₛ Circ .F₁ = mapₛ Circ .identity = cong mkCircuitₛ List∘Edge.identity diff --git a/Functor/Instance/Nat/Edge.agda b/Functor/Instance/Nat/Edge.agda index 618807d..f8d47c2 100644 --- a/Functor/Instance/Nat/Edge.agda +++ b/Functor/Instance/Nat/Edge.agda @@ -11,7 +11,7 @@ open import Categories.Category.Instance.Nat using (Nat) open import Categories.Category.Instance.Setoids using (Setoids) open import Categories.Functor using (Functor) open import Data.Fin using (Fin) -open import Data.Hypergraph.Edge HL as Edge using (≈-Edge-IsEquivalence; map; ≈-Edge; Edgeₛ) +open import Data.Hypergraph.Edge HL as Edge using (Edgeₛ; map; _≈_) open import Data.Nat using (ℕ) open import Data.Vec.Relation.Binary.Equality.Cast using (≈-cong′; ≈-reflexive) open import Level using (0ℓ) @@ -22,10 +22,9 @@ open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_) module HL = HypergraphLabel HL open Edge.Edge +open Edge._≈_ open Func open Functor -open Setoid -open ≈-Edge Edge₁ : {n m : ℕ} → (Fin n → Fin m) → Edgeₛ n ⟶ₛ Edgeₛ m Edge₁ f .to = map f @@ -35,7 +34,7 @@ Edge₁ f .cong x≈y = record ; ≡ports = ≈-cong′ (Vec.map f) (≡ports x≈y) } -map-id : {v : ℕ} {e : Edge.Edge v} → ≈-Edge (map id e) e +map-id : {v : ℕ} {e : Edge.Edge v} → map id e ≈ e map-id .≡arity = ≡.refl map-id .≡label = HL.≈-reflexive ≡.refl map-id {_} {e} .≡ports = ≈-reflexive (VecProps.map-id (ports e)) @@ -45,7 +44,7 @@ map-∘ (f : Fin n → Fin m) (g : Fin m → Fin o) {e : Edge.Edge n} - → ≈-Edge (map (g ∘ f) e) (map g (map f e)) + → map (g ∘ f) e ≈ map g (map f e) map-∘ f g .≡arity = ≡.refl map-∘ f g .≡label = HL.≈-reflexive ≡.refl map-∘ f g {e} .≡ports = ≈-reflexive (VecProps.map-∘ g f (ports e)) @@ -55,7 +54,7 @@ map-resp-≗ {f g : Fin n → Fin m} → f ≗ g → {e : Edge.Edge n} - → ≈-Edge (map f e) (map g e) + → map f e ≈ map g e map-resp-≗ f≗g .≡arity = ≡.refl map-resp-≗ f≗g .≡label = HL.≈-reflexive ≡.refl map-resp-≗ f≗g {e} .≡ports = ≈-reflexive (VecProps.map-cong f≗g (ports e)) |