Fix fixities

parent 2b5d1abd
......@@ -44,6 +44,11 @@ c₁ ≗[ g ] c₂ at w = ⟦ c₁ ⟧[ g ] w ≡ ⟦ c₂ ⟧[ g ] w
\end{code}
%</eq-pointwise-at>
\begin{code}
infix 3 _≗[_]_
\end{code}
%<*eq-pointwise>
\AgdaTarget{\_≗[\_]\_}
\begin{code}
......@@ -60,6 +65,11 @@ c₁ ≗ᶜ[ g ] c₂ at γ = ⟦ c₁ ⟧ᶜ[ g ] γ ≡ ⟦ c₂ ⟧ᶜ[ g ]
\end{code}
%</eq-pointwise-c-at>
\begin{code}
infix 3 _≗ᶜ[_]_
\end{code}
%<*eq-pointwise-c>
\AgdaTarget{\_≗ᶜ[\_]\_}
\begin{code}
......@@ -76,6 +86,11 @@ c₁ ≗ω[ g ] c₂ at ins = ⟦ c₁ ⟧ω[ g ] ins ≈ₛ ⟦ c₂ ⟧ω[ g ]
\end{code}
%</eq-pointwise-omega-at>
\begin{code}
infix 3 _≗ω[_]_
\end{code}
%<*eq-pointwise-omega>
\AgdaTarget{\_≗ω[\_]\_}
\begin{code}
......@@ -93,6 +108,11 @@ c₁ ≅[ g ] c₂ at w = ⟦ c₁ ⟧[ g ] w ≈ ⟦ c₂ ⟧[ g ] w
\end{code}
%</eq-semihet-at>
\begin{code}
infix 3 _≅[_]_
\end{code}
%<*eq-semihet>
\AgdaTarget{\_≅[\_]\_}
\begin{code}
......@@ -109,6 +129,11 @@ c₁ ≅ᶜ[ g ] c₂ at γ = ⟦ c₁ ⟧ᶜ[ g ] γ ≈ ⟦ c₂ ⟧ᶜ[ g ]
\end{code}
%</eq-semihet-c-at>
\begin{code}
infix 3 _≅ᶜ[_]_
\end{code}
%<*eq-semihet-c>
\AgdaTarget{\_≅ᶜ[\_]\_}
\begin{code}
......@@ -125,6 +150,11 @@ c₁ ≅ω[ g ] c₂ at ins = ⊥ where postulate ⊥ : _ -- ⟦ c₁ ⟧ω[ g
\end{code}
%</eq-semihet-omega-at>
\begin{code}
infix 3 _≅ω[_]_
\end{code}
%<*eq-semihet-omega>
\AgdaTarget{\_≅ω[\_]\_}
\begin{code}
......@@ -134,6 +164,11 @@ c₁ ≅ω[ g ] c₂ = ∀ ins → c₁ ≅ω[ g ] c₂ at ins
%</eq-semihet-omega>
\begin{code}
infix 3 _≊[_]_
\end{code}
%<*eq-preserve-semihet>
\AgdaTarget{\_≊[\_]\_}
\begin{code}
......@@ -142,11 +177,17 @@ c₁ ≊[ g ] c₂ = ∀ {w w′} → w ≈ w′ → ⟦ c₁ ⟧[ g ] w ≈ ⟦
\end{code}
%</eq-preserve-semihet>
\begin{code}
--infix 3 _≊ᶜ[_]_
\end{code}
-- TODO: The equality on the left is always over the argument of the carrier, but index-heterogeneous
%<*eq-preserve-semihet-c>
\AgdaTarget{\_≊[\_]\_}
\begin{code}
_≊ᶜ[_]_ : ∀ {i o i′ o′ G} → ℂ G {ω} i o → TyGate G W⟶W → ℂ G {ω} i′ o′ → Set
c₁ ≊ᶜ[ g ] c₂ = ∀ {w w′} → w ≈ w′ → ⟦ c₁ ⟧ᶜ[ g ] w ≈ ⟦ c₂ ⟧ᶜ[ g ] w′
--_≊ᶜ[_]_ : ∀ {i o i′ o′ G} → ℂ G {ω} i o → TyGate G W⟶W → ℂ G {ω} i′ o′ → Set
--c₁ ≊ᶜ[ g ] c₂ = ∀ {w w′} → _NE.≈_ w w′ → ⟦ c₁ ⟧ᶜ[ g ] w ≈ ⟦ c₂ ⟧ᶜ[ g ] w′
\end{code}
%</eq-preserve-semihet-c>
......@@ -162,6 +203,11 @@ module ≊-unsound where
%</eq-preserve-semihet-unsound>
\begin{code}
infix 3 _≋[_]_
\end{code}
%<*eq>
\AgdaTarget{\_≋[\_]\_}
\begin{code}
......@@ -277,7 +323,7 @@ module WithGates {G} (g : TyGate G W⟶W) where
%</eq-pointwise-at-with-gates>
\begin{code}
infixl 3 _≗_
infix 3 _≗_
\end{code}
%<*eq-pointwise-with-gates>
......@@ -298,7 +344,7 @@ module WithGates {G} (g : TyGate G W⟶W) where
%</eq-semihet-at-with-gates>
\begin{code}
infixl 3 _≅_
infix 3 _≅_
\end{code}
%<*eq-semihet-with-gates>
......@@ -311,7 +357,7 @@ module WithGates {G} (g : TyGate G W⟶W) where
\begin{code}
infixl 3 _≊_
infix 3 _≊_
\end{code}
%<*eq-preserve-semihet-with-gates>
......@@ -324,7 +370,7 @@ module WithGates {G} (g : TyGate G W⟶W) where
\begin{code}
infixl 3 _≋_
infix 3 _≋_
\end{code}
%<*eq-with-gates>
......
......@@ -3,42 +3,41 @@ open import PiWare.Atomic using (Atomic)
module PiWare.Semantics.Simulation.Properties.Extension (A : Atomic) where
open import Function using (_$_; _∘′_; id)
open import Function using (_$_; _⟨_⟩_)
open import Coinduction using (♯_; ♭)
open import Data.CausalStream using (runᶜ′)
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
open import Data.Stream.Equality.WithTrans using (_≈ₚ_; _∷_; ≈ₚ-to-≈; ≈-to-≈ₚ) renaming (refl to sreflₚ; trans to stransₚ)
open import Relation.Binary
import Relation.Binary.EqReasoning
open import Relation.Binary.PropositionalEquality using (_≡_; _≗_; refl; sym; trans; inspect; [_])
import Relation.Binary.PropositionalEquality as P
import Data.List.NonEmpty as NL
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 Relation.Binary.PropositionalEquality using (_≗_; refl)
open import Data.List.NonEmpty using (_∷_)
open import PiWare.Gates using (Gates)
open Gates ⦃ … ⦄ using (Gate#; |in|; |out|)
open import PiWare.Circuit using (ℂ; C; σ; ω; Gate; Plug; _⟫_; _∥_)
open Gates using (|in|; |out|)
open import PiWare.Circuit using (ℂ; C; Gate; Plug)
open import PiWare.Circuit.Algebra using (TyGate)
open import PiWare.Plugs.Core using (_⤪_)
open import PiWare.Semantics.Simulation A using (W⟶W; ⟦_⟧[_]; ⟦_⟧ω[_]; ⟦_⟧ᶜ[_])
private
open module StreamSetoid {A} = Setoid (Data.Stream.setoid A) using () renaming (refl to srefl; sym to ssym; trans to strans)
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 NL.∷ cs) ins ≈ₚ f c0 ∷ ♯ map f ins
lemma-plug {g = g} pp {c0 = c0} (x ∷ xs) rewrite pp c0 = refl ∷ ♯ (stransₚ (lemma-plug {g = g} pp (♭ xs)) (refl ∷ (♯ sreflₚ)))
→ ⟦ 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ₚ)
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) = strans (≈ₚ-to-≈ (lemma-plug {g = g} pp (♭ xs))) (refl ∷ (♯ srefl))
proof-plug {g = g} pp (x ∷ xs) = ≈ₚ-to-≈ $ lemma-plug {g = g} pp (♭ xs) ⟨ transₚ ⟩ (refl ∷ₚ ♯ reflₚ)
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ₚ)
lemma-gate : ∀ {G h} {g : TyGate G W⟶W} {f : W⟶W (|in| h) (|out| h)} → ⟦ Gate h ⟧[ g ] ≗ f → ∀ {c0 cs} ins → runᶜ′ ⟦ Gate h ⟧ᶜ[ g ] (c0 NL.∷ cs) ins ≈ₚ f c0 ∷ ♯ map f ins
lemma-gate {g = g} pp {c0 = c0} (x ∷ xs) rewrite pp c0 = refl ∷ ♯ (stransₚ (lemma-gate {g = g} pp (♭ xs)) (refl ∷ (♯ sreflₚ)))
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ₚ)
proof-gate : ∀ {G h} {g : TyGate G W⟶W} {f : W⟶W (|in| h) (|out| h)} → ⟦ Gate h ⟧[ g ] ≗ f → ∀ ins → ⟦ Gate h ⟧ω[ g ] ins ≈ map f ins
proof-gate {g = g} pp (x ∷ xs) = strans (≈ₚ-to-≈ (lemma-gate {g = g} pp (♭ xs))) (refl ∷ (♯ srefl))
-- The property we would actually like to have
ω-extends-σ : Set₁
......
......@@ -11,7 +11,7 @@ open import Data.Vec using (Vec; lookup; tabulate; allFin; map; splitAt)
open import Data.Vec.Properties using (lookup-morphism; tabulate∘lookup; lookup∘tabulate; map-lookup-allFin)
open import Data.Vec.Equality using () renaming (module PropositionalEquality to VPE)
open VPE using (from-≡)
open import Relation.Binary.PropositionalEquality using (refl; _≡_; sym; cong; module ≡-Reasoning)
open import Relation.Binary.PropositionalEquality using (refl; _≡_; sym; cong; module ≡-Reasoning; _≗_)
open ≡-Reasoning using (begin_; _∎; _≡⟨_⟩_; _≡⟨⟩_)
open import Category.Functor.Extra using (app-NaturalT)
......@@ -40,7 +40,7 @@ lookupᵗ = flip lookup
%<*plug-Vec-implements-eta-identical>
\AgdaTarget{plug-Vecη⫃op[\_]}
\begin{code}
plug-Vecη⫃op[_] : ∀ {i o G} (g : TyGate G W⟶W) (η : VecNaturalT i o) → (plug-Vecη η) ⫃[ g ] (op η)
plug-Vecη⫃op[_] : ∀ {i o G} (g : TyGate G W⟶W) (η : VecNaturalT i o) → plug-Vecη η ⫃[ g ] op η
plug-Vecη⫃op[_] {i} g η w = begin
tabulate (λ i → lookupᵗ w (lookup i $ op η (allFin _))) ≡⟨ tabulate-ext (λ i → sym $ op-<$> (app-NaturalT $ lookup-morphism i) (lookupᵗ w) _) ⟩
tabulate (lookupᵗ (map (lookupᵗ w) (op η (allFin _)))) ≡⟨ tabulate-ext (λ i → sym $ cong (lookup i) (op-<$> η (lookupᵗ w) _)) ⟩
......@@ -53,7 +53,7 @@ plug-Vecη⫃op[_] {i} g η w = begin
%<*plug-Vec-implements-eta-one-input>
\AgdaTarget{plug-Vecη⫅op[\_]}
\begin{code}
plug-Vecη⫅op[_] : ∀ {i o G} (g : TyGate G W⟶W) (η : VecNaturalT i o) → (plug-Vecη η) ⫅[ g ] (op η)
plug-Vecη⫅op[_] : ∀ {i o G} (g : TyGate G W⟶W) (η : VecNaturalT i o) → plug-Vecη η ⫅[ g ] op η
plug-Vecη⫅op[_] {i} g η w = from-≡ (plug-Vecη⫃op[ g ] η w)
\end{code}
%</plug-Vec-implements-eta-one-input>
......@@ -92,10 +92,10 @@ id⤨-cong refl = ≋-refl
%<*id-plug-par-fusion-identical>
\AgdaTarget{∥-id⤨≡[\_]}
\begin{code}
∥-id⤨≡[_] : ∀ {n m G} (g : TyGate G W⟶W) → ∀ w → ⟦ id⤨ {n} ∥ id⤨ {m} ⟧[ g ] w ≡ ⟦ id⤨ {n + m} ⟧[ g ] w
∥-id⤨≡[_] {n} g w with splitAt n w
∥-id⤨≡[_] {n} g w | wₙ , wₘ , w≡wₙ⧺wₘ with id⤨⫃id[ g ] wₙ | id⤨⫃id[ g ] wₘ | id⤨⫃id[ g ] w
∥-id⤨≡[_] {n} g w | wₙ , wₘ , w≡wₙ⧺wₘ | eq-wₙ | eq-wₘ | eq-w rewrite eq-wₙ | eq-wₘ | eq-w = sym w≡wₙ⧺wₘ
∥-id⤨≡[_] : ∀ {n m G} (g : TyGate G W⟶W) → ⟦ id⤨ {n} ∥ id⤨ {m} ⟧[ g ] ≗ ⟦ id⤨ {n + m} ⟧[ g ]
∥-id⤨≡[_] {n} _ w with splitAt n w
∥-id⤨≡[_] {_} g w | wₙ , wₘ , _ with id⤨⫃id[ g ] wₙ | id⤨⫃id[ g ] wₘ | id⤨⫃id[ g ] w
∥-id⤨≡[_] {_} _ w | wₙ , wₘ , w≡wₙ⧺wₘ | eq-wₙ | eq-wₘ | eq-w rewrite eq-wₙ | eq-wₘ | eq-w = sym w≡wₙ⧺wₘ
\end{code}
%</id-plug-par-fusion-identical>
......@@ -110,7 +110,7 @@ id⤨-cong refl = ≋-refl
%<*id-plug-par-fusion>
\AgdaTarget{∥-id⤨≋[\_]}
\begin{code}
∥-id⤨≋[_] : ∀ {n m G} (g : TyGate G W⟶W) → id⤨ {n} ∥ id⤨ {m} ≋[ g ] id⤨ {n + m}
∥-id⤨≋[_] : ∀ {n m G} (g : TyGate G W⟶W) → (id⤨ {n} ∥ id⤨ {m}) ≋[ g ] (id⤨ {n + m})
∥-id⤨≋[_] {n} {m} g = ≅⇒≋ (∥-id⤨≅[_] {n} g)
\end{code}
%</id-plug-par-fusion>
......@@ -163,7 +163,8 @@ plug-Vecη-∘[ g ] η ε = ≅⇒≋ (plug-Vecη-∘≅[ g ] η ε)
%<*plug-Vec-eta-ext-one-input>
\AgdaTarget{plug-Vecη-ext≅[\_]}
\begin{code}
plug-Vecη-ext≅[_] : ∀ {i o G} (g : TyGate G W⟶W) (η : VecNaturalT i o) (ε : VecNaturalT i o) → (∀ {X} (w : Vec X i) → op η w ≡ op ε w) → plug-Vecη η ≅[ g ] plug-Vecη ε
plug-Vecη-ext≅[_] : ∀ {i o G} (g : TyGate G W⟶W) (η : VecNaturalT i o) (ε : VecNaturalT i o)
→ (∀ {X} (w : Vec X i) → op η w ≡ op ε w) → plug-Vecη η ≅[ g ] plug-Vecη ε
plug-Vecη-ext≅[ g ] η ε η≈ε w = from-≡ $ begin
⟦ plug-Vecη η ⟧[ g ] w ≡⟨ plug-Vecη⫃op[ g ] η w ⟩
op η w ≡⟨ η≈ε w ⟩
......@@ -175,7 +176,8 @@ plug-Vecη-ext≅[ g ] η ε η≈ε w = from-≡ $ begin
%<*plug-Vec-eta-ext>
\AgdaTarget{plug-Vecη-ext[\_]}
\begin{code}
plug-Vecη-ext[_] : ∀ {i o G} (g : TyGate G W⟶W) {η : VecNaturalT i o} {ε : VecNaturalT i o} → (∀ {X} (w : Vec X i) → op η w ≡ op ε w) → plug-Vecη η ≋[ g ] plug-Vecη ε
plug-Vecη-ext[_] : ∀ {i o G} (g : TyGate G W⟶W) {η : VecNaturalT i o} {ε : VecNaturalT i o}
→ (∀ {X} (w : Vec X i) → op η w ≡ op ε w) → plug-Vecη η ≋[ g ] plug-Vecη ε
plug-Vecη-ext[ g ] {η} {ε} p = ≅⇒≋ (plug-Vecη-ext≅[ g ] η ε p)
\end{code}
%</plug-Vec-eta-ext>
......@@ -234,7 +236,7 @@ module WithGates {G} (g : TyGate G W⟶W) where
%<*id-plug-par-fusion-identical-with-gates>
\AgdaTarget{∥-id⤨≡}
\begin{code}
∥-id⤨≡ : ∀ {n m} → ∀ w → ⟦ id⤨ {n} ∥ id⤨ {m} ⟧ w ≡ ⟦ id⤨ {n + m} ⟧ w
∥-id⤨≡ : ∀ {n m} → ⟦ id⤨ {n} ∥ id⤨ {m} ⟧ ≗ ⟦ id⤨ {n + m} ⟧
∥-id⤨≡ {n} {m} w = ∥-id⤨≡[_] {n} {m} g w
\end{code}
%</id-plug-par-fusion-identical-with-gates>
......
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