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/Permutation.agda') 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 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/Permutation.agda') 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