Commit 1a427415 by João Paulo Pizani Flor

Move out ProofSamples completely, some to general lemma modules

parent 0496a35e
 ... ... @@ -2,13 +2,14 @@ module Data.CausalStream where open import Level using (_⊔_) open import Function using (const) open import Data.Product using (_×_; _,_) open import Data.List.Base using (List; _∷_; []) open import Data.List.NonEmpty using (List⁺; _∷_) open import Data.List.NonEmpty.Extra using (tails⁺) open import Coinduction using (♯_; ♭) open import Data.Stream using (Stream; _∷_) open import Data.Stream using (Stream; _∷_; _≈_; repeat) open import Relation.Binary.PropositionalEquality using (refl) \end{code} ... ... @@ -41,13 +42,36 @@ pasts = tails⁺ % %<*run-causal> \AgdaTarget{runᶜ} %<*run-causal-prime> \AgdaTarget{runᶜ′} \begin{code} runᶜ′ : ∀ {α β} (fᶜ : α ⇒ᶜ β) (x⁰x⁻ : Γᶜ α) (x¹x⁺ : Stream α) → Stream β runᶜ′ fᶜ (x⁰ ∷ x⁻) (x¹ ∷ x⁺) = fᶜ (x⁰ ∷ x⁻) ∷ ♯ runᶜ′ fᶜ (x¹ ∷ x⁰ ∷ x⁻) (♭ x⁺) \end{code} % %<*run-causal> \AgdaTarget{runᶜ} \begin{code} runᶜ : ∀ {α β} (fᶜ : α ⇒ᶜ β) → (Stream α → Stream β) runᶜ fᶜ (x⁰ ∷ x⁺) = runᶜ′ fᶜ (x⁰ ∷ []) (♭ x⁺) \end{code} % %<*runᶜ′-const> \AgdaTarget{runᶜ′-const} \begin{code} runᶜ′-const : ∀ {α β} {x⁰⁻} {x⁺ : Stream α} (c : β) → runᶜ′ (const c) x⁰⁻ x⁺ ≈ repeat c runᶜ′-const {x⁺ = _ ∷ _} c = refl ∷ ♯ runᶜ′-const c \end{code} % %<*runᶜ-const> \AgdaTarget{runᶜ-const} \begin{code} runᶜ-const : ∀ {α β} {xs : Stream α} (c : β) → runᶜ (const c) xs ≈ repeat c runᶜ-const {xs = _ ∷ _} = runᶜ′-const \end{code} %
 \begin{code} module PiWare.ProofSamples.EmptySeq where open import Function using (_$_; _∘′_; id; const) open import Coinduction using (♯_; ♭) open import Data.Vec using (Vec; []) open import Data.Stream using (Stream; _∷_; _≈_; repeat) open import Relation.Binary.PropositionalEquality using (_≡_; refl) open import Data.CausalStream using (runᶜ; runᶜ′) \end{code} %<*runᶜ′-const> \AgdaTarget{runᶜ′-const} \begin{code} runᶜ′-const : ∀ {α β} {x⁰⁻} {x⁺ : Stream α} (c : β) → runᶜ′ (const c) x⁰⁻ x⁺ ≈ repeat c runᶜ′-const {x⁺ = _ ∷ _} c = refl ∷ ♯ runᶜ′-const c \end{code} % %<*runᶜ-const> \AgdaTarget{runᶜ-const} \begin{code} runᶜ-const : ∀ {α β} {xs : Stream α} (c : β) → runᶜ (const c) xs ≈ repeat c runᶜ-const {xs = _ ∷ _} = runᶜ′-const \end{code} %  \begin{code} open import PiWare.Atomic module PiWare.ProofSamples.EqPlug (A : Atomic) where open import Function using (id; _⟨_⟩_; _∘_; flip; _$_) open import Coinduction using (♯_) open import Data.CausalStream using (runᶜ′) open import Data.Stream using (_∷_; map; _≈_) open import Data.Stream.Properties using (module Setoidₛ) open import Data.Stream.Equality.WithTrans using (_≈ₚ_; _∷ₚ_; ≈ₚ-to-≈; reflₚ; transₚ) open import Data.List.NonEmpty using (_∷_; head) open import Data.Vec using (Vec; _∷_; tabulate; lookup; allFin) open import Data.Vec.Equality using () renaming (module PropositionalEquality to VPE) open VPE using (from-≡) renaming (_≈_ to _≈ᵥ_) open import Data.Vec.Properties using (lookup-allFin; tabulate∘lookup) open import Data.Vec.Properties.Extra using (tabulate-cong) open import Relation.Binary using (Setoid) open import Relation.Binary.PropositionalEquality using (_≡_; _≗_; refl; sym; module ≡-Reasoning; cong) open import Function.Bijection.Sets using (_RightInverseOf′_) open ≡-Reasoning using (begin_; _≡⟨_⟩_; _∎) open Setoidₛ using () renaming (refl to reflₛ; trans to transₛ) open import PiWare.Gates using (Gates) open import PiWare.Circuit using (ℂ; C; Plug; DelayLoop; _⟫_; ω) open import PiWare.Circuit.Algebra using (TyGate) open import PiWare.Plugs.Core using (eq⤪) open import PiWare.Semantics.Simulation A using (W; ⟦_⟧ω[_]; ⟦_⟧ᶜ[_]; W⟶W) \end{code} %<*vecCoerce> \AgdaTarget{vecCoerce} \begin{code} vecCoerce : ∀ {m n ℓ} {α : Set ℓ} → m ≡ n → Vec α m → Vec α n vecCoerce refl v = v \end{code} % %<*unfold-vecCoerce> \AgdaTarget{unfold-vecCoerce} \begin{code} unfold-vecCoerce : ∀ {m n ℓ} {α : Set ℓ} {≡₁ ≡₂} {x} {xs : Vec α m} → vecCoerce ≡₁ (x ∷ xs) ≡ x ∷ vecCoerce {n = n} ≡₂ xs unfold-vecCoerce {≡₁ = refl} {refl} = refl \end{code} % \begin{code} module _ {ℓ} {α : Set ℓ} {m} where private _↠_ = _RightInverseOf′_ {ℓ} {ℓ} {α = Vec α m} \end{code} %<*vecCoerce-rightInverse> \AgdaTarget{vecCoerce-rightInverse} \begin{code} vecCoerce-rightInverse : ∀ {n p} → vecCoerce (sym p) ↠ vecCoerce {n = n} p vecCoerce-rightInverse {p = refl} x = refl \end{code} % %<*eq⤨⫃[ᶜ]id> \AgdaTarget{eq⤨⫃[ᶜ]id} \begin{code} eq⤨⫃[ᶜ]id : ∀ {i o G} {g : TyGate G W⟶W} {p x⁰ x⁻} → ⟦ Plug {G} {i} {o} (eq⤪ p) ⟧ᶜ[ g ] (x⁰ ∷ x⁻) ≡ vecCoerce p x⁰ eq⤨⫃[ᶜ]id {p = refl} {x⁰} = begin tabulate (λ y → lookup (lookup y (allFin _)) x⁰) ≡⟨ tabulate-cong (λ z → cong (λ w → lookup w x⁰) (lookup-allFin z) ) ⟩ tabulate (flip lookup x⁰) ≡⟨ tabulate∘lookup x⁰ ⟩ x⁰ ∎ \end{code} % -- TODO: One property of plugs and one of identity plugs: plugs always comply with a function over only "now" (no dependency on past) -- For the special case of an identity plug, this function is the identity %<*eq⤨⫅[ᶜ]id∘head> \AgdaTarget{eq⤨⫅[ᶜ]id∘head} \begin{code} eq⤨⫅[ᶜ]id∘head : ∀ {i o G} {g : TyGate G W⟶W} {p x⁰⁻} → ⟦ Plug {G} {i} {o} (eq⤪ p) ⟧ᶜ[ g ] x⁰⁻ ≈ᵥ (id ∘ head) x⁰⁻ eq⤨⫅[ᶜ]id∘head {G = G} {g} {refl} {x⁰ ∷ x⁻} = from-≡ $eq⤨⫃[ᶜ]id {G = G} {g} {refl} {x⁰} {x⁻} \end{code} % %<*eq⤨⊑[runᶜ′]id> \AgdaTarget{eq⤨⊑[runᶜ′]id} \begin{code} eq⤨⊑[runᶜ′]id : ∀ {i o G} {g : TyGate G W⟶W} {p x⁰ x⁻ x⁺} → runᶜ′ ⟦ Plug {G} {i} {o} (eq⤪ p) ⟧ᶜ[ g ] (x⁰ ∷ x⁻) x⁺ ≈ₚ vecCoerce p x⁰ ∷ ♯ map (vecCoerce p) x⁺ eq⤨⊑[runᶜ′]id {G = G} {g} {p} {_} {x⁻} {x⁰ ∷ x⁺} = eq⤨⫃[ᶜ]id {G = G} {g} {p} {_} {x⁻} ∷ₚ ♯ transₚ (eq⤨⊑[runᶜ′]id {G = G} {g} {p}) (refl ∷ₚ ♯ reflₚ) \end{code} % %<*eq⤨⊑ωid> \AgdaTarget{eq⤨⊑ωid} \begin{code} eq⤨⊑ωid : ∀ {i o G} {g : TyGate G W⟶W} {p x⁰⁺} → ⟦ Plug {G} {i} {o} (eq⤪ p) ⟧ω[ g ] x⁰⁺ ≈ map (vecCoerce p) x⁰⁺ eq⤨⊑ωid {G = G} {g} {p} {x⁰ ∷ x⁺} = ≈ₚ-to-≈ (eq⤨⊑[runᶜ′]id {G = G} {g} {p}) ⟨ transₛ ⟩ refl ∷ ♯ reflₛ \end{code} %  ... ... @@ -20,7 +20,7 @@ open Setoidₛ using () renaming (refl to reflₛ; sym to symₛ; trans to trans open import Relation.Binary.PropositionalEquality using (_≡_; _≗_; refl; cong; module ≡-Reasoning) open ≡-Reasoning using (begin_; _≡⟨_⟩_; _∎) open import Data.CausalStream using (runᶜ′) open import Data.CausalStream using (runᶜ′; runᶜ-const) open import PiWare.Atomic.Bool using (Atomic-Bool) open import PiWare.Gates.BoolTrio using () renaming (BoolTrio to B₃) open import PiWare.Circuit using (ℂ; C; Plug; _⟫_; _∥_) ... ... @@ -32,7 +32,6 @@ open import PiWare.Semantics.Simulation.Properties.SequentialCongruence Atomic-B 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.Samples.BoolTrioSeq using (reg; proofReg-never; proofReg-always) open import PiWare.ProofSamples.EmptySeq using (runᶜ-const) open import Data.Serializable using (_⇕_; ⇕×) open import Data.Serializable.Bool using (⇕Bool) ... ...  ... ... @@ -3,7 +3,7 @@ module PiWare.Samples.RegN'Properties where open import Function using (_∘′_; flip) open import Coinduction using (♯_; ♭) open import Data.CausalStream using (runᶜ′) open import Data.CausalStream using (runᶜ′; runᶜ-const) open import Data.Stream using (Stream; take; drop; map; zipWith; _≈_; head-cong; _∷_) renaming (head to headₛ) open import Data.Stream.Equality.WithTrans using (_≈ₚ_; _∷ₚ_; ≈ₚ-to-≈; ≈-to-≈ₚ; reflₚ; transₚ) open import Data.Stream.Properties using (module Setoidₛ; module EqReasoningₛ; take-cong; drop-cong; drop-repeat) ... ... @@ -30,7 +30,6 @@ open import PiWare.Samples.BoolTrioSeq using (reg) open import PiWare.Samples.RegN using (p₁∘split1; p₂∘split1) 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.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) ... ...  ... ... @@ -36,10 +36,10 @@ open import PiWare.Samples.BoolTrioSeq using (reg) 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.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 () renaming (proof to proofSeq) open import PiWare.Samples.BoolTrioSeq using (proofReg-never; proofReg-always) open import PiWare.ProofSamples.EqPlug Atomic-Bool using (vecCoerce; unfold-vecCoerce; vecCoerce-rightInverse; eq⤨⊑ωid) open import Data.Serializable using (_⇕_; ⇕×) open import Data.Serializable.Bool using (⇕Bool) ... ...  ... ... @@ -4,30 +4,40 @@ open import PiWare.Atomic using (Atomic) module PiWare.Semantics.Simulation.Properties.Plugs (A : Atomic) where open import Function using (flip; _$_; _∘_; _∘′_; id; _⟨_⟩_) open import Coinduction using (♯_) open import Data.Fin using (Fin) open import Data.Nat.Base using (_+_) open import Data.Product using (_,_) 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 using (Vec; _∷_; lookup; tabulate; allFin; splitAt) renaming (map to mapᵥ) open import Data.Vec.Extra using (VecNaturalT) open import Data.Vec.Properties using (lookup-morphism; tabulate∘lookup; lookup∘tabulate; map-lookup-allFin; lookup-allFin) open import Data.Vec.Properties.Extra using (tabulate-cong; tabulate-ext) open import Data.Vec.Equality using () renaming (module PropositionalEquality to VPE) open VPE using (from-≡) open VPE using (from-≡) renaming (_≈_ to _≈ᵥ_) open import Data.List.NonEmpty using (_∷_; head) open import Relation.Binary.PropositionalEquality using (refl; _≡_; sym; cong; module ≡-Reasoning; _≗_) open import Function.Bijection.Sets using (_RightInverseOf′_) open ≡-Reasoning using (begin_; _∎; _≡⟨_⟩_; _≡⟨⟩_) open import Data.Stream using (_∷_; map; _≈_) open import Data.Stream.Properties using (module Setoidₛ) open Setoidₛ using () renaming (refl to reflₛ; trans to transₛ) open import Data.Stream.Equality.WithTrans using (_≈ₚ_; _∷ₚ_; ≈ₚ-to-≈; reflₚ; transₚ) open import Category.Functor.Extra using (app-NaturalT) open import Category.NaturalT using (NaturalT; _∘⇓_) open NaturalT using (op; op-<$>) open import Data.Vec.Extra using (VecNaturalT) open import Data.Vec.Properties.Extra using (tabulate-ext) open import PiWare.Circuit using (_⟫_; _∥_) open import Data.CausalStream using (runᶜ′) open import PiWare.Plugs.Core using (eq⤪) open import PiWare.Circuit using (_⟫_; _∥_; Plug) open import PiWare.Circuit.Algebra using (TyGate) open import PiWare.Plugs using (plug-Vecη; id⤨) open import PiWare.Semantics.Simulation A using (W; W⟶W; ⟦_⟧[_]) renaming (module WithGates to SimulationWithGates) open import PiWare.Semantics.Simulation A using (W; W⟶W; ⟦_⟧[_]; ⟦_⟧ᶜ[_]; ⟦_⟧ω[_]) renaming (module WithGates to SimulationWithGates) open import PiWare.Semantics.Simulation.Compliance A using (_⫅[_]_; _⫃[_]_) renaming (module WithGates to ComplianceWithGates) open import PiWare.Semantics.Simulation.Equality A using (_≅[_]_; _≋[_]_; ≅⇒≋; ≋-refl; ≋-trans) renaming (module WithGates to EqWithGates) \end{code} %<*flip-lookup> \AgdaTarget{lookupᵗ} \begin{code} ... ... @@ -43,10 +53,10 @@ lookupᵗ = flip lookup 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) _)) ⟩ tabulate (lookupᵗ (op η (map (lookupᵗ w) (allFin _)))) ≡⟨ tabulate∘lookup _ ⟩ op η (map (lookupᵗ w) (allFin _)) ≡⟨ cong (op η) (map-lookup-allFin _) ⟩ op η w ∎ tabulate (lookupᵗ (mapᵥ (lookupᵗ w) (op η (allFin _)))) ≡⟨ tabulate-ext (λ i → sym$ cong (lookup i) (op-<$> η (lookupᵗ w) _)) ⟩ tabulate (lookupᵗ (op η (mapᵥ (lookupᵗ w) (allFin _)))) ≡⟨ tabulate∘lookup _ ⟩ op η (mapᵥ (lookupᵗ w) (allFin _)) ≡⟨ cong (op η) (map-lookup-allFin _) ⟩ op η w ∎ \end{code} % ... ... @@ -312,3 +322,84 @@ module WithGates {G} (g : TyGate G W⟶W) where plugs-Vecη⁻¹ = plugs-Vecη⁻¹[ g ] \end{code} % %<*vecCoerce> \AgdaTarget{vecCoerce} \begin{code} vecCoerce : ∀ {m n ℓ} {α : Set ℓ} → m ≡ n → Vec α m → Vec α n vecCoerce refl v = v \end{code} % %<*unfold-vecCoerce> \AgdaTarget{unfold-vecCoerce} \begin{code} unfold-vecCoerce : ∀ {m n ℓ} {α : Set ℓ} {≡₁ ≡₂} {x} {xs : Vec α m} → vecCoerce ≡₁ (x ∷ xs) ≡ x ∷ vecCoerce {n = n} ≡₂ xs unfold-vecCoerce {≡₁ = refl} {refl} = refl \end{code} % \begin{code} module _ {ℓ} {α : Set ℓ} {m} where private _↠_ = _RightInverseOf′_ {ℓ} {ℓ} {α = Vec α m} \end{code} %<*vecCoerce-rightInverse> \AgdaTarget{vecCoerce-rightInverse} \begin{code} vecCoerce-rightInverse : ∀ {n p} → vecCoerce (sym p) ↠ vecCoerce {n = n} p vecCoerce-rightInverse {p = refl} x = refl \end{code} % %<*eq⤨⫃[ᶜ]id> \AgdaTarget{eq⤨⫃[ᶜ]id} \begin{code} eq⤨⫃[ᶜ]id : ∀ {i o G} {g : TyGate G W⟶W} {p x⁰ x⁻} → ⟦ Plug {G} {i} {o} (eq⤪ p) ⟧ᶜ[ g ] (x⁰ ∷ x⁻) ≡ vecCoerce p x⁰ eq⤨⫃[ᶜ]id {p = refl} {x⁰} = begin tabulate (λ y → lookup (lookup y (allFin _)) x⁰) ≡⟨ tabulate-cong (λ z → cong (λ w → lookup w x⁰) (lookup-allFin z) ) ⟩ tabulate (flip lookup x⁰) ≡⟨ tabulate∘lookup x⁰ ⟩ x⁰ ∎ \end{code} % -- TODO: One property of plugs and one of identity plugs: plugs always comply with a function over only "now" (no dependency on past) -- For the special case of an identity plug, this function is the identity %<*eq⤨⫅[ᶜ]id∘head> \AgdaTarget{eq⤨⫅[ᶜ]id∘head} \begin{code} eq⤨⫅[ᶜ]id∘head : ∀ {i o G} {g : TyGate G W⟶W} {p x⁰⁻} → ⟦ Plug {G} {i} {o} (eq⤪ p) ⟧ᶜ[ g ] x⁰⁻ ≈ᵥ (id ∘ head) x⁰⁻ eq⤨⫅[ᶜ]id∘head {G = G} {g} {refl} {x⁰ ∷ x⁻} = from-≡$ eq⤨⫃[ᶜ]id {G = G} {g} {refl} {x⁰} {x⁻} \end{code} % %<*eq⤨⊑[runᶜ′]id> \AgdaTarget{eq⤨⊑[runᶜ′]id} \begin{code} eq⤨⊑[runᶜ′]id : ∀ {i o G} {g : TyGate G W⟶W} {p x⁰ x⁻ x⁺} → runᶜ′ ⟦ Plug {G} {i} {o} (eq⤪ p) ⟧ᶜ[ g ] (x⁰ ∷ x⁻) x⁺ ≈ₚ vecCoerce p x⁰ ∷ ♯ map (vecCoerce p) x⁺ eq⤨⊑[runᶜ′]id {G = G} {g} {p} {_} {x⁻} {x⁰ ∷ x⁺} = eq⤨⫃[ᶜ]id {G = G} {g} {p} {_} {x⁻} ∷ₚ ♯ transₚ (eq⤨⊑[runᶜ′]id {G = G} {g} {p}) (refl ∷ₚ ♯ reflₚ) \end{code} % %<*eq⤨⊑ωid> \AgdaTarget{eq⤨⊑ωid} \begin{code} eq⤨⊑ωid : ∀ {i o G} {g : TyGate G W⟶W} {p x⁰⁺} → ⟦ Plug {G} {i} {o} (eq⤪ p) ⟧ω[ g ] x⁰⁺ ≈ map (vecCoerce p) x⁰⁺ eq⤨⊑ωid {G = G} {g} {p} {x⁰ ∷ x⁺} = ≈ₚ-to-≈ (eq⤨⊑[runᶜ′]id {G = G} {g} {p}) ⟨ transₛ ⟩ refl ∷ ♯ reflₛ \end{code} %
 ... ... @@ -64,9 +64,6 @@ import PiWare.Patterns import PiWare.Plugs.Core import PiWare.Plugs import PiWare.ProofSamples.EmptySeq -- M import PiWare.ProofSamples.EqPlug -- M import PiWare.Samples.BoolTrioComb import PiWare.Samples.BoolTrioSeq import PiWare.Samples.Muxes ... ...
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!