Move SimState/BoolTrioSeq to ProofSamples

parent df9c921b
......@@ -12,17 +12,18 @@ open import Data.List.All using (All; _∷_; [])
open import Data.Product using (∃; _,_)
open import Data.Vec using (Vec; lookup; _++_; [_]; _∷_; [])
open import Data.CausalStream using (runᶜ′)
open import Data.Stream using (Stream; _∷_; head; tail; map; take; repeat; iterate; _≈_; map-cong)
open import Data.Stream using (Stream; _∷_; tail; map; take; repeat; iterate; _≈_; map-cong)
open import Data.Stream.Extra using (zip)
open import Data.Stream.Equality.WithTrans using (_≈ₚ_; _∷ₚ_; ≈ₚ-to-≈; reflₚ; transₚ)
open import Data.Stream.Properties using (≡-to-≈; map-id; map-compose; module Setoidₛ)
open import Data.Stream.Properties using (≡-to-≈; module Setoidₛ)
open Setoidₛ using () renaming (refl to reflₛ; sym to symₛ; trans to transₛ)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; inspect; cong) renaming ([_] to [_]ᵣ)
open import PiWare.Atomic.Bool using (Atomic-Bool)
open import PiWare.Semantics.Simulation Atomic-Bool using (delay′; module WithGates)
open import PiWare.Semantics.Simulation.BoolTrio using () renaming (spec to spec-B₃)
open WithGates spec-B₃ using (⟦_⟧ω; ⟦_⟧ᶜ; ⟦_⟧)
open import PiWare.Semantics.SimulationState Atomic-Bool using (mealy; ⟦_⟧ₛ[_]; DelayLoopₛ; Plugₛ; Gateₛ; _⟫ₛ_; ⟦_⟧ω'[_])
open import PiWare.Semantics.Simulation.BoolTrio using () renaming (spec to b₃)
open WithGates b₃ using (⟦_⟧ω; ⟦_⟧ᶜ; ⟦_⟧)
open import PiWare.Samples.BoolTrioSeq using (toggle; shift; reg; regCore)
open import Data.Serializable using (_⇕_; ⇕⊤; ⇕×)
open import Data.Serializable.Bool using (⇕Bool)
......@@ -36,6 +37,8 @@ open _⇕_ (⇕× ⦃ ⇕Bool ⦄ ⦃ ⇕Bool ⦄) using () renaming (⇓ to ⇓
%<*lookup#1-singletons>
\begin{code}
lookup#1-singletons : ∀ {ℓ} {α : Set ℓ} {a b c : Vec α 1} → [ lookup (# 1) (a ++ [ lookup (# 0) (b ++ c) ]) ] ≡ b
......@@ -43,7 +46,6 @@ lookup#1-singletons {a = _ ∷ []} {_ ∷ []} = refl
\end{code}
%</lookup#1-singletons>
%<*shift-runᶜ′>
\begin{code}
shift-runᶜ′ : ∀ {x⁻ x⁻¹ x⁰ x⁺} → runᶜ′ ⟦ shift ⟧ᶜ (x⁰ ∷ x⁻¹ ∷ x⁻) x⁺ ≈ₚ x⁻¹ ∷ ♯ (x⁰ ∷ ♯ x⁺)
......@@ -55,23 +57,59 @@ shift-runᶜ′ {x⁻² ∷ x⁻} {x⁻¹} {x⁰} {x¹ ∷ x⁺} =
%</shift-runᶜ′>
%<*proofShift-tail>
%<*proofShift>
\AgdaTarget{proofShift}
\begin{code}
proofShift-tail : ∀ {xs} → tail (⟦ shift ⟧ω xs) ≈ xs
proofShift-tail {_ ∷ x⁺} with ♭ x⁺ | inspect ♭ x⁺
proofShift-tail {_ ∷ _} | _ ∷ _ | [ xseq ]ᵣ = transₛ (≈ₚ-to-≈ shift-runᶜ′)
(refl ∷ ♯ transₛ (refl ∷ ♯ reflₛ) (symₛ (≡-to-≈ xseq)))
proofShift : ∀ {xs} → tail (⟦ shift ⟧ω xs) ≈ xs
proofShift {_ ∷ x⁺} with ♭ x⁺ | inspect ♭ x⁺
proofShift {_ ∷ _} | _ ∷ _ | [ xseq ]ᵣ = transₛ (≈ₚ-to-≈ shift-runᶜ′)
(refl ∷ ♯ transₛ (refl ∷ ♯ reflₛ) (symₛ (≡-to-≈ xseq)))
\end{code}
%</proofShift-tail>
%</proofShift>
%<*singleton∘lookup1>
\AgdaTarget{singleton∘lookup1}
\begin{code}
singleton∘lookup1 : ∀ {ℓ} {α : Set ℓ} {x : Vec α 1} {c} → [ lookup (# 1) (x ++ [ c ]) ] ≡ [ c ]
singleton∘lookup1 {x = _ ∷ []} = refl
\end{code}
%</singleton∘lookup1>
%<*proofShift-head>
%<*singleton∘lookup0>
\AgdaTarget{singleton∘lookup0}
\begin{code}
proofShift-head : ∀ {xs} → head (⟦ shift ⟧ω xs) ≡ [ 𝔽 ]
proofShift-head {(_ ∷ []) ∷ x⁺} with ♭ x⁺
proofShift-head {(_ ∷ []) ∷ _} | _ ∷ _ = refl
singleton∘lookup0 : ∀ {ℓ} {α : Set ℓ} {x : Vec α 1} {c} → [ lookup (# 0) (x ++ [ c ]) ] ≡ x
singleton∘lookup0 {x = _ ∷ []} = refl
\end{code}
%</proofShift-head>
%</singleton∘lookup0>
%<*lemmaShiftₚ>
\AgdaTarget{lemmaShiftₚ}
\begin{code}
lemmaShiftₚ : ∀ {c ins} → mealy ⟦ shift ⟧ₛ[ b₃ ] (DelayLoopₛ (⇓ c) Plugₛ) ins ≈ₚ ⇓ c ∷ ♯ ins
lemmaShiftₚ {c} {x ∷ _} = singleton∘lookup1 {x = x} ∷ₚ ♯ transₚ lemmaShiftₚ (singleton∘lookup0 {x = x} ∷ₚ ♯ reflₚ)
\end{code}
%</lemmaShiftₚ>
%<*lemmaShift>
\AgdaTarget{lemmaShift}
\begin{code}
lemmaShift : ∀ {c ins} → mealy ⟦ shift ⟧ₛ[ b₃ ] (DelayLoopₛ (⇓ c) Plugₛ) ins ≈ ⇓ c ∷ ♯ ins
lemmaShift = ≈ₚ-to-≈ $ lemmaShiftₚ ⟨ transₚ ⟩ (refl ∷ₚ ♯ reflₚ)
\end{code}
%</lemmaShift>
%<*proofShift′>
\AgdaTarget{proofShift′}
\begin{code}
proofShift′ : ∀ {ins} → ⟦ shift ⟧ω'[ b₃ ] ins ≈ ⇓ 𝔽 ∷ ♯ ins
proofShift′ {x ∷ xs} = singleton∘lookup1 {x = x} ∷ ♯ transₛ lemmaShift (singleton∘lookup0 ∷ ♯ reflₛ)
\end{code}
%</proofShift′>
......@@ -130,6 +168,30 @@ proofToggle = toggle-runᶜ′-𝕋 (toggleᶜ-start {[]})
%</proofToggle>
%<*proofToggle𝔽-𝕋-types>
\AgdaTarget{proofToggle𝔽′, proofToggle𝕋′}
\begin{code}
proofToggle𝔽′ : ∀ {ins} → mealy ⟦ toggle ⟧ₛ[ b₃ ] (Gateₛ ⟫ₛ DelayLoopₛ (⇓ 𝔽) ((Gateₛ ⟫ₛ Gateₛ) ⟫ₛ Plugₛ)) ins ≈ₚ map ⇓ (iterate not 𝕋)
proofToggle𝕋′ : ∀ {ins} → mealy ⟦ toggle ⟧ₛ[ b₃ ] (Gateₛ ⟫ₛ DelayLoopₛ (⇓ 𝕋) ((Gateₛ ⟫ₛ Gateₛ) ⟫ₛ Plugₛ)) ins ≈ₚ map ⇓ (iterate not 𝔽)
\end{code}
%</proofToggle𝔽-𝕋-types>
%<*proofToggle𝔽-𝕋-defs>
\begin{code}
proofToggle𝔽′ {_ ∷ _} = refl ∷ₚ ♯ transₚ proofToggle𝕋′ (refl ∷ₚ ♯ reflₚ)
proofToggle𝕋′ {_ ∷ _} = refl ∷ₚ ♯ transₚ proofToggle𝔽′ (refl ∷ₚ ♯ reflₚ)
\end{code}
%</proofToggle𝔽-𝕋-defs>
%<*proofToggle′>
\AgdaTarget{proofToggle′}
\begin{code}
proofToggle′ : ∀ {ins} → ⟦ toggle ⟧ω'[ b₃ ] ins ≈ map ⇓ (iterate not 𝕋)
proofToggle′ = ≈ₚ-to-≈ proofToggle𝔽′
\end{code}
%</proofToggle′>
%<*reg-delay′-never>
\begin{code}
......@@ -179,6 +241,7 @@ proofReg-always {x ∷ xs} = ≈ₚ-to-≈ $ transₚ reg-runᶜ′-always (refl
-- Typed stuff should be moved
proofShift̂ : ∀ {ins} → ⟦ shift̂ ⟧ω̂ (♭ ins) ≈ 𝔽 ∷ ins
proofShift̂ {ins} with ♭ ins | inspect ♭ ins
......
......@@ -30,7 +30,7 @@ open import PiWare.Semantics.Simulation.BoolTrio using () renaming (spec to spec
open WithGates spec-B₃ using (⟦_⟧ω; ⟦_⟧ᶜ; ⟦_⟧)
open import PiWare.Samples.BoolTrioSeq using (reg)
open import PiWare.Samples.RegN' using (regn-plug; regn)
open import PiWare.ProofSamples.BoolTrioSeq using (proofRegNeverLoad; proofRegAlwaysLoad)
open import PiWare.ProofSamples.BoolTrioSeq using (proofReg-never; proofReg-always)
open import PiWare.ProofSamples.EmptySeq using (runᶜ-const)
open import PiWare.Semantics.Simulation.Properties.SequentialCongruence Atomic-Bool using (⟦⟧ω[_]-cong)
open import PiWare.Semantics.Simulation.Properties.SequentialParalleling Atomic-Bool using () renaming (proof to proofPar)
......@@ -55,31 +55,31 @@ lemma {x ∷ xs} {v} = reduce x ∷ ♯ lemma
%</lemma>
%<*proofRegNeverLoadPlain>
\AgdaTarget{proofRegNeverLoadPlain}
%<*proofReg-never-plain>
\AgdaTarget{proofReg-never-plain}
\begin{code}
proofRegNeverLoadPlain : ∀ {xs} → ⟦ reg ⟧ω (zipWith _++_ xs (repeat [ false ])) ≈ repeat [ false ]
proofRegNeverLoadPlain {xs} = beginₛ
proofReg-never-plain : ∀ {xs} → ⟦ reg ⟧ω (zipWith _++_ xs (repeat [ false ])) ≈ repeat [ false ]
proofReg-never-plain {xs} = beginₛ
⟦ reg ⟧ω (zipWith _++_ xs (repeat [ false ]))
≈⟨ ⟦⟧ω[_]-cong {c = reg} spec-B₃ (lemma {xs = xs}) ⟩
⟦ reg ⟧ω (map ⇓² (zipWith _,_ (map ⇑¹ xs) (repeat false)))
≈⟨ proofRegNeverLoad {xs = map ⇑¹ xs} ⟩
≈⟨ proofReg-never {xs = map ⇑¹ xs} ⟩
map ⇓¹ (repeat false)
≈⟨ map-repeat ⟩
repeat [ false ] ∎ₛ
\end{code}
%</proofRegNeverLoadPlain>
%</proofReg-never-plain>
%<*proofRegAlwaysLoadPlain>
\AgdaTarget{proofRegAlwaysLoadPlain}
%<*proofReg-always-plain>
\AgdaTarget{proofReg-always-plain}
\begin{code}
proofRegAlwaysLoadPlain : ∀ {xs} → ⟦ reg ⟧ω (zipWith _++_ xs (repeat [ true ])) ≈ xs
proofRegAlwaysLoadPlain {xs} = beginₛ
proofReg-always-plain : ∀ {xs} → ⟦ reg ⟧ω (zipWith _++_ xs (repeat [ true ])) ≈ xs
proofReg-always-plain {xs} = beginₛ
⟦ reg ⟧ω (zipWith _++_ xs (repeat [ true ]))
≈⟨ ⟦⟧ω[_]-cong {c = reg} spec-B₃ (lemma {xs = xs}) ⟩
⟦ reg ⟧ω (map ⇓² (zipWith _,_ (map ⇑¹ xs) (repeat true)))
≈⟨ proofRegAlwaysLoad {xs = map ⇑¹ xs} ⟩
≈⟨ proofReg-always {xs = map ⇑¹ xs} ⟩
map ⇓¹ (map ⇑¹ xs)
≈⟨ symₛ map-compose ⟩
map (⇓¹ ∘′ ⇑¹) xs
......@@ -89,7 +89,7 @@ proofRegAlwaysLoadPlain {xs} = beginₛ
xs ∎ₛ
where postulate ⊥ : _
\end{code}
%</proofRegAlwaysLoadPlain>
%</proofReg-always-plain>
%<*lemma-plug''>
......@@ -135,21 +135,21 @@ lemma-plug {xs = x ∷ xs} = transₛ (≈ₚ-to-≈ lemma-plug') (refl ∷ (♯
%</lemma-plug>
%<*lemmaRegNNeverLoad>
\AgdaTarget{lemmaRegNNeverLoad}
%<*lemmaRegN-never>
\AgdaTarget{lemmaRegN-never}
\begin{code}
lemmaRegNNeverLoad : ∀ {n} → zipWith _++_ (repeat [ false ]) (repeat (replicate false)) ≈ repeat (replicate {n = suc n} false)
lemmaRegNNeverLoad = refl ∷ (♯ lemmaRegNNeverLoad)
lemmaRegN-never : ∀ {n} → zipWith _++_ (repeat [ false ]) (repeat (replicate false)) ≈ repeat (replicate {n = suc n} false)
lemmaRegN-never = refl ∷ ♯ lemmaRegN-never
\end{code}
%</lemmaRegNNeverLoad>
%</lemmaRegN-never>
%<*proofRegNNeverLoad>
\AgdaTarget{proofRegNNeverLoad}
%<*proofRegN-never>
\AgdaTarget{proofRegN-never}
\begin{code}
proofRegNNeverLoad : ∀ {n xs} → ⟦ regn n ⟧ω (zipWith _∷_ (repeat false) xs) ≈ repeat (replicate false)
proofRegNNeverLoad {zero} {xs} = runᶜ-const {xs = zipWith _∷_ (repeat false) xs} (replicate false)
proofRegNNeverLoad {suc n} {xs} = beginₛ
proofRegN-never : ∀ {n xs} → ⟦ regn n ⟧ω (zipWith _∷_ (repeat false) xs) ≈ repeat (replicate false)
proofRegN-never {zero} {xs} = runᶜ-const {xs = zipWith _∷_ (repeat false) xs} (replicate false)
proofRegN-never {suc n} {xs} = beginₛ
⟦ regn (suc n) ⟧ω (zipWith _∷_ (repeat false) xs)
≈⟨ reflₛ ⟩
⟦ regn-plug {n} ⟫ (reg ∥ regn n) ⟧ω (zipWith _∷_ (repeat false) xs)
......@@ -160,12 +160,12 @@ proofRegNNeverLoad {suc n} {xs} = beginₛ
≈⟨ proofPar {c = reg} {d = regn n}
{ins₁ = (zipWith _++_ (map (proj₁ ∘′ splitAt′ 1) xs) (repeat [ false ]))} {ins₂ = zipWith _∷_ (repeat false) (map (proj₂ ∘′ splitAt′ 1) xs)} ⟩
zipWith _++_ (⟦ reg ⟧ω (zipWith _++_ (map (proj₁ ∘′ splitAt′ 1) xs) (repeat [ false ]))) (⟦ regn n ⟧ω (zipWith _∷_ (repeat false) (map (proj₂ ∘′ splitAt′ 1) xs)))
≈⟨ zipWith-cong _++_ (proofRegNeverLoadPlain {xs = map (proj₁ ∘′ splitAt′ 1) xs}) (proofRegNNeverLoad {n = n} {xs = 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 _++_ (repeat [ false ]) (repeat (replicate false))
≈⟨ lemmaRegNNeverLoad {n = n} ⟩
≈⟨ lemmaRegN-never {n = n} ⟩
repeat (replicate false) ∎ₛ
\end{code}
%</proofRegNNeverLoad>
%</proofRegN-never>
%<*lemma-repeat-empty>
......@@ -177,22 +177,22 @@ lemma-repeat-empty {xs = [] ∷ xs} = refl ∷ (♯ lemma-repeat-empty)
%</lemma-repeat-empty>
%<*lemmaRegNAlwaysLoad>
\AgdaTarget{lemmaRegNAlwaysLoad}
%<*lemmaRegN-always>
\AgdaTarget{lemmaRegN-always}
\begin{code}
lemmaRegNAlwaysLoad : ∀ {A} {n} {xs : Stream (Vec A (suc n))} → zipWith _++_ (map (proj₁ ∘′ splitAt′ 1) xs) (map (proj₂ ∘′ splitAt′ 1) xs) ≈ xs
lemmaRegNAlwaysLoad {xs = x ∷ xs} with splitAt 1 x
lemmaRegNAlwaysLoad {xs = .(xh ++ xt) ∷ xs} | xh , xt , refl = refl ∷ (♯ lemmaRegNAlwaysLoad)
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
\end{code}
%</lemmaRegNAlwaysLoad>
%</lemmaRegN-always>
%<*proofRegNAlwaysLoad>
\AgdaTarget{proofRegNAlwaysLoad}
%<*proofRegN-always>
\AgdaTarget{proofRegN-always}
\begin{code}
proofRegNAlwaysLoad : ∀ {n xs} → ⟦ regn n ⟧ω (zipWith _∷_ (repeat true) xs) ≈ xs
proofRegNAlwaysLoad {zero} {xs} = transₛ (runᶜ-const {xs = zipWith _∷_ (repeat true) xs} []) lemma-repeat-empty
proofRegNAlwaysLoad {suc n} {xs} = beginₛ
proofRegN-always : ∀ {n xs} → ⟦ regn n ⟧ω (zipWith _∷_ (repeat true) xs) ≈ xs
proofRegN-always {zero} {xs} = transₛ (runᶜ-const {xs = zipWith _∷_ (repeat true) xs} []) lemma-repeat-empty
proofRegN-always {suc n} {xs} = beginₛ
⟦ regn (suc n) ⟧ω (zipWith _∷_ (repeat true) xs)
≈⟨ reflₛ ⟩
⟦ regn-plug {n} ⟫ (reg ∥ regn n) ⟧ω (zipWith _∷_ (repeat true) xs)
......@@ -203,9 +203,9 @@ proofRegNAlwaysLoad {suc n} {xs} = beginₛ
≈⟨ proofPar {c = reg} {d = regn n}
{ins₁ = (zipWith _++_ (map (proj₁ ∘′ splitAt′ 1) xs) (repeat [ true ]))} {ins₂ = zipWith _∷_ (repeat true) (map (proj₂ ∘′ splitAt′ 1) xs)} ⟩
zipWith _++_ (⟦ reg ⟧ω (zipWith _++_ (map (proj₁ ∘′ splitAt′ 1) xs) (repeat [ true ]))) (⟦ regn n ⟧ω (zipWith _∷_ (repeat true) (map (proj₂ ∘′ splitAt′ 1) xs)))
≈⟨ zipWith-cong _++_ (proofRegAlwaysLoadPlain {xs = map (proj₁ ∘′ splitAt′ 1) xs}) (proofRegNAlwaysLoad {n = n} {xs = 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)
≈⟨ lemmaRegNAlwaysLoad
≈⟨ lemmaRegN-always
xs ∎ₛ
\end{code}
%</proofRegNAlwaysLoad>
%</proofRegN-always>
......@@ -27,7 +27,7 @@ open import PiWare.Semantics.Simulation.BoolTrio using () renaming (spec to spec
open WithGates spec-B₃ using (⟦_⟧ω; ⟦_⟧)
open import PiWare.Samples.BoolTrioSeq using (reg)
open import PiWare.Samples.RegN using (+⋎-*2; regn-regs; regn-equalise; regn-join; regn-distribute; regn)
open import PiWare.ProofSamples.BoolTrioSeq using (proofRegNeverLoad; proofRegAlwaysLoad)
open import PiWare.ProofSamples.BoolTrioSeq using (proofReg-never; proofReg-always)
open import PiWare.ProofSamples.EmptySeq using (runᶜ-const)
open import PiWare.ProofSamples.EqPlug Atomic-Bool using (vecCoerce; unfold-vecCoerce; vecCoerce-rightInverse; eq⤨⊑ωid)
open import PiWare.ProofSamples.RegN.Distribution using (lemma-regn-distribute)
......@@ -90,32 +90,32 @@ zipWith-++-⇑ {x ∷ _} {y} = reduce x ∷ ♯ zipWith-++-⇑
%</zipWith-++-⇑>
%<*proofRegNeverLoadPlain>
\AgdaTarget{proofRegNeverLoadPlain}
%<*proofReg-never-plain>
\AgdaTarget{proofReg-never-plain}
\begin{code}
proofRegNeverLoadPlain : ∀ {xs} → ⟦ reg ⟧ω (zipWith _++_ xs (repeat [ 𝔽 ])) ≈ repeat [ 𝔽 ]
proofRegNeverLoadPlain {xs} = beginₛ
proofReg-never-plain : ∀ {xs} → ⟦ reg ⟧ω (zipWith _++_ xs (repeat [ 𝔽 ])) ≈ repeat [ 𝔽 ]
proofReg-never-plain {xs} = beginₛ
⟦ reg ⟧ω (zipWith _++_ xs (repeat [ 𝔽 ])) ≈⟨ ⟦⟧ω[_]-cong {c = reg} spec-B₃ (zipWith-++-⇑ {xs}) ⟩
⟦ reg ⟧ω (map ⇓² (zipWith _,_ (map ⇑ xs) (repeat 𝔽))) ≈⟨ proofRegNeverLoad {xs = map ⇑ xs} ⟩
⟦ reg ⟧ω (map ⇓² (zipWith _,_ (map ⇑ xs) (repeat 𝔽))) ≈⟨ proofReg-never {xs = map ⇑ xs} ⟩
map ⇓ (repeat 𝔽) ≈⟨ map-repeat ⟩
repeat [ 𝔽 ] ∎ₛ
\end{code}
%</proofRegNeverLoadPlain>
%</proofReg-never-plain>
%<*proofRegAlwaysLoadPlain>
\AgdaTarget{proofRegAlwaysLoadPlain}
%<*proofReg-always-plain>
\AgdaTarget{proofReg-always-plain}
\begin{code}
proofRegAlwaysLoadPlain : ∀ {xs} → ⟦ reg ⟧ω (zipWith _++_ xs (repeat [ 𝕋 ])) ≈ xs
proofRegAlwaysLoadPlain {xs} = beginₛ
proofReg-always-plain : ∀ {xs} → ⟦ reg ⟧ω (zipWith _++_ xs (repeat [ 𝕋 ])) ≈ xs
proofReg-always-plain {xs} = beginₛ
⟦ reg ⟧ω (zipWith _++_ xs (repeat [ 𝕋 ])) ≈⟨ ⟦⟧ω[_]-cong {c = reg} spec-B₃ (zipWith-++-⇑ {xs}) ⟩
⟦ reg ⟧ω (map ⇓² (zipWith _,_ (map ⇑ xs) (repeat 𝕋))) ≈⟨ proofRegAlwaysLoad {map ⇑ xs} ⟩
⟦ reg ⟧ω (map ⇓² (zipWith _,_ (map ⇑ xs) (repeat 𝕋))) ≈⟨ proofReg-always {map ⇑ xs} ⟩
map ⇓ (map ⇑ xs) ≈⟨ symₛ map-compose ⟩
map (⇓ ∘′ ⇑) xs ≈⟨ map-cong-fun singleton∘head ⟩
map id xs ≈⟨ map-id ⟩
xs ∎ₛ
\end{code}
%</proofRegAlwaysLoadPlain>
%</proofReg-always-plain
%<*⋎-replicate>
......@@ -163,13 +163,13 @@ repeat-replicate {n} = sym (vecCoerce-replicate {n}) ∷ ♯ repeat-replicate {n
%</repeat-replicate>
%<*lemmaRegNNeverLoad>
\AgdaTarget{lemmaRegNNeverLoad}
%<*lemmaRegN-never>
\AgdaTarget{lemmaRegN-never}
\begin{code}
postulate lemmaRegNNeverLoad : ∀ {n} {xs : Stream (W n)} → ⟦ regn-regs n ⟧ω (map (λ x → (vc⋎ n) (x ⋎ replicate {n = n} 𝔽)) xs) ≈ map (vc* n) (repeat (replicate 𝔽))
postulate lemmaRegN-never : ∀ {n} {xs : Stream (W n)} → ⟦ regn-regs n ⟧ω (map (λ x → (vc⋎ n) (x ⋎ replicate {n = n} 𝔽)) xs) ≈ map (vc* n) (repeat (replicate 𝔽))
\end{code}
lemmaRegNNeverLoad {zero} {xs} = transₛ (runᶜ-const {xs = map (λ x → (vc⋎ zero) (x ⋎ replicate 𝔽)) xs} (replicate 𝔽)) (symₛ map-id)
lemmaRegNNeverLoad {suc n} {xs} = beginₛ
lemmaRegN-never {zero} {xs} = transₛ (runᶜ-const {xs = map (λ x → (vc⋎ zero) (x ⋎ replicate 𝔽)) xs} (replicate 𝔽)) (symₛ map-id)
lemmaRegN-never {suc n} {xs} = beginₛ
⟦ regn-regs (suc n) ⟧ω (map (λ x → (vc⋎ (suc n)) (x ⋎ replicate {n = suc n} 𝔽)) xs)
≈⟨ ⟦⟧ω[_]-cong {c = regn-regs (suc n)} spec-B₃ (map-⋎-replicate {n} {xs = xs}) ⟩
⟦ reg ∥ regn-regs n ⟧ω (zipWith _++_
......@@ -183,11 +183,11 @@ lemmaRegNNeverLoad {suc n} {xs} = beginₛ
(⟦ regn-regs n ⟧ω (map (λ x → (vc⋎ n) (x ⋎ replicate {n = n} 𝔽)) (map p₂∘split1 xs)))
≈⟨ zipWith-cong _++_
(proofRegNeverLoadPlain {xs = map p₁∘split1 xs})
(lemmaRegNNeverLoad {n = n} {xs = map p₂∘split1 xs}) ⟩
(lemmaRegN-never {n = n} {xs = map p₂∘split1 xs}) ⟩
zipWith _++_ (repeat [ 𝔽 ]) (map (vc* n) (repeat (replicate {n = n} 𝔽)))
≈⟨ repeat-replicate {n} ⟩
map (vc* (suc n)) (repeat (replicate {n = suc n} 𝔽)) ∎ₛ
%</lemmaRegNNeverLoad>
%</lemmaRegN-never>
%<*map-id-Stream-Vec0>
......@@ -279,27 +279,27 @@ reg-remove-eq-plugs {n} {v} {xs} {ys} p = beginₛ
%</reg-remove-eq-plugs>
%<*proofRegNNeverLoad>
\AgdaTarget{proofRegNNeverLoad}
%<*proofRegN-never>
\AgdaTarget{proofRegN-never}
\begin{code}
proofRegNNeverLoad : ∀ {n xs} → ⟦ regn n ⟧ω (zipWith _∷_ (repeat 𝔽) xs) ≈ repeat (replicate 𝔽)
proofRegNNeverLoad {n} {xs} = beginₛ
proofRegN-never : ∀ {n xs} → ⟦ regn n ⟧ω (zipWith _∷_ (repeat 𝔽) xs) ≈ repeat (replicate 𝔽)
proofRegN-never {n} {xs} = beginₛ
⟦ regn-distribute n ⟫ (regn-equalise n ⟫ regn-regs n ⟫ regn-join n) ⟧ω (zipWith _∷_ (repeat 𝔽) xs)
≈⟨ proofSeq {c = regn-distribute n} {d = regn-equalise n ⟫ regn-regs n ⟫ regn-join n} {ins = zipWith _∷_ (repeat 𝔽) xs} ⟩
⟦ regn-equalise n ⟫ regn-regs n ⟫ regn-join n ⟧ω (⟦ regn-distribute n ⟧ω (zipWith _∷_ (repeat 𝔽) xs))
≈⟨ ⟦⟧ω[_]-cong {c = regn-equalise n ⟫ regn-regs n ⟫ regn-join n} spec-B₃ (lemma-regn-distribute {xs = xs}) ⟩
⟦ regn-equalise n ⟫ regn-regs n ⟫ regn-join n ⟧ω (map (λ x → x ⋎ replicate 𝔽) xs)
≈⟨ reg-remove-eq-plugs {xs = xs} {ys = repeat (replicate 𝔽)} (lemmaRegNNeverLoad {xs = xs}) ⟩
≈⟨ reg-remove-eq-plugs {xs = xs} {ys = repeat (replicate 𝔽)} (lemmaRegN-never {xs = xs}) ⟩
repeat (replicate 𝔽) ∎ₛ
\end{code}
%</proofRegNNeverLoad>
%</proofRegN-never>
%<*proofRegNAlwaysLoad>
\AgdaTarget{proofRegNAlwaysLoad}
%<*proofRegN-always>
\AgdaTarget{proofRegN-always}
\begin{code}
proofRegNAlwaysLoad : ∀ {n xs} → ⟦ regn n ⟧ω (zipWith _∷_ (repeat 𝕋) xs) ≈ xs
proofRegNAlwaysLoad {n} {xs} = beginₛ
proofRegN-always : ∀ {n xs} → ⟦ regn n ⟧ω (zipWith _∷_ (repeat 𝕋) xs) ≈ xs
proofRegN-always {n} {xs} = beginₛ
⟦ regn-distribute n ⟫ (regn-equalise n ⟫ regn-regs n ⟫ regn-join n) ⟧ω (zipWith _∷_ (repeat 𝕋) xs)
≈⟨ proofSeq {c = regn-distribute n} {d = regn-equalise n ⟫ regn-regs n ⟫ regn-join n} {ins = zipWith _∷_ (repeat 𝕋) xs} ⟩
⟦ regn-equalise n ⟫ regn-regs n ⟫ regn-join n ⟧ω (⟦ regn-distribute n ⟧ω (zipWith _∷_ (repeat 𝕋) xs))
......@@ -308,4 +308,4 @@ proofRegNAlwaysLoad {n} {xs} = beginₛ
≈⟨ reg-remove-eq-plugs {xs = xs} {ys = xs} (lemmaRegNAlwaysLoad {xs = xs}) ⟩
xs ∎ₛ
\end{code}
%</proofRegNAlwaysLoad>
%</proofRegN-always>
\begin{code}
module PiWare.Semantics.SimulationState.BoolTrioSeq where
open import Function using (_$_; _⟨_⟩_)
open import Data.Bool.Base using (not) renaming (false to 𝔽; true to 𝕋)
open import Data.Product using (_,_)
open import Coinduction using (♯_)
open import Data.Stream using (_∷_; map; iterate; _≈_)
open import Data.Stream.Equality.WithTrans using (_≈ₚ_; _∷ₚ_; ≈ₚ-to-≈; transₚ; reflₚ)
open import Data.Stream.Properties using (module Setoidₛ)
open Setoidₛ using () renaming (refl to reflₛ; trans to transₛ)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
open import Data.Fin using (#_)
open import Data.Vec using (Vec; lookup; []; _++_; _∷_; [_])
open import PiWare.Atomic.Bool using (Atomic-Bool)
open import PiWare.Semantics.Simulation.BoolTrio using () renaming (spec to b₃)
open import PiWare.Semantics.SimulationState Atomic-Bool using (mealy; Gateₛ; Plugₛ; _⟫ₛ_; DelayLoopₛ; ⟦_⟧ω'[_]; ⟦_⟧ₛ[_])
open import PiWare.Samples.BoolTrioSeq using (toggle; shift)
\end{code}
\begin{code}
open import Data.Serializable using (_⇕_)
open import Data.Serializable.Bool using (⇕Bool)
open _⇕_ ⇕Bool using (⇓)
\end{code}
%<*singleton∘lookup1>
\AgdaTarget{singleton∘lookup1}
\begin{code}
singleton∘lookup1 : ∀ {ℓ} {α : Set ℓ} {x : Vec α 1} {c} → [ lookup (# 1) (x ++ [ c ]) ] ≡ [ c ]
singleton∘lookup1 {x = _ ∷ []} = refl
\end{code}
%</singleton∘lookup1>
%<*singleton∘lookup0>
\AgdaTarget{singleton∘lookup0}
\begin{code}
singleton∘lookup0 : ∀ {ℓ} {α : Set ℓ} {x : Vec α 1} {c} → [ lookup (# 0) (x ++ c ∷ []) ] ≡ x
singleton∘lookup0 {x = _ ∷ []} = refl
\end{code}
%</singleton∘lookup0>
%<*lemmaShiftₚ>
\AgdaTarget{lemmaShiftₚ}
\begin{code}
lemmaShiftₚ : ∀ {c ins} → mealy ⟦ shift ⟧ₛ[ b₃ ] (DelayLoopₛ (⇓ c) Plugₛ) ins ≈ₚ ⇓ c ∷ ♯ ins
lemmaShiftₚ {c} {x ∷ _} = singleton∘lookup1 {x = x} ∷ₚ ♯ transₚ lemmaShiftₚ (singleton∘lookup0 {x = x} ∷ₚ ♯ reflₚ)
\end{code}
%</lemmaShiftₚ>
%<*lemmaShift>
\AgdaTarget{lemmaShift}
\begin{code}
lemmaShift : ∀ {c ins} → mealy ⟦ shift ⟧ₛ[ b₃ ] (DelayLoopₛ (⇓ c) Plugₛ) ins ≈ ⇓ c ∷ ♯ ins
lemmaShift = ≈ₚ-to-≈ $ lemmaShiftₚ ⟨ transₚ ⟩ (refl ∷ₚ ♯ reflₚ)
\end{code}
%</lemmaShift>
%<*proofShift>
\AgdaTarget{proofShift}
\begin{code}
proofShift : ∀ {ins} → ⟦ shift ⟧ω'[ b₃ ] ins ≈ ⇓ 𝔽 ∷ ♯ ins
proofShift {x ∷ xs} = singleton∘lookup1 {x = x} ∷ ♯ transₛ lemmaShift (singleton∘lookup0 ∷ ♯ reflₛ)
\end{code}
%</proofShift>
%<*proofToggle𝔽>
\AgdaTarget{proofToggle𝔽}
\begin{code}
proofToggle𝔽 : ∀ {ins} → mealy ⟦ toggle ⟧ₛ[ b₃ ] (Gateₛ ⟫ₛ DelayLoopₛ (⇓ 𝔽) ((Gateₛ ⟫ₛ Gateₛ) ⟫ₛ Plugₛ)) ins ≈ₚ map ⇓ (iterate not 𝕋)
proofToggle𝕋 : ∀ {ins} → mealy ⟦ toggle ⟧ₛ[ b₃ ] (Gateₛ ⟫ₛ DelayLoopₛ (⇓ 𝕋) ((Gateₛ ⟫ₛ Gateₛ) ⟫ₛ Plugₛ)) ins ≈ₚ map ⇓ (iterate not 𝔽)
\end{code}
%</proofToggle𝔽>
%<*proofToggle𝔽>
\AgdaTarget{proofToggle𝔽}
\begin{code}
proofToggle𝔽 {x ∷ xs} = refl ∷ₚ ♯ transₚ proofToggle𝕋 (refl ∷ₚ ♯ reflₚ)
proofToggle𝕋 {x ∷ xs} = refl ∷ₚ ♯ transₚ proofToggle𝔽 (refl ∷ₚ ♯ reflₚ)
\end{code}
%</proofToggle𝔽>
%<*proofToggle>
\AgdaTarget{proofToggle}
\begin{code}
proofToggle : ∀ {ins} → ⟦ toggle ⟧ω'[ b₃ ] ins ≈ map ⇓ (iterate not 𝕋)
proofToggle = ≈ₚ-to-≈ proofToggle𝔽
\end{code}
%</proofToggle>
......@@ -97,7 +97,6 @@ import PiWare.Semantics.Simulation.Semigroup.Base
import PiWare.Semantics.Simulation.Semigroup.Op2
import PiWare.Semantics.Simulation.Testing
import PiWare.Semantics.Simulation
import PiWare.Semantics.SimulationState.BoolTrioSeq -- M
import PiWare.Semantics.SimulationState.Properties.SequentialCongruence -- M
import PiWare.Semantics.SimulationState.Properties.SequentialParalleling -- M
import PiWare.Semantics.SimulationState.Properties.SequentialSequencing -- M
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment