Merge Extension and NoExtension

parent f95079bd
......@@ -3,43 +3,92 @@ open import PiWare.Atomic using (Atomic)
module PiWare.Semantics.Simulation.Properties.Extension (A : Atomic) where
open import Function using (_$_; _⟨_⟩_)
open import Function using (_$_; _⟨_⟩_; _∘′_)
open import Coinduction using (♯_; ♭)
open import Data.Bool.Base using () renaming (false to 𝔽; true to 𝕋)
open import Data.Fin using () renaming (zero to Fz; suc to Fs)
open import Data.Vec using ([]; _∷_; [_]; head)
open import Data.List.NonEmpty using (_∷_)
open import Data.CausalStream using (runᶜ′)
open import Data.Stream using (Stream; _∷_; _≈_; map)
open import Data.Stream.Properties using (module Setoidₛ)
open Setoidₛ using () renaming (trans to transₛ; refl to reflₛ)
open import Data.Stream.Equality.WithTrans using (_≈ₚ_; _∷ₚ_; ≈ₚ-to-≈; ≈-to-≈ₚ; reflₚ; transₚ)
open import Data.Stream using (Stream; _∷_; _≈_; map; repeat)
open import Data.Stream.Equality.WithTrans using (_≈ₚ_; _∷ₚ_; ≈ₚ-to-≈; reflₚ; transₚ)
open import Relation.Binary.PropositionalEquality using (_≗_; refl)
open import Data.List.NonEmpty using (_∷_)
open import Relation.Nullary using (¬_)
open import PiWare.Gates using (Gates)
open Gates using (|in|; |out|)
open import PiWare.Circuit using (C[_]; Gate; Plug)
open import PiWare.Circuit.Algebra using (TyGate)
open import PiWare.Gates.BoolTrio using () renaming (BoolTrio to B₃)
open import PiWare.Plugs.Core using (_⤪_)
open import PiWare.Circuit using (C[_]; Gate; Plug; σ; ω)
open import PiWare.Circuit.Algebra using (TyGate)
open import PiWare.Semantics.Simulation A using (W⟶W; ⟦_⟧[_]; ⟦_⟧ω[_]; ⟦_⟧ᶜ[_])
open import PiWare.Semantics.Simulation.BoolTrio using () renaming (spec to b₃)
\end{code}
lemma-plug : ∀ {i o G} {g : TyGate G W⟶W} {p : i ⤪ o} {f}
→ ⟦ Plug p ⟧[ g ] ≗ f → ∀ {c0 cs} ins → runᶜ′ ⟦ Plug p ⟧ᶜ[ g ] (c0 ∷ cs) ins ≈ₚ f c0 ∷ ♯ map f ins
lemma-plug {g = g} pp {c0 = c0} (x ∷ xs) rewrite pp c0 = refl ∷ₚ ♯ transₚ (lemma-plug {g = g} pp (♭ xs)) (refl ∷ₚ ♯ reflₚ)
%<*runᶜ′⟦⟧ᶜ⇒⟦⟧-Plug>
\AgdaTarget{runᶜ′⟦⟧ᶜ⇒⟦⟧-Plug}
\begin{code}
runᶜ′⟦⟧ᶜ⇒⟦⟧-Plug : ∀ {i o G} {g : TyGate G W⟶W} {p : i ⤪ o} {f}
→ ⟦ Plug p ⟧[ g ] ≗ f → (∀ {x⁰ x⁻} x⁺ → runᶜ′ ⟦ Plug p ⟧ᶜ[ g ] (x⁰ ∷ x⁻) x⁺ ≈ₚ f x⁰ ∷ ♯ map f x⁺)
runᶜ′⟦⟧ᶜ⇒⟦⟧-Plug {g = g} eq {x⁰} (x¹ ∷ x²⁺) rewrite eq x⁰ = refl ∷ₚ ♯ transₚ (runᶜ′⟦⟧ᶜ⇒⟦⟧-Plug {g = g} eq (♭ x²⁺)) (refl ∷ₚ ♯ reflₚ)
\end{code}
%</runᶜ′⟦⟧ᶜ⇒⟦⟧-Plug>
proof-plug : ∀ {i o G} {g : TyGate G W⟶W} {p : i ⤪ o} {f} → ⟦ Plug p ⟧[ g ] ≗ f → ∀ ins → ⟦ Plug p ⟧ω[ g ] ins ≈ map f ins
proof-plug {g = g} pp (x ∷ xs) = ≈ₚ-to-≈ $ lemma-plug {g = g} pp (♭ xs) ⟨ transₚ ⟩ (refl ∷ₚ ♯ reflₚ)
%<*⟦⟧ω⇒⟦⟧-Plug>
\AgdaTarget{⟦⟧ω⇒⟦⟧-Plug}
\begin{code}
⟦⟧ω⇒⟦⟧-Plug : ∀ {i o G} {g : TyGate G W⟶W} {p : i ⤪ o} {f} → ⟦ Plug p ⟧[ g ] ≗ f → (∀ xs → ⟦ Plug p ⟧ω[ g ] xs ≈ map f xs)
⟦⟧ω⇒⟦⟧-Plug {g = g} eq (x⁰ ∷ x⁺) = ≈ₚ-to-≈ $ runᶜ′⟦⟧ᶜ⇒⟦⟧-Plug {g = g} eq (♭ x⁺) ⟨ transₚ ⟩ (refl ∷ₚ ♯ reflₚ)
\end{code}
%</⟦⟧ω⇒⟦⟧-Plug>
lemma-gate : ∀ {G h} {g : TyGate G W⟶W} {f : W⟶W (|in| G h) (|out| G h)}
→ ⟦ Gate h ⟧[ g ] ≗ f → ∀ {c0 cs} ins → runᶜ′ ⟦ Gate h ⟧ᶜ[ g ] (c0 ∷ cs) ins ≈ₚ f c0 ∷ ♯ map f ins
lemma-gate {g = g} pp {c0 = c0} (x ∷ xs) rewrite pp c0 = refl ∷ₚ ♯ transₚ (lemma-gate {g = g} pp (♭ xs)) (refl ∷ₚ ♯ reflₚ)
%<*runᶜ′⟦⟧ᶜ⇒⟦⟧-Gate>
\AgdaTarget{runᶜ′⟦⟧ᶜ⇒⟦⟧-Gate}
\begin{code}
runᶜ′⟦⟧ᶜ⇒⟦⟧-Gate : ∀ {G h} {g : TyGate G W⟶W} {f : W⟶W (|in| G h) (|out| G h)}
→ ⟦ Gate h ⟧[ g ] ≗ f → (∀ {x⁰ x⁻} x⁺ → runᶜ′ ⟦ Gate h ⟧ᶜ[ g ] (x⁰ ∷ x⁻) x⁺ ≈ₚ f x⁰ ∷ ♯ map f x⁺)
runᶜ′⟦⟧ᶜ⇒⟦⟧-Gate {g = g} eq {x⁰} (x¹ ∷ x²⁺) rewrite eq x⁰ = refl ∷ₚ ♯ transₚ (runᶜ′⟦⟧ᶜ⇒⟦⟧-Gate {g = g} eq (♭ x²⁺)) (refl ∷ₚ ♯ reflₚ)
\end{code}
%</runᶜ′⟦⟧ᶜ⇒⟦⟧-Gate>
%<*⟦⟧ω⇒⟦⟧-Gate>
\AgdaTarget{⟦⟧ω⇒⟦⟧-Gate}
\begin{code}
⟦⟧ω⇒⟦⟧-Gate : ∀ {G h} {g : TyGate G W⟶W} {f : W⟶W (|in| G h) (|out| G h)}
→ ⟦ Gate h ⟧[ g ] ≗ f → (∀ xs → ⟦ Gate h ⟧ω[ g ] xs ≈ map f xs)
⟦⟧ω⇒⟦⟧-Gate {g = g} eq (x⁰ ∷ x⁺) = ≈ₚ-to-≈ $ runᶜ′⟦⟧ᶜ⇒⟦⟧-Gate {g = g} eq (♭ x⁺) ⟨ transₚ ⟩ (refl ∷ₚ ♯ reflₚ)
\end{code}
%</⟦⟧ω⇒⟦⟧-Gate>
proof-gate : ∀ {G h} {g : TyGate G W⟶W} {f : W⟶W (|in| G h) (|out| G h)} → ⟦ Gate h ⟧[ g ] ≗ f → ∀ ins → ⟦ Gate h ⟧ω[ g ] ins ≈ map f ins
proof-gate {g = g} pp (x ∷ xs) = ≈ₚ-to-≈ $ lemma-gate {g = g} pp (♭ xs) ⟨ transₚ ⟩ (refl ∷ₚ ♯ reflₚ)
-- The property we would actually like to have
%<*ω-extends-σ>
\AgdaTarget{ω-extends-σ}
\begin{code}
ω-extends-σ : Set₁
ω-extends-σ = ∀ {i o G} {g : TyGate G W⟶W} {c : C[ G ] i o} {f} → ⟦ c ⟧[ g ] ≗ f → ∀ ins → ⟦ c ⟧ω[ g ] ins ≈ map f ins
ω-extends-σ = ∀ {i o G} {g : TyGate G W⟶W} {c : C[ G ] i o} {f} → ⟦ c ⟧[ g ] ≗ f → (∀ xs → ⟦ c ⟧ω[ g ] xs ≈ map f xs)
\end{code}
%</ω-extends-σ>
%<*badC>
\AgdaTarget{badC}
\begin{code}
badC : C[ B₃ ] 2 1
badC {σ} = Plug (Fz ∷ [])
badC {ω} = Plug (Fs Fz ∷ [])
\end{code}
%</badC>
%<*¬ω-extends-σ>
\AgdaTarget{¬ω-extends-σ}
\begin{code}
--¬ω-extends-σ : ¬ ω-extends-σ
--¬ω-extends-σ e with e {g = b₃} {c = badC} {f = [_] ∘′ head} (λ {(_ ∷ _ ∷ []) → refl}) (repeat (𝕋 ∷ 𝔽 ∷ []))
--¬ω-extends-σ _ | () ∷ xs≈
\end{code}
%</¬ω-extends-σ>
\begin{code}
module PiWare.Semantics.Simulation.Properties.NoExtension where
open import Function using (_∘′_)
open import Data.Bool using () renaming (false to 𝔽; true to 𝕋)
open import Data.Fin using () renaming (zero to Fz; suc to Fs)
open import Data.Vec using ([]; _∷_; [_]; head)
open import Data.Stream using (repeat; _∷_)
open import Data.Empty using (⊥)
open import Relation.Nullary using (¬_)
open import Relation.Binary.PropositionalEquality using (refl)
open import PiWare.Circuit using (σ; ω; Plug) renaming (module WithGates to CircuitWithGates)
open import PiWare.Gates.BoolTrio using (BoolTrio)
open CircuitWithGates BoolTrio using (C)
open import PiWare.Atomic.Bool using (Atomic-Bool)
open import PiWare.Semantics.Simulation.Properties.Extension Atomic-Bool using (ω-extends-σ)
open import PiWare.Semantics.Simulation.BoolTrio using () renaming (spec to b₃)
badC : C 2 1
badC {σ} = Plug (Fz ∷ [])
badC {ω} = Plug (Fs Fz ∷ [])
¬ω-extends-σ : ¬ ω-extends-σ
¬ω-extends-σ e with e {g = b₃} {c = badC} {f = [_] ∘′ head} (λ {(_ ∷ _ ∷ []) → refl}) (repeat (𝕋 ∷ 𝔽 ∷ []))
¬ω-extends-σ _ | () ∷ xs≈
\end{code}
......@@ -326,10 +326,6 @@ module WithGates {G} (g : TyGate G W⟶W) where
%<*vecCoerce>
\AgdaTarget{vecCoerce}
\begin{code}
......
......@@ -80,7 +80,6 @@ import PiWare.Semantics.Simulation.Compliance
import PiWare.Semantics.Simulation.Equality
import PiWare.Semantics.Simulation.Nand
import PiWare.Semantics.Simulation.Properties.Extension
import PiWare.Semantics.Simulation.Properties.NoExtension
import PiWare.Semantics.Simulation.Properties.Plugs
import PiWare.Semantics.Simulation.Properties.Sequential
import PiWare.Semantics.Simulation.Properties
......
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