From 02a7c2e196435b6b60a1164ff75a805685d2d151 Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Thu, 19 Jun 2025 20:11:18 -0500 Subject: Add new hypergraph definitions --- Data/Castable.agda | 24 +++++++++++++++++++++ Data/Hypergraph/Base.agda | 55 +++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 79 insertions(+) create mode 100644 Data/Castable.agda create mode 100644 Data/Hypergraph/Base.agda (limited to 'Data') diff --git a/Data/Castable.agda b/Data/Castable.agda new file mode 100644 index 0000000..2c6932e --- /dev/null +++ b/Data/Castable.agda @@ -0,0 +1,24 @@ +{-# OPTIONS --without-K --safe #-} + +module Data.Castable where + +open import Level using (Level; suc; _⊔_) +open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; sym; trans; subst) + +record IsCastable {ℓ₁ ℓ₂ : Level} {A : Set ℓ₁} (B : A → Set ℓ₂) : Set (ℓ₁ ⊔ ℓ₂) where + + field + cast : {e e′ : A} → .(e ≡ e′) → B e → B e′ + cast-trans + : {m n o : A} + → .(eq₁ : m ≡ n) + .(eq₂ : n ≡ o) + (x : B m) + → cast eq₂ (cast eq₁ x) ≡ cast (trans eq₁ eq₂) x + cast-is-id : {m : A} .(eq : m ≡ m) (x : B m) → cast eq x ≡ x + subst-is-cast : {m n : A} (eq : m ≡ n) (x : B m) → subst B eq x ≡ cast eq x + +record Castable {ℓ₁ ℓ₂ : Level} {A : Set ℓ₁} : Set (suc (ℓ₁ ⊔ ℓ₂)) where + field + B : A → Set ℓ₂ + isCastable : IsCastable B diff --git a/Data/Hypergraph/Base.agda b/Data/Hypergraph/Base.agda new file mode 100644 index 0000000..a2157fb --- /dev/null +++ b/Data/Hypergraph/Base.agda @@ -0,0 +1,55 @@ +{-# OPTIONS --without-K --safe #-} + +module Data.Hypergraph.Base where + +open import Data.Castable using (IsCastable) +open import Data.Nat.Base using (ℕ) +open import Data.Fin using (Fin) + +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; _⊔_) + +record HypergraphLabel {ℓ : Level} : Set (suc ℓ) where + field + Label : ℕ → Set ℓ + isCastable : IsCastable Label + _[_≈_] : (n : ℕ) → Rel (Label n) ℓ + _[_≤_] : (n : ℕ) → Rel (Label n) ℓ + decTotalOrder : (n : ℕ) → IsDecTotalOrder (n [_≈_]) (n [_≤_]) + open IsCastable isCastable public + +module Edge (HL : HypergraphLabel) where + + open HypergraphLabel HL using (Label; cast) + open VecBase using (Vec) + + record Edge (v : ℕ) : Set where + field + {arity} : ℕ + label : Label arity + ports : Vec (Fin v) arity + + 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 + +module HypergraphList (HL : HypergraphLabel) where + + open import Data.List.Base using (List) + open Edge HL using (Edge) + + record Hypergraph (v : ℕ) : Set where + field + edges : List (Edge v) -- cgit v1.2.3 From 6831517a4a8358415e5664b974000620b2581c3f Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Tue, 1 Jul 2025 23:09:57 -0500 Subject: Begin strict total order for hypergraph edges --- Data/Castable.agda | 28 +++++++- Data/Hypergraph/Base.agda | 179 +++++++++++++++++++++++++++++++++++++++++++--- 2 files changed, 198 insertions(+), 9 deletions(-) (limited to 'Data') diff --git a/Data/Castable.agda b/Data/Castable.agda index 2c6932e..4f85b3d 100644 --- a/Data/Castable.agda +++ b/Data/Castable.agda @@ -3,7 +3,8 @@ module Data.Castable where open import Level using (Level; suc; _⊔_) -open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; sym; trans; subst) +open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; subst; cong; module ≡-Reasoning) +open import Relation.Binary using (Sym; Trans; _⇒_) record IsCastable {ℓ₁ ℓ₂ : Level} {A : Set ℓ₁} (B : A → Set ℓ₂) : Set (ℓ₁ ⊔ ℓ₂) where @@ -18,6 +19,31 @@ record IsCastable {ℓ₁ ℓ₂ : Level} {A : Set ℓ₁} (B : A → Set ℓ₂ cast-is-id : {m : A} .(eq : m ≡ m) (x : B m) → cast eq x ≡ x subst-is-cast : {m n : A} (eq : m ≡ n) (x : B m) → subst B eq x ≡ cast eq x + infix 3 _≈[_]_ + _≈[_]_ : {n m : A} → B n → .(eq : n ≡ m) → B m → Set ℓ₂ + _≈[_]_ x eq y = cast eq x ≡ y + + ≈-reflexive : {n : A} → _≡_ ⇒ (λ xs ys → _≈[_]_ {n} xs refl ys) + ≈-reflexive {n} {x} {y} eq = trans (cast-is-id refl x) eq + + ≈-sym : {m n : A} .{m≡n : m ≡ n} → Sym _≈[ m≡n ]_ _≈[ sym m≡n ]_ + ≈-sym {m} {n} {m≡n} {x} {y} x≡y = begin + cast (sym m≡n) y ≡⟨ cong (cast (sym m≡n)) x≡y ⟨ + cast (sym m≡n) (cast m≡n x) ≡⟨ cast-trans m≡n (sym m≡n) x ⟩ + cast (trans m≡n (sym m≡n)) x ≡⟨ cast-is-id (trans m≡n (sym m≡n)) x ⟩ + x ∎ + where + open ≡-Reasoning + + ≈-trans : {m n o : A} .{m≡n : m ≡ n} .{n≡o : n ≡ o} → Trans _≈[ m≡n ]_ _≈[ n≡o ]_ _≈[ trans m≡n n≡o ]_ + ≈-trans {m} {n} {o} {m≡n} {n≡o} {x} {y} {z} x≡y y≡z = begin + cast (trans m≡n n≡o) x ≡⟨ cast-trans m≡n n≡o x ⟨ + cast n≡o (cast m≡n x) ≡⟨ cong (cast n≡o) x≡y ⟩ + cast n≡o y ≡⟨ y≡z ⟩ + z ∎ + where + open ≡-Reasoning + record Castable {ℓ₁ ℓ₂ : Level} {A : Set ℓ₁} : Set (suc (ℓ₁ ⊔ ℓ₂)) where field B : A → Set ℓ₂ 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 x≮y′ x≢y y + ¬x x≮y x≢y y ¬x Date: Thu, 3 Jul 2025 11:55:43 -0500 Subject: Finish strict total order for hypergraph edges --- Data/Hypergraph/Base.agda | 178 ++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 173 insertions(+), 5 deletions(-) (limited to 'Data') diff --git a/Data/Hypergraph/Base.agda b/Data/Hypergraph/Base.agda index f54468d..0771a78 100644 --- a/Data/Hypergraph/Base.agda +++ b/Data/Hypergraph/Base.agda @@ -17,20 +17,31 @@ open import Relation.Binary ; _Respects_ ) open import Relation.Binary.Bundles using (DecTotalOrder; StrictTotalOrder) +open import Relation.Binary.Structures using (IsEquivalence) 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; _⊔_) +open import Level using (Level; suc; _⊔_; 0ℓ) +open import Data.String using (String; _<+>_; unlines) +open import Data.Fin.Show using () renaming (show to showFin) +open import Data.List.Show using () renaming (show to showList) +open import Data.List.Base using (map) +open import Data.Vec.Show using () renaming (show to showVec) +import Data.Fin.Base as Fin +import Data.Fin.Properties as FinProp import Data.Vec.Base as VecBase 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 record HypergraphLabel {ℓ : Level} : Set (suc ℓ) where field Label : ℕ → Set ℓ + showLabel : (n : ℕ) → Label n → String isCastable : IsCastable Label -- _[_≈_] : (n : ℕ) → Rel (Label n) ℓ _[_≤_] : (n : ℕ) → Rel (Label n) ℓ @@ -105,6 +116,8 @@ module Edge (HL : HypergraphLabel) where module j≈k = ≈-Edge j≈k 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} @@ -115,19 +128,46 @@ module Edge (HL : HypergraphLabel) where (≡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) + → VecBase.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 x≮y″ x≢y y + ¬x x≮y′ x≢y y ¬x x≮y x≢y y ¬x showVec showFin p + module HypergraphList (HL : HypergraphLabel) where open import Data.List.Base using (List) @@ -216,3 +375,12 @@ module HypergraphList (HL : HypergraphLabel) where record Hypergraph (v : ℕ) : Set where field edges : List (Edge v) + + sortHypergraph : {v : ℕ} → Hypergraph v → Hypergraph v + sortHypergraph {v} H = record { edges = sort edges } + where + open Hypergraph H + open import Data.List.Sort.MergeSort (Edge.decTotalOrder HL) using (sort) + + showHypergraph : {v : ℕ} → Hypergraph v → String + showHypergraph record { edges = e} = unlines (map (Edge.showEdge HL) e) -- cgit v1.2.3 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 +++++++++++++++++++++++++ Data/SExp.agda | 75 ++++++++++++++++++++++++ Data/SExp/Parser.agda | 73 +++++++++++++++++++++++ 4 files changed, 363 insertions(+) create mode 100644 Data/Circuit/Gate.agda create mode 100644 Data/Circuit/Typecheck.agda create mode 100644 Data/SExp.agda create mode 100644 Data/SExp/Parser.agda (limited to 'Data') 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 (ℕ; __) + +open List + +module ListBased where + + data SExp : Set where + Atom : String → SExp + Nat : ℕ → SExp + SExps : List SExp → SExp + + mutual + showSExp : SExp → String + showSExp (Atom s) = s + showSExp (Nat n) = showNat n + showSExp (SExps xs) = parens (intersperse " " (showList xs)) + + -- expanded out map for termination checker + showList : List SExp → List String + showList [] = [] + showList (x ∷ xs) = showSExp x ∷ showList xs + +module PairBased where + + data SExp : Set where + Atom : String → SExp + Nat : ℕ → SExp + Nil : SExp + Pair : SExp → SExp → SExp + + mutual + showSExp : SExp → String + showSExp (Atom s) = s + showSExp (Nat n) = showNat n + showSExp Nil = "()" + showSExp (Pair l r) = parens (showPair l r) + + showPair : SExp → SExp → String + showPair x (Atom s) = showSExp x <+> "." <+> s + showPair x (Nat n) = showSExp x <+> "." <+> showNat n + showPair x Nil = showSExp x + showPair x (Pair l r) = showSExp x <+> showPair l r + +open ListBased public +open PairBased + +mutual + sexpL→sexpP : ListBased.SExp → PairBased.SExp + sexpL→sexpP (Atom s) = Atom s + sexpL→sexpP (Nat n) = Nat n + sexpL→sexpP (SExps xs) = [sexpL]→sexpP xs + + [sexpL]→sexpP : List (ListBased.SExp) → PairBased.SExp + [sexpL]→sexpP [] = Nil + [sexpL]→sexpP (x ∷ xs) = Pair (sexpL→sexpP x) ([sexpL]→sexpP xs) + +mutual + sexpP→sexpL : PairBased.SExp → ListBased.SExp + sexpP→sexpL (Atom s) = Atom s + sexpP→sexpL (Nat n) = Nat n + sexpP→sexpL Nil = SExps [] + sexpP→sexpL (Pair x y) = SExps (sexpP→sexpL x ∷ sexpP→[sexpL] y) + + sexpP→[sexpL] : PairBased.SExp → List (ListBased.SExp) + sexpP→[sexpL] (Atom _) = [] + sexpP→[sexpL] (Nat _) = [] + sexpP→[sexpL] Nil = [] + sexpP→[sexpL] (Pair x y) = sexpP→sexpL x ∷ sexpP→[sexpL] y diff --git a/Data/SExp/Parser.agda b/Data/SExp/Parser.agda new file mode 100644 index 0000000..ec1b6a5 --- /dev/null +++ b/Data/SExp/Parser.agda @@ -0,0 +1,73 @@ +{-# OPTIONS --without-K --guardedness --safe #-} + +open import Text.Parser.Types.Core using (Parameters) + +module Data.SExp.Parser {l} {P : Parameters l} where + +import Data.String.Base as String +open import Data.List as List using (List) + +open import Data.Char.Base using (Char) +open import Data.List.Sized.Interface using (Sized) +open import Data.List.NonEmpty as List⁺ using (List⁺) renaming (map to map⁺) +open import Data.Subset using (Subset; into) +open import Effect.Monad using (RawMonadPlus) +open import Function.Base using (_∘_; _$_) +open import Induction.Nat.Strong using (fix; map; □_) +open import Relation.Binary.PropositionalEquality.Decidable using (DecidableEquality) +open import Relation.Unary using (IUniversal; _⇒_) +open import Level.Bounded using (theSet; [_]) +open import Text.Parser.Types P using (Parser) +open import Text.Parser.Combinators {P = P} using (_<$>_; list⁺; _<|>_; _<$_; _<&_; _<&?_; box) +open import Text.Parser.Combinators.Char {P = P} using (alpha; parens; withSpaces; spaces; char) +open import Text.Parser.Combinators.Numbers {P = P} using (decimalℕ) + +open import Data.SExp using (SExp) +open SExp + +open Parameters P using (M; Tok; Toks) + +module _ + {{𝕄 : RawMonadPlus M}} + {{𝕊 : Sized Tok Toks}} + {{𝔻 : DecidableEquality (theSet Tok)}} + {{ℂ : Subset Char (theSet Tok)}} + {{ℂ⁻ : Subset (theSet Tok) Char}} + where + + -- An atom is just a non-empty list of alphabetical characters. + -- We use `<$>` to turn that back into a string and apply the `Atom` constructor. + atom : ∀[ Parser [ SExp ] ] + atom = Atom ∘ String.fromList⁺ ∘ map⁺ (into ℂ⁻) <$> list⁺ alpha + + -- Natural number parser + nat : ∀[ Parser [ SExp ] ] + nat = Nat <$> decimalℕ + + -- Empty list parser + nil : ∀[ Parser [ SExp ] ] + nil = SExps List.[] <$ char '(' <&? box spaces <& box (char ')') + + -- Parser for a list of S-Expressions + list : ∀[ Parser [ SExp ] ⇒ Parser [ List SExp ] ] + list sexp = List⁺.toList <$> list⁺ (withSpaces sexp) + + -- Compound S-Expression parser + compound : ∀[ □ Parser [ SExp ] ⇒ Parser [ SExp ] ] + compound rec = nil <|> SExps <$> parens (map list rec) + + -- S-Expression parser + sexp : ∀[ □ Parser [ SExp ] ⇒ Parser [ SExp ] ] + sexp rec = atom <|> nat <|> compound rec + + -- Build the parser as a fixpoint since SExp is an inductive type + sexp-top : ∀[ Parser [ SExp ] ] + sexp-top = fix (Parser [ SExp ]) sexp + + -- Top-level parser for list of S-Expressions + LIST : ∀[ Parser [ SExp ] ] + LIST = SExps <$> list sexp-top + + -- Top-level S-Expression parser + SEXP : ∀[ Parser [ SExp ] ] + SEXP = withSpaces sexp-top -- cgit v1.2.3 From ee5c56a58154840f08a18d581983d6f6f3630970 Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Wed, 9 Jul 2025 12:15:51 -0500 Subject: Split hypergraph label and edge into separate files --- Data/Hypergraph/Base.agda | 393 ++------------------------------------------- Data/Hypergraph/Edge.agda | 326 +++++++++++++++++++++++++++++++++++++ Data/Hypergraph/Label.agda | 36 +++++ 3 files changed, 378 insertions(+), 377 deletions(-) create mode 100644 Data/Hypergraph/Edge.agda create mode 100644 Data/Hypergraph/Label.agda (limited to 'Data') diff --git a/Data/Hypergraph/Base.agda b/Data/Hypergraph/Base.agda index 0771a78..e43cbce 100644 --- a/Data/Hypergraph/Base.agda +++ b/Data/Hypergraph/Base.agda @@ -1,386 +1,25 @@ {-# OPTIONS --without-K --safe #-} -module Data.Hypergraph.Base where +open import Data.Hypergraph.Label using (HypergraphLabel) -open import Data.Castable using (IsCastable) -open import Data.Fin using (Fin) +module Data.Hypergraph.Base (HL : HypergraphLabel) where -open import Relation.Binary - using - ( Rel - ; IsDecTotalOrder - ; IsStrictTotalOrder - ; Tri - ; Trichotomous - ; _Respectsˡ_ - ; _Respectsʳ_ - ; _Respects_ - ) -open import Relation.Binary.Bundles using (DecTotalOrder; StrictTotalOrder) -open import Relation.Binary.Structures using (IsEquivalence) -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; _⊔_; 0ℓ) -open import Data.String using (String; _<+>_; unlines) -open import Data.Fin.Show using () renaming (show to showFin) -open import Data.List.Show using () renaming (show to showList) -open import Data.List.Base using (map) -open import Data.Vec.Show using () renaming (show to showVec) +open import Data.Hypergraph.Edge HL using (Edge; decTotalOrder; showEdge) +open import Data.List.Base using (List; map) +open import Data.Nat.Base using (ℕ) +open import Data.String using (String; unlines) -import Data.Fin.Base as Fin -import Data.Fin.Properties as FinProp -import Data.Vec.Base as VecBase -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 +import Data.List.Sort.MergeSort as MergeSort -record HypergraphLabel {ℓ : Level} : Set (suc ℓ) where +record Hypergraph (v : ℕ) : Set where field - Label : ℕ → Set ℓ - showLabel : (n : ℕ) → Label n → String - isCastable : IsCastable Label - -- _[_≈_] : (n : ℕ) → Rel (Label n) ℓ - _[_≤_] : (n : ℕ) → Rel (Label n) ℓ - isDecTotalOrder : (n : ℕ) → IsDecTotalOrder ≡._≡_ (n [_≤_]) - decTotalOrder : (n : ℕ) → DecTotalOrder ℓ ℓ ℓ - decTotalOrder n = record - { Carrier = Label n - ; _≈_ = ≡._≡_ - ; _≤_ = n [_≤_] - ; isDecTotalOrder = isDecTotalOrder n - } + edges : List (Edge v) - 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 +sortHypergraph : {v : ℕ} → Hypergraph v → Hypergraph v +sortHypergraph {v} H = record { edges = sort edges } + where + open Hypergraph H + open MergeSort decTotalOrder using (sort) -module Edge (HL : HypergraphLabel) where - - module HL = HypergraphLabel HL - open HL using (Label; cast; cast-is-id; cast-trans) - open VecBase using (Vec) - - record Edge (v : ℕ) : Set where - field - {arity} : ℕ - label : Label arity - ports : Vec (Fin v) arity - - open ≡ using (_≡_) - open VecCast using (_≈[_]_) - - record ≈-Edge {n : ℕ} (E E′ : Edge n) : Set where - eta-equality - 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 - - 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) - → VecBase.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 x≮y″ x≢y y - ¬x x≮y′ x≢y y - ¬x x≮y x≢y y ¬x showVec showFin p - -module HypergraphList (HL : HypergraphLabel) where - - open import Data.List.Base using (List) - open Edge HL using (Edge) - - record Hypergraph (v : ℕ) : Set where - field - edges : List (Edge v) - - sortHypergraph : {v : ℕ} → Hypergraph v → Hypergraph v - sortHypergraph {v} H = record { edges = sort edges } - where - open Hypergraph H - open import Data.List.Sort.MergeSort (Edge.decTotalOrder HL) using (sort) - - showHypergraph : {v : ℕ} → Hypergraph v → String - showHypergraph record { edges = e} = unlines (map (Edge.showEdge HL) e) +showHypergraph : {v : ℕ} → Hypergraph v → String +showHypergraph record { edges = e} = unlines (map showEdge e) diff --git a/Data/Hypergraph/Edge.agda b/Data/Hypergraph/Edge.agda new file mode 100644 index 0000000..3c2a3a1 --- /dev/null +++ b/Data/Hypergraph/Edge.agda @@ -0,0 +1,326 @@ +{-# OPTIONS --without-K --safe #-} + +open import Data.Hypergraph.Label using (HypergraphLabel) + +module Data.Hypergraph.Edge (HL : HypergraphLabel) where + + +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.Base using (ℕ; _<_) +open import Data.Nat.Properties using (<-irrefl; <-trans; <-resp₂-≡; <-cmp) +open import Data.Product.Base using (_,_; proj₁; proj₂) +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.Bundles using (DecTotalOrder; StrictTotalOrder) +open import Relation.Binary.Structures using (IsEquivalence) +open import Relation.Nullary using (¬_) + +import Data.Fin.Base as Fin +import Data.Fin.Properties as FinProp +import Data.Vec.Base as VecBase +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 + +module HL = HypergraphLabel HL +open HL using (Label; cast; cast-is-id) +open VecBase using (Vec) + +record Edge (v : ℕ) : Set where + field + {arity} : ℕ + label : Label arity + ports : Vec (Fin v) arity + +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 + +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) + → VecBase.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 x≮y″ x≢y y + ¬x x≮y′ x≢y y + ¬x x≮y x≢y y ¬x showVec showFin p + +open module STOP′ {v} = STOP (strictTotalOrder {v}) using (decTotalOrder) public diff --git a/Data/Hypergraph/Label.agda b/Data/Hypergraph/Label.agda new file mode 100644 index 0000000..c23d33a --- /dev/null +++ b/Data/Hypergraph/Label.agda @@ -0,0 +1,36 @@ +{-# OPTIONS --without-K --safe #-} +module Data.Hypergraph.Label where + +open import Data.Castable using (IsCastable) +open import Data.Nat.Base using (ℕ) +open import Data.String using (String) +open import Level using (Level; suc) +open import Relation.Binary using (Rel; IsDecTotalOrder) +open import Relation.Binary.Bundles using (DecTotalOrder; StrictTotalOrder) +open import Relation.Binary.Properties.DecTotalOrder using (<-strictTotalOrder; _<_) +open import Relation.Binary.PropositionalEquality using (_≡_) + +record HypergraphLabel {ℓ : Level} : Set (suc ℓ) where + + field + Label : ℕ → Set ℓ + showLabel : (n : ℕ) → Label n → String + isCastable : IsCastable Label + _[_≤_] : (n : ℕ) → Rel (Label n) ℓ + isDecTotalOrder : (n : ℕ) → IsDecTotalOrder _≡_ (n [_≤_]) + + decTotalOrder : (n : ℕ) → DecTotalOrder ℓ ℓ ℓ + decTotalOrder n = record + { Carrier = Label n + ; _≈_ = _≡_ + ; _≤_ = n [_≤_] + ; isDecTotalOrder = isDecTotalOrder n + } + + _[_<_] : (n : ℕ) → Rel (Label n) ℓ + _[_<_] n = _<_ (decTotalOrder n) + + strictTotalOrder : (n : ℕ) → StrictTotalOrder ℓ ℓ ℓ + strictTotalOrder n = <-strictTotalOrder (decTotalOrder n) + + open IsCastable isCastable public -- cgit v1.2.3 From 61506ab9d74b1b9fc6f580f569fa22e84e557d54 Mon Sep 17 00:00:00 2001 From: Jacques Comeaux 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') 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 3b460f16ecc99253cb7f5bae32a3a076717fa12f Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Fri, 18 Jul 2025 15:45:08 -0500 Subject: Convert between List and Vector permutations --- Data/Permutation.agda | 218 ++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 218 insertions(+) create mode 100644 Data/Permutation.agda (limited to 'Data') diff --git a/Data/Permutation.agda b/Data/Permutation.agda new file mode 100644 index 0000000..2413a0d --- /dev/null +++ b/Data/Permutation.agda @@ -0,0 +1,218 @@ +{-# OPTIONS --without-K --safe #-} + +open import Level using (Level) + +module Data.Permutation {ℓ : Level} (A : Set ℓ) where + +import Data.Fin as Fin +import Data.Fin.Properties as FinProp +import Data.Fin.Permutation as ↔-Fin +import Data.List as List +import Data.List.Properties as ListProp +import Data.List.Relation.Binary.Permutation.Propositional as ↭-List +import Data.Nat as Nat +import Data.Vec.Functional as Vector +import Data.Vec.Functional.Properties as VectorProp +import Data.Vec.Functional.Relation.Binary.Permutation as ↭-Vec +import Data.Vec.Functional.Relation.Binary.Permutation.Properties as ↭-VecProp + +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_) +open import Data.Product.Base using (_,_; proj₁; proj₂) +open import Data.Vec.Functional.Relation.Unary.Any using (Any) +open import Function.Base using (_∘_) + +open ↭-Vec using () renaming (_↭_ to _↭′_) +open ↭-List using (_↭_; ↭-sym; module PermutationReasoning) +open ↔-Fin using (Permutation; _⟨$⟩ˡ_; _⟨$⟩ʳ_) +open List using (List) hiding (module List) +open Fin using (Fin; cast) hiding (module Fin) +open Vector using (Vector; toList; fromList) +open Fin.Fin +open Nat using (ℕ; zero; suc) +open _↭_ + +module _ where + + open Fin using (#_) + open ↔-Fin using (lift₀; insert) + open ↭-VecProp using (↭-refl; ↭-trans) + + -- convert a List permutation to a Vector permutation + fromList-↭ + : {A : Set} + {xs ys : List A} + → xs ↭ ys + → fromList xs ↭′ fromList ys + fromList-↭ refl = ↭-refl + fromList-↭ (prep _ xs↭ys) + with n↔m , xs↭ys′ ← fromList-↭ xs↭ys = lift₀ n↔m , λ where + zero → ≡.refl + (suc i) → xs↭ys′ i + fromList-↭ (swap x y xs↭ys) + with n↔m , xs↭ys′ ← fromList-↭ xs↭ys = insert (# 0) (# 1) (lift₀ n↔m) , λ where + zero → ≡.refl + (suc zero) → ≡.refl + (suc (suc i)) → xs↭ys′ i + fromList-↭ (trans {xs} xs↭ys ys↭zs) = + ↭-trans {_} {_} {_} {i = fromList xs} (fromList-↭ xs↭ys) (fromList-↭ ys↭zs) + +-- witness for an element in a Vector +_∈_ : A → {n : ℕ} → Vector A n → Set ℓ +x ∈ xs = Any (x ≡_) xs + +-- apply a permutation to a witness +apply + : {n m : ℕ} + {xs : Vector A n} + {ys : Vector A m} + {x : A} + → (xs↭ys : xs ↭′ ys) + → x ∈ xs + → x ∈ ys +apply {suc n} {zero} (↔n , _) (i , _) with () ← ↔n ⟨$⟩ˡ i +apply {suc n} {suc m} {xs} {ys} {x} (↔n , ↔≗) (i , x≡xs-i) = i′ , x≡ys-i′ + where + i′ : Fin (suc m) + i′ = ↔n ⟨$⟩ˡ i + open ≡.≡-Reasoning + x≡ys-i′ : x ≡ ys i′ + x≡ys-i′ = begin + x ≡⟨ x≡xs-i ⟩ + xs i ≡⟨ ≡.cong xs (↔-Fin.inverseʳ ↔n) ⟨ + xs (↔n ⟨$⟩ʳ (↔n ⟨$⟩ˡ i)) ≡⟨⟩ + xs (↔n ⟨$⟩ʳ i′) ≡⟨ ↔≗ i′ ⟩ + ys i′ ∎ + +-- remove an element from a Vector +remove : {n : ℕ} {x : A} (xs : Vector A (suc n)) → x ∈ xs → Vector A n +remove xs (i , _) = Vector.removeAt xs i + +-- remove an element and its image from a permutation +↭-remove + : {n m : ℕ} + {xs : Vector A (suc n)} + {ys : Vector A (suc m)} + {x : A} + → (xs↭ys : xs ↭′ ys) + → (x∈xs : x ∈ xs) + → let x∈ys = apply xs↭ys x∈xs in + remove xs x∈xs ↭′ remove ys x∈ys +↭-remove {n} {m} {xs} {ys} {x} xs↭ys@(ρ , ↔≗) x∈xs@(k , _) = ρ⁻ , ↔≗⁻ + where + k′ : Fin (suc m) + k′ = ρ ⟨$⟩ˡ k + x∈ys : x ∈ ys + x∈ys = apply xs↭ys x∈xs + ρ⁻ : Permutation m n + ρ⁻ = ↔-Fin.remove k′ ρ + xs⁻ : Vector A n + xs⁻ = remove xs x∈xs + ys⁻ : Vector A m + ys⁻ = remove ys x∈ys + open ≡.≡-Reasoning + open Fin using (punchIn) + ↔≗⁻ : (i : Fin m) → xs⁻ (ρ⁻ ⟨$⟩ʳ i) ≡ ys⁻ i + ↔≗⁻ i = begin + xs⁻ (ρ⁻ ⟨$⟩ʳ i) ≡⟨⟩ + remove xs x∈xs (ρ⁻ ⟨$⟩ʳ i) ≡⟨⟩ + xs (punchIn k (ρ⁻ ⟨$⟩ʳ i)) ≡⟨ ≡.cong xs (↔-Fin.punchIn-permute′ ρ k i) ⟨ + xs (ρ ⟨$⟩ʳ (punchIn k′ i)) ≡⟨ ↔≗ (punchIn k′ i) ⟩ + ys (punchIn k′ i) ≡⟨⟩ + remove ys x∈ys i ≡⟨⟩ + ys⁻ i ∎ + +open List.List +open List using (length; insertAt) + +-- build a permutation which moves the first element of a list to an arbitrary position +↭-insert-half + : {x₀ : A} + {xs : List A} + → (i : Fin (suc (length xs))) + → x₀ ∷ xs ↭ insertAt xs i x₀ +↭-insert-half zero = refl +↭-insert-half {x₀} {x₁ ∷ xs} (suc i) = trans (swap x₀ x₁ refl) (prep x₁ (↭-insert-half i)) + +-- add a mapping to a permutation, given a value and its start and end positions +↭-insert + : {xs ys : List A} + → xs ↭ ys + → (i : Fin (suc (length xs))) + (j : Fin (suc (length ys))) + (x : A) + → insertAt xs i x ↭ insertAt ys j x +↭-insert {xs} {ys} xs↭ys i j x = xs↭ys⁺ + where + open PermutationReasoning + xs↭ys⁺ : insertAt xs i x ↭ insertAt ys j x + xs↭ys⁺ = begin + insertAt xs i x ↭⟨ ↭-insert-half i ⟨ + x ∷ xs <⟨ xs↭ys ⟩ + x ∷ ys ↭⟨ ↭-insert-half j ⟩ + insertAt ys j x ∎ + +open ListProp using (length-tabulate; tabulate-cong) +insertAt-toList + : {n : ℕ} + {v : Vector A n} + (i : Fin (suc (length (toList v)))) + (i′ : Fin (suc n)) + → i ≡ cast (≡.cong suc (≡.sym (length-tabulate v))) i′ + → (x : A) + → insertAt (toList v) i x + ≡ toList (Vector.insertAt v i′ x) +insertAt-toList zero zero _ x = ≡.refl +insertAt-toList {suc n} {v} (suc i) (suc i′) ≡.refl x = + ≡.cong (v zero ∷_) (insertAt-toList i i′ ≡.refl x) + +-- convert a Vector permutation to a List permutation +toList-↭ + : {n m : ℕ} + {xs : Vector A n} + {ys : Vector A m} + → xs ↭′ ys + → toList xs ↭ toList ys +toList-↭ {zero} {zero} _ = refl +toList-↭ {zero} {suc m} (ρ , _) with () ← ρ ⟨$⟩ʳ zero +toList-↭ {suc n} {zero} (ρ , _) with () ← ρ ⟨$⟩ˡ zero +toList-↭ {suc n} {suc m} {xs} {ys} xs↭ys′ = xs↭ys + where + -- first element and its image + x₀ : A + x₀ = xs zero + x₀∈xs : x₀ ∈ xs + x₀∈xs = zero , ≡.refl + x₀∈ys : x₀ ∈ ys + x₀∈ys = apply xs↭ys′ x₀∈xs + -- reduce the problem by removing those elements + xs⁻ : Vector A n + xs⁻ = remove xs x₀∈xs + ys⁻ : Vector A m + ys⁻ = remove ys x₀∈ys + xs↭ys⁻ : xs⁻ ↭′ ys⁻ + xs↭ys⁻ = ↭-remove xs↭ys′ x₀∈xs + -- recursion on the reduced problem + xs↭ys⁻′ : toList xs⁻ ↭ toList ys⁻ + xs↭ys⁻′ = toList-↭ xs↭ys⁻ + -- indices for working with vectors + i : Fin (suc n) + i = proj₁ x₀∈xs + j : Fin (suc m) + j = proj₁ x₀∈ys + i′ : Fin (suc (length (toList xs⁻))) + i′ = cast (≡.sym (≡.cong suc (length-tabulate xs⁻))) i + j′ : Fin (suc (length (toList ys⁻))) + j′ = cast (≡.sym (≡.cong suc (length-tabulate ys⁻))) j + -- main construction + open VectorProp using (insertAt-removeAt) + open PermutationReasoning + open Vector using () renaming (insertAt to insertAt′) + xs↭ys : toList xs ↭ toList ys + xs↭ys = begin + toList xs ≡⟨ tabulate-cong (insertAt-removeAt xs i) ⟨ + toList (insertAt′ xs⁻ i x₀) ≡⟨ insertAt-toList i′ i ≡.refl x₀ ⟨ + insertAt (toList xs⁻) i′ x₀ ↭⟨ ↭-insert xs↭ys⁻′ i′ j′ x₀ ⟩ + insertAt (toList ys⁻) j′ x₀ ≡⟨ insertAt-toList j′ j ≡.refl x₀ ⟩ + toList (insertAt′ ys⁻ j x₀) ≡⟨ ≡.cong (toList ∘ insertAt′ ys⁻ j) (proj₂ x₀∈ys) ⟩ + toList (insertAt′ ys⁻ j (ys j)) ≡⟨ tabulate-cong (insertAt-removeAt ys j) ⟩ + toList ys ∎ -- cgit v1.2.3 From 2184a8f47f72a415e3387a9aaca042dd63c80fd9 Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Fri, 18 Jul 2025 17:34:52 -0500 Subject: Sorted lists with the same elements are equal --- Data/Permutation/Sort.agda | 176 +++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 176 insertions(+) create mode 100644 Data/Permutation/Sort.agda (limited to 'Data') diff --git a/Data/Permutation/Sort.agda b/Data/Permutation/Sort.agda new file mode 100644 index 0000000..977443a --- /dev/null +++ b/Data/Permutation/Sort.agda @@ -0,0 +1,176 @@ +{-# OPTIONS --without-K --safe #-} + +open import Relation.Binary.Bundles using (DecTotalOrder) + +module Data.Permutation.Sort {ℓ₁ ℓ₂ ℓ₃} (dto : DecTotalOrder ℓ₁ ℓ₂ ℓ₃) where + +open DecTotalOrder dto + using + ( _≈_ ; module Eq + ; totalOrder + ; _≤_ ; _≤?_ + ; ≤-respˡ-≈ ; ≤-respʳ-≈ + ; antisym + ) + renaming (Carrier to A; trans to ≤-trans; reflexive to ≤-reflexive) + +open import Data.Fin.Base using (Fin) +open import Data.List.Base using (List; _++_; [_]) +open import Data.List.Membership.Setoid Eq.setoid using (_∈_) +open import Data.List.Relation.Binary.Pointwise using (module Pointwise) +open import Data.List.Relation.Binary.Equality.Setoid Eq.setoid using (_≋_; ≋-refl; ≋-sym; ≋-trans) +open import Data.List.Relation.Unary.Linked using (Linked) +open import Data.List.Relation.Unary.Sorted.TotalOrder totalOrder using (Sorted) +open import Data.List.Relation.Binary.Permutation.Propositional using (_↭_; ↭-trans; ↭-sym) +open import Data.List.Relation.Binary.Permutation.Propositional.Properties using (↭-length) +open import Data.List.Relation.Unary.Any using (Any) +open import Data.List.Sort dto using (sort; sort-↭; sort-↗) +open import Relation.Nullary.Decidable.Core using (yes; no) +open Fin +open _↭_ +open Any +open List +open Linked +open Pointwise + +insert : List A → A → List A +insert [] x = [ x ] +insert (x₀ ∷ xs) x with x ≤? x₀ +... | yes _ = x ∷ x₀ ∷ xs +... | no _ = x₀ ∷ insert xs x + +insert-resp-≋ : {xs ys : List A} (v : A) → xs ≋ ys → insert xs v ≋ insert ys v +insert-resp-≋ _ [] = ≋-refl +insert-resp-≋ {x ∷ xs} {y ∷ ys} v (x≈y ∷ xs≋ys) + with v ≤? x | v ≤? y +... | yes v≤x | yes v≤y = Eq.refl ∷ x≈y ∷ xs≋ys +... | yes v≤x | no v≰y with () ← v≰y (≤-respʳ-≈ x≈y v≤x) +... | no v≰x | yes v≤y with () ← v≰x (≤-respʳ-≈ (Eq.sym x≈y) v≤y) +... | no v≰x | no v≰y = x≈y ∷ insert-resp-≋ v xs≋ys + +remove : {x : A} (xs : List A) → x ∈ xs → List A +remove (_ ∷ xs) (here _) = xs +remove (x ∷ xs) (there elem) = x ∷ remove xs elem + +remove-sorted : {x : A} {xs : List A} → Sorted xs → (x∈xs : x ∈ xs) → Sorted (remove xs x∈xs) +remove-sorted [-] (here x≡x₀) = [] +remove-sorted (x₀≤x₁ ∷ s-xs) (here px) = s-xs +remove-sorted (x₀≤x₁ ∷ [-]) (there (here px)) = [-] +remove-sorted (x₀≤x₁ ∷ x₁≤x₂ ∷ s-xs) (there (here px)) = ≤-trans x₀≤x₁ x₁≤x₂ ∷ s-xs +remove-sorted (x₀≤x₁ ∷ x₁≤x₂ ∷ s-xs) (there (there x∈xs)) = x₀≤x₁ ∷ remove-sorted (x₁≤x₂ ∷ s-xs) (there x∈xs) + +head : {xs : List A} {x : A} → .(x ∈ xs) → A +head {x ∷ _} _ = x + +tail : {xs : List A} {x : A} → .(x ∈ xs) → List A +tail {_ ∷ xs} _ = xs + +head-≤ : {xs : List A} + {x : A} + → Sorted xs + → (x∈xs : x ∈ xs) + → head x∈xs ≤ x +head-≤ {x ∷ []} [-] (here px) = ≤-reflexive (Eq.sym px) +head-≤ {x₀ ∷ x₁ ∷ xs} (x₀≤x₁ ∷ s-xs) (here px) = ≤-reflexive (Eq.sym px) +head-≤ {x₀ ∷ x₁ ∷ xs} (x₀≤x₁ ∷ s-xs) (there x∈xs) = ≤-trans x₀≤x₁ (head-≤ s-xs x∈xs) + +remove-head + : {xs : List A} + {x : A} + → Sorted xs + → (x∈xs : x ∈ xs) + → x ≈ head x∈xs + → remove xs x∈xs ≋ tail x∈xs +remove-head _ (here _) _ = ≋-refl +remove-head {x₀ ∷ x₁ ∷ xs} {x} (x₀≤x₁ ∷ s-xs) (there x∈xs) x≈x₀ = + x₀≈x₁ ∷ remove-head s-xs x∈xs x≈x₁ + where + x₀≈x₁ : x₀ ≈ x₁ + x₀≈x₁ = antisym x₀≤x₁ (≤-respʳ-≈ x≈x₀ (head-≤ s-xs x∈xs)) + x≈x₁ : x ≈ x₁ + x≈x₁ = Eq.trans x≈x₀ x₀≈x₁ + +insert-remove + : {xs : List A} + {x : A} + → (s-xs : Sorted xs) + → (x∈xs : x ∈ xs) + → insert (remove xs x∈xs) x ≋ xs +insert-remove [-] (here px) = px ∷ [] +insert-remove {x₀ ∷ x₁ ∷ xs} {x} (x₀≤x₁ ∷ s-xs) (here px) with x ≤? x₁ +... | yes x≤x₁ = px ∷ ≋-refl +... | no x≰x₁ with () ← x≰x₁ (≤-respˡ-≈ (Eq.sym px) x₀≤x₁) +insert-remove {x₀ ∷ x₁ ∷ xs} {x} (x₀≤x₁ ∷ s-xs) (there x∈xs) with x ≤? x₀ +... | yes x≤x₀ = + antisym x≤x₀ (≤-trans x₀≤x₁ x₁≤x) ∷ + antisym x₀≤x₁ (≤-trans x₁≤x x≤x₀) ∷ + remove-head s-xs x∈xs (antisym (≤-trans x≤x₀ x₀≤x₁) (head-≤ s-xs x∈xs)) + where + x₁≤x : x₁ ≤ x + x₁≤x = head-≤ s-xs x∈xs +... | no x≰x₀ = Eq.refl ∷ insert-remove s-xs x∈xs + +apply : {xs ys : List A} {x : A} → xs ↭ ys → x ∈ xs → x ∈ ys +apply refl x-in-xs = x-in-xs +apply (prep x xs↭ys) (here px) = here px +apply (prep x xs↭ys) (there x-in-xs) = there (apply xs↭ys x-in-xs) +apply (swap x y xs↭ys) (here px) = there (here px) +apply (swap x y xs↭ys) (there (here px)) = here px +apply (swap x y xs↭ys) (there (there x-in-xs)) = there (there (apply xs↭ys x-in-xs)) +apply (trans xs↭ys ys↭zs) x-in-xs = apply ys↭zs (apply xs↭ys x-in-xs) + +↭-remove + : {xs ys : List A} + {x : A} + → (xs↭ys : xs ↭ ys) + → (x∈xs : x ∈ xs) + → let x∈ys = apply xs↭ys x∈xs in + remove xs x∈xs ↭ remove ys x∈ys +↭-remove refl x∈xs = refl +↭-remove (prep x xs↭ys) (here px) = xs↭ys +↭-remove (prep x xs↭ys) (there x∈xs) = prep x (↭-remove xs↭ys x∈xs) +↭-remove (swap x y xs↭ys) (here px) = prep y xs↭ys +↭-remove (swap x y xs↭ys) (there (here px)) = prep x xs↭ys +↭-remove (swap x y xs↭ys) (there (there x∈xs)) = swap x y (↭-remove xs↭ys x∈xs) +↭-remove (trans xs↭ys ys↭zs) x∈xs = trans (↭-remove xs↭ys x∈xs) (↭-remove ys↭zs (apply xs↭ys x∈xs)) + +sorted-unique + : {xs ys : List A} + → xs ↭ ys + → Sorted xs + → Sorted ys + → xs ≋ ys +sorted-unique {[]} {ys} xs↭ys s-xs s-ys with .(↭-length xs↭ys) +sorted-unique {[]} {[]} xs↭ys s-xs s-ys | _ = [] +sorted-unique xs@{x ∷ xs′} {ys} xs↭ys s-xs s-ys = ≋-trans ≋xs (≋-trans xs≋ys″ ≋ys) + where + x∈xs : x ∈ xs + x∈xs = here Eq.refl + x∈ys : x ∈ ys + x∈ys = apply xs↭ys x∈xs + s-xs′ : Sorted (remove xs x∈xs) + s-xs′ = remove-sorted s-xs x∈xs + s-ys′ : Sorted (remove ys x∈ys) + s-ys′ = remove-sorted s-ys x∈ys + xs↭ys′ : remove xs x∈xs ↭ remove ys x∈ys + xs↭ys′ = ↭-remove xs↭ys x∈xs + xs≋ys′ : remove xs x∈xs ≋ remove ys x∈ys + xs≋ys′ = sorted-unique {xs′} xs↭ys′ s-xs′ s-ys′ + xs≋ys″ : insert (remove xs x∈xs) x ≋ insert (remove ys x∈ys) x + xs≋ys″ = insert-resp-≋ x xs≋ys′ + ≋xs : xs ≋ insert (remove xs x∈xs) x + ≋xs = ≋-sym (insert-remove s-xs x∈xs) + ≋ys : insert (remove ys x∈ys) x ≋ ys + ≋ys = insert-remove s-ys x∈ys + +sorted-≋ + : {xs ys : List A} + → xs ↭ ys + → sort xs ≋ sort ys +sorted-≋ {xs} {ys} xs↭ys = + sorted-unique + (↭-trans + (sort-↭ xs) + (↭-trans xs↭ys (↭-sym (sort-↭ ys)))) + (sort-↗ xs) + (sort-↗ ys) -- cgit v1.2.3 From d91f74bce9a8eb1dd38f74de5fae597bde54df5a Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Fri, 18 Jul 2025 17:45:53 -0500 Subject: Add Hypergraph setoid --- Data/Hypergraph/Base.agda | 4 ++-- Data/Hypergraph/Edge.agda | 5 +++++ Data/Hypergraph/Setoid.agda | 50 +++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 57 insertions(+), 2 deletions(-) create mode 100644 Data/Hypergraph/Setoid.agda (limited to 'Data') diff --git a/Data/Hypergraph/Base.agda b/Data/Hypergraph/Base.agda index e43cbce..5cf5388 100644 --- a/Data/Hypergraph/Base.agda +++ b/Data/Hypergraph/Base.agda @@ -9,7 +9,7 @@ open import Data.List.Base using (List; map) open import Data.Nat.Base using (ℕ) open import Data.String using (String; unlines) -import Data.List.Sort.MergeSort as MergeSort +import Data.List.Sort as Sort record Hypergraph (v : ℕ) : Set where field @@ -19,7 +19,7 @@ sortHypergraph : {v : ℕ} → Hypergraph v → Hypergraph v sortHypergraph {v} H = record { edges = sort edges } where open Hypergraph H - open MergeSort decTotalOrder using (sort) + open Sort decTotalOrder using (sort) showHypergraph : {v : ℕ} → Hypergraph v → String showHypergraph record { edges = e} = unlines (map showEdge e) diff --git a/Data/Hypergraph/Edge.agda b/Data/Hypergraph/Edge.agda index 3c2a3a1..cbf61e6 100644 --- a/Data/Hypergraph/Edge.agda +++ b/Data/Hypergraph/Edge.agda @@ -324,3 +324,8 @@ showEdge : {v : ℕ} → Edge v → String showEdge 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 diff --git a/Data/Hypergraph/Setoid.agda b/Data/Hypergraph/Setoid.agda new file mode 100644 index 0000000..c39977d --- /dev/null +++ b/Data/Hypergraph/Setoid.agda @@ -0,0 +1,50 @@ +{-# OPTIONS --without-K --safe #-} + +open import Data.Hypergraph.Label using (HypergraphLabel) + +module Data.Hypergraph.Setoid (HL : HypergraphLabel) where + +open import Data.Hypergraph.Edge HL using (decTotalOrder) +open import Data.Hypergraph.Base HL using (Hypergraph; sortHypergraph) +open import Data.Nat.Base using (ℕ) +open import Level using (0ℓ) +open import Relation.Binary.Bundles using (Setoid) +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_) + +record ≈-Hypergraph {v : ℕ} (H H′ : Hypergraph v) : Set where + module H = Hypergraph H + module H′ = Hypergraph H′ + field + ≡sorted : sortHypergraph H ≡ sortHypergraph H′ + open Hypergraph using (edges) + ≡edges : edges (sortHypergraph H) ≡ edges (sortHypergraph H′) + ≡edges = ≡.cong edges ≡sorted + open import Data.List.Relation.Binary.Permutation.Propositional using (_↭_; ↭-reflexive; ↭-sym; ↭-trans) + open import Data.List.Sort decTotalOrder using (sort-↭) + ↭edges : H.edges ↭ H′.edges + ↭edges = ↭-trans (↭-sym (sort-↭ H.edges)) (↭-trans (↭-reflexive ≡edges) (sort-↭ H′.edges)) + +≈-refl : {v : ℕ} {H : Hypergraph v} → ≈-Hypergraph H H +≈-refl = record { ≡sorted = ≡.refl } + +≈-sym : {v : ℕ} {H H′ : Hypergraph v} → ≈-Hypergraph H H′ → ≈-Hypergraph H′ H +≈-sym ≈H = record { ≡sorted = ≡.sym ≡sorted } + where + open ≈-Hypergraph ≈H + +≈-trans : {v : ℕ} {H H′ H″ : Hypergraph v} → ≈-Hypergraph H H′ → ≈-Hypergraph H′ H″ → ≈-Hypergraph H H″ +≈-trans ≈H₁ ≈H₂ = record { ≡sorted = ≡.trans ≈H₁.≡sorted ≈H₂.≡sorted } + where + module ≈H₁ = ≈-Hypergraph ≈H₁ + module ≈H₂ = ≈-Hypergraph ≈H₂ + +Hypergraph-Setoid : (v : ℕ) → Setoid 0ℓ 0ℓ +Hypergraph-Setoid v = record + { Carrier = Hypergraph v + ; _≈_ = ≈-Hypergraph + ; isEquivalence = record + { refl = ≈-refl + ; sym = ≈-sym + ; trans = ≈-trans + } + } -- 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') 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') 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') 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 Date: Wed, 15 Oct 2025 16:18:45 -0500 Subject: Replace proof with new stdlib property --- Data/Permutation/Sort.agda | 199 ++++----------------------------------------- 1 file changed, 16 insertions(+), 183 deletions(-) (limited to 'Data') diff --git a/Data/Permutation/Sort.agda b/Data/Permutation/Sort.agda index 658997d..8d097f2 100644 --- a/Data/Permutation/Sort.agda +++ b/Data/Permutation/Sort.agda @@ -4,193 +4,26 @@ open import Relation.Binary.Bundles using (DecTotalOrder) module Data.Permutation.Sort {ℓ₁ ℓ₂ ℓ₃} (dto : DecTotalOrder ℓ₁ ℓ₂ ℓ₃) where -open DecTotalOrder dto - using - ( _≈_ ; module Eq - ; totalOrder - ; _≤_ ; _≤?_ - ; ≤-respˡ-≈ ; ≤-respʳ-≈ - ; antisym - ) - renaming (Carrier to A; trans to ≤-trans; reflexive to ≤-reflexive) +open DecTotalOrder dto using (module Eq; totalOrder) renaming (Carrier to A) -open import Data.Nat.Base using (ℕ) -open import Data.List.Base using (List; _++_; [_]) -open import Data.List.Membership.Setoid Eq.setoid using (_∈_) -open import Data.List.Relation.Binary.Pointwise using (module Pointwise) -open import Data.List.Relation.Binary.Equality.Setoid Eq.setoid using (_≋_; ≋-refl; ≋-sym; ≋-trans; ≋-length; Any-resp-≋) -open import Data.List.Relation.Unary.Linked using (Linked) -open import Data.List.Relation.Unary.Sorted.TotalOrder totalOrder using (Sorted) -open import Data.List.Relation.Binary.Permutation.Homogeneous using (map) -open import Data.List.Relation.Binary.Permutation.Propositional using () renaming (_↭_ to _↭′_) -open import Data.List.Relation.Binary.Permutation.Setoid Eq.setoid using (_↭_; ↭-trans; ↭-sym; refl; prep; swap; trans; ↭-reflexive-≋) -open import Data.List.Relation.Binary.Permutation.Setoid.Properties Eq.setoid using (∈-resp-↭) -open import Relation.Binary.PropositionalEquality as ≡ using (_≡_) -open import Data.List.Relation.Binary.Permutation.Setoid.Properties (≡.setoid A) using (map⁺) -open import Data.List.Relation.Unary.Any using (Any) -open import Data.List.Sort dto using (sort; sort-↭; sort-↗) -open import Relation.Nullary.Decidable.Core using (yes; no) -open ℕ -open Any -open List -open Linked -open Pointwise - -insert : List A → A → List A -insert [] x = [ x ] -insert (x₀ ∷ xs) x with x ≤? x₀ -... | yes _ = x ∷ x₀ ∷ xs -... | no _ = x₀ ∷ insert xs x - -insert-resp-≋ : {xs ys : List A} (v : A) → xs ≋ ys → insert xs v ≋ insert ys v -insert-resp-≋ _ [] = ≋-refl -insert-resp-≋ {x ∷ xs} {y ∷ ys} v (x≈y ∷ xs≋ys) - with v ≤? x | v ≤? y -... | yes v≤x | yes v≤y = Eq.refl ∷ x≈y ∷ xs≋ys -... | yes v≤x | no v≰y with () ← v≰y (≤-respʳ-≈ x≈y v≤x) -... | no v≰x | yes v≤y with () ← v≰x (≤-respʳ-≈ (Eq.sym x≈y) v≤y) -... | no v≰x | no v≰y = x≈y ∷ insert-resp-≋ v xs≋ys - -remove : {x : A} (xs : List A) → x ∈ xs → List A -remove (_ ∷ xs) (here _) = xs -remove (x ∷ xs) (there elem) = x ∷ remove xs elem - -remove-sorted : {x : A} {xs : List A} → Sorted xs → (x∈xs : x ∈ xs) → Sorted (remove xs x∈xs) -remove-sorted [-] (here x≡x₀) = [] -remove-sorted (x₀≤x₁ ∷ s-xs) (here px) = s-xs -remove-sorted (x₀≤x₁ ∷ [-]) (there (here px)) = [-] -remove-sorted (x₀≤x₁ ∷ x₁≤x₂ ∷ s-xs) (there (here px)) = ≤-trans x₀≤x₁ x₁≤x₂ ∷ s-xs -remove-sorted (x₀≤x₁ ∷ x₁≤x₂ ∷ s-xs) (there (there x∈xs)) = x₀≤x₁ ∷ remove-sorted (x₁≤x₂ ∷ s-xs) (there x∈xs) - -head : {xs : List A} {x : A} → .(x ∈ xs) → A -head {x ∷ _} _ = x - -tail : {xs : List A} {x : A} → .(x ∈ xs) → List A -tail {_ ∷ xs} _ = xs - -head-≤ : {xs : List A} - {x : A} - → Sorted xs - → (x∈xs : x ∈ xs) - → head x∈xs ≤ x -head-≤ {x ∷ []} [-] (here px) = ≤-reflexive (Eq.sym px) -head-≤ {x₀ ∷ x₁ ∷ xs} (x₀≤x₁ ∷ s-xs) (here px) = ≤-reflexive (Eq.sym px) -head-≤ {x₀ ∷ x₁ ∷ xs} (x₀≤x₁ ∷ s-xs) (there x∈xs) = ≤-trans x₀≤x₁ (head-≤ s-xs x∈xs) - -remove-head - : {xs : List A} - {x : A} - → Sorted xs - → (x∈xs : x ∈ xs) - → x ≈ head x∈xs - → remove xs x∈xs ≋ tail x∈xs -remove-head _ (here _) _ = ≋-refl -remove-head {x₀ ∷ x₁ ∷ xs} {x} (x₀≤x₁ ∷ s-xs) (there x∈xs) x≈x₀ = - x₀≈x₁ ∷ remove-head s-xs x∈xs x≈x₁ - where - x₀≈x₁ : x₀ ≈ x₁ - x₀≈x₁ = antisym x₀≤x₁ (≤-respʳ-≈ x≈x₀ (head-≤ s-xs x∈xs)) - x≈x₁ : x ≈ x₁ - x≈x₁ = Eq.trans x≈x₀ x₀≈x₁ - -insert-remove - : {xs : List A} - {x : A} - → (s-xs : Sorted xs) - → (x∈xs : x ∈ xs) - → insert (remove xs x∈xs) x ≋ xs -insert-remove [-] (here px) = px ∷ [] -insert-remove {x₀ ∷ x₁ ∷ xs} {x} (x₀≤x₁ ∷ s-xs) (here px) with x ≤? x₁ -... | yes x≤x₁ = px ∷ ≋-refl -... | no x≰x₁ with () ← x≰x₁ (≤-respˡ-≈ (Eq.sym px) x₀≤x₁) -insert-remove {x₀ ∷ x₁ ∷ xs} {x} (x₀≤x₁ ∷ s-xs) (there x∈xs) with x ≤? x₀ -... | yes x≤x₀ = - antisym x≤x₀ (≤-trans x₀≤x₁ x₁≤x) ∷ - antisym x₀≤x₁ (≤-trans x₁≤x x≤x₀) ∷ - remove-head s-xs x∈xs (antisym (≤-trans x≤x₀ x₀≤x₁) (head-≤ s-xs x∈xs)) - where - x₁≤x : x₁ ≤ x - x₁≤x = head-≤ s-xs x∈xs -... | no x≰x₀ = Eq.refl ∷ insert-remove s-xs x∈xs - -open import Data.List.Base using (length) -open import Function.Base using (_∘_; flip; id) -open import Data.List.Relation.Binary.Permutation.Propositional using (↭⇒↭ₛ) - -∈-resp-≋ : {xs ys : List A} {x : A} → xs ≋ ys → x ∈ xs → x ∈ ys -∈-resp-≋ = Any-resp-≋ (flip Eq.trans) - -≋-remove - : {xs ys : List A} - {x : A} - → (xs≋ys : xs ≋ ys) - → (x∈xs : x ∈ xs) - → let x∈ys = ∈-resp-≋ xs≋ys x∈xs in - remove xs x∈xs ≋ remove ys x∈ys -≋-remove (x≈y ∷ xs≋ys) (here px) = xs≋ys -≋-remove (x≈y ∷ xs≋ys) (there x∈xs) = x≈y ∷ ≋-remove xs≋ys x∈xs - -↭-remove - : {xs ys : List A} - {x : A} - → (xs↭ys : xs ↭ ys) - → (x∈xs : x ∈ xs) - → let x∈ys = ∈-resp-↭ xs↭ys x∈xs in - remove xs x∈xs ↭ remove ys x∈ys -↭-remove (refl xs≋ys) x∈xs = ↭-reflexive-≋ (≋-remove xs≋ys x∈xs) -↭-remove (prep x xs↭ys) (here px) = xs↭ys -↭-remove (prep x xs↭ys) (there x∈xs) = prep x (↭-remove xs↭ys x∈xs) -↭-remove (swap x y xs↭ys) (here px) = prep y xs↭ys -↭-remove (swap x y xs↭ys) (there (here px)) = prep x xs↭ys -↭-remove (swap x y xs↭ys) (there (there x∈xs)) = swap x y (↭-remove xs↭ys x∈xs) -↭-remove (trans xs↭ys ys↭zs) x∈xs = trans (↭-remove xs↭ys x∈xs) (↭-remove ys↭zs (∈-resp-↭ xs↭ys x∈xs)) - -↭-length : ∀ {xs ys : List A} → xs ↭ ys → length xs ≡ length ys -↭-length (refl xs≋ys) = ≋-length xs≋ys -↭-length (prep x lr) = ≡.cong suc (↭-length lr) -↭-length (swap x y lr) = ≡.cong (suc ∘ suc) (↭-length lr) -↭-length (trans lr₁ lr₂) = ≡.trans (↭-length lr₁) (↭-length lr₂) - -sorted-unique - : {xs ys : List A} - → xs ↭ ys - → Sorted xs - → Sorted ys - → xs ≋ ys -sorted-unique {[]} {ys} xs↭ys s-xs s-ys with .(↭-length xs↭ys) -sorted-unique {[]} {[]} xs↭ys s-xs s-ys | _ = [] -sorted-unique xs@{x ∷ xs′} {ys} xs↭ys s-xs s-ys = ≋-trans ≋xs (≋-trans xs≋ys″ ≋ys) - where - x∈xs : x ∈ xs - x∈xs = here Eq.refl - x∈ys : x ∈ ys - x∈ys = ∈-resp-↭ xs↭ys x∈xs - s-xs′ : Sorted (remove xs x∈xs) - s-xs′ = remove-sorted s-xs x∈xs - s-ys′ : Sorted (remove ys x∈ys) - s-ys′ = remove-sorted s-ys x∈ys - xs↭ys′ : remove xs x∈xs ↭ remove ys x∈ys - xs↭ys′ = ↭-remove xs↭ys x∈xs - xs≋ys′ : remove xs x∈xs ≋ remove ys x∈ys - xs≋ys′ = sorted-unique {xs′} xs↭ys′ s-xs′ s-ys′ - xs≋ys″ : insert (remove xs x∈xs) x ≋ insert (remove ys x∈ys) x - xs≋ys″ = insert-resp-≋ x xs≋ys′ - ≋xs : xs ≋ insert (remove xs x∈xs) x - ≋xs = ≋-sym (insert-remove s-xs x∈xs) - ≋ys : insert (remove ys x∈ys) x ≋ ys - ≋ys = insert-remove s-ys x∈ys +open import Data.List.Base using (List) +open import Data.List.Relation.Binary.Equality.Setoid Eq.setoid using (_≋_) +open import Data.List.Relation.Binary.Permutation.Setoid Eq.setoid using (_↭_; module PermutationReasoning) +open import Data.List.Relation.Unary.Sorted.TotalOrder.Properties using (↗↭↗⇒≋) +open import Data.List.Sort dto using (sortingAlgorithm) +open import Data.List.Sort.Base totalOrder using (SortingAlgorithm) +open SortingAlgorithm sortingAlgorithm using (sort; sort-↭ₛ; sort-↗) sorted-≋ : {xs ys : List A} → xs ↭ ys → sort xs ≋ sort ys -sorted-≋ {xs} {ys} xs↭ys = - sorted-unique - (↭-trans - (⇒↭ (sort-↭ xs)) - (↭-trans xs↭ys (↭-sym (⇒↭ (sort-↭ ys))))) - (sort-↗ xs) - (sort-↗ ys) +sorted-≋ {xs} {ys} xs↭ys = ↗↭↗⇒≋ totalOrder (sort-↗ xs) (sort-↗ ys) sort-xs↭sort-ys where - ⇒↭ : {xs ys : List A} → xs ↭′ ys → xs ↭ ys - ⇒↭ = map Eq.reflexive ∘ ↭⇒↭ₛ + open PermutationReasoning + sort-xs↭sort-ys : sort xs ↭ sort ys + sort-xs↭sort-ys = begin + sort xs ↭⟨ sort-↭ₛ xs ⟩ + xs ↭⟨ xs↭ys ⟩ + ys ↭⟨ sort-↭ₛ ys ⟨ + sort ys ∎ -- cgit v1.2.3