diff options
| -rw-r--r-- | Data/Circuit/Merge.agda | 338 | ||||
| -rw-r--r-- | Data/Fin/Preimage.agda | 42 | ||||
| -rw-r--r-- | Data/Subset/Functional.agda | 162 | ||||
| -rw-r--r-- | Functor/Instance/Nat/Pull.agda | 70 | ||||
| -rw-r--r-- | Functor/Instance/Nat/Push.agda | 66 |
5 files changed, 678 insertions, 0 deletions
diff --git a/Data/Circuit/Merge.agda b/Data/Circuit/Merge.agda new file mode 100644 index 0000000..d8180b4 --- /dev/null +++ b/Data/Circuit/Merge.agda @@ -0,0 +1,338 @@ +{-# 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) +open import Data.Fin.Properties using (punchInᵢ≢i; punchIn-punchOut) +open import Data.Bool.Properties using (if-float) +open import Data.Bool using (Bool; if_then_else_) +open import Data.Circuit.Value using (Value; join; join-comm; join-assoc) +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.Fin.Permutation + using + ( 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 (∣_⟩-_; _∘_) +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_) + +open Value using (U) +open ℕ +open Fin +open Bool + +_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)) (either-way (head S)) ⟨ + merge-with e (tail (λ _ → U)) (tail S) ≡⟨⟩ + merge-with e (λ _ → U) (tail S) ≡⟨ merge-with-U e (tail S) ⟩ + e ∎ + where + open ≡.≡-Reasoning + either-way : (b : Bool) → e ≡ (if b then e else e) + either-way b = if-float (λ _ → e) b {e} {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-with U 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)) ∎ + where + open ≡.≡-Reasoning +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) + open ≡.≡-Reasoning + +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 : ℕ} + → (ρ : Permutation′ A) + → (v : Vector Value A) + (S : Subset A) + → merge v (preimage (ρ ⟨$⟩ʳ_) S) ≡ merge (v ∘ (ρ ⟨$⟩ˡ_)) S +merge-preimage-ρ {zero} ρ v S = merge-[]₂ +merge-preimage-ρ {suc A} ρ 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 A) → Fin (suc A) + ρˡ = ρ ⟨$⟩ˡ_ + ρʳ = ρ ⟨$⟩ʳ_ + ρ- : Permutation′ A + ρ- = remove (head ρˡ) ρ + ρˡ- ρʳ- : Fin A → Fin A + ρˡ- = ρ- ⟨$⟩ˡ_ + ρʳ- = ρ- ⟨$⟩ʳ_ + v- : Vector Value A + v- = removeAt v (head ρˡ) + [preimageρʳS]- : Subset A + [preimageρʳS]- = removeAt (preimage ρʳ S) (head ρˡ) + S- : Subset A + S- = tail S + vρˡ0? : Value + vρˡ0? = head (v ∘ ρˡ) when head S + open ≡.≡-Reasoning + ≡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 ∎ + where + open ≡.≡-Reasoning + 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 + open ≡.≡-Reasoning + ρʳ ρˡ : 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 + open ≡.≡-Reasoning + ≡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 ⁆) diff --git a/Data/Fin/Preimage.agda b/Data/Fin/Preimage.agda new file mode 100644 index 0000000..f6e4373 --- /dev/null +++ b/Data/Fin/Preimage.agda @@ -0,0 +1,42 @@ +{-# 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 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/Functor/Instance/Nat/Pull.agda b/Functor/Instance/Nat/Pull.agda new file mode 100644 index 0000000..3f13303 --- /dev/null +++ b/Functor/Instance/Nat/Pull.agda @@ -0,0 +1,70 @@ +{-# OPTIONS --without-K --safe #-} + +module Functor.Instance.Nat.Pull where + +open import Categories.Category.Core using (module Category) +open import Categories.Category.Instance.Nat using (Nat) +open import Categories.Category.Instance.Setoids using (Setoids) +open import Categories.Functor using (Functor) +open import Data.Circuit.Merge using (merge; merge-cong₁; merge-cong₂; merge-⁅⁆; merge-preimage) +open import Data.Circuit.Value using (Value) +open import Data.Fin.Base using (Fin) +open import Data.Fin.Preimage using (preimage; preimage-cong₁) +open import Data.Nat.Base using (ℕ) +open import Data.Subset.Functional using (⁅_⁆) +open import Data.Vec.Functional.Relation.Binary.Equality.Setoid using (≋-setoid) +open import Function.Base using (id; flip; _∘_) +open import Function.Bundles using (Func; _⟶ₛ_) +open import Function.Construct.Identity using () renaming (function to Id) +open import Function.Construct.Setoid using (setoid; _∙_) +open import Level using (0ℓ) +open import Relation.Binary using (Rel; Setoid) +open import Relation.Binary.PropositionalEquality as ≡ using (_≗_) + +open Functor +open Func + +module Nat = Category Nat + +_≈_ : {X Y : Setoid 0ℓ 0ℓ} → Rel (X ⟶ₛ Y) 0ℓ +_≈_ {X} {Y} = Setoid._≈_ (setoid X Y) +infixr 4 _≈_ + +private + variable A B C : ℕ + +-- action on objects (Vector Value n) +Values : ℕ → Setoid 0ℓ 0ℓ +Values = ≋-setoid (≡.setoid Value) + +-- action of Pull on morphisms (contravariant) +Pull₁ : (Fin A → Fin B) → Values B ⟶ₛ Values A +to (Pull₁ f) i = i ∘ f +cong (Pull₁ f) x≗y = x≗y ∘ f + +-- Pull respects identity +Pull-identity : Pull₁ id ≈ Id (Values A) +Pull-identity {A} = Setoid.refl (Values A) + +-- Pull flips composition +Pull-homomorphism + : {A B C : ℕ} + (f : Fin A → Fin B) + (g : Fin B → Fin C) + → Pull₁ (g ∘ f) ≈ Pull₁ f ∙ Pull₁ g +Pull-homomorphism {A} _ _ = Setoid.refl (Values A) + +-- Pull respects equality +Pull-resp-≈ + : {f g : Fin A → Fin B} + → f ≗ g + → Pull₁ f ≈ Pull₁ g +Pull-resp-≈ f≗g {v} = ≡.cong v ∘ f≗g + +-- the Pull functor +Pull : Functor Nat.op (Setoids 0ℓ 0ℓ) +F₀ Pull = Values +F₁ Pull = Pull₁ +identity Pull = Pull-identity +homomorphism Pull {f = f} {g} {v} = Pull-homomorphism g f {v} +F-resp-≈ Pull = Pull-resp-≈ diff --git a/Functor/Instance/Nat/Push.agda b/Functor/Instance/Nat/Push.agda new file mode 100644 index 0000000..c7443ab --- /dev/null +++ b/Functor/Instance/Nat/Push.agda @@ -0,0 +1,66 @@ +{-# OPTIONS --without-K --safe #-} + +module Functor.Instance.Nat.Push where + +open import Categories.Functor using (Functor) +open import Categories.Category.Instance.Nat using (Nat) +open import Categories.Category.Instance.Setoids using (Setoids) +open import Data.Circuit.Value using (Value) +open import Data.Circuit.Merge using (merge; merge-cong₁; merge-cong₂; merge-⁅⁆; merge-preimage) +open import Data.Fin.Base using (Fin) +open import Data.Fin.Preimage using (preimage; preimage-cong₁) +open import Data.Nat.Base using (ℕ) +open import Data.Subset.Functional using (⁅_⁆) +open import Data.Vec.Functional.Relation.Binary.Equality.Setoid using (≋-setoid) +open import Function.Base using (id; flip; _∘_) +open import Function.Bundles using (Func; _⟶ₛ_) +open import Function.Construct.Identity using () renaming (function to Id) +open import Function.Construct.Setoid using (setoid; _∙_) +open import Level using (0ℓ) +open import Relation.Binary using (Rel; Setoid) +open import Relation.Binary.PropositionalEquality as ≡ using (_≗_) + +open Func +open Functor + +private + variable A B C : ℕ + +_≈_ : {X Y : Setoid 0ℓ 0ℓ} → Rel (X ⟶ₛ Y) 0ℓ +_≈_ {X} {Y} = Setoid._≈_ (setoid X Y) +infixr 4 _≈_ + +-- action on objects (Vector Value n) +Values : ℕ → Setoid 0ℓ 0ℓ +Values = ≋-setoid (≡.setoid Value) + +-- action of Push on morphisms (covariant) +Push₁ : (Fin A → Fin B) → Values A ⟶ₛ Values B +to (Push₁ f) v = merge v ∘ preimage f ∘ ⁅_⁆ +cong (Push₁ f) x≗y = merge-cong₁ x≗y ∘ preimage f ∘ ⁅_⁆ + +-- Push respects identity +Push-identity : Push₁ id ≈ Id (Values A) +Push-identity {_} {v} = merge-⁅⁆ v + +-- Push respects composition +Push-homomorphism + : {f : Fin A → Fin B} + {g : Fin B → Fin C} + → Push₁ (g ∘ f) ≈ Push₁ g ∙ Push₁ f +Push-homomorphism {f = f} {g} {v} = merge-preimage f v ∘ preimage g ∘ ⁅_⁆ + +-- Push respects equality +Push-resp-≈ + : {f g : Fin A → Fin B} + → f ≗ g + → Push₁ f ≈ Push₁ g +Push-resp-≈ f≗g {v} = merge-cong₂ v ∘ preimage-cong₁ f≗g ∘ ⁅_⁆ + +-- the Push functor +Push : Functor Nat (Setoids 0ℓ 0ℓ) +F₀ Push = Values +F₁ Push = Push₁ +identity Push = Push-identity +homomorphism Push = Push-homomorphism +F-resp-≈ Push = Push-resp-≈ |