-- Some auxiliary definitions related to binary relations
module Relation where

open import GeneralLemmas

infix 1 _↔_

-- | Heterogeneous binary relations
Rel : Set  Set  Set₁
Rel A B = A  B  Set

Predicate : Set  Set₁
Predicate A = A  Set

-- | Property-preserving relations
_preserves_ :  {A}  (_R_ : Rel A A)(P : Predicate A)  Set
_preserves_ {A} _R_ P = {a b : A}  a R b  P a  P b

-- | The reflexive transitive closure of a binary relation
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)

-- | The transitive closure of a binary relation
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)

-- | The inverse of a relation
_⁻¹ :  {A B}  Rel A B  Rel B A
(R ⁻¹) b a = R a b

-- | Relation composition
_∘ᵣ_ :  {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

-- * Determinism
_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

-- * Decidable relations
-- This is perhaps not the standard definition. This is decidability
-- of whether a is in the domain of the relation.
_is-decidable : {A B : Set}(_R_ : Rel A B)  Set
_R_ is-decidable =  a  Dec ( λ b  a R b)

-- * Some predicates ranging over the codomain of a function
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')

-- * Simulations
module Simulation {A B : Set}(_⟶_ : Rel A A)(_⟶'_ : Rel B B) where
  -- | TODO:  Is there a standard name for this?
  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'

  -- | q simulates p when p ≤ q
  _≤_ : A  B  Set₁
  p  q =  λ _R_  Simulation _R_ × p R q

open Simulation using (Simulation; Presimulation) public

-- | Simulation composition
_∘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'

-- * Bisimulations
module Bisimulation {A B : Set}( : Rel A A)(⟶' : Rel B B) where
  Bisimulation : (R : Rel A B)  Set
  Bisimulation R = Simulation  ⟶' R × Simulation ⟶'  (R ⁻¹)

  -- | p is bisimilar to q when p ~ q
  _~_ : 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

-- | Bisimulation composition
_∘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)

-- * Divergence
 : {A : Set}( : Rel A A)  A  Set
  a =  b  ( *) a b   λ c   b c

-- | This is a bit specialised, but a useful lemma
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