Almost all of ProofSamples into Samples

parent b7cef0b5
\begin{code}
module PiWare.ProofSamples.BoolTrioSeq where
open import Function using (_$_; _⟨_⟩_; _∘_)
open import Data.Unit.Base using (⊤; tt)
open import Data.Bool.Base using (Bool; not) renaming (false to 𝔽; true to 𝕋)
open import Coinduction using (♯_; ♭)
open import Data.Fin using (#_)
open import Data.List using ([]; _∷_)
open import Data.List.NonEmpty using (_∷_) renaming ([_] to [_]⁺)
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; _∷_; 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-≈; 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.Gates.BoolTrio using () renaming (BoolTrio to B₃)
open import PiWare.Semantics.Simulation Atomic-Bool using (delay′; module WithGates)
open import PiWare.Semantics.Simulation.BoolTrio using () renaming (spec to spec-B₃)
open import PiWare.Semantics.SimulationState Atomic-Bool using (mealy; ⟦_⟧ₛ[_]; DelayLoopₛ; Plugₛ; Gateₛ; _⟫ₛ_; ⟦_⟧ω'[_]; ℂₛ)
renaming (module WithGates to WithGatesₛ)
open WithGates spec-B₃ using (⟦_⟧ω; ⟦_⟧ᶜ; ⟦_⟧)
open WithGatesₛ spec-B₃ using (⟦_⟧ₛ; ⟦_⟧ω')
open import PiWare.Samples.BoolTrioSeq using (toggle; shift; reg; regCore)
open import Data.Serializable using (_⇕_; ⇕⊤; ⇕×)
open import Data.Serializable.Bool using (⇕Bool)
\end{code}
\begin{code}
open _⇕_ ⇕Bool
open _⇕_ {⊤} {Bool} ⇕⊤ using () renaming (⇓ to ⇓⊤)
open _⇕_ (⇕× ⦃ ⇕Bool ⦄ ⦃ ⇕Bool ⦄) using () renaming (⇓ to ⇓²)
\end{code}
%<*lookup#1-singletons>
\begin{code}
lookup#1-singletons : ∀ {ℓ} {α : Set ℓ} {a b c : Vec α 1} → [ lookup (# 1) (a ++ [ lookup (# 0) (b ++ c) ]) ] ≡ b
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⁺)
shift-runᶜ′ {[]} {x⁻¹} {x⁰} {x¹ ∷ x⁺} =
lookup#1-singletons {a = x⁰} {x⁻¹} ∷ₚ ♯ transₚ (shift-runᶜ′ {x⁻¹ ∷ []} {x⁰} {x¹} {♭ x⁺}) (refl ∷ₚ ♯ (refl ∷ₚ ♯ reflₚ))
shift-runᶜ′ {x⁻² ∷ x⁻} {x⁻¹} {x⁰} {x¹ ∷ x⁺} =
lookup#1-singletons {a = x⁰} {x⁻¹} ∷ₚ ♯ transₚ (shift-runᶜ′ {x⁻¹ ∷ x⁻² ∷ x⁻} {x⁰} {x¹} {♭ x⁺}) (refl ∷ₚ ♯ (refl ∷ₚ ♯ reflₚ))
\end{code}
%</shift-runᶜ′>
%<*proofShift>
\AgdaTarget{proofShift}
\begin{code}
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>
%<*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 ⟧ₛ (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 ⟧ₛ (DelayLoopₛ (⇓ c) Plugₛ) ins ≈ ⇓ c ∷ ♯ ins
lemmaShift = ≈ₚ-to-≈ $ lemmaShiftₚ ⟨ transₚ ⟩ (refl ∷ₚ ♯ reflₚ)
\end{code}
%</lemmaShift>
%<*proofShift′>
\AgdaTarget{proofShift′}
\begin{code}
proofShift′ : ∀ {ins} → ⟦ shift ⟧ω' ins ≈ ⇓ 𝔽 ∷ ♯ ins
proofShift′ {x ∷ xs} = singleton∘lookup1 {x = x} ∷ ♯ transₛ lemmaShift (singleton∘lookup0 ∷ ♯ reflₛ)
\end{code}
%</proofShift′>
%<*toggleᶜ-start>
\begin{code}
toggleᶜ-start : ∀ {x⁰} → ⟦ toggle ⟧ᶜ [ x⁰ ]⁺ ≡ [ 𝕋 ]
toggleᶜ-start = refl
\end{code}
%</toggleᶜ-start>
%<*[_]-injective>
\begin{code}
[_]-injective : ∀ {ℓ} {α : Set ℓ} {x y : α} → [ x ] ≡ [ y ] → x ≡ y
[_]-injective refl = refl
\end{code}
%</[_]-injective>
%<*toggleᶜ-𝔽⇒𝕋>
\begin{code}
toggleᶜ-𝔽⇒𝕋 : ∀ {x⁻ x⁻¹ x⁰} → ⟦ toggle ⟧ᶜ (x⁻¹ ∷ x⁻) ≡ ⇓ 𝔽 → ⟦ toggle ⟧ᶜ (x⁰ ∷ x⁻¹ ∷ x⁻) ≡ ⇓ 𝕋
toggleᶜ-𝔽⇒𝕋 {[]} ()
toggleᶜ-𝔽⇒𝕋 {_ ∷ _} p = cong ([_] ∘ not) ([_]-injective p)
\end{code}
%</toggleᶜ-𝔽⇒𝕋>
%<*toggleᶜ-𝕋⇒𝔽>
\begin{code}
toggleᶜ-𝕋⇒𝔽 : ∀ {x⁻ x⁻¹ x⁰} → ⟦ toggle ⟧ᶜ (x⁻¹ ∷ x⁻) ≡ ⇓ 𝕋 → ⟦ toggle ⟧ᶜ (x⁰ ∷ x⁻¹ ∷ x⁻) ≡ ⇓ 𝔽
toggleᶜ-𝕋⇒𝔽 {[]} _ = refl
toggleᶜ-𝕋⇒𝔽 {_ ∷ _} p = cong ([_] ∘ not) ([_]-injective p)
\end{code}
%</toggleᶜ-𝕋⇒𝔽>
%<*toggle-runᶜ′-𝕋-𝔽-types>
\begin{code}
toggle-runᶜ′-𝕋 : ∀ {x⁻ x⁰ x⁺} → ⟦ toggle ⟧ᶜ (x⁰ ∷ x⁻) ≡ ⇓ 𝕋 → runᶜ′ ⟦ toggle ⟧ᶜ (x⁰ ∷ x⁻) x⁺ ≈ map ⇓ (iterate not 𝕋)
toggle-runᶜ′-𝔽 : ∀ {x⁻ x⁰ x⁺} → ⟦ toggle ⟧ᶜ (x⁰ ∷ x⁻) ≡ ⇓ 𝔽 → runᶜ′ ⟦ toggle ⟧ᶜ (x⁰ ∷ x⁻) x⁺ ≈ map ⇓ (iterate not 𝔽)
\end{code}
%</toggle-runᶜ′-𝕋-𝔽-types>
%<*toggle-runᶜ′-𝕋-𝔽-defs>
\begin{code}
toggle-runᶜ′-𝕋 {x⁻} {x⁰} {x¹ ∷ _} p = p ∷ ♯ toggle-runᶜ′-𝔽 (toggleᶜ-𝕋⇒𝔽 {x⁻} {x⁰} {x¹} p)
toggle-runᶜ′-𝔽 {x⁻} {x⁰} {x¹ ∷ _} p = p ∷ ♯ toggle-runᶜ′-𝕋 (toggleᶜ-𝔽⇒𝕋 {x⁻} {x⁰} {x¹} p)
\end{code}
%</toggle-runᶜ′-𝕋-𝔽-defs>
%<*proofToggle>
\begin{code}
proofToggle : ⟦ toggle ⟧ω (map ⇓⊤ (repeat tt)) ≈ map ⇓ (iterate not 𝕋)
proofToggle = toggle-runᶜ′-𝕋 (toggleᶜ-start {[]})
\end{code}
%</proofToggle>
\begin{code}
stateToggle𝔽 stateToggle𝕋 : ℂₛ B₃ toggle
\end{code}
%<*stateToggle𝔽-𝕋>
\AgdaTarget{stateToggle𝔽, stateToggle𝕋}
\begin{code}
stateToggle𝔽 = Gateₛ ⟫ₛ DelayLoopₛ (⇓ 𝔽) ((Gateₛ ⟫ₛ Gateₛ) ⟫ₛ Plugₛ)
stateToggle𝕋 = Gateₛ ⟫ₛ DelayLoopₛ (⇓ 𝕋) ((Gateₛ ⟫ₛ Gateₛ) ⟫ₛ Plugₛ)
\end{code}
%</stateToggle𝔽-stateToggle𝕋>
%<*proofToggle𝔽-𝕋-types>
\AgdaTarget{proofToggle𝔽′, proofToggle𝕋′}
\begin{code}
proofToggle𝔽′ : ∀ {ins} → mealy ⟦ toggle ⟧ₛ stateToggle𝔽 ins ≈ₚ map ⇓ (iterate not 𝕋)
proofToggle𝕋′ : ∀ {ins} → mealy ⟦ toggle ⟧ₛ stateToggle𝕋 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 ⟧ω' ins ≈ map ⇓ (iterate not 𝕋)
proofToggle′ = ≈ₚ-to-≈ proofToggle𝔽′
\end{code}
%</proofToggle′>
%<*reg-delay′-never>
\begin{code}
reg-delay′-never : ∀ {d⁰ x⁻} → All (λ x → ∃ (λ d → ⇓² (d , 𝔽) ≡ x)) x⁻ → delay′ 1 {i = 2} ⟦ regCore ⟧ (⇓² (d⁰ , 𝔽)) x⁻ ≡ 𝔽 ∷ 𝔽 ∷ []
reg-delay′-never {x⁻ = []} p = refl
reg-delay′-never {x⁻ = .(d⁻¹ ∷ 𝔽 ∷ []) ∷ xs} ((d⁻¹ , refl) ∷ pxs) rewrite reg-delay′-never {d⁻¹} pxs = refl
\end{code}
%</reg-delay′-never>
%<*regᶜ-never>
\begin{code}
regᶜ-never : ∀ {d⁰ x⁻} → All (λ x → ∃ (λ d → ⇓² (d , 𝔽) ≡ x)) x⁻ → ⟦ reg ⟧ᶜ (⇓² (d⁰ , 𝔽) ∷ x⁻) ≡ ⇓ 𝔽
regᶜ-never {d⁰} {x⁻} p rewrite reg-delay′-never {d⁰} p = refl
\end{code}
%</regᶜ-never>
%<*reg-runᶜ′-never>
\begin{code}
reg-runᶜ′-never : ∀ {d⁰ x⁺ x⁻} → All (λ c → ∃ (λ i → ⇓² (i , 𝔽) ≡ c)) x⁻
→ runᶜ′ ⟦ reg ⟧ᶜ (⇓² (d⁰ , 𝔽) ∷ x⁻) (map ⇓² (x⁺ ⟨ zip ⟩ repeat 𝔽)) ≈ map ⇓ (repeat 𝔽)
reg-runᶜ′-never {d⁰} {x⁺ = _ ∷ _} p rewrite regᶜ-never {d⁰} p = refl ∷ ♯ reg-runᶜ′-never ((d⁰ , refl) ∷ p)
\end{code}
%</reg-runᶜ′-never>
%<*proofReg-never>
\begin{code}
proofReg-never : ∀ {xs} → ⟦ reg ⟧ω (map ⇓² (xs ⟨ zip ⟩ repeat 𝔽)) ≈ map ⇓ (repeat 𝔽)
proofReg-never {_ ∷ _} = reg-runᶜ′-never []
\end{code}
%</proofReg-never>
%<*reg-runᶜ′-always>
\begin{code}
reg-runᶜ′-always : ∀ {d⁰ x⁻ x⁺} → runᶜ′ ⟦ reg ⟧ᶜ (⇓² (d⁰ , 𝕋) ∷ x⁻) (map ⇓² (x⁺ ⟨ zip ⟩ repeat 𝕋)) ≈ₚ map ⇓ (d⁰ ∷ ♯ x⁺)
reg-runᶜ′-always {x⁻ = []} {x⁺ = _ ∷ _} = refl ∷ₚ ♯ transₚ reg-runᶜ′-always (refl ∷ₚ ♯ reflₚ)
reg-runᶜ′-always {x⁻ = _ ∷ _} {x⁺ = _ ∷ _} = refl ∷ₚ ♯ transₚ reg-runᶜ′-always (refl ∷ₚ ♯ reflₚ)
\end{code}
%</reg-runᶜ′-always>
%<*proofReg-always>
\begin{code}
proofReg-always : ∀ {xs} → ⟦ reg ⟧ω (map ⇓² (xs ⟨ zip ⟩ repeat 𝕋)) ≈ map ⇓ xs
proofReg-always {x ∷ xs} = ≈ₚ-to-≈ $ transₚ reg-runᶜ′-always (refl ∷ₚ ♯ reflₚ)
\end{code}
%</proofReg-always>
-- Typed stuff should be moved
proofShift̂ : ∀ {ins} → ⟦ shift̂ ⟧ω̂ (♭ ins) ≈ 𝔽 ∷ ins
proofShift̂ {ins} with ♭ ins | inspect ♭ ins
proofShift̂ | x ∷ xs | [ inseq ] with ♭ xs | proofShiftHead̂ {x ∷ xs} | proofShiftTail̂ {x ∷ xs}
proofShift̂ | x ∷ xs | [ inseq ] | x₁ ∷ xs₁ | p1 | p2 = p1 ∷ (♯ strans p2 (ssym (≡-to-≈ inseq)))
proofShiftTail̂ : ∀ {ins} → tail (⟦ shift̂ ⟧ω̂ ins) ≈ ins
proofShiftTail̂ {ins} = liftProof {α̂ = ⇕Bool} {β̂ = ⇕Bool} {f = shift} {xs = ins}
(λ {_} {_} {_} {s} → (tail-map-swap {s = s}))
(λ x → refl)
proofShiftTail
proofShiftHead̂ : ∀ {ins} → head (⟦ shift̂ ⟧ω̂ ins) ≡ 𝔽
proofShiftHead̂ {_ ∷ xs} with ♭ xs
proofShiftHead̂ {_ ∷ _ } | _ ∷ _ = refl
proofTogglê : ⟦ togglê ⟧ω̂ (repeat tt) ≈ iterate not 𝕋
proofTogglê = map-cong ⇑ proofToggle ⟨ transₛ ⟩ symₛ map-compose ⟨ transₛ ⟩ map-id
proofReĝAlwaysLoad : ∀ {xs} → ⟦ reĝ ⟧ω̂ (zipWith _,_ xs (repeat 𝕋)) ≈ xs
proofReĝAlwaysLoad {xs} = liftProof {p = id} {α̂ = ⇕Bool²} {β̂ = ⇕Bool} {f = reg} {xs = zipWith _,_ xs (repeat 𝕋)}
(λ {_} {_} {f} {s} → ssym (id-swap {f = map f} {s = s}))
(λ x → refl)
proofReĝNeverLoad : ∀ {xs} → ⟦ reĝ ⟧ω̂ (zipWith P._,_ xs (repeat 𝔽)) ≈ repeat 𝔽
proofReĝNeverLoad {xs} = liftProof {p = id} {α̂ = ⇕Bool²} {β̂ = ⇕Bool} {f = reg} {xs = zipWith P._,_ xs (repeat 𝔽)}
(λ {_} {_} {f} {s} → ssym (id-swap {f = map f} {s = s}))
(λ x → refl)
(proofRegNeverLoad {xs = xs})
\begin{code}
module PiWare.ProofSamples.RegN' where
open import Function using (_$_; _∘′_; id; flip)
open import Coinduction using (♯_)
open import Data.CausalStream using (runᶜ′)
open import Data.Stream using (Stream; _∷_; zipWith; repeat; _≈_; map; zipWith-cong)
open import Data.Stream.Equality.WithTrans using (_≈ₚ_; _∷ₚ_; ≈ₚ-to-≈; ≈-to-≈ₚ; reflₚ; transₚ)
open import Data.Stream.Properties using (module EqReasoningₛ; module Setoidₛ; map-repeat; map-compose; map-cong-fun; map-id)
open EqReasoningₛ using (_≈⟨_⟩_) renaming (begin_ to beginₛ_; _∎ to _∎ₛ)
open Setoidₛ using () renaming (refl to reflₛ; sym to symₛ; trans to transₛ)
open import Relation.Binary.PropositionalEquality using (_≡_; _≗_; refl; cong; sym; trans; module ≡-Reasoning)
open ≡-Reasoning using (begin_; _≡⟨_⟩_; _∎)
open import Data.Bool.Base using (Bool; false; true)
open import Data.Fin using () renaming (suc to Fs)
open import Data.List.NonEmpty using (_∷_)
open import Data.Nat.Base using (zero; suc)
open import Data.Product using (_,_; proj₁; proj₂)
open import Data.Vec using (Vec; []; _∷_; _++_; [_]; head; tabulate; lookup; splitAt; replicate)
open import Data.Vec.Extra using (splitAt′)
open import Data.Vec.Properties using (lookup∘tabulate; tabulate∘lookup)
open import Data.Vec.Properties.Extra using (tabulate-cong)
open import Data.Serializable using (_⇕_; ⇕⊤; ⇕×)
open import Data.Serializable.Bool using (⇕Bool)
open import PiWare.Circuit using (Plug; _⟫_; _∥_)
open import PiWare.Atomic.Bool using (Atomic-Bool)
open import PiWare.Semantics.Simulation Atomic-Bool using (module WithGates)
open import PiWare.Semantics.Simulation.BoolTrio using () renaming (spec to spec-B₃)
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 (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)
open import PiWare.Semantics.Simulation.Properties.SequentialSequencing Atomic-Bool using () renaming (proof to proofSeq)
\end{code}
\begin{code}
open _⇕_ ⇕Bool using () renaming (⇑ to ⇑¹; ⇓ to ⇓¹)
open _⇕_ (⇕× ⦃ ⇕Bool ⦄ ⦃ ⇕Bool ⦄) using () renaming (⇓ to ⇓²)
\end{code}
%<*lemma>
\AgdaTarget{lemma}
\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
\end{code}
%</lemma>
%<*proofReg-never-plain>
\AgdaTarget{proofReg-never-plain}
\begin{code}
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)))
≈⟨ proofReg-never {xs = map ⇑¹ xs} ⟩
map ⇓¹ (repeat false)
≈⟨ map-repeat ⟩
repeat [ false ] ∎ₛ
\end{code}
%</proofReg-never-plain>
%<*proofReg-always-plain>
\AgdaTarget{proofReg-always-plain}
\begin{code}
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)))
≈⟨ proofReg-always {xs = map ⇑¹ xs} ⟩
map ⇓¹ (map ⇑¹ xs)
≈⟨ symₛ map-compose ⟩
map (⇓¹ ∘′ ⇑¹) xs
≈⟨ map-cong-fun ⊥ ⟩
map id xs
≈⟨ map-id ⟩
xs ∎ₛ
where postulate ⊥ : _
\end{code}
%</proofReg-always-plain>
%<*lemma-plug''>
\AgdaTarget{lemma-plug''}
\begin{code}
lemma-plug'' : ∀ {a} {A : Set a} {n} {x1 x2} {xs : Vec A n} →
tabulate
(λ x → lookup
(lookup x (tabulate (λ i → Fs (Fs i))))
(x1 ∷ x2 ∷ xs))
≡ xs
lemma-plug''{x1 = x1} {x2} {xs} = begin
tabulate
(λ x → lookup
(lookup x (tabulate (λ i → Fs (Fs i))))
(x1 ∷ x2 ∷ xs))
≡⟨ tabulate-cong (λ x → cong (λ z → lookup z (x1 ∷ x2 ∷ xs)) (lookup∘tabulate (λ z → Fs (Fs z)) x)) ⟩
tabulate (flip lookup xs)
≡⟨ tabulate∘lookup xs ⟩
xs ∎
\end{code}
%</lemma-plug''>
%<*lemma-plug'>
\AgdaTarget{lemma-plug'}
\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ₚ)))
\end{code}
%</lemma-plug'>
%<*lemma-plug>
\AgdaTarget{lemma-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ₛ))
\end{code}
%</lemma-plug>
%<*lemmaRegN-never>
\AgdaTarget{lemmaRegN-never}
\begin{code}
lemmaRegN-never : ∀ {n} → zipWith _++_ (repeat [ false ]) (repeat (replicate false)) ≈ repeat (replicate {n = suc n} false)
lemmaRegN-never = refl ∷ ♯ lemmaRegN-never
\end{code}
%</lemmaRegN-never>
%<*proofRegN-never>
\AgdaTarget{proofRegN-never}
\begin{code}
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)
≈⟨ proofSeq {c = regn-plug {n}} {d = reg ∥ regn n} {ins = zipWith _∷_ (repeat false) xs} ⟩
⟦ reg ∥ regn n ⟧ω (⟦ regn-plug {n} ⟧ω (zipWith _∷_ (repeat false) xs))
≈⟨ ⟦⟧ω[_]-cong {c = reg ∥ regn n} spec-B₃ (lemma-plug {xs = xs}) ⟩
⟦ reg ∥ regn n ⟧ω (zipWith _++_ (zipWith _++_ (map (proj₁ ∘′ splitAt′ 1) xs) (repeat [ false ])) (zipWith _∷_ (repeat false) (map (proj₂ ∘′ splitAt′ 1) xs)))
≈⟨ 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 _++_ (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))
≈⟨ lemmaRegN-never {n = n} ⟩
repeat (replicate false) ∎ₛ
\end{code}
%</proofRegN-never>
%<*lemma-repeat-empty>
\AgdaTarget{lemma-repeat-empty}
\begin{code}
lemma-repeat-empty : ∀ {A} {xs : Stream (Vec A 0)} → repeat [] ≈ xs
lemma-repeat-empty {xs = [] ∷ xs} = refl ∷ (♯ lemma-repeat-empty)
\end{code}
%</lemma-repeat-empty>
%<*lemmaRegN-always>
\AgdaTarget{lemmaRegN-always}
\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
\end{code}
%</lemmaRegN-always>
%<*proofRegN-always>
\AgdaTarget{proofRegN-always}
\begin{code}
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)
≈⟨ proofSeq {c = regn-plug {n}} {d = reg ∥ regn n} {ins = zipWith _∷_ (repeat true) xs} ⟩
⟦ reg ∥ regn n ⟧ω (⟦ regn-plug {n} ⟧ω (zipWith _∷_ (repeat true) xs))
≈⟨ ⟦⟧ω[_]-cong {c = reg ∥ regn n} spec-B₃ (lemma-plug {xs = xs}) ⟩
⟦ reg ∥ regn n ⟧ω (zipWith _++_ (zipWith _++_ (map (proj₁ ∘′ splitAt′ 1) xs) (repeat [ true ])) (zipWith _∷_ (repeat true) (map (proj₂ ∘′ splitAt′ 1) xs)))
≈⟨ 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 _++_ (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 ⟩
xs ∎ₛ
\end{code}
%</proofRegN-always>
\begin{code}
module PiWare.ProofSamples.RegN where
open import Function using (_$_; _∘′_; id)
open import Coinduction using (♯_)
open import Data.Bool.Base using (Bool) renaming (false to 𝔽; true to 𝕋)
open import Data.Nat.Base using (_+_; suc; _+⋎_; zero; _*_)
open import Data.Nat.Properties using () renaming (isCommutativeSemiring to ℕ-isCommSemiring)
open import Algebra.Structures using (module IsCommutativeSemiring; module IsCommutativeMonoid)
open IsCommutativeSemiring ℕ-isCommSemiring using (*-isCommutativeMonoid)
open IsCommutativeMonoid *-isCommutativeMonoid using () renaming (identity to *-id)
open import Data.Product using (_,_; proj₁; proj₂)
open import Data.Vec using ([]; _∷_; [_]; _++_; head; Vec; _⋎_; replicate; splitAt)
open import Data.Vec.Extra using (splitAt′)
open import Data.Vec.Properties.Extra using (singleton∘head)
open import Data.Stream using (zipWith; repeat; _≈_; map; _∷_; Stream; zipWith-cong)
open import Relation.Binary.PropositionalEquality using (_≡_; _≗_; refl; sym; cong; module ≡-Reasoning)
open ≡-Reasoning using (begin_; _≡⟨_⟩_; _≡⟨⟩_; _∎)
open import Data.Stream.Properties using (module Setoidₛ; module EqReasoningₛ; map-compose; map-cong-fun; map-id; map-repeat)
open Setoidₛ using () renaming (sym to symₛ; trans to transₛ)
open EqReasoningₛ using (_≈⟨_⟩_) renaming (begin_ to beginₛ_; _∎ to _∎ₛ)
open import PiWare.Circuit using (Plug; _⟫_; _∥_)
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.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 (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)
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)
open import PiWare.Semantics.Simulation.Properties.SequentialSequencing Atomic-Bool using () renaming (proof to proofSeq)
open import Data.Serializable using (_⇕_; ⇕×)
open import Data.Serializable.Bool using (⇕Bool)
\end{code}
\begin{code}
open _⇕_ ⇕Bool using (⇑; ⇓)
open _⇕_ (⇕× ⦃ ⇕Bool ⦄ ⦃ ⇕Bool ⦄) using () renaming (⇓ to ⇓²)
\end{code}
%<*p₁∘split1>
\AgdaTarget{p₁∘split1}
\begin{code}
p₁∘split1 : ∀ {n ℓ} {α : Set ℓ} → Vec α (1 + n) → Vec α 1
p₁∘split1 = proj₁ ∘′ splitAt′ 1
\end{code}
%</p₁∘split1>
%<*p₂∘split1>
\AgdaTarget{p₂∘split1}
\begin{code}
p₂∘split1 : ∀ {n ℓ} {α : Set ℓ} → Vec α (1 + n) → Vec α n
p₂∘split1 = proj₂ ∘′ splitAt′ 1
\end{code}
%</p₂∘split1>
%<*vc*>
\AgdaTarget{vc*}
\begin{code}
vc* : ∀ {ℓ} {α : Set ℓ} n → Vec α n → Vec α (n * 1)
vc* n = vecCoerce $ sym ((proj₂ *-id) n)
\end{code}
%</vc*>
%<*vc⋎>
\AgdaTarget{vc⋎}
\begin{code}
vc⋎ : ∀ {ℓ} {α : Set ℓ} n → Vec α (n +⋎ n) → Vec α (n * 2)
vc⋎ n = vecCoerce (+⋎-*2 n)
\end{code}
%</vc⋎>
-- TODO: for any serializable data
%<*zipWith-++-⇑>
\AgdaTarget{zipWith-++-⇑}
\begin{code}
zipWith-++-⇑ : ∀ {xs y} → zipWith _++_ xs (repeat [ y ]) ≈ map ⇓² (zipWith _,_ (map ⇑ xs) (repeat y))
zipWith-++-⇑ {x ∷ _} {y} = reduce x ∷ ♯ zipWith-++-⇑
where reduce : ∀ z → z ++ (y ∷ []) ≡ head z ∷ y ∷ []
reduce (_ ∷ []) = refl
\end{code}
%</zipWith-++-⇑>
%<*proofReg-never-plain>
\AgdaTarget{proofReg-never-plain}
\begin{code}
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 𝔽))) ≈⟨ proofReg-never {xs = map ⇑ xs} ⟩
map ⇓ (repeat 𝔽) ≈⟨ map-repeat ⟩
repeat [ 𝔽 ] ∎ₛ
\end{code}
%</proofReg-never-plain>
%<*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₃ (zipWith-++-⇑ {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}
%</proofReg-always-plain
%<*⋎-replicate>
\AgdaTarget{⋎-replicate}