diff options
Diffstat (limited to 'Data')
| -rw-r--r-- | Data/CMonoid.agda | 77 | ||||
| -rw-r--r-- | Data/Castable.agda | 50 | ||||
| -rw-r--r-- | Data/Circuit.agda | 42 | ||||
| -rw-r--r-- | Data/Circuit/Convert.agda | 181 | ||||
| -rw-r--r-- | Data/Circuit/Gate.agda | 137 | ||||
| -rw-r--r-- | Data/Circuit/Merge.agda | 427 | ||||
| -rw-r--r-- | Data/Circuit/Typecheck.agda | 78 | ||||
| -rw-r--r-- | Data/Circuit/Value.agda | 180 | ||||
| -rw-r--r-- | Data/Fin/Preimage.agda | 48 | ||||
| -rw-r--r-- | Data/Hypergraph.agda | 86 | ||||
| -rw-r--r-- | Data/Hypergraph/Edge.agda | 113 | ||||
| -rw-r--r-- | Data/Hypergraph/Edge/Order.agda | 280 | ||||
| -rw-r--r-- | Data/Hypergraph/Label.agda | 36 | ||||
| -rw-r--r-- | Data/Monoid.agda | 86 | ||||
| -rw-r--r-- | Data/Opaque/List.agda | 165 | ||||
| -rw-r--r-- | Data/Opaque/Multiset.agda | 131 | ||||
| -rw-r--r-- | Data/Permutation.agda | 217 | ||||
| -rw-r--r-- | Data/Permutation/Sort.agda | 29 | ||||
| -rw-r--r-- | Data/SExp.agda | 75 | ||||
| -rw-r--r-- | Data/SExp/Parser.agda | 73 | ||||
| -rw-r--r-- | Data/Setoid.agda | 8 | ||||
| -rw-r--r-- | Data/Setoid/Unit.agda | 11 | ||||
| -rw-r--r-- | Data/Subset/Functional.agda | 162 | ||||
| -rw-r--r-- | Data/System.agda | 144 | ||||
| -rw-r--r-- | Data/System/Values.agda | 146 | ||||
| -rw-r--r-- | Data/Vector.agda | 126 |
26 files changed, 3108 insertions, 0 deletions
diff --git a/Data/CMonoid.agda b/Data/CMonoid.agda new file mode 100644 index 0000000..8aaf869 --- /dev/null +++ b/Data/CMonoid.agda @@ -0,0 +1,77 @@ +{-# OPTIONS --without-K --safe #-} + +open import Level using (Level) +module Data.CMonoid {c ℓ : Level} where + +open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory) +open import Category.Instance.Setoids.SymmetricMonoidal {c} {ℓ} using (Setoids-×; ×-symmetric′) +open import Object.Monoid.Commutative using (CommutativeMonoid; CommutativeMonoid⇒) +open import Categories.Object.Monoid using (Monoid) + +open import Data.Monoid {c} {ℓ} using (toMonoid; fromMonoid; toMonoid⇒) + +import Algebra.Bundles as Alg + +open import Data.Setoid using (∣_∣) +open import Relation.Binary using (Setoid) +open import Function using (Func; _⟨$⟩_) +open import Data.Product using (curry′; uncurry′; _,_) +open Func + +-- A commutative monoid object in the (symmetric monoidal) category of setoids +-- is just a commutative monoid + +toCMonoid : CommutativeMonoid Setoids-×.symmetric → Alg.CommutativeMonoid c ℓ +toCMonoid M = record + { M + ; isCommutativeMonoid = record + { isMonoid = M.isMonoid + ; comm = comm + } + } + where + open CommutativeMonoid M using (monoid; commutative; μ) + module M = Alg.Monoid (toMonoid monoid) + opaque + unfolding toMonoid + comm : (x y : M.Carrier) → x M.∙ y M.≈ y M.∙ x + comm x y = commutative {x , y} + +open import Function.Construct.Constant using () renaming (function to Const) +open import Data.Setoid.Unit using (⊤ₛ) + +fromCMonoid : Alg.CommutativeMonoid c ℓ → CommutativeMonoid Setoids-×.symmetric +fromCMonoid M = record + { M + ; isCommutativeMonoid = record + { isMonoid = M.isMonoid + ; commutative = commutative + } + } + where + open Alg.CommutativeMonoid M using (monoid; comm) + module M = Monoid (fromMonoid monoid) + open Setoids-× using (_≈_; _∘_; module braiding) + opaque + unfolding toMonoid + commutative : M.μ ≈ M.μ ∘ braiding.⇒.η _ + commutative {x , y} = comm x y + +-- A morphism of monoids in the (monoidal) category of setoids is a monoid homomorphism + +module _ (M N : CommutativeMonoid Setoids-×.symmetric) where + + module M = Alg.CommutativeMonoid (toCMonoid M) + module N = Alg.CommutativeMonoid (toCMonoid N) + + open import Data.Product using (Σ; _,_) + open import Function using (_⟶ₛ_) + open import Algebra.Morphism using (IsMonoidHomomorphism) + open CommutativeMonoid + open CommutativeMonoid⇒ + + toCMonoid⇒ + : CommutativeMonoid⇒ Setoids-×.symmetric M N + → Σ (M.setoid ⟶ₛ N.setoid) (λ f + → IsMonoidHomomorphism M.rawMonoid N.rawMonoid (to f)) + toCMonoid⇒ f = toMonoid⇒ (monoid M) (monoid N) (monoid⇒ f) diff --git a/Data/Castable.agda b/Data/Castable.agda new file mode 100644 index 0000000..4f85b3d --- /dev/null +++ b/Data/Castable.agda @@ -0,0 +1,50 @@ +{-# OPTIONS --without-K --safe #-} + +module Data.Castable where + +open import Level using (Level; suc; _⊔_) +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 + + 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 + + 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 ℓ₂ + isCastable : IsCastable B diff --git a/Data/Circuit.agda b/Data/Circuit.agda new file mode 100644 index 0000000..473e4fc --- /dev/null +++ b/Data/Circuit.agda @@ -0,0 +1,42 @@ +{-# OPTIONS --without-K --safe #-} + +open import Level using (Level) + +module Data.Circuit {ℓ : Level} where + +open import Data.Circuit.Gate using (Gates) + +import Data.List as List +import Data.Hypergraph {ℓ} Gates as Hypergraph + +open import Data.Fin using (Fin) +open import Data.Nat using (ℕ) +open import Data.List.Relation.Binary.Permutation.Setoid.Properties using (map⁺) +open import Function using (Func; _⟶ₛ_; _∘_) +open import Relation.Binary using (Setoid) + +open Func + +open Hypergraph using (Multiset∘Edgeₛ) +open Hypergraph + using (_≈_ ; mk≈ ; module Edge; edgesₛ) + renaming + ( Hypergraph to Circuit + ; Hypergraphₛ to Circuitₛ + ; mkHypergraph to mkCircuit + ; mkHypergraphₛ to mkCircuitₛ + ) + public +open List using ([]) + +map : {n m : ℕ} → (Fin n → Fin m) → Circuit n → Circuit m +map f (mkCircuit edges) = mkCircuit (List.map (Edge.map f) edges) + +discrete : (n : ℕ) → Circuit n +discrete n = mkCircuit [] + +open Edge using (Edgeₛ) + +mapₛ : {n m : ℕ} → (Fin n → Fin m) → Circuitₛ n ⟶ₛ Circuitₛ m +mapₛ f .to = map f +mapₛ {n} {m} f .cong (mk≈ x≈y) = mk≈ (map⁺ (Edgeₛ n) (Edgeₛ m) (cong (Edge.mapₛ f)) x≈y) diff --git a/Data/Circuit/Convert.agda b/Data/Circuit/Convert.agda new file mode 100644 index 0000000..d5abd35 --- /dev/null +++ b/Data/Circuit/Convert.agda @@ -0,0 +1,181 @@ +{-# OPTIONS --without-K --safe #-} + +module Data.Circuit.Convert where + +open import Level using (0ℓ) + +import Data.Vec as Vec +import Data.Vec.Relation.Binary.Equality.Cast as VecCast +import Data.List.Relation.Binary.Permutation.Propositional as L +import Data.Vec.Functional.Relation.Binary.Permutation as V +import DecorationFunctor.Hypergraph.Labeled {0ℓ} {0ℓ} as LabeledHypergraph + +open import Data.Nat.Base using (ℕ) +open import Data.Circuit.Gate using (Gate; Gates; cast-gate; cast-gate-is-id; subst-is-cast-gate) +open import Data.Circuit {0ℓ} {0ℓ} using (Circuit; Circuitₛ; _≈_; mkCircuit; module Edge; mk≈) +open import Data.Fin.Base using (Fin) +open import Data.Product.Base using (_,_) +open import Data.Permutation using (fromList-↭; toList-↭) +open import Data.List using (length) +open import Data.Vec.Functional using (toVec; fromVec; toList; fromList) +open import Function.Bundles using (Equivalence; _↔_) +open import Function.Base using (_∘_; id) +open import Data.Vec.Properties using (tabulate-cong; tabulate-∘; map-cast) +open import Data.Fin.Base using () renaming (cast to fincast) +open import Data.Fin.Properties using () renaming (cast-trans to fincast-trans; cast-is-id to fincast-is-id) +open import Data.List.Relation.Binary.Permutation.Homogeneous using (Permutation) +open import Data.Product.Base using (proj₁; proj₂; _×_) +open import Data.Fin.Permutation using (flip; _⟨$⟩ˡ_) +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_) + +open LabeledHypergraph using (Hypergraph-same) renaming (Hypergraph to Hypergraph′; Hypergraph-setoid to Hypergraph-Setoid′) + +to : {v : ℕ} → Circuit v → Hypergraph′ v +to C = record + { h = length edges + ; a = arity ∘ fromList edges + ; j = fromVec ∘ ports ∘ fromList edges + ; l = label ∘ fromList edges + } + where + open Edge.Edge using (arity; ports; label) + open Circuit C + +from : {v : ℕ} → Hypergraph′ v → Circuit v +from {v} H = record + { edges = toList asEdge + } + where + open Hypergraph′ H + asEdge : Fin h → Edge.Edge v + asEdge e = record { label = l e ; ports = toVec (j e) } + +to-cong : {v : ℕ} {H H′ : Circuit v} → H ≈ H′ → Hypergraph-same (to H) (to H′) +to-cong {v} {H} {H′} ≈H = record + { ↔h = flip ρ + ; ≗a = ≗a + ; ≗j = ≗j + ; ≗l = ≗l + } + where + open Edge.Edge using (arity; ports; label) + open _≈_ ≈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.Label using (HypergraphLabel) + open HypergraphLabel Gates 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′ + → from H ≈ from H′ + from-cong {H} {H′} ≈H = mk≈ (toList-↭ (flip ↔h , H∘ρ≗H′)) + where + + module H = Hypergraph′ H + module H′ = Hypergraph′ H′ + open Hypergraph′ + open Hypergraph-same ≈H using (↔h; ≗a; ≗l; ≗j; inverseˡ) renaming (from to f; to to t) + asEdge : (H : Hypergraph′ v) → Fin (h H) → Edge.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) + + 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) + → Vec.cast m≡n (toVec (f ∘ fincast m≡n)) ≡ toVec f + cast-toVec m≡n f rewrite m≡n = begin + Vec.cast _ (toVec (f ∘ (fincast _))) ≡⟨ VecCast.cast-is-id ≡.refl (toVec (f ∘ fincast ≡.refl)) ⟩ + toVec (f ∘ fincast _) ≡⟨ tabulate-∘ f (fincast ≡.refl) ⟩ + Vec.map f (toVec (fincast _)) ≡⟨ ≡.cong (Vec.map f) (tabulate-cong (fincast-is-id ≡.refl)) ⟩ + Vec.map f (toVec id) ≡⟨ tabulate-∘ f id ⟨ + toVec f ∎ + + ≗p′ : (e : Fin H′.h) → Vec.cast (≗a′ e) (toVec (H.j (f e))) ≡ toVec (H′.j e) + ≗p′ e = begin + Vec.cast (≗a′ e) (toVec (H.j (f e))) ≡⟨ ≡.cong (Vec.cast (≗a′ e)) (tabulate-cong (≗j′ e)) ⟩ + Vec.cast _ (toVec (H′.j e ∘ fincast _)) ≡⟨ cast-toVec (≗a′ e) (H′.j e) ⟩ + toVec (H′.j e) ∎ + + H∘ρ≗H′ : (e : Fin H′.h) → asEdge H (↔h ⟨$⟩ˡ e) ≡ asEdge H′ e + H∘ρ≗H′ e = Edge.≈⇒≡ record + { ≡arity = ≗a′ e + ; ≡label = ≗l′ e + ; ≡ports = ≗p′ e + } + +equiv : (v : ℕ) → Equivalence (Circuitₛ v) (Hypergraph-Setoid′ v) +equiv v = record + { to = to + ; from = from + ; to-cong = to-cong + ; from-cong = from-cong + } diff --git a/Data/Circuit/Gate.agda b/Data/Circuit/Gate.agda new file mode 100644 index 0000000..f4b55de --- /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.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) +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 + +Gates : HypergraphLabel +Gates = 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/Merge.agda b/Data/Circuit/Merge.agda new file mode 100644 index 0000000..9cf180a --- /dev/null +++ b/Data/Circuit/Merge.agda @@ -0,0 +1,427 @@ +{-# OPTIONS --without-K --safe #-} + +module Data.Circuit.Merge where + +open import Data.Nat.Base using (ℕ) +open import Data.Fin.Base using (Fin; pinch; punchIn; punchOut; splitAt) +open import Data.Fin.Properties using (punchInᵢ≢i; punchIn-punchOut) +open import Data.Bool.Properties using (if-eta) +open import Data.Bool using (Bool; if_then_else_) +open import Data.Circuit.Value using (Value; join; join-comm; join-assoc) +open import Data.Sum.Properties using ([,]-cong; [,-]-cong; [-,]-cong; [,]-∘; [,]-map) +open import Data.Subset.Functional + using + ( Subset + ; ⁅_⁆ ; ⊥ ; ⁅⁆∘ρ + ; foldl ; foldl-cong₁ ; foldl-cong₂ + ; foldl-[] ; foldl-suc + ; foldl-⊥ ; foldl-⁅⁆ + ; foldl-fusion + ) +open import Data.Vector as V using (Vector; head; tail; removeAt) +open import Data.Vec.Functional using (_++_) +open import Data.Fin.Permutation + using + ( Permutation + ; Permutation′ + ; _⟨$⟩ˡ_ ; _⟨$⟩ʳ_ + ; inverseˡ ; inverseʳ + ; id + ; flip + ; insert ; remove + ; punchIn-permute + ) +open import Data.Product using (Σ-syntax; _,_) +open import Data.Fin.Preimage using (preimage; preimage-cong₁; preimage-cong₂) +open import Function.Base using (∣_⟩-_; _∘_; case_of_; _$_) +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≢_; _≗_; module ≡-Reasoning) + +open Value using (U) +open ℕ +open Fin +open Bool + +open ≡-Reasoning + +_when_ : Value → Bool → Value +x when b = if b then x else U + +opaque + merge-with : {A : ℕ} → Value → Vector Value A → Subset A → Value + merge-with e v = foldl (∣ join ⟩- v) e + + merge-with-cong : {A : ℕ} {v₁ v₂ : Vector Value A} (e : Value) → v₁ ≗ v₂ → merge-with e v₁ ≗ merge-with e v₂ + merge-with-cong e v₁≗v₂ = foldl-cong₁ (λ x → ≡.cong (join x) ∘ v₁≗v₂) e + + merge-with-cong₂ : {A : ℕ} (e : Value) (v : Vector Value A) {S₁ S₂ : Subset A} → S₁ ≗ S₂ → merge-with e v S₁ ≡ merge-with e v S₂ + merge-with-cong₂ e v = foldl-cong₂ (∣ join ⟩- v) e + + merge-with-⊥ : {A : ℕ} (e : Value) (v : Vector Value A) → merge-with e v ⊥ ≡ e + merge-with-⊥ e v = foldl-⊥ (∣ join ⟩- v) e + + merge-with-[] : (e : Value) (v : Vector Value 0) (S : Subset 0) → merge-with e v S ≡ e + merge-with-[] e v = foldl-[] (∣ join ⟩- v) e + + merge-with-suc + : {A : ℕ} (e : Value) (v : Vector Value (suc A)) (S : Subset (suc A)) + → merge-with e v S + ≡ merge-with (if head S then join e (head v) else e) (tail v) (tail S) + merge-with-suc e v = foldl-suc (∣ join ⟩- v) e + + merge-with-join + : {A : ℕ} + (x y : Value) + (v : Vector Value A) + → merge-with (join x y) v ≗ join x ∘ merge-with y v + merge-with-join {A} x y v S = ≡.sym (foldl-fusion (join x) fuse y S) + where + fuse : (acc : Value) (k : Fin A) → join x (join acc (v k)) ≡ join (join x acc) (v k) + fuse acc k = ≡.sym (join-assoc x acc (v k)) + + merge-with-⁅⁆ : {A : ℕ} (e : Value) (v : Vector Value A) (x : Fin A) → merge-with e v ⁅ x ⁆ ≡ join e (v x) + merge-with-⁅⁆ e v = foldl-⁅⁆ (∣ join ⟩- v) e + +merge-with-U : {A : ℕ} (e : Value) (S : Subset A) → merge-with e (λ _ → U) S ≡ e +merge-with-U {zero} e S = merge-with-[] e (λ _ → U) S +merge-with-U {suc A} e S = begin + merge-with e (λ _ → U) S ≡⟨ merge-with-suc e (λ _ → U) S ⟩ + merge-with + (if head S then join e U else e) + (tail (λ _ → U)) (tail S) ≡⟨ ≡.cong (λ h → merge-with (if head S then h else e) _ _) (join-comm e U) ⟩ + merge-with + (if head S then e else e) + (tail (λ _ → U)) (tail S) ≡⟨ ≡.cong (λ h → merge-with h (λ _ → U) (tail S)) (if-eta (head S)) ⟩ + merge-with e (tail (λ _ → U)) (tail S) ≡⟨⟩ + merge-with e (λ _ → U) (tail S) ≡⟨ merge-with-U e (tail S) ⟩ + e ∎ + +merge : {A : ℕ} → Vector Value A → Subset A → Value +merge v = merge-with U v + +merge-cong₁ : {A : ℕ} {v₁ v₂ : Vector Value A} → v₁ ≗ v₂ → merge v₁ ≗ merge v₂ +merge-cong₁ = merge-with-cong U + +merge-cong₂ : {A : ℕ} (v : Vector Value A) {S₁ S₂ : Subset A} → S₁ ≗ S₂ → merge v S₁ ≡ merge v S₂ +merge-cong₂ = merge-with-cong₂ U + +merge-⊥ : {A : ℕ} (v : Vector Value A) → merge v ⊥ ≡ U +merge-⊥ = merge-with-⊥ U + +merge-[] : (v : Vector Value 0) (S : Subset 0) → merge v S ≡ U +merge-[] = merge-with-[] U + +merge-[]₂ : {v₁ v₂ : Vector Value 0} {S₁ S₂ : Subset 0} → merge v₁ S₁ ≡ merge v₂ S₂ +merge-[]₂ {v₁} {v₂} {S₁} {S₂} = ≡.trans (merge-[] v₁ S₁) (≡.sym (merge-[] v₂ S₂)) + +merge-⁅⁆ : {A : ℕ} (v : Vector Value A) (x : Fin A) → merge v ⁅ x ⁆ ≡ v x +merge-⁅⁆ = merge-with-⁅⁆ U + +join-merge : {A : ℕ} (e : Value) (v : Vector Value A) (S : Subset A) → join e (merge v S) ≡ merge-with e v S +join-merge e v S = ≡.sym (≡.trans (≡.cong (λ h → merge-with h v S) (join-comm U e)) (merge-with-join e U v S)) + +merge-suc + : {A : ℕ} (v : Vector Value (suc A)) (S : Subset (suc A)) + → merge v S + ≡ merge-with (head v when head S) (tail v) (tail S) +merge-suc = merge-with-suc U + +insert-f0-0 + : {A B : ℕ} + (f : Fin (suc A) → Fin (suc B)) + → Σ[ ρ ∈ Permutation′ (suc B) ] (ρ ⟨$⟩ʳ (f zero) ≡ zero) +insert-f0-0 f = insert (f zero) zero id , help + where + open import Data.Fin using (_≟_) + open import Relation.Nullary.Decidable using (yes; no) + help : insert (f zero) zero id ⟨$⟩ʳ f zero ≡ zero + help with f zero ≟ f zero + ... | yes _ = ≡.refl + ... | no f0≢f0 with () ← f0≢f0 ≡.refl + +merge-removeAt + : {A : ℕ} + (k : Fin (suc A)) + (v : Vector Value (suc A)) + (S : Subset (suc A)) + → merge v S ≡ join (v k when S k) (merge (removeAt v k) (removeAt S k)) +merge-removeAt {A} zero v S = begin + merge-with U v S ≡⟨ merge-suc v S ⟩ + merge-with (head v when head S) (tail v) (tail S) ≡⟨ join-merge (head v when head S) (tail v) (tail S) ⟨ + join (head v when head S) (merge-with U (tail v) (tail S)) ∎ +merge-removeAt {suc A} (suc k) v S = begin + merge-with U v S ≡⟨ merge-suc v S ⟩ + merge-with v0? (tail v) (tail S) ≡⟨ join-merge _ (tail v) (tail S) ⟨ + join v0? (merge (tail v) (tail S)) ≡⟨ ≡.cong (join v0?) (merge-removeAt k (tail v) (tail S)) ⟩ + join v0? (join vk? (merge (tail v-) (tail S-))) ≡⟨ join-assoc (head v when head S) _ _ ⟨ + join (join v0? vk?) (merge (tail v-) (tail S-)) ≡⟨ ≡.cong (λ h → join h (merge (tail v-) (tail S-))) (join-comm (head v- when head S-) _) ⟩ + join (join vk? v0?) (merge (tail v-) (tail S-)) ≡⟨ join-assoc (tail v k when tail S k) _ _ ⟩ + join vk? (join v0? (merge (tail v-) (tail S-))) ≡⟨ ≡.cong (join vk?) (join-merge _ (tail v-) (tail S-)) ⟩ + join vk? (merge-with v0? (tail v-) (tail S-)) ≡⟨ ≡.cong (join vk?) (merge-suc v- S-) ⟨ + join vk? (merge v- S-) ∎ + where + v0? vk? : Value + v0? = head v when head S + vk? = tail v k when tail S k + v- : Vector Value (suc A) + v- = removeAt v (suc k) + S- : Subset (suc A) + S- = removeAt S (suc k) + +import Function.Structures as FunctionStructures +open module FStruct {A B : Set} = FunctionStructures {_} {_} {_} {_} {A} _≡_ {B} _≡_ using (IsInverse) +open IsInverse using () renaming (inverseˡ to invˡ; inverseʳ to invʳ) + +merge-preimage-ρ + : {A B : ℕ} + → (ρ : Permutation A B) + → (v : Vector Value A) + (S : Subset B) + → merge v (preimage (ρ ⟨$⟩ʳ_) S) ≡ merge (v ∘ (ρ ⟨$⟩ˡ_)) S +merge-preimage-ρ {zero} {zero} ρ v S = merge-[]₂ +merge-preimage-ρ {zero} {suc B} ρ v S with () ← ρ ⟨$⟩ˡ zero +merge-preimage-ρ {suc A} {zero} ρ v S with () ← ρ ⟨$⟩ʳ zero +merge-preimage-ρ {suc A} {suc B} ρ v S = begin + merge v (preimage ρʳ S) ≡⟨ merge-removeAt (head ρˡ) v (preimage ρʳ S) ⟩ + join + (head (v ∘ ρˡ) when S (ρʳ (ρˡ zero))) + (merge v- [preimageρʳS]-) ≡⟨ ≡.cong (λ h → join h (merge v- [preimageρʳS]-)) ≡vρˡ0? ⟩ + join vρˡ0? (merge v- [preimageρʳS]-) ≡⟨ ≡.cong (join vρˡ0?) (merge-cong₂ v- preimage-) ⟩ + join vρˡ0? (merge v- (preimage ρʳ- S-)) ≡⟨ ≡.cong (join vρˡ0?) (merge-preimage-ρ ρ- v- S-) ⟩ + join vρˡ0? (merge (v- ∘ ρˡ-) S-) ≡⟨ ≡.cong (join vρˡ0?) (merge-cong₁ v∘ρˡ- S-) ⟩ + join vρˡ0? (merge (tail (v ∘ ρˡ)) S-) ≡⟨ join-merge vρˡ0? (tail (v ∘ ρˡ)) S- ⟩ + merge-with vρˡ0? (tail (v ∘ ρˡ)) S- ≡⟨ merge-suc (v ∘ ρˡ) S ⟨ + merge (v ∘ ρˡ) S ∎ + where + ρˡ : Fin (suc B) → Fin (suc A) + ρˡ = ρ ⟨$⟩ˡ_ + ρʳ : Fin (suc A) → Fin (suc B) + ρʳ = ρ ⟨$⟩ʳ_ + ρ- : Permutation A B + ρ- = remove (head ρˡ) ρ + ρˡ- : Fin B → Fin A + ρˡ- = ρ- ⟨$⟩ˡ_ + ρʳ- : Fin A → Fin B + ρʳ- = ρ- ⟨$⟩ʳ_ + v- : Vector Value A + v- = removeAt v (head ρˡ) + [preimageρʳS]- : Subset A + [preimageρʳS]- = removeAt (preimage ρʳ S) (head ρˡ) + S- : Subset B + S- = tail S + vρˡ0? : Value + vρˡ0? = head (v ∘ ρˡ) when head S + ≡vρˡ0? : head (v ∘ ρˡ) when S (ρʳ (head ρˡ)) ≡ head (v ∘ ρˡ) when head S + ≡vρˡ0? = ≡.cong ((head (v ∘ ρˡ) when_) ∘ S) (inverseʳ ρ) + v∘ρˡ- : v- ∘ ρˡ- ≗ tail (v ∘ ρˡ) + v∘ρˡ- x = begin + v- (ρˡ- x) ≡⟨⟩ + v (punchIn (head ρˡ) (punchOut {A} {head ρˡ} _)) ≡⟨ ≡.cong v (punchIn-punchOut _) ⟩ + v (ρˡ (punchIn (ρʳ (ρˡ zero)) x)) ≡⟨ ≡.cong (λ h → v (ρˡ (punchIn h x))) (inverseʳ ρ) ⟩ + v (ρˡ (punchIn zero x)) ≡⟨⟩ + v (ρˡ (suc x)) ≡⟨⟩ + tail (v ∘ ρˡ) x ∎ + preimage- : [preimageρʳS]- ≗ preimage ρʳ- S- + preimage- x = begin + [preimageρʳS]- x ≡⟨⟩ + removeAt (preimage ρʳ S) (head ρˡ) x ≡⟨⟩ + S (ρʳ (punchIn (head ρˡ) x)) ≡⟨ ≡.cong S (punchIn-permute ρ (head ρˡ) x) ⟩ + S (punchIn (ρʳ (head ρˡ)) (ρʳ- x)) ≡⟨⟩ + S (punchIn (ρʳ (ρˡ zero)) (ρʳ- x)) ≡⟨ ≡.cong (λ h → S (punchIn h (ρʳ- x))) (inverseʳ ρ) ⟩ + S (punchIn zero (ρʳ- x)) ≡⟨⟩ + S (suc (ρʳ- x)) ≡⟨⟩ + preimage ρʳ- S- x ∎ + +push-with : {A B : ℕ} → (e : Value) → Vector Value A → (Fin A → Fin B) → Vector Value B +push-with e v f = merge-with e v ∘ preimage f ∘ ⁅_⁆ + +push : {A B : ℕ} → Vector Value A → (Fin A → Fin B) → Vector Value B +push = push-with U + +mutual + merge-preimage + : {A B : ℕ} + (f : Fin A → Fin B) + → (v : Vector Value A) + (S : Subset B) + → merge v (preimage f S) ≡ merge (push v f) S + merge-preimage {zero} {zero} f v S = merge-[]₂ + merge-preimage {zero} {suc B} f v S = begin + merge v (preimage f S) ≡⟨ merge-[] v (preimage f S) ⟩ + U ≡⟨ merge-with-U U S ⟨ + merge (λ _ → U) S ≡⟨ merge-cong₁ (λ x → ≡.sym (merge-[] v (⁅ x ⁆ ∘ f))) S ⟩ + merge (push v f) S ∎ + merge-preimage {suc A} {zero} f v S with () ← f zero + merge-preimage {suc A} {suc B} f v S with insert-f0-0 f + ... | ρ , ρf0≡0 = begin + merge v (preimage f S) ≡⟨ merge-cong₂ v (preimage-cong₁ (λ x → inverseˡ ρ {f x}) S) ⟨ + merge v (preimage (ρˡ ∘ ρʳ ∘ f) S) ≡⟨⟩ + merge v (preimage (ρʳ ∘ f) (preimage ρˡ S)) ≡⟨ merge-preimage-f0≡0 (ρʳ ∘ f) ρf0≡0 v (preimage ρˡ S) ⟩ + merge (merge v ∘ preimage (ρʳ ∘ f) ∘ ⁅_⁆) (preimage ρˡ S) ≡⟨ merge-preimage-ρ (flip ρ) (merge v ∘ preimage (ρʳ ∘ f) ∘ ⁅_⁆) S ⟩ + merge (merge v ∘ preimage (ρʳ ∘ f) ∘ ⁅_⁆ ∘ ρʳ) S ≡⟨ merge-cong₁ (merge-cong₂ v ∘ preimage-cong₂ (ρʳ ∘ f) ∘ ⁅⁆∘ρ ρ) S ⟩ + merge (merge v ∘ preimage (ρʳ ∘ f) ∘ preimage ρˡ ∘ ⁅_⁆) S ≡⟨⟩ + merge (merge v ∘ preimage (ρˡ ∘ ρʳ ∘ f) ∘ ⁅_⁆) S ≡⟨ merge-cong₁ (merge-cong₂ v ∘ preimage-cong₁ (λ y → inverseˡ ρ {f y}) ∘ ⁅_⁆) S ⟩ + merge (merge v ∘ preimage f ∘ ⁅_⁆) S ∎ + where + ρʳ ρˡ : Fin (ℕ.suc B) → Fin (ℕ.suc B) + ρʳ = ρ ⟨$⟩ʳ_ + ρˡ = ρ ⟨$⟩ˡ_ + + merge-preimage-f0≡0 + : {A B : ℕ} + (f : Fin (ℕ.suc A) → Fin (ℕ.suc B)) + → f Fin.zero ≡ Fin.zero + → (v : Vector Value (ℕ.suc A)) + (S : Subset (ℕ.suc B)) + → merge v (preimage f S) ≡ merge (merge v ∘ preimage f ∘ ⁅_⁆) S + merge-preimage-f0≡0 {A} {B} f f0≡0 v S + using S0 , S- ← head S , tail S + using v0 , v- ← head v , tail v + using _ , f- ← head f , tail f + = begin + merge v f⁻¹[S] ≡⟨ merge-suc v f⁻¹[S] ⟩ + merge-with v0? v- f⁻¹[S]- ≡⟨ join-merge v0? v- f⁻¹[S]- ⟨ + join v0? (merge v- f⁻¹[S]-) ≡⟨ ≡.cong (join v0?) (merge-preimage f- v- S) ⟩ + join v0? (merge f[v-] S) ≡⟨ join-merge v0? f[v-] S ⟩ + merge-with v0? f[v-] S ≡⟨ merge-with-suc v0? f[v-] S ⟩ + merge-with v0?+[f[v-]0?] f[v-]- S- ≡⟨ ≡.cong (λ h → merge-with h f[v-]- S-) ≡f[v]0 ⟩ + merge-with f[v]0? f[v-]- S- ≡⟨ merge-with-cong f[v]0? ≡f[v]- S- ⟩ + merge-with f[v]0? f[v]- S- ≡⟨ merge-suc f[v] S ⟨ + merge f[v] S ∎ + where + f⁻¹[S] : Subset (suc A) + f⁻¹[S] = preimage f S + f⁻¹[S]- : Subset A + f⁻¹[S]- = tail f⁻¹[S] + f⁻¹[S]0 : Bool + f⁻¹[S]0 = head f⁻¹[S] + f[v] : Vector Value (suc B) + f[v] = push v f + f[v]- : Vector Value B + f[v]- = tail f[v] + f[v]0 : Value + f[v]0 = head f[v] + f[v-] : Vector Value (suc B) + f[v-] = push v- f- + f[v-]- : Vector Value B + f[v-]- = tail f[v-] + f[v-]0 : Value + f[v-]0 = head f[v-] + f⁻¹⁅0⁆ : Subset (suc A) + f⁻¹⁅0⁆ = preimage f ⁅ zero ⁆ + f⁻¹⁅0⁆- : Subset A + f⁻¹⁅0⁆- = tail f⁻¹⁅0⁆ + v0? v0?+[f[v-]0?] f[v]0? : Value + v0? = v0 when f⁻¹[S]0 + v0?+[f[v-]0?] = (if S0 then join v0? f[v-]0 else v0?) + f[v]0? = f[v]0 when S0 + ≡f[v]0 : v0?+[f[v-]0?] ≡ f[v]0? + ≡f[v]0 rewrite f0≡0 with S0 + ... | true = begin + join v0 (merge v- f⁻¹⁅0⁆-) ≡⟨ join-merge v0 v- (tail (preimage f ⁅ zero ⁆)) ⟩ + merge-with v0 v- f⁻¹⁅0⁆- ≡⟨ ≡.cong (λ h → merge-with (v0 when ⁅ zero ⁆ h) v- f⁻¹⁅0⁆-) f0≡0 ⟨ + merge-with v0?′ v- f⁻¹⁅0⁆- ≡⟨ merge-suc v (preimage f ⁅ zero ⁆) ⟨ + merge v f⁻¹⁅0⁆ ∎ + where + v0?′ : Value + v0?′ = v0 when head f⁻¹⁅0⁆ + ... | false = ≡.refl + ≡f[v]- : f[v-]- ≗ f[v]- + ≡f[v]- x = begin + push v- f- (suc x) ≡⟨ ≡.cong (λ h → merge-with (v0 when ⁅ suc x ⁆ h) v- (preimage f- ⁅ suc x ⁆)) f0≡0 ⟨ + push-with v0?′ v- f- (suc x) ≡⟨ merge-suc v (preimage f ⁅ suc x ⁆) ⟨ + push v f (suc x) ∎ + where + v0?′ : Value + v0?′ = v0 when head (preimage f ⁅ suc x ⁆) + +merge-++ + : {n m : ℕ} + (xs : Vector Value n) + (ys : Vector Value m) + (S₁ : Subset n) + (S₂ : Subset m) + → merge (xs ++ ys) (S₁ ++ S₂) + ≡ join (merge xs S₁) (merge ys S₂) +merge-++ {zero} {m} xs ys S₁ S₂ = begin + merge (xs ++ ys) (S₁ ++ S₂) ≡⟨ merge-cong₂ (xs ++ ys) (λ _ → ≡.refl) ⟩ + merge (xs ++ ys) S₂ ≡⟨ merge-cong₁ (λ _ → ≡.refl) S₂ ⟩ + merge ys S₂ ≡⟨ ≡.cong (λ h → join h (merge ys S₂)) (merge-[] xs S₁) ⟨ + join (merge xs S₁) (merge ys S₂) ∎ +merge-++ {suc n} {m} xs ys S₁ S₂ = begin + merge (xs ++ ys) (S₁ ++ S₂) ≡⟨ merge-suc (xs ++ ys) (S₁ ++ S₂) ⟩ + merge-with (head xs when head S₁) (tail (xs ++ ys)) (tail (S₁ ++ S₂)) ≡⟨ join-merge (head xs when head S₁) (tail (xs ++ ys)) (tail (S₁ ++ S₂)) ⟨ + join (head xs when head S₁) (merge (tail (xs ++ ys)) (tail (S₁ ++ S₂))) + ≡⟨ ≡.cong (join (head xs when head S₁)) (merge-cong₁ ([,]-map ∘ splitAt n) (tail (S₁ ++ S₂))) ⟩ + join (head xs when head S₁) (merge (tail xs ++ ys) (tail (S₁ ++ S₂))) + ≡⟨ ≡.cong (join (head xs when head S₁)) (merge-cong₂ (tail xs ++ ys) ([,]-map ∘ splitAt n)) ⟩ + join (head xs when head S₁) (merge (tail xs ++ ys) (tail S₁ ++ S₂)) ≡⟨ ≡.cong (join (head xs when head S₁)) (merge-++ (tail xs) ys (tail S₁) S₂) ⟩ + join (head xs when head S₁) (join (merge (tail xs) (tail S₁)) (merge ys S₂)) ≡⟨ join-assoc (head xs when head S₁) (merge (tail xs) (tail S₁)) _ ⟨ + join (join (head xs when head S₁) (merge (tail xs) (tail S₁))) (merge ys S₂) + ≡⟨ ≡.cong (λ h → join h (merge ys S₂)) (join-merge (head xs when head S₁) (tail xs) (tail S₁)) ⟩ + join (merge-with (head xs when head S₁) (tail xs) (tail S₁)) (merge ys S₂) ≡⟨ ≡.cong (λ h → join h (merge ys S₂)) (merge-suc xs S₁) ⟨ + join (merge xs S₁) (merge ys S₂) ∎ + +open import Function using (Equivalence) +open Equivalence +open import Data.Nat using (_+_) +open import Data.Fin using (_↑ˡ_; _↑ʳ_; _≟_) +open import Data.Fin.Properties using (↑ˡ-injective; ↑ʳ-injective; splitAt⁻¹-↑ˡ; splitAt-↑ˡ; splitAt⁻¹-↑ʳ; splitAt-↑ʳ) +open import Relation.Nullary.Decidable using (does; does-⇔; dec-false) + +open Fin +⁅⁆-≟ : {n : ℕ} (x y : Fin n) → ⁅ x ⁆ y ≡ does (x ≟ y) +⁅⁆-≟ zero zero = ≡.refl +⁅⁆-≟ zero (suc y) = ≡.refl +⁅⁆-≟ (suc x) zero = ≡.refl +⁅⁆-≟ (suc x) (suc y) = ⁅⁆-≟ x y + +open import Data.Sum using ([_,_]′; inj₁; inj₂) +⁅⁆-++ + : {n′ m′ : ℕ} + (i : Fin (n′ + m′)) + → [ (λ x → ⁅ x ⁆ ++ ⊥) , (λ x → ⊥ ++ ⁅ x ⁆) ]′ (splitAt n′ i) ≗ ⁅ i ⁆ +⁅⁆-++ {n′} {m′} i x with splitAt n′ i in eq₁ +... | inj₁ i′ with splitAt n′ x in eq₂ +... | inj₁ x′ = begin + ⁅ i′ ⁆ x′ ≡⟨ ⁅⁆-≟ i′ x′ ⟩ + does (i′ ≟ x′) ≡⟨ does-⇔ ⇔ (i′ ≟ x′) (i′ ↑ˡ m′ ≟ x′ ↑ˡ m′) ⟩ + does (i′ ↑ˡ m′ ≟ x′ ↑ˡ m′) ≡⟨ ⁅⁆-≟ (i′ ↑ˡ m′) (x′ ↑ˡ m′) ⟨ + ⁅ i′ ↑ˡ m′ ⁆ (x′ ↑ˡ m′) ≡⟨ ≡.cong₂ ⁅_⁆ (splitAt⁻¹-↑ˡ eq₁) (splitAt⁻¹-↑ˡ eq₂) ⟩ + ⁅ i ⁆ x ∎ + where + ⇔ : Equivalence (≡.setoid (i′ ≡ x′)) (≡.setoid (i′ ↑ˡ m′ ≡ x′ ↑ˡ m′)) + ⇔ .to = ≡.cong (_↑ˡ m′) + ⇔ .from = ↑ˡ-injective m′ i′ x′ + ⇔ .to-cong ≡.refl = ≡.refl + ⇔ .from-cong ≡.refl = ≡.refl +... | inj₂ x′ = begin + false ≡⟨ dec-false (i′ ↑ˡ m′ ≟ n′ ↑ʳ x′) ↑ˡ≢↑ʳ ⟨ + does (i′ ↑ˡ m′ ≟ n′ ↑ʳ x′) ≡⟨ ⁅⁆-≟ (i′ ↑ˡ m′) (n′ ↑ʳ x′) ⟨ + ⁅ i′ ↑ˡ m′ ⁆ (n′ ↑ʳ x′) ≡⟨ ≡.cong₂ ⁅_⁆ (splitAt⁻¹-↑ˡ eq₁) (splitAt⁻¹-↑ʳ eq₂) ⟩ + ⁅ i ⁆ x ∎ + where + ↑ˡ≢↑ʳ : i′ ↑ˡ m′ ≢ n′ ↑ʳ x′ + ↑ˡ≢↑ʳ ≡ = case ≡.trans (≡.sym (splitAt-↑ˡ n′ i′ m′)) (≡.trans (≡.cong (splitAt n′) ≡) (splitAt-↑ʳ n′ m′ x′)) of λ { () } +⁅⁆-++ {n′} i x | inj₂ i′ with splitAt n′ x in eq₂ +⁅⁆-++ {n′} {m′} i x | inj₂ i′ | inj₁ x′ = begin + [ ⊥ , ⁅ i′ ⁆ ]′ (splitAt n′ x) ≡⟨ ≡.cong ([ ⊥ , ⁅ i′ ⁆ ]′) eq₂ ⟩ + false ≡⟨ dec-false (n′ ↑ʳ i′ ≟ x′ ↑ˡ m′) ↑ʳ≢↑ˡ ⟨ + does (n′ ↑ʳ i′ ≟ x′ ↑ˡ m′) ≡⟨ ⁅⁆-≟ (n′ ↑ʳ i′) (x′ ↑ˡ m′) ⟨ + ⁅ n′ ↑ʳ i′ ⁆ (x′ ↑ˡ m′) ≡⟨ ≡.cong₂ ⁅_⁆ (splitAt⁻¹-↑ʳ eq₁) (splitAt⁻¹-↑ˡ eq₂) ⟩ + ⁅ i ⁆ x ∎ + where + ↑ʳ≢↑ˡ : n′ ↑ʳ i′ ≢ x′ ↑ˡ m′ + ↑ʳ≢↑ˡ ≡ = case ≡.trans (≡.sym (splitAt-↑ʳ n′ m′ i′)) (≡.trans (≡.cong (splitAt n′) ≡) (splitAt-↑ˡ n′ x′ m′)) of λ { () } +⁅⁆-++ {n′} i x | inj₂ i′ | inj₂ x′ = begin + [ ⊥ , ⁅ i′ ⁆ ]′ (splitAt n′ x) ≡⟨ ≡.cong [ ⊥ , ⁅ i′ ⁆ ]′ eq₂ ⟩ + ⁅ i′ ⁆ x′ ≡⟨ ⁅⁆-≟ i′ x′ ⟩ + does (i′ ≟ x′) ≡⟨ does-⇔ ⇔ (i′ ≟ x′) (n′ ↑ʳ i′ ≟ n′ ↑ʳ x′) ⟩ + does (n′ ↑ʳ i′ ≟ n′ ↑ʳ x′) ≡⟨ ⁅⁆-≟ (n′ ↑ʳ i′) (n′ ↑ʳ x′) ⟨ + ⁅ n′ ↑ʳ i′ ⁆ (n′ ↑ʳ x′) ≡⟨ ≡.cong₂ ⁅_⁆ (splitAt⁻¹-↑ʳ eq₁) (splitAt⁻¹-↑ʳ eq₂) ⟩ + ⁅ i ⁆ x ∎ + where + ⇔ : Equivalence (≡.setoid (i′ ≡ x′)) (≡.setoid (n′ ↑ʳ i′ ≡ n′ ↑ʳ x′)) + ⇔ .to = ≡.cong (n′ ↑ʳ_) + ⇔ .from = ↑ʳ-injective n′ i′ x′ + ⇔ .to-cong ≡.refl = ≡.refl + ⇔ .from-cong ≡.refl = ≡.refl diff --git a/Data/Circuit/Typecheck.agda b/Data/Circuit/Typecheck.agda new file mode 100644 index 0000000..e34ea44 --- /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.Circuit.Gate using (GateLabel; Gate) +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) +open import Data.Maybe using (Maybe) renaming (map to mapM) +open import Data.Nat using (ℕ; _<?_; _≟_) +open import Data.String using (String) +open import Data.Product using (_×_; _,_; Σ) +open import Data.Vec using (Vec; []; _∷_; fromList) renaming (map to mapV) +open import Data.Vec.Effectful using () renaming (module TraversableA to VecTraversable) +open import Data.Maybe.Effectful using (applicative) +open import Data.Fin using (Fin; #_; fromℕ<) +open import Level using (0ℓ) + +import Relation.Binary.PropositionalEquality as ≡ + +open List +open SExp +open Gate +open Maybe + +gate : {n a : ℕ} (g : Gate a) → Vec (Fin n) a → Edge n +gate g p = record { label = g; ports = p } + +typeCheckGateLabel : SExp → Maybe (Σ ℕ Gate) +typeCheckGateLabel (Atom "one") = just (1 , ONE) +typeCheckGateLabel (Atom "zero") = just (1 , ZERO) +typeCheckGateLabel (Atom "not") = just (2 , NOT) +typeCheckGateLabel (Atom "id") = just (2 , ID) +typeCheckGateLabel (Atom "and") = just (3 , AND) +typeCheckGateLabel (Atom "or") = just (3 , OR) +typeCheckGateLabel (Atom "xor") = just (3 , XOR) +typeCheckGateLabel (Atom "nand") = just (3 , NAND) +typeCheckGateLabel (Atom "nor") = just (3 , NOR) +typeCheckGateLabel (Atom "xnor") = just (3 , XNOR) +typeCheckGateLabel _ = nothing + +open import Relation.Nullary.Decidable using (Dec; yes; no) +open Dec +open VecTraversable {0ℓ} applicative using () renaming (sequenceA to vecSequenceA) +open ListTraversable {0ℓ} applicative using () renaming (sequenceA to listSequenceA) + +typeCheckPort : (v : ℕ) → SExp → Maybe (Fin v) +typeCheckPort v (Nat n) with n <? v +... | yes n<v = just (fromℕ< n<v) +... | no _ = nothing +typeCheckPort _ _ = nothing + +typeCheckPorts : (v n : ℕ) → List SExp → Maybe (Vec (Fin v) n) +typeCheckPorts v n xs with length xs ≟ n +... | yes ≡.refl = vecSequenceA (mapV (typeCheckPort v) (fromList xs)) +... | no _ = nothing + +typeCheckGate : (v : ℕ) → SExp → Maybe (Edge v) +typeCheckGate v (SExps (labelString ∷ ports)) with typeCheckGateLabel labelString +... | just (n , label) = mapM (gate label) (typeCheckPorts v n ports) +... | nothing = nothing +typeCheckGate v _ = nothing + +typeCheckHeader : SExp → Maybe ℕ +typeCheckHeader (SExps (Atom "hypergraph" ∷ Nat n ∷ [])) = just n +typeCheckHeader _ = nothing + +typeCheckHypergraph : SExp → Maybe (Σ ℕ Hypergraph) +typeCheckHypergraph (SExps (x ∷ xs)) with typeCheckHeader x +... | nothing = nothing +... | just n with listSequenceA (mapL (typeCheckGate n) xs) +... | just e = just (n , record { edges = e }) +... | nothing = nothing +typeCheckHypergraph _ = nothing diff --git a/Data/Circuit/Value.agda b/Data/Circuit/Value.agda new file mode 100644 index 0000000..b135c35 --- /dev/null +++ b/Data/Circuit/Value.agda @@ -0,0 +1,180 @@ +{-# OPTIONS --without-K --safe #-} + +module Data.Circuit.Value where + +import Relation.Binary.Lattice.Properties.BoundedJoinSemilattice as LatticeProp + +open import Algebra.Bundles using (CommutativeMonoid) +open import Algebra.Structures using (IsCommutativeMonoid; IsMonoid; IsSemigroup; IsMagma) +open import Data.Product.Base using (_×_; _,_) +open import Data.String.Base using (String) +open import Level using (0ℓ) +open import Relation.Binary.Lattice.Bundles using (BoundedJoinSemilattice) +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_) + +open CommutativeMonoid +open IsCommutativeMonoid +open IsMagma +open IsMonoid +open IsSemigroup + +data Value : Set where + U T F X : Value + +data ≤-Value : Value → Value → Set where + v≤v : {v : Value} → ≤-Value v v + U≤T : ≤-Value U T + U≤F : ≤-Value U F + U≤X : ≤-Value U X + T≤X : ≤-Value T X + F≤X : ≤-Value F X + +≤-reflexive : {x y : Value} → x ≡ y → ≤-Value x y +≤-reflexive ≡.refl = v≤v + +≤-transitive : {i j k : Value} → ≤-Value i j → ≤-Value j k → ≤-Value i k +≤-transitive v≤v y = y +≤-transitive x v≤v = x +≤-transitive U≤T T≤X = U≤X +≤-transitive U≤F F≤X = U≤X + +≤-antisymmetric : {i j : Value} → ≤-Value i j → ≤-Value j i → i ≡ j +≤-antisymmetric v≤v _ = ≡.refl + +showValue : Value → String +showValue U = "U" +showValue T = "T" +showValue F = "F" +showValue X = "X" + +join : Value → Value → Value +join U y = y +join x U = x +join T T = T +join T F = X +join F T = X +join F F = F +join X _ = X +join _ X = X + +≤-supremum + : (x y : Value) + → ≤-Value x (join x y) + × ≤-Value y (join x y) + × ((z : Value) → ≤-Value x z → ≤-Value y z → ≤-Value (join x y) z) +≤-supremum U U = v≤v , v≤v , λ _ U≤z _ → U≤z +≤-supremum U T = U≤T , v≤v , λ { z x≤z y≤z → y≤z } +≤-supremum U F = U≤F , v≤v , λ { z x≤z y≤z → y≤z } +≤-supremum U X = U≤X , v≤v , λ { z x≤z y≤z → y≤z } +≤-supremum T U = v≤v , U≤T , λ { z x≤z y≤z → x≤z } +≤-supremum T T = v≤v , v≤v , λ { z x≤z y≤z → x≤z } +≤-supremum T F = T≤X , F≤X , λ { X x≤z y≤z → v≤v } +≤-supremum T X = T≤X , v≤v , λ { z x≤z y≤z → y≤z } +≤-supremum F U = v≤v , U≤F , λ { z x≤z y≤z → x≤z } +≤-supremum F T = F≤X , T≤X , λ { X x≤z y≤z → v≤v } +≤-supremum F F = v≤v , v≤v , λ { z x≤z y≤z → x≤z } +≤-supremum F X = F≤X , v≤v , λ { z x≤z y≤z → y≤z } +≤-supremum X U = v≤v , U≤X , λ { z x≤z y≤z → x≤z } +≤-supremum X T = v≤v , T≤X , λ { z x≤z y≤z → x≤z } +≤-supremum X F = v≤v , F≤X , λ { z x≤z y≤z → x≤z } +≤-supremum X X = v≤v , v≤v , λ { z x≤z y≤z → x≤z } + +join-comm : (x y : Value) → join x y ≡ join y x +join-comm U U = ≡.refl +join-comm U T = ≡.refl +join-comm U F = ≡.refl +join-comm U X = ≡.refl +join-comm T U = ≡.refl +join-comm T T = ≡.refl +join-comm T F = ≡.refl +join-comm T X = ≡.refl +join-comm F U = ≡.refl +join-comm F T = ≡.refl +join-comm F F = ≡.refl +join-comm F X = ≡.refl +join-comm X U = ≡.refl +join-comm X T = ≡.refl +join-comm X F = ≡.refl +join-comm X X = ≡.refl + +join-assoc : (x y z : Value) → join (join x y) z ≡ join x (join y z) +join-assoc U y z = ≡.refl +join-assoc T U z = ≡.refl +join-assoc T T U = ≡.refl +join-assoc T T T = ≡.refl +join-assoc T T F = ≡.refl +join-assoc T T X = ≡.refl +join-assoc T F U = ≡.refl +join-assoc T F T = ≡.refl +join-assoc T F F = ≡.refl +join-assoc T F X = ≡.refl +join-assoc T X U = ≡.refl +join-assoc T X T = ≡.refl +join-assoc T X F = ≡.refl +join-assoc T X X = ≡.refl +join-assoc F U z = ≡.refl +join-assoc F T U = ≡.refl +join-assoc F T T = ≡.refl +join-assoc F T F = ≡.refl +join-assoc F T X = ≡.refl +join-assoc F F U = ≡.refl +join-assoc F F T = ≡.refl +join-assoc F F F = ≡.refl +join-assoc F F X = ≡.refl +join-assoc F X U = ≡.refl +join-assoc F X T = ≡.refl +join-assoc F X F = ≡.refl +join-assoc F X X = ≡.refl +join-assoc X U z = ≡.refl +join-assoc X T U = ≡.refl +join-assoc X T T = ≡.refl +join-assoc X T F = ≡.refl +join-assoc X T X = ≡.refl +join-assoc X F U = ≡.refl +join-assoc X F T = ≡.refl +join-assoc X F F = ≡.refl +join-assoc X F X = ≡.refl +join-assoc X X U = ≡.refl +join-assoc X X T = ≡.refl +join-assoc X X F = ≡.refl +join-assoc X X X = ≡.refl + +Lattice : BoundedJoinSemilattice 0ℓ 0ℓ 0ℓ +Lattice = record + { Carrier = Value + ; _≈_ = _≡_ + ; _≤_ = ≤-Value + ; _∨_ = join + ; ⊥ = U + ; isBoundedJoinSemilattice = record + { isJoinSemilattice = record + { isPartialOrder = record + { isPreorder = record + { isEquivalence = ≡.isEquivalence + ; reflexive = ≤-reflexive + ; trans = ≤-transitive + } + ; antisym = ≤-antisymmetric + } + ; supremum = ≤-supremum + } + ; minimum = λ where + U → v≤v + T → U≤T + F → U≤F + X → U≤X + } + } + +module Lattice = BoundedJoinSemilattice Lattice + +Monoid : CommutativeMonoid 0ℓ 0ℓ +Monoid .Carrier = Lattice.Carrier +Monoid ._≈_ = Lattice._≈_ +Monoid ._∙_ = Lattice._∨_ +Monoid .ε = Lattice.⊥ +Monoid .isCommutativeMonoid .isMonoid .isSemigroup .isMagma .isEquivalence = ≡.isEquivalence +Monoid .isCommutativeMonoid .isMonoid .isSemigroup .isMagma .∙-cong = ≡.cong₂ join +Monoid .isCommutativeMonoid .isMonoid .isSemigroup .assoc = join-assoc +Monoid .isCommutativeMonoid .isMonoid .identity = LatticeProp.identity Lattice +Monoid .isCommutativeMonoid .comm = join-comm diff --git a/Data/Fin/Preimage.agda b/Data/Fin/Preimage.agda new file mode 100644 index 0000000..4f7ea43 --- /dev/null +++ b/Data/Fin/Preimage.agda @@ -0,0 +1,48 @@ +{-# OPTIONS --without-K --safe #-} + +module Data.Fin.Preimage where + +open import Data.Nat.Base using (ℕ) +open import Data.Fin.Base using (Fin) +open import Function.Base using (∣_⟩-_; _∘_) +open import Relation.Binary.PropositionalEquality as ≡ using (_≗_) +open import Data.Subset.Functional using (Subset; foldl; _∪_; ⊥; ⁅_⁆) + +private + variable A B C : ℕ + +preimage : (Fin A → Fin B) → Subset B → Subset A +preimage f Y = Y ∘ f + +⋃ : Subset A → (Fin A → Subset B) → Subset B +⋃ S f = foldl (∣ _∪_ ⟩- f) ⊥ S + +image : (Fin A → Fin B) → Subset A → Subset B +image f X = ⋃ X (⁅_⁆ ∘ f) + +preimage-cong₁ + : {f g : Fin A → Fin B} + → f ≗ g + → (S : Subset B) + → preimage f S ≗ preimage g S +preimage-cong₁ f≗g S x = ≡.cong S (f≗g x) + +preimage-cong₂ + : (f : Fin A → Fin B) + {S₁ S₂ : Subset B} + → S₁ ≗ S₂ + → preimage f S₁ ≗ preimage f S₂ +preimage-cong₂ f S₁≗S₂ = S₁≗S₂ ∘ f + +preimage-∘ + : (f : Fin A → Fin B) + (g : Fin B → Fin C) + (z : Fin C) + → preimage (g ∘ f) ⁅ z ⁆ ≗ preimage f (preimage g ⁅ z ⁆) +preimage-∘ f g S x = ≡.refl + +preimage-⊥ + : {n m : ℕ} + (f : Fin n → Fin m) + → preimage f ⊥ ≗ ⊥ +preimage-⊥ f x = ≡.refl diff --git a/Data/Hypergraph.agda b/Data/Hypergraph.agda new file mode 100644 index 0000000..532e082 --- /dev/null +++ b/Data/Hypergraph.agda @@ -0,0 +1,86 @@ +{-# OPTIONS --without-K --safe #-} + +open import Data.Hypergraph.Label using (HypergraphLabel) +open import Level using (Level; 0ℓ) + +module Data.Hypergraph {ℓ : Level} (HL : HypergraphLabel) where + +import Data.List.Relation.Binary.Pointwise as PW +import Function.Reasoning as →-Reasoning +import Relation.Binary.PropositionalEquality as ≡ +import Data.Hypergraph.Edge {ℓ} HL as Hyperedge +import Data.List.Relation.Binary.Permutation.Propositional as List-↭ +import Data.List.Relation.Binary.Permutation.Setoid as ↭ + +open HypergraphLabel HL using (Label) public + +open import Data.List using (List; map) +open import Data.Nat using (ℕ) +open import Data.String using (String; unlines) +open import Function using (_∘_; _⟶ₛ_; Func) +open import Relation.Binary using (Setoid) + +module Edge = Hyperedge +open Edge using (Edge; Edgeₛ) + +-- A hypergraph is a list of edges +record Hypergraph (v : ℕ) : Set ℓ where + constructor mkHypergraph + field + edges : List (Edge v) + +module _ {v : ℕ} where + + open ↭ (Edgeₛ v) using (_↭_; ↭-refl; ↭-sym; ↭-trans) + + show : Hypergraph v → String + show (mkHypergraph e) = unlines (map Edge.show e) + + -- an equivalence relation on hypergraphs + record _≈_ (H H′ : Hypergraph v) : Set ℓ where + + constructor mk≈ + + module H = Hypergraph H + module H′ = Hypergraph H′ + + field + ↭-edges : H.edges ↭ H′.edges + + infixr 4 _≈_ + + ≈-refl : {H : Hypergraph v} → H ≈ H + ≈-refl = mk≈ ↭-refl + + ≈-sym : {H H′ : Hypergraph v} → H ≈ H′ → H′ ≈ H + ≈-sym (mk≈ ≡n) = mk≈ (↭-sym ≡n) + + ≈-trans : {H H′ H″ : Hypergraph v} → H ≈ H′ → H′ ≈ H″ → H ≈ H″ + ≈-trans (mk≈ ≡n₁) (mk≈ ≡n₂) = mk≈ (↭-trans ≡n₁ ≡n₂) + +-- The setoid of labeled hypergraphs with v nodes +Hypergraphₛ : ℕ → Setoid ℓ ℓ +Hypergraphₛ v = record + { Carrier = Hypergraph v + ; _≈_ = _≈_ + ; isEquivalence = record + { refl = ≈-refl + ; sym = ≈-sym + ; trans = ≈-trans + } + } + +open Func + +open ↭ using (↭-setoid) + +Multiset∘Edgeₛ : (n : ℕ) → Setoid ℓ ℓ +Multiset∘Edgeₛ = ↭-setoid ∘ Edgeₛ + +mkHypergraphₛ : {n : ℕ} → Multiset∘Edgeₛ n ⟶ₛ Hypergraphₛ n +mkHypergraphₛ .to = mkHypergraph +mkHypergraphₛ .cong = mk≈ + +edgesₛ : {n : ℕ} → Hypergraphₛ n ⟶ₛ Multiset∘Edgeₛ n +edgesₛ .to = Hypergraph.edges +edgesₛ .cong = _≈_.↭-edges diff --git a/Data/Hypergraph/Edge.agda b/Data/Hypergraph/Edge.agda new file mode 100644 index 0000000..447f008 --- /dev/null +++ b/Data/Hypergraph/Edge.agda @@ -0,0 +1,113 @@ +{-# OPTIONS --without-K --safe #-} + +open import Data.Hypergraph.Label using (HypergraphLabel) + +open import Level using (Level; 0ℓ) +module Data.Hypergraph.Edge {ℓ : Level} (HL : HypergraphLabel) where + +import Data.Vec.Functional as Vec +import Data.Vec.Functional.Relation.Binary.Equality.Setoid as PW +import Data.Fin.Properties as FinProp + +open import Data.Fin as Fin using (Fin) +open import Data.Fin.Show using () renaming (show to showFin) +open import Data.Nat using (ℕ) +open import Data.String using (String; _<+>_) +open import Data.Vec.Show using () renaming (show to showVec) +open import Level using (0ℓ) +open import Relation.Binary using (Setoid; IsEquivalence) +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; module ≡-Reasoning) +open import Function using (_⟶ₛ_; Func; _∘_) + +module HL = HypergraphLabel HL + +open HL using (Label) +open Vec using (Vector) +open Func + +record Edge (v : ℕ) : Set ℓ where + constructor mkEdge + field + {arity} : ℕ + label : Label arity + ports : Fin arity → Fin v + +map : {n m : ℕ} → (Fin n → Fin m) → Edge n → Edge m +map f edge = record + { label = label + ; ports = Vec.map f ports + } + where + open Edge edge + +module _ {v : ℕ} where + + open PW (≡.setoid (Fin v)) using (_≋_) + + -- an equivalence relation on edges with v nodes + record _≈_ (E E′ : Edge v) : Set ℓ where + constructor mk≈ + module E = Edge E + module E′ = Edge E′ + field + ≡arity : E.arity ≡ E′.arity + ≡label : HL.cast ≡arity E.label ≡ E′.label + ≡ports : E.ports ≋ E′.ports ∘ Fin.cast ≡arity + + ≈-refl : {x : Edge v} → x ≈ x + ≈-refl {x} = record + { ≡arity = ≡.refl + ; ≡label = HL.≈-reflexive ≡.refl + ; ≡ports = ≡.cong (Edge.ports x) ∘ ≡.sym ∘ FinProp.cast-is-id _ + } + + ≈-sym : {x y : Edge v} → x ≈ y → y ≈ x + ≈-sym x≈y = record + { ≡arity = ≡.sym ≡arity + ; ≡label = HL.≈-sym ≡label + ; ≡ports = ≡.sym ∘ ≡ports-sym + } + where + open _≈_ x≈y + open ≡-Reasoning + ≡ports-sym : (i : Fin E′.arity) → E.ports (Fin.cast _ i) ≡ E′.ports i + ≡ports-sym i = begin + E.ports (Fin.cast _ i) ≡⟨ ≡ports (Fin.cast _ i) ⟩ + E′.ports (Fin.cast ≡arity (Fin.cast _ i)) + ≡⟨ ≡.cong E′.ports (FinProp.cast-involutive ≡arity _ i) ⟩ + E′.ports i ∎ + + ≈-trans : {x y z : Edge v} → x ≈ y → y ≈ z → x ≈ z + ≈-trans {x} {y} {z} x≈y y≈z = record + { ≡arity = ≡.trans x≈y.≡arity y≈z.≡arity + ; ≡label = HL.≈-trans x≈y.≡label y≈z.≡label + ; ≡ports = ≡-ports + } + where + module x≈y = _≈_ x≈y + module y≈z = _≈_ y≈z + open ≡-Reasoning + ≡-ports : (i : Fin x≈y.E.arity) → x≈y.E.ports i ≡ y≈z.E′.ports (Fin.cast _ i) + ≡-ports i = begin + x≈y.E.ports i ≡⟨ x≈y.≡ports i ⟩ + y≈z.E.ports (Fin.cast _ i) ≡⟨ y≈z.≡ports (Fin.cast _ i) ⟩ + y≈z.E′.ports (Fin.cast y≈z.≡arity (Fin.cast _ i)) + ≡⟨ ≡.cong y≈z.E′.ports (FinProp.cast-trans _ y≈z.≡arity i) ⟩ + y≈z.E′.ports (Fin.cast _ i) ∎ + + ≈-IsEquivalence : IsEquivalence _≈_ + ≈-IsEquivalence = record + { refl = ≈-refl + ; sym = ≈-sym + ; trans = ≈-trans + } + + show : Edge v → String + show (mkEdge {a} l p) = HL.showLabel a l <+> showVec showFin (Vec.toVec p) + +Edgeₛ : (v : ℕ) → Setoid ℓ ℓ +Edgeₛ v = record { isEquivalence = ≈-IsEquivalence {v} } + +mapₛ : {n m : ℕ} → (Fin n → Fin m) → Edgeₛ n ⟶ₛ Edgeₛ m +mapₛ f .to = map f +mapₛ f .cong (mk≈ ≡a ≡l ≡p) = mk≈ ≡a ≡l (≡.cong f ∘ ≡p) diff --git a/Data/Hypergraph/Edge/Order.agda b/Data/Hypergraph/Edge/Order.agda new file mode 100644 index 0000000..4b3c1e8 --- /dev/null +++ b/Data/Hypergraph/Edge/Order.agda @@ -0,0 +1,280 @@ +{-# OPTIONS --without-K --safe #-} + +open import Data.Hypergraph.Label using (HypergraphLabel) + +module Data.Hypergraph.Edge.Order (HL : HypergraphLabel) where + +import Data.List.Sort as ListSort +import Data.Fin as Fin +import Data.Fin.Properties as FinProp +import Data.Vec as Vec +import Data.Vec.Relation.Binary.Equality.Cast as VecCast +import Data.Vec.Relation.Binary.Lex.Strict as Lex +import Relation.Binary.PropositionalEquality as ≡ +import Relation.Binary.Properties.DecTotalOrder as DTOP +import Relation.Binary.Properties.StrictTotalOrder as STOP + +open import Data.Hypergraph.Edge HL using (Edge; ≈-Edge; ≈-Edge-IsEquivalence) +open import Data.Fin using (Fin) +open import Data.Nat using (ℕ; _<_) +open import Data.Nat.Properties using (<-irrefl; <-trans; <-resp₂-≡; <-cmp) +open import Data.Product.Base using (_,_; proj₁; proj₂) +open import Data.Vec.Relation.Binary.Pointwise.Inductive using (Pointwise-≡⇒≡) +open import Level using (0ℓ) +open import Relation.Binary + using + ( Rel + ; Tri ; Trichotomous + ; IsStrictTotalOrder ; IsEquivalence + ; _Respects_ + ; DecTotalOrder ; StrictTotalOrder + ) +open import Relation.Nullary using (¬_) + +module HL = HypergraphLabel HL +open HL using (Label; cast; cast-is-id) +open Vec using (Vec) + +open ≡ using (_≡_) + +open HL using (_[_<_]) +_<<_ : {v a : ℕ} → Rel (Vec (Fin v) a) 0ℓ +_<<_ {v} = Lex.Lex-< _≡_ (Fin._<_ {v}) + +data <-Edge {v : ℕ} : Edge v → Edge v → Set where + <-arity + : {x y : Edge v} + → Edge.arity x < Edge.arity y + → <-Edge x y + <-label + : {x y : Edge v} + (≡a : Edge.arity x ≡ Edge.arity y) + → Edge.arity y [ cast ≡a (Edge.label x) < Edge.label y ] + → <-Edge x y + <-ports + : {x y : Edge v} + (≡a : Edge.arity x ≡ Edge.arity y) + (≡l : Edge.label x HL.≈[ ≡a ] Edge.label y) + → Vec.cast ≡a (Edge.ports x) << Edge.ports y + → <-Edge x y + +<-Edge-irrefl : {v : ℕ} {x y : Edge v} → ≈-Edge x y → ¬ <-Edge x y +<-Edge-irrefl record { ≡arity = ≡a } (<-arity n<m) = <-irrefl ≡a n<m +<-Edge-irrefl record { ≡label = ≡l } (<-label _ (_ , x≉y)) = x≉y ≡l +<-Edge-irrefl record { ≡ports = ≡p } (<-ports ≡.refl ≡l x<y) + = Lex.<-irrefl FinProp.<-irrefl (≡⇒Pointwise-≡ ≡p) x<y + +<-Edge-trans : {v : ℕ} {i j k : Edge v} → <-Edge i j → <-Edge j k → <-Edge i k +<-Edge-trans (<-arity i<j) (<-arity j<k) = <-arity (<-trans i<j j<k) +<-Edge-trans (<-arity i<j) (<-label ≡.refl j<k) = <-arity i<j +<-Edge-trans (<-arity i<j) (<-ports ≡.refl _ j<k) = <-arity i<j +<-Edge-trans (<-label ≡.refl i<j) (<-arity j<k) = <-arity j<k +<-Edge-trans {_} {i} (<-label ≡.refl i<j) (<-label ≡.refl j<k) + = <-label ≡.refl (<-label-trans i<j (<-respˡ-≈ (HL.≈-reflexive ≡.refl) j<k)) + where + open DTOP (HL.decTotalOrder (Edge.arity i)) using (<-respˡ-≈) renaming (<-trans to <-label-trans) +<-Edge-trans {k = k} (<-label ≡.refl i<j) (<-ports ≡.refl ≡.refl _) + = <-label ≡.refl (<-respʳ-≈ (≡.sym (HL.≈-reflexive ≡.refl)) i<j) + where + open DTOP (HL.decTotalOrder (Edge.arity k)) using (<-respʳ-≈) +<-Edge-trans (<-ports ≡.refl _ _) (<-arity j<k) = <-arity j<k +<-Edge-trans {k = k} (<-ports ≡.refl ≡.refl _) (<-label ≡.refl j<k) + = <-label ≡.refl (<-respˡ-≈ (≡.cong (cast _) (HL.≈-reflexive ≡.refl)) j<k) + where + open DTOP (HL.decTotalOrder (Edge.arity k)) using (<-respˡ-≈) +<-Edge-trans {j = j} (<-ports ≡.refl ≡l₁ i<j) (<-ports ≡.refl ≡l₂ j<k) + rewrite (VecCast.cast-is-id ≡.refl (Edge.ports j)) + = <-ports ≡.refl + (HL.≈-trans ≡l₁ ≡l₂) + (Lex.<-trans ≡-isPartialEquivalence FinProp.<-resp₂-≡ FinProp.<-trans i<j j<k) + where + open IsEquivalence ≡.isEquivalence using () renaming (isPartialEquivalence to ≡-isPartialEquivalence) + +<-Edge-respˡ-≈ : {v : ℕ} {y : Edge v} → (λ x → <-Edge x y) Respects ≈-Edge +<-Edge-respˡ-≈ ≈x (<-arity x₁<y) = <-arity (proj₂ <-resp₂-≡ ≡arity x₁<y) + where + open ≈-Edge ≈x using (≡arity) +<-Edge-respˡ-≈ {_} {y} record { ≡arity = ≡.refl ; ≡label = ≡.refl } (<-label ≡.refl x₁<y) + = <-label ≡.refl (<-respˡ-≈ (≡.sym (HL.≈-reflexive ≡.refl)) x₁<y) + where + module y = Edge y + open DTOP (HL.decTotalOrder y.arity) using (<-respˡ-≈) +<-Edge-respˡ-≈ record { ≡arity = ≡.refl ; ≡label = ≡.refl; ≡ports = ≡.refl} (<-ports ≡.refl ≡.refl x₁<y) + = <-ports + ≡.refl + (≡.cong (cast _) (HL.≈-reflexive ≡.refl)) + (Lex.<-respectsˡ + ≡-isPartialEquivalence + FinProp.<-respˡ-≡ + (≡⇒Pointwise-≡ (≡.sym (VecCast.≈-reflexive ≡.refl))) + x₁<y) + where + open IsEquivalence ≡.isEquivalence using () renaming (isPartialEquivalence to ≡-isPartialEquivalence) + +<-Edge-respʳ-≈ : {v : ℕ} {x : Edge v} → <-Edge x Respects ≈-Edge +<-Edge-respʳ-≈ record { ≡arity = ≡a } (<-arity x<y₁) = <-arity (proj₁ <-resp₂-≡ ≡a x<y₁) +<-Edge-respʳ-≈ {_} {x} record { ≡arity = ≡.refl ; ≡label = ≡.refl } (<-label ≡.refl x<y₁) + = <-label ≡.refl (<-respʳ-≈ (≡.sym (HL.≈-reflexive ≡.refl)) x<y₁) + where + module x = Edge x + open DTOP (HL.decTotalOrder x.arity) using (<-respʳ-≈) +<-Edge-respʳ-≈ record { ≡arity = ≡.refl ; ≡label = ≡.refl; ≡ports = ≡.refl} (<-ports ≡.refl ≡.refl x<y₁) + = <-ports + ≡.refl + (≡.cong (cast _) (≡.sym (HL.≈-reflexive ≡.refl))) + (Lex.<-respectsʳ + ≡-isPartialEquivalence + FinProp.<-respʳ-≡ + (≡⇒Pointwise-≡ (≡.sym (VecCast.≈-reflexive ≡.refl))) + x<y₁) + where + open IsEquivalence ≡.isEquivalence using () renaming (isPartialEquivalence to ≡-isPartialEquivalence) + +open Tri +open ≈-Edge +tri : {v : ℕ} → Trichotomous (≈-Edge {v}) (<-Edge {v}) +tri x y with <-cmp x.arity y.arity + where + module x = Edge x + module y = Edge y +tri x y | tri< x<y x≢y y≮x = tri< (<-arity x<y) (λ x≡y → x≢y (≡arity x≡y)) ¬y<x + where + ¬y<x : ¬ <-Edge y x + ¬y<x (<-arity y<x) = y≮x y<x + ¬y<x (<-label ≡a _) = x≢y (≡.sym ≡a) + ¬y<x (<-ports ≡a _ _) = x≢y (≡.sym ≡a) +tri x y | tri≈ x≮y ≡.refl y≮x = compare-label + where + module x = Edge x + module y = Edge y + open StrictTotalOrder (HL.strictTotalOrder x.arity) using (compare) + import Relation.Binary.Properties.DecTotalOrder + open DTOP (HL.decTotalOrder x.arity) using (<-respˡ-≈) + compare-label : Tri (<-Edge x y) (≈-Edge x y) (<-Edge y x) + compare-label with compare x.label y.label + ... | tri< x<y x≢y y≮x′ = tri< + (<-label ≡.refl (<-respˡ-≈ (≡.sym (HL.≈-reflexive ≡.refl)) x<y)) + (λ x≡y → x≢y (≡.trans (≡.sym (HL.≈-reflexive ≡.refl)) (≡label x≡y))) + ¬y<x + where + ¬y<x : ¬ <-Edge y x + ¬y<x (<-arity y<x) = y≮x y<x + ¬y<x (<-label _ y<x) = y≮x′ (<-respˡ-≈ (HL.≈-reflexive ≡.refl) y<x) + ¬y<x (<-ports _ ≡l _) = x≢y (≡.trans (≡.sym ≡l) (cast-is-id ≡.refl y.label)) + ... | tri≈ x≮y′ x≡y′ y≮x′ = compare-ports + where + compare-ports : Tri (<-Edge x y) (≈-Edge x y) (<-Edge y x) + compare-ports with Lex.<-cmp ≡.sym FinProp.<-cmp x.ports y.ports + ... | tri< x<y x≢y y≮x″ = + tri< + (<-ports ≡.refl + (HL.≈-reflexive x≡y′) + (Lex.<-respectsˡ + ≡-isPartialEquivalence + FinProp.<-respˡ-≡ + (≡⇒Pointwise-≡ (≡.sym (VecCast.≈-reflexive ≡.refl))) + x<y)) + (λ x≡y → x≢y (≡⇒Pointwise-≡ (≡.trans (≡.sym (VecCast.≈-reflexive ≡.refl)) (≡ports x≡y)))) + ¬y<x + where + open IsEquivalence ≡.isEquivalence using () renaming (isPartialEquivalence to ≡-isPartialEquivalence) + ¬y<x : ¬ <-Edge y x + ¬y<x (<-arity y<x) = y≮x y<x + ¬y<x (<-label _ y<x) = y≮x′ (<-respˡ-≈ (HL.≈-reflexive ≡.refl) y<x) + ¬y<x (<-ports _ _ y<x) = + y≮x″ + (Lex.<-respectsˡ + ≡-isPartialEquivalence + FinProp.<-respˡ-≡ + (≡⇒Pointwise-≡ (VecCast.≈-reflexive ≡.refl)) + y<x) + ... | tri≈ x≮y″ x≡y″ y≮x″ = tri≈ + ¬x<y + (record { ≡arity = ≡.refl ; ≡label = HL.≈-reflexive x≡y′ ; ≡ports = VecCast.≈-reflexive (Pointwise-≡⇒≡ x≡y″) }) + ¬y<x + where + open IsEquivalence ≡.isEquivalence using () renaming (isPartialEquivalence to ≡-isPartialEquivalence) + ¬x<y : ¬ <-Edge x y + ¬x<y (<-arity x<y) = x≮y x<y + ¬x<y (<-label _ x<y) = x≮y′ (<-respˡ-≈ (HL.≈-reflexive ≡.refl) x<y) + ¬x<y (<-ports _ _ x<y) = + x≮y″ + (Lex.<-respectsˡ + ≡-isPartialEquivalence + FinProp.<-respˡ-≡ + (≡⇒Pointwise-≡ (VecCast.≈-reflexive ≡.refl)) + x<y) + ¬y<x : ¬ <-Edge y x + ¬y<x (<-arity y<x) = y≮x y<x + ¬y<x (<-label _ y<x) = y≮x′ (<-respˡ-≈ (HL.≈-reflexive ≡.refl) y<x) + ¬y<x (<-ports _ _ y<x) = + y≮x″ + (Lex.<-respectsˡ + ≡-isPartialEquivalence + FinProp.<-respˡ-≡ + (≡⇒Pointwise-≡ (VecCast.≈-reflexive ≡.refl)) + y<x) + + ... | tri> x≮y″ x≢y y<x = + tri> + ¬x<y + (λ x≡y → x≢y (≡⇒Pointwise-≡ (≡.trans (≡.sym (VecCast.≈-reflexive ≡.refl)) (≡ports x≡y)))) + (<-ports + ≡.refl + (HL.≈-sym (HL.≈-reflexive x≡y′)) + (Lex.<-respectsˡ + ≡-isPartialEquivalence + FinProp.<-respˡ-≡ + (≡⇒Pointwise-≡ (≡.sym (VecCast.≈-reflexive ≡.refl))) + y<x)) + where + open IsEquivalence ≡.isEquivalence using () renaming (isPartialEquivalence to ≡-isPartialEquivalence) + ¬x<y : ¬ <-Edge x y + ¬x<y (<-arity x<y) = x≮y x<y + ¬x<y (<-label _ x<y) = x≮y′ (<-respˡ-≈ (HL.≈-reflexive ≡.refl) x<y) + ¬x<y (<-ports _ _ x<y) = + x≮y″ + (Lex.<-respectsˡ + ≡-isPartialEquivalence + FinProp.<-respˡ-≡ + (≡⇒Pointwise-≡ (VecCast.≈-reflexive ≡.refl)) + x<y) + ... | tri> x≮y′ x≢y y<x = tri> + ¬x<y + (λ x≡y → x≢y (≡.trans (≡.sym (HL.≈-reflexive ≡.refl)) (≡label x≡y))) + (<-label ≡.refl (<-respˡ-≈ (≡.sym (HL.≈-reflexive ≡.refl)) y<x)) + where + ¬x<y : ¬ <-Edge x y + ¬x<y (<-arity x<y) = x≮y x<y + ¬x<y (<-label ≡a x<y) = x≮y′ (<-respˡ-≈ (HL.≈-reflexive ≡.refl) x<y) + ¬x<y (<-ports _ ≡l _) = x≢y (≡.trans (≡.sym (HL.≈-reflexive ≡.refl)) ≡l) +tri x y | tri> x≮y x≢y y<x = tri> ¬x<y (λ x≡y → x≢y (≡arity x≡y)) (<-arity y<x) + where + ¬x<y : ¬ <-Edge x y + ¬x<y (<-arity x<y) = x≮y x<y + ¬x<y (<-label ≡a x<y) = x≢y ≡a + ¬x<y (<-ports ≡a _ _) = x≢y ≡a + +isStrictTotalOrder : {v : ℕ} → IsStrictTotalOrder (≈-Edge {v}) (<-Edge {v}) +isStrictTotalOrder = record + { isStrictPartialOrder = record + { isEquivalence = ≈-Edge-IsEquivalence + ; irrefl = <-Edge-irrefl + ; trans = <-Edge-trans + ; <-resp-≈ = <-Edge-respʳ-≈ , <-Edge-respˡ-≈ + } + ; compare = tri + } + +strictTotalOrder : {v : ℕ} → StrictTotalOrder 0ℓ 0ℓ 0ℓ +strictTotalOrder {v} = record + { Carrier = Edge v + ; _≈_ = ≈-Edge {v} + ; _<_ = <-Edge {v} + ; isStrictTotalOrder = isStrictTotalOrder {v} + } + +open module STOP′ {v} = STOP (strictTotalOrder {v}) using (decTotalOrder) public + +module Sort {v} = ListSort (decTotalOrder {v}) +open Sort using (sort) public diff --git a/Data/Hypergraph/Label.agda b/Data/Hypergraph/Label.agda new file mode 100644 index 0000000..ca95002 --- /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; 0ℓ) +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 : Set₁ where + + field + Label : ℕ → Set + showLabel : (n : ℕ) → Label n → String + isCastable : IsCastable Label + _[_≤_] : (n : ℕ) → Rel (Label n) 0ℓ + isDecTotalOrder : (n : ℕ) → IsDecTotalOrder _≡_ (n [_≤_]) + + decTotalOrder : (n : ℕ) → DecTotalOrder 0ℓ 0ℓ 0ℓ + decTotalOrder n = record + { Carrier = Label n + ; _≈_ = _≡_ + ; _≤_ = n [_≤_] + ; isDecTotalOrder = isDecTotalOrder n + } + + _[_<_] : (n : ℕ) → Rel (Label n) 0ℓ + _[_<_] n = _<_ (decTotalOrder n) + + strictTotalOrder : (n : ℕ) → StrictTotalOrder 0ℓ 0ℓ 0ℓ + strictTotalOrder n = <-strictTotalOrder (decTotalOrder n) + + open IsCastable isCastable public diff --git a/Data/Monoid.agda b/Data/Monoid.agda new file mode 100644 index 0000000..1ba0af4 --- /dev/null +++ b/Data/Monoid.agda @@ -0,0 +1,86 @@ +{-# OPTIONS --without-K --safe #-} + +open import Level using (Level) +module Data.Monoid {c ℓ : Level} where + +open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory) +open import Category.Instance.Setoids.SymmetricMonoidal {c} {ℓ} using (Setoids-×; ×-monoidal′) +open import Categories.Object.Monoid using (Monoid; Monoid⇒) + +import Algebra.Bundles as Alg + +open import Data.Setoid using (∣_∣) +open import Relation.Binary using (Setoid) +open import Function using (Func) +open import Data.Product using (curry′; uncurry′; _,_) +open Func + +-- A monoid object in the (monoidal) category of setoids is just a monoid + +open import Function.Construct.Constant using () renaming (function to Const) +open import Data.Setoid.Unit using (⊤ₛ) + +opaque + unfolding ×-monoidal′ + toMonoid : Monoid Setoids-×.monoidal → Alg.Monoid c ℓ + toMonoid M = record + { Carrier = Carrier + ; _≈_ = _≈_ + ; _∙_ = curry′ (to μ) + ; ε = to η _ + ; isMonoid = record + { isSemigroup = record + { isMagma = record + { isEquivalence = isEquivalence + ; ∙-cong = curry′ (cong μ) + } + ; assoc = λ x y z → assoc {(x , y) , z} + } + ; identity = (λ x → sym (identityˡ {_ , x}) ) , λ x → sym (identityʳ {x , _}) + } + } + where + open Monoid M renaming (Carrier to A) + open Setoid A + + fromMonoid : Alg.Monoid c ℓ → Monoid Setoids-×.monoidal + fromMonoid M = record + { Carrier = setoid + ; isMonoid = record + { μ = record { to = uncurry′ _∙_ ; cong = uncurry′ ∙-cong } + ; η = Const ⊤ₛ setoid ε + ; assoc = λ { {(x , y) , z} → assoc x y z } + ; identityˡ = λ { {_ , x} → sym (identityˡ x) } + ; identityʳ = λ { {x , _} → sym (identityʳ x) } + } + } + where + open Alg.Monoid M + +-- A morphism of monoids in the (monoidal) category of setoids is a monoid homomorphism + +module _ (M N : Monoid Setoids-×.monoidal) where + + module M = Alg.Monoid (toMonoid M) + module N = Alg.Monoid (toMonoid N) + + open import Data.Product using (Σ; _,_) + open import Function using (_⟶ₛ_) + open import Algebra.Morphism using (IsMonoidHomomorphism) + open Monoid⇒ + + opaque + + unfolding toMonoid + + toMonoid⇒ + : Monoid⇒ Setoids-×.monoidal M N + → Σ (M.setoid ⟶ₛ N.setoid) (λ f + → IsMonoidHomomorphism M.rawMonoid N.rawMonoid (to f)) + toMonoid⇒ f = arr f , record + { isMagmaHomomorphism = record + { isRelHomomorphism = record { cong = cong (arr f) } + ; homo = λ x y → preserves-μ f {x , y} + } + ; ε-homo = preserves-η f + } diff --git a/Data/Opaque/List.agda b/Data/Opaque/List.agda new file mode 100644 index 0000000..83a2fe3 --- /dev/null +++ b/Data/Opaque/List.agda @@ -0,0 +1,165 @@ +{-# OPTIONS --without-K --safe #-} + +module Data.Opaque.List where + +import Data.List as L +import Function.Construct.Constant as Const +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning + +open import Algebra.Bundles using (Monoid) +open import Algebra.Morphism using (IsMonoidHomomorphism) +open import Data.List.Effectful.Foldable using (foldable; ++-homo) +open import Data.List.Relation.Binary.Pointwise as PW using (++⁺; map⁺) +open import Data.Product using (_,_; curry′; uncurry′) +open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_) +open import Data.Setoid using (∣_∣) +open import Data.Unit.Polymorphic using (⊤) +open import Effect.Foldable using (RawFoldable) +open import Function using (_⟶ₛ_; Func; _⟨$⟩_; id) +open import Level using (Level; _⊔_) +open import Relation.Binary using (Setoid) + +open Func + +private + + variable + a c ℓ : Level + A B : Set a + Aₛ Bₛ : Setoid c ℓ + + ⊤ₛ : Setoid c ℓ + ⊤ₛ = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ } + +opaque + + List : Set a → Set a + List = L.List + + [] : List A + [] = L.[] + + _∷_ : A → List A → List A + _∷_ = L._∷_ + + map : (A → B) → List A → List B + map = L.map + + _++_ : List A → List A → List A + _++_ = L._++_ + + Listₛ : Setoid c ℓ → Setoid c (c ⊔ ℓ) + Listₛ = PW.setoid + + []ₛ : ⊤ₛ {c} {c ⊔ ℓ} ⟶ₛ Listₛ {c} {ℓ} Aₛ + []ₛ = Const.function ⊤ₛ (Listₛ _) [] + + ∷ₛ : Aₛ ×ₛ Listₛ Aₛ ⟶ₛ Listₛ Aₛ + ∷ₛ .to = uncurry′ _∷_ + ∷ₛ .cong = uncurry′ PW._∷_ + + [-]ₛ : Aₛ ⟶ₛ Listₛ Aₛ + [-]ₛ .to = L.[_] + [-]ₛ .cong y = y PW.∷ PW.[] + + mapₛ : (Aₛ ⟶ₛ Bₛ) → Listₛ Aₛ ⟶ₛ Listₛ Bₛ + mapₛ f .to = map (to f) + mapₛ f .cong xs≈ys = map⁺ (to f) (to f) (PW.map (cong f) xs≈ys) + + cartesianProduct : ∣ Listₛ Aₛ ∣ → ∣ Listₛ Bₛ ∣ → ∣ Listₛ (Aₛ ×ₛ Bₛ) ∣ + cartesianProduct = L.cartesianProduct + + cartesian-product-cong + : {xs xs′ : ∣ Listₛ Aₛ ∣} + {ys ys′ : ∣ Listₛ Bₛ ∣} + → (let open Setoid (Listₛ Aₛ) in xs ≈ xs′) + → (let open Setoid (Listₛ Bₛ) in ys ≈ ys′) + → (let open Setoid (Listₛ (Aₛ ×ₛ Bₛ)) in cartesianProduct xs ys ≈ cartesianProduct xs′ ys′) + cartesian-product-cong PW.[] ys≋ys′ = PW.[] + cartesian-product-cong {Aₛ = Aₛ} {Bₛ = Bₛ} {xs = x₀ L.∷ xs} {xs′ = x₀′ L.∷ xs′} (x₀≈x₀′ PW.∷ xs≋xs′) ys≋ys′ = + ++⁺ + (map⁺ (x₀ ,_) (x₀′ ,_) (PW.map (x₀≈x₀′ ,_) ys≋ys′)) + (cartesian-product-cong {Aₛ = Aₛ} {Bₛ = Bₛ} xs≋xs′ ys≋ys′) + + pairsₛ : Listₛ Aₛ ×ₛ Listₛ Bₛ ⟶ₛ Listₛ (Aₛ ×ₛ Bₛ) + pairsₛ .to = uncurry′ L.cartesianProduct + pairsₛ {Aₛ = Aₛ} {Bₛ = Bₛ} .cong = uncurry′ (cartesian-product-cong {Aₛ = Aₛ} {Bₛ = Bₛ}) + + ++ₛ : Listₛ Aₛ ×ₛ Listₛ Aₛ ⟶ₛ Listₛ Aₛ + ++ₛ .to = uncurry′ _++_ + ++ₛ .cong = uncurry′ ++⁺ + + foldr : (Aₛ ×ₛ Bₛ ⟶ₛ Bₛ) → ∣ Bₛ ∣ → ∣ Listₛ Aₛ ∣ → ∣ Bₛ ∣ + foldr f = L.foldr (curry′ (to f)) + + foldr-cong + : (f : Aₛ ×ₛ Bₛ ⟶ₛ Bₛ) + → (e : ∣ Bₛ ∣) + → (let module [A]ₛ = Setoid (Listₛ Aₛ)) + → {xs ys : ∣ Listₛ Aₛ ∣} + → (xs [A]ₛ.≈ ys) + → (open Setoid Bₛ) + → foldr f e xs ≈ foldr f e ys + foldr-cong {Bₛ = Bₛ} f e PW.[] = Setoid.refl Bₛ + foldr-cong f e (x≈y PW.∷ xs≋ys) = cong f (x≈y , foldr-cong f e xs≋ys) + + foldrₛ : (Aₛ ×ₛ Bₛ ⟶ₛ Bₛ) → ∣ Bₛ ∣ → Listₛ Aₛ ⟶ₛ Bₛ + foldrₛ f e .to = foldr f e + foldrₛ {Bₛ = Bₛ} f e .cong = foldr-cong f e + +module _ (M : Monoid c ℓ) where + + open Monoid M renaming (setoid to Mₛ) + + opaque + unfolding List + fold : ∣ Listₛ Mₛ ∣ → ∣ Mₛ ∣ + fold = RawFoldable.fold foldable rawMonoid + + fold-cong + : {xs ys : ∣ Listₛ Mₛ ∣} + → (let module [M]ₛ = Setoid (Listₛ Mₛ)) + → (xs [M]ₛ.≈ ys) + → fold xs ≈ fold ys + fold-cong = PW.rec (λ {xs} {ys} _ → fold xs ≈ fold ys) ∙-cong refl + + foldₛ : Listₛ Mₛ ⟶ₛ Mₛ + foldₛ .to = fold + foldₛ .cong = fold-cong + + opaque + unfolding fold + ++ₛ-homo + : (xs ys : ∣ Listₛ Mₛ ∣) + → foldₛ ⟨$⟩ (++ₛ ⟨$⟩ (xs , ys)) ≈ (foldₛ ⟨$⟩ xs) ∙ (foldₛ ⟨$⟩ ys) + ++ₛ-homo xs ys = ++-homo M id xs + + []ₛ-homo : foldₛ ⟨$⟩ ([]ₛ ⟨$⟩ _) ≈ ε + []ₛ-homo = refl + +module _ (M N : Monoid c ℓ) where + + module M = Monoid M + module N = Monoid N + + open IsMonoidHomomorphism + + opaque + unfolding fold + + fold-mapₛ + : (f : M.setoid ⟶ₛ N.setoid) + → IsMonoidHomomorphism M.rawMonoid N.rawMonoid (to f) + → {xs : ∣ Listₛ M.setoid ∣} + → foldₛ N ⟨$⟩ (mapₛ f ⟨$⟩ xs) N.≈ f ⟨$⟩ (foldₛ M ⟨$⟩ xs) + fold-mapₛ f isMH {L.[]} = N.sym (ε-homo isMH) + fold-mapₛ f isMH {x L.∷ xs} = begin + f′ x ∙ fold N (map f′ xs) ≈⟨ N.∙-cong N.refl (fold-mapₛ f isMH {xs}) ⟩ + f′ x ∙ f′ (fold M xs) ≈⟨ homo isMH x (fold M xs) ⟨ + f′ (x ∘ fold M xs) ∎ + where + open N using (_∙_) + open M using () renaming (_∙_ to _∘_) + open ≈-Reasoning N.setoid + f′ : M.Carrier → N.Carrier + f′ = to f diff --git a/Data/Opaque/Multiset.agda b/Data/Opaque/Multiset.agda new file mode 100644 index 0000000..99501d6 --- /dev/null +++ b/Data/Opaque/Multiset.agda @@ -0,0 +1,131 @@ +{-# OPTIONS --without-K --safe #-} +{-# OPTIONS --hidden-argument-puns #-} + +module Data.Opaque.Multiset where + +import Data.List as L +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning +import Data.Opaque.List as List + +open import Algebra.Bundles using (CommutativeMonoid) +open import Data.List.Effectful.Foldable using (foldable; ++-homo) +open import Data.List.Relation.Binary.Permutation.Setoid as ↭ using (↭-setoid; ↭-refl) +open import Data.List.Relation.Binary.Permutation.Setoid.Properties using (map⁺; ++⁺; ++-comm) +open import Algebra.Morphism using (IsMonoidHomomorphism) +open import Data.Product using (_,_; uncurry′) +open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_) +open import Data.Setoid using (∣_∣) +open import Data.Setoid.Unit using (⊤ₛ) +open import Effect.Foldable using (RawFoldable) +open import Function using (_⟶ₛ_; Func; _⟨$⟩_; id) +open import Function.Construct.Constant using () renaming (function to Const) +open import Level using (Level; _⊔_) +open import Relation.Binary using (Setoid) + +open Func + +private + + variable + a c ℓ : Level + A B : Set a + Aₛ Bₛ : Setoid c ℓ + +opaque + + Multiset : Set a → Set a + Multiset = L.List + + [] : Multiset A + [] = L.[] + + _∷_ : A → Multiset A → Multiset A + _∷_ = L._∷_ + + map : (A → B) → Multiset A → Multiset B + map = L.map + + _++_ : Multiset A → Multiset A → Multiset A + _++_ = L._++_ + + Multisetₛ : Setoid c ℓ → Setoid c (c ⊔ ℓ) + Multisetₛ = ↭-setoid + + []ₛ : ⊤ₛ {c} {c ⊔ ℓ} ⟶ₛ Multisetₛ {c} {ℓ} Aₛ + []ₛ {Aₛ} = Const ⊤ₛ (Multisetₛ Aₛ) [] + + ∷ₛ : Aₛ ×ₛ Multisetₛ Aₛ ⟶ₛ Multisetₛ Aₛ + ∷ₛ .to = uncurry′ _∷_ + ∷ₛ .cong = uncurry′ ↭.prep + + [-]ₛ : Aₛ ⟶ₛ Multisetₛ Aₛ + [-]ₛ .to = L.[_] + [-]ₛ {Aₛ} .cong y = ↭.prep y (↭-refl Aₛ) + + mapₛ : (Aₛ ⟶ₛ Bₛ) → Multisetₛ Aₛ ⟶ₛ Multisetₛ Bₛ + mapₛ f .to = map (to f) + mapₛ {Aₛ} {Bₛ} f .cong xs≈ys = map⁺ Aₛ Bₛ (cong f) xs≈ys + + ++ₛ : Multisetₛ Aₛ ×ₛ Multisetₛ Aₛ ⟶ₛ Multisetₛ Aₛ + ++ₛ .to = uncurry′ _++_ + ++ₛ {Aₛ} .cong = uncurry′ (++⁺ Aₛ) + + ++ₛ-comm + : (open Setoid (Multisetₛ Aₛ)) + → (xs ys : Carrier) + → ++ₛ ⟨$⟩ (xs , ys) ≈ ++ₛ ⟨$⟩ (ys , xs) + ++ₛ-comm {Aₛ} xs ys = ++-comm Aₛ xs ys + +module _ (M : CommutativeMonoid c ℓ) where + + open CommutativeMonoid M renaming (setoid to Mₛ) + + opaque + unfolding Multiset List.fold-cong + fold : ∣ Multisetₛ Mₛ ∣ → ∣ Mₛ ∣ + fold = List.fold monoid -- RawFoldable.fold foldable rawMonoid + + fold-cong + : {xs ys : ∣ Multisetₛ Mₛ ∣} + → (let module [M]ₛ = Setoid (Multisetₛ Mₛ)) + → (xs [M]ₛ.≈ ys) + → fold xs ≈ fold ys + fold-cong (↭.refl x) = cong (List.foldₛ monoid) x + fold-cong (↭.prep x≈y xs↭ys) = ∙-cong x≈y (fold-cong xs↭ys) + fold-cong + {x₀ L.∷ x₁ L.∷ xs} + {y₀ L.∷ y₁ L.∷ ys} + (↭.swap x₀≈y₁ x₁≈y₀ xs↭ys) = trans + (sym (assoc x₀ x₁ (fold xs))) (trans + (∙-cong (trans (∙-cong x₀≈y₁ x₁≈y₀) (comm y₁ y₀)) (fold-cong xs↭ys)) + (assoc y₀ y₁ (fold ys))) + fold-cong {xs} {ys} (↭.trans xs↭zs zs↭ys) = trans (fold-cong xs↭zs) (fold-cong zs↭ys) + + foldₛ : Multisetₛ Mₛ ⟶ₛ Mₛ + foldₛ .to = fold + foldₛ .cong = fold-cong + + opaque + unfolding fold + ++ₛ-homo + : (xs ys : ∣ Multisetₛ Mₛ ∣) + → foldₛ ⟨$⟩ (++ₛ ⟨$⟩ (xs , ys)) ≈ (foldₛ ⟨$⟩ xs) ∙ (foldₛ ⟨$⟩ ys) + ++ₛ-homo xs ys = ++-homo monoid id xs + + []ₛ-homo : foldₛ ⟨$⟩ ([]ₛ ⟨$⟩ _) ≈ ε + []ₛ-homo = refl + +module _ (M N : CommutativeMonoid c ℓ) where + + module M = CommutativeMonoid M + module N = CommutativeMonoid N + + opaque + unfolding fold + + fold-mapₛ + : (f : M.setoid ⟶ₛ N.setoid) + → IsMonoidHomomorphism M.rawMonoid N.rawMonoid (to f) + → {xs : ∣ Multisetₛ M.setoid ∣} + → foldₛ N ⟨$⟩ (mapₛ f ⟨$⟩ xs) N.≈ f ⟨$⟩ (foldₛ M ⟨$⟩ xs) + fold-mapₛ = List.fold-mapₛ M.monoid N.monoid diff --git a/Data/Permutation.agda b/Data/Permutation.agda new file mode 100644 index 0000000..55c8748 --- /dev/null +++ b/Data/Permutation.agda @@ -0,0 +1,217 @@ +{-# 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-↭ + : {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 ∎ diff --git a/Data/Permutation/Sort.agda b/Data/Permutation/Sort.agda new file mode 100644 index 0000000..8d097f2 --- /dev/null +++ b/Data/Permutation/Sort.agda @@ -0,0 +1,29 @@ +{-# 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) renaming (Carrier to A) + +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 = ↗↭↗⇒≋ totalOrder (sort-↗ xs) (sort-↗ ys) sort-xs↭sort-ys + where + 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 ∎ diff --git a/Data/SExp.agda b/Data/SExp.agda new file mode 100644 index 0000000..adf4325 --- /dev/null +++ b/Data/SExp.agda @@ -0,0 +1,75 @@ +{-# OPTIONS --without-K --safe #-} + +module Data.SExp where + +open import Data.List using (List) +open import Data.Nat.Base using (ℕ) +open import Data.Nat.Show using () renaming (show to showNat) +open import Data.String.Base as String using (String; parens; intersperse; _<+>_) + +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 diff --git a/Data/Setoid.agda b/Data/Setoid.agda new file mode 100644 index 0000000..454d276 --- /dev/null +++ b/Data/Setoid.agda @@ -0,0 +1,8 @@ +{-# OPTIONS --without-K --safe #-} + +module Data.Setoid where + +open import Relation.Binary using (Setoid) +open import Function.Construct.Setoid using () renaming (setoid to infixr 0 _⇒ₛ_) public + +open Setoid renaming (Carrier to ∣_∣) public diff --git a/Data/Setoid/Unit.agda b/Data/Setoid/Unit.agda new file mode 100644 index 0000000..8b8edde --- /dev/null +++ b/Data/Setoid/Unit.agda @@ -0,0 +1,11 @@ +{-# OPTIONS --without-K --safe #-} + +open import Level using (Level) + +module Data.Setoid.Unit {c ℓ : Level} where + +open import Categories.Category.Instance.SingletonSet using (SingletonSetoid) +open import Relation.Binary using (Setoid) + +⊤ₛ : Setoid c ℓ +⊤ₛ = SingletonSetoid {c} {ℓ} diff --git a/Data/Subset/Functional.agda b/Data/Subset/Functional.agda new file mode 100644 index 0000000..33a6d8e --- /dev/null +++ b/Data/Subset/Functional.agda @@ -0,0 +1,162 @@ +{-# OPTIONS --without-K --safe #-} + +module Data.Subset.Functional where + +open import Data.Bool.Base using (Bool; _∨_; _∧_; if_then_else_) +open import Data.Bool.Properties using (if-float) +open import Data.Fin.Base using (Fin) +open import Data.Fin.Permutation using (Permutation′; _⟨$⟩ʳ_; _⟨$⟩ˡ_; inverseˡ; inverseʳ) +open import Data.Fin.Properties using (suc-injective; 0≢1+n) +open import Data.Nat.Base using (ℕ) +open import Function.Base using (∣_⟩-_; _∘_) +open import Function.Definitions using (Injective) +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_; _≢_) +open import Data.Vector as V using (Vector; head; tail) + +open Bool +open Fin +open ℕ + +Subset : ℕ → Set +Subset = Vector Bool + +private + variable n A : ℕ + variable B C : Set + +⊥ : Subset n +⊥ _ = false + +_∪_ : Subset n → Subset n → Subset n +(A ∪ B) k = A k ∨ B k + +_∩_ : Subset n → Subset n → Subset n +(A ∩ B) k = A k ∧ B k + +⁅_⁆ : Fin n → Subset n +⁅_⁆ zero zero = true +⁅_⁆ zero (suc _) = false +⁅_⁆ (suc k) zero = false +⁅_⁆ (suc k) (suc i) = ⁅ k ⁆ i + +⁅⁆-refl : (k : Fin n) → ⁅ k ⁆ k ≡ true +⁅⁆-refl zero = ≡.refl +⁅⁆-refl (suc k) = ⁅⁆-refl k + +⁅x⁆y≡true + : (x y : Fin n) + → .(⁅ x ⁆ y ≡ true) + → x ≡ y +⁅x⁆y≡true zero zero prf = ≡.refl +⁅x⁆y≡true (suc x) (suc y) prf = ≡.cong suc (⁅x⁆y≡true x y prf) + +⁅x⁆y≡false + : (x y : Fin n) + → .(⁅ x ⁆ y ≡ false) + → x ≢ y +⁅x⁆y≡false zero (suc y) prf = 0≢1+n +⁅x⁆y≡false (suc x) zero prf = 0≢1+n ∘ ≡.sym +⁅x⁆y≡false (suc x) (suc y) prf = ⁅x⁆y≡false x y prf ∘ suc-injective + +f-⁅⁆ + : {n m : ℕ} + (f : Fin n → Fin m) + → Injective _≡_ _≡_ f + → (x y : Fin n) + → ⁅ x ⁆ y ≡ ⁅ f x ⁆ (f y) +f-⁅⁆ f f-inj zero zero = ≡.sym (⁅⁆-refl (f zero)) +f-⁅⁆ f f-inj zero (suc y) with ⁅ f zero ⁆ (f (suc y)) in eq +... | true with () ← f-inj (⁅x⁆y≡true (f zero) (f (suc y)) eq) +... | false = ≡.refl +f-⁅⁆ f f-inj (suc x) zero with ⁅ f (suc x) ⁆ (f zero) in eq +... | true with () ← f-inj (⁅x⁆y≡true (f (suc x)) (f zero) eq) +... | false = ≡.refl +f-⁅⁆ f f-inj (suc x) (suc y) = f-⁅⁆ (f ∘ suc) (suc-injective ∘ f-inj) x y + +⁅⁆∘ρ + : (ρ : Permutation′ (suc n)) + (x : Fin (suc n)) + → ⁅ ρ ⟨$⟩ʳ x ⁆ ≗ ⁅ x ⁆ ∘ (ρ ⟨$⟩ˡ_) +⁅⁆∘ρ {n} ρ x y = begin + ⁅ ρ ⟨$⟩ʳ x ⁆ y ≡⟨ f-⁅⁆ (ρ ⟨$⟩ˡ_) ρˡ-inj (ρ ⟨$⟩ʳ x) y ⟩ + ⁅ ρ ⟨$⟩ˡ (ρ ⟨$⟩ʳ x) ⁆ (ρ ⟨$⟩ˡ y) ≡⟨ ≡.cong (λ h → ⁅ h ⁆ (ρ ⟨$⟩ˡ y)) (inverseˡ ρ) ⟩ + ⁅ x ⁆ (ρ ⟨$⟩ˡ y) ∎ + where + open ≡.≡-Reasoning + ρˡ-inj : {x y : Fin (suc n)} → ρ ⟨$⟩ˡ x ≡ ρ ⟨$⟩ˡ y → x ≡ y + ρˡ-inj {x} {y} ρˡx≡ρˡy = begin + x ≡⟨ inverseʳ ρ ⟨ + ρ ⟨$⟩ʳ (ρ ⟨$⟩ˡ x) ≡⟨ ≡.cong (ρ ⟨$⟩ʳ_) ρˡx≡ρˡy ⟩ + ρ ⟨$⟩ʳ (ρ ⟨$⟩ˡ y) ≡⟨ inverseʳ ρ ⟩ + y ∎ + +opaque + -- TODO dependent fold + foldl : (B → Fin A → B) → B → Subset A → B + foldl {B = B} f = V.foldl (λ _ → B) (λ { {k} acc b → if b then f acc k else acc }) + + foldl-cong₁ + : {f g : B → Fin A → B} + → (∀ x y → f x y ≡ g x y) + → (e : B) + → (S : Subset A) + → foldl f e S ≡ foldl g e S + foldl-cong₁ {B = B} f≗g e S = V.foldl-cong (λ _ → B) (λ { {k} x y → ≡.cong (if y then_else x) (f≗g x k) }) e S + + foldl-cong₂ + : (f : B → Fin A → B) + (e : B) + {S₁ S₂ : Subset A} + → (S₁ ≗ S₂) + → foldl f e S₁ ≡ foldl f e S₂ + foldl-cong₂ {B = B} f e S₁≗S₂ = V.foldl-cong-arg (λ _ → B) (λ {n} acc b → if b then f acc n else acc) e S₁≗S₂ + + foldl-suc + : (f : B → Fin (suc A) → B) + → (e : B) + → (S : Subset (suc A)) + → foldl f e S ≡ foldl (∣ f ⟩- suc) (if head S then f e zero else e) (tail S) + foldl-suc f e S = ≡.refl + + foldl-⊥ + : {A : ℕ} + {B : Set} + (f : B → Fin A → B) + (e : B) + → foldl f e ⊥ ≡ e + foldl-⊥ {zero} _ _ = ≡.refl + foldl-⊥ {suc A} f e = foldl-⊥ (∣ f ⟩- suc) e + + foldl-⁅⁆ + : (f : B → Fin A → B) + (e : B) + (k : Fin A) + → foldl f e ⁅ k ⁆ ≡ f e k + foldl-⁅⁆ f e zero = foldl-⊥ f (f e zero) + foldl-⁅⁆ f e (suc k) = foldl-⁅⁆ (∣ f ⟩- suc) e k + + foldl-fusion + : (h : C → B) + {f : C → Fin A → C} + {g : B → Fin A → B} + → (∀ x n → h (f x n) ≡ g (h x) n) + → (e : C) + → h ∘ foldl f e ≗ foldl g (h e) + foldl-fusion {C = C} {A = A} h {f} {g} fuse e = V.foldl-fusion h ≡.refl fuse′ + where + open ≡.≡-Reasoning + fuse′ + : {k : Fin A} + (acc : C) + (b : Bool) + → h (if b then f acc k else acc) ≡ (if b then g (h acc) k else h acc) + fuse′ {k} acc b = begin + h (if b then f acc k else acc) ≡⟨ if-float h b ⟩ + (if b then h (f acc k) else h acc) ≡⟨ ≡.cong (if b then_else h acc) (fuse acc k) ⟩ + (if b then g (h acc) k else h acc) ∎ + +Subset0≗⊥ : (S : Subset 0) → S ≗ ⊥ +Subset0≗⊥ S () + +foldl-[] : (f : B → Fin 0 → B) (e : B) (S : Subset 0) → foldl f e S ≡ e +foldl-[] f e S = ≡.trans (foldl-cong₂ f e (Subset0≗⊥ S)) (foldl-⊥ f e) diff --git a/Data/System.agda b/Data/System.agda new file mode 100644 index 0000000..d71c2a8 --- /dev/null +++ b/Data/System.agda @@ -0,0 +1,144 @@ +{-# OPTIONS --without-K --safe #-} + +open import Level using (Level; 0ℓ; suc) + +module Data.System {ℓ : Level} where + +import Relation.Binary.Properties.Preorder as PreorderProperties +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning + +open import Categories.Category using (Category) +open import Data.Circuit.Value using (Monoid) +open import Data.Nat using (ℕ) +open import Data.Setoid using (_⇒ₛ_; ∣_∣) +open import Data.Setoid.Unit using (⊤ₛ) +open import Data.System.Values Monoid using (Values; _≋_; module ≋; <ε>) +open import Function using (Func; _⟨$⟩_; flip) +open import Function.Construct.Constant using () renaming (function to Const) +open import Function.Construct.Identity using () renaming (function to Id) +open import Function.Construct.Setoid using (_∙_) +open import Level using (Level; 0ℓ; suc) +open import Relation.Binary as Rel using (Reflexive; Transitive; Preorder; Setoid; Rel) +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_) + +open Func + +module _ (n : ℕ) where + + record System : Set₁ where + + field + S : Setoid 0ℓ 0ℓ + fₛ : ∣ Values n ⇒ₛ S ⇒ₛ S ∣ + fₒ : ∣ S ⇒ₛ Values n ∣ + + fₛ′ : ∣ Values n ∣ → ∣ S ∣ → ∣ S ∣ + fₛ′ i = to (to fₛ i) + + fₒ′ : ∣ S ∣ → ∣ Values n ∣ + fₒ′ = to fₒ + + module S = Setoid S + + open System + + discrete : System + discrete .S = ⊤ₛ + discrete .fₛ = Const (Values n) (⊤ₛ ⇒ₛ ⊤ₛ) (Id ⊤ₛ) + discrete .fₒ = Const ⊤ₛ (Values n) <ε> + +module _ {n : ℕ} where + + record _≤_ (a b : System n) : Set ℓ where + + private + module A = System a + module B = System b + + open B using (S) + + field + ⇒S : ∣ A.S ⇒ₛ B.S ∣ + ≗-fₛ : (i : ∣ Values n ∣) (s : ∣ A.S ∣) → ⇒S ⟨$⟩ (A.fₛ′ i s) S.≈ B.fₛ′ i (⇒S ⟨$⟩ s) + ≗-fₒ : (s : ∣ A.S ∣) → A.fₒ′ s ≋ B.fₒ′ (⇒S ⟨$⟩ s) + + infix 4 _≤_ + +open System + +private + + module _ {n : ℕ} where + + open _≤_ + + ≤-refl : Reflexive (_≤_ {n}) + ⇒S ≤-refl = Id _ + ≗-fₛ (≤-refl {x}) _ _ = S.refl x + ≗-fₒ ≤-refl _ = ≋.refl + + ≡⇒≤ : _≡_ Rel.⇒ _≤_ + ≡⇒≤ ≡.refl = ≤-refl + + ≤-trans : Transitive _≤_ + ⇒S (≤-trans a b) = ⇒S b ∙ ⇒S a + ≗-fₛ (≤-trans {x} {y} {z} a b) i s = let open ≈-Reasoning (S z) in begin + ⇒S b ⟨$⟩ (⇒S a ⟨$⟩ (fₛ′ x i s)) ≈⟨ cong (⇒S b) (≗-fₛ a i s) ⟩ + ⇒S b ⟨$⟩ (fₛ′ y i (⇒S a ⟨$⟩ s)) ≈⟨ ≗-fₛ b i (⇒S a ⟨$⟩ s) ⟩ + fₛ′ z i (⇒S b ⟨$⟩ (⇒S a ⟨$⟩ s)) ∎ + ≗-fₒ (≤-trans {x} {y} {z} a b) s = let open ≈-Reasoning (Values n) in begin + fₒ′ x s ≈⟨ ≗-fₒ a s ⟩ + fₒ′ y (⇒S a ⟨$⟩ s) ≈⟨ ≗-fₒ b (⇒S a ⟨$⟩ s) ⟩ + fₒ′ z (⇒S b ⟨$⟩ (⇒S a ⟨$⟩ s)) ∎ + + variable + A B C : System n + + _≈_ : Rel (A ≤ B) 0ℓ + _≈_ {A} {B} ≤₁ ≤₂ = ⇒S ≤₁ A⇒B.≈ ⇒S ≤₂ + where + module A⇒B = Setoid (S A ⇒ₛ S B) + + open Rel.IsEquivalence + + ≈-isEquiv : Rel.IsEquivalence (_≈_ {A} {B}) + ≈-isEquiv {B = B} .refl = S.refl B + ≈-isEquiv {B = B} .sym a = S.sym B a + ≈-isEquiv {B = B} .trans a b = S.trans B a b + + ≤-resp-≈ : {f h : B ≤ C} {g i : A ≤ B} → f ≈ h → g ≈ i → ≤-trans g f ≈ ≤-trans i h + ≤-resp-≈ {_} {C} {_} {f} {h} {g} {i} f≈h g≈i {x} = begin + ⇒S f ⟨$⟩ (⇒S g ⟨$⟩ x) ≈⟨ f≈h ⟩ + ⇒S h ⟨$⟩ (⇒S g ⟨$⟩ x) ≈⟨ cong (⇒S h) g≈i ⟩ + ⇒S h ⟨$⟩ (⇒S i ⟨$⟩ x) ∎ + where + open ≈-Reasoning (System.S C) + +System-≤ : ℕ → Preorder (suc 0ℓ) (suc 0ℓ) ℓ +System-≤ n = record + { _≲_ = _≤_ {n} + ; isPreorder = record + { isEquivalence = ≡.isEquivalence + ; reflexive = ≡⇒≤ + ; trans = ≤-trans + } + } + +Systemₛ : ℕ → Setoid (suc 0ℓ) ℓ +Systemₛ n = PreorderProperties.InducedEquivalence (System-≤ n) + +Systems : ℕ → Category (suc 0ℓ) ℓ 0ℓ +Systems n = record + { Obj = System n + ; _⇒_ = _≤_ + ; _≈_ = _≈_ + ; id = ≤-refl + ; _∘_ = flip ≤-trans + ; assoc = λ {D = D} → S.refl D + ; sym-assoc = λ {D = D} → S.refl D + ; identityˡ = λ {B = B} → S.refl B + ; identityʳ = λ {B = B} → S.refl B + ; identity² = λ {A = A} → S.refl A + ; equiv = ≈-isEquiv + ; ∘-resp-≈ = λ {f = f} {h} {g} {i} → ≤-resp-≈ {f = f} {h} {g} {i} + } diff --git a/Data/System/Values.agda b/Data/System/Values.agda new file mode 100644 index 0000000..545a835 --- /dev/null +++ b/Data/System/Values.agda @@ -0,0 +1,146 @@ +{-# OPTIONS --without-K --safe #-} + +open import Algebra.Bundles using (CommutativeMonoid) +open import Level using (0ℓ) + +module Data.System.Values (A : CommutativeMonoid 0ℓ 0ℓ) where + +import Algebra.Properties.CommutativeMonoid.Sum as Sum +import Data.Vec.Functional.Relation.Binary.Equality.Setoid as Pointwise +import Relation.Binary.PropositionalEquality as ≡ + +open import Data.Fin using (_↑ˡ_; _↑ʳ_; zero; suc; splitAt) +open import Data.Nat using (ℕ; _+_; suc) +open import Data.Product using (_,_) +open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_) +open import Data.Setoid using (∣_∣) +open import Data.Sum using (inj₁; inj₂) +open import Data.Vec.Functional as Vec using (Vector; zipWith; replicate) +open import Function using (Func; _⟶ₛ_; _⟨$⟩_; _∘_) +open import Level using (0ℓ) +open import Relation.Binary using (Rel; Setoid; IsEquivalence) + +open CommutativeMonoid A renaming (Carrier to Value) +open Func +open Sum A using (sum) + +open Pointwise setoid using (≋-setoid; ≋-isEquivalence) + +opaque + + Values : ℕ → Setoid 0ℓ 0ℓ + Values = ≋-setoid + +module _ {n : ℕ} where + + opaque + + unfolding Values + + merge : ∣ Values n ∣ → Value + merge = sum + + _⊕_ : ∣ Values n ∣ → ∣ Values n ∣ → ∣ Values n ∣ + xs ⊕ ys = zipWith _∙_ xs ys + + <ε> : ∣ Values n ∣ + <ε> = replicate n ε + + head : ∣ Values (suc n) ∣ → Value + head xs = xs zero + + tail : ∣ Values (suc n) ∣ → ∣ Values n ∣ + tail xs = xs ∘ suc + + module ≋ = Setoid (Values n) + + _≋_ : Rel ∣ Values n ∣ 0ℓ + _≋_ = ≋._≈_ + + infix 4 _≋_ + +opaque + + unfolding Values + open Setoid + ≋-isEquiv : ∀ n → IsEquivalence (_≈_ (Values n)) + ≋-isEquiv = ≋-isEquivalence + +module _ {n : ℕ} where + + opaque + unfolding _⊕_ + + ⊕-cong : {x y u v : ≋.Carrier {n}} → x ≋ y → u ≋ v → x ⊕ u ≋ y ⊕ v + ⊕-cong x≋y u≋v i = ∙-cong (x≋y i) (u≋v i) + + ⊕-assoc : (x y z : ≋.Carrier {n}) → (x ⊕ y) ⊕ z ≋ x ⊕ (y ⊕ z) + ⊕-assoc x y z i = assoc (x i) (y i) (z i) + + ⊕-identityˡ : (x : ≋.Carrier {n}) → <ε> ⊕ x ≋ x + ⊕-identityˡ x i = identityˡ (x i) + + ⊕-identityʳ : (x : ≋.Carrier {n}) → x ⊕ <ε> ≋ x + ⊕-identityʳ x i = identityʳ (x i) + + ⊕-comm : (x y : ≋.Carrier {n}) → x ⊕ y ≋ y ⊕ x + ⊕-comm x y i = comm (x i) (y i) + +open CommutativeMonoid +Valuesₘ : ℕ → CommutativeMonoid 0ℓ 0ℓ +Valuesₘ n .Carrier = ∣ Values n ∣ +Valuesₘ n ._≈_ = _≋_ +Valuesₘ n ._∙_ = _⊕_ +Valuesₘ n .ε = <ε> +Valuesₘ n .isCommutativeMonoid = record + { isMonoid = record + { isSemigroup = record + { isMagma = record + { isEquivalence = ≋-isEquiv n + ; ∙-cong = ⊕-cong + } + ; assoc = ⊕-assoc + } + ; identity = ⊕-identityˡ , ⊕-identityʳ + } + ; comm = ⊕-comm + } + +opaque + + unfolding Values + + [] : ∣ Values 0 ∣ + [] = Vec.[] + + []-unique : (xs ys : ∣ Values 0 ∣) → xs ≋ ys + []-unique xs ys () + +module _ {n m : ℕ} where + + opaque + + unfolding Values + + _++_ : ∣ Values n ∣ → ∣ Values m ∣ → ∣ Values (n + m) ∣ + _++_ = Vec._++_ + + infixr 5 _++_ + + ++-cong + : (xs xs′ : ∣ Values n ∣) + {ys ys′ : ∣ Values m ∣} + → xs ≋ xs′ + → ys ≋ ys′ + → xs ++ ys ≋ xs′ ++ ys′ + ++-cong xs xs′ xs≋xs′ ys≋ys′ i with splitAt n i + ... | inj₁ i = xs≋xs′ i + ... | inj₂ i = ys≋ys′ i + + splitₛ : Values (n + m) ⟶ₛ Values n ×ₛ Values m + to splitₛ v = v ∘ (_↑ˡ m) , v ∘ (n ↑ʳ_) + cong splitₛ v₁≋v₂ = v₁≋v₂ ∘ (_↑ˡ m) , v₁≋v₂ ∘ (n ↑ʳ_) + + ++ₛ : Values n ×ₛ Values m ⟶ₛ Values (n + m) + to ++ₛ (xs , ys) = xs ++ ys + cong ++ₛ (≗xs , ≗ys) = ++-cong _ _ ≗xs ≗ys diff --git a/Data/Vector.agda b/Data/Vector.agda new file mode 100644 index 0000000..874f0b2 --- /dev/null +++ b/Data/Vector.agda @@ -0,0 +1,126 @@ +{-# OPTIONS --without-K --safe #-} + +module Data.Vector where + +open import Data.Nat.Base using (ℕ) +open import Data.Vec.Functional using (Vector; head; tail; []; removeAt; map; _++_) public +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_; module ≡-Reasoning) +open import Function.Base using (∣_⟩-_; _∘_) +open import Data.Fin.Base using (Fin; toℕ; _↑ˡ_; _↑ʳ_) +open ℕ +open Fin + +foldl + : ∀ {n : ℕ} {A : Set} (B : ℕ → Set) + → (∀ {k : Fin n} → B (toℕ k) → A → B (suc (toℕ k))) + → B zero + → Vector A n + → B n +foldl {zero} B ⊕ e v = e +foldl {suc n} B ⊕ e v = foldl (B ∘ suc) ⊕ (⊕ e (head v)) (tail v) + +foldl-cong + : {n : ℕ} {A : Set} + (B : ℕ → Set) + {f g : ∀ {k : Fin n} → B (toℕ k) → A → B (suc (toℕ k))} + → (∀ {k} → ∀ x y → f {k} x y ≡ g {k} x y) + → (e : B zero) + → (v : Vector A n) + → foldl B f e v ≡ foldl B g e v +foldl-cong {zero} B f≗g e v = ≡.refl +foldl-cong {suc n} B {g = g} f≗g e v rewrite (f≗g e (head v)) = foldl-cong (B ∘ suc) f≗g (g e (head v)) (tail v) + +foldl-cong-arg + : {n : ℕ} {A : Set} + (B : ℕ → Set) + (f : ∀ {k : Fin n} → B (toℕ k) → A → B (suc (toℕ k))) + → (e : B zero) + → {v w : Vector A n} + → v ≗ w + → foldl B f e v ≡ foldl B f e w +foldl-cong-arg {zero} B f e v≗w = ≡.refl +foldl-cong-arg {suc n} B f e {w = w} v≗w rewrite v≗w zero = foldl-cong-arg (B ∘ suc) f (f e (head w)) (v≗w ∘ suc) + +foldl-map + : {n : ℕ} {A : ℕ → Set} {B C : Set} + (f : ∀ {k : Fin n} → A (toℕ k) → B → A (suc (toℕ k))) + (g : C → B) + (x : A zero) + (xs : Vector C n) + → foldl A f x (map g xs) + ≡ foldl A (∣ f ⟩- g) x xs +foldl-map {zero} f g e xs = ≡.refl +foldl-map {suc n} f g e xs = foldl-map f g (f e (g (head xs))) (tail xs) + +foldl-fusion + : {n : ℕ} + {A : Set} {B C : ℕ → Set} + (h : {k : ℕ} → B k → C k) + → {f : {k : Fin n} → B (toℕ k) → A → B (suc (toℕ k))} {d : B zero} + → {g : {k : Fin n} → C (toℕ k) → A → C (suc (toℕ k))} {e : C zero} + → (h d ≡ e) + → ({k : Fin n} (b : B (toℕ k)) (x : A) → h (f {k} b x) ≡ g (h b) x) + → h ∘ foldl B f d ≗ foldl C g e +foldl-fusion {zero} _ base _ _ = base +foldl-fusion {suc n} {A} h {f} {d} {g} {e} base fuse xs = foldl-fusion h eq fuse (tail xs) + where + x₀ : A + x₀ = head xs + open ≡.≡-Reasoning + eq : h (f d x₀) ≡ g e x₀ + eq = begin + h (f d x₀) ≡⟨ fuse d x₀ ⟩ + g (h d) x₀ ≡⟨ ≡.cong-app (≡.cong g base) x₀ ⟩ + g e x₀ ∎ + +foldl-[] + : {A : Set} + (B : ℕ → Set) + (f : {k : Fin 0} → B (toℕ k) → A → B (suc (toℕ k))) + {e : B 0} + → foldl B f e [] ≡ e +foldl-[] _ _ = ≡.refl + +open import Data.Sum using ([_,_]′) +open import Data.Sum.Properties using ([,-]-cong; [-,]-cong; [,]-∘) +open import Data.Fin.Properties using (splitAt-↑ˡ; splitAt-↑ʳ) +open import Data.Fin using (splitAt) +open import Data.Nat using (_+_) +++-↑ˡ + : {n m : ℕ} + {A : Set} + (X : Vector A n) + (Y : Vector A m) + → (X ++ Y) ∘ (_↑ˡ m) ≗ X +++-↑ˡ {n} {m} X Y i = ≡.cong [ X , Y ]′ (splitAt-↑ˡ n i m) + +++-↑ʳ + : {n m : ℕ} + {A : Set} + (X : Vector A n) + (Y : Vector A m) + → (X ++ Y) ∘ (n ↑ʳ_) ≗ Y +++-↑ʳ {n} {m} X Y i = ≡.cong [ X , Y ]′ (splitAt-↑ʳ n m i) + ++-assocʳ : {m n o : ℕ} → Fin (m + (n + o)) → Fin (m + n + o) ++-assocʳ {m} {n} {o} = [ (λ x → x ↑ˡ n ↑ˡ o) , [ (λ x → (m ↑ʳ x) ↑ˡ o) , m + n ↑ʳ_ ]′ ∘ splitAt n ]′ ∘ splitAt m + +open ≡-Reasoning +++-assoc + : {m n o : ℕ} + {A : Set} + (X : Vector A m) + (Y : Vector A n) + (Z : Vector A o) + → ((X ++ Y) ++ Z) ∘ +-assocʳ {m} ≗ X ++ (Y ++ Z) +++-assoc {m} {n} {o} X Y Z i = begin + ((X ++ Y) ++ Z) (+-assocʳ {m} i) ≡⟨⟩ + ((X ++ Y) ++ Z) ([ (λ x → x ↑ˡ n ↑ˡ o) , _ ]′ (splitAt m i)) ≡⟨ [,]-∘ ((X ++ Y) ++ Z) (splitAt m i) ⟩ + [ ((X ++ Y) ++ Z) ∘ (λ x → x ↑ˡ n ↑ˡ o) , _ ]′ (splitAt m i) ≡⟨ [-,]-cong (++-↑ˡ (X ++ Y) Z ∘ (_↑ˡ n)) (splitAt m i) ⟩ + [ (X ++ Y) ∘ (_↑ˡ n) , _ ]′ (splitAt m i) ≡⟨ [-,]-cong (++-↑ˡ X Y) (splitAt m i) ⟩ + [ X , ((X ++ Y) ++ Z) ∘ [ _ , _ ]′ ∘ splitAt n ]′ (splitAt m i) ≡⟨ [,-]-cong ([,]-∘ ((X ++ Y) ++ Z) ∘ splitAt n) (splitAt m i) ⟩ + [ X , [ (_ ++ Z) ∘ (_↑ˡ o) ∘ (m ↑ʳ_) , _ ]′ ∘ splitAt n ]′ (splitAt m i) ≡⟨ [,-]-cong ([-,]-cong (++-↑ˡ (X ++ Y) Z ∘ (m ↑ʳ_)) ∘ splitAt n) (splitAt m i) ⟩ + [ X , [ (X ++ Y) ∘ (m ↑ʳ_) , _ ]′ ∘ splitAt n ]′ (splitAt m i) ≡⟨ [,-]-cong ([-,]-cong (++-↑ʳ X Y) ∘ splitAt n) (splitAt m i) ⟩ + [ X , [ Y , ((X ++ Y) ++ Z) ∘ (m + n ↑ʳ_) ]′ ∘ splitAt n ]′ (splitAt m i) ≡⟨ [,-]-cong ([,-]-cong (++-↑ʳ (X ++ Y) Z) ∘ splitAt n) (splitAt m i) ⟩ + [ X , [ Y , Z ]′ ∘ splitAt n ]′ (splitAt m i) ≡⟨⟩ + (X ++ (Y ++ Z)) i ∎ |