From 273b12e8f016fe1a716164d514af0b2683711fd2 Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Thu, 3 Jul 2025 12:01:43 -0500 Subject: Add S-Expression parser and circuit typechecker --- Data/Circuit/Gate.agda | 137 ++++++++++++++++++++++++++++++++++++++++++++ Data/Circuit/Typecheck.agda | 78 +++++++++++++++++++++++++ 2 files changed, 215 insertions(+) create mode 100644 Data/Circuit/Gate.agda create mode 100644 Data/Circuit/Typecheck.agda (limited to 'Data/Circuit') diff --git a/Data/Circuit/Gate.agda b/Data/Circuit/Gate.agda new file mode 100644 index 0000000..915ee8b --- /dev/null +++ b/Data/Circuit/Gate.agda @@ -0,0 +1,137 @@ +{-# OPTIONS --without-K --safe #-} + +module Data.Circuit.Gate where + +open import Level using (0ℓ) +open import Data.Castable using (Castable) +open import Data.Hypergraph.Base using (HypergraphLabel; module Edge; module HypergraphList) +open import Data.String using (String) +open import Data.Nat.Base using (ℕ; _≤_) +open import Data.Nat.Properties using (≤-refl; ≤-trans; ≤-antisym; ≤-total) +open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; subst; isEquivalence; cong) +import Relation.Binary.PropositionalEquality as ≡ + +import Data.Nat as Nat +import Data.Fin as Fin + +data Gate : ℕ → Set where + ZERO : Gate 1 + ONE : Gate 1 + ID : Gate 2 + NOT : Gate 2 + AND : Gate 3 + OR : Gate 3 + XOR : Gate 3 + NAND : Gate 3 + NOR : Gate 3 + XNOR : Gate 3 + +cast-gate : {e e′ : ℕ} → .(e ≡ e′) → Gate e → Gate e′ +cast-gate {1} {1} eq g = g +cast-gate {2} {2} eq g = g +cast-gate {3} {3} eq g = g + +cast-gate-trans + : {m n o : ℕ} + → .(eq₁ : m ≡ n) + .(eq₂ : n ≡ o) + (g : Gate m) + → cast-gate eq₂ (cast-gate eq₁ g) ≡ cast-gate (trans eq₁ eq₂) g +cast-gate-trans {1} {1} {1} eq₁ eq₂ g = refl +cast-gate-trans {2} {2} {2} eq₁ eq₂ g = refl +cast-gate-trans {3} {3} {3} eq₁ eq₂ g = refl + +cast-gate-is-id : {m : ℕ} .(eq : m ≡ m) (g : Gate m) → cast-gate eq g ≡ g +cast-gate-is-id {1} eq g = refl +cast-gate-is-id {2} eq g = refl +cast-gate-is-id {3} eq g = refl + +subst-is-cast-gate : {m n : ℕ} (eq : m ≡ n) (g : Gate m) → subst Gate eq g ≡ cast-gate eq g +subst-is-cast-gate refl g = sym (cast-gate-is-id refl g) + +GateCastable : Castable +GateCastable = record + { B = Gate + ; isCastable = record + { cast = cast-gate + ; cast-trans = cast-gate-trans + ; cast-is-id = cast-gate-is-id + ; subst-is-cast = subst-is-cast-gate + } + } + +showGate : (n : ℕ) → Gate n → String +showGate _ ZERO = "ZERO" +showGate _ ONE = "ONE" +showGate _ ID = "ID" +showGate _ NOT = "NOT" +showGate _ AND = "AND" +showGate _ OR = "OR" +showGate _ XOR = "XOR" +showGate _ NAND = "NAND" +showGate _ NOR = "NOR" +showGate _ XNOR = "XNOR" + +toℕ : (n : ℕ) → Gate n → ℕ +toℕ 1 ZERO = 0 +toℕ 1 ONE = 1 +toℕ 2 ID = 0 +toℕ 2 NOT = 1 +toℕ 3 AND = 0 +toℕ 3 OR = 1 +toℕ 3 XOR = 2 +toℕ 3 NAND = 3 +toℕ 3 NOR = 4 +toℕ 3 XNOR = 5 + +toℕ-injective : {n : ℕ} {x y : Gate n} → toℕ n x ≡ toℕ n y → x ≡ y +toℕ-injective {1} {ZERO} {ZERO} refl = refl +toℕ-injective {1} {ONE} {ONE} refl = refl +toℕ-injective {2} {ID} {ID} refl = refl +toℕ-injective {2} {NOT} {NOT} refl = refl +toℕ-injective {3} {AND} {AND} refl = refl +toℕ-injective {3} {OR} {OR} refl = refl +toℕ-injective {3} {XOR} {XOR} refl = refl +toℕ-injective {3} {NAND} {NAND} refl = refl +toℕ-injective {3} {NOR} {NOR} refl = refl +toℕ-injective {3} {XNOR} {XNOR} refl = refl + +open import Relation.Binary using (Rel; Decidable; DecidableEquality) +import Relation.Nullary.Decidable as Dec + +_[_≤_] : (n : ℕ) → Rel (Gate n) 0ℓ +_[_≤_] n x y = toℕ n x ≤ toℕ n y + +_≟_ : {n : ℕ} → DecidableEquality (Gate n) +_≟_ {n} x y = Dec.map′ toℕ-injective (cong (toℕ n)) (toℕ n x Nat.≟ toℕ n y) + +_≤?_ : {n : ℕ} → Decidable (n [_≤_]) +_≤?_ {n} x y = toℕ n x Nat.≤? toℕ n y + +GateLabel : HypergraphLabel +GateLabel = record + { Label = Gate + ; showLabel = showGate + ; isCastable = record + { cast = cast-gate + ; cast-trans = cast-gate-trans + ; cast-is-id = cast-gate-is-id + ; subst-is-cast = subst-is-cast-gate + } + ; _[_≤_] = λ n x y → toℕ n x ≤ toℕ n y + ; isDecTotalOrder = λ n → record + { isTotalOrder = record + { isPartialOrder = record + { isPreorder = record + { isEquivalence = isEquivalence + ; reflexive = λ { refl → ≤-refl } + ; trans = ≤-trans + } + ; antisym = λ i≤j j≤i → toℕ-injective (≤-antisym i≤j j≤i) + } + ; total = λ { x y → ≤-total (toℕ n x) (toℕ n y) } + } + ; _≟_ = _≟_ + ; _≤?_ = _≤?_ + } + } diff --git a/Data/Circuit/Typecheck.agda b/Data/Circuit/Typecheck.agda new file mode 100644 index 0000000..bb7e23c --- /dev/null +++ b/Data/Circuit/Typecheck.agda @@ -0,0 +1,78 @@ +{-# OPTIONS --without-K --safe #-} + +module Data.Circuit.Typecheck where + +open import Data.SExp using (SExp) +open import Data.Hypergraph.Base using (HypergraphLabel; module Edge; module HypergraphList) +open import Data.Circuit.Gate using (GateLabel; Gate) +open Edge GateLabel using (Edge) +open HypergraphList GateLabel using (Hypergraph) + +open import Data.List using (List; length) renaming (map to mapL) +open import Data.List.Effectful using () renaming (module TraversableA to ListTraversable) +open import Data.Maybe using (Maybe) renaming (map to mapM) +open import Data.Nat using (ℕ; _ Date: Wed, 9 Jul 2025 13:48:15 -0500 Subject: Fix broken import --- Data/Circuit/Gate.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Data/Circuit') diff --git a/Data/Circuit/Gate.agda b/Data/Circuit/Gate.agda index 915ee8b..8ce7e0a 100644 --- a/Data/Circuit/Gate.agda +++ b/Data/Circuit/Gate.agda @@ -4,7 +4,7 @@ module Data.Circuit.Gate where open import Level using (0ℓ) open import Data.Castable using (Castable) -open import Data.Hypergraph.Base using (HypergraphLabel; module Edge; module HypergraphList) +open import Data.Hypergraph.Label using (HypergraphLabel) open import Data.String using (String) open import Data.Nat.Base using (ℕ; _≤_) open import Data.Nat.Properties using (≤-refl; ≤-trans; ≤-antisym; ≤-total) -- cgit v1.2.3 From 44a665ee5bb2659be2147881e2e0e869570429cf Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Fri, 18 Jul 2025 17:46:01 -0500 Subject: Fix imports --- Data/Circuit/Typecheck.agda | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'Data/Circuit') diff --git a/Data/Circuit/Typecheck.agda b/Data/Circuit/Typecheck.agda index bb7e23c..e34ea44 100644 --- a/Data/Circuit/Typecheck.agda +++ b/Data/Circuit/Typecheck.agda @@ -3,10 +3,10 @@ module Data.Circuit.Typecheck where open import Data.SExp using (SExp) -open import Data.Hypergraph.Base using (HypergraphLabel; module Edge; module HypergraphList) open import Data.Circuit.Gate using (GateLabel; Gate) -open Edge GateLabel using (Edge) -open HypergraphList GateLabel using (Hypergraph) +open import Data.Hypergraph.Label using (HypergraphLabel) +open import Data.Hypergraph.Edge GateLabel using (Edge) +open import Data.Hypergraph.Base GateLabel using (Hypergraph) open import Data.List using (List; length) renaming (map to mapL) open import Data.List.Effectful using () renaming (module TraversableA to ListTraversable) -- cgit v1.2.3 From 4c4ca752bcbc900b3ffa30602c955728778dc9a1 Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Sat, 19 Jul 2025 01:36:42 -0500 Subject: Show equivalence of old and new Hypergraph setoids --- Data/Circuit/Convert.agda | 197 ++++++++++++++++++++++++++++++++++++++++++++++ Data/Permutation.agda | 5 +- 2 files changed, 199 insertions(+), 3 deletions(-) create mode 100644 Data/Circuit/Convert.agda (limited to 'Data/Circuit') diff --git a/Data/Circuit/Convert.agda b/Data/Circuit/Convert.agda new file mode 100644 index 0000000..497b0cd --- /dev/null +++ b/Data/Circuit/Convert.agda @@ -0,0 +1,197 @@ +{-# OPTIONS --without-K --safe #-} + +module Data.Circuit.Convert where + +open import Data.Nat.Base using (ℕ) +open import Data.Circuit.Gate using (Gate; GateLabel; cast-gate; cast-gate-is-id; subst-is-cast-gate) +open import Data.Fin.Base using (Fin) +open import Function.Bundles using (Equivalence) +open import Data.Hypergraph.Edge GateLabel using (Edge) +open import Data.Hypergraph.Base GateLabel using (Hypergraph; sortHypergraph) +open import Data.Hypergraph.Setoid GateLabel using (Hypergraph-Setoid; ≈-Hypergraph) +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.Base using (_∘_; id; _$_) + +import DecorationFunctor.Hypergraph.Labeled 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 + { 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 + +from : {v : ℕ} → Hypergraph′ v → Hypergraph v +from {v} H = record + { edges = toList asEdge + } + where + open Hypergraph′ H + asEdge : Fin h → Edge v + asEdge e = record { label = l e ; ports = toVec (j e) } + +open import Data.Product.Base using (proj₁; proj₂) +open import Data.Fin.Permutation using (flip) +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_) +to-cong : {v : ℕ} {H H′ : Hypergraph v} → ≈-Hypergraph H H′ → Hypergraph-same (to H) (to H′) +to-cong {v} {H} {H′} ≈H = record + { ↔h = flip ρ + ; ≗a = ≗a + ; ≗j = ≗j + ; ≗l = ≗l + } + where + open Edge using (arity; ports; label) + open import Data.List.Relation.Binary.Permutation.Propositional using (_↭_) + open import Function.Bundles using (_↔_) + open ≈-Hypergraph ≈H + open import Data.Fin.Permutation using (_⟨$⟩ʳ_; _⟨$⟩ˡ_; Permutation′; inverseʳ) + open import Data.Fin.Base using (cast) + open import Data.Fin.Properties using (cast-is-id) + ρ : Fin (length H′.edges) ↔ Fin (length H.edges) + ρ = proj₁ (fromList-↭ ↭edges) + + open ≡.≡-Reasoning + edges≗ρ∘edges′ : (i : Fin (length H.edges)) → fromList H.edges i ≡ fromList H′.edges (ρ ⟨$⟩ˡ i) + edges≗ρ∘edges′ i = begin + fromList H.edges i ≡⟨ ≡.cong (fromList H.edges) (inverseʳ ρ) ⟨ + fromList H.edges (ρ ⟨$⟩ʳ (ρ ⟨$⟩ˡ i)) ≡⟨ proj₂ (fromList-↭ ↭edges) (ρ ⟨$⟩ˡ i) ⟩ + fromList H′.edges (ρ ⟨$⟩ˡ i) ∎ + + ≗a : (e : Fin (Hypergraph′.h (to H))) + → Hypergraph′.a (to H) e + ≡ arity (fromList H′.edges (ρ ⟨$⟩ˡ e)) + ≗a = ≡.cong arity ∘ edges≗ρ∘edges′ + + ≗j : (e : Fin (Hypergraph′.h (to H))) + (i : Fin (Hypergraph′.a (to H) e)) + → fromVec (ports (fromList H.edges e)) i + ≡ fromVec (ports (fromList H′.edges (ρ ⟨$⟩ˡ e))) (cast (≗a e) i) + ≗j e i + rewrite edges≗ρ∘edges′ e + rewrite cast-is-id ≡.refl i = ≡.refl + + ≗l : (e : Fin (Hypergraph′.h (to H))) + → label (fromList H.edges e) + ≡ cast-gate (≡.sym (≗a e)) (label (fromList H′.edges (ρ ⟨$⟩ˡ e))) + ≗l e + rewrite edges≗ρ∘edges′ e + rewrite cast-gate-is-id ≡.refl (label (fromList H′.edges (ρ ⟨$⟩ˡ e))) = + ≡.refl + +module _ {v : ℕ} where + open import Data.Hypergraph.Edge GateLabel using (decTotalOrder; ≈-Edge; ≈-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.Permutation.Propositional using (_↭_) + open import Data.Vec.Functional.Relation.Binary.Permutation using () renaming (_↭_ to _↭′_) + 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 GateLabel using (isCastable) + open import Data.Castable using (IsCastable) + open IsCastable isCastable using (≈-reflexive; ≈-sym; ≈-trans) + from-cong + : {H H′ : Hypergraph′ v} + → Hypergraph-same H H′ + → ≈-Hypergraph (from H) (from H′) + from-cong {H} {H′} ≈H = record + { ≡sorted = ≡sorted + } + 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 e = record { label = l H e ; ports = toVec (j H e) } + + to-from : (e : Fin H′.h) → t (f e) ≡ e + to-from e = inverseˡ ≡.refl + + a∘to-from : (e : Fin H′.h) → H′.a (t (f e)) ≡ H′.a e + a∘to-from = ≡.cong H′.a ∘ to-from + + ≗a′ : (e : Fin H′.h) → H.a (f e) ≡ H′.a e + ≗a′ e = ≡.trans (≗a (f e)) (a∘to-from e) + + l≗ : (e : Fin H.h) → cast-gate (≗a e) (H.l e) ≡ H′.l (t e) + l≗ e = ≈-sym (≡.sym (≗l e)) + + l∘to-from : (e : Fin H′.h) → cast-gate (a∘to-from e) (H′.l (t (f e))) ≡ H′.l e + l∘to-from e rewrite to-from e = ≈-reflexive ≡.refl + + ≗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 + ≡ H′.j e (fincast (a∘to-from e) i) + j∘to-from e i rewrite to-from e = ≡.cong (H′.j e) (≡.sym (fincast-is-id ≡.refl i)) + + open ≡.≡-Reasoning + + ≗j′ : (e : Fin H′.h) (i : Fin (H.a (f e))) → H.j (f e) i ≡ H′.j e (fincast (≗a′ e) i) + ≗j′ e i = begin + H.j (f e) i ≡⟨ ≗j (f e) i ⟩ + H′.j (t (f e)) (fincast _ i) ≡⟨ j∘to-from e (fincast _ i) ⟩ + H′.j e (fincast (a∘to-from e) (fincast _ i)) ≡⟨ ≡.cong (H′.j e) (fincast-trans (≗a (f e)) _ i) ⟩ + H′.j e (fincast (≗a′ e) i) ∎ + + cast-toVec + : {n m : ℕ} + {A : Set} + (m≡n : m ≡ n) + (f : Fin n → A) + → 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)) ⟩ + 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 ⟨ + toVec f ∎ + + ≗p′ : (e : Fin H′.h) → 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) ⟩ + toVec (H′.j e) ∎ + + H∘ρ≗H′ : (e : Fin H′.h) → asEdge H (flip ↔h Data.Fin.Permutation.⟨$⟩ʳ e) ≡ asEdge H′ e + H∘ρ≗H′ e = ≈-Edge⇒≡ record + { ≡arity = ≗a′ e + ; ≡label = ≗l′ e + ; ≡ports = ≗p′ e + } + + ≡sorted : sortHypergraph (from H) ≡ sortHypergraph (from H′) + ≡sorted = + ≡.cong (λ x → record { edges = x } ) $ + Pointwise-≡⇒≡ $ + map ≈-Edge⇒≡ $ + sorted-≋ $ + toList-↭ $ + flip ↔h , H∘ρ≗H′ + +equiv : (v : ℕ) → Equivalence (Hypergraph-Setoid v) (Hypergraph-Setoid′ v) +equiv v = record + { to = to + ; from = from + ; to-cong = to-cong + ; from-cong = from-cong + } diff --git a/Data/Permutation.agda b/Data/Permutation.agda index 2413a0d..55c8748 100644 --- a/Data/Permutation.agda +++ b/Data/Permutation.agda @@ -2,7 +2,7 @@ open import Level using (Level) -module Data.Permutation {ℓ : Level} (A : Set ℓ) where +module Data.Permutation {ℓ : Level} {A : Set ℓ} where import Data.Fin as Fin import Data.Fin.Properties as FinProp @@ -39,8 +39,7 @@ module _ where -- convert a List permutation to a Vector permutation fromList-↭ - : {A : Set} - {xs ys : List A} + : {xs ys : List A} → xs ↭ ys → fromList xs ↭′ fromList ys fromList-↭ refl = ↭-refl -- cgit v1.2.3 From 21aa7526f51030be9ffd86be2eabd5d07f64b6f4 Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Wed, 15 Oct 2025 13:31:13 -0500 Subject: Strengthen permutation sort theorem --- Data/Circuit/Convert.agda | 42 +++++++++++++++++--------------- Data/Hypergraph/Base.agda | 1 + Data/Hypergraph/Edge.agda | 14 +++++++---- Data/Permutation/Sort.agda | 60 ++++++++++++++++++++++++++++++---------------- 4 files changed, 73 insertions(+), 44 deletions(-) (limited to 'Data/Circuit') diff --git a/Data/Circuit/Convert.agda b/Data/Circuit/Convert.agda index 497b0cd..ce6de69 100644 --- a/Data/Circuit/Convert.agda +++ b/Data/Circuit/Convert.agda @@ -5,16 +5,24 @@ module Data.Circuit.Convert where open import Data.Nat.Base using (ℕ) open import Data.Circuit.Gate using (Gate; GateLabel; cast-gate; cast-gate-is-id; subst-is-cast-gate) open import Data.Fin.Base using (Fin) -open import Function.Bundles using (Equivalence) open import Data.Hypergraph.Edge GateLabel using (Edge) -open import Data.Hypergraph.Base GateLabel using (Hypergraph; sortHypergraph) +open import Data.Hypergraph.Base GateLabel using (Hypergraph; sortHypergraph; mkHypergraph) open import Data.Hypergraph.Setoid GateLabel using (Hypergraph-Setoid; ≈-Hypergraph) 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.Base using (_∘_; id; _$_) - +open import Function.Bundles using (Equivalence; _↔_) +open import Function.Base using (_∘_; 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 as LabeledHypergraph + open LabeledHypergraph using (Hypergraph-same) renaming (Hypergraph to Hypergraph′; Hypergraph-setoid to Hypergraph-Setoid′) to : {v : ℕ} → Hypergraph v → Hypergraph′ v @@ -37,9 +45,6 @@ from {v} H = record asEdge : Fin h → Edge v asEdge e = record { label = l e ; ports = toVec (j e) } -open import Data.Product.Base using (proj₁; proj₂) -open import Data.Fin.Permutation using (flip) -open import Relation.Binary.PropositionalEquality as ≡ using (_≡_) to-cong : {v : ℕ} {H H′ : Hypergraph v} → ≈-Hypergraph H H′ → Hypergraph-same (to H) (to H′) to-cong {v} {H} {H′} ≈H = record { ↔h = flip ρ @@ -49,8 +54,6 @@ to-cong {v} {H} {H′} ≈H = record } where open Edge using (arity; ports; label) - open import Data.List.Relation.Binary.Permutation.Propositional using (_↭_) - open import Function.Bundles using (_↔_) open ≈-Hypergraph ≈H open import Data.Fin.Permutation using (_⟨$⟩ʳ_; _⟨$⟩ˡ_; Permutation′; inverseʳ) open import Data.Fin.Base using (cast) @@ -87,11 +90,9 @@ to-cong {v} {H} {H′} ≈H = record ≡.refl module _ {v : ℕ} where - open import Data.Hypergraph.Edge GateLabel using (decTotalOrder; ≈-Edge; ≈-Edge⇒≡) + open import Data.Hypergraph.Edge GateLabel 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.Permutation.Propositional using (_↭_) - open import Data.Vec.Functional.Relation.Binary.Permutation using () renaming (_↭_ to _↭′_) open import Data.List.Relation.Binary.Pointwise using (Pointwise; Pointwise-≡⇒≡; map) open import Data.Product.Base using (_,_) open import Data.Hypergraph.Label using (HypergraphLabel) @@ -172,21 +173,24 @@ module _ {v : ℕ} where 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 (flip ↔h Data.Fin.Permutation.⟨$⟩ʳ e) ≡ asEdge H′ e + H∘ρ≗H′ : (e : Fin H′.h) → asEdge H (↔h ⟨$⟩ˡ e) ≡ asEdge H′ e H∘ρ≗H′ e = ≈-Edge⇒≡ record { ≡arity = ≗a′ e ; ≡label = ≗l′ e ; ≡ports = ≗p′ e } + open Hypergraph using (edges) + open →-Reasoning ≡sorted : sortHypergraph (from H) ≡ sortHypergraph (from H′) ≡sorted = - ≡.cong (λ x → record { edges = x } ) $ - Pointwise-≡⇒≡ $ - map ≈-Edge⇒≡ $ - sorted-≋ $ - toList-↭ $ - flip ↔h , H∘ρ≗H′ + 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 ∶ sortHypergraph (from H) ≡ sortHypergraph (from H′) equiv : (v : ℕ) → Equivalence (Hypergraph-Setoid v) (Hypergraph-Setoid′ v) equiv v = record diff --git a/Data/Hypergraph/Base.agda b/Data/Hypergraph/Base.agda index 5cf5388..6988cf0 100644 --- a/Data/Hypergraph/Base.agda +++ b/Data/Hypergraph/Base.agda @@ -12,6 +12,7 @@ open import Data.String using (String; unlines) import Data.List.Sort as Sort record Hypergraph (v : ℕ) : Set where + constructor mkHypergraph field edges : List (Edge v) diff --git a/Data/Hypergraph/Edge.agda b/Data/Hypergraph/Edge.agda index cbf61e6..13b9278 100644 --- a/Data/Hypergraph/Edge.agda +++ b/Data/Hypergraph/Edge.agda @@ -80,6 +80,14 @@ record ≈-Edge {n : ℕ} (E E′ : Edge n) : Set where module i≈j = ≈-Edge i≈j module j≈k = ≈-Edge j≈k +open import Relation.Binary using (IsEquivalence) +≈-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}) @@ -300,11 +308,7 @@ tri x y | tri> x≮y x≢y y ¬x