blob: 0be86f91d25fe68dde8ea3eb6841eba28b4dfe88 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
|
{-# OPTIONS --without-K --safe #-}
open import Level using (Level; _⊔_)
module Data.Circuit {c ℓ : Level} where
import Data.List as List
open import Data.Circuit.Gate using (Gates)
open import Data.Fin using (Fin)
open import Data.Hypergraph {c} {ℓ} Gates
using
( Hypergraph
; mkHypergraph
; Hypergraphₛ
; module Edge
; normalize
; _≈_
; mk≈
)
open import Data.Nat using (ℕ)
open import Relation.Binary using (Rel; Setoid)
open import Function.Bundles using (Func; _⟶ₛ_)
open List using (List)
open Edge using (Edge; ≈-Edge⇒≡)
Circuit : ℕ → Set c
Circuit = Hypergraph
map : {n m : ℕ} → (Fin n → Fin m) → Circuit n → Circuit m
map f (mkHypergraph edges) = mkHypergraph (List.map (Edge.map f) edges)
Circuitₛ : ℕ → Setoid c (c ⊔ ℓ)
Circuitₛ = Hypergraphₛ
open Func
open Edge.Sort using (sort)
open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
open import Data.List.Relation.Binary.Permutation.Propositional using (_↭_; ↭⇒↭ₛ′)
open import Data.List.Relation.Binary.Permutation.Propositional.Properties using (map⁺)
open import Data.List.Relation.Binary.Pointwise as PW using (Pointwise; Pointwise-≡⇒≡)
open import Data.List.Relation.Binary.Permutation.Homogeneous using (Permutation)
import Data.Permutation.Sort as ↭-Sort
mapₛ : {n m : ℕ} → (Fin n → Fin m) → Circuitₛ n ⟶ₛ Circuitₛ m
mapₛ {n} {m} f .to = map f
mapₛ {n} {m} f .cong {mkHypergraph xs} {mkHypergraph ys} x≈y = mk≈ ≡-norm
where
open _≈_ x≈y using (↭-edges)
open ↭-Sort (Edge.decTotalOrder {m}) using (sorted-≋)
open import Function.Reasoning
xs′ ys′ : List (Edge m)
xs′ = List.map (Edge.map f) xs
ys′ = List.map (Edge.map f) ys
≡-norm : mkHypergraph (sort xs′) ≡ mkHypergraph (sort ys′)
≡-norm = ↭-edges ∶ xs ↭ ys
|> map⁺ (Edge.map f) ∶ xs′ ↭ ys′
|> ↭⇒↭ₛ′ Edge.≈-Edge-IsEquivalence ∶ Permutation Edge.≈-Edge xs′ ys′
|> sorted-≋ ∶ Pointwise Edge.≈-Edge (sort xs′) (sort ys′)
|> PW.map ≈-Edge⇒≡ ∶ Pointwise _≡_ (sort xs′) (sort ys′)
|> Pointwise-≡⇒≡ ∶ sort xs′ ≡ sort ys′
|> ≡.cong mkHypergraph ∶ mkHypergraph (sort xs′) ≡ mkHypergraph (sort ys′)
|
