------------------------------------------------------------------------
-- Pointwise equalities can be lifted
------------------------------------------------------------------------

{-# OPTIONS --universe-polymorphism #-}

module Stream.Pointwise where

open import Coinduction hiding (; unfold)
open import Stream
open import Stream.Equality
import Stream.Programs as Prog
open Prog hiding (lift; ⟦_⟧)
open import Data.Nat
open import Data.Fin using (Fin; zero; suc)
open import Data.Vec as Vec using (Vec; _∷_)
open import Level hiding (lift)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
private
module IsEq {A} =
IsEquivalence (Setoid.isEquivalence (Stream.setoid A))

------------------------------------------------------------------------
-- Definitions

infix  8 _∞
infixr 7 _·_
infix  6 _⟨_⟩_

-- Expressions corresponding to pointwise definitions of streams.
-- Indexed on the number of variables.

-- It is possible to generalise this type, allowing variables to
-- correspond to streams containing elements of arbitrary type, and
-- letting the function arguments of _·_ and _⟨_⟩_ be more general.
-- However, this would complicate the development, so I hesitate to do
-- so without evidence that it would be genuinely useful.

data Pointwise A n : Set where
var   : (x : Fin n)  Pointwise A n
_∞    : (x : A)  Pointwise A n
_·_   : (f : A  A) (xs : Pointwise A n)  Pointwise A n
_⟨_⟩_ : (xs : Pointwise A n)
(_∙_ : A  A  A)
(ys : Pointwise A n)
Pointwise A n

-- Stream semantics.

⟦_⟧ :  {A n}  Pointwise A n  (Vec (Prog A) n  Prog A)
var x          ρ = Vec.lookup x ρ
x             ρ = x
f · xs         ρ = f ·  xs  ρ
xs  _∙_  ys  ρ =  xs  ρ  _∙_   ys  ρ

-- Pointwise semantics.

⟪_⟫ :  {A n}  Pointwise A n  (Vec A n  A)
var x          ρ = Vec.lookup x ρ
x             ρ = x
f · xs         ρ = f ( xs  ρ)
xs  _∙_  ys  ρ =  xs  ρ   ys  ρ

------------------------------------------------------------------------
-- Some lemmas used below

private

-- lookup is natural.

lookup-nat :  {a b n} {A : Set a} {B : Set b}
(f : A  B) (x : Fin n) ρ
f (Vec.lookup x ρ)  Vec.lookup x (Vec.map f ρ)
lookup-nat f zero    (x  ρ) = refl
lookup-nat f (suc i) (x  ρ) = lookup-nat f i ρ

------------------------------------------------------------------------
-- The two semantics above are related via the function lift

private

-- Lifts a pointwise function to a function on stream programs.

lift :  {A B n}
(Vec A n  B)  Vec (Prog A) n  Prog B
lift f xs = f (Vec.map headP xs)   lift f (Vec.map tailP xs)

-- lift is a congruence in its first argument.

lift-cong :  {A B n} {f g : Vec A n  B}
(∀ ρ  f ρ  g ρ)
ρ  lift f ρ  lift g ρ
lift-cong hyp ρ = hyp (Vec.map headP ρ)
lift-cong hyp (Vec.map tailP ρ)

-- unfold xs ρ is the one-step unfolding of ⟦ xs ⟧ ρ. Note the
-- similarity to lift.

unfold :  {A n} (xs : Pointwise A n) ρ  Prog A
unfold xs ρ =  xs  (Vec.map headP ρ) ≺♯
xs  (Vec.map tailP ρ)

unfold-lemma :  {A n} (xs : Pointwise A n) ρ
xs  ρ  unfold xs ρ
unfold-lemma (var x) ρ =
Vec.lookup x ρ
≊⟨ ≊-η (Vec.lookup x ρ)
headP (Vec.lookup x ρ) ≺♯ tailP (Vec.lookup x ρ)
≊⟨ lookup-nat headP x ρ
≈⇒≅ (IsEq.reflexive
(cong Prog.⟦_⟧ (lookup-nat tailP x ρ)))
Vec.lookup x (Vec.map headP ρ) ≺♯
Vec.lookup x (Vec.map tailP ρ)
≡⟨ refl
unfold (var x) ρ

unfold-lemma (x )    ρ = x
unfold-lemma (f · xs) ρ =
f ·  xs  ρ
≊⟨ ·-cong f ( xs  ρ) (unfold xs ρ) (unfold-lemma xs ρ)
f · unfold xs ρ

unfold-lemma (xs    ys) ρ =
xs  ρ     ys  ρ
≊⟨   ⟩-cong ( xs  ρ) (unfold xs ρ) (unfold-lemma xs ρ)
( ys  ρ) (unfold ys ρ) (unfold-lemma ys ρ)
unfold xs ρ    unfold ys ρ

-- The two semantics are related.

main-lemma :  {A n} (xs : Pointwise A n)
ρ   xs  ρ  lift  xs  ρ
main-lemma xs ρ =
xs  ρ
≊⟨ unfold-lemma xs ρ
unfold xs ρ
≡⟨ refl
xs  (Vec.map headP ρ) ≺♯  xs  (Vec.map tailP ρ)
≊⟨ refl   main-lemma xs (Vec.map tailP ρ)
lift  xs  ρ

------------------------------------------------------------------------
-- To prove that two streams which are defined pointwise are equal, it
-- is enough to reason about a single (arbitrary) point

-- This function is a bit awkward to use, since the user has to come
-- up with a suitable environment manually. The alternative function
-- pointwise below may be slightly easier to use.

pointwise' :  {A n} (xs ys : Pointwise A n)
(∀ ρ   xs  ρ   ys  ρ)
(∀ ρ   xs  ρ   ys  ρ)
pointwise' xs ys hyp ρ =
xs  ρ
≊⟨ main-lemma xs ρ
lift  xs  ρ
≊⟨ lift-cong hyp ρ
lift  ys  ρ
≊⟨ ≅-sym (main-lemma ys ρ)
ys  ρ

open import Data.Vec.N-ary

-- Applies the function to all possible variables.

app :  {A} n
N-ary n (Pointwise A n) (Pointwise A n)  Pointwise A n
app n f = f \$ⁿ Vec.map var (Vec.allFin n)

-- The type signature of this function may be a bit daunting, but once
-- n, f and g are instantiated with well-behaved concrete values the
-- remaining type evaluates nicely.

pointwise
:  {A} n (f g : N-ary n (Pointwise A n) (Pointwise A n))
Eq n _≡_ (curryⁿ  app n f ) (curryⁿ  app n g )
Eq n _≊_ (curryⁿ  app n f ) (curryⁿ  app n g )
pointwise n f g hyp =
curryⁿ-cong  app n f   app n g
(pointwise' (app n f) (app n g)
(curryⁿ-cong⁻¹  app n f   app n g  hyp))

------------------------------------------------------------------------
-- Some examples

private

example₁ : suc · 0   1
example₁ = pointwise 0 (suc · 0 ) (1 ) refl

example₂ :  s  suc · s  1   _+_  s
example₂ = pointwise 1  s  suc · s)
s  1   _+_  s)
_  refl)

example₃ :  s t u
(s  _+_  t)  _+_  u  s  _+_  (t  _+_  u)
example₃ = pointwise 3  s t u  (s  _+_  t)  _+_  u)
s t u   s  _+_  (t  _+_  u))
+-assoc
where
open import Data.Nat.Properties
open import Algebra.Structures
open IsCommutativeSemiring isCommutativeSemiring