------------------------------------------------------------------------
-- Some results related to an LTS from Section 6.2.5 of "Enhancements
-- of the bisimulation proof method" by Pous and Sangiorgi,
-- implemented using the coinductive definition of bisimilarity
------------------------------------------------------------------------

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

module Bisimilarity.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.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 6-2-5
open import Bisimilarity.Up-to 6-2-5

-- Some simple lemmas. The first two are stated by Pous and Sangiorgi,
-- and the third one is a generalisation of a result stated by Pous
-- and Sangiorgi.

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
...   | _ , () , _

-- Pous and Sangiorgi note that every context preserves bisimilarity.
-- One can prove that 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

-- The operator op also preserves bisimilarity, but this lemma is not
-- claimed to be 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.
--
-- The proof is based on an argument presented by Pous and Sangiorgi.

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₂ (# ) Proc
Up-to-context R (P , Q) =
  ∃ λ (C : Context ) →
  ∃ λ 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₂ (# ) 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).
--
-- This result is due to Pous and Sangiorgi.

¬-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₂ (# ) 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 ⊆ ⟦ StepC ⟧ (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 ) → [ 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