------------------------------------------------------------------------
-- Some exercises and results from "Enhancements of the bisimulation
-- proof method" by Pous and Sangiorgi, as well as other results,
-- related to an LTS from Section 6.2.5 in the aforementioned chapter
--
-- Implemented using the coinductive definition of bisimilarity.
------------------------------------------------------------------------

{-# OPTIONS --without-K #-}

module Bisimilarity.Exercises.Coinductive.6-2-5 {Name : Set} where

open import Equality.Propositional
open import Logical-equivalence using (_⇔_)
open import Prelude

open import Function-universe equality-with-J hiding (id; _∘_)

import Bisimilarity.Coinductive.Equational-reasoning-instances
open import Equational-reasoning
open import Indexed-container using (⟦_⟧)
open import Labelled-transition-system.6-2-5 Name
open import Relation

open import Bisimilarity.Coinductive 6-2-5
open import Bisimilarity.Up-to 6-2-5

-- Some simple lemmas.

op·∅ :  {a}  op (a · )  
op·∅ {a} =  lr ,  ()) 
  where
  lr :  {P′ μ} 
       op (a · ) [ μ ]⟶ P′ 
        λ Q′   [ μ ]⟶ Q′ × P′ ∼′ Q′
  lr (op action ())

op··∅ :  {a}  op (a · a · )  a · 
op··∅ {a} =  lr , rl 
  where
  lr :  {P′ μ b} 
       op (a · b · ) [ μ ]⟶ P′ 
        λ Q′  b ·  [ μ ]⟶ Q′ × P′ ∼′ Q′
  lr (op action action) = _ , action , reflexive

  rl :  {Q′ μ} 
       a ·  [ μ ]⟶ Q′ 
        λ P′  op (a · a · ) [ μ ]⟶ P′ × P′ ∼′ Q′
  rl action = _ , op action action , reflexive

a≁b·c :  {a b c}  ¬ (a ·   b · c · )
a≁b·c a∼b·c with right-to-left a∼b·c action
... | . , action , ∅∼a with right-to-left (force ∅∼a) action
...   | _ , () , _

-- a ·_ preserves bisimilarity (in a size-preserving way).

·-cong :  {i a P Q}  [ i ] P  Q  [ i ] a · P  a · Q
·-cong {i} {a} P∼Q =
   lr P∼Q
  , Σ-map id (Σ-map id symmetric)  lr (symmetric P∼Q)
  
  where
  lr :  {P P′ Q μ} 
       [ i ] P  Q  a · P [ μ ]⟶ P′ 
        λ Q′  a · Q [ μ ]⟶ Q′ × [ i ] P′ ∼′ Q′
  lr P∼Q action = _ , action , convert P∼Q

-- op preserves bisimilarity. Note that this lemma is not necessarily
-- size-preserving.

op-cong :  {i} {j : Size< i} {P Q} 
          [ i ] P  Q  [ j ] op P  op Q
op-cong {i} {j} P∼Q =
   lr P∼Q
  , Σ-map id (Σ-map id symmetric)  lr (symmetric P∼Q)
  
  where
  lr :  {P P′ Q μ} 
       [ i ] P  Q  op P [ μ ]⟶ P′ 
        λ Q′  op Q [ μ ]⟶ Q′ × [ j ] P′ ∼′ Q′
  lr P∼Q (op P⟶P′ P′⟶P″) =
    let Q′ , Q⟶Q′  , P′∼Q′ = left-to-right        P∼Q    P⟶P′
        Q″ , Q′⟶Q″ , P″∼Q″ = left-to-right (force P′∼Q′) P′⟶P″
    in Q″ , op Q⟶Q′ Q′⟶Q″ , P″∼Q″

-- Let us assume that the Name type is inhabited. In that case op-cong
-- /cannot/ preserve the size of its argument.

op-cong-cannot-preserve-size :
  Name 
  ¬ (∀ {i P Q}  [ i ] P  Q  [ i ] op P  op Q)
op-cong-cannot-preserve-size a op-cong = a≁b·c a∼a·a
  where
  op-cong′ :  {i P Q}  [ i ] P ∼′ Q  [ i ] op P ∼′ op Q
  force (op-cong′ P∼′Q) = op-cong (force P∼′Q)

  a∼a·a :  {i}  [ i ] a ·   a · a · 
  a∼a·a {i} =  lr , rl 
    where
    a∼′a·a :  {i}  [ i ] a ·  ∼′ a · a · 
    force a∼′a·a = a∼a·a

    lemma = ∼′:
                     ∼⟨ symmetric op·∅ 
      op (a · )      ∼⟨ op-cong′ (a∼′a·a {i = i}) 
      op (a · a · )  ∼⟨ op··∅ ⟩■
      a · 

    lr :  {P′ μ} 
         a ·  [ μ ]⟶ P′ 
          λ Q′  a · a ·  [ μ ]⟶ Q′ × [ i ] P′ ∼′ Q′
    lr action = a ·  , action , lemma

    rl :  {Q′ μ} 
         a · a ·  [ μ ]⟶ Q′ 
          λ P′  a ·  [ μ ]⟶ P′ × [ i ] P′ ∼′ Q′
    rl action =  , action , lemma

-- Up to context (for monadic contexts).

Up-to-context : Trans₂ (# 0) Proc
Up-to-context R (P , Q) =
   λ (C : Context 1) 
   λ P′ 
   λ Q′ 
  P  C [  _  P′) ]
    ×
  Q  C [  _  Q′) ]
    ×
  R (P′ , Q′)

-- Up to context is monotone.

Up-to-context-monotone : Monotone Up-to-context
Up-to-context-monotone R⊆S =
  Σ-map id $ Σ-map id $ Σ-map id $ Σ-map id $ Σ-map id R⊆S

-- Up to bisimilarity and context.

Up-to-bisimilarity-and-context : Trans₂ (# 0) Proc
Up-to-bisimilarity-and-context =
  Up-to-bisimilarity  Up-to-context

-- Up to bisimilarity and context is monotone.

Up-to-bisimilarity-and-context-monotone :
  Monotone Up-to-bisimilarity-and-context
Up-to-bisimilarity-and-context-monotone =
  Up-to-bisimilarity-monotone  Up-to-context-monotone

-- Up to bisimilarity and context is not sound (assuming that Name is
-- inhabited).

¬-up-to-bisimilarity-and-context :
  Name 
  ¬ Up-to-technique Up-to-bisimilarity-and-context
¬-up-to-bisimilarity-and-context a =
  Up-to-technique Up-to-bisimilarity-and-context  ↝⟨ _$ R⊆ 
  R  Bisimilarity                               ↝⟨ R⊈∼ ⟩□
                                                 
  where
  data R : Rel₂ (# 0) Proc where
    base : R (a ·  , a · a · )

  lemma : Up-to-bisimilarity-and-context R ( , a · )
  lemma =
    op (a · ) ,
    symmetric op·∅ ,
    op (a · a · ) ,
    (op (hole fzero) , a ·  , a · a ·  , refl , refl , base) ,
    op··∅

  R⊆ : R   S̲t̲e̲p̲  (Up-to-bisimilarity-and-context R)
  R⊆ base =
      { action  a ·  , action , lemma })
    ,  { action       , action , lemma })
    

  R⊈∼ : ¬ R  Bisimilarity 
  R⊈∼ =
    R  Bisimilarity   ↝⟨  R⊆∼  R⊆∼ base) 
    a ·   a · a ·    ↝⟨ a≁b·c ⟩□
                       

-- The last result above can be used to give another proof showing
-- that op-cong cannot preserve the size of its argument (assuming
-- that Name is inhabited).

op-cong-cannot-preserve-size′ :
  Name 
  ¬ (∀ {i P Q}  [ i ] P  Q  [ i ] op P  op Q)
op-cong-cannot-preserve-size′ a =
  (∀ {i P Q}  [ i ] P  Q  [ i ] op P  op Q)               ↝⟨  op-cong C P∼Q  []-cong op-cong C  _  P∼Q)) 

  (∀ {i P Q} (C : Context 1)  [ i ] P  Q 
   [ i ] C [  _  P) ]  C [  _  Q) ])                   ↝⟨  []-cong  λ where
                                                                    {x = P , Q} (_ , P∼C[R₁] , _ ,
                                                                                 (C , R₁ , R₂ , refl , refl , R₁∼R₂) , C[R₂]∼Q) 

                                                                      P                 ∼⟨ P∼C[R₁] 
                                                                      C [  _  R₁) ]  ∼⟨ []-cong C R₁∼R₂ 
                                                                      C [  _  R₂) ]  ∼⟨ C[R₂]∼Q ⟩■
                                                                      Q) 
  (∀ {i}  Up-to-bisimilarity-and-context (Bisimilarity i) 
           Bisimilarity i)                                    ↝⟨ _⇔_.from (monotone→⇔ Up-to-bisimilarity-and-context-monotone) 

  Size-preserving Up-to-bisimilarity-and-context              ↝⟨ size-preserving→up-to 

  Up-to-technique Up-to-bisimilarity-and-context              ↝⟨ ¬-up-to-bisimilarity-and-context a ⟩□

                                                             
  where
  []-cong :
    (∀ {i P Q}  [ i ] P  Q  [ i ] op P  op Q) 
     {i n Ps Qs}
    (C : Context n)  (∀ x  [ i ] Ps x  Qs x) 
    [ i ] C [ Ps ]  C [ Qs ]
  []-cong op-cong (hole x) Ps∼Qs = Ps∼Qs x
  []-cong op-cong (op C)   Ps∼Qs = op-cong ([]-cong op-cong C Ps∼Qs)
  []-cong op-cong (a · C)  Ps∼Qs = ·-cong ([]-cong op-cong C Ps∼Qs)
  []-cong op-cong         Ps∼Qs = reflexive