------------------------------------------------------------------------ -- 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 open import Relation.Binary.PropositionalEquality as P using (_≡_) private variable a ℓ : Level A B C D : Set a R S T : REL A B ℓ xs ys : Stream A ------------------------------------------------------------------------ -- Bisimilarity record Pointwise (_∼_ : REL A B ℓ) (as : Stream A) (bs : Stream B) : Set ℓ where coinductive constructor _∷_ field head : head as ∼ head bs 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 head (map R⇒S xs) = R⇒S (head xs) tail (map R⇒S xs) = map R⇒S (tail xs) reflexive : Reflexive R → Reflexive (Pointwise R) head (reflexive R-refl) = R-refl tail (reflexive R-refl) = reflexive R-refl symmetric : Sym R S → Sym (Pointwise R) (Pointwise S) head (symmetric R-sym-S xsRys) = R-sym-S (head xsRys) tail (symmetric R-sym-S xsRys) = symmetric R-sym-S (tail xsRys) transitive : Trans R S T → Trans (Pointwise R) (Pointwise S) (Pointwise T) head (transitive RST-trans xsRys ysSzs) = RST-trans (head xsRys) (head ysSzs) 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) head (antisymmetric RST-antisym xsRys ysSxs) = RST-antisym (head xsRys) (head ysSxs) 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) head (map⁺ f g faRgb) = head faRgb 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 head (map⁻ f g faRgb) = head faRgb 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 head : (as .head) ∼ (bs .head) 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 `head : ∀ {as bs} → `Pointwise as bs → as .head ∼ bs .head `head (`lift rs) = rs .head `head (`refl eq) = S.reflexive (P.cong head eq) `head (`bisim rs) = S.reflexive (rs .head) `head (`step `rs) = `rs .head `head (`sym `rs) = S.sym (`head `rs) `head (`trans `rs₁ `rs₂) = S.trans (`head `rs₁) (`head `rs₂) `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 .head = `head `rs 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) .head = `rs .head (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 _≈∞_ = `Pointwise∞