------------------------------------------------------------------------
-- Some lemmas used by the other modules in this directory
------------------------------------------------------------------------

module Hinze.Lemmas where

open import Stream.Programs
open import Stream.Equality

open import Codata.Musical.Notation hiding ()
open import Relation.Binary.PropositionalEquality
open import Function using (_∘_; flip)

------------------------------------------------------------------------
-- Some lemmas from Section 2.3 of Hinze's paper

⋎-∞ :  {A} (x : A)  x   x   x
⋎-∞ x = refl   ⋎-∞ x

⋎-map :  {A B} ( : A  B) s t
· s   · t   · (s  t)
⋎-map  s t with whnf s
⋎-map  s t | x  s′ = refl   ⋎-map  t s′

abide-law :  {A B C} ( : A  B  C) s₁ s₂ t₁ t₂
s₁    s₂  t₁    t₂  (s₁  t₁)    (s₂  t₂)
abide-law  s₁ s₂ t₁ t₂ with whnf s₁ | whnf s₂
abide-law  s₁ s₂ t₁ t₂ | x₁  s₁′ | x₂  s₂′ =
refl   abide-law  t₁ t₂ s₁′ s₂′

------------------------------------------------------------------------
-- Other lemmas

tailP-cong :  {A} (xs ys : Prog A)
xs  ys  tailP xs  tailP ys
tailP-cong xs ys xs≈ys with whnf xs | whnf ys | ≅⇒≃ xs≈ys
tailP-cong xs ys xs≈ys | x  xs′ | y  ys′ | x≡y  xs≈ys′ = xs≈ys′

map-fusion :  {A B C} (f : B  C) (g : A  B) xs
f · g · xs  (f  g) · xs
map-fusion f g xs with whnf xs
map-fusion f g xs | x  xs′ = refl   map-fusion f g xs′

zip-const-is-map :  {A B C} (_∙_ : A  B  C) xs y
xs  _∙_  y    x  x  y) · xs
zip-const-is-map _∙_ xs y with whnf xs
zip-const-is-map _∙_ xs y | x  xs′ =
refl   zip-const-is-map _∙_ xs′ y

zip-flip :  {A B C} ( : A  B  C) s t
s    t  t  flip   s
zip-flip  s t with whnf s | whnf t
zip-flip  s t | x  s′ | y  t′ = refl   zip-flip  s′ t′

zip-⋎-const :  {A B C} ( : A  B  C) s t x
(s  t)    x   s    x   t    x
zip-⋎-const _∙_ s t x =
(s  t)  _∙_  x
≊⟨ zip-const-is-map _ (s  t) _
y  y  x) · (s  t)
≊⟨ ≅-sym (⋎-map  y  y  x) s t)
y  y  x) · s   y  y  x) · t
≊⟨ ≅-sym (⋎-cong (s  _∙_  x ) ((λ y  y  x) · s)
(zip-const-is-map _∙_ s x)
_ _ (zip-const-is-map _∙_ t x))
s  _∙_  x   t  _∙_  x

zip-const-⋎ :  {A B C} ( : A  B  C) x s t
x     (s  t)  x     s  x     t
zip-const-⋎  x s t =
x     (s  t)
≊⟨ zip-flip  (x ) (s  t)
(s  t)  flip   x
≊⟨ zip-⋎-const (flip ) s t x
s  flip   x   t  flip   x
≊⟨ ≅-sym (⋎-cong (x     s) (s  flip   x )
(zip-flip  (x ) s)
_ _ (zip-flip  (x ) t))
x     s  x     t