Some duplication eliminated

parent 1d856461
......@@ -12,6 +12,7 @@ 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; head)
open import Data.Vec.Properties.Extra using (singleton∘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ₛ; module EqReasoningₛ; map-repeat; map-compose; map-cong-fun; map-id)
......@@ -322,42 +323,24 @@ map⇓²-zip-map⇑¹-repeat {x ∷ _} {y} = append-headCons x ∷ ♯ map⇓²-
\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 [ 𝔽 ] ∎ₛ
⟦ 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>
-- 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>
\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 ∎ₛ
⟦ 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 singleton∘head ⟩
map id xs ≈⟨ map-id ⟩
xs ∎ₛ
\end{code}
%</proofReg-always>
......@@ -10,7 +10,7 @@ open import Data.Product using (_,_; proj₂)
open import Data.List.NonEmpty using (_∷_)
open import Data.Vec using ([]; _∷_; _∷ʳ_; [_]; tabulate; _++_; head; Vec; _⋎_; replicate; splitAt; lookup)
open import Data.Vec.Extra using (splitAt′; ₁∘split1′; ₂∘split1′)
open import Data.Vec.Properties.Extra using (singleton∘head; tabulate-cong)
open import Data.Vec.Properties.Extra using (tabulate-cong)
open import Data.Stream using (zipWith; repeat; _≈_; map; _∷_; Stream; zipWith-cong)
open import Data.Stream.Equality.WithTrans using (_≈ₚ_; _∷ₚ_; transₚ; reflₚ; ≈ₚ-to-≈)
open import Data.Stream.Properties using (module Setoidₛ; module EqReasoningₛ; map-compose; map-repeat; map-cong-fun; map-id)
......@@ -279,34 +279,6 @@ zipWith-++-⇑ {x ∷ _} {y} = reduce x ∷ ♯ zipWith-++-⇑
%</zipWith-++-⇑>
%<*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 (zipWith-++-⇑ {xs}) ⟩
⟦ reg ⟧ω (map ⇓² (zipWith _,_ (map ⇑ xs) (repeat 𝔽))) ≈⟨ proofReg-never-typed {xs = map ⇑ xs} ⟩
map ⇓ (repeat 𝔽) ≈⟨ map-repeat ⟩
repeat [ 𝔽 ] ∎ₛ
\end{code}
%</proofReg-never-plain>
%<*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 (zipWith-++-⇑ {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 ⟩
xs ∎ₛ
\end{code}
%</proofReg-always-plain
%<*⋎-replicate>
\AgdaTarget{⋎-replicate}
\begin{code}
......
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