Integrate Semantics/Simulation/Properties/Sequential*

parent eab3f485
......@@ -29,9 +29,7 @@ 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 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.Semantics.Simulation.Properties.Sequential Atomic-Bool using (⟦⟧ω[–]-cong; ⟦⟧ω[–]-∥⇒zipWith++; ⟦⟧ω[–]-⟫⇒∘)
open import PiWare.Samples.BoolTrioSeq using (reg; proofReg-never; proofReg-always)
open import Data.Serializable using (_⇕_; ⇕×)
......
......@@ -29,9 +29,7 @@ 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 (⟦⟧ω[–]-∥⇒zipWith++)
open import PiWare.Semantics.Simulation.Properties.SequentialSequencing Atomic-Bool using (⟦⟧ω[–]-⟫⇒∘)
open import PiWare.Semantics.Simulation.Properties.Sequential Atomic-Bool using (⟦⟧ω[–]-cong; ⟦⟧ω[–]-⟫⇒∘; ⟦⟧ω[–]-∥⇒zipWith++)
lemma-deconstruct-split : ∀ {α n d} {y z : α} {ys zs : Vec α n} {xs}
......
......@@ -35,8 +35,7 @@ open import PiWare.Semantics.Simulation Atomic-Bool using (module WithGates; W)
open import PiWare.Semantics.Simulation.BoolTrio using () renaming (spec to b₃)
open WithGates b₃ using (⟦_⟧ω; ⟦_⟧; ⟦_⟧ᶜ)
open import PiWare.Semantics.Simulation.Properties.Plugs Atomic-Bool using (vecCoerce; unfold-vecCoerce; vecCoerce-rightInverse; eq⤨⊑ωid)
open import PiWare.Semantics.Simulation.Properties.SequentialCongruence Atomic-Bool using (⟦⟧ω[–]-cong)
open import PiWare.Semantics.Simulation.Properties.SequentialSequencing Atomic-Bool using (⟦⟧ω[–]-⟫⇒∘)
open import PiWare.Semantics.Simulation.Properties.Sequential Atomic-Bool using (⟦⟧ω[–]-cong; ⟦⟧ω[–]-⟫⇒∘)
open import PiWare.Samples.BoolTrioSeq using (proofReg-never; proofReg-always)
open import Data.Serializable using (_⇕_; ⇕×)
......
\begin{code}
open import PiWare.Atomic using (Atomic)
module PiWare.Semantics.Simulation.Properties.SequentialSequencing (A : Atomic) where
module PiWare.Semantics.Simulation.Properties.Sequential (A : Atomic) where
open import Function using (_$_; _∘′_; id)
open import Function using (_∘′_; id)
open import Coinduction using (♯_; ♭)
open import Data.Stream using (Stream; _∷_; head; tail; map; take; drop; repeat; iterate; zipWith; lookup; _≈_; map-cong; head-cong; tail-cong)
open import Data.Stream.Equality.FromPointwiseEquality using (lookup≗⇒≈)
open import Data.Vec using (_++_)
open import Data.Vec.Extra using (splitAt′)
open import Data.Vec.Properties.Extra using (splitAt′-++-inverse)
open import Data.Product using (uncurry′; _,_) renaming (map to map×)
open import Data.Nat.Base using (zero; suc)
open import Data.List.NonEmpty using (_∷_; _∷⁺_; _⁺∷ʳ_; length) renaming (map to map⁺)
open import Data.List.NonEmpty.Extra using (zipWith⁺; tails⁺; reverse⁺′; inits⁺; unzip⁺; splitAt⁺; zip⁺)
open import Data.List.NonEmpty.Properties.Extra using (zipWith⁺-map⁺-zip⁺; unzip⁺-zip⁺-inverse)
open import Data.Stream using (_∷_; _≈_; tail; lookup; drop; tail-cong; head-cong; map; zipWith)
open import Data.Stream.Extra using (take⁺) renaming (inits⁺ to sinits⁺)
open import Data.Stream.Equality.FromPointwiseEquality using (lookup≗⇒≈)
open import Data.Stream.Properties using (≡-to-≈; module Setoidₛ; module EqReasoningₛ)
open import Data.Stream.Properties.Extra using
( lookup-drop; unfold'⁺-reverse⁺′; unfold-take⁺; lemma-drop-tail; lemma-lookup-drop; lemma-lookup-inits⁺-take⁺
; lemma-lookup-map; map⁺-id; map⁺-cong; reverse⁺′-involutive; map⁺-compose; lemma-tails⁺-inits⁺
; reverse⁺′-map⁺-commute; lemma-inits⁺-take⁺-inits⁺; map⁺-take⁺-mapₛ; take⁺-cong)
open import Data.Stream.Properties using (≡-to-≈; module Setoidₛ; module EqReasoningₛ)
; reverse⁺′-map⁺-commute; lemma-inits⁺-take⁺-inits⁺; map⁺-take⁺-mapₛ; take⁺-cong )
open import Relation.Binary.PropositionalEquality using (_≡_; _≗_; refl; sym; trans; cong; module ≡-Reasoning)
open ≡-Reasoning using (begin_; _≡⟨_⟩_; _≡⟨⟩_; _∎)
open import Data.List.NonEmpty using (_∷_; _∷⁺_; _⁺∷ʳ_) renaming (map to map⁺)
open import Data.List.NonEmpty.Extra using (tails⁺; reverse⁺′; inits⁺)
open import Data.Nat.Base using (zero; suc)
open Setoidₛ using () renaming (refl to reflₛ; sym to symₛ)
open EqReasoningₛ using (_≈⟨_⟩_) renaming (begin_ to beginₛ_; _∎ to _∎ₛ)
open import Data.CausalStream using (runᶜ′)
open import PiWare.Circuit using (ℂ; _⟫_)
open import Data.CausalStream using (_⇒ᶜ_; runᶜ′; runᶜ)
open import PiWare.Circuit using (ℂ; _⟫_; _∥_)
open import PiWare.Circuit.Algebra using (TyGate)
open import PiWare.Semantics.Simulation.Properties.SequentialCongruence A using (runᶜ′-cong)
open import PiWare.Semantics.Simulation A using (W⟶W; ⟦_⟧ω[_]; ⟦_⟧ᶜ[_]; ⟦_⟧[_])
open import PiWare.Semantics.Simulation A using (W⟶W; ⟦_⟧ω[_]; ⟦_⟧ᶜ[_])
\end{code}
open Setoidₛ using () renaming (refl to reflₛ; sym to symₛ)
open EqReasoningₛ using (_≈⟨_⟩_) renaming (begin_ to beginₛ_; _∎ to _∎ₛ)
%<*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>
%<*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>
%<*⟦⟧ᶜ-∥⇒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 ]) (x⁰⁻ , y⁰⁻)
≡⟨ refl ⟩
⟦ c ⟧ᶜ[ g ] x⁰⁻ ++ ⟦ d ⟧ᶜ[ g ] y⁰⁻ ∎
\end{code}
%</⟦⟧ᶜ-∥⇒zipWith++>
%<*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++>
%<*lemma-drop-ω′>
......
\begin{code}
open import PiWare.Atomic using (Atomic)
module PiWare.Semantics.Simulation.Properties.SequentialCongruence (A : Atomic) where
open import Coinduction using (♯_; ♭)
open import Data.Stream using (_∷_; _≈_)
open import Data.List.NonEmpty using (_∷_)
open import Relation.Binary.PropositionalEquality using (_≡_; _≗_; refl; sym; trans)
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>
\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>
%<*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>
\begin{code}
open import PiWare.Atomic using (Atomic)
module PiWare.Semantics.Simulation.Properties.SequentialParalleling (A : Atomic) where
open import Function using (_∘′_; id)
open import Coinduction using (♯_; ♭)
open import Data.List.NonEmpty using (_∷_; length) renaming (map to map⁺)
open import Data.List.NonEmpty.Extra using (unzip⁺; splitAt⁺; zipWith⁺; zip⁺)
open import Data.List.NonEmpty.Properties.Extra using (zipWith⁺-map⁺-zip⁺; unzip⁺-zip⁺-inverse)
open import Data.Nat.Base using (suc)
open import Data.Product using (_,_; uncurry′; map)
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 import PiWare.Circuit using (ℂ; _∥_)
open import PiWare.Circuit.Algebra using (TyGate)
open import PiWare.Semantics.Simulation A using (W⟶W; ⟦_⟧ω[_]; ⟦_⟧ᶜ[_]; ⟦_⟧[_])
\end{code}
%<*⟦⟧ᶜ-∥⇒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 ]) (x⁰⁻ , y⁰⁻)
≡⟨ refl ⟩
⟦ c ⟧ᶜ[ g ] x⁰⁻ ++ ⟦ d ⟧ᶜ[ g ] y⁰⁻ ∎
\end{code}
%</⟦⟧ᶜ-∥⇒zipWith++>
%<*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++>
......@@ -24,7 +24,7 @@ import Data.IVec
import Data.List.Extra
import Data.List.NonEmpty.Extra
import Data.List.NonEmpty.Properties.Extra -- M
import Data.List.NonEmpty.Properties.Extra
--import Data.Rvec
--import Data.RVec
......@@ -32,19 +32,19 @@ import Data.List.NonEmpty.Properties.Extra -- M
import Data.Serializable.Bool
import Data.Serializable
import Data.Stream.DistantReasoning -- M
import Data.Stream.Equality.FromPointwiseEquality -- M
import Data.Stream.Equality.FromPrefixEquality -- M
import Data.Stream.Equality.NAD -- M
import Data.Stream.Equality.WithTrans -- M
import Data.Stream.Extra -- M
import Data.Stream.Properties -- M
import Data.Stream.Properties.Extra -- M
import Data.Stream.DistantReasoning
import Data.Stream.Equality.FromPointwiseEquality
import Data.Stream.Equality.FromPrefixEquality
import Data.Stream.Equality.NAD
import Data.Stream.Equality.WithTrans
import Data.Stream.Extra
import Data.Stream.Properties
import Data.Stream.Properties.Extra
import Data.Vec.Extra
import Data.Vec.Forall
import Data.Vec.Padding
import Data.Vec.Properties.Extra -- M
import Data.Vec.Properties.Extra
import Function.Bijection.Sets
import Function.Extra
......@@ -67,10 +67,10 @@ import PiWare.Plugs
import PiWare.Samples.BoolTrioComb
import PiWare.Samples.BoolTrioSeq
import PiWare.Samples.Muxes
import PiWare.Samples.RegN -- M
import PiWare.Samples.RegN' -- M
import PiWare.Samples.RegN'Properties -- M
import PiWare.Samples.RegProperties -- M
import PiWare.Samples.RegN
import PiWare.Samples.RegN'
import PiWare.Samples.RegN'Properties
import PiWare.Samples.RegProperties
import PiWare.Semantics.AreaAnalysis.BoolTrio
import PiWare.Semantics.AreaAnalysis.Nand
......@@ -79,21 +79,19 @@ import PiWare.Semantics.Simulation.BoolTrio
import PiWare.Semantics.Simulation.Compliance
import PiWare.Semantics.Simulation.Equality
import PiWare.Semantics.Simulation.Nand
import PiWare.Semantics.Simulation.Properties.Extension -- M
import PiWare.Semantics.Simulation.Properties.NoExtension -- M
import PiWare.Semantics.Simulation.Properties.Extension
import PiWare.Semantics.Simulation.Properties.NoExtension
import PiWare.Semantics.Simulation.Properties.Plugs
import PiWare.Semantics.Simulation.Properties.SequentialCongruence -- M
import PiWare.Semantics.Simulation.Properties.SequentialParalleling -- M
import PiWare.Semantics.Simulation.Properties.SequentialSequencing -- M
import PiWare.Semantics.Simulation.Properties.Sequential
import PiWare.Semantics.Simulation.Properties
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.Properties.SequentialCongruence -- M
import PiWare.Semantics.SimulationState.Properties.SequentialParalleling -- M
import PiWare.Semantics.SimulationState.Properties.SequentialSequencing -- M
import PiWare.Semantics.SimulationState -- M
import PiWare.Semantics.SimulationState.Properties.SequentialCongruence
import PiWare.Semantics.SimulationState.Properties.SequentialParalleling
import PiWare.Semantics.SimulationState.Properties.SequentialSequencing
import PiWare.Semantics.SimulationState
import PiWare.Typed.Circuit
import PiWare.Typed.Patterns
......@@ -102,7 +100,7 @@ import PiWare.Typed.Samples.BoolTrioComb
import PiWare.Typed.Samples.BoolTrioSeq
import PiWare.Typed.Samples.Muxes
import PiWare.Typed.Semantics.Simulation
import PiWare.Typed.Semantics.ProofLifting -- M
import PiWare.Typed.Semantics.ProofLifting
import Relation.Binary.Indexed.Core.Extra
......
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