```------------------------------------------------------------------------
-- The Agda standard library
--
-- Coinductive pointwise lifting of relations to streams
------------------------------------------------------------------------

{-# OPTIONS --safe --cubical-compatible --guardedness #-}

module Codata.Guarded.Stream.Relation.Binary.Pointwise where

open import Codata.Guarded.Stream as Stream using (Stream; head; tail)
open import Data.Nat.Base using (ℕ; zero; suc)
open import Function.Base using (_∘_; _on_)
open import Level using (Level; _⊔_)
open import Relation.Binary.Core using (REL; _⇒_)
open import Relation.Binary.Bundles using (Setoid)
open import Relation.Binary.Definitions
using (Reflexive; Sym; Trans; Antisym; Symmetric; Transitive)
open import Relation.Binary.Structures using (IsEquivalence)
open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
import Relation.Binary.PropositionalEquality.Properties as P

private
variable
a ℓ : Level
A B C D : Set a
R S T : REL A B ℓ
xs ys : Stream A

------------------------------------------------------------------------
-- Bisimilarity

infixr 5 _∷_

record Pointwise (_∼_ : REL A B ℓ) (as : Stream A) (bs : Stream B) : Set ℓ where
coinductive
constructor _∷_
field
tail : Pointwise _∼_ (tail as) (tail bs)

open Pointwise public

lookup⁺ : ∀ {as bs} → Pointwise R as bs →
∀ n → R (Stream.lookup as n) (Stream.lookup bs n)
lookup⁺ rs zero    = rs .head
lookup⁺ rs (suc n) = lookup⁺ (rs .tail) n

map : R ⇒ S → Pointwise R ⇒ Pointwise S
tail (map R⇒S xs) = map R⇒S (tail xs)

reflexive : Reflexive R → Reflexive (Pointwise R)
tail (reflexive R-refl) = reflexive R-refl

symmetric : Sym R S → Sym (Pointwise R) (Pointwise S)
tail (symmetric R-sym-S xsRys) = symmetric R-sym-S (tail xsRys)

transitive : Trans R S T → Trans (Pointwise R) (Pointwise S) (Pointwise T)
tail (transitive RST-trans xsRys ysSzs) = transitive RST-trans (tail xsRys) (tail ysSzs)

isEquivalence : IsEquivalence R → IsEquivalence (Pointwise R)
isEquivalence equiv^R = record
{ refl  = reflexive equiv^R.refl
; sym   = symmetric equiv^R.sym
; trans = transitive equiv^R.trans
} where module equiv^R = IsEquivalence equiv^R

setoid : Setoid a ℓ → Setoid a ℓ
setoid S = record
{ isEquivalence = isEquivalence (Setoid.isEquivalence S)
}

antisymmetric : Antisym R S T → Antisym (Pointwise R) (Pointwise S) (Pointwise T)
tail (antisymmetric RST-antisym xsRys ysSxs) = antisymmetric RST-antisym (tail xsRys) (tail ysSxs)

tabulate⁺ : ∀ {f : ℕ → A} {g : ℕ → B} →
(∀ i → R (f i) (g i)) → Pointwise R (Stream.tabulate f) (Stream.tabulate g)
head (tabulate⁺ f∼g) = f∼g 0
tail (tabulate⁺ f∼g) = tabulate⁺ (f∼g ∘ suc)

tabulate⁻ : ∀ {f : ℕ → A} {g : ℕ → B} →
Pointwise R (Stream.tabulate f) (Stream.tabulate g) → (∀ i → R (f i) (g i))
tabulate⁻ xsRys zero    = head xsRys
tabulate⁻ xsRys (suc i) = tabulate⁻ (tail xsRys) i

map⁺ : ∀ (f : A → C) (g : B → D) →
Pointwise (λ a b → R (f a) (g b)) xs ys →
Pointwise R (Stream.map f xs) (Stream.map g ys)
tail (map⁺ f g faRgb) = map⁺ f g (tail faRgb)

map⁻ : ∀ (f : A → C) (g : B → D) →
Pointwise R (Stream.map f xs) (Stream.map g ys) →
Pointwise (λ a b → R (f a) (g b)) xs ys
tail (map⁻ f g faRgb) = map⁻ f g (tail faRgb)

drop⁺ : ∀ n → Pointwise R ⇒ (Pointwise R on Stream.drop n)
drop⁺ zero    as≈bs = as≈bs
drop⁺ (suc n) as≈bs = drop⁺ n (as≈bs .tail)

------------------------------------------------------------------------
-- Pointwise Equality as a Bisimilarity

module _ {A : Set a} where

infix 1 _≈_
_≈_ : Stream A → Stream A → Set a
_≈_ = Pointwise _≡_

refl : Reflexive _≈_
refl = reflexive P.refl

sym : Symmetric _≈_
sym = symmetric P.sym

trans : Transitive _≈_
trans = transitive P.trans

≈-setoid : Setoid _ _
≈-setoid = setoid (P.setoid A)

------------------------------------------------------------------------
-- Pointwise DSL
-- A guardedness check does not play well with compositional proofs.
-- Luckily we can learn from Nils Anders Danielsson's
-- Beating the Productivity Checker Using Embedded Languages
-- and design a little compositional DSL to define such proofs

module pw-Reasoning (S : Setoid a ℓ) where
private module S = Setoid S
open S using (Carrier) renaming (_≈_ to _∼_)

record `Pointwise∞ (as bs : Stream Carrier) : Set (a ⊔ ℓ)
data   `Pointwise  (as bs : Stream Carrier) : Set (a ⊔ ℓ)

record `Pointwise∞ as bs where
coinductive
field
tail : `Pointwise (as .tail) (bs .tail)

data `Pointwise as bs where
`lift  : Pointwise _∼_ as bs → `Pointwise as bs
`step  : `Pointwise∞ as bs → `Pointwise as bs
`refl  : as ≡ bs → `Pointwise as bs
`bisim : as ≈ bs → `Pointwise as bs
`sym   : `Pointwise bs as → `Pointwise as bs
`trans : ∀ {ms} → `Pointwise as ms → `Pointwise ms bs → `Pointwise as bs

open `Pointwise∞ public

`tail : ∀ {as bs} → `Pointwise as bs → `Pointwise (as .tail)  (bs .tail)
`tail (`lift rs)         = `lift (rs .tail)
`tail (`refl eq)         = `refl (P.cong tail eq)
`tail (`bisim rs)        = `bisim (rs .tail)
`tail (`step `rs)        = `rs .tail
`tail (`sym `rs)         = `sym (`tail `rs)
`tail (`trans `rs₁ `rs₂) = `trans (`tail `rs₁) (`tail `rs₂)

run : ∀ {as bs} → `Pointwise as bs → Pointwise _∼_ as bs
run `rs .tail = run (`tail `rs)

infix  1 begin_
infixr 2 _↺⟨_⟩_ _↺˘⟨_⟩_ _∼⟨_⟩_ _∼˘⟨_⟩_ _≈⟨_⟩_ _≈˘⟨_⟩_ _≡⟨_⟩_ _≡˘⟨_⟩_ _≡⟨⟩_
infix  3 _∎

-- Beginning of a proof
begin_ : ∀ {as bs} → `Pointwise∞ as bs → Pointwise _∼_ as bs
(begin `rs) .tail = run (`rs .tail)

pattern _↺⟨_⟩_  as as∼bs bs∼cs = `trans {as = as} (`step as∼bs) bs∼cs
pattern _↺˘⟨_⟩_ as bs∼as bs∼cs = `trans {as = as} (`sym (`step bs∼as)) bs∼cs
pattern _∼⟨_⟩_  as as∼bs bs∼cs = `trans {as = as} (`lift as∼bs) bs∼cs
pattern _∼˘⟨_⟩_ as bs∼as bs∼cs = `trans {as = as} (`sym (`lift bs∼as)) bs∼cs
pattern _≈⟨_⟩_  as as∼bs bs∼cs = `trans {as = as} (`bisim as∼bs) bs∼cs
pattern _≈˘⟨_⟩_ as bs∼as bs∼cs = `trans {as = as} (`sym (`bisim bs∼as)) bs∼cs
pattern _≡⟨_⟩_  as as∼bs bs∼cs = `trans {as = as} (`refl as∼bs) bs∼cs
pattern _≡˘⟨_⟩_ as bs∼as bs∼cs = `trans {as = as} (`sym (`refl bs∼as)) bs∼cs
pattern _≡⟨⟩_   as as∼bs       = `trans {as = as} (`refl P.refl) as∼bs
pattern _∎      as             = `refl  {as = as} P.refl

module ≈-Reasoning {a} {A : Set a} where

open pw-Reasoning (P.setoid A) public

infix 4 _≈∞_
_≈∞_ = `Pointwise∞
```