module Relation where
open import GeneralLemmas
infix 1 _↔_
Rel : Set → Set → Set₁
Rel A B = A → B → Set
Predicate : Set → Set₁
Predicate A = A → Set
_preserves_ : ∀ {A} → (_R_ : Rel A A)(P : Predicate A) → Set
_preserves_ {A} _R_ P = {a b : A} → a R b → P a → P b
data _* {A : Set}(R : Rel A A)(a : A) : A → Set where
[] : (R *) a a
_∷_ : {b c : A} → R a b → (R *) b c → (R *) a c
preserves* : {A : Set}{_⟶_ : Rel A A}{P : Predicate A} → _⟶_ preserves P → _⟶_ * preserves P
preserves* f [] Pa = Pa
preserves* f (x ∷ xs) Pa = preserves* f xs (f x Pa)
data _⁺ {A : Set}(R : Rel A A)(a : A) : A → Set where
[_] : {b : A} → R a b → (R ⁺) a b
_∷_ : {b c : A} → R a b → (R ⁺) b c → (R ⁺) a c
⁺-to-* : {A : Set}{a b : A}{R : Rel A A} → (R ⁺) a b → (R *) a b
⁺-to-* [ x ] = x ∷ []
⁺-to-* (x ∷ xs) = x ∷ ⁺-to-* xs
_⁺++*_ : {A : Set}{a b c : A}{R : Rel A A} → (R ⁺) a b → (R *) b c → (R *) a c
[ x ] ⁺++* ys = x ∷ ys
(x ∷ xs) ⁺++* ys = x ∷ (xs ⁺++* ys)
_⁻¹ : ∀ {A B} → Rel A B → Rel B A
(R ⁻¹) b a = R a b
_∘ᵣ_ : ∀ {A B C} → Rel B C → Rel A B → Rel A C
(R ∘ᵣ S) a c = ∃ λ b → S a b × R b c
composition-inverse : ∀ {A B C}{R : Rel B C}{S : Rel A B} a c → ((R ∘ᵣ S) ⁻¹) c a → ((S ⁻¹) ∘ᵣ (R ⁻¹)) c a
composition-inverse a c (b , Sab , Rbc) = b , Rbc , Sab
_is-deterministic-at_ : {A B : Set}(R : Rel A B)(x : A) → Set
_R_ is-deterministic-at a = ∀ {b b'} → a R b → a R b' → b ≡ b'
_is-deterministic : {A B : Set}(R : Rel A B) → Set
R is-deterministic = ∀ {a} → R is-deterministic-at a
_is-decidable : {A B : Set}(_R_ : Rel A B) → Set
_R_ is-decidable = ∀ a → Dec (∃ λ b → a R b)
all_are_ : {A B : Set} → (A → B) → Predicate B → Set
all f are P = ∀ n → P (f n)
all_except_are_ : {A B : Set} → (A → B) → A → Predicate B → Set
all f except n are P = ∀ n' → n' ≢ n → P (f n')
module Simulation {A B : Set}(_⟶_ : Rel A A)(_⟶'_ : Rel B B) where
Presimulation : (_R_ : Rel A B) → Set
Presimulation _R_ = ∀ a a' b → a ⟶ a' → a R b → ∃ λ b' → b ⟶' b'
Simulation : (_R_ : Rel A B) → Set
Simulation _R_ = ∀ a a' b → a ⟶ a' → a R b → ∃ λ b' → b ⟶' b' × a' R b'
_≤_ : A → B → Set₁
p ≤ q = ∃ λ _R_ → Simulation _R_ × p R q
open Simulation using (Simulation; Presimulation) public
_∘sim_ : ∀ {A B C}{O : Rel A A}{P : Rel B B}{Q : Rel C C}{R₁ : Rel A B}{R₂ : Rel B C}
→ Simulation P Q R₂ → Simulation O P R₁ → Simulation O Q (R₂ ∘ᵣ R₁)
(sim₂ ∘sim sim₁) a a' c step₁ (b , R₁ab , R₂bc) =
let
(b' , step₂ , R₁a'b') = sim₁ a a' b step₁ R₁ab
(c' , step₃ , R₂b'c') = sim₂ b b' c step₂ R₂bc
in c' , step₃ , b' , R₁a'b' , R₂b'c'
module Bisimulation {A B : Set}(⟶ : Rel A A)(⟶' : Rel B B) where
Bisimulation : (R : Rel A B) → Set
Bisimulation R = Simulation ⟶ ⟶' R × Simulation ⟶' ⟶ (R ⁻¹)
_~_ : A → B → Set₁
p ~ q = ∃ λ _R_ → Bisimulation _R_ × p R q
presimulation-to-simulation : (_R_ : Rel A B)
→ Simulation ⟶ ⟶' _R_
→ Presimulation ⟶' ⟶ (_R_ ⁻¹)
→ (∀ a b → a R b → ⟶' is-deterministic-at b)
→ Simulation ⟶' ⟶ (_R_ ⁻¹)
presimulation-to-simulation R sim presim det = sim⁻¹
where
sim⁻¹ : Simulation ⟶' ⟶ (R ⁻¹)
sim⁻¹ b b' a bstep aRb
= let (a' , astep) = presim b b' a bstep aRb
(b'' , bstep' , a'Rb'') = sim a a' b astep aRb
in a' , astep , subst (λ b'' → R a' b'') (sym (det a b aRb bstep bstep')) a'Rb''
simulation-to-bisimulation : (_R_ : Rel A B)
→ Simulation ⟶ ⟶' _R_
→ Presimulation ⟶' ⟶ (_R_ ⁻¹)
→ (∀ a b → a R b → ⟶' is-deterministic-at b)
→ Bisimulation _R_
simulation-to-bisimulation R sim presim det = sim , presimulation-to-simulation R sim presim det
open Bisimulation using (Bisimulation) public
_∘bisim_ : ∀ {A B C}{O : Rel A A}{P : Rel B B}{Q : Rel C C}{R₁ : Rel A B}{R₂ : Rel B C}
→ Bisimulation P Q R₂ → Bisimulation O P R₁ → Bisimulation O Q (R₂ ∘ᵣ R₁)
((sim₂ , sim₂⁻¹) ∘bisim (sim₁ , sim₁⁻¹)) = (sim₂ ∘sim sim₁) , sim'
where
sim' : Simulation _ _ _
sim' c c' a Qcc' R₂∘R₁⁻¹cc' =
let (a' , Oaa' , b , R₂bc' , R₁a'b) = (sim₁⁻¹ ∘sim sim₂⁻¹) c c' a Qcc' (composition-inverse c c' R₂∘R₁⁻¹cc')
in a' , Oaa' , b , R₁a'b , R₂bc'
_↔_ : Set → Set → Set
A ↔ B = (A → B) × (B → A)
↑ : {A : Set}(⟶ : Rel A A) → A → Set
↑ ⟶ a = ∀ b → (⟶ *) a b → ∃ λ c → ⟶ b c
divergence-simulation-dec-det : ∀ {A B}{⟶ : Rel A A}{⟶' : Rel B B}{R : Rel A B}{P : B → Set}(a : A)(b : B) →
Simulation ⟶ (⟶' ⁺) R →
⟶ is-decidable →
⟶' preserves P →
(∀ b → P b → ⟶' is-deterministic-at b) →
R a b → P b →
↑ ⟶ a → ↑ ⟶' b
divergence-simulation-dec-det a b sim dec pres det Rab Pb a↑ b'' bsteps with dec a
divergence-simulation-dec-det a b sim dec pres det Rab Pb a↑ b'' bsteps | yes (a' , astep) with sim a a' b astep Rab
... | b' , bsteps' , Ra'b' = lemma a' b b' b'' sim dec pres det Pb (λ a asteps → a↑ a (astep ∷ asteps)) bsteps bsteps' Ra'b'
where
lemma : ∀ {A B}{⟶ : Rel A A}{⟶' : Rel B B}{R : Rel A B}{P : B → Set}(a : A)(b b' b'' : B) →
Simulation ⟶ (⟶' ⁺) R →
⟶ is-decidable →
⟶' preserves P →
(∀ b → P b → ⟶' is-deterministic-at b) →
P b →
↑ ⟶ a → (⟶' *) b b'' →
(⟶' ⁺) b b' → R a b' →
∃ λ b''' → ⟶' b'' b'''
lemma a b b' .b sim dec pres det Pb a↑ [] [ bstep ] Rab' = b' , bstep
lemma a b b' .b sim dec pres det Pb a↑ [] (bstep ∷ bsteps') Rab' = _ , bstep
lemma a b b' b'' sim dec pres det Pb a↑ (bstep ∷ bsteps) [ bstep' ] Rab' =
let (a' , astep) = a↑ a []
a'↑ = λ a'' asteps → a↑ a'' (astep ∷ asteps)
(b''' , bsteps' , Ra'b') = sim a a' b' astep Rab'
b≡b' : _ ≡ b'
b≡b' = det b Pb bstep bstep'
bsteps'' = subst (λ p → (_ ⁺) p _) (sym b≡b') bsteps'
(b''' , step) = lemma a' _ _ _ sim dec pres det (pres bstep Pb) a'↑ bsteps bsteps'' Ra'b'
in b''' , step
lemma a b b' b'' sim dec pres det Pb a↑ (bstep ∷ bsteps) (bstep' ∷ bsteps') Rab' =
let b≡b' : _ ≡ _
b≡b' = det b Pb bstep bstep'
bsteps'' = subst (λ p → (_ ⁺) p _) (sym b≡b') bsteps'
in lemma a _ b' b'' sim dec pres det (pres bstep Pb) a↑ bsteps bsteps'' Rab'
divergence-simulation-dec-det a b sim dec pres det Rab Pb a↑ b'' bsteps | no ¬p =
let astep = a↑ a []
in ⊥-elim (¬p astep)
open Bisimulation using (_~_)
divergence-bisimulation : ∀ {A B}{⟶ : Rel A A}{⟶' : Rel B B}(a : A)(b : B) → _~_ ⟶ ⟶' a b → ↑ ⟶ a ↔ ↑ ⟶' b
divergence-bisimulation a b (R , (sim , sim⁻¹) , Rab) = (⇒ a b (R , (sim , sim⁻¹) , Rab))
, ⇒ b a ((R ⁻¹) , (sim⁻¹ , sim) , Rab)
where
⇒ : ∀ {A B}{⟶ : Rel A A}{⟶' : Rel B B}(a : A)(b : B) → _~_ ⟶ ⟶' a b → ↑ ⟶ a → ↑ ⟶' b
⇒ a b (R , (sim , sim⁻¹) , Rab) a↑ .b [] =
let (a' , step) = a↑ a []
(b' , step' , Ra'b') = sim a a' b step Rab
in b' , step'
⇒ a b (R , (sim , sim⁻¹) , Rab) a↑ b' (bstep ∷ bsteps) =
let (a' , astep , Ra'b') = sim⁻¹ b _ a bstep Rab
a'↑ = λ a'' asteps → a↑ a'' (astep ∷ asteps)
in ⇒ a' _ (R , (sim , sim⁻¹) , Ra'b') a'↑ b' bsteps