Commit ba5f364a by João Paulo Pizani Flor

### Cleanup after merge, these plug lemmas are hell on eartch

parent 1a427415
 \begin{code} module Data.Vec.Extra where open import Function using (id; _∘_) open import Function using (id; _∘_; _∘′_) open import Data.Nat.Base using (ℕ; suc; _+_; _*_) open import Data.Product using (∃₂; _×_; proj₁; proj₂; map) open import Data.Vec using (Vec; splitAt; _++_; group; initLast; applicative) ... ... @@ -49,6 +49,24 @@ splitAt′ m v = map id proj₁ (splitAt m v) % %<*₁∘split1′> \AgdaTarget{₁∘split1′} \begin{code} ₁∘split1′ : ∀ {n ℓ} {α : Set ℓ} → Vec α (1 + n) → Vec α 1 ₁∘split1′ = proj₁ ∘′ splitAt′ 1 \end{code} % %<*₂∘split1′> \AgdaTarget{₂∘split1′} \begin{code} ₂∘split1′ : ∀ {n ℓ} {α : Set ℓ} → Vec α (1 + n) → Vec α n ₂∘split1′ = proj₂ ∘′ splitAt′ 1 \end{code} % %<*group-ignore-eq> \AgdaTarget{group′} \begin{code} ... ...
 \begin{code} module PiWare.Samples.RegN' where open import Function using (_∘′_; id; flip) open import Function using (_∘′_; id; flip; _$_) open import Coinduction using (♯_) open import Data.Fin using (#_; raise) renaming (suc to Fs) open import Data.Bool.Base using (Bool) renaming (false to 𝔽; true to 𝕋) ... ... @@ -13,6 +13,7 @@ open import Data.Vec.Properties using (lookup∘tabulate; tabulate∘lookup) open import Data.Vec.Extra using (splitAt′) open import Data.Vec.Properties.Extra using (tabulate-cong) open import Data.Stream using (Stream; _∷_; zipWith; repeat; _≈_; map; zipWith-cong) open import Data.Stream.Extra using (zip) open import Data.Stream.Properties using (module EqReasoningₛ; module Setoidₛ; map-repeat; map-compose; map-cong-fun; map-id) open import Data.Stream.Equality.WithTrans using (_≈ₚ_; _∷ₚ_; transₚ; reflₚ; ≈ₚ-to-≈) open EqReasoningₛ using (_≈⟨_⟩_) renaming (begin_ to beginₛ_; _∎ to _∎ₛ) ... ... @@ -21,11 +22,11 @@ open import Relation.Binary.PropositionalEquality using (_≡_; _≗_; refl; con open ≡-Reasoning using (begin_; _≡⟨_⟩_; _∎) open import Data.CausalStream using (runᶜ′; runᶜ-const) open import PiWare.Atomic.Bool using (Atomic-Bool) open import PiWare.Gates.BoolTrio using () renaming (BoolTrio to B₃) open import PiWare.Circuit using (ℂ; C; Plug; _⟫_; _∥_) open import PiWare.Plugs using (nil⤨) open import PiWare.Semantics.Simulation Atomic-Bool using (module WithGates) open import PiWare.Atomic.Bool using (Atomic-Bool) open import PiWare.Semantics.Simulation Atomic-Bool using (module WithGates; W) open import PiWare.Semantics.Simulation.BoolTrio using () renaming (spec to spec-B₃) open WithGates spec-B₃ using (⟦_⟧ω; ⟦_⟧ᶜ; ⟦_⟧) open import PiWare.Semantics.Simulation.Properties.SequentialCongruence Atomic-Bool using (⟦⟧ω[_]-cong) ... ... @@ -64,15 +65,16 @@ regn (suc n) = regn-plug {n} ⟫ (reg ∥ regn n) %<*lemma> \AgdaTarget{lemma} -- TODO: this holds for any serializable product %<*map⇓²-zip-map⇑¹-repeat> \AgdaTarget{map⇓²-zip-map⇑¹-repeat} \begin{code} lemma : ∀ {xs v} → zipWith _++_ xs (repeat [ v ]) ≈ map ⇓² (zipWith _,_ (map ⇑¹ xs) (repeat v)) lemma {x ∷ xs} {v} = reduce x ∷ ♯ lemma where reduce : ∀ x → x ++ v ∷ [] ≡ head x ∷ v ∷ [] reduce (x ∷ []) = refl map⇓²-zip-map⇑¹-repeat : ∀ {xs y} → zipWith _++_ xs (repeat [ y ]) ≈ map ⇓² (zip (map ⇑¹ xs) (repeat y)) map⇓²-zip-map⇑¹-repeat {x ∷ _} {y} = append-headCons x ∷ ♯ map⇓²-zip-map⇑¹-repeat where append-headCons : ∀ (z : W 1) → z ++ [ y ] ≡ (head z) ∷ [ y ] append-headCons (_ ∷ []) = refl \end{code} % % %<*proofReg-never-plain> ... ... @@ -81,7 +83,7 @@ lemma {x ∷ xs} {v} = reduce x ∷ ♯ lemma proofReg-never-plain : ∀ {xs} → ⟦ reg ⟧ω (zipWith _++_ xs (repeat [ 𝔽 ])) ≈ repeat [ 𝔽 ] proofReg-never-plain {xs} = beginₛ ⟦ reg ⟧ω (zipWith _++_ xs (repeat [ 𝔽 ])) ≈⟨ ⟦⟧ω[_]-cong {c = reg} spec-B₃ (lemma {xs = xs}) ⟩ ≈⟨ ⟦⟧ω[_]-cong {c = reg} spec-B₃ (map⇓²-zip-map⇑¹-repeat {xs = xs}) ⟩ ⟦ reg ⟧ω (map ⇓² (zipWith _,_ (map ⇑¹ xs) (repeat 𝔽))) ≈⟨ proofReg-never {xs = map ⇑¹ xs} ⟩ map ⇓¹ (repeat 𝔽) ... ... @@ -91,70 +93,83 @@ proofReg-never-plain {xs} = beginₛ % -- TODO: move to Data.Vec.Properties.Extra %<*head∘[x]-involutive-Vec1> \AgdaTarget{head∘[x]-involutive-Vec1} \begin{code} head∘[x]-involutive-Vec1 : ∀ {ℓ} {α : Set ℓ} (xs : Vec α 1) → [_] (head xs) ≡ xs head∘[x]-involutive-Vec1 (x ∷ []) = refl \end{code} % %<*proofReg-always-plain> \AgdaTarget{proofReg-always-plain} \begin{code} proofReg-always-plain : ∀ {xs} → ⟦ reg ⟧ω (zipWith _++_ xs (repeat [ 𝕋 ])) ≈ xs proofReg-always-plain {xs} = beginₛ ⟦ reg ⟧ω (zipWith _++_ xs (repeat [ 𝕋 ])) ≈⟨ ⟦⟧ω[_]-cong {c = reg} spec-B₃ (lemma {xs = xs}) ⟩ ≈⟨ ⟦⟧ω[_]-cong {c = reg} spec-B₃ (map⇓²-zip-map⇑¹-repeat {xs = xs}) ⟩ ⟦ reg ⟧ω (map ⇓² (zipWith _,_ (map ⇑¹ xs) (repeat 𝕋))) ≈⟨ proofReg-always {xs = map ⇑¹ xs} ⟩ map ⇓¹ (map ⇑¹ xs) ≈⟨ symₛ map-compose ⟩ map (⇓¹ ∘′ ⇑¹) xs ≈⟨ map-cong-fun ⊥ ⟩ ≈⟨ map-cong-fun head∘[x]-involutive-Vec1 ⟩ map id xs ≈⟨ map-id ⟩ xs ∎ₛ where postulate ⊥ : _ \end{code} % %<*lemma-plug''> \AgdaTarget{lemma-plug''} -- TODO: move? %<*regn-plug-tabulates-lookups> \AgdaTarget{regn-plug-tabulates-lookups} \begin{code} lemma-plug'' : ∀ {ℓ} {α : Set ℓ} {n} {x1 x2} {xs : Vec α n} → tabulate (λ x → lookup (lookup x (tabulate (Fs ∘′ Fs))) (x1 ∷ x2 ∷ xs)) ≡ xs lemma-plug''{x1 = x1} {x2} {xs} = begin tabulate (λ x → lookup (lookup x (tabulate (Fs ∘′ Fs))) (x1 ∷ x2 ∷ xs)) ≡⟨ tabulate-cong (λ x → cong (λ z → lookup z (x1 ∷ x2 ∷ xs)) (lookup∘tabulate (Fs ∘′ Fs) x)) ⟩ tabulate (flip lookup xs) ≡⟨ tabulate∘lookup xs ⟩ xs ∎ regn-plug-tabulates-lookups : ∀ {n ℓ} {α : Set ℓ} {x y} {zs : Vec α n} → tabulate (λ k → lookup (lookup k (tabulate (Fs ∘′ Fs))) (x ∷ y ∷ zs)) ≡ zs regn-plug-tabulates-lookups {x = x} {y} {zs} = begin tabulate (λ k → lookup (lookup k (tabulate (Fs ∘′ Fs))) (x ∷ y ∷ zs)) ≡⟨ tabulate-cong (λ k₁ → cong (λ k₂ → lookup k₂ (x ∷ y ∷ zs)) (lookup∘tabulate (Fs ∘′ Fs) k₁)) ⟩ tabulate (flip lookup zs) ≡⟨ tabulate∘lookup zs ⟩ zs ∎ \end{code} % % %<*lemma-plug'> \AgdaTarget{lemma-plug'} %<*regn-plug-runᶜ′> \AgdaTarget{regn-plug-runᶜ′} \begin{code} lemma-plug' : ∀ {n v x cs xs} → runᶜ′ ⟦ regn-plug {n} ⟧ᶜ ((v ∷ x) ∷ cs) (zipWith _∷_ (repeat v) xs) ≈ₚ zipWith _++_ (zipWith _++_ (map (proj₁ ∘′ splitAt′ 1) (x ∷ ♯ xs)) (repeat [ v ])) (zipWith _∷_ (repeat v) (map (proj₂ ∘′ splitAt′ 1) (x ∷ ♯ xs))) lemma-plug' {x = x} {xs = x₁ ∷ xs₁} with splitAt 1 x lemma-plug' {v = v} {x = ._} {xs = x₁ ∷ xs₁} | xh ∷ [] , xt , refl = cong (λ z → xh ∷ v ∷ v ∷ z) lemma-plug'' ∷ₚ (♯ transₚ lemma-plug' (refl ∷ₚ (♯ reflₚ))) regn-plug-runᶜ′ : ∀ {n v x cs xs} → runᶜ′ ⟦ regn-plug {n} ⟧ᶜ ((v ∷ x) ∷ cs) (zipWith _∷_ (repeat v) xs) ≈ₚ zipWith _++_ (zipWith _++_ (map (proj₁ ∘′ splitAt′ 1) (x ∷ ♯ xs)) (repeat [ v ])) (zipWith _∷_ (repeat v) (map (proj₂ ∘′ splitAt′ 1) (x ∷ ♯ xs))) regn-plug-runᶜ′ {x = x} {xs = _ ∷ _} with splitAt 1 x regn-plug-runᶜ′ {v = v} {xs = _ ∷ _} | xh ∷ [] , _ , refl = cong (λ z → xh ∷ v ∷ v ∷ z) regn-plug-tabulates-lookups ∷ₚ ♯ transₚ regn-plug-runᶜ′ (refl ∷ₚ ♯ reflₚ) \end{code} % % %<*lemma-plug> \AgdaTarget{lemma-plug} %<*regn-plug-ω> \AgdaTarget{regn-plug-ω} \begin{code} lemma-plug : ∀ {n v xs} → ⟦ regn-plug {n} ⟧ω (zipWith _∷_ (repeat v) xs) ≈ zipWith _++_ (zipWith _++_ (map (proj₁ ∘′ splitAt′ 1) xs) (repeat [ v ])) (zipWith _∷_ (repeat v) (map (proj₂ ∘′ splitAt′ 1) xs)) lemma-plug {xs = x ∷ xs} = transₛ (≈ₚ-to-≈ lemma-plug') (refl ∷ (♯ reflₛ)) regn-plug-ω : ∀ {n v xs} → ⟦ regn-plug {n} ⟧ω (zipWith _∷_ (repeat v) xs) ≈ zipWith _++_ (zipWith _++_ (map (proj₁ ∘′ splitAt′ 1) xs) (repeat [ v ])) (zipWith _∷_ (repeat v) (map (proj₂ ∘′ splitAt′ 1) xs)) regn-plug-ω {xs = _ ∷ _} = ≈ₚ-to-≈$ transₚ regn-plug-runᶜ′ (refl ∷ₚ ♯ reflₚ) \end{code} % % %<*lemmaRegN-never> \AgdaTarget{lemmaRegN-never} %<*regN-never-data𝔽> \AgdaTarget{regN-never-data𝔽} \begin{code} lemmaRegN-never : ∀ {n} → zipWith _++_ (repeat [ 𝔽 ]) (repeat (replicate 𝔽)) ≈ repeat (replicate {n = suc n} 𝔽) lemmaRegN-never = refl ∷ ♯ lemmaRegN-never regN-never-data𝔽 : ∀ {n} → zipWith _++_ (repeat [ 𝔽 ]) (repeat (replicate 𝔽)) ≈ repeat (replicate {n = suc n} 𝔽) regN-never-data𝔽 = refl ∷ ♯ regN-never-data𝔽 \end{code} % % %<*proofRegN-never> ... ... @@ -168,57 +183,57 @@ proofRegN-never {suc n} {xs} = beginₛ ⟦ regn-plug {n} ⟫ (reg ∥ regn n) ⟧ω (zipWith _∷_ (repeat 𝔽) xs) ≈⟨ proofSeq {c = regn-plug {n}} {d = reg ∥ regn n} {ins = zipWith _∷_ (repeat 𝔽) xs} ⟩ ⟦ reg ∥ regn n ⟧ω (⟦ regn-plug {n} ⟧ω (zipWith _∷_ (repeat 𝔽) xs)) ≈⟨ ⟦⟧ω[_]-cong {c = reg ∥ regn n} spec-B₃ (lemma-plug {xs = xs}) ⟩ ≈⟨ ⟦⟧ω[_]-cong {c = reg ∥ regn n} spec-B₃ (regn-plug-ω {xs = xs}) ⟩ ⟦ reg ∥ regn n ⟧ω (zipWith _++_ (zipWith _++_ (map (proj₁ ∘′ splitAt′ 1) xs) (repeat [ 𝔽 ])) (zipWith _∷_ (repeat 𝔽) (map (proj₂ ∘′ splitAt′ 1) xs))) ≈⟨ proofPar {c = reg} {d = regn n} {ins₁ = (zipWith _++_ (map (proj₁ ∘′ splitAt′ 1) xs) (repeat [ 𝔽 ]))} {ins₂ = zipWith _∷_ (repeat 𝔽) (map (proj₂ ∘′ splitAt′ 1) xs)} ⟩ {(zipWith _++_ (map (proj₁ ∘′ splitAt′ 1) xs) (repeat [ 𝔽 ]))} {zipWith _∷_ (repeat 𝔽) (map (proj₂ ∘′ splitAt′ 1) xs)} ⟩ zipWith _++_ (⟦ reg ⟧ω (zipWith _++_ (map (proj₁ ∘′ splitAt′ 1) xs) (repeat [ 𝔽 ]))) (⟦ regn n ⟧ω (zipWith _∷_ (repeat 𝔽) (map (proj₂ ∘′ splitAt′ 1) xs))) ≈⟨ zipWith-cong _++_ (proofReg-never-plain {xs = map (proj₁ ∘′ splitAt′ 1) xs}) (proofRegN-never {n = n} {xs = map (proj₂ ∘′ splitAt′ 1) xs}) ⟩ ≈⟨ zipWith-cong _++_ (proofReg-never-plain {map (proj₁ ∘′ splitAt′ 1) xs}) (proofRegN-never {n} {map (proj₂ ∘′ splitAt′ 1) xs}) ⟩ zipWith _++_ (repeat [ 𝔽 ]) (repeat (replicate 𝔽)) ≈⟨ lemmaRegN-never {n = n} ⟩ ≈⟨ regN-never-data𝔽 {n} ⟩ repeat (replicate 𝔽) ∎ₛ \end{code} % %<*lemma-repeat-empty> \AgdaTarget{lemma-repeat-empty} %<*repeat[]≈xs-Vec0> \AgdaTarget{repeat[]≈xs-Vec0} \begin{code} lemma-repeat-empty : ∀ {A} {xs : Stream (Vec A 0)} → repeat [] ≈ xs lemma-repeat-empty {xs = [] ∷ xs} = refl ∷ (♯ lemma-repeat-empty) repeat[]≈xs-Vec0 : ∀ {α} {xs : Stream (Vec α zero)} → repeat [] ≈ xs repeat[]≈xs-Vec0 {xs = [] ∷ xs} = refl ∷ ♯ repeat[]≈xs-Vec0 \end{code} % % %<*lemmaRegN-always> \AgdaTarget{lemmaRegN-always} %<*zipWith++-map-splitAt> \AgdaTarget{zipWith++-map-splitAt} \begin{code} lemmaRegN-always : ∀ {A} {n} {xs : Stream (Vec A (suc n))} → zipWith _++_ (map (proj₁ ∘′ splitAt′ 1) xs) (map (proj₂ ∘′ splitAt′ 1) xs) ≈ xs lemmaRegN-always {xs = x ∷ xs} with splitAt 1 x lemmaRegN-always {xs = .(xh ++ xt) ∷ xs} | xh , xt , refl = refl ∷ ♯ lemmaRegN-always zipWith++-map-splitAt : ∀ {n α} {xs : Stream (Vec α (suc n))} → zipWith _++_ (map (proj₁ ∘′ splitAt′ 1) xs) (map (proj₂ ∘′ splitAt′ 1) xs) ≈ xs zipWith++-map-splitAt {xs = x ∷ _} with splitAt 1 x zipWith++-map-splitAt {xs = .(xh ++ xt) ∷ _} | xh , xt , refl = refl ∷ ♯ zipWith++-map-splitAt \end{code} % % %<*proofRegN-always> \AgdaTarget{proofRegN-always} \begin{code} proofRegN-always : ∀ {n xs} → ⟦ regn n ⟧ω (zipWith _∷_ (repeat 𝕋) xs) ≈ xs proofRegN-always {zero} {xs} = transₛ (runᶜ-const {xs = zipWith _∷_ (repeat 𝕋) xs} []) lemma-repeat-empty proofRegN-always {zero} {xs} = transₛ (runᶜ-const {xs = zipWith _∷_ (repeat 𝕋) xs} []) repeat[]≈xs-Vec0 proofRegN-always {suc n} {xs} = beginₛ ⟦ regn (suc n) ⟧ω (zipWith _∷_ (repeat 𝕋) xs) ≈⟨ reflₛ ⟩ ⟦ regn-plug {n} ⟫ (reg ∥ regn n) ⟧ω (zipWith _∷_ (repeat 𝕋) xs) ≈⟨ proofSeq {c = regn-plug {n}} {d = reg ∥ regn n} {ins = zipWith _∷_ (repeat 𝕋) xs} ⟩ ⟦ reg ∥ regn n ⟧ω (⟦ regn-plug {n} ⟧ω (zipWith _∷_ (repeat 𝕋) xs)) ≈⟨ ⟦⟧ω[_]-cong {c = reg ∥ regn n} spec-B₃ (lemma-plug {xs = xs}) ⟩ ≈⟨ ⟦⟧ω[_]-cong {c = reg ∥ regn n} spec-B₃ (regn-plug-ω {xs = xs}) ⟩ ⟦ reg ∥ regn n ⟧ω (zipWith _++_ (zipWith _++_ (map (proj₁ ∘′ splitAt′ 1) xs) (repeat [ 𝕋 ])) (zipWith _∷_ (repeat 𝕋) (map (proj₂ ∘′ splitAt′ 1) xs))) ≈⟨ proofPar {c = reg} {d = regn n} {ins₁ = (zipWith _++_ (map (proj₁ ∘′ splitAt′ 1) xs) (repeat [ 𝕋 ]))} {ins₂ = zipWith _∷_ (repeat 𝕋) (map (proj₂ ∘′ splitAt′ 1) xs)} ⟩ zipWith _++_ (⟦ reg ⟧ω (zipWith _++_ (map (proj₁ ∘′ splitAt′ 1) xs) (repeat [ 𝕋 ]))) (⟦ regn n ⟧ω (zipWith _∷_ (repeat 𝕋) (map (proj₂ ∘′ splitAt′ 1) xs))) ≈⟨ zipWith-cong _++_ (proofReg-always-plain {xs = map (proj₁ ∘′ splitAt′ 1) xs}) (proofRegN-always {n = n} {xs = map (proj₂ ∘′ splitAt′ 1) xs}) ⟩ zipWith _++_ (map (proj₁ ∘′ splitAt′ 1) xs) (map (proj₂ ∘′ splitAt′ 1) xs) ≈⟨ lemmaRegN-always ⟩ ≈⟨ zipWith++-map-splitAt ⟩ xs ∎ₛ \end{code} %