proofReg-*-plain → proofReg-*, proofReg-* → proofReg-*-typed

parent f9409386
\begin{code}
module PiWare.Samples.BoolTrioSeq where
open import Function using (_$_; _⟨_⟩_; _∘_)
open import Function using (_$_; _⟨_⟩_; _∘_; _∘′_; id)
open import Coinduction using (♯_; ♭)
open import Data.Unit.Base using (⊤; tt)
open import Data.Nat.Base using (_+_)
......@@ -11,12 +11,13 @@ open import Data.List using ([]; _∷_)
open import Data.List.All using (All; _∷_; [])
open import Data.List.NonEmpty using (_∷_) renaming ([_] to [_]⁺)
open import Data.Bool.Base using (Bool; not) renaming (false to 𝔽; true to 𝕋)
open import Data.Vec using (Vec; _++_; []; _∷_; [_]; lookup)
open import Data.Stream using (Stream; _∷_; repeat; take; iterate; tail; _≈_; map)
open import Data.Vec using (Vec; _++_; []; _∷_; [_]; lookup; head)
open import Data.Stream using (Stream; _∷_; repeat; take; iterate; tail; _≈_; map; zipWith)
open import Data.Stream.Extra using (zip)
open import Data.Stream.Properties using (≡-to-≈; module Setoidₛ)
open import Data.Stream.Properties using (≡-to-≈; module Setoidₛ; module EqReasoningₛ; map-repeat; map-compose; map-cong-fun; map-id)
open import Data.Stream.Equality.WithTrans using (_≈ₚ_; _∷ₚ_; ≈ₚ-to-≈; reflₚ; transₚ)
open Setoidₛ using () renaming (refl to reflₛ; sym to symₛ; trans to transₛ)
open EqReasoningₛ using (_≈⟨_⟩_) renaming (begin_ to beginₛ_; _∎ to _∎ₛ)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; inspect; cong) renaming ([_] to [_]ᵣ)
open import Data.CausalStream using (runᶜ′)
......@@ -26,11 +27,12 @@ open import PiWare.Circuit using (Plug; DelayLoop; _⟫_) renaming (module WithG
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 Atomic-Bool using (module WithGates; delay′)
open import PiWare.Semantics.Simulation.BoolTrio using () renaming (spec to spec-B₃)
open WithGates spec-B₃ using (⟦_⟧ω; ⟦_⟧ᶜ; ⟦_⟧)
open import PiWare.Semantics.SimulationState Atomic-Bool using (mealy; ⟦_⟧ₛ[_]; DelayLoopₛ; Plugₛ; Gateₛ; _⟫ₛ_; ⟦_⟧ω'[_]) renaming (module WithGates to WithGatesₛ)
open WithGatesₛ spec-B₃ using (⟦_⟧ₛ; ⟦_⟧ω'; ℂₛ)
open import PiWare.Semantics.Simulation Atomic-Bool using (module WithGates; delay′; W)
open import PiWare.Semantics.Simulation.BoolTrio using () renaming (spec to b₃)
open WithGates b₃ using (⟦_⟧; ⟦_⟧ᶜ; ⟦_⟧ω)
open import PiWare.Semantics.SimulationState Atomic-Bool using (mealy; DelayLoopₛ; Plugₛ; Gateₛ; _⟫ₛ_) renaming (module WithGates to WithGatesₛ)
open WithGatesₛ b₃ using (⟦_⟧ₛ; ⟦_⟧ω'; ℂₛ)
open import PiWare.Semantics.Simulation.Properties.Sequential Atomic-Bool using (⟦⟧ω[–]-cong)
open import PiWare.Samples.BoolTrioComb using (¬ℂ; ⊥ℂ; ∨ℂ)
open import PiWare.Samples.Muxes using (mux)
......@@ -38,6 +40,7 @@ open import Data.Serializable using (_⇕_; ⇕⊤; ⇕×)
open import Data.Serializable.Bool using (⇕Bool)
open _⇕_ ⇕Bool
open _⇕_ {⊤} {Bool} ⇕⊤ using () renaming (⇓ to ⇓⊤)
open _⇕_ ⇕Bool using () renaming (⇑ to ⇑¹; ⇓ to ⇓¹)
open _⇕_ (⇕× ⦃ ⇕Bool ⦄ ⦃ ⇕Bool ⦄) using () renaming (⇓ to ⇓²)
\end{code}
......@@ -277,12 +280,12 @@ reg-runᶜ′-never {d⁰} {x⁺ = _ ∷ _} p rewrite regᶜ-never {d⁰} p = re
\end{code}
%</reg-runᶜ′-never>
%<*proofReg-never>
%<*proofReg-never-typed>
\begin{code}
proofReg-never : ∀ {xs} → ⟦ reg ⟧ω (map ⇓² (xs ⟨ zip ⟩ repeat 𝔽)) ≈ map ⇓ (repeat 𝔽)
proofReg-never {_ ∷ _} = reg-runᶜ′-never []
proofReg-never-typed : ∀ {xs} → ⟦ reg ⟧ω (map ⇓² (xs ⟨ zip ⟩ repeat 𝔽)) ≈ map ⇓ (repeat 𝔽)
proofReg-never-typed {_ ∷ _} = reg-runᶜ′-never []
\end{code}
%</proofReg-never>
%</proofReg-never-typed>
%<*reg-runᶜ′-always>
......@@ -293,46 +296,68 @@ reg-runᶜ′-always {x⁻ = _ ∷ _} {x⁺ = _ ∷ _} = refl ∷ₚ ♯ trans
\end{code}
%</reg-runᶜ′-always>
%<*proofReg-always>
%<*proofReg-always-typed>
\begin{code}
proofReg-always : ∀ {xs} → ⟦ reg ⟧ω (map ⇓² (xs ⟨ zip ⟩ repeat 𝕋)) ≈ map ⇓ xs
proofReg-always {x ∷ xs} = ≈ₚ-to-≈ $ transₚ reg-runᶜ′-always (refl ∷ₚ ♯ reflₚ)
proofReg-always-typed : ∀ {xs} → ⟦ reg ⟧ω (map ⇓² (xs ⟨ zip ⟩ repeat 𝕋)) ≈ map ⇓ xs
proofReg-always-typed {x ∷ xs} = ≈ₚ-to-≈ $ transₚ reg-runᶜ′-always (refl ∷ₚ ♯ reflₚ)
\end{code}
%</proofReg-always>
%</proofReg-always-typed>
-- Typed stuff should be moved
proofShift̂ : ∀ {ins} → ⟦ shift̂ ⟧ω̂ (♭ ins) ≈ 𝔽 ∷ ins
proofShift̂ {ins} with ♭ ins | inspect ♭ ins
proofShift̂ | x ∷ xs | [ inseq ] with ♭ xs | proofShiftHead̂ {x ∷ xs} | proofShiftTail̂ {x ∷ xs}
proofShift̂ | x ∷ xs | [ inseq ] | x₁ ∷ xs₁ | p1 | p2 = p1 ∷ (♯ strans p2 (ssym (≡-to-≈ inseq)))
proofShiftTail̂ : ∀ {ins} → tail (⟦ shift̂ ⟧ω̂ ins) ≈ ins
proofShiftTail̂ {ins} = liftProof {α̂ = ⇕Bool} {β̂ = ⇕Bool} {f = shift} {xs = ins}
(λ {_} {_} {_} {s} → (tail-map-swap {s = s}))
(λ x → refl)
proofShiftTail
-- TODO: this holds for any serializable product
%<*map⇓²-zip-map⇑¹-repeat>
\AgdaTarget{map⇓²-zip-map⇑¹-repeat}
\begin{code}
map⇓²-zip-map⇑¹-repeat : ∀ {xs y} → zipWith _++_ xs (repeat [ y ]) ≈ map ⇓² (zip (map ⇑¹ xs) (repeat y))
map⇓²-zip-map⇑¹-repeat {x ∷ _} {y} = append-headCons x ∷ ♯ map⇓²-zip-map⇑¹-repeat
where append-headCons : ∀ (z : W 1) → z ++ [ y ] ≡ (head z) ∷ [ y ]
append-headCons (_ ∷ []) = refl
\end{code}
%</map⇓²-zip-map⇑¹-repeat>
proofShiftHead̂ : ∀ {ins} → head (⟦ shift̂ ⟧ω̂ ins) ≡ 𝔽
proofShiftHead̂ {_ ∷ xs} with ♭ xs
proofShiftHead̂ {_ ∷ _ } | _ ∷ _ = refl
%<*proofReg-never>
\AgdaTarget{proofReg-never}
\begin{code}
proofReg-never : ∀ {xs} → ⟦ reg ⟧ω (zipWith _++_ xs (repeat [ 𝔽 ])) ≈ repeat [ 𝔽 ]
proofReg-never {xs} = beginₛ
⟦ reg ⟧ω (zipWith _++_ xs (repeat [ 𝔽 ]))
≈⟨ ⟦⟧ω[–]-cong b₃ reg (map⇓²-zip-map⇑¹-repeat {xs = xs}) ⟩
⟦ reg ⟧ω (map ⇓² (zipWith _,_ (map ⇑¹ xs) (repeat 𝔽)))
≈⟨ proofReg-never-typed {xs = map ⇑¹ xs} ⟩
map ⇓¹ (repeat 𝔽)
≈⟨ map-repeat ⟩
repeat [ 𝔽 ] ∎ₛ
\end{code}
%</proofReg-never>
proofTogglê : ⟦ togglê ⟧ω̂ (repeat tt) ≈ iterate not 𝕋
proofTogglê = map-cong ⇑ proofToggle ⟨ transₛ ⟩ symₛ map-compose ⟨ transₛ ⟩ map-id
proofReĝAlwaysLoad : ∀ {xs} → ⟦ reĝ ⟧ω̂ (zipWith _,_ xs (repeat 𝕋)) ≈ xs
proofReĝAlwaysLoad {xs} = liftProof {p = id} {α̂ = ⇕Bool²} {β̂ = ⇕Bool} {f = reg} {xs = zipWith _,_ xs (repeat 𝕋)}
(λ {_} {_} {f} {s} → ssym (id-swap {f = map f} {s = s}))
(λ x → refl)
-- TODO: move to Data.Vec.Properties.Extra
%<*head∘[x]-involutive-Vec1>
\AgdaTarget{head∘[x]-involutive-Vec1}
\begin{code}
head∘[x]-involutive-Vec1 : ∀ {ℓ} {α : Set ℓ} (xs : Vec α 1) → [_] (head xs) ≡ xs
head∘[x]-involutive-Vec1 (x ∷ []) = refl
\end{code}
%</head∘[x]-involutive-Vec1>
proofReĝNeverLoad : ∀ {xs} → ⟦ reĝ ⟧ω̂ (zipWith P._,_ xs (repeat 𝔽)) ≈ repeat 𝔽
proofReĝNeverLoad {xs} = liftProof {p = id} {α̂ = ⇕Bool²} {β̂ = ⇕Bool} {f = reg} {xs = zipWith P._,_ xs (repeat 𝔽)}
(λ {_} {_} {f} {s} → ssym (id-swap {f = map f} {s = s}))
(λ x → refl)
(proofRegNeverLoad {xs = xs})
%<*proofReg-always>
\AgdaTarget{proofReg-always}
\begin{code}
proofReg-always : ∀ {xs} → ⟦ reg ⟧ω (zipWith _++_ xs (repeat [ 𝕋 ])) ≈ xs
proofReg-always {xs} = beginₛ
⟦ reg ⟧ω (zipWith _++_ xs (repeat [ 𝕋 ]))
≈⟨ ⟦⟧ω[–]-cong b₃ reg (map⇓²-zip-map⇑¹-repeat {xs = xs}) ⟩
⟦ reg ⟧ω (map ⇓² (zipWith _,_ (map ⇑¹ xs) (repeat 𝕋)))
≈⟨ proofReg-always-typed {xs = map ⇑¹ xs} ⟩
map ⇓¹ (map ⇑¹ xs)
≈⟨ symₛ map-compose ⟩
map (⇓¹ ∘′ ⇑¹) xs
≈⟨ map-cong-fun head∘[x]-involutive-Vec1 ⟩
map id xs
≈⟨ map-id ⟩
xs ∎ₛ
\end{code}
%</proofReg-always>
\begin{code}
module PiWare.Samples.RegN' where
open import Function using (_∘′_; id; flip; _$_)
open import Function using (_∘′_; flip; _$_)
open import Coinduction using (♯_)
open import Data.Fin using (#_; raise) renaming (suc to Fs)
open import Data.Bool.Base using (Bool) renaming (false to 𝔽; true to 𝕋)
open import Data.Nat.Base using (ℕ; zero; suc; _+_)
open import Data.Product using (_,_; proj₁; proj₂)
open import Data.List.NonEmpty using (_∷_)
open import Data.Vec using (Vec; []; _∷_; _++_; [_]; head; tabulate; lookup; splitAt; replicate)
open import Data.Vec using (Vec; []; _∷_; _++_; [_]; tabulate; lookup; splitAt; replicate)
open import Data.Vec.Properties using (lookup∘tabulate; tabulate∘lookup)
open import Data.Vec.Extra using (splitAt′)
open import Data.Vec.Properties.Extra using (tabulate-cong)
open import Data.Stream using (Stream; _∷_; zipWith; repeat; _≈_; map; zipWith-cong)
open import Data.Stream.Extra using (zip)
open import Data.Stream.Properties using (module EqReasoningₛ; module Setoidₛ; map-repeat; map-compose; map-cong-fun; map-id)
open import Data.Stream.Properties using (module EqReasoningₛ; module Setoidₛ)
open import Data.Stream.Equality.WithTrans using (_≈ₚ_; _∷ₚ_; transₚ; reflₚ; ≈ₚ-to-≈)
open EqReasoningₛ using (_≈⟨_⟩_) renaming (begin_ to beginₛ_; _∎ to _∎ₛ)
open Setoidₛ using () renaming (refl to reflₛ; sym to symₛ; trans to transₛ)
open import Relation.Binary.PropositionalEquality using (_≡_; _≗_; refl; cong; module ≡-Reasoning)
open Setoidₛ using () renaming (refl to reflₛ; trans to transₛ)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; module ≡-Reasoning)
open ≡-Reasoning using (begin_; _≡⟨_⟩_; _∎)
open import Data.CausalStream using (runᶜ′; runᶜ-const)
......@@ -27,16 +26,11 @@ open import PiWare.Gates.BoolTrio using (BoolTrio)
open CircuitWithGates BoolTrio using (ℂ; C)
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 Atomic-Bool using (module WithGates)
open import PiWare.Semantics.Simulation.BoolTrio using () renaming (spec to b₃)
open WithGates b₃ 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 (_⇕_; ⇕×)
open import Data.Serializable.Bool using (⇕Bool)
open _⇕_ ⇕Bool using () renaming (⇑ to ⇑¹; ⇓ to ⇓¹)
open _⇕_ (⇕× ⦃ ⇕Bool ⦄ ⦃ ⇕Bool ⦄) using () renaming (⇓ to ⇓²)
\end{code}
......@@ -64,64 +58,6 @@ regn (suc n) = regn-plug {n} ⟫ (reg ∥ regn n)
-- TODO: this holds for any serializable product
%<*map⇓²-zip-map⇑¹-repeat>
\AgdaTarget{map⇓²-zip-map⇑¹-repeat}
\begin{code}
map⇓²-zip-map⇑¹-repeat : ∀ {xs y} → zipWith _++_ xs (repeat [ y ]) ≈ map ⇓² (zip (map ⇑¹ xs) (repeat y))
map⇓²-zip-map⇑¹-repeat {x ∷ _} {y} = append-headCons x ∷ ♯ map⇓²-zip-map⇑¹-repeat
where append-headCons : ∀ (z : W 1) → z ++ [ y ] ≡ (head z) ∷ [ y ]
append-headCons (_ ∷ []) = refl
\end{code}
%</map⇓²-zip-map⇑¹-repeat>
%<*proofReg-never-plain>
\AgdaTarget{proofReg-never-plain}
\begin{code}
proofReg-never-plain : ∀ {xs} → ⟦ reg ⟧ω (zipWith _++_ xs (repeat [ 𝔽 ])) ≈ repeat [ 𝔽 ]
proofReg-never-plain {xs} = beginₛ
⟦ reg ⟧ω (zipWith _++_ xs (repeat [ 𝔽 ]))
≈⟨ ⟦⟧ω[–]-cong b₃ reg (map⇓²-zip-map⇑¹-repeat {xs = xs}) ⟩
⟦ reg ⟧ω (map ⇓² (zipWith _,_ (map ⇑¹ xs) (repeat 𝔽)))
≈⟨ proofReg-never {xs = map ⇑¹ xs} ⟩
map ⇓¹ (repeat 𝔽)
≈⟨ map-repeat ⟩
repeat [ 𝔽 ] ∎ₛ
\end{code}
%</proofReg-never-plain>
-- TODO: move to Data.Vec.Properties.Extra
%<*head∘[x]-involutive-Vec1>
\AgdaTarget{head∘[x]-involutive-Vec1}
\begin{code}
head∘[x]-involutive-Vec1 : ∀ {ℓ} {α : Set ℓ} (xs : Vec α 1) → [_] (head xs) ≡ xs
head∘[x]-involutive-Vec1 (x ∷ []) = refl
\end{code}
%</head∘[x]-involutive-Vec1>
%<*proofReg-always-plain>
\AgdaTarget{proofReg-always-plain}
\begin{code}
proofReg-always-plain : ∀ {xs} → ⟦ reg ⟧ω (zipWith _++_ xs (repeat [ 𝕋 ])) ≈ xs
proofReg-always-plain {xs} = beginₛ
⟦ reg ⟧ω (zipWith _++_ xs (repeat [ 𝕋 ]))
≈⟨ ⟦⟧ω[–]-cong b₃ reg (map⇓²-zip-map⇑¹-repeat {xs = xs}) ⟩
⟦ reg ⟧ω (map ⇓² (zipWith _,_ (map ⇑¹ xs) (repeat 𝕋)))
≈⟨ proofReg-always {xs = map ⇑¹ xs} ⟩
map ⇓¹ (map ⇑¹ xs)
≈⟨ symₛ map-compose ⟩
map (⇓¹ ∘′ ⇑¹) xs
≈⟨ map-cong-fun head∘[x]-involutive-Vec1 ⟩
map id xs
≈⟨ map-id ⟩
xs ∎ₛ
\end{code}
%</proofReg-always-plain>
-- TODO: move?
%<*regn-plug-tabulates-lookups>
\AgdaTarget{regn-plug-tabulates-lookups}
......@@ -186,7 +122,7 @@ proofRegN-never {suc n} {xs} = beginₛ
⟦ reg ∥ regn n ⟧ω (zipWith _++_ (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-cong _++_ (proofReg-never {map (proj₁ ∘′ splitAt′ 1) xs}) (proofRegN-never {n} {map (proj₂ ∘′ splitAt′ 1) xs}) ⟩
zipWith _++_ (repeat [ 𝔽 ]) (repeat (replicate 𝔽))
≈⟨ regN-never-data𝔽 {n} ⟩
repeat (replicate 𝔽) ∎ₛ
......@@ -228,7 +164,7 @@ proofRegN-always {suc n} {xs} = beginₛ
⟦ reg ∥ regn n ⟧ω (zipWith _++_ (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-always-plain {xs = map (proj₁ ∘′ splitAt′ 1) xs}) (proofRegN-always {n = n} {xs = map (proj₂ ∘′ splitAt′ 1) xs}) ⟩
≈⟨ zipWith-cong _++_ (proofReg-always {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)
≈⟨ zipWith++-map-splitAt ⟩
xs ∎ₛ
......
......@@ -37,7 +37,7 @@ 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.Sequential Atomic-Bool using (⟦⟧ω[–]-cong; ⟦⟧ω[–]-⟫⇒∘)
open import PiWare.Samples.BoolTrioSeq using (proofReg-never; proofReg-always)
open import PiWare.Samples.BoolTrioSeq using (proofReg-never-typed; proofReg-always-typed)
open import Data.Serializable using (_⇕_; ⇕×)
open import Data.Serializable.Bool using (⇕Bool)
......@@ -285,7 +285,7 @@ zipWith-++-⇑ {x ∷ _} {y} = reduce x ∷ ♯ zipWith-++-⇑
proofReg-never-plain : ∀ {xs} → ⟦ reg ⟧ω (zipWith _++_ xs (repeat [ 𝔽 ])) ≈ repeat [ 𝔽 ]
proofReg-never-plain {xs} = beginₛ
⟦ reg ⟧ω (zipWith _++_ xs (repeat [ 𝔽 ])) ≈⟨ ⟦⟧ω[–]-cong b₃ reg (zipWith-++-⇑ {xs}) ⟩
⟦ reg ⟧ω (map ⇓² (zipWith _,_ (map ⇑ xs) (repeat 𝔽))) ≈⟨ proofReg-never {xs = map ⇑ xs} ⟩
⟦ reg ⟧ω (map ⇓² (zipWith _,_ (map ⇑ xs) (repeat 𝔽))) ≈⟨ proofReg-never-typed {xs = map ⇑ xs} ⟩
map ⇓ (repeat 𝔽) ≈⟨ map-repeat ⟩
repeat [ 𝔽 ] ∎ₛ
\end{code}
......@@ -298,7 +298,7 @@ proofReg-never-plain {xs} = beginₛ
proofReg-always-plain : ∀ {xs} → ⟦ reg ⟧ω (zipWith _++_ xs (repeat [ 𝕋 ])) ≈ xs
proofReg-always-plain {xs} = beginₛ
⟦ reg ⟧ω (zipWith _++_ xs (repeat [ 𝕋 ])) ≈⟨ ⟦⟧ω[–]-cong b₃ reg (zipWith-++-⇑ {xs}) ⟩
⟦ reg ⟧ω (map ⇓² (zipWith _,_ (map ⇑ xs) (repeat 𝕋))) ≈⟨ proofReg-always {map ⇑ xs} ⟩
⟦ reg ⟧ω (map ⇓² (zipWith _,_ (map ⇑ xs) (repeat 𝕋))) ≈⟨ proofReg-always-typed {map ⇑ xs} ⟩
map ⇓ (map ⇑ xs) ≈⟨ symₛ map-compose ⟩
map (⇓ ∘′ ⇑) xs ≈⟨ map-cong-fun singleton∘head ⟩
map id xs ≈⟨ map-id ⟩
......
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