------------------------------------------------------------------------
-- 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 ≡ using (_≡_)
import Relation.Binary.PropositionalEquality.Properties as ≡ using (setoid)
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
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 ≡.refl
sym : Symmetric _≈_
sym = symmetric ≡.sym
trans : Transitive _≈_
trans = transitive ≡.trans
≈-setoid : Setoid _ _
≈-setoid = setoid (≡.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
--
-- NOTE: also because of the guardedness check we can't use the standard
-- `Relation.Binary.Reasoning.Syntax` approach.
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 (≡.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 (≡.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 ≡.refl) as∼bs
pattern _∎ as = `refl {as = as} ≡.refl
-- Deprecated v2.0
infixr 2 _↺˘⟨_⟩_ _∼˘⟨_⟩_ _≈˘⟨_⟩_ _≡˘⟨_⟩_
pattern _↺˘⟨_⟩_ as bs∼as bs∼cs = `trans {as = as} (`sym (`step bs∼as)) bs∼cs
pattern _∼˘⟨_⟩_ as bs∼as bs∼cs = `trans {as = as} (`sym (`lift bs∼as)) bs∼cs
pattern _≈˘⟨_⟩_ as bs∼as bs∼cs = `trans {as = as} (`sym (`bisim bs∼as)) bs∼cs
pattern _≡˘⟨_⟩_ as bs∼as bs∼cs = `trans {as = as} (`sym (`refl bs∼as)) bs∼cs
{-# WARNING_ON_USAGE _↺˘⟨_⟩_
"Warning: _↺˘⟨_⟩_ was deprecated in v2.0.
Please use _↺⟨_⟨_ instead."
#-}
{-# WARNING_ON_USAGE _∼˘⟨_⟩_
"Warning: _∼˘⟨_⟩_ was deprecated in v2.0.
Please use _∼⟨_⟨_ instead."
#-}
{-# WARNING_ON_USAGE _≈˘⟨_⟩_
"Warning: _≈˘⟨_⟩_ was deprecated in v2.0.
Please use _≈⟨_⟨_ instead."
#-}
{-# WARNING_ON_USAGE _≡˘⟨_⟩_
"Warning: _≡˘⟨_⟩_ was deprecated in v2.0.
Please use _≡⟨_⟨_ instead."
#-}
module ≈-Reasoning {a} {A : Set a} where
open pw-Reasoning (≡.setoid A) public
infix 4 _≈∞_
_≈∞_ = `Pointwise∞
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4