------------------------------------------------------------------------
-- Some Vec-related properties
------------------------------------------------------------------------

module Data.Vec.Properties where

open import Algebra
open import Data.Vec
open import Data.Nat
import Data.Nat.Properties as Nat
open import Data.Fin using (Fin; zero; suc)
open import Data.Function
open import Relation.Binary

module UsingVectorEquality (S : Setoid) where

private module SS = Setoid S
open SS using () renaming (carrier to A)
import Data.Vec.Equality as VecEq
open VecEq.Equality S

replicate-lemma :  {m} n x (xs : Vec A m)
replicate {n = n}     x ++ (x  xs)
replicate {n = 1 + n} x ++      xs
replicate-lemma zero    x xs = refl (x  xs)
replicate-lemma (suc n) x xs = SS.refl ∷-cong replicate-lemma n x xs

xs++[]=xs :  {n} (xs : Vec A n)  xs ++ []  xs
xs++[]=xs []       = []-cong
xs++[]=xs (x  xs) = SS.refl ∷-cong xs++[]=xs xs

map-++-commute :  {B m n} (f : B  A) (xs : Vec B m) {ys : Vec B n}
map f (xs ++ ys)  map f xs ++ map f ys
map-++-commute f []       = refl _
map-++-commute f (x  xs) = SS.refl ∷-cong map-++-commute f xs

open import Relation.Binary.PropositionalEquality as PropEq
open import Relation.Binary.HeterogeneousEquality as HetEq

-- lookup is natural.

lookup-natural :  {A B n} (f : A  B) (i : Fin n)
lookup i  map f  f  lookup i
lookup-natural f zero    (x  xs) = refl
lookup-natural f (suc i) (x  xs) = lookup-natural f i xs

-- map is a congruence.

map-cong :  {A B n} {f g : A  B}
f  g  _≗_ {Vec A n} (map f) (map g)
map-cong f≗g []       = refl
map-cong f≗g (x  xs) = PropEq.cong₂ _∷_ (f≗g x) (map-cong f≗g xs)

-- map is functorial.

map-id :  {A n}  _≗_ {Vec A n} (map id) id
map-id []       = refl
map-id (x  xs) = PropEq.cong (_∷_ x) (map-id xs)

map-∘ :  {A B C n} (f : B  C) (g : A  B)
_≗_ {Vec A n} (map (f  g)) (map f  map g)
map-∘ f g []       = refl
map-∘ f g (x  xs) = PropEq.cong (_∷_ (f (g x))) (map-∘ f g xs)

-- sum commutes with _++_.

sum-++-commute :  {m n} (xs : Vec  m) {ys : Vec  n}
sum (xs ++ ys)  sum xs + sum ys
sum-++-commute []            = refl
sum-++-commute (x  xs) {ys} = begin
x + sum (xs ++ ys)
≡⟨ PropEq.cong  p  x + p) (sum-++-commute xs)
x + (sum xs + sum ys)
≡⟨ PropEq.sym (+-assoc x (sum xs) (sum ys))
sum (x  xs) + sum ys

where
open ≡-Reasoning
open CommutativeSemiring Nat.commutativeSemiring hiding (_+_; sym)

-- foldr is a congruence.

foldr-cong :  {A} {B₁} {f₁ :  {n}  A  B₁ n  B₁ (suc n)} {e₁}
{B₂} {f₂ :  {n}  A  B₂ n  B₂ (suc n)} {e₂}
(∀ {n x} {y₁ : B₁ n} {y₂ : B₂ n}
y₁  y₂  f₁ x y₁  f₂ x y₂)
e₁  e₂
{n} (xs : Vec A n)
foldr B₁ f₁ e₁ xs  foldr B₂ f₂ e₂ xs
foldr-cong           _     e₁=e₂ []       = e₁=e₂
foldr-cong {B₁ = B₁} f₁=f₂ e₁=e₂ (x  xs) =
f₁=f₂ (foldr-cong {B₁ = B₁} f₁=f₂ e₁=e₂ xs)

-- foldl is a congruence.

foldl-cong :  {A} {B₁} {f₁ :  {n}  B₁ n  A  B₁ (suc n)} {e₁}
{B₂} {f₂ :  {n}  B₂ n  A  B₂ (suc n)} {e₂}
(∀ {n x} {y₁ : B₁ n} {y₂ : B₂ n}
y₁  y₂  f₁ y₁ x  f₂ y₂ x)
e₁  e₂
{n} (xs : Vec A n)
foldl B₁ f₁ e₁ xs  foldl B₂ f₂ e₂ xs
foldl-cong           _     e₁=e₂ []       = e₁=e₂
foldl-cong {B₁ = B₁} f₁=f₂ e₁=e₂ (x  xs) =
foldl-cong {B₁ = B₁ ∘₀ suc} f₁=f₂ (f₁=f₂ e₁=e₂) xs

-- The (uniqueness part of the) universality property for foldr.

foldr-universal :  {A} (B :   Set)
(f :  {n}  A  B n  B (suc n)) {e}
(h :  {n}  Vec A n  B n)
h []  e
(∀ {n} x  h  _∷_ x  f {n} x  h)
{n}  h  foldr B {n} f e
foldr-universal B f     h base step []       = base
foldr-universal B f {e} h base step (x  xs) = begin
h (x  xs)
≡⟨ step x xs
f x (h xs)
≡⟨ PropEq.cong (f x) (foldr-universal B f h base step xs)
f x (foldr B f e xs)

where open ≡-Reasoning

-- A fusion law for foldr.

foldr-fusion :  {A} {B :   Set} {f :  {n}  A  B n  B (suc n)} e
{C :   Set} {g :  {n}  A  C n  C (suc n)}
(h :  {n}  B n  C n)
(∀ {n} x  h  f {n} x  g x  h)
{n}  h  foldr B {n} f e  foldr C g (h e)
foldr-fusion {B = B} {f} e {C} h fuse =
foldr-universal C _ _ refl  x xs  fuse x (foldr B f e xs))

-- The identity function is a fold.

idIsFold :  {A n}  id  foldr (Vec A) {n} _∷_ []
idIsFold = foldr-universal _ _ id refl  _ _  refl)