Uniformized Sim*/Properties/Seq* in order to be unified

parent ba5f364a
......@@ -27,11 +27,11 @@ open import PiWare.Circuit using (ℂ; C; Plug; _⟫_; _∥_)
open import PiWare.Plugs using (nil⤨)
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)
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 PiWare.Semantics.Simulation.BoolTrio using () renaming (spec to b₃)
open WithGates b₃ using (⟦_⟧ω; ⟦_⟧ᶜ; ⟦_⟧)
open import PiWare.Semantics.Simulation.Properties.SequentialCongruence Atomic-Bool using (⟦⟧ω[]-cong)
open import PiWare.Semantics.Simulation.Properties.SequentialParalleling Atomic-Bool using (⟦⟧ω[–]-∥⇒zipWith++)
open import PiWare.Semantics.Simulation.Properties.SequentialSequencing Atomic-Bool using (⟦⟧ω[–]-⟫⇒∘)
open import PiWare.Samples.BoolTrioSeq using (reg; proofReg-never; proofReg-always)
open import Data.Serializable using (_⇕_; ⇕×)
......@@ -83,7 +83,7 @@ map⇓²-zip-map⇑¹-repeat {x ∷ _} {y} = append-headCons x ∷ ♯ map⇓²-
proofReg-never-plain : ∀ {xs} → ⟦ reg ⟧ω (zipWith _++_ xs (repeat [ 𝔽 ])) ≈ repeat [ 𝔽 ]
proofReg-never-plain {xs} = beginₛ
⟦ reg ⟧ω (zipWith _++_ xs (repeat [ 𝔽 ]))
≈⟨ ⟦⟧ω[_]-cong {c = reg} spec-B₃ (map⇓²-zip-map⇑¹-repeat {xs = xs}) ⟩
≈⟨ ⟦⟧ω[–]-cong b₃ reg (map⇓²-zip-map⇑¹-repeat {xs = xs}) ⟩
⟦ reg ⟧ω (map ⇓² (zipWith _,_ (map ⇑¹ xs) (repeat 𝔽)))
≈⟨ proofReg-never {xs = map ⇑¹ xs} ⟩
map ⇓¹ (repeat 𝔽)
......@@ -109,7 +109,7 @@ head∘[x]-involutive-Vec1 (x ∷ []) = refl
proofReg-always-plain : ∀ {xs} → ⟦ reg ⟧ω (zipWith _++_ xs (repeat [ 𝕋 ])) ≈ xs
proofReg-always-plain {xs} = beginₛ
⟦ reg ⟧ω (zipWith _++_ xs (repeat [ 𝕋 ]))
≈⟨ ⟦⟧ω[_]-cong {c = reg} spec-B₃ (map⇓²-zip-map⇑¹-repeat {xs = xs}) ⟩
≈⟨ ⟦⟧ω[–]-cong b₃ reg (map⇓²-zip-map⇑¹-repeat {xs = xs}) ⟩
⟦ reg ⟧ω (map ⇓² (zipWith _,_ (map ⇑¹ xs) (repeat 𝕋)))
≈⟨ proofReg-always {xs = map ⇑¹ xs} ⟩
map ⇓¹ (map ⇑¹ xs)
......@@ -181,12 +181,11 @@ proofRegN-never {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} ⟩
≈⟨ ⟦⟧ω[–]-⟫⇒∘ b₃ (regn-plug {n}) (reg ∥ regn n) {zipWith _∷_ (repeat 𝔽) xs} ⟩
⟦ reg ∥ regn n ⟧ω (⟦ regn-plug {n} ⟧ω (zipWith _∷_ (repeat 𝔽) xs))
≈⟨ ⟦⟧ω[_]-cong {c = reg ∥ regn n} spec-B₃ (regn-plug-ω {xs = xs}) ⟩
≈⟨ ⟦⟧ω[–]-cong b₃ (reg ∥ regn n) (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}
{(zipWith _++_ (map (proj₁ ∘′ splitAt′ 1) xs) (repeat [ 𝔽 ]))} {zipWith _∷_ (repeat 𝔽) (map (proj₂ ∘′ splitAt′ 1) xs)} ⟩
≈⟨ ⟦⟧ω[–]-∥⇒zipWith++ b₃ reg (regn n) {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 {map (proj₁ ∘′ splitAt′ 1) xs}) (proofRegN-never {n} {map (proj₂ ∘′ splitAt′ 1) xs}) ⟩
zipWith _++_ (repeat [ 𝔽 ]) (repeat (replicate 𝔽))
......@@ -224,12 +223,11 @@ 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} ⟩
≈⟨ ⟦⟧ω[–]-⟫⇒∘ b₃ (regn-plug {n}) (reg ∥ regn n) {zipWith _∷_ (repeat 𝕋) xs} ⟩
⟦ reg ∥ regn n ⟧ω (⟦ regn-plug {n} ⟧ω (zipWith _∷_ (repeat 𝕋) xs))
≈⟨ ⟦⟧ω[_]-cong {c = reg ∥ regn n} spec-B₃ (regn-plug-ω {xs = xs}) ⟩
≈⟨ ⟦⟧ω[–]-cong b₃ (reg ∥ regn n) (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++ b₃ reg (regn n) {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-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)
......
......@@ -24,14 +24,14 @@ open ≡-Reasoning using (begin_; _≡⟨_⟩_; _∎)
open import PiWare.Circuit using (Plug; _⟫_; _∥_)
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.Simulation.BoolTrio using () renaming (spec to b₃)
open WithGates b₃ using (⟦_⟧ᶜ; ⟦_⟧ω)
open import PiWare.Samples.BoolTrioSeq using (reg)
open import PiWare.Samples.RegN' using (regn-plug; regn)
open import PiWare.Samples.RegProperties using (regW,R-I⇒O; regR,R-I⇒O)
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 PiWare.Semantics.Simulation.Properties.SequentialCongruence Atomic-Bool using (⟦⟧ω[]-cong)
open import PiWare.Semantics.Simulation.Properties.SequentialParalleling Atomic-Bool using (⟦⟧ω[–]-∥⇒zipWith++)
open import PiWare.Semantics.Simulation.Properties.SequentialSequencing Atomic-Bool using (⟦⟧ω[–]-⟫⇒∘)
lemma-deconstruct-split : ∀ {α n d} {y z : α} {ys zs : Vec α n} {xs}
......@@ -119,16 +119,16 @@ proofNWriteRead {suc n} {d} {wh ∷ wt} {c1h ∷ c1t} {ins} p with lemma-deconst
proofNWriteRead {suc n} {d} {wh ∷ wt} {c1h ∷ c1t} {ins} p | pls , pvs with lemma-deconstruct-split {n = n} {d} {wh} {c1h} {wt} {c1t} pvs
proofNWriteRead {suc n} {d} {wh ∷ wt} {c1h ∷ c1t} {ins} p | pls , pvs | pvhs , pvts = begin
take 2 (drop d (⟦ regn (suc n) ⟧ω ins))
≡⟨ take-cong (drop-cong {n = d} (⟦⟧ω[_]-cong {c = regn (suc n)} spec-B₃ {xs = ins} (symₛ (lemma-merge-head-tail {n = suc n})))) ⟩
≡⟨ take-cong (drop-cong {n = d} (⟦⟧ω[–]-cong b₃ (regn (suc n)) {xs = ins} (symₛ (lemma-merge-head-tail {n = suc n})))) ⟩
take 2 (drop d (⟦ regn (suc n) ⟧ω (zipWith _∷_ (map head ins) (map tail ins))))
≡⟨ take-cong (drop-cong {n = d} (proofSeq {c = regn-plug} {d = reg ∥ regn n} {ins = zipWith _∷_ (map head ins) (map tail ins)})) ⟩
≡⟨ take-cong (drop-cong {n = d} (⟦⟧ω[–]-⟫⇒∘ b₃ regn-plug (reg ∥ regn n) {zipWith _∷_ (map head ins) (map tail ins)})) ⟩
take 2 (drop d (⟦ reg ∥ regn n ⟧ω (⟦ regn-plug ⟧ω (zipWith _∷_ (map head ins) (map tail ins)))))
≡⟨ take-cong (drop-cong {n = d} (⟦⟧ω[_]-cong {c = reg ∥ regn n} spec-B₃ (lemma-plug {ls = map head ins} {xs = map tail ins}))) ⟩
≡⟨ take-cong (drop-cong {n = d} (⟦⟧ω[–]-cong b₃ (reg ∥ regn n) (lemma-plug {ls = map head ins} {xs = map tail ins}))) ⟩
take 2 (drop d (⟦ reg ∥ regn n ⟧ω (zipWith _++_ (zipWith _∷ʳ_ (map ₁∘split1′ (map tail ins)) (map head ins))
(zipWith _∷_ (map head ins) (map ₂∘split1′ (map tail ins))))))
≡⟨ take-cong (drop-cong {n = d} (proofPar {c = reg} {d = regn n}
{ins₁ = zipWith _∷ʳ_ (map ₁∘split1′ (map tail ins)) (map head ins)}
{ins₂ = zipWith _∷_ (map head ins) (map ₂∘split1′ (map tail ins))})) ⟩
≡⟨ take-cong (drop-cong {n = d} (⟦⟧ω[–]-∥⇒zipWith++ b₃ reg (regn n)
{zipWith _∷ʳ_ (map ₁∘split1′ (map tail ins)) (map head ins)}
{zipWith _∷_ (map head ins) (map ₂∘split1′ (map tail ins))})) ⟩
take 2 (drop d (zipWith _++_ (⟦ reg ⟧ω (zipWith _∷ʳ_ (map ₁∘split1′ (map tail ins)) (map head ins)))
(⟦ regn n ⟧ω (zipWith _∷_ (map head ins) (map ₂∘split1′ (map tail ins))))))
≡⟨ take-cong (lemma-drop-zipWith {d = d}) ⟩
......@@ -153,17 +153,17 @@ lemma-unfold-regn' {n} {ins} = beginₛ
⟦ regn (suc n) ⟧ω ins
≈⟨ reflₛ ⟩
⟦ regn-plug ⟫ (reg ∥ regn n) ⟧ω ins
≈⟨ proofSeq {c = regn-plug} {d = reg ∥ regn n} {ins = ins} ⟩
≈⟨ ⟦⟧ω[–]-⟫⇒∘ b₃ regn-plug (reg ∥ regn n) {ins} ⟩
⟦ reg ∥ regn n ⟧ω (⟦ regn-plug ⟧ω ins)
≈⟨ ⟦⟧ω[_]-cong {c = reg ∥ regn n} spec-B₃ (⟦⟧ω[_]-cong {c = regn-plug} spec-B₃ {xs = ins} (symₛ lemma-merge-head-tail)) ⟩
≈⟨ ⟦⟧ω[–]-cong b₃ (reg ∥ regn n) (⟦⟧ω[–]-cong b₃ regn-plug {xs = ins} (symₛ lemma-merge-head-tail)) ⟩
⟦ reg ∥ regn n ⟧ω (⟦ regn-plug ⟧ω (zipWith _∷_ (map head ins) (map tail ins)))
≈⟨ ⟦⟧ω[_]-cong {c = reg ∥ regn n} spec-B₃ (lemma-plug {ls = map head ins} {xs = map tail ins}) ⟩
≈⟨ ⟦⟧ω[–]-cong b₃ (reg ∥ regn n) (lemma-plug {ls = map head ins} {xs = map tail ins}) ⟩
⟦ reg ∥ regn n ⟧ω (zipWith _++_
(zipWith _∷ʳ_ (map ₁∘split1′ (map tail ins)) (map head ins))
(zipWith _∷_ (map head ins) (map ₂∘split1′ (map tail ins))))
≈⟨ proofPar {c = reg} {d = regn n}
{ins₁ = zipWith _∷ʳ_ (map ₁∘split1′ (map tail ins)) (map head ins)}
{ins₂ = zipWith _∷_ (map head ins) (map ₂∘split1′ (map tail ins))} ⟩
≈⟨ ⟦⟧ω[–]-∥⇒zipWith++ b₃ reg (regn n)
{zipWith _∷ʳ_ (map ₁∘split1′ (map tail ins)) (map head ins)}
{zipWith _∷_ (map head ins) (map ₂∘split1′ (map tail ins))} ⟩
zipWith _++_
(⟦ reg ⟧ω (zipWith _∷ʳ_ (map ₁∘split1′ (map tail ins)) (map head ins)))
(⟦ regn n ⟧ω (zipWith _∷_ (map head ins) (map ₂∘split1′ (map tail ins)))) ∎ₛ
......@@ -207,16 +207,16 @@ proofNReadRead {suc n} {d} {wh ∷ wt} {c1h ∷ c1t} {c2h ∷ c2t} {ins} pp ph |
proofNReadRead {suc n} {d} {wh ∷ wt} {c1h ∷ c1t} {c2h ∷ c2t} {ins} pp ph | pls , pvs | pvhs , pvts with lemma-unfold-regn {n = n} {d} {ins = ins} ph
proofNReadRead {suc n} {d} {wh ∷ wt} {c1h ∷ c1t} {c2h ∷ c2t} {ins} pp ph | pls , pvs | pvhs , pvts | phhs , phts = begin
take 2 (drop d (⟦ regn (suc n) ⟧ω ins))
≡⟨ take-cong (drop-cong {n = d} (⟦⟧ω[_]-cong {c = regn (suc n)} spec-B₃ {xs = ins} (symₛ (lemma-merge-head-tail {n = suc n})))) ⟩
≡⟨ take-cong (drop-cong {n = d} (⟦⟧ω[–]-cong b₃ (regn (suc n)) {xs = ins} (symₛ (lemma-merge-head-tail {n = suc n})))) ⟩
take 2 (drop d (⟦ regn (suc n) ⟧ω (zipWith _∷_ (map head ins) (map tail ins))))
≡⟨ take-cong (drop-cong {n = d} (proofSeq {c = regn-plug} {d = reg ∥ regn n} {ins = zipWith _∷_ (map head ins) (map tail ins)})) ⟩
≡⟨ take-cong (drop-cong {n = d} (⟦⟧ω[–]-⟫⇒∘ b₃ regn-plug (reg ∥ regn n) {zipWith _∷_ (map head ins) (map tail ins)})) ⟩
take 2 (drop d (⟦ reg ∥ regn n ⟧ω (⟦ regn-plug ⟧ω (zipWith _∷_ (map head ins) (map tail ins)))))
≡⟨ take-cong (drop-cong {n = d} (⟦⟧ω[_]-cong {c = reg ∥ regn n} spec-B₃ (lemma-plug {ls = map head ins} {xs = map tail ins}))) ⟩
≡⟨ take-cong (drop-cong {n = d} (⟦⟧ω[–]-cong b₃ (reg ∥ regn n) (lemma-plug {ls = map head ins} {xs = map tail ins}))) ⟩
take 2 (drop d (⟦ reg ∥ regn n ⟧ω (zipWith _++_ (zipWith _∷ʳ_ (map ₁∘split1′ (map tail ins)) (map head ins))
(zipWith _∷_ (map head ins) (map ₂∘split1′ (map tail ins))))))
≡⟨ take-cong (drop-cong {n = d} (proofPar {c = reg} {d = regn n}
{ins₁ = zipWith _∷ʳ_ (map ₁∘split1′ (map tail ins)) (map head ins)}
{ins₂ = zipWith _∷_ (map head ins) (map ₂∘split1′ (map tail ins))})) ⟩
≡⟨ take-cong (drop-cong {n = d} (⟦⟧ω[–]-∥⇒zipWith++ b₃ reg (regn n)
{zipWith _∷ʳ_ (map ₁∘split1′ (map tail ins)) (map head ins)}
{zipWith _∷_ (map head ins) (map ₂∘split1′ (map tail ins))})) ⟩
take 2 (drop d (zipWith _++_
(⟦ reg ⟧ω (zipWith _∷ʳ_ (map ₁∘split1′ (map tail ins)) (map head ins)))
(⟦ regn n ⟧ω (zipWith _∷_ (map head ins) (map ₂∘split1′ (map tail ins))))))
......
This diff is collapsed.
......@@ -3,25 +3,40 @@ open import PiWare.Atomic using (Atomic)
module PiWare.Semantics.Simulation.Properties.SequentialCongruence (A : Atomic) where
open import Coinduction
open import Data.Stream
open import Coinduction using (♯_; ♭)
open import Data.Stream using (_∷_; _≈_)
open import Data.List.NonEmpty using (_∷_)
open import Relation.Binary.PropositionalEquality using (_≡_; _≗_; refl; sym; trans)
import Relation.Binary.PropositionalEquality as P
import Data.List.NonEmpty as NL
open import Data.CausalStream using (runᶜ′; runᶜ)
open import Data.CausalStream using (_⇒ᶜ_; runᶜ′; runᶜ)
open import PiWare.Circuit using (ℂ)
open import PiWare.Circuit.Algebra using (TyGate)
open import PiWare.Semantics.Simulation A using (W⟶W; ⟦_⟧ω[_])
\end{code}
runᶜ′-cong : ∀ {A B} {f : NL.List⁺ A → B} {cs} {xs ys} → xs ≈ ys → runᶜ′ f cs xs ≈ runᶜ′ f cs ys
runᶜ′-cong {f = f} {xs = x ∷ xs} {.x ∷ ys} (refl ∷ xs≈) = refl ∷ (♯ runᶜ′-cong {f = f} (♭ xs≈))
runᶜ-cong : ∀ {A B} {f : NL.List⁺ A → B} {xs ys} → xs ≈ ys → runᶜ f xs ≈ runᶜ f ys
runᶜ-cong {f = f} {xs = x ∷ xs} {.x ∷ ys} (refl ∷ xs≈) = runᶜ′-cong (♭ xs≈)
%<*runᶜ′-cong>
\AgdaTarget{runᶜ′-cong}
\begin{code}
runᶜ′-cong : ∀ {α β} {f : α ⇒ᶜ β} {x⁰⁻ x⁺ y⁺} → x⁺ ≈ y⁺ → (runᶜ′ f x⁰⁻) x⁺ ≈ (runᶜ′ f x⁰⁻) y⁺
runᶜ′-cong {f = f} {x⁺ = x¹ ∷ _} {.x¹ ∷ _} (refl ∷ x²⁺≈y²⁺) = refl ∷ ♯ runᶜ′-cong {f = f} (♭ x²⁺≈y²⁺)
\end{code}
%</runᶜ′-cong>
⟦⟧ω[_]-cong : ∀ {i o G} {c : ℂ G i o} (g : TyGate G W⟶W) {xs ys} → xs ≈ ys → ⟦ c ⟧ω[ g ] xs ≈ ⟦ c ⟧ω[ g ] ys
⟦⟧ω[ g ]-cong xs≈ys = runᶜ-cong xs≈ys
%<*runᶜ-cong>
\AgdaTarget{runᶜ-cong}
\begin{code}
runᶜ-cong : ∀ {α β} {f : α ⇒ᶜ β} {xs ys} → xs ≈ ys → (runᶜ f) xs ≈ (runᶜ f) ys
runᶜ-cong {f = f} {xs = x ∷ _} {.x ∷ _} (refl ∷ xs′≈ys′) = runᶜ′-cong (♭ xs′≈ys′)
\end{code}
%</runᶜ-cong>
%<*⟦⟧ω[–]-cong>
\AgdaTarget{⟦⟧ω[–]-cong}
\begin{code}
⟦⟧ω[–]-cong : ∀ {i o G} (g : TyGate G W⟶W) (c : ℂ G i o) {xs ys} → xs ≈ ys → ⟦ c ⟧ω[ g ] xs ≈ ⟦ c ⟧ω[ g ] ys
⟦⟧ω[–]-cong _ _ xs≈ys = runᶜ-cong xs≈ys
\end{code}
%</⟦⟧ω[–]-cong>
......@@ -14,54 +14,60 @@ open import Data.Vec using (_++_)
open import Data.Vec.Extra using (splitAt′)
open import Data.Vec.Properties.Extra using (splitAt′-++-inverse)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; cong; module ≡-Reasoning)
open ≡-Reasoning using (begin_; _≡⟨_⟩_; _≡⟨⟩_; _∎)
open import Data.Stream using (_∷_; zipWith; _≈_)
open import Data.Stream.Properties using (module Setoidₛ)
open import Data.Stream.Properties.Extra using (map⁺-compose; map⁺-id; map⁺-cong)
open import Data.CausalStream using (runᶜ′)
open ≡-Reasoning using (begin_; _≡⟨_⟩_; _∎)
open import Data.CausalStream using (runᶜ′)
open import PiWare.Circuit using (ℂ; _∥_)
open import PiWare.Circuit.Algebra using (TyGate)
open import PiWare.Semantics.Simulation A using (W⟶W; ⟦_⟧ω[_]; ⟦_⟧ᶜ[_]; ⟦_⟧[_])
\end{code}
open import Relation.Binary using (Setoid)
import Relation.Binary.EqReasoning
private
open module StreamSetoid {A} = Setoid (Data.Stream.setoid A) using ()
renaming (refl to srefl; sym to ssym; trans to strans)
module StreamEqReasoning {A} = Relation.Binary.EqReasoning (Data.Stream.setoid A)
lemma-⟦⟧ᶜ : ∀ {i₁ i₂ o₁ o₂ G} {g : TyGate G W⟶W} {c : ℂ G i₁ o₁} {d : ℂ G i₂ o₂} {cs₁ cs₂} →
length cs₁ ≡ length cs₂ →
⟦ c ∥ d ⟧ᶜ[ g ] (zipWith⁺ _++_ cs₁ cs₂) ≡ ⟦ c ⟧ᶜ[ g ] cs₁ ++ ⟦ d ⟧ᶜ[ g ] cs₂
lemma-⟦⟧ᶜ {g = g} {c} {d} {cs₁} {cs₂} p = begin
⟦ c ∥ d ⟧ᶜ[ g ] (zipWith⁺ _++_ cs₁ cs₂)
≡⟨ refl ⟩
(uncurry′ _++_ ∘′ map ⟦ c ⟧ᶜ[ g ] ⟦ d ⟧ᶜ[ g ] ∘′ unzip⁺ ∘′ splitAt⁺ _) (zipWith⁺ _++_ cs₁ cs₂)
≡⟨ cong (uncurry′ _++_ ∘′ map ⟦ c ⟧ᶜ[ g ] ⟦ d ⟧ᶜ[ g ] ∘′ unzip⁺ ∘′ splitAt⁺ _) (zipWith⁺-map⁺-zip⁺ {xs = cs₁} {ys = cs₂} ) ⟩
(uncurry′ _++_ ∘′ map ⟦ c ⟧ᶜ[ g ] ⟦ d ⟧ᶜ[ g ] ∘′ unzip⁺ ∘′ map⁺ (splitAt′ _) ∘′ map⁺ (uncurry′ _++_)) (zip⁺ cs₁ cs₂)
≡⟨ cong (uncurry′ _++_ ∘′ map ⟦ c ⟧ᶜ[ g ] ⟦ d ⟧ᶜ[ g ] ∘′ unzip⁺) (sym (map⁺-compose (zip⁺ cs₁ cs₂))) ⟩
(uncurry′ _++_ ∘′ map ⟦ c ⟧ᶜ[ g ] ⟦ d ⟧ᶜ[ g ] ∘′ unzip⁺ ∘′ map⁺ (splitAt′ _ ∘′ uncurry′ _++_)) (zip⁺ cs₁ cs₂)
≡⟨ cong (uncurry′ _++_ ∘′ map ⟦ c ⟧ᶜ[ g ] ⟦ d ⟧ᶜ[ g ] ∘′ unzip⁺) (map⁺-cong (λ x → splitAt′-++-inverse) (zip⁺ cs₁ cs₂)) ⟩
(uncurry′ _++_ ∘′ map ⟦ c ⟧ᶜ[ g ] ⟦ d ⟧ᶜ[ g ] ∘′ unzip⁺ ∘′ map⁺ id) (zip⁺ cs₁ cs₂)
≡⟨ cong (uncurry′ _++_ ∘′ map ⟦ c ⟧ᶜ[ g ] ⟦ d ⟧ᶜ[ g ] ∘′ unzip⁺) (map⁺-id (zip⁺ cs₁ cs₂)) ⟩
(uncurry′ _++_ ∘′ map ⟦ c ⟧ᶜ[ g ] ⟦ d ⟧ᶜ[ g ]) (unzip⁺ (zip⁺ cs₁ cs₂))
%<*⟦⟧ᶜ-∥⇒zipWith++>
\AgdaTarget{⟦⟧ᶜ-∥⇒zipWith++}
\begin{code}
⟦⟧ᶜ-∥⇒zipWith++ : ∀ {i₁ i₂ o₁ o₂ G} (g : TyGate G W⟶W) (c : ℂ G i₁ o₁) (d : ℂ G i₂ o₂) {x⁰⁻ y⁰⁻}
→ length x⁰⁻ ≡ length y⁰⁻ → ⟦ c ∥ d ⟧ᶜ[ g ] (zipWith⁺ _++_ x⁰⁻ y⁰⁻) ≡ ⟦ c ⟧ᶜ[ g ] x⁰⁻ ++ ⟦ d ⟧ᶜ[ g ] y⁰⁻
⟦⟧ᶜ-∥⇒zipWith++ g c d {x⁰⁻} {y⁰⁻} p = begin
⟦ c ∥ d ⟧ᶜ[ g ] (zipWith⁺ _++_ x⁰⁻ y⁰⁻)
≡⟨⟩
(uncurry′ _++_ ∘′ map ⟦ c ⟧ᶜ[ g ] ⟦ d ⟧ᶜ[ g ] ∘′ unzip⁺ ∘′ splitAt⁺ _) (zipWith⁺ _++_ x⁰⁻ y⁰⁻)
≡⟨ cong (uncurry′ _++_ ∘′ map ⟦ c ⟧ᶜ[ g ] ⟦ d ⟧ᶜ[ g ] ∘′ unzip⁺ ∘′ splitAt⁺ _) (zipWith⁺-map⁺-zip⁺ {xs = x⁰⁻} {ys = y⁰⁻} ) ⟩
(uncurry′ _++_ ∘′ map ⟦ c ⟧ᶜ[ g ] ⟦ d ⟧ᶜ[ g ] ∘′ unzip⁺ ∘′ map⁺ (splitAt′ _) ∘′ map⁺ (uncurry′ _++_)) (zip⁺ x⁰⁻ y⁰⁻)
≡⟨ cong (uncurry′ _++_ ∘′ map ⟦ c ⟧ᶜ[ g ] ⟦ d ⟧ᶜ[ g ] ∘′ unzip⁺) (sym (map⁺-compose (zip⁺ x⁰⁻ y⁰⁻))) ⟩
(uncurry′ _++_ ∘′ map ⟦ c ⟧ᶜ[ g ] ⟦ d ⟧ᶜ[ g ] ∘′ unzip⁺ ∘′ map⁺ (splitAt′ _ ∘′ uncurry′ _++_)) (zip⁺ x⁰⁻ y⁰⁻)
≡⟨ cong (uncurry′ _++_ ∘′ map ⟦ c ⟧ᶜ[ g ] ⟦ d ⟧ᶜ[ g ] ∘′ unzip⁺) (map⁺-cong (λ x → splitAt′-++-inverse) (zip⁺ x⁰⁻ y⁰⁻)) ⟩
(uncurry′ _++_ ∘′ map ⟦ c ⟧ᶜ[ g ] ⟦ d ⟧ᶜ[ g ] ∘′ unzip⁺ ∘′ map⁺ id) (zip⁺ x⁰⁻ y⁰⁻)
≡⟨ cong (uncurry′ _++_ ∘′ map ⟦ c ⟧ᶜ[ g ] ⟦ d ⟧ᶜ[ g ] ∘′ unzip⁺) (map⁺-id (zip⁺ x⁰⁻ y⁰⁻)) ⟩
(uncurry′ _++_ ∘′ map ⟦ c ⟧ᶜ[ g ] ⟦ d ⟧ᶜ[ g ]) (unzip⁺ (zip⁺ x⁰⁻ y⁰⁻))
≡⟨ cong (uncurry′ _++_ ∘′ map ⟦ c ⟧ᶜ[ g ] ⟦ d ⟧ᶜ[ g ]) (unzip⁺-zip⁺-inverse p) ⟩
(uncurry′ _++_ ∘′ map ⟦ c ⟧ᶜ[ g ] ⟦ d ⟧ᶜ[ g ]) (cs₁ , cs₂)
(uncurry′ _++_ ∘′ map ⟦ c ⟧ᶜ[ g ] ⟦ d ⟧ᶜ[ g ]) (x⁰⁻ , y⁰⁻)
≡⟨ refl ⟩
⟦ c ⟧ᶜ[ g ] cs₁ ++ ⟦ d ⟧ᶜ[ g ] cs₂ ∎
⟦ c ⟧ᶜ[ g ] x⁰⁻ ++ ⟦ d ⟧ᶜ[ g ] y⁰⁻ ∎
\end{code}
%</⟦⟧ᶜ-∥⇒zipWith++>
lemma-runᶜ′ : ∀ {i₁ i₂ o₁ o₂ G} {g : TyGate G W⟶W} {c : ℂ G i₁ o₁} {d : ℂ G i₂ o₂} {cs₁ cs₂} {ins₁ ins₂} →
length cs₁ ≡ length cs₂ →
runᶜ′ ⟦ c ∥ d ⟧ᶜ[ g ] (zipWith⁺ _++_ cs₁ cs₂) (zipWith _++_ ins₁ ins₂)
≈ zipWith _++_ (runᶜ′ ⟦ c ⟧ᶜ[ g ] cs₁ ins₁) (runᶜ′ ⟦ d ⟧ᶜ[ g ] cs₂ ins₂)
lemma-runᶜ′ {g = g} {c} {d} {c₁ ∷ cs₁} {c₂ ∷ cs₂} {i₁ ∷ is₁} {i₂ ∷ is₂} p =
lemma-⟦⟧ᶜ {g = g} {c} {d} p ∷ (♯ (lemma-runᶜ′ {g = g} {c} {d} (cong suc p)))
proof : ∀ {i₁ i₂ o₁ o₂ G} {g : TyGate G W⟶W} {c : ℂ G i₁ o₁} {d : ℂ G i₂ o₂} {ins₁ ins₂} →
⟦ c ∥ d ⟧ω[ g ] (zipWith _++_ ins₁ ins₂) ≈ zipWith _++_ (⟦ c ⟧ω[ g ] ins₁) (⟦ d ⟧ω[ g ] ins₂)
proof {g = g} {c} {d} {_ ∷ _} {_ ∷ _} = lemma-runᶜ′ {g = g} {c} {d} refl
%<*runᶜ′⟦⟧ᶜ-∥⇒zipWith++>
\AgdaTarget{runᶜ′⟦⟧ᶜ-∥⇒zipWith++}
\begin{code}
runᶜ′⟦⟧ᶜ-∥⇒zipWith++ : ∀ {i₁ i₂ o₁ o₂ G} (g : TyGate G W⟶W) (c : ℂ G i₁ o₁) (d : ℂ G i₂ o₂) {x⁰⁻ y⁰⁻ x⁺ y⁺}
→ length x⁰⁻ ≡ length y⁰⁻
→ runᶜ′ ⟦ c ∥ d ⟧ᶜ[ g ] (zipWith⁺ _++_ x⁰⁻ y⁰⁻) (zipWith _++_ x⁺ y⁺)
≈ zipWith _++_ (runᶜ′ ⟦ c ⟧ᶜ[ g ] x⁰⁻ x⁺) (runᶜ′ ⟦ d ⟧ᶜ[ g ] y⁰⁻ y⁺)
runᶜ′⟦⟧ᶜ-∥⇒zipWith++ g c d {_ ∷ _} {_ ∷ _} {_ ∷ _} {_ ∷ _} p = ⟦⟧ᶜ-∥⇒zipWith++ g c d p ∷ ♯ runᶜ′⟦⟧ᶜ-∥⇒zipWith++ g c d (cong suc p)
\end{code}
%</runᶜ′⟦⟧ᶜ-∥⇒zipWith++>
%<*⟦⟧ω[–]-∥⇒zipWith++>
\AgdaTarget{⟦⟧ω[–]-∥⇒zipWith++}
\begin{code}
⟦⟧ω[–]-∥⇒zipWith++ : ∀ {i₁ i₂ o₁ o₂ G} (g : TyGate G W⟶W) (c : ℂ G i₁ o₁) (d : ℂ G i₂ o₂) {xs ys}
→ ⟦ c ∥ d ⟧ω[ g ] (zipWith _++_ xs ys) ≈ zipWith _++_ (⟦ c ⟧ω[ g ] xs) (⟦ d ⟧ω[ g ] ys)
⟦⟧ω[–]-∥⇒zipWith++ g c d {_ ∷ _} {_ ∷ _} = runᶜ′⟦⟧ᶜ-∥⇒zipWith++ g c d refl
\end{code}
%</⟦⟧ω[–]-∥⇒zipWith++>
......@@ -6,7 +6,7 @@ module PiWare.Semantics.SimulationState.Properties.SequentialCongruence (A : Ato
open import Coinduction using (♯_; ♭)
open import Data.Stream using (Stream; _≈_; _∷_)
open import Data.Product using (_×_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
open import Relation.Binary.PropositionalEquality using (refl)
open import PiWare.Circuit using (ℂ)
open import PiWare.Circuit.Algebra using (TyGate)
......@@ -18,17 +18,16 @@ open import PiWare.Semantics.SimulationState A using (mealy; ⟦_⟧ω'[_])
%<*mealy-cong>
\AgdaTarget{mealy-cong}
\begin{code}
mealy-cong : ∀ {ℓ} {𝕊 : Set ℓ} {α β} {f : 𝕊 → α → (𝕊 × β)} {s : 𝕊} {xs ys : Stream α}
→ xs ≈ ys → mealy f s xs ≈ mealy f s ys
mealy-cong {xs = x ∷ xs} {.x ∷ ys} (refl ∷ xs≈ys) = refl ∷ ♯ (mealy-cong (♭ xs≈ys))
mealy-cong : ∀ {ℓ} {𝕊 : Set ℓ} {α β} {f : 𝕊 → α → (𝕊 × β)} {s xs ys} → xs ≈ ys → mealy f s xs ≈ mealy f s ys
mealy-cong {xs = x ∷ xs′} {.x ∷ ys′} (refl ∷ xs′≈ys′) = refl ∷ ♯ mealy-cong (♭ xs′≈ys′)
\end{code}
%</mealy-cong>
%<*⟦⟧ω'-cong>
\AgdaTarget{⟦⟧ω'-cong}
%<*⟦⟧ω'[–]-cong>
\AgdaTarget{⟦⟧ω'[–]-cong}
\begin{code}
⟦⟧ω'-cong : ∀ {i o s G} {g : TyGate G W⟶W} {c : ℂ G {s} i o} {xs ys} → xs ≈ ys → ⟦ c ⟧ω'[ g ] xs ≈ ⟦ c ⟧ω'[ g ] ys
⟦⟧ω'-cong = mealy-cong
⟦⟧ω'[–]-cong : ∀ {i o s G} (g : TyGate G W⟶W) (c : ℂ G {s} i o) {xs ys} → xs ≈ ys → ⟦ c ⟧ω'[ g ] xs ≈ ⟦ c ⟧ω'[ g ] ys
⟦⟧ω'[–]-cong _ _ = mealy-cong
\end{code}
%</⟦⟧ω'-cong>
%</⟦⟧ω'[–]-cong>
......@@ -12,41 +12,42 @@ open import Data.Product using (_,_; proj₁)
open import Data.Vec using (_++_)
open import Data.Vec.Properties.Extra using (,-injective; splitAt′-++-inverse)
open import PiWare.Circuit using (IsComb; σ; ω; ℂ; Gate; Plug; _⟫_; _∥_; DelayLoop)
open import PiWare.Circuit using (ℂ; _∥_)
open import PiWare.Circuit.Algebra using (TyGate)
open import PiWare.Semantics.Simulation A using (W⟶W)
open import PiWare.Semantics.SimulationState A using (⟦_⟧ₛ[_]; ⟦_⟧ω'[_]; mealy; _∥ₛ_)
\end{code}
%<*lemma∥ₚ>
\AgdaTarget{lemma∥ₚ}
%<*mealy⟦⟧ₛ[–]-∥⇒zipWith++ₚ>
\AgdaTarget{mealy⟦⟧ₛ[–]-∥⇒zipWith++ₚ}
\begin{code}
lemma∥ₚ : ∀ {i₁ i₂ o₁ o₂ s G} {g : TyGate G W⟶W} {c : ℂ G {s} i₁ o₁} {d : ℂ G {s} i₂ o₂} {cₛ dₛ ins₁ ins₂}
→ mealy ⟦ c ∥ d ⟧ₛ[ g ] (cₛ ∥ₛ dₛ) (zipWith _++_ ins₁ ins₂) ≈ₚ zipWith _++_ (mealy ⟦ c ⟧ₛ[ g ] cₛ ins₁) (mealy ⟦ d ⟧ₛ[ g ] dₛ ins₂)
lemma∥ₚ {ins₁ = i₁ ∷ is₁} {i₂ ∷ is₂} with ,-injective (splitAt′-++-inverse {xs = i₁} {ys = i₂})
lemma∥ₚ {m} {g = g} {c} {d} {cₛ} {dₛ} {i₁ ∷ is₁} {i₂ ∷ is₂} | i₁≡ , i₂≡ rewrite i₁≡ | i₂≡ = refl ∷ₚ ♯ transₚ (≈-to-≈ₚ (≡-to-≈ sub)) lemma∥ₚ
where sub = cong-app (cong₂ (λ z₁ z₂ → mealy ⟦ c ∥ d ⟧ₛ[ g ] ((proj₁ (⟦ c ⟧ₛ[ g ] cₛ z₁)) ∥ₛ (proj₁ (⟦ d ⟧ₛ[ g ] dₛ z₂)))) i₁≡ i₂≡)
(zipWith _++_ (♭ is₁) (♭ is₂))
mealy⟦⟧ₛ[–]-∥⇒zipWith++ₚ : ∀ {i₁ i₂ o₁ o₂ s G} (g : TyGate G W⟶W) (c : ℂ G {s} i₁ o₁) (d : ℂ G {s} i₂ o₂) {cₛ dₛ xs ys}
→ mealy ⟦ c ∥ d ⟧ₛ[ g ] (cₛ ∥ₛ dₛ) (zipWith _++_ xs ys) ≈ₚ zipWith _++_ (mealy ⟦ c ⟧ₛ[ g ] cₛ xs) (mealy ⟦ d ⟧ₛ[ g ] dₛ ys)
mealy⟦⟧ₛ[–]-∥⇒zipWith++ₚ _ _ _ {xs = x ∷ _} {y ∷ _} with ,-injective (splitAt′-++-inverse {xs = x} {y})
mealy⟦⟧ₛ[–]-∥⇒zipWith++ₚ {m} g c d {cₛ} {dₛ} {_ ∷ xs} {_ ∷ ys} | x≡ , y≡ rewrite x≡ | y≡ = refl ∷ₚ ♯ transₚ (≈-to-≈ₚ (≡-to-≈ sub))
(mealy⟦⟧ₛ[–]-∥⇒zipWith++ₚ g c d)
where sub = cong-app (cong₂ (λ z₁ z₂ → mealy ⟦ c ∥ d ⟧ₛ[ g ] ((proj₁ (⟦ c ⟧ₛ[ g ] cₛ z₁)) ∥ₛ (proj₁ (⟦ d ⟧ₛ[ g ] dₛ z₂)))) x≡ y≡)
(zipWith _++_ (♭ xs) (♭ ys))
\end{code}
%</lemma∥ₚ>
%</mealy⟦⟧ₛ[–]-∥⇒zipWith++ₚ>
%<*lemma∥>
\AgdaTarget{lemma∥}
%<*mealy⟦⟧ₛ[–]-∥⇒zipWith++>
\AgdaTarget{mealy⟦⟧ₛ[–]-∥⇒zipWith++}
\begin{code}
lemma∥ : ∀ {i₁ i₂ o₁ o₂ s G} {g : TyGate G W⟶W} {c : ℂ G {s} i₁ o₁} {d : ℂ G {s} i₂ o₂} {cₛ dₛ ins₁ ins₂}
→ mealy ⟦ c ∥ d ⟧ₛ[ g ] (cₛ ∥ₛ dₛ) (zipWith _++_ ins₁ ins₂) ≈ zipWith _++_ (mealy ⟦ c ⟧ₛ[ g ] cₛ ins₁) (mealy ⟦ d ⟧ₛ[ g ] dₛ ins₂)
lemma∥ = ≈ₚ-to-≈ lemma∥ₚ
mealy⟦⟧ₛ[–]-∥⇒zipWith++ : ∀ {i₁ i₂ o₁ o₂ s G} (g : TyGate G W⟶W) (c : ℂ G {s} i₁ o₁) (d : ℂ G {s} i₂ o₂) {cₛ dₛ xs ys}
→ mealy ⟦ c ∥ d ⟧ₛ[ g ] (cₛ ∥ₛ dₛ) (zipWith _++_ xs ys) ≈ zipWith _++_ (mealy ⟦ c ⟧ₛ[ g ] cₛ xs) (mealy ⟦ d ⟧ₛ[ g ] dₛ ys)
mealy⟦⟧ₛ[–]-∥⇒zipWith++ g c d = ≈ₚ-to-≈ (mealy⟦⟧ₛ[–]-∥⇒zipWith++ₚ g c d)
\end{code}
%</lemma∥>
%</mealy⟦⟧ₛ[–]-∥⇒zipWith++>
%<*proof∥>
\AgdaTarget{proof∥}
%<*⟦⟧ω'[–]-∥⇒zipWith++>
\AgdaTarget{⟦⟧ω'[–]-∥⇒zipWith++}
\begin{code}
proof∥ : ∀ {i₁ i₂ o₁ o₂ s G} {g : TyGate G W⟶W} {c : ℂ G {s} i₁ o₁} {d : ℂ G {s} i₂ o₂} {ins₁ ins₂}
→ ⟦ c ∥ d ⟧ω'[ g ] (zipWith _++_ ins₁ ins₂) ≈ zipWith _++_ (⟦ c ⟧ω'[ g ] ins₁) (⟦ d ⟧ω'[ g ] ins₂)
proof∥ = lemma∥
⟦⟧ω'[–]-∥⇒zipWith++ : ∀ {i₁ i₂ o₁ o₂ s G} (g : TyGate G W⟶W) (c : ℂ G {s} i₁ o₁) (d : ℂ G {s} i₂ o₂) {xs ys}
→ ⟦ c ∥ d ⟧ω'[ g ] (zipWith _++_ xs ys) ≈ zipWith _++_ (⟦ c ⟧ω'[ g ] xs) (⟦ d ⟧ω'[ g ] ys)
⟦⟧ω'[–]-∥⇒zipWith++ g c d = mealy⟦⟧ₛ[–]-∥⇒zipWith++ g c d
\end{code}
%</proof∥>
%</⟦⟧ω'[–]-∥⇒zipWith++>
......@@ -14,20 +14,21 @@ open import PiWare.Semantics.SimulationState A using (⟦_⟧ₛ[_]; ⟦_⟧ω'[
\end{code}
%<*lemma⟫>
\AgdaTarget{lemma⟫}
%<*mealy⟦⟧ₛ[–]-⟫⇒∘>
\AgdaTarget{mealy⟦⟧ₛ[–]-⟫⇒∘}
\begin{code}
lemma⟫ : ∀ {i m o s G} {g : TyGate G W⟶W} {c : ℂ G {s} i m} {d : ℂ G m o} {cₛ dₛ ins}
→ mealy ⟦ c ⟫ d ⟧ₛ[ g ] (cₛ ⟫ₛ dₛ) ins ≈ mealy ⟦ d ⟧ₛ[ g ] dₛ (mealy ⟦ c ⟧ₛ[ g ] cₛ ins)
lemma⟫ {ins = x ∷ xs} = refl ∷ (♯ lemma⟫)
mealy⟦⟧ₛ[–]-⟫⇒∘ : ∀ {i m o s G} (g : TyGate G W⟶W) (c : ℂ G {s} i m) (d : ℂ G m o) {cₛ dₛ xs}
→ mealy ⟦ c ⟫ d ⟧ₛ[ g ] (cₛ ⟫ₛ dₛ) xs ≈ mealy ⟦ d ⟧ₛ[ g ] dₛ (mealy ⟦ c ⟧ₛ[ g ] cₛ xs)
mealy⟦⟧ₛ[–]-⟫⇒∘ g c d {xs = _ ∷ _} = refl ∷ ♯ mealy⟦⟧ₛ[–]-⟫⇒∘ g c d
\end{code}
%</lemma⟫>
%</mealy⟦⟧ₛ[–]-⟫⇒∘>
%<*proof⟫>
\AgdaTarget{proof⟫}
%<*⟦⟧ω'[–]-⟫⇒∘>
\AgdaTarget{⟦⟧ω'[–]-⟫⇒∘}
\begin{code}
proof⟫ : ∀ {i m o s G} {g : TyGate G W⟶W} {c : ℂ G {s} i m} {d : ℂ G {s} m o} {ins} → ⟦ c ⟫ d ⟧ω'[ g ] ins ≈ ⟦ d ⟧ω'[ g ] (⟦ c ⟧ω'[ g ] ins)
proof⟫ = lemma⟫
⟦⟧ω'[–]-⟫⇒∘ : ∀ {i m o s G} (g : TyGate G W⟶W) (c : ℂ G {s} i m) (d : ℂ G {s} m o) {xs}
→ ⟦ c ⟫ d ⟧ω'[ g ] xs ≈ ⟦ d ⟧ω'[ g ] (⟦ c ⟧ω'[ g ] xs)
⟦⟧ω'[–]-⟫⇒∘ g c d = mealy⟦⟧ₛ[–]-⟫⇒∘ g c d
\end{code}
%</proof⟫>
%</⟦⟧ω'[–]-⟫⇒∘>
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