------------------------------------------------------------------------
-- The Agda standard library
--
-- Bisimilarity for Covecs
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --sized-types #-}
module Codata.Sized.Covec.Bisimilarity where
open import Level using (_⊔_)
open import Size using (Size; ∞)
open import Codata.Sized.Thunk using (Thunk; Thunk^R; force)
open import Codata.Sized.Conat hiding (_⊔_)
open import Codata.Sized.Covec using (Covec; _∷_; [])
open import Relation.Binary.Definitions
using (Reflexive; Symmetric; Transitive; Sym; Trans)
open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
data Bisim {a b r} {A : Set a} {B : Set b} (R : A → B → Set r) (i : Size) :
∀ m n (xs : Covec A ∞ m) (ys : Covec B ∞ n) → Set (r ⊔ a ⊔ b) where
[] : Bisim R i zero zero [] []
_∷_ : ∀ {x y m n xs ys} → R x y → Thunk^R (λ i → Bisim R i (m .force) (n .force)) i xs ys →
Bisim R i (suc m) (suc n) (x ∷ xs) (y ∷ ys)
infixr 5 _∷_
module _ {a r} {A : Set a} {R : A → A → Set r} where
reflexive : Reflexive R → ∀ {i m} → Reflexive (Bisim R i m m)
reflexive refl^R {i} {m} {[]} = []
reflexive refl^R {i} {m} {r ∷ rs} = refl^R ∷ λ where .force → reflexive refl^R
module _ {a b} {A : Set a} {B : Set b}
{r} {P : A → B → Set r} {Q : B → A → Set r} where
symmetric : Sym P Q → ∀ {i m n} → Sym (Bisim P i m n) (Bisim Q i n m)
symmetric sym^PQ [] = []
symmetric sym^PQ (p ∷ ps) = sym^PQ p ∷ λ where .force → symmetric sym^PQ (ps .force)
module _ {a b c} {A : Set a} {B : Set b} {C : Set c}
{r} {P : A → B → Set r} {Q : B → C → Set r} {R : A → C → Set r} where
transitive : Trans P Q R → ∀ {i m n p} → Trans (Bisim P i m n) (Bisim Q i n p) (Bisim R i m p)
transitive trans^PQR [] [] = []
transitive trans^PQR (p ∷ ps) (q ∷ qs) =
trans^PQR p q ∷ λ where .force → transitive trans^PQR (ps .force) (qs .force)
-- Pointwise Equality as a Bisimilarity
------------------------------------------------------------------------
module _ {ℓ} {A : Set ℓ} where
infix 1 _,_⊢_≈_
_,_⊢_≈_ : ∀ i m → Covec A ∞ m → Covec A ∞ m → Set ℓ
_,_⊢_≈_ i m = Bisim _≡_ i m m
refl : ∀ {i m} → Reflexive (i , m ⊢_≈_)
refl = reflexive ≡.refl
sym : ∀ {i m} → Symmetric (i , m ⊢_≈_)
sym = symmetric ≡.sym
trans : ∀ {i m} → Transitive (i , m ⊢_≈_)
trans = transitive ≡.trans
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