----------------------------------------------------------------------------------------------------
-- Simulations
----------------------------------------------------------------------------------------------------

{-# OPTIONS --cubical #-}

open import Cubical.Foundations.Prelude

open import Cubical.Data.Nat
open import Cubical.Data.Sigma

open import Cubical.Relation.Binary
open BinaryRelation

module Simulations {ℓ₁ ℓ₂} (A : Type ℓ₁) (_≼_ : A → A → Type ℓ₂) where


_simulated-by_ : (f g : ℕ → A) → Type _
f simulated-by g = ∀ k → ∃[ n ∈ ℕ ] f k ≼ g n

_bisimilar-to_ : (f g : ℕ → A) → Type _
f bisimilar-to g = f simulated-by g × g simulated-by f


{- Strong (bi)simulations and their properties -}

_strongly-simulated-by_ : (f g : ℕ → A) → Type _
f strongly-simulated-by g = ∀ k → Σ[ n ∈ ℕ ] f k ≼ g n

_strongly-bisimilar-to_ : (f g : ℕ → A) → Type _
f strongly-bisimilar-to g = f strongly-simulated-by g × g strongly-simulated-by f

sim-trans : isTrans _≼_ → ∀ {f g h} →
            f strongly-simulated-by g → g strongly-simulated-by h → f strongly-simulated-by h
sim-trans ≼-trans {f} {g} {h} f-g-sim g-h-sim k = n , ≼-trans _ _ _ fk≼gm gm≼hn
  where
  m = fst (f-g-sim k)
  fk≼gm = snd (f-g-sim k)
  n = fst (g-h-sim m)
  gm≼hn = snd (g-h-sim m)

bisim-sym : ∀ {f} {g} → f strongly-bisimilar-to g → g strongly-bisimilar-to f
bisim-sym (f-g-sim , g-f-sim) = (g-f-sim , f-g-sim)

bisim-trans : isTrans _≼_ → ∀ {f g h} →
              f strongly-bisimilar-to g → g strongly-bisimilar-to h → f strongly-bisimilar-to h
bisim-trans ≼-trans (f-g-sim , g-f-sim) (g-h-sim , h-g-sim) =
  sim-trans ≼-trans f-g-sim g-h-sim , sim-trans ≼-trans h-g-sim g-f-sim