diff options
Diffstat (limited to 'Data')
| -rw-r--r-- | Data/CMonoid.agda | 25 | ||||
| -rw-r--r-- | Data/Monoid.agda | 78 | ||||
| -rw-r--r-- | Data/System.agda | 92 | ||||
| -rw-r--r-- | Data/System/Values.agda | 445 |
4 files changed, 518 insertions, 122 deletions
diff --git a/Data/CMonoid.agda b/Data/CMonoid.agda index 8aaf869..dd0277c 100644 --- a/Data/CMonoid.agda +++ b/Data/CMonoid.agda @@ -3,19 +3,16 @@ open import Level using (Level) module Data.CMonoid {c ℓ : Level} where -open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory) +import Algebra.Bundles as Alg + +open import Algebra.Morphism using (IsMonoidHomomorphism) +open import Categories.Object.Monoid using (Monoid) open import Category.Instance.Setoids.SymmetricMonoidal {c} {ℓ} using (Setoids-×; ×-symmetric′) +open import Data.Monoid {c} {ℓ} using (toMonoid; fromMonoid; toMonoid⇒; module FromMonoid) +open import Data.Product using (_,_; Σ) +open import Function using (Func; _⟨$⟩_; _⟶ₛ_) 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 @@ -37,9 +34,6 @@ toCMonoid M = record 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 @@ -53,7 +47,7 @@ fromCMonoid M = record module M = Monoid (fromMonoid monoid) open Setoids-× using (_≈_; _∘_; module braiding) opaque - unfolding toMonoid + unfolding FromMonoid.μ commutative : M.μ ≈ M.μ ∘ braiding.⇒.η _ commutative {x , y} = comm x y @@ -64,9 +58,6 @@ 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⇒ diff --git a/Data/Monoid.agda b/Data/Monoid.agda index 1ba0af4..02a8062 100644 --- a/Data/Monoid.agda +++ b/Data/Monoid.agda @@ -1,25 +1,26 @@ {-# 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⇒) +module Data.Monoid {c ℓ : Level} where import Algebra.Bundles as Alg +open import Algebra.Morphism using (IsMonoidHomomorphism) +open import Categories.Object.Monoid using (Monoid; Monoid⇒) +open import Category.Instance.Setoids.SymmetricMonoidal {c} {ℓ} using (Setoids-×; ×-monoidal′) +open import Data.Product using (curry′; uncurry′; _,_; Σ) open import Data.Setoid using (∣_∣) +open import Data.Setoid.Unit using (⊤ₛ) +open import Function using (Func; _⟶ₛ_; _⟨$⟩_) +open import Function.Construct.Constant using () renaming (function to Const) +open import Function.Construct.Identity using () renaming (function to Id) 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 ℓ @@ -43,19 +44,57 @@ opaque open Monoid M renaming (Carrier to A) open Setoid A - fromMonoid : Alg.Monoid c ℓ → Monoid Setoids-×.monoidal - fromMonoid M = record +module FromMonoid (M : Alg.Monoid c ℓ) where + + open Alg.Monoid M + open Setoids-× using (_⊗₁_; _⊗₀_; _∘_; unit; module unitorˡ; module unitorʳ; module associator) + + opaque + + unfolding ×-monoidal′ + + μ : setoid ⊗₀ setoid ⟶ₛ setoid + μ .to = uncurry′ _∙_ + μ .cong = uncurry′ ∙-cong + + η : unit ⟶ₛ setoid + η = Const ⊤ₛ setoid ε + + opaque + + unfolding μ + + μ-assoc + : {x : ∣ (setoid ⊗₀ setoid) ⊗₀ setoid ∣} + → μ ∘ μ ⊗₁ Id setoid ⟨$⟩ x + ≈ μ ∘ Id setoid ⊗₁ μ ∘ associator.from ⟨$⟩ x + μ-assoc {(x , y) , z} = assoc x y z + + μ-identityˡ + : {x : ∣ unit ⊗₀ setoid ∣} + → unitorˡ.from ⟨$⟩ x + ≈ μ ∘ η ⊗₁ Id setoid ⟨$⟩ x + μ-identityˡ {_ , x} = sym (identityˡ x) + + μ-identityʳ + : {x : ∣ setoid ⊗₀ unit ∣} + → unitorʳ.from ⟨$⟩ x + ≈ μ ∘ Id setoid ⊗₁ η ⟨$⟩ x + μ-identityʳ {x , _} = sym (identityʳ x) + + fromMonoid : Monoid Setoids-×.monoidal + fromMonoid = 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) } + { μ = μ + ; η = η + ; assoc = μ-assoc + ; identityˡ = μ-identityˡ + ; identityʳ = μ-identityʳ } } - where - open Alg.Monoid M + +open FromMonoid using (fromMonoid) public -- A morphism of monoids in the (monoidal) category of setoids is a monoid homomorphism @@ -64,9 +103,6 @@ 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 diff --git a/Data/System.agda b/Data/System.agda index d71c2a8..d12fa12 100644 --- a/Data/System.agda +++ b/Data/System.agda @@ -66,53 +66,51 @@ module _ {n : ℕ} where 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) +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 diff --git a/Data/System/Values.agda b/Data/System/Values.agda index 545a835..d1cd6c9 100644 --- a/Data/System/Values.agda +++ b/Data/System/Values.agda @@ -5,53 +5,98 @@ 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 Category.Instance.Setoids.SymmetricMonoidal {0ℓ} {0ℓ} using (Setoids-×) -open import Data.Fin using (_↑ˡ_; _↑ʳ_; zero; suc; splitAt) -open import Data.Nat using (ℕ; _+_; suc) -open import Data.Product using (_,_) +import Algebra.Properties.CommutativeMonoid.Sum A as Sum +import Data.Vec.Functional.Relation.Binary.Equality.Setoid as Pointwise +import Object.Monoid.Commutative Setoids-×.symmetric as Obj +import Relation.Binary.Reasoning.Setoid as ≈-Reasoning + +open import Data.Bool using (Bool; if_then_else_) +open import Data.Bool.Properties using (if-cong) +open import Data.Monoid using (module FromMonoid) +open import Data.CMonoid using (fromCMonoid) +open import Data.Fin using (Fin; splitAt; _↑ˡ_; _↑ʳ_; punchIn; punchOut) +open import Data.Fin using (_≟_) +open import Data.Fin.Permutation using (Permutation; Permutation′; _⟨$⟩ʳ_; _⟨$⟩ˡ_; id; flip; inverseˡ; inverseʳ; punchIn-permute; insert; remove) +open import Data.Fin.Preimage using (preimage; preimage-cong₁; preimage-cong₂) +open import Data.Fin.Properties using (punchIn-punchOut) +open import Data.Nat using (ℕ; _+_) +open import Data.Product using (_,_; Σ-syntax) open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_) open import Data.Setoid using (∣_∣) +open import Data.Subset.Functional using (Subset; ⁅_⁆; ⁅⁆∘ρ) 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 import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_; module ≡-Reasoning) +open import Relation.Nullary.Decidable using (yes; no) -open CommutativeMonoid A renaming (Carrier to Value) +open Bool +open CommutativeMonoid A renaming (Carrier to Value; setoid to Valueₛ) +open Fin open Func -open Sum A using (sum) - -open Pointwise setoid using (≋-setoid; ≋-isEquivalence) +open Pointwise Valueₛ using (≋-setoid; ≋-isEquivalence) +open ℕ opaque - Values : ℕ → Setoid 0ℓ 0ℓ Values = ≋-setoid +_when_ : Value → Bool → Value +x when b = if b then x else ε + +-- when preserves setoid equivalence +when-cong + : {x y : Value} + → x ≈ y + → (b : Bool) + → x when b ≈ y when b +when-cong _ false = refl +when-cong x≈y true = x≈y + 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 ε + mask : Subset n → ∣ Values n ∣ → ∣ Values n ∣ + mask S v i = v i when S i + + sum : ∣ Values n ∣ → Value + sum = Sum.sum + + merge : ∣ Values n ∣ → Subset n → Value + merge v S = sum (mask S v) + + -- mask preserves setoid equivalence + maskₛ : Subset n → Values n ⟶ₛ Values n + maskₛ S .to = mask S + maskₛ S .cong v≋w i = when-cong (v≋w i) (S i) + + -- sum preserves setoid equivalence + sumₛ : Values n ⟶ₛ Valueₛ + sumₛ .to = Sum.sum + sumₛ .cong = Sum.sum-cong-≋ + head : ∣ Values (suc n) ∣ → Value head xs = xs zero tail : ∣ Values (suc n) ∣ → ∣ Values n ∣ tail xs = xs ∘ suc + lookup : ∣ Values n ∣ → Fin n → Value + lookup v i = v i + module ≋ = Setoid (Values n) _≋_ : Rel ∣ Values n ∣ 0ℓ @@ -59,16 +104,45 @@ module _ {n : ℕ} where infix 4 _≋_ -opaque + opaque + + unfolding merge + + -- merge preserves setoid equivalence + merge-cong + : (S : Subset n) + → {xs ys : ∣ Values n ∣} + → xs ≋ ys + → merge xs S ≈ merge ys S + merge-cong S {xs} {ys} xs≋ys = cong sumₛ (cong (maskₛ S) xs≋ys) + + mask-cong₁ + : {S₁ S₂ : Subset n} + → S₁ ≗ S₂ + → (xs : ∣ Values n ∣) + → mask S₁ xs ≋ mask S₂ xs + mask-cong₁ S₁≋S₂ _ i = reflexive (if-cong (S₁≋S₂ i)) + + merge-cong₂ + : (xs : ∣ Values n ∣) + → {S₁ S₂ : Subset n} + → S₁ ≗ S₂ + → merge xs S₁ ≈ merge xs S₂ + merge-cong₂ xs S₁≋S₂ = cong sumₛ (mask-cong₁ S₁≋S₂ xs) + +module _ where - unfolding Values open Setoid - ≋-isEquiv : ∀ n → IsEquivalence (_≈_ (Values n)) - ≋-isEquiv = ≋-isEquivalence + + opaque + unfolding Values + ≋-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 @@ -86,25 +160,35 @@ module _ {n : ℕ} where ⊕-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 - } +module Algebra where + + 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 + } + +module Object where + + opaque + unfolding FromMonoid.μ + Valuesₘ : ℕ → Obj.CommutativeMonoid + Valuesₘ n = fromCMonoid (Algebra.Valuesₘ n) opaque @@ -144,3 +228,290 @@ module _ {n m : ℕ} where ++ₛ : Values n ×ₛ Values m ⟶ₛ Values (n + m) to ++ₛ (xs , ys) = xs ++ ys cong ++ₛ (≗xs , ≗ys) = ++-cong _ _ ≗xs ≗ys + +opaque + + unfolding merge + + mask-⊕ + : {n : ℕ} + (xs ys : ∣ Values n ∣) + (S : Subset n) + → mask S (xs ⊕ ys) ≋ mask S xs ⊕ mask S ys + mask-⊕ xs ys S i with S i + ... | false = sym (identityˡ ε) + ... | true = refl + + sum-⊕ + : {n : ℕ} + → (xs ys : ∣ Values n ∣) + → sum (xs ⊕ ys) ≈ sum xs ∙ sum ys + sum-⊕ {zero} xs ys = sym (identityˡ ε) + sum-⊕ {suc n} xs ys = begin + (head xs ∙ head ys) ∙ sum (tail xs ⊕ tail ys) ≈⟨ ∙-congˡ (sum-⊕ (tail xs) (tail ys)) ⟩ + (head xs ∙ head ys) ∙ (sum (tail xs) ∙ sum (tail ys)) ≈⟨ assoc (head xs) (head ys) _ ⟩ + head xs ∙ (head ys ∙ (sum (tail xs) ∙ sum (tail ys))) ≈⟨ ∙-congˡ (assoc (head ys) (sum (tail xs)) _) ⟨ + head xs ∙ ((head ys ∙ sum (tail xs)) ∙ sum (tail ys)) ≈⟨ ∙-congˡ (∙-congʳ (comm (head ys) (sum (tail xs)))) ⟩ + head xs ∙ ((sum (tail xs) ∙ head ys) ∙ sum (tail ys)) ≈⟨ ∙-congˡ (assoc (sum (tail xs)) (head ys) _) ⟩ + head xs ∙ (sum (tail xs) ∙ (head ys ∙ sum (tail ys))) ≈⟨ assoc (head xs) (sum (tail xs)) _ ⟨ + (head xs ∙ sum (tail xs)) ∙ (head ys ∙ sum (tail ys)) ∎ + where + open ≈-Reasoning Valueₛ + + merge-⊕ + : {n : ℕ} + (xs ys : ∣ Values n ∣) + (S : Subset n) + → merge (xs ⊕ ys) S ≈ merge xs S ∙ merge ys S + merge-⊕ {n} xs ys S = begin + sum (mask S (xs ⊕ ys)) ≈⟨ cong sumₛ (mask-⊕ xs ys S) ⟩ + sum (mask S xs ⊕ mask S ys) ≈⟨ sum-⊕ (mask S xs) (mask S ys) ⟩ + sum (mask S xs) ∙ sum (mask S ys) ∎ + where + open ≈-Reasoning Valueₛ + + mask-<ε> : {n : ℕ} (S : Subset n) → mask {n} S <ε> ≋ <ε> + mask-<ε> S i with S i + ... | false = refl + ... | true = refl + + sum-<ε> : (n : ℕ) → sum {n} <ε> ≈ ε + sum-<ε> zero = refl + sum-<ε> (suc n) = trans (identityˡ (sum {n} <ε>)) (sum-<ε> n) + + merge-<ε> : {n : ℕ} (S : Subset n) → merge {n} <ε> S ≈ ε + merge-<ε> {n} S = begin + sum (mask S <ε>) ≈⟨ cong sumₛ (mask-<ε> S) ⟩ + sum {n} <ε> ≈⟨ sum-<ε> n ⟩ + ε ∎ + where + open ≈-Reasoning Valueₛ + + merge-⁅⁆ + : {n : ℕ} + (xs : ∣ Values n ∣) + (i : Fin n) + → merge xs ⁅ i ⁆ ≈ lookup xs i + merge-⁅⁆ {suc n} xs zero = trans (∙-congˡ (sum-<ε> n)) (identityʳ (head xs)) + merge-⁅⁆ {suc n} xs (suc i) = begin + ε ∙ merge (tail xs) ⁅ i ⁆ ≈⟨ identityˡ (sum (mask ⁅ i ⁆ (tail xs))) ⟩ + merge (tail xs) ⁅ i ⁆ ≈⟨ merge-⁅⁆ (tail xs) i ⟩ + tail xs i ∎ + where + open ≈-Reasoning Valueₛ + +opaque + + unfolding Values + + push : {A B : ℕ} → ∣ Values A ∣ → (Fin A → Fin B) → ∣ Values B ∣ + push v f = merge v ∘ preimage f ∘ ⁅_⁆ + + pull : {A B : ℕ} → ∣ Values B ∣ → (Fin A → Fin B) → ∣ Values A ∣ + pull v f = v ∘ f + +insert-f0-0 + : {A B : ℕ} + (f : Fin (suc A) → Fin (suc B)) + → Σ[ ρ ∈ Permutation′ (suc B) ] (ρ ⟨$⟩ʳ (f zero) ≡ zero) +insert-f0-0 {A} {B} f = ρ , ρf0≡0 + where + ρ : Permutation′ (suc B) + ρ = insert (f zero) zero id + ρf0≡0 : ρ ⟨$⟩ʳ f zero ≡ zero + ρf0≡0 with f zero ≟ f zero + ... | yes _ = ≡.refl + ... | no f0≢f0 with () ← f0≢f0 ≡.refl + +opaque + unfolding push + push-cong + : {A B : ℕ} + → (v : ∣ Values A ∣) + {f g : Fin A → Fin B} + → f ≗ g + → push v f ≋ push v g + push-cong v f≋g i = merge-cong₂ v (≡.cong ⁅ i ⁆ ∘ f≋g) + +opaque + unfolding Values + removeAt : {n : ℕ} → ∣ Values (suc n) ∣ → Fin (suc n) → ∣ Values n ∣ + removeAt v i = Vec.removeAt v i + +opaque + unfolding merge removeAt + merge-removeAt + : {A : ℕ} + (k : Fin (suc A)) + (v : ∣ Values (suc A) ∣) + (S : Subset (suc A)) + → merge v S ≈ lookup v k when S k ∙ merge (removeAt v k) (Vec.removeAt S k) + merge-removeAt {A} zero v S = refl + merge-removeAt {suc A} (suc k) v S = begin + v0? ∙ merge (tail v) (Vec.tail S) ≈⟨ ∙-congˡ (merge-removeAt k (tail v) (Vec.tail S)) ⟩ + v0? ∙ (vk? ∙ merge (tail v-) (Vec.tail S-)) ≈⟨ assoc v0? vk? _ ⟨ + (v0? ∙ vk?) ∙ merge (tail v-) (Vec.tail S-) ≈⟨ ∙-congʳ (comm v0? vk?) ⟩ + (vk? ∙ v0?) ∙ merge (tail v-) (Vec.tail S-) ≈⟨ assoc vk? v0? _ ⟩ + vk? ∙ (v0? ∙ merge (tail v-) (Vec.tail S-)) ≡⟨⟩ + vk? ∙ merge v- S- ∎ + where + open ≈-Reasoning Valueₛ + v0? vk? : Value + v0? = head v when Vec.head S + vk? = tail v k when Vec.tail S k + v- : Vector Value (suc A) + v- = removeAt v (suc k) + S- : Subset (suc A) + S- = Vec.removeAt S (suc k) + +opaque + unfolding merge pull removeAt + merge-preimage-ρ + : {A B : ℕ} + → (ρ : Permutation A B) + → (v : ∣ Values A ∣) + (S : Subset B) + → merge v (preimage (ρ ⟨$⟩ʳ_) S) ≈ merge (pull v (ρ ⟨$⟩ˡ_)) S + merge-preimage-ρ {zero} {zero} ρ v S = refl + 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 (ρˡ zero) v (preimage ρʳ S) ⟩ + mask (preimage ρʳ S) v (ρˡ zero) ∙ merge v- [preimage-ρʳ-S]- ≈⟨ ∙-congʳ ≈vρˡ0? ⟩ + mask S (pull v ρˡ) zero ∙ merge v- [preimage-ρʳ-S]- ≈⟨ ∙-congˡ (merge-cong₂ v- preimage-) ⟩ + mask S (pull v ρˡ) zero ∙ merge v- (preimage ρʳ- S-) ≈⟨ ∙-congˡ (merge-preimage-ρ ρ- v- S-) ⟩ + mask S (pull v ρˡ) zero ∙ merge (pull v- ρˡ-) S- ≈⟨ ∙-congˡ (merge-cong S- (reflexive ∘ pull-v-ρˡ-)) ⟩ + mask S (pull v ρˡ) zero ∙ merge (tail (pull v ρˡ)) S- ≡⟨⟩ + merge (pull v ρˡ) S ∎ + where + ρˡ : Fin (suc B) → Fin (suc A) + ρˡ = ρ ⟨$⟩ˡ_ + ρʳ : Fin (suc A) → Fin (suc B) + ρʳ = ρ ⟨$⟩ʳ_ + ρ- : Permutation A B + ρ- = remove (ρˡ zero) ρ + ρˡ- : Fin B → Fin A + ρˡ- = ρ- ⟨$⟩ˡ_ + ρʳ- : Fin A → Fin B + ρʳ- = ρ- ⟨$⟩ʳ_ + v- : ∣ Values A ∣ + v- = removeAt v (ρˡ zero) + S- : Subset B + S- = S ∘ suc + [preimage-ρʳ-S]- : Subset A + [preimage-ρʳ-S]- = Vec.removeAt (preimage ρʳ S) (ρˡ zero) + vρˡ0? : Value + vρˡ0? = head (pull v ρˡ) when S zero + ≈vρˡ0? : mask (S ∘ ρʳ ∘ ρˡ) (pull v ρˡ) zero ≈ mask S (pull v ρˡ) zero + ≈vρˡ0? = mask-cong₁ (λ i → ≡.cong S (inverseʳ ρ {i})) (pull v ρˡ) zero + module _ where + open ≡-Reasoning + preimage- : [preimage-ρʳ-S]- ≗ preimage ρʳ- S- + preimage- x = begin + [preimage-ρʳ-S]- x ≡⟨⟩ + Vec.removeAt (preimage ρʳ S) (ρˡ zero) x ≡⟨⟩ + S (ρʳ (punchIn (ρˡ zero) x)) ≡⟨ ≡.cong S (punchIn-permute ρ (ρˡ zero) x) ⟩ + S (punchIn (ρʳ (ρˡ zero)) (ρʳ- x)) ≡⟨ ≡.cong (λ h → S (punchIn h (ρʳ- x))) (inverseʳ ρ) ⟩ + S (punchIn zero (ρʳ- x)) ≡⟨⟩ + S (suc (ρʳ- x)) ≡⟨⟩ + preimage ρʳ- S- x ∎ + pull-v-ρˡ- : pull v- ρˡ- ≗ tail (pull v ρˡ) + pull-v-ρˡ- i = begin + v- (ρˡ- i) ≡⟨⟩ + v (punchIn (ρˡ zero) (punchOut {A} {ρˡ zero} _)) ≡⟨ ≡.cong v (punchIn-punchOut _) ⟩ + v (ρˡ (punchIn (ρʳ (ρˡ zero)) i)) ≡⟨ ≡.cong (λ h → v (ρˡ (punchIn h i))) (inverseʳ ρ) ⟩ + v (ρˡ (punchIn zero i)) ≡⟨⟩ + v (ρˡ (suc i)) ≡⟨⟩ + tail (v ∘ ρˡ) i ∎ + open ≈-Reasoning Valueₛ + +opaque + + unfolding push merge mask + + mutual + + merge-preimage + : {A B : ℕ} + (f : Fin A → Fin B) + → (v : ∣ Values A ∣) + (S : Subset B) + → merge v (preimage f S) ≈ merge (push v f) S + merge-preimage {zero} {zero} f v S = refl + merge-preimage {zero} {suc B} f v S = sym (trans (cong sumₛ (mask-<ε> S)) (sum-<ε> (suc B))) + 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 (push v (ρʳ ∘ f)) (preimage ρˡ S) ≈⟨ merge-preimage-ρ (flip ρ) (push v (ρʳ ∘ f)) S ⟩ + merge (pull (push v (ρʳ ∘ f)) ρʳ) S ≈⟨ merge-cong S (merge-cong₂ v ∘ preimage-cong₂ (ρʳ ∘ f) ∘ ⁅⁆∘ρ ρ) ⟩ + merge (push v (ρˡ ∘ ρʳ ∘ f)) S ≈⟨ merge-cong S (push-cong v (λ x → inverseˡ ρ {f x})) ⟩ + merge (push v f) S ∎ + where + open ≈-Reasoning Valueₛ + ρʳ ρˡ : Fin (ℕ.suc B) → Fin (ℕ.suc B) + ρʳ = ρ ⟨$⟩ʳ_ + ρˡ = ρ ⟨$⟩ˡ_ + + merge-preimage-f0≡0 + : {A B : ℕ} + (f : Fin (suc A) → Fin (suc B)) + → f zero ≡ zero + → (v : ∣ Values (suc A) ∣) + (S : Subset (suc B)) + → merge v (preimage f S) ≈ merge (push v f) S + merge-preimage-f0≡0 {A} {B} f f0≡0 v S + using S0 , S- ← S zero , S ∘ suc + using v0 , v- ← head v , tail v + using f0 , f- ← f zero , f ∘ suc = begin + merge v f⁻¹[S] ≡⟨⟩ + v0? ∙ merge v- f⁻¹[S]- ≈⟨ ∙-congˡ (merge-preimage f- v- S) ⟩ + v0? ∙ merge f[v-] S ≡⟨⟩ + v0? ∙ (f[v-]0? ∙ merge f[v-]- S-) ≈⟨ assoc v0? f[v-]0? (merge f[v-]- S-) ⟨ + v0? ∙ f[v-]0? ∙ merge f[v-]- S- ≈⟨ ∙-congʳ v0?∙f[v-]0?≈f[v]0? ⟩ + f[v]0? ∙ merge f[v-]- S- ≈⟨ ∙-congˡ (merge-cong S- ≋f[v]-) ⟩ + f[v]0? ∙ merge f[v]- S- ≡⟨⟩ + merge f[v] S ∎ + where + open ≈-Reasoning Valueₛ + f⁻¹[S] : Subset (suc A) + f⁻¹[S] = preimage f S + f⁻¹[S]- : Subset A + f⁻¹[S]- = f⁻¹[S] ∘ suc + f⁻¹[S]0 : Bool + f⁻¹[S]0 = f⁻¹[S] zero + f[v] : ∣ Values (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-] : ∣ Values (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-] + v0? f[v-]0? v0?+[f[v-]0?] f[v]0? : Value + v0? = v0 when f⁻¹[S]0 + f[v-]0? = f[v-]0 when S0 + v0?+[f[v-]0?] = if S0 then v0? ∙ f[v-]0 else v0? + f[v]0? = f[v]0 when S0 + v0?∙f[v-]0?≈f[v]0? : v0? ∙ f[v-]0? ≈ f[v]0? + v0?∙f[v-]0?≈f[v]0? rewrite f0≡0 with S0 + ... | true = refl + ... | false = identityˡ ε + ≋f[v]- : f[v-]- ≋ f[v]- + ≋f[v]- x rewrite f0≡0 = sym (identityˡ (push v- f- (suc x))) + +opaque + unfolding push + merge-push + : {A B C : ℕ} + (f : Fin A → Fin B) + (g : Fin B → Fin C) + → (v : ∣ Values A ∣) + → push v (g ∘ f) ≋ push (push v f) g + merge-push f g v i = merge-preimage f v (preimage g ⁅ i ⁆) |