------------------------------------------------------------------------
-- A coinductive definition of weak similarity
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe --sized-types #-}

open import Labelled-transition-system

module Similarity.Weak {} (lts : LTS ) where

open import Equality.Propositional
open import Prelude
open import Size

open import Bisimilarity.Weak lts as WB using ([_]_≈_; [_]_≈′_)
open import Expansion lts as E using ([_]_≳_; [_]_≳′_)
open import Indexed-container hiding (⟨_⟩)
open import Relation
open import Similarity lts as S using ([_]_≤_; [_]_≤′_)
import Similarity.General

open LTS lts

private
  module General = Similarity.General lts _[_]⇒̂_ ⟶→⇒̂

open General public
  using (module StepC; ⟨_⟩; challenge; force;
         [_]_≡_; [_]_≡′_; []≡↔; Extensionality; extensionality)
  renaming ( reflexive-≤ to reflexive-≼
           ; reflexive-≤′ to reflexive-≼′
           ; ≡⇒≤ to ≡⇒≼
           ; ≤:_ to ≼:_
           ; ≤′:_ to ≼′:_
           )

-- StepC is given in the following way, rather than via open public,
-- to make hyperlinks to it more informative.

StepC : Container (Proc × Proc) (Proc × Proc)
StepC = General.StepC

-- The following definitions are given explicitly, in order to make
-- the code easier to follow.

Weak-similarity : Size  Rel₂  Proc
Weak-similarity = ν StepC

Weak-similarity′ : Size  Rel₂  Proc
Weak-similarity′ = ν′ StepC

infix 4 [_]_≼_ [_]_≼′_ _≼_ _≼′_

[_]_≼_ : Size  Proc  Proc  Set 
[ i ] p  q = ν StepC i (p , q)

[_]_≼′_ : Size  Proc  Proc  Set 
[ i ] p ≼′ q = ν′ StepC i (p , q)

_≼_ : Proc  Proc  Set 
_≼_ = [  ]_≼_

_≼′_ : Proc  Proc  Set 
_≼′_ = [  ]_≼′_

private

  -- However, these definitions are definitionally equivalent to
  -- corresponding definitions in General.

  indirect-Weak-similarity : Weak-similarity  General.Similarity
  indirect-Weak-similarity = refl

  indirect-Weak-similarity′ : Weak-similarity′  General.Similarity′
  indirect-Weak-similarity′ = refl

  indirect-[]≼ : [_]_≼_  General.[_]_≤_
  indirect-[]≼ = refl

  indirect-[]≼′ : [_]_≼′_  General.[_]_≤′_
  indirect-[]≼′ = refl

  indirect-≼ : _≼_  General._≤_
  indirect-≼ = refl

  indirect-≼′ : _≼′_  General._≤′_
  indirect-≼′ = refl

mutual

  -- Weak bisimilarity is contained in weak similarity.

  ≈⇒≼ :  {i p q}  [ i ] p  q  [ i ] p  q
  ≈⇒≼ = λ p≈q 
      q⟶q′ 
         let p′ , p⇒̂p′ , p′≈′q′ = WB.left-to-right p≈q q⟶q′
         in p′ , p⇒̂p′ , ≈⇒≼′ p′≈′q′)
    

  ≈⇒≼′ :  {i p q}  [ i ] p ≈′ q  [ i ] p ≼′ q
  force (≈⇒≼′ p≳′q) = ≈⇒≼ (S.force p≳′q)

mutual

  -- Similarity is contained in weak similarity.

  ≤⇒≼ :  {i p q}  [ i ] p  q  [ i ] p  q
  ≤⇒≼ = λ p≤q 
      q⟶q′ 
         let p′ , p⟶p′ , p′≤′q′ = S.challenge p≤q q⟶q′
         in p′ , ⟶→⇒̂ p⟶p′ , ≤⇒≼′ p′≤′q′)
    

  ≤⇒≼′ :  {i p q}  [ i ] p ≤′ q  [ i ] p ≼′ q
  force (≤⇒≼′ p≳′q) = ≤⇒≼ (S.force p≳′q)

-- Weak similarity is a weak simulation (of a certain kind).

weak-is-weak⇒̂ :
   {p p′ q μ} 
  p  q  p [ μ ]⇒̂ p′ 
   λ q′  q [ μ ]⇒̂ q′ × p′  q′
weak-is-weak⇒̂ = is-weak⇒̂ challenge  p≼′q  force p≼′q) ⇒̂→⇒ id

mutual

  -- Weak similarity is transitive.
  --
  -- Note that the size of the second argument is not preserved.
  --
  -- TODO: Can one prove that the size cannot be preserved?

  transitive-≼ :  {i p q r}  [ i ] p  q  q  r  [ i ] p  r
  transitive-≼ p≼q q≼r =
      p⟶p′ 
         let q′ , q⇒̂q′ , p′≼q′ = challenge p≼q p⟶p′
             r′ , r⇒̂r′ , q′≼r′ = weak-is-weak⇒̂ q≼r q⇒̂q′
         in r′ , r⇒̂r′ , transitive-≼′ p′≼q′ q′≼r′)
    

  transitive-≼′ :
     {i p q r}  [ i ] p ≼′ q  q  r  [ i ] p ≼′ r
  force (transitive-≼′ p≼q q≼r) = transitive-≼ (force p≼q) q≼r

mutual

  -- A fully size-preserving transitivity-like lemma.
  --
  -- Note that expansion could be replaced by a kind of one-sided
  -- expansion.

  transitive-≳≼ :  {i p q r}  [ i ] p  q  [ i ] q  r  [ i ] p  r
  transitive-≳≼ p≳q q≼r =
      p⟶p′  case E.left-to-right p≳q p⟶p′ of λ where
                  (_ , done s , p′≳q) 
                    _ , silent s done
                      , transitive-≳≼′
                          p′≳q (record { force = λ { {_}  q≼r } })

                  (q′ , step q⟶q′ , p′≳q′) 
                    let r′ , r⇒̂r′ , q′≼r′ = challenge q≼r q⟶q′
                    in r′ , r⇒̂r′ , transitive-≳≼′ p′≳q′ q′≼r′)
    

  transitive-≳≼′ :
     {i p q r}  [ i ] p ≳′ q  [ i ] q ≼′ r  [ i ] p ≼′ r
  force (transitive-≳≼′ p≼q q≼r) =
    transitive-≳≼ (force p≼q) (force q≼r)