Finish ProofSamples/B3Seq

parent 2156a844
......@@ -7,7 +7,7 @@ open import Data.Bool.Base using (Bool; not) renaming (false to 𝔽; true to
open import Coinduction using (♯_; ♭)
open import Data.Fin using (#_)
open import Data.List using ([]; _∷_)
open import Data.List.NonEmpty using (_∷_)
open import Data.List.NonEmpty using (_∷_) renaming ([_] to [_]⁺)
open import Data.List.All using (All; _∷_; [])
open import Data.Product using (∃; _,_)
open import Data.Vec using (Vec; lookup; _++_; [_]; _∷_; [])
......@@ -24,187 +24,192 @@ open import PiWare.Semantics.Simulation Atomic-Bool using (delay′; module With
open import PiWare.Semantics.Simulation.BoolTrio using () renaming (spec to spec-B₃)
open WithGates spec-B₃ using (⟦_⟧ω; ⟦_⟧ᶜ; ⟦_⟧)
open import PiWare.Samples.BoolTrioSeq using (toggle; shift; reg; regCore)
open import PiWare.Typed.Semantics.Simulation Atomic-Bool using () renaming (module WithGates to TypedWithGates)
open TypedWithGates spec-B₃ using (⟦_⟧ω̂)
open import PiWare.Typed.Samples.BoolTrioSeq using (togglê; shift̂; reĝ)
open import Data.Serializable using (_⇕_; ⇕⊤; ⇕×)
open import Data.Serializable.Bool using (⇕Bool)
\end{code}
\begin{code}
open _⇕_ ⇕Bool
open _⇕_ {⊤} {Bool} ⇕⊤ using () renaming (⇓ to ⇓⊤; ⇑ to ⇑⊤)
open _⇕_ {⊤} {Bool} ⇕⊤ using () renaming (⇓ to ⇓⊤)
open _⇕_ (⇕× ⦃ ⇕Bool ⦄ ⦃ ⇕Bool ⦄) using () renaming (⇓ to ⇓²)
\end{code}
\begin{code}
proofShiftHead : ∀ {ins} → head (⟦ shift ⟧ω ins) ≡ [ 𝔽 ]
proofShiftHead {(_ ∷ []) ∷ xs} with ♭ xs
proofShiftHead {(_ ∷ []) ∷ _} | _ ∷ _ = refl
%<*lookup#1-singletons>
\begin{code}
lookup#1-singletons : ∀ {ℓ} {α : Set ℓ} {a b c : Vec α 1} → [ lookup (# 1) (a ++ [ lookup (# 0) (b ++ c) ]) ] ≡ b
lookup#1-singletons {a = _ ∷ []} {_ ∷ []} = refl
\end{code}
%</lookup#1-singletons>
proofShift : ∀ {x⁻ x⁻¹ x⁰ x⁺} → runᶜ′ ⟦ shift ⟧ᶜ (x⁰ ∷ x⁻¹ ∷ x⁻) x⁺ ≈ₚ x⁻¹ ∷ ♯ (x⁰ ∷ ♯ x⁺)
proofShift {[]} {x⁻¹} {x⁰} {x¹ ∷ x⁺} =
lookup#1-singletons {a = x⁰} {x⁻¹} ∷ₚ ♯ transₚ (proofShift {x⁻¹ ∷ []} {x⁰} {x¹} {♭ x⁺}) (refl ∷ₚ ♯ (refl ∷ₚ ♯ reflₚ))
%<*shift-runᶜ′>
\begin{code}
shift-runᶜ′ : ∀ {x⁻ x⁻¹ x⁰ x⁺} → runᶜ′ ⟦ shift ⟧ᶜ (x⁰ ∷ x⁻¹ ∷ x⁻) x⁺ ≈ₚ x⁻¹ ∷ ♯ (x⁰ ∷ ♯ x⁺)
shift-runᶜ′ {[]} {x⁻¹} {x⁰} {x¹ ∷ x⁺} =
lookup#1-singletons {a = x⁰} {x⁻¹} ∷ₚ ♯ transₚ (shift-runᶜ′ {x⁻¹ ∷ []} {x⁰} {x¹} {♭ x⁺}) (refl ∷ₚ ♯ (refl ∷ₚ ♯ reflₚ))
shift-runᶜ′ {x⁻² ∷ x⁻} {x⁻¹} {x⁰} {x¹ ∷ x⁺} =
lookup#1-singletons {a = x⁰} {x⁻¹} ∷ₚ ♯ transₚ (shift-runᶜ′ {x⁻¹ ∷ x⁻² ∷ x⁻} {x⁰} {x¹} {♭ x⁺}) (refl ∷ₚ ♯ (refl ∷ₚ ♯ reflₚ))
\end{code}
%</shift-runᶜ′>
proofShift {x⁻² ∷ x⁻} {x⁻¹} {x⁰} {x¹ ∷ x⁺} = lookup#1-singletons {a = x⁰} {x⁻¹} ∷ₚ ♯
transₚ (proofShift {x⁻¹ ∷ x⁻² ∷ x⁻} {x⁰} {x¹} {♭ x⁺}) (refl ∷ₚ ♯ (refl ∷ₚ ♯ reflₚ))
%<*proofShift-tail>
\begin{code}
proofShift-tail : ∀ {xs} → tail (⟦ shift ⟧ω xs) ≈ xs
proofShift-tail {_ ∷ x⁺} with ♭ x⁺ | inspect ♭ x⁺
proofShift-tail {_ ∷ _} | _ ∷ _ | [ xseq ]ᵣ = transₛ (≈ₚ-to-≈ shift-runᶜ′)
(refl ∷ ♯ transₛ (refl ∷ ♯ reflₛ) (symₛ (≡-to-≈ xseq)))
\end{code}
%</proofShift-tail>
proofShiftTail : ∀ {ins} → tail (⟦ shift ⟧ω ins) ≈ ins
proofShiftTail {_ ∷ x⁺} with ♭ x⁺ | inspect ♭ x⁺
proofShiftTail {x⁰ ∷ x⁺} | x¹ ∷ x²⁺ | [ xseq ]ᵣ = transₛ (≈ₚ-to-≈ proofShift) (refl ∷ ♯ transₛ (refl ∷ ♯ reflₛ) (symₛ (≡-to-≈ xseq)))
%<*proofShift-head>
\begin{code}
proofShift-head : ∀ {xs} → head (⟦ shift ⟧ω xs) ≡ [ 𝔽 ]
proofShift-head {(_ ∷ []) ∷ x⁺} with ♭ x⁺
proofShift-head {(_ ∷ []) ∷ _} | _ ∷ _ = refl
\end{code}
%</proofShift-head>
proofToggleᶜ-t⁰ : ∀ {x⁰} → ⟦ toggle ⟧ᶜ (x⁰ ∷ []) ≡ [ 𝕋 ]
proofToggleᶜ-t⁰ = refl
[_]-injective : ∀ {ℓ} {α : Set ℓ} {x y : α} → [ x ] ≡ [ y ] → x ≡ y
[ refl ]-injective = refl
%<*toggleᶜ-start>
\begin{code}
toggleᶜ-start : ∀ {x⁰} → ⟦ toggle ⟧ᶜ [ x⁰ ]⁺ ≡ [ 𝕋 ]
toggleᶜ-start = refl
\end{code}
%</toggleᶜ-start>
%<*[_]-injective>
\begin{code}
[_]-injective : ∀ {ℓ} {α : Set ℓ} {x y : α} → [ x ] ≡ [ y ] → x ≡ y
[_]-injective refl = refl
\end{code}
%</[_]-injective>
%<*toggleᶜ-𝔽⇒𝕋>
\begin{code}
toggleᶜ-𝔽⇒𝕋 : ∀ {x⁻ x⁻¹ x⁰} → ⟦ toggle ⟧ᶜ (x⁻¹ ∷ x⁻) ≡ ⇓ 𝔽 → ⟦ toggle ⟧ᶜ (x⁰ ∷ x⁻¹ ∷ x⁻) ≡ ⇓ 𝕋
toggleᶜ-𝔽⇒𝕋 {[]} ()
toggleᶜ-𝔽⇒𝕋 {_ ∷ _} p = cong ([_] ∘ not) ([_]-injective p)
\end{code}
%</toggleᶜ-𝔽⇒𝕋>
%<*toggleᶜ-𝕋⇒𝔽>
\begin{code}
toggleᶜ-𝕋⇒𝔽 : ∀ {x⁻ x⁻¹ x⁰} → ⟦ toggle ⟧ᶜ (x⁻¹ ∷ x⁻) ≡ ⇓ 𝕋 → ⟦ toggle ⟧ᶜ (x⁰ ∷ x⁻¹ ∷ x⁻) ≡ ⇓ 𝔽
toggleᶜ-𝕋⇒𝔽 {[]} _ = refl
toggleᶜ-𝕋⇒𝔽 {_ ∷ _} p = cong ([_] ∘ not) [ p ]-injective
toggleᶜ-𝕋⇒𝔽 {_ ∷ _} p = cong ([_] ∘ not) ([_]-injective p)
\end{code}
%</toggleᶜ-𝕋⇒𝔽>
%<*toggle-runᶜ′-𝕋-𝔽-types>
\begin{code}
toggle-runᶜ′-𝕋 : ∀ {x⁻ x⁰ x⁺} → ⟦ toggle ⟧ᶜ (x⁰ ∷ x⁻) ≡ ⇓ 𝕋 → runᶜ′ ⟦ toggle ⟧ᶜ (x⁰ ∷ x⁻) x⁺ ≈ map ⇓ (iterate not 𝕋)
toggle-runᶜ′-𝔽 : ∀ {x⁻ x⁰ x⁺} → ⟦ toggle ⟧ᶜ (x⁰ ∷ x⁻) ≡ ⇓ 𝔽 → runᶜ′ ⟦ toggle ⟧ᶜ (x⁰ ∷ x⁻) x⁺ ≈ map ⇓ (iterate not 𝔽)
\end{code}
%</toggle-runᶜ′-𝕋-𝔽-types>
%<*toggle-runᶜ′-𝕋-𝔽-defs>
\begin{code}
toggle-runᶜ′-𝕋 {x⁻} {x⁰} {x¹ ∷ _} p = p ∷ ♯ toggle-runᶜ′-𝔽 (toggleᶜ-𝕋⇒𝔽 {x⁻} {x⁰} {x¹} p)
toggle-runᶜ′-𝔽 {x⁻} {x⁰} {x¹ ∷ _} p = p ∷ ♯ toggle-runᶜ′-𝕋 (toggleᶜ-𝔽⇒𝕋 {x⁻} {x⁰} {x¹} p)
\end{code}
%</toggle-runᶜ′-𝕋-𝔽-defs>
%<*proofToggle>
\begin{code}
proofToggle : ⟦ toggle ⟧ω (map ⇓⊤ (repeat tt)) ≈ map ⇓ (iterate not 𝕋)
proofToggle = toggle-runᶜ′-𝕋 (proofToggleᶜ-t⁰ {[]})
-- TODO: remove typed stuff from here
proofTogglê : ⟦ togglê ⟧ω̂ (repeat tt) ≈ iterate not 𝕋
proofTogglê = map-cong ⇑ proofToggle ⟨ transₛ ⟩ symₛ map-compose ⟨ transₛ ⟩ map-id
lemma''RegNeverLoadHardcoded : ∀ {cs} → All (⇓² (𝕋 , 𝔽) ≡_) cs → delay′ 1 {i = 2} ⟦ regCore ⟧ (⇓² (𝕋 , 𝔽)) cs ≡ 𝔽 ∷ 𝔽 ∷ []
lemma''RegNeverLoadHardcoded {[]} p = refl
lemma''RegNeverLoadHardcoded {.(𝕋 ∷ 𝔽 ∷ []) ∷ xs} (refl ∷ pxs) rewrite lemma''RegNeverLoadHardcoded pxs = refl
lemma'RegNeverLoadHardcoded : ∀ {cs} → All (⇓² (𝕋 , 𝔽) ≡_) cs → ⟦ reg ⟧ᶜ (⇓² (𝕋 , 𝔽) ∷ cs) ≡ ⇓ 𝔽
lemma'RegNeverLoadHardcoded {cs} p rewrite lemma''RegNeverLoadHardcoded p = refl
lemmaRegNeverLoadHardcoded : ∀ {cs} → All (⇓² (𝕋 , 𝔽) ≡_) cs → runᶜ′ ⟦ reg ⟧ᶜ (⇓² (𝕋 , 𝔽) ∷ cs) (map ⇓² (repeat (𝕋 , 𝔽))) ≈ map ⇓ (repeat 𝔽)
lemmaRegNeverLoadHardcoded {cs} p rewrite lemma'RegNeverLoadHardcoded p = refl ∷ (♯ (lemmaRegNeverLoadHardcoded (refl ∷ p)))
proofRegNeverLoadHardcoded : ⟦ reg ⟧ω (map ⇓² (repeat (𝕋 , 𝔽))) ≈ map ⇓ (repeat 𝔽)
proofRegNeverLoadHardcoded = lemmaRegNeverLoadHardcoded []
lemma''RegNeverLoad : ∀ {cs c0i} → All (λ c → ∃ (λ i → ⇓² (i , 𝔽) ≡ c)) cs → delay′ 1 {i = 2} ⟦ regCore ⟧ (⇓² (c0i , 𝔽)) cs ≡ 𝔽 ∷ 𝔽 ∷ []
lemma''RegNeverLoad {[]} p = refl
lemma''RegNeverLoad {.(xi ∷ 𝔽 ∷ []) ∷ xs} ((xi , refl) ∷ pxs) rewrite lemma''RegNeverLoad {c0i = xi} pxs = refl
lemma'RegNeverLoad : ∀ {cs c0i} → All (λ c → ∃ (λ i → ⇓² (i , 𝔽) ≡ c)) cs → ⟦ reg ⟧ᶜ (⇓² (c0i , 𝔽) ∷ cs) ≡ ⇓ 𝔽
lemma'RegNeverLoad {cs} {c0i} p rewrite lemma''RegNeverLoad {c0i = c0i} p = refl
lemmaRegNeverLoad : ∀ {xs cs c0i} → All (λ c → ∃ (λ i → ⇓² (i , 𝔽) ≡ c)) cs
→ runᶜ′ ⟦ reg ⟧ᶜ (⇓² (c0i , 𝔽) ∷ cs) (map ⇓² (xs ⟨ zip ⟩ repeat 𝔽)) ≈ map ⇓ (repeat 𝔽)
lemmaRegNeverLoad {x ∷ xs} {cs} {c0i} p rewrite lemma'RegNeverLoad {c0i = c0i} p = refl ∷ ♯ (lemmaRegNeverLoad ((c0i , refl) ∷ p))
proofRegNeverLoad : ∀ {xs} → ⟦ reg ⟧ω (map ⇓² (xs ⟨ zip ⟩ repeat 𝔽)) ≈ map ⇓ (repeat 𝔽)
proofRegNeverLoad {x ∷ xs} = lemmaRegNeverLoad []
lemmaRegAlwaysLoadHardcoded : ∀ {cs} → runᶜ′ ⟦ reg ⟧ᶜ (⇓² (𝕋 , 𝕋) ∷ cs) (map ⇓² (repeat (𝕋 , 𝕋))) ≈ map ⇓ (repeat 𝕋)
lemmaRegAlwaysLoadHardcoded {[]} = refl ∷ ♯ lemmaRegAlwaysLoadHardcoded
lemmaRegAlwaysLoadHardcoded {x ∷ xs} = refl ∷ ♯ lemmaRegAlwaysLoadHardcoded
proofRegAlwaysLoadHardcoded : ⟦ reg ⟧ω (map ⇓² (repeat (𝕋 , 𝕋))) ≈ map ⇓ (repeat 𝕋)
proofRegAlwaysLoadHardcoded = lemmaRegAlwaysLoadHardcoded
proofToggle = toggle-runᶜ′-𝕋 (toggleᶜ-start {[]})
\end{code}
%</proofToggle>
lemmaRegAlwaysLoad : ∀ {ins outs cs c0i} → outs ≈ c0i ∷ ins → runᶜ′ ⟦ reg ⟧ᶜ (⇓² (c0i , 𝕋) ∷ cs) (map ⇓² (♭ ins ⟨ zip ⟩ repeat 𝕋)) ≈ map ⇓ outs
lemmaRegAlwaysLoad {ins} {outs} {cs} {c0i} p with ♭ ins | inspect ♭ ins
lemmaRegAlwaysLoad {ins} {outs} {[]} p | i ∷ is | [ inseq ]ᵣ with outs
lemmaRegAlwaysLoad {ins} {outs} {[]} (refl ∷ xs≈) | i ∷ is | [ inseq ]ᵣ | o ∷ os = refl ∷ (♯ (lemmaRegAlwaysLoad {ins = is} (transₛ (♭ xs≈) (≡-to-≈ inseq))))
lemmaRegAlwaysLoad {ins} {outs} {x ∷ xs} p | i ∷ is | [ inseq ]ᵣ with outs
lemmaRegAlwaysLoad {ins} {outs} {x ∷ xs} (refl ∷ xs≈) | i ∷ is | [ inseq ]ᵣ | o ∷ os = refl ∷ (♯ (lemmaRegAlwaysLoad {ins = is} (transₛ (♭ xs≈) (≡-to-≈ inseq))))
proofRegAlwaysLoad : ∀ {xs} → ⟦ reg ⟧ω (map ⇓² (xs ⟨ zip ⟩ repeat 𝕋)) ≈ map ⇓ xs
proofRegAlwaysLoad {x ∷ xs} = lemmaRegAlwaysLoad reflₛ
%<*reg-delay′-never>
\begin{code}
reg-delay′-never : ∀ {d⁰ x⁻} → All (λ x → ∃ (λ d → ⇓² (d , 𝔽) ≡ x)) x⁻ → delay′ 1 {i = 2} ⟦ regCore ⟧ (⇓² (d⁰ , 𝔽)) x⁻ ≡ 𝔽 ∷ 𝔽 ∷ []
reg-delay′-never {x⁻ = []} p = refl
reg-delay′-never {x⁻ = .(d⁻¹ ∷ 𝔽 ∷ []) ∷ xs} ((d⁻¹ , refl) ∷ pxs) rewrite reg-delay′-never {d⁻¹} pxs = refl
\end{code}
%</reg-delay′-never>
lemmaRegAlwaysLoad' : ∀ {ins cs c0i} → runᶜ′ ⟦ reg ⟧ᶜ (⇓² (c0i , 𝕋) ∷ cs) (map ⇓² (ins ⟨ zip ⟩ repeat 𝕋)) ≈ₚ map ⇓ (c0i ∷ ♯ ins)
lemmaRegAlwaysLoad' {x ∷ xs} {[]} = refl ∷ₚ (♯ (transₚ lemmaRegAlwaysLoad' (refl ∷ₚ (♯ reflₚ))))
lemmaRegAlwaysLoad' {x ∷ xs} {c ∷ cs} = refl ∷ₚ (♯ (transₚ lemmaRegAlwaysLoad' (refl ∷ₚ (♯ reflₚ))))
%<*regᶜ-never>
\begin{code}
regᶜ-never : ∀ {d⁰ x⁻} → All (λ x → ∃ (λ d → ⇓² (d , 𝔽) ≡ x)) x⁻ → ⟦ reg ⟧ᶜ (⇓² (d⁰ , 𝔽) ∷ x⁻) ≡ ⇓ 𝔽
regᶜ-never {d⁰} {x⁻} p rewrite reg-delay′-never {d⁰} p = refl
\end{code}
%</regᶜ-never>
proofRegAlwaysLoad' : ∀ {xs} → ⟦ reg ⟧ω (map ⇓² (xs ⟨ zip ⟩ repeat 𝕋)) ≈ map ⇓ xs
proofRegAlwaysLoad' {x ∷ xs} = transₛ (≈ₚ-to-≈ lemmaRegAlwaysLoad') (refl ∷ (♯ reflₛ))
%<*reg-runᶜ′-never>
\begin{code}
reg-runᶜ′-never : ∀ {d⁰ x⁺ x⁻} → All (λ c → ∃ (λ i → ⇓² (i , 𝔽) ≡ c)) x⁻
→ runᶜ′ ⟦ reg ⟧ᶜ (⇓² (d⁰ , 𝔽) ∷ x⁻) (map ⇓² (x⁺ ⟨ zip ⟩ repeat 𝔽)) ≈ map ⇓ (repeat 𝔽)
reg-runᶜ′-never {d⁰} {x⁺ = _ ∷ _} p rewrite regᶜ-never {d⁰} p = refl ∷ ♯ reg-runᶜ′-never ((d⁰ , refl) ∷ p)
\end{code}
%</reg-runᶜ′-never>
%<*proofReg-never>
\begin{code}
proofReg-never : ∀ {xs} → ⟦ reg ⟧ω (map ⇓² (xs ⟨ zip ⟩ repeat 𝔽)) ≈ map ⇓ (repeat 𝔽)
proofReg-never {_ ∷ _} = reg-runᶜ′-never []
\end{code}
%</proofReg-never>
--proofShift : ∀ {cs c1 c0 ins outs⁺ outs} → outs ≈ c1 ∷ outs⁺ → ♭ outs⁺ ≈ c0 ∷ ins → runᶜ′ ⟦ shift ⟧ᶜ (cs ≻ c1 ≻ c0) (♭ ins) ≈ outs
--proofShift {outs⁺ = outs⁺} p1 p2 with ♭ outs⁺ | p2
--proofShift {c0 = c0} {ins = ins} p1 p2 | .c0 ∷ xs | refl ∷ xs≈ with ♭ ins | inspect ♭ ins
--proofShift {c0 = c0} p1 p2 | .c0 ∷ xs | refl ∷ xs≈ | x ∷ xs₁ | [ inseq ] with p1
--proofShift {[]} {c1} {c0} {ins} {outs⁺} {.c1 ∷ xs₂} p1 p2 | .c0 ∷ xs | refl ∷ xs≈ | x ∷ xs₁ | [ inseq ] | refl ∷ xs≈₁ =
-- (lemma {c0} {c1}) ∷ (♯ (proofShift {[] ≻ c1} {c0} {x} {xs₁} {xs} {♭ xs₂} (strans (♭ xs≈₁) (strans p2 (refl ∷ ♯ (strans (≡-to-≈ inseq) (ssym (♭ xs≈)))))) (♭ xs≈)))
--proofShift {cs ≻ x₁} {c1} {c0} {ins} {outs⁺} {.c1 ∷ xs₂} p1 p2 | .c0 ∷ xs | refl ∷ xs≈ | x ∷ xs₁ | [ inseq ] | refl ∷ xs≈₁ =
-- (lemma {c0} {c1}) ∷ (♯ (proofShift {cs ≻ x₁ ≻ c1} {c0} {x} {xs₁} {xs} {♭ xs₂} (strans (♭ xs≈₁) (strans p2 (refl ∷ ♯ (strans (≡-to-≈ inseq) (ssym (♭ xs≈)))))) (♭ xs≈)))
--proofShiftTail : ∀ {ins} → tail (⟦ shift ⟧ω ins) ≈ ins
--proofShiftTail {x ∷ xs} with ♭ xs | inspect ♭ xs
--proofShiftTail {x ∷ xs} | x₁ ∷ xs₁ | [ xseq ] = proofShift {[]} {x} {x₁} {xs₁} {xs} srefl (≡-to-≈ xseq)
%<*reg-runᶜ′-always>
\begin{code}
reg-runᶜ′-always : ∀ {d⁰ x⁻ x⁺} → runᶜ′ ⟦ reg ⟧ᶜ (⇓² (d⁰ , 𝕋) ∷ x⁻) (map ⇓² (x⁺ ⟨ zip ⟩ repeat 𝕋)) ≈ₚ map ⇓ (d⁰ ∷ ♯ x⁺)
reg-runᶜ′-always {x⁻ = []} {x⁺ = _ ∷ _} = refl ∷ₚ ♯ transₚ reg-runᶜ′-always (refl ∷ₚ ♯ reflₚ)
reg-runᶜ′-always {x⁻ = _ ∷ _} {x⁺ = _ ∷ _} = refl ∷ₚ ♯ transₚ reg-runᶜ′-always (refl ∷ₚ ♯ reflₚ)
\end{code}
%</reg-runᶜ′-always>
%<*proofReg-always>
\begin{code}
proofReg-always : ∀ {xs} → ⟦ reg ⟧ω (map ⇓² (xs ⟨ zip ⟩ repeat 𝕋)) ≈ map ⇓ xs
proofReg-always {x ∷ xs} = ≈ₚ-to-≈ $ transₚ reg-runᶜ′-always (refl ∷ₚ ♯ reflₚ)
\end{code}
%</proofReg-always>
--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)
--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})
-- 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)))
--proofReĝAlwaysLoadHardcoded : ⟦ reĝ ⟧ω̂ (repeat (𝕋 , 𝕋)) ≈ repeat 𝕋
--proofReĝAlwaysLoadHardcoded = liftProof {p = id} {α̂ = ⇕Bool²} {β̂ = ⇕Bool} {f = reg} {xs = repeat (𝕋 , 𝕋)}
-- (λ {_} {_} {f} {s} → ssym (id-swap {f = map f} {s = s}))
-- (λ x → refl)
-- proofRegAlwaysLoadHardcoded
proofShiftTail̂ : ∀ {ins} → tail (⟦ shift̂ ⟧ω̂ ins) ≈ ins
proofShiftTail̂ {ins} = liftProof {α̂ = ⇕Bool} {β̂ = ⇕Bool} {f = shift} {xs = ins}
(λ {_} {_} {_} {s} → (tail-map-swap {s = s}))
(λ x → refl)
proofShiftTail
--proofReĝNeverLoadHardcoded : ⟦ reĝ ⟧ω̂ (repeat (𝕋 , 𝔽)) ≈ repeat 𝔽
--proofReĝNeverLoadHardcoded = liftProof {p = id} {α̂ = ⇕Bool²} {β̂ = ⇕Bool} {f = reg} {xs = repeat (𝕋 , 𝔽)}
-- (λ {_} {_} {f} {s} → ssym (id-swap {f = map f} {s = s}))
-- (λ x → refl)
-- proofRegNeverLoadHardcoded
proofShiftHead̂ : ∀ {ins} → head (⟦ shift̂ ⟧ω̂ ins) ≡ 𝔽
proofShiftHead̂ {_ ∷ xs} with ♭ xs
proofShiftHead̂ {_ ∷ _ } | _ ∷ _ = refl
--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)))
proofTogglê : ⟦ togglê ⟧ω̂ (repeat tt) ≈ iterate not 𝕋
proofTogglê = map-cong ⇑ proofToggle ⟨ transₛ ⟩ symₛ map-compose ⟨ transₛ ⟩ map-id
--proofShiftTail̂ : ∀ {ins} → tail (⟦ shift̂ ⟧ω̂ ins) ≈ ins
--proofShiftTail̂ {ins} = liftProof {α̂ = ⇕Bool} {β̂ = ⇕Bool} {f = shift} {xs = ins}
-- (λ {_} {_} {_} {s} → (tail-map-swap {s = s}))
-- (λ x → refl)
-- proofShiftTail
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)
proofShiftHead̂ : ∀ {ins} → head (⟦ shift̂ ⟧ω̂ ins) ≡ 𝔽
proofShiftHead̂ {_ ∷ xs} with ♭ xs
proofShiftHead̂ {_ ∷ _ } | _ ∷ _ = refl
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})
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