module Stream.Pointwise where
open import Codata.Musical.Notation hiding (∞)
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 Relation.Binary
open import Relation.Binary.PropositionalEquality
private
module IsEq {A : Set} =
IsEquivalence (Setoid.isEquivalence (Stream.setoid A))
infix 8 _∞
infixr 7 _·_
infix 6 _⟨_⟩_
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
⟦_⟧ : ∀ {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 ⟧ ρ
⟪_⟫ : ∀ {A n} → Pointwise A n → (Vec A n → A)
⟪ var x ⟫ ρ = Vec.lookup ρ x
⟪ x ∞ ⟫ ρ = x
⟪ f · xs ⟫ ρ = f (⟪ xs ⟫ ρ)
⟪ xs ⟨ _∙_ ⟩ ys ⟫ ρ = ⟪ xs ⟫ ρ ∙ ⟪ ys ⟫ ρ
private
lookup-nat : ∀ {a b n} {A : Set a} {B : Set b}
(f : A → B) (x : Fin n) ρ →
f (Vec.lookup ρ x) ≡ Vec.lookup (Vec.map f ρ) x
lookup-nat f zero (x ∷ ρ) = refl
lookup-nat f (suc i) (x ∷ ρ) = lookup-nat f i ρ
private
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-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 : ∀ {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 (Vec.map headP ρ) x ≺♯
Vec.lookup (Vec.map tailP ρ) x
≡⟨ 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 ρ
∎
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 ⟫ ρ
∎
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
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)
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))
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