------------------------------------------------------------------------
-- Some exercises and results related to CCS, mostly from
-- "Enhancements of the bisimulation proof method" by Pous and
-- Sangiorgi
--
-- Implemented using the coinductive definition of bisimilarity.
------------------------------------------------------------------------

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

module Bisimilarity.Exercises.Coinductive.CCS {Name : Set} where

open import Equality.Propositional
open import Prelude

import Bisimilarity.Coinductive.Equational-reasoning-instances
import Bisimilarity.Exercises.Other.CCS
open import Equational-reasoning
open import Labelled-transition-system.CCS Name

open import Bisimilarity.Coinductive CCS
import Labelled-transition-system.Equational-reasoning-instances CCS

------------------------------------------------------------------------
-- Congruence lemmas

-- Some lemmas used to prove the congruence results below as well as
-- similar results in Similarity.Strong.CCS.

module Cong-lemmas
  ({R} R′ : Proc   Proc   Set)
   _ : Convertible R R′ 
   _ : Convertible R′ R′ 
   _ : Convertible _∼_ R′ 
   _ : Transitive R′ R′ 
  (left-to-right :
    {P Q}  R P Q 
    {P′ μ}  P [ μ ]⟶ P′   λ Q′  Q [ μ ]⟶ Q′ × R′ P′ Q′)
  where

  private

    infix -2 R′:_

    R′:_ :  {P Q}  R′ P Q  R′ P Q
    R′:_ = id

    infix -3 lr-result

    lr-result :
       {P′ Q Q′} μ  R′ P′ Q′  Q [ μ ]⟶ Q′ 
       λ Q′  Q [ μ ]⟶ Q′ × R′ P′ Q′
    lr-result _ P′∼′Q′ Q⟶Q′ = _ , Q⟶Q′ , P′∼′Q′

    syntax lr-result μ P′∼′Q′ Q⟶Q′ = P′∼′Q′ [ μ ]⟵ Q⟶Q′

  ∣-cong :
    (∀ {P P′ Q Q′}  R′ P P′  R′ Q Q′  R′ (P  Q) (P′  Q′)) 
     {P₁ P₂ Q₁ Q₂ S₁ μ} 
    R P₁ P₂  R Q₁ Q₂  P₁  Q₁ [ μ ]⟶ S₁ 
     λ S₂  P₂  Q₂ [ μ ]⟶ S₂ × R′ S₁ S₂
  ∣-cong _∣-cong′_ P₁∼P₂ Q₁∼Q₂ = λ where
    (par-left  tr)   Σ-map (_∣ _)
                        (Σ-map par-left
                               (_∣-cong′ convert Q₁∼Q₂))
                        (left-to-right P₁∼P₂ tr)
    (par-right tr)   Σ-map (_ ∣_)
                        (Σ-map par-right
                               (convert P₁∼P₂ ∣-cong′_))
                        (left-to-right Q₁∼Q₂ tr)
    (par-τ tr₁ tr₂)  Σ-zip _∣_ (Σ-zip par-τ _∣-cong′_)
                        (left-to-right P₁∼P₂ tr₁)
                        (left-to-right Q₁∼Q₂ tr₂)

  ⊕-cong :
     {P₁ P₁′ P₂ P₂′ S μ} 
    R P₁ P₁′  R P₂ P₂′  P₁  P₂ [ μ ]⟶ S 
     λ S′  P₁′  P₂′ [ μ ]⟶ S′ × R′ S S′
  ⊕-cong {P₁} {P₁′} {P₂} {P₂′} {S} {μ} P₁∼P₁′ P₂∼P₂′ = λ where
    (choice-left P₁⟶S)  case left-to-right P₁∼P₁′ P₁⟶S of λ where
      (S′ , P₁′⟶S′ , S∼′S′) 
        S          ∼⟨ S∼′S′ ⟩■
        S′
          [ μ ]⟵   ←⟨ choice-left P₁′⟶S′ ⟩■
        P₁′  P₂′

    (choice-right P₂⟶S)  case left-to-right P₂∼P₂′ P₂⟶S of λ where
      (S′ , P₂′⟶S′ , S∼′S′) 
        S          ∼⟨ S∼′S′ ⟩■
        S′
          [ μ ]⟵   ←⟨ choice-right P₂′⟶S′ ⟩■
        P₁′  P₂′

  ·′-cong :
     {P₁ P₂ Q₁ μ μ′} 
    R′ (force P₁) (force P₂)  μ ·′ P₁ [ μ′ ]⟶ Q₁ 
     λ Q₂  μ ·′ P₂ [ μ′ ]⟶ Q₂ × R′ Q₁ Q₂
  ·′-cong {P₁} {P₂} {μ = μ} P₁∼P₂ action =
    force P₁  ∼⟨ P₁∼P₂ ⟩■
    force P₂
      [ μ ]⟵  ←⟨ _[_]⟶_.action ⟩■
    μ ·′ P₂

  ν-cong :
    (∀ {a P P′}  R′ P P′  R′ (ν a P) (ν a P′)) 
     {a μ P P′ Q} 
    R P P′  ν a P [ μ ]⟶ Q 
     λ Q′  ν a P′ [ μ ]⟶ Q′ × R′ Q Q′
  ν-cong ν-cong′ {a} {μ} {P′ = P′} P∼P′ (restriction {P′ = Q} a∉μ P⟶Q) =
    case left-to-right P∼P′ P⟶Q of λ where
      (Q′ , P′⟶Q′ , Q∼′Q′) 
        ν a Q     ∼⟨ ν-cong′ Q∼′Q′ ⟩■
        ν a Q′
          [ μ ]⟵  ←⟨ restriction a∉μ P′⟶Q′ ⟩■
        ν a P′

  !-cong :
    (∀ {μ P P₀} 
     ! P [ μ ]⟶ P₀ 
     ( λ P′  P [ μ ]⟶ P′ × P₀  ! P  P′)
       
     (μ  τ ×  λ P′   λ P″   λ a 
      P [ name a ]⟶ P′ × P [ name (co a) ]⟶ P″ ×
      P₀  (! P  P′)  P″)) 
    (∀ {P P′ Q Q′}  R′ P P′  R′ Q Q′  R′ (P  Q) (P′  Q′)) 
    (∀ {P P′}  R′ P P′  R′ (! P) (! P′)) 
     {P P′ Q μ} 
    R P P′  ! P [ μ ]⟶ Q 
     λ Q′  ! P′ [ μ ]⟶ Q′ × R′ Q Q′
  !-cong 6-1-3-2 _∣-cong′_ !-cong′_ {P} {P′} {Q} {μ} P∼P′ !P⟶Q =
    case 6-1-3-2 !P⟶Q of λ where

      (inj₁ (P″ , P⟶P″ , Q∼!P∣P″)) 
        let Q′ , P′⟶Q′ , P″∼′Q′ = left-to-right P∼P′ P⟶P″
        in
        Q          ∼⟨ R′: convert Q∼!P∣P″ 
        ! P   P″  ∼⟨ (!-cong′ convert P∼P′) ∣-cong′ P″∼′Q′ ⟩■
        ! P′  Q′
          [ μ ]⟵   ←⟨ replication (par-right P′⟶Q′) ⟩■
        ! P′

      (inj₂ (refl , P″ , P‴ , a , P⟶P″ , P⟶P‴ , Q∼!P∣P″∣P‴)) 
        let Q′ , P′⟶Q′ , P″∼′Q′ = left-to-right P∼P′ P⟶P″
            Q″ , P′⟶Q″ , P‴∼′Q″ = left-to-right P∼P′ P⟶P‴
        in
        Q                 ∼⟨ R′: convert Q∼!P∣P″∣P‴ 
        (! P  P″)  P‴   ∼⟨ ((!-cong′ convert P∼P′) ∣-cong′ P″∼′Q′) ∣-cong′ P‴∼′Q″ ⟩■
        (! P′  Q′)  Q″
          [ τ ]⟵          ←⟨ replication (par-τ (replication (par-right P′⟶Q′)) P′⟶Q″) ⟩■
        ! P′

private
  module CL {i} = Cong-lemmas [ i ]_∼′_ left-to-right

------------------------------------------------------------------------
-- Various lemmas related to _∣_

mutual

  -- _∣_ is commutative.

  ∣-comm :  {P Q i}  [ i ] P  Q  Q  P
  ∣-comm {i = i} =  lr , Σ-map id (Σ-map id symmetric)  lr 
    where
    lr :  {P P′ Q μ} 
         P  Q [ μ ]⟶ P′ 
          λ Q′  Q  P [ μ ]⟶ Q′ × [ i ] P′ ∼′ Q′
    lr (par-left tr)   = _ , par-right tr , ∣-comm′
    lr (par-right tr)  = _ , par-left tr , ∣-comm′
    lr (par-τ tr₁ tr₂) =
        _
      , par-τ tr₂ (subst  a  _ [ name a ]⟶ _)
                         (sym $ co-involutive _)
                         tr₁)
      , ∣-comm′

  ∣-comm′ :  {P Q i}  [ i ] P  Q ∼′ Q  P
  force ∣-comm′ = ∣-comm

mutual

  -- _∣_ is associative.

  ∣-assoc :  {P Q R i}  [ i ] P  (Q  R)  (P  Q)  R
  ∣-assoc {i = i} =  lr , rl 
    where
    lr :  {P Q R P′ μ} 
         P  (Q  R) [ μ ]⟶ P′ 
          λ Q′  (P  Q)  R [ μ ]⟶ Q′ × [ i ] P′ ∼′ Q′
    lr (par-left tr)               = _ , par-left (par-left tr)    , ∣-assoc′
    lr (par-right (par-left tr))   = _ , par-left (par-right tr)   , ∣-assoc′
    lr (par-right (par-right tr))  = _ , par-right tr              , ∣-assoc′
    lr (par-right (par-τ tr₁ tr₂)) = _ , par-τ (par-right tr₁) tr₂ , ∣-assoc′
    lr (par-τ tr₁ (par-left tr₂))  = _ , par-left (par-τ tr₁ tr₂)  , ∣-assoc′
    lr (par-τ tr₁ (par-right tr₂)) = _ , par-τ (par-left tr₁) tr₂  , ∣-assoc′

    rl :  {P Q R Q′ μ} 
         (P  Q)  R [ μ ]⟶ Q′ 
          λ P′  P  (Q  R) [ μ ]⟶ P′ × [ i ] P′ ∼′ Q′
    rl (par-left (par-left tr))    = _ , par-left tr               , ∣-assoc′
    rl (par-left (par-right tr))   = _ , par-right (par-left tr)   , ∣-assoc′
    rl (par-left (par-τ tr₁ tr₂))  = _ , par-τ tr₁ (par-left tr₂)  , ∣-assoc′
    rl (par-right tr)              = _ , par-right (par-right tr)  , ∣-assoc′
    rl (par-τ (par-left tr₁) tr₂)  = _ , par-τ tr₁ (par-right tr₂) , ∣-assoc′
    rl (par-τ (par-right tr₁) tr₂) = _ , par-right (par-τ tr₁ tr₂) , ∣-assoc′

  ∣-assoc′ :  {P Q R i}  [ i ] P  (Q  R) ∼′ (P  Q)  R
  force ∣-assoc′ = ∣-assoc

mutual

  -- ∅ is a left identity of _∣_.

  ∣-left-identity :  {P i}  [ i ]   P  P
  ∣-left-identity {i = i} =  lr , rl 
    where

    lr :  {P P′ μ} 
           P [ μ ]⟶ P′ 
          λ Q′  P [ μ ]⟶ Q′ × [ i ] P′ ∼′ Q′
    lr (par-right tr) = _ , tr , ∣-left-identity′
    lr (par-left ())
    lr (par-τ () _)

    rl :  {P Q′ μ} 
         P [ μ ]⟶ Q′ 
          λ P′    P [ μ ]⟶ P′ × [ i ] P′ ∼′ Q′
    rl tr = _ , par-right tr , ∣-left-identity′

  ∣-left-identity′ :  {P i}  [ i ]   P ∼′ P
  force ∣-left-identity′ = ∣-left-identity

-- ∅ is a right identity of _∣_.

∣-right-identity :  {P}  P    P
∣-right-identity {P} =
  P    ∼⟨ ∣-comm 
    P  ∼⟨ ∣-left-identity ⟩■
  P

mutual

  -- _∣_ preserves bisimilarity.

  infix 6 _∣-cong_ _∣-cong′_

  _∣-cong_ :  {i P P′ Q Q′} 
             [ i ] P  P′  [ i ] Q  Q′  [ i ] P  Q  P′  Q′
  P∼P′ ∣-cong Q∼Q′ =
     lr P∼P′ Q∼Q′
    , Σ-map id (Σ-map id symmetric) 
      lr (symmetric P∼P′) (symmetric Q∼Q′)
    
    where
    lr = CL.∣-cong _∣-cong′_

  _∣-cong′_ :  {i P P′ Q Q′} 
              [ i ] P ∼′ P′  [ i ] Q ∼′ Q′  [ i ] P  Q ∼′ P′  Q′
  force (P∼P′ ∣-cong′ Q∼Q′) = force P∼P′ ∣-cong force Q∼Q′

------------------------------------------------------------------------
-- Exercise 6.1.2

private

  -- A compact proof.

  6-1-2-compact :  {P i}  [ i ] ! P  P  ! P
  6-1-2-compact =
      tr  _ , replication tr , reflexive)
    ,  { (replication tr)  _ , tr , reflexive })
    

-- A less compact proof.

6-1-2 :  {P i}  [ i ] ! P  P  ! P
6-1-2 {P} =
    {P′} {μ} tr 
       P′   ∼⟨ ∼′: reflexive ⟩■
       P′   [ μ ]⟵⟨ replication tr 
       ! P)
  ,  { {q′ = P′} {μ = μ} (replication tr) 
         ! P  P  [ μ ]⟶⟨ tr ⟩ʳˡ
         P′       ∼⟨ ∼′: reflexive ⟩■
         P′ })
  

------------------------------------------------------------------------
-- Exercise 6.1.3 (2), plus some rearrangement lemmas

private
  module 6-1-3-2 = Bisimilarity.Exercises.Other.CCS.6-1-3-2 (record
    { _∼_       = _∼_
    ; step-∼    = step-∼
    ; finally-∼ = Equational-reasoning.finally₂
    ; reflexive = reflexive
    ; symmetric = symmetric
    ; ∣-comm    = ∣-comm
    ; ∣-assoc   = ∣-assoc
    ; _∣-cong_  = _∣-cong_
    ; 6-1-2     = 6-1-2
    })

6-1-3-2 :
   {μ P P₀} 
  ! P [ μ ]⟶ P₀ 
  ( λ P′  P [ μ ]⟶ P′ × P₀  ! P  P′)
    
  (μ  τ ×  λ P′   λ P″   λ a 
   P [ name a ]⟶ P′ × P [ name (co a) ]⟶ P″ × P₀  (! P  P′)  P″)
6-1-3-2 = 6-1-3-2.6-1-3-2

swap-rightmost :  {P Q R}  (P  Q)  R  (P  R)  Q
swap-rightmost = 6-1-3-2.swap-rightmost

swap-in-the-middle :  {P Q R S} 
                     (P  Q)  (R  S)  (P  R)  (Q  S)
swap-in-the-middle {P} {Q} {R} {S} =
  (P  Q)  (R  S)  ∼⟨ swap-rightmost 
  (P  (R  S))  Q  ∼⟨ ∣-assoc ∣-cong reflexive 
  ((P  R)  S)  Q  ∼⟨ symmetric ∣-assoc 
  (P  R)  (S  Q)  ∼⟨ reflexive ∣-cong ∣-comm ⟩■
  (P  R)  (Q  S)

------------------------------------------------------------------------
-- A result mentioned in "Enhancements of the bisimulation proof
-- method"

mutual

  -- For a more general result, see 6-2-14 below.

  !·⊕·∼!·∣!· :  {i a b}  [ i ] ! (a ·  b ·)  ! a ·  ! b ·
  !·⊕·∼!·∣!· {i} =  lr , rl 
    where
    lemma = λ {a b}  ∼′:
      ! (a ·  b ·)    ∼⟨ ∣-right-identity 
      ! (a ·  b ·)      ∼⟨ !·⊕·∼′!·∣!· {i = i} ⟩■
      ! a ·  ! b ·

    left-lemma = λ {a b}  ∼′:
      ! (a ·  b ·)      ∼⟨ lemma 
      ! a ·  ! b ·        ∼⟨ symmetric ∣-right-identity ∣-cong reflexive ⟩■
      (! a ·  )  ! b ·

    right-lemma = λ {a b}  ∼′:
      ! (a ·  b ·)      ∼⟨ lemma 
      ! a ·   ! b ·       ∼⟨ reflexive ∣-cong symmetric ∣-right-identity ⟩■
      ! a ·  (! b ·  )

    τ-lemma = λ {a b}  ∼′:
      (! (a ·  b ·)  )      ∼⟨ ∣-right-identity 
      ! (a ·  b ·)            ∼⟨ lemma 
      ! a ·  ! b ·              ∼⟨ symmetric (∣-right-identity ∣-cong ∣-right-identity) ⟩■
      (! a ·  )  (! b ·  )

    lr :  {a b P μ} 
         ! (a ·  b ·) [ μ ]⟶ P 
          λ Q  ! a ·  ! b · [ μ ]⟶ Q × [ i ] P ∼′ Q
    lr {a} {b} {P} tr = case 6-1-3-2 tr of λ where

      (inj₁ (. , choice-left action , P∼![a⊕b]∣∅)) 
        P                    ∼⟨ P∼![a⊕b]∣∅ 
        ! (a ·  b ·)      ∼⟨ left-lemma ⟩■
        (! a ·  )  ! b ·  [ name a ]⟵⟨ par-left (replication (par-right action)) 
        ! a ·        ! b ·

      (inj₁ (. , choice-right action , P∼![a⊕b]∣∅)) 
        P                    ∼⟨ P∼![a⊕b]∣∅ 
        ! (a ·  b ·)      ∼⟨ right-lemma ⟩■
        ! a ·  (! b ·  )  [ name b ]⟵⟨ par-right (replication (par-right action)) 
        ! a ·  ! b ·

      (inj₂ (refl , P′ , P″ , c , a⊕b⟶P′ , a⊕b⟶P″ , P∼![a⊕b]∣P′∣P″)) 
        let b≡co-a , P′≡∅ , P″≡∅ = Σ-map id [ id , id ]
                                     (·′⊕·′-co a⊕b⟶P′ a⊕b⟶P″) in

        P                          ∼⟨ P∼![a⊕b]∣P′∣P″ 
        (! (a ·  b ·)  P′)  P″  ∼⟨ (reflexive ∣-cong ≡⇒∼ P′≡∅) ∣-cong ≡⇒∼ P″≡∅ 
        (! (a ·  b ·)  )      ∼⟨ τ-lemma ⟩■
        (! a ·  )  (! b ·  )  [ τ ]⟵⟨ par-τ′ b≡co-a (replication (par-right action))
                                                         (replication (par-right action)) 
        ! a ·  ! b ·

    rl :  {a b Q μ} 
         ! a ·  ! b · [ μ ]⟶ Q 
          λ P  ! (a ·  b ·) [ μ ]⟶ P × [ i ] P ∼′ Q
    rl {a} {b} (par-left {P′ = P′} tr) =
      case 6-1-3-2 tr of λ where

        (inj₁ (. , action , P′∼!a∣∅)) 
          ! (a ·  b ·)        [ name a ]⟶⟨ replication (par-right (choice-left action)) ⟩ʳˡ
          ! (a ·  b ·)      ∼⟨ left-lemma 
          (! a ·  )  ! b ·  ∼⟨ symmetric P′∼!a∣∅ ∣-cong reflexive ⟩■
          P′  ! b ·

        (inj₂ (refl , . , P″ , .a , action , a⟶P″ , P′∼!a∣∅∣P″)) 
          ⊥-elim (names-are-not-inverted a⟶P″)

    rl {a} {b} (par-right {Q′ = Q′} tr) =
      case 6-1-3-2 tr of λ where

        (inj₁ (. , action , Q′∼!b∣∅)) 
          ! (a ·  b ·)        [ name b ]⟶⟨ replication (par-right (choice-right action)) ⟩ʳˡ
          ! (a ·  b ·)      ∼⟨ right-lemma 
          ! a ·  (! b ·  )  ∼⟨ reflexive ∣-cong symmetric Q′∼!b∣∅ ⟩■
          ! a ·  Q′

        (inj₂ (refl , . , Q″ , .b , action , b⟶Q″ , Q′∼!b∣∅∣Q″)) 
          ⊥-elim (names-are-not-inverted b⟶Q″)

    rl {a} (par-τ {P′ = P′} {Q′ = Q′} tr₁ tr₂) =
      case 6-1-3-2 tr₁ ,′ 6-1-3-2 tr₂ of λ where

        (inj₁ (. , action , P′∼!a∣∅) ,
         inj₁ (. , action , Q′∼!co-a∣∅)) 
          ! (a ·  co a ·)              [ τ ]⟶⟨ replication (par-τ (replication (par-right (choice-left action)))
                                                                   (choice-right action)) ⟩ʳˡ
          (! (a ·  co a ·)  )      ∼⟨ τ-lemma 
          (! a ·  )  (! co a ·  )  ∼⟨ symmetric (P′∼!a∣∅ ∣-cong Q′∼!co-a∣∅) ⟩■
          P′  Q′

        (inj₁ _ , inj₂ (() , _))
        (inj₂ (() , _) , _)

  !·⊕·∼′!·∣!· :  {a b i}  [ i ] ! (a ·  b ·) ∼′ ! a ·  ! b ·
  force !·⊕·∼′!·∣!· = !·⊕·∼!·∣!·

------------------------------------------------------------------------
-- Exercise 6.2.4

mutual

  -- For a more general result, see 6-2-17-4 below.

  6-2-4 :  {a i}  [ i ] ! ! a ·  ! a ·
  6-2-4 {a} {i} =  lr , rl 
    where
    impossible :  {μ P q} {Q : Set q} 
                 ! ! a · [ μ ]⟶ P  μ  τ  Q
    impossible {μ} !!a⟶P μ≡τ = ⊥-elim $ name≢τ
      (name a  ≡⟨ !-only (!-only ·′-only) !!a⟶P 
       μ       ≡⟨ μ≡τ ⟩∎
       τ       )

    lemma = λ {P} P∼!a∣∅  ∼′:
      ! ! a ·  P            ∼⟨ reflexive ∣-cong P∼!a∣∅ 
      ! ! a ·  (! a ·  )  ∼⟨ reflexive ∣-cong ∣-right-identity 
      ! ! a ·  ! a ·        ∼⟨ 6-1-2 
      ! ! a ·                ∼⟨ 6-2-4′ {i = i} 
      ! a ·                  ∼⟨ symmetric ∣-right-identity ⟩■
      ! a ·  

    lr :  {P μ} 
         ! ! a · [ μ ]⟶ P 
          λ P′  ! a · [ μ ]⟶ P′ × [ i ] P ∼′ P′
    lr {P = P} !!a⟶P = case 6-1-3-2 !!a⟶P of λ where
      (inj₂ (μ≡τ , _))                impossible !!a⟶P μ≡τ
      (inj₁ (P′ , !a⟶P′ , P∼!!a∣P′))  case 6-1-3-2 !a⟶P′ of λ where
        (inj₂ (μ≡τ , _))                impossible !!a⟶P μ≡τ
        (inj₁ (. , action , P′∼!a∣∅)) 
          P             ∼⟨ P∼!!a∣P′ 
          ! ! a ·  P′  ∼⟨ lemma P′∼!a∣∅ ⟩■
          ! a ·       [ name a ]⟵⟨ replication (par-right action) 
          ! a ·

    rl :  {P μ} 
         ! a · [ μ ]⟶ P 
          λ P′  ! ! a · [ μ ]⟶ P′ × [ i ] P′ ∼′ P
    rl {P = P} !a⟶P = case 6-1-3-2 !a⟶P of λ where
      (inj₂ (refl , . , Q″ , .a , action , a⟶Q″ , _)) 
        ⊥-elim (names-are-not-inverted a⟶Q″)
      (inj₁ (. , action , P∼!a∣∅)) 
        ! ! a ·      [ name a ]⟶⟨ replication (par-right !a⟶P) ⟩ʳˡ
        ! ! a ·  P  ∼⟨ lemma P∼!a∣∅ 
        ! a ·      ∼⟨ symmetric P∼!a∣∅ ⟩■
        P

  6-2-4′ :  {a i}  [ i ] ! ! a · ∼′ ! a ·
  force 6-2-4′ = 6-2-4

------------------------------------------------------------------------
-- A result mentioned in "Enhancements of the bisimulation proof
-- method"

·∣·∼·· :  {a}  a ·  a ·  name a · (a ·)
·∣·∼·· {a} =  lr , rl 
  where
  lr :  {P μ}  a ·  a · [ μ ]⟶ P 
        λ P′  name a · (a ·) [ μ ]⟶ P′ × P ∼′ P′
  lr (par-left action) =
      a ·         ∼⟨ ∣-left-identity ⟩■
    a ·             [ name a ]⟵⟨ action 
    name a · (a ·)

  lr (par-right action) =
    a ·           ∼⟨ ∣-right-identity ⟩■
    a ·             [ name a ]⟵⟨ action 
    name a · (a ·)

  lr (par-τ′ a≡co-a action action) = ⊥-elim (id≢co a≡co-a)

  rl :  {P μ}  name a · (a ·) [ μ ]⟶ P 
        λ P′  a ·  a · [ μ ]⟶ P′ × P′ ∼′ P
  rl action =
    a ·  a ·  [ name a ]⟶⟨ par-right action ⟩ʳˡ
    a ·      ∼⟨ ∣-right-identity ⟩■
    a ·

------------------------------------------------------------------------
-- More preservation lemmas

-- _⊕_ preserves bisimilarity.

infix 8 _⊕-cong_ _⊕-cong′_

_⊕-cong_ :  {i P P′ Q Q′} 
           [ i ] P  P′  [ i ] Q  Q′  [ i ] P  Q  P′  Q′
P∼P′ ⊕-cong Q∼Q′ =
   CL.⊕-cong P∼P′ Q∼Q′
  , Σ-map id (Σ-map id symmetric) 
    CL.⊕-cong (symmetric P∼P′) (symmetric Q∼Q′)
  

_⊕-cong′_ :  {i P P′ Q Q′} 
            [ i ] P ∼′ P′  [ i ] Q ∼′ Q′  [ i ] P  Q ∼′ P′  Q′
force (P∼P′ ⊕-cong′ Q∼Q′) = force P∼P′ ⊕-cong force Q∼Q′

-- _·′_ preserves bisimilarity.

infix 12 _·′-cong_ _·′-cong′_

_·′-cong_ :
   {i μ μ′ P P′} 
  μ  μ′  [ i ] force P ∼′ force P′  [ i ] μ ·′ P  μ′ ·′ P′
refl ·′-cong P∼P′ =
   CL.·′-cong P∼P′
  , Σ-map id (Σ-map id symmetric)  CL.·′-cong (symmetric P∼P′)
  

_·′-cong′_ :
   {i μ μ′ P P′} 
  μ  μ′  [ i ] force P ∼′ force P′  [ i ] μ ·′ P ∼′ μ′ ·′ P′
force (μ≡μ′ ·′-cong′ P∼P′) = μ≡μ′ ·′-cong P∼P′

-- _·_ preserves bisimilarity.

infix 12 _·-cong_ _·-cong′_

_·-cong_ :
   {i μ μ′ P P′} 
  μ  μ′  [ i ] P  P′  [ i ] μ · P  μ′ · P′
refl ·-cong P∼P′ = refl ·′-cong convert P∼P′

_·-cong′_ :
   {i μ μ′ P P′} 
  μ  μ′  [ i ] P ∼′ P′  [ i ] μ · P ∼′ μ′ · P′
force (μ≡μ′ ·-cong′ P∼P′) = μ≡μ′ ·-cong force P∼P′

-- _· turns equality into bisimilarity.

infix 12 _·-cong _·-cong′

_·-cong :  {μ μ′}  μ  μ′  μ ·  μ′ ·
refl ·-cong = reflexive

_·-cong′ :  {μ μ′}  μ  μ′  μ · ∼′ μ′ ·
refl ·-cong′ = reflexive

mutual

  -- !_ preserves bisimilarity.

  infix 10 !-cong_ !-cong′_

  !-cong_ :  {i P P′} 
            [ i ] P  P′  [ i ] ! P  ! P′
  !-cong P∼P′ =
     lr P∼P′
    , Σ-map id (Σ-map id symmetric)  lr (symmetric P∼P′)
    
    where
    lr = CL.!-cong 6-1-3-2 _∣-cong′_ !-cong′_

  !-cong′_ :  {i P P′}  [ i ] P ∼′ P′  [ i ] ! P ∼′ ! P′
  force (!-cong′ P∼P′) = !-cong force P∼P′

mutual

  -- ν preserves bisimilarity.

  ν-cong :  {i a a′ P P′} 
           a  a′  [ i ] P  P′  [ i ] ν a P  ν a′ P′
  ν-cong refl = λ P∼P′ 
     lr P∼P′
    , Σ-map id (Σ-map id symmetric)  lr (symmetric P∼P′)
    
    where
    lr = CL.ν-cong (ν-cong′ refl)

  ν-cong′ :  {i a a′ P P′} 
            a  a′  [ i ] P ∼′ P′  [ i ] ν a P ∼′ ν a′ P′
  force (ν-cong′ a≡a′ P∼P′) = ν-cong a≡a′ (force P∼P′)

-- _[_] preserves bisimilarity. (This result is related to Exercise
-- 6.2.10.)

mutual

  infix 5 _[_]-cong _[_]-cong′

  _[_]-cong :
     {i n Ps Qs}
    (C : Context  n)  (∀ x  [ i ] Ps x  Qs x) 
    [ i ] C [ Ps ]  C [ Qs ]
  hole x  [ Ps∼Qs ]-cong = Ps∼Qs x
         [ Ps∼Qs ]-cong = reflexive
  C₁  C₂ [ Ps∼Qs ]-cong = (C₁ [ Ps∼Qs ]-cong) ∣-cong (C₂ [ Ps∼Qs ]-cong)
  C₁  C₂ [ Ps∼Qs ]-cong = (C₁ [ Ps∼Qs ]-cong) ⊕-cong (C₂ [ Ps∼Qs ]-cong)
  μ ·′ C  [ Ps∼Qs ]-cong = refl ·′-cong λ { .force  force C [ Ps∼Qs ]-cong }
  ν a C   [ Ps∼Qs ]-cong = ν-cong refl (C [ Ps∼Qs ]-cong)
  ! C     [ Ps∼Qs ]-cong = !-cong (C [ Ps∼Qs ]-cong)

  _[_]-cong′ :
     {i n Ps Qs}
    (C : Context  n)  (∀ x  [ i ] Ps x ∼′ Qs x) 
    [ i ] C [ Ps ] ∼′ C [ Qs ]
  force (C [ Ps∼Qs ]-cong′) = C [  x  force (Ps∼Qs x)) ]-cong

-- The proof of _[_]-cong uses 6-1-3-2 (in !-cong_). The following
-- direct proof does not use 6-1-3-2 (but it does use
-- extensionality).

module _ (ext : Proc-extensionality) where

 mutual

  infix 5 _[_]-cong₂ _[_]-cong₂′ _[_]-cong₂″

  _[_]-cong₂ :
     {i n Ps Qs}
    (C : Context  n)  (∀ x  [ i ] Ps x  Qs x) 
    [ i ] C [ Ps ]  C [ Qs ]
  _[_]-cong₂ {i} C Ps∼Qs =
     lr C Ps∼Qs
    , Σ-map id (Σ-map id symmetric)  lr C (symmetric  Ps∼Qs)
    
    where

    infix 5 _[_][_]-cong₁ _[_][_]-cong₂

    _[_][_]-cong₁ :
       {n P Q Ps Qs} 
      (C : Context  (suc n)) 
      [ i ] P ∼′ Q 
      (∀ x  [ i ] Ps x  Qs x) 
      [ i ] C [ [ const P , Ps ] ] ∼′ C [ [ const Q , Qs ] ]
    force (C [ P∼′Q ][ Ps∼Qs ]-cong₁) =
      C [ [ const (force P∼′Q) , Ps∼Qs ] ]-cong₂

    _[_][_]-cong₂ :
       {P Q R S} 
      (C : Context  2) 
      [ i ] P ∼′ Q 
      [ i ] R ∼′ S 
      [ i ] C [ [ const P , [ const R ,  ()) ] ] ] ∼′
            C [ [ const Q , [ const S ,  ()) ] ] ]
    force (C [ P∼′Q ][ R∼′S ]-cong₂) =
      C [ [ const (force P∼′Q)
          , [ const (force R∼′S) ,  ()) ]
          ] ]-cong₂

    lr :  {n Ps Qs P′ μ} (C : Context  n) 
         (∀ x  [ i ] Ps x  Qs x) 
         C [ Ps ] [ μ ]⟶ P′ 
          λ Q′  C [ Qs ] [ μ ]⟶ Q′ × [ i ] P′ ∼′ Q′
    lr (hole x)  Ps∼Qs tr                  = left-to-right (Ps∼Qs x) tr
    lr          Ps∼Qs ()
    lr (C₁  C₂) Ps∼Qs (par-left tr)       = Σ-map (_∣ _) (Σ-map par-left  b  subst  P  [ i ] _ ∼′ _  P) (ext $ weaken-[] C₂) $
                                                                                 subst  P  [ i ] _  P ∼′ _) (ext $ weaken-[] C₂) $
                                                                                 hole fzero  weaken C₂ [ b ][ Ps∼Qs ]-cong₁)) (lr C₁ Ps∼Qs tr)
    lr (C₁  C₂) Ps∼Qs (par-right tr)      = Σ-map (_ ∣_) (Σ-map par-right  b  subst  P  [ i ] _ ∼′ P  _) (ext $ weaken-[] C₁) $
                                                                                  subst  P  [ i ] P  _ ∼′ _) (ext $ weaken-[] C₁) $
                                                                                  weaken C₁  hole fzero [ b ][ Ps∼Qs ]-cong₁)) (lr C₂ Ps∼Qs tr)
    lr (C₁  C₂) Ps∼Qs (par-τ tr₁ tr₂)     = Σ-zip _∣_ (Σ-zip par-τ  b₁ b₂  hole fzero  hole (fsuc fzero) [ b₁ ][ b₂ ]-cong₂))
                                               (lr C₁ Ps∼Qs tr₁) (lr C₂ Ps∼Qs tr₂)
    lr (C₁  C₂) Ps∼Qs (choice-left tr)    = Σ-map id (Σ-map choice-left id) (lr C₁ Ps∼Qs tr)
    lr (C₁  C₂) Ps∼Qs (choice-right tr)   = Σ-map id (Σ-map choice-right id) (lr C₂ Ps∼Qs tr)
    lr (μ ·′ C)  Ps∼Qs action              = _ , action , force C [ Ps∼Qs ]-cong₂′
    lr (ν a C)   Ps∼Qs (restriction a∉ tr) = Σ-map (ν a) (Σ-map (restriction a∉)  b  ν a (hole fzero) [ b ][ Ps∼Qs ]-cong₁)) (lr C Ps∼Qs tr)
    lr (! C)     Ps∼Qs (replication tr)    = Σ-map id (Σ-map replication id) (lr (! C  C) Ps∼Qs tr)

  _[_]-cong₂′ :
     {i n Ps Qs}
    (C : Context  n)  (∀ x  [ i ] Ps x  Qs x) 
    [ i ] C [ Ps ] ∼′ C [ Qs ]
  force (C [ Ps∼Qs ]-cong₂′) = C [ Ps∼Qs ]-cong₂

  _[_]-cong₂″ :
     {i n Ps Qs}
    (C : Context  n)  (∀ x  [ i ] Ps x ∼′ Qs x) 
    [ i ] C [ Ps ] ∼′ C [ Qs ]
  force (C [ Ps∼′Qs ]-cong₂″) = C [  x  force (Ps∼′Qs x)) ]-cong₂

-- Very strong bisimilarity is contained in bisimilarity.

mutual

  ≡→∼ :  {i P Q}  Equal i P Q  [ i ] P  Q
  ≡→∼             = reflexive
  ≡→∼ (eq₁  eq₂)  = ≡→∼ eq₁ ∣-cong ≡→∼ eq₂
  ≡→∼ (eq₁  eq₂)  = ≡→∼ eq₁ ⊕-cong ≡→∼ eq₂
  ≡→∼ (refl ·′ eq) = refl ·′-cong ≡→∼′ eq
  ≡→∼ (ν refl eq)  = ν-cong refl (≡→∼ eq)
  ≡→∼ (! eq)       = !-cong ≡→∼ eq

  ≡→∼′ :  {i P Q}  Equal′ i P Q  [ i ] P ∼′ Q
  force (≡→∼′ eq) = ≡→∼ (force eq)

------------------------------------------------------------------------
-- Lemma 6.2.14

mutual

  -- A more general variant of !·⊕·∼!·∣!·. For an even more general
  -- variant, see 6-2-17-2 below.

  6-2-14 :
     {i a b P Q} 
    [ i ] ! (name a · P  name b · Q)  ! name a · P  ! name b · Q
  6-2-14 {i} =  lr , rl 
    where
    left-lemma = λ {a b P Q}  ∼′:
      ! (name a · P  name b · Q)  P    ∼⟨ 6-2-14′ {i = i} ∣-cong′ reflexive 
      (! name a · P  ! name b · Q)  P  ∼⟨ swap-rightmost ⟩■
      (! name a · P  P)  ! name b · Q

    right-lemma = λ {a b P Q}  ∼′:
      ! (name a · P  name b · Q)  Q    ∼⟨ 6-2-14′ {i = i} ∣-cong′ reflexive 
      (! name a · P  ! name b · Q)  Q  ∼⟨ symmetric ∣-assoc ⟩■
      ! name a · P  (! name b · Q  Q)

    τ-lemma = λ {a b P Q}  ∼′:
      (! (name a · P  name b · Q)  P)  Q    ∼⟨ left-lemma ∣-cong′ reflexive 
      ((! name a · P  P)  ! name b · Q)  Q  ∼⟨ symmetric ∣-assoc ⟩■
      (! name a · P  P)  (! name b · Q  Q)

    lr :  {a b P Q R μ} 
         ! (name a · P  name b · Q) [ μ ]⟶ R 
          λ S  ! name a · P  ! name b · Q [ μ ]⟶ S × [ i ] R ∼′ S
    lr {a} {b} {P} {Q} {R} tr = case 6-1-3-2 tr of λ where

      (inj₁ (.P , choice-left action , R∼![aP⊕bQ]∣P)) 
        R                                  ∼⟨ R∼![aP⊕bQ]∣P 
        ! (name a · P  name b · Q)  P    ∼⟨ left-lemma ⟩■
        (! name a · P  P)  ! name b · Q  [ name a ]⟵⟨ par-left (replication (par-right action)) 
        ! name a · P        ! name b · Q

      (inj₁ (.Q , choice-right action , R∼![aP⊕bQ]∣Q)) 
        R                                  ∼⟨ R∼![aP⊕bQ]∣Q 
        ! (name a · P  name b · Q)  Q    ∼⟨ right-lemma ⟩■
        ! name a · P  (! name b · Q  Q)  [ name b ]⟵⟨ par-right (replication (par-right action)) 
        ! name a · P  ! name b · Q

      (inj₂ ( refl , R′ , R″ , c , aP⊕bQ⟶R′ , aP⊕bQ⟶R″
            , R∼![aP⊕bQ]∣R′∣R″
            )) 
        let b≡co-a , R′≡,R″≡ = ·′⊕·′-co aP⊕bQ⟶R′ aP⊕bQ⟶R″

            lemma : _  [ _ ] _  _
            lemma = λ where
              (inj₁ (R′≡P , R″≡Q)) 
                (! (name a · P  name b · Q)  R′)  R″  ∼⟨ (reflexive ∣-cong ≡⇒∼ R′≡P) ∣-cong ≡⇒∼ R″≡Q ⟩■
                (! (name a · P  name b · Q)  P)  Q
              (inj₂ (R′≡Q , R″≡P)) 
                (! (name a · P  name b · Q)  R′)  R″  ∼⟨ (reflexive ∣-cong ≡⇒∼ R′≡Q) ∣-cong ≡⇒∼ R″≡P 
                (! (name a · P  name b · Q)  Q)  P    ∼⟨ swap-rightmost ⟩■
                (! (name a · P  name b · Q)  P)  Q
        in
        R                                        ∼⟨ R∼![aP⊕bQ]∣R′∣R″ 
        (! (name a · P  name b · Q)  R′)  R″  ∼⟨ lemma R′≡,R″≡ 
        (! (name a · P  name b · Q)  P)  Q    ∼⟨ τ-lemma ⟩■
        (! name a · P  P)  (! name b · Q  Q)  [ τ ]⟵⟨ par-τ′ b≡co-a (replication (par-right action))
                                                                       (replication (par-right action)) 
        ! name a · P  ! name b · Q

    rl :  {a b P Q S μ} 
         ! name a · P  ! name b · Q [ μ ]⟶ S 
          λ R  ! (name a · P  name b · Q) [ μ ]⟶ R × [ i ] R ∼′ S
    rl {a} {b} {P} {Q} (par-left {P′ = S} tr) =
      case 6-1-3-2 tr of λ where
        (inj₁ (.P , action , S∼!aP∣P)) 
          ! (name a · P  name b · Q)        [ name a ]⟶⟨ replication (par-right (choice-left action)) ⟩ʳˡ
          ! (name a · P  name b · Q)  P    ∼⟨ left-lemma 
          (! name a · P  P)  ! name b · Q  ∼⟨ symmetric S∼!aP∣P ∣-cong reflexive ⟩■
          S  ! name b · Q

        (inj₂ (refl , .P , S′ , .a , action , aP⟶S′ , S∼!aP∣P∣S′)) 
          ⊥-elim (names-are-not-inverted aP⟶S′)

    rl {a} {b} {P} {Q} (par-right {Q′ = S} tr) =
      case 6-1-3-2 tr of λ where
        (inj₁ (.Q , action , S∼!bQ∣Q)) 
          ! (name a · P  name b · Q)        [ name b ]⟶⟨ replication (par-right (choice-right action)) ⟩ʳˡ
          ! (name a · P  name b · Q)  Q    ∼⟨ right-lemma 
          ! name a · P  (! name b · Q  Q)  ∼⟨ reflexive ∣-cong symmetric S∼!bQ∣Q ⟩■
          ! name a · P  S

        (inj₂ (refl , .Q , S′ , .b , action , bQ⟶S′ , S∼!bQ∣Q∣S′)) 
          ⊥-elim (names-are-not-inverted bQ⟶S′)

    rl {a} {P = P} {Q} (par-τ {P′ = S} {Q′ = S′} tr₁ tr₂) =
      case 6-1-3-2 tr₁ ,′ 6-1-3-2 tr₂ of λ where
        (inj₁ (.P , action , S∼!aP∣P) ,
         inj₁ (.Q , action , S′∼!co-aQ∣Q)) 
          ! (name a · P  name (co a) · Q)              [ τ ]⟶⟨ replication (par-τ (replication (par-right (choice-left action)))
                                                                                   (choice-right action)) ⟩ʳˡ
          (! (name a · P  name (co a) · Q)  P)  Q    ∼⟨ τ-lemma 
          (! name a · P  P)  (! name (co a) · Q  Q)  ∼⟨ symmetric (S∼!aP∣P ∣-cong S′∼!co-aQ∣Q) ⟩■
          S  S′

        (inj₁ _ , inj₂ (() , _))
        (inj₂ (() , _) , _)

  6-2-14′ :
     {i a b P Q} 
    [ i ] ! (name a · P  name b · Q) ∼′ ! name a · P  ! name b · Q
  force 6-2-14′ = 6-2-14

------------------------------------------------------------------------
-- Theorem 6.2.16

mutual

  6-2-16 :
     {i n} {Ps Qs : Fin n  Proc } {C : Fin n  Context  n} 
    (∀ x  Weakly-guarded (C x)) 
    (∀ x  [ i ] Ps x  C x [ Ps ]) 
    (∀ x  [ i ] Qs x  C x [ Qs ]) 
     x  [ i ] Ps x  Qs x
  6-2-16 {i} {Ps = Ps} {Qs} {C} w ∼C[Ps] ∼C[Qs] x =
    Ps x        ∼⟨ ∼C[Ps] x 
    C x [ Ps ]  ∼⟨ ∼:  lr ∼C[Ps] ∼C[Qs] , Σ-map id (Σ-map id symmetric)  lr ∼C[Qs] ∼C[Ps]  
    C x [ Qs ]  ∼⟨ symmetric (∼C[Qs] x) ⟩■
    Qs x
    where
    lr :
       {Ps Qs μ P} 
      (∀ x  [ i ] Ps x  C x [ Ps ]) 
      (∀ x  [ i ] Qs x  C x [ Qs ]) 
      C x [ Ps ] [ μ ]⟶ P 
       λ Q  C x [ Qs ] [ μ ]⟶ Q × [ i ] P ∼′ Q
    lr {Ps} {Qs} {μ} ∼C[Ps] ∼C[Qs] ⟶P =
      case 6-2-15 (C x) (w x) ⟶P of λ where
        (C′ , refl , trs) 
          C′ [ Ps ]   ∼⟨ C′ [ 6-2-16′ w ∼C[Ps] ∼C[Qs] ]-cong′ ⟩■
          C′ [ Qs ]   [ μ ]⟵⟨ trs Qs 
          C x [ Qs ]

  6-2-16′ :
     {i n} {Ps Qs : Fin n  Proc } {C : Fin n  Context  n} 
    (∀ x  Weakly-guarded (C x)) 
    (∀ x  [ i ] Ps x  C x [ Ps ]) 
    (∀ x  [ i ] Qs x  C x [ Qs ]) 
     x  [ i ] Ps x ∼′ Qs x
  force (6-2-16′ w ∼C[Ps] ∼C[Qs] x) = 6-2-16 w ∼C[Ps] ∼C[Qs] x

------------------------------------------------------------------------
-- Some lemmas related to _⊕_

-- _⊕_ is idempotent.

⊕-idempotent :  {P}  P  P  P
⊕-idempotent {P} =
   lr
  ,  {R} P⟶R 
       P  P  ⟶⟨ choice-left P⟶R ⟩ʳˡ
       R      ∼⟨ ∼′: reflexive ⟩■
       R)
  
  where
  lr :  {Q μ}  P  P [ μ ]⟶ Q   λ R  P [ μ ]⟶ R × Q ∼′ R
  lr {Q} (choice-left P⟶Q) =
    Q  ∼⟨ ∼′: reflexive ⟩■
    Q  ⟵⟨ P⟶Q 
    P

  lr {Q} (choice-right P⟶Q) =
    Q  ∼⟨ ∼′: reflexive ⟩■
    Q  ⟵⟨ P⟶Q 
    P

⊕-idempotent′ :  {P}  P  P ∼′ P
force ⊕-idempotent′ = ⊕-idempotent

-- _⊕_ is commutative.

⊕-comm :  {P Q}  P  Q  Q  P
⊕-comm =  lr , Σ-map id (Σ-map id symmetric)  lr 
  where
  lr :  {P Q R μ} 
       P  Q [ μ ]⟶ R   λ R′  Q  P [ μ ]⟶ R′ × R ∼′ R′
  lr {P} {Q} {R} = λ where
    (choice-left  P⟶R) 
      R       ⟵⟨ choice-right P⟶R 
      Q  P

    (choice-right Q⟶R) 
      R       ⟵⟨ choice-left Q⟶R 
      Q  P

------------------------------------------------------------------------
-- Lemma 6.2.17

-- Some results mentioned in the proof of 6.2.17 (1) in
-- "Enhancements of the bisimulation proof method".

6-2-17-1-lemma₁ :  {P Q}  (! P  ! Q)  (P  Q)  ! P  ! Q
6-2-17-1-lemma₁ {P} {Q} =
  (! P  ! Q)  (P  Q)  ∼⟨ swap-in-the-middle 
  (! P  P)  (! Q  Q)  ∼⟨ 6-1-2 ∣-cong 6-1-2 ⟩■
  ! P  ! Q

abstract

  6-2-17-1-lemma₂ :
     {P Q R μ} 
    ! (P  Q) [ μ ]⟶ R 
     λ S 
      R  ! (P  Q)  S ×
       λ T 
        ! P  ! Q [ μ ]⟶ T ×
        (! P  ! Q)  S ∼′ T
  6-2-17-1-lemma₂ {P} {Q} {R} tr = case 6-1-3-2 tr of λ where
    (inj₁ (R′ , P∣Q⟶R′ , R∼![P∣Q]∣R′)) 
      let R″ , !P∣!Q⟶R″ , !P∣!Q∣R′∼R″ =
            left-to-right
              ((! P  ! Q)  (P  Q)  ∼⟨ 6-2-17-1-lemma₁ ⟩■
               ! P  ! Q)
              ((! P  ! Q)  (P  Q)  ⟶⟨ par-right P∣Q⟶R′ 
               (! P  ! Q)  R′)
      in _ , R∼![P∣Q]∣R′ , _ , !P∣!Q⟶R″ , !P∣!Q∣R′∼R″

    (inj₂ (refl , R′ , R″ , a , P∣Q⟶R′ , P∣Q⟶R″ , R∼![P∣Q]∣R′∣R″)) 
      let T , !P∣!Q⟶T , !P∣!Q∣[R′∣R″]∼T =
            left-to-right
              ((! P  ! Q)  ((P  Q)  (P  Q))  ∼⟨ ∣-assoc 
               ((! P  ! Q)  (P  Q))  (P  Q)  ∼⟨ 6-2-17-1-lemma₁ ∣-cong reflexive 
               (! P  ! Q)  (P  Q)              ∼⟨ 6-2-17-1-lemma₁ ⟩■
               ! P  ! Q)
              ((! P  ! Q)  ((P  Q)  (P  Q))  ⟶⟨ par-right (par-τ P∣Q⟶R′ P∣Q⟶R″) 
               (! P  ! Q)  (R′  R″))
      in
        _
      , (R                      ∼⟨ R∼![P∣Q]∣R′∣R″ 
         (! (P  Q)  R′)  R″  ∼⟨ symmetric ∣-assoc ⟩■
         ! (P  Q)  (R′  R″))
      , _
      , !P∣!Q⟶T
      , !P∣!Q∣[R′∣R″]∼T

mutual

  6-2-17-1 :  {i P Q}  [ i ] ! (P  Q)  ! P  ! Q
  6-2-17-1 {i} =  lr , rl 
    where
    lr :  {P Q R μ} 
         ! (P  Q) [ μ ]⟶ R 
          λ S  ! P  ! Q [ μ ]⟶ S × [ i ] R ∼′ S
    lr {P} {Q} {R} tr =
      let S , R∼![P∣Q]∣S , T , !P∣!Q⟶T , !P∣!Q∣S∼T =
            6-2-17-1-lemma₂ tr in

      R                ∼⟨ R∼![P∣Q]∣S 
      ! (P  Q)  S    ∼⟨ 6-2-17-1′ ∣-cong′ reflexive 
      (! P  ! Q)  S  ∼⟨ !P∣!Q∣S∼T ⟩■
      T                ⟵⟨ !P∣!Q⟶T 
      ! P  ! Q

    lemma = λ {P Q R S}  ∼′:
      ! (P  Q)  (R  S)    ∼⟨ 6-2-17-1′ {i = i} ∣-cong′ reflexive 
      (! P  ! Q)  (R  S)  ∼⟨ swap-in-the-middle ⟩■
      (! P  R)  (! Q  S)

    left-lemma = λ {P Q R}  ∼′:
      ! (P  Q)  (R  Q)    ∼⟨ lemma 
      (! P  R)  (! Q  Q)  ∼⟨ reflexive ∣-cong 6-1-2 ⟩■
      (! P  R)  ! Q

    right-lemma = λ {P Q R}  ∼′:
      ! (P  Q)  (P  R)    ∼⟨ lemma 
      (! P  P)  (! Q  R)  ∼⟨ 6-1-2 ∣-cong reflexive ⟩■
      ! P  (! Q  R)

    rl :  {P Q S μ} 
         ! P  ! Q [ μ ]⟶ S 
          λ R  ! (P  Q) [ μ ]⟶ R × [ i ] R ∼′ S
    rl {P} {Q} (par-left {P′ = S} !P⟶S) =
      case 6-1-3-2 !P⟶S
        return (const $  λ _  _ × [ i ] _ ∼′ _)
        of λ where
        (inj₁ (P′ , P⟶P′ , S∼!P∣P′)) 
          ! (P  Q)             ⟶⟨ replication (par-right (par-left P⟶P′)) ⟩ʳˡ
          ! (P  Q)  (P′  Q)  ∼⟨ left-lemma 
          (! P  P′)  ! Q      ∼⟨ symmetric S∼!P∣P′ ∣-cong reflexive ⟩■
          S  ! Q

        (inj₂ (refl , P′ , P″ , a , P⟶P′ , P⟶P″ , S∼!P∣P′∣P″)) 
          ! (P  Q)                          [ τ ]⟶⟨ replication (par-τ (replication (par-right (par-left P⟶P′)))
                                                                        (par-left P⟶P″)) ⟩ʳˡ
          (! (P  Q)  (P′  Q))  (P″  Q)  ∼⟨ left-lemma ∣-cong′ reflexive 
          ((! P  P′)  ! Q)  (P″  Q)      ∼⟨ swap-in-the-middle 
          ((! P  P′)  P″)  (! Q  Q)      ∼⟨ reflexive ∣-cong 6-1-2 
          ((! P  P′)  P″)  ! Q            ∼⟨ symmetric S∼!P∣P′∣P″ ∣-cong reflexive ⟩■
          S  ! Q

    rl {P} {Q} (par-right {Q′ = S} !Q⟶S) =
      case 6-1-3-2 !Q⟶S
        return (const $  λ _  _ × [ i ] _ ∼′ _)
        of λ where
        (inj₁ (Q′ , Q⟶Q′ , S∼!Q∣Q′)) 
          ! (P  Q)             ⟶⟨ replication (par-right (par-right Q⟶Q′)) ⟩ʳˡ
          ! (P  Q)  (P  Q′)  ∼⟨ right-lemma 
          ! P  (! Q  Q′)      ∼⟨ reflexive ∣-cong symmetric S∼!Q∣Q′ ⟩■
          ! P  S

        (inj₂ (refl , Q′ , Q″ , a , Q⟶Q′ , Q⟶Q″ , S∼!Q∣Q′∣Q″)) 
          ! (P  Q)                          [ τ ]⟶⟨ replication (par-τ (replication (par-right (par-right Q⟶Q′)))
                                                                        (par-right Q⟶Q″)) ⟩ʳˡ
          (! (P  Q)  (P  Q′))  (P  Q″)  ∼⟨ right-lemma ∣-cong′ reflexive 
          (! P  (! Q  Q′))  (P  Q″)      ∼⟨ swap-in-the-middle 
          (! P  P)  ((! Q  Q′)  Q″)      ∼⟨ 6-1-2 ∣-cong reflexive 
          ! P  ((! Q  Q′)  Q″)            ∼⟨ reflexive ∣-cong symmetric S∼!Q∣Q′∣Q″ ⟩■
          ! P  S

    rl {P} {Q} (par-τ {P′ = S} {Q′ = S′} !P⟶S !Q⟶S′) =
      case 6-1-3-2 !P⟶S ,′ 6-1-3-2 !Q⟶S′ of λ where
        (inj₁ (P′ , P⟶P′ , S∼!P∣P′) ,
         inj₁ (Q′ , Q⟶Q′ , S′∼!Q∣Q′)) 
          ! (P  Q)                          [ τ ]⟶⟨ replication (par-τ (replication (par-right (par-left P⟶P′)))
                                                                                     (par-right Q⟶Q′)) ⟩ʳˡ
          (! (P  Q)  (P′  Q))  (P  Q′)  ∼⟨ left-lemma ∣-cong′ reflexive 
          ((! P  P′)  ! Q)  (P  Q′)      ∼⟨ swap-in-the-middle 
          ((! P  P′)  P)  (! Q  Q′)      ∼⟨ swap-rightmost ∣-cong reflexive 
          ((! P  P)  P′)  (! Q  Q′)      ∼⟨ (6-1-2 ∣-cong reflexive) ∣-cong reflexive 
          (! P  P′)  (! Q  Q′)            ∼⟨ symmetric (S∼!P∣P′ ∣-cong S′∼!Q∣Q′) ⟩■
          S  S′

        (inj₁ _ , inj₂ (() , _))
        (inj₂ (() , _) , _)

  6-2-17-1′ :  {i P Q}  [ i ] ! (P  Q) ∼′ ! P  ! Q
  force 6-2-17-1′ = 6-2-17-1

mutual

  6-2-17-2 :  {i P Q}  [ i ] ! (P  Q)  ! P  ! Q
  6-2-17-2 {i} =  lr , rl 
    where
    left-lemma = λ {P Q R}  ∼′:
      ! (P  Q)  R    ∼⟨ 6-2-17-2′ {i = i} ∣-cong′ reflexive 
      (! P  ! Q)  R  ∼⟨ swap-rightmost ⟩■
      (! P  R)  ! Q

    right-lemma = λ {P Q R}  ∼′:
      ! (P  Q)  R    ∼⟨ 6-2-17-2′ {i = i} ∣-cong′ reflexive 
      (! P  ! Q)  R  ∼⟨ symmetric ∣-assoc ⟩■
      ! P  (! Q  R)

    τ-lemma₁ = λ {P P′ P″ Q}  ∼′:
      (! (P  Q)  P′)  P″    ∼⟨ left-lemma ∣-cong′ reflexive 
      ((! P  P′)  ! Q)  P″  ∼⟨ swap-rightmost ⟩■
      ((! P  P′)  P″)  ! Q

    τ-lemma₂ = λ {P P′ Q Q′}  ∼′:
      (! (P  Q)  P′)  Q′    ∼⟨ left-lemma ∣-cong′ reflexive 
      ((! P  P′)  ! Q)  Q′  ∼⟨ symmetric ∣-assoc ⟩■
      (! P  P′)  (! Q  Q′)

    τ-lemma₃ = λ {P Q Q′ Q″}  ∼′:
      (! (P  Q)  Q′)  Q″    ∼⟨ right-lemma ∣-cong′ reflexive 
      (! P  (! Q  Q′))  Q″  ∼⟨ symmetric ∣-assoc ⟩■
      ! P  ((! Q  Q′)  Q″)

    lr :  {P Q R μ} 
         ! (P  Q) [ μ ]⟶ R 
          λ S  ! P  ! Q [ μ ]⟶ S × [ i ] R ∼′ S
    lr {P} {Q} {R} tr =
      case 6-1-3-2 tr
        return (const $  λ _  _ × [ i ] _ ∼′ _)
        of λ where

        (inj₁ (P′ , choice-left P⟶P′ , R∼![P⊕Q]∣P′)) 
          R                 ∼⟨ R∼![P⊕Q]∣P′ 
          ! (P  Q)  P′    ∼⟨ left-lemma ⟩■
          (! P  P′)  ! Q  ⟵⟨ par-left (replication (par-right P⟶P′)) 
          ! P         ! Q

        (inj₁ (Q′ , choice-right Q⟶Q′ , R∼![P⊕Q]∣Q′)) 
          R                 ∼⟨ R∼![P⊕Q]∣Q′ 
          ! (P  Q)  Q′    ∼⟨ right-lemma ⟩■
          ! P  (! Q  Q′)  ⟵⟨ par-right (replication (par-right Q⟶Q′)) 
          ! P   ! Q

        (inj₂ ( refl , P′ , P″ , c
              , choice-left P⟶P′ , choice-left P⟶P″
              , R∼![P⊕Q]∣P′∣P″
              )) 
          R                        ∼⟨ R∼![P⊕Q]∣P′∣P″ 
          (! (P  Q)  P′)  P″    ∼⟨ τ-lemma₁ ⟩■
          ((! P  P′)  P″)  ! Q  [ τ ]⟵⟨ par-left (replication (par-τ (replication (par-right P⟶P′)) P⟶P″)) 
          ! P  ! Q

        (inj₂ ( refl , P′ , Q′ , c
              , choice-left P⟶P′ , choice-right Q⟶Q′
              , R∼![P⊕Q]∣P′∣Q′
              )) 
          R                        ∼⟨ R∼![P⊕Q]∣P′∣Q′ 
          (! (P  Q)  P′)  Q′    ∼⟨ τ-lemma₂ ⟩■
          (! P  P′)  (! Q  Q′)  [ τ ]⟵⟨ par-τ (replication (par-right P⟶P′))
                                                 (replication (par-right Q⟶Q′)) 
          ! P  ! Q

        (inj₂ ( refl , Q′ , P′ , c
              , choice-right Q⟶Q′ , choice-left P⟶P′
              , R∼![P⊕Q]∣Q′∣P′
              )) 
          R                        ∼⟨ R∼![P⊕Q]∣Q′∣P′ 
          (! (P  Q)  Q′)  P′    ∼⟨ right-lemma ∣-cong′ reflexive 
          (! P  (! Q  Q′))  P′  ∼⟨ swap-rightmost ⟩■
          (! P  P′)  (! Q  Q′)  [ τ ]⟵⟨ par-τ′ (sym $ co-involutive c)
                                                  (replication (par-right P⟶P′))
                                                  (replication (par-right Q⟶Q′)) 
          ! P  ! Q

        (inj₂ ( refl , Q′ , Q″ , c
              , choice-right Q⟶Q′ , choice-right Q⟶Q″
              , R∼![P⊕Q]∣Q′∣Q″
              )) 
          R                        ∼⟨ R∼![P⊕Q]∣Q′∣Q″ 
          (! (P  Q)  Q′)  Q″    ∼⟨ τ-lemma₃ ⟩■
          ! P  ((! Q  Q′)  Q″)  [ τ ]⟵⟨ par-right (replication (par-τ (replication (par-right Q⟶Q′)) Q⟶Q″)) 
          ! P  ! Q

    rl :  {P Q S μ} 
         ! P  ! Q [ μ ]⟶ S 
          λ R  ! (P  Q) [ μ ]⟶ R × [ i ] R ∼′ S
    rl {P} {Q} (par-left {P′ = S} !P⟶S) =
      case 6-1-3-2 !P⟶S
        return (const $  λ _  _ × [ i ] _ ∼′ _)
        of λ where
        (inj₁ (P′ , P⟶P′ , S∼!P∣P′)) 
          ! (P  Q)         ⟶⟨ replication (par-right (choice-left P⟶P′)) ⟩ʳˡ
          ! (P  Q)  P′    ∼⟨ left-lemma 
          (! P  P′)  ! Q  ∼⟨ symmetric S∼!P∣P′ ∣-cong reflexive ⟩■
          S  ! Q

        (inj₂ (refl , P′ , P″ , a , P⟶P′ , P⟶P″ , S∼!P∣P′∣P″)) 
          ! (P  Q)                [ τ ]⟶⟨ replication (par-τ (replication (par-right (choice-left P⟶P′)))
                                                              (choice-left P⟶P″)) ⟩ʳˡ
          (! (P  Q)  P′)  P″    ∼⟨ τ-lemma₁ 
          ((! P  P′)  P″)  ! Q  ∼⟨ symmetric S∼!P∣P′∣P″ ∣-cong reflexive ⟩■
          S  ! Q

    rl {P} {Q} (par-right {Q′ = S} !Q⟶S) =
      case 6-1-3-2 !Q⟶S
        return (const $  λ _  _ × [ i ] _ ∼′ _)
        of λ where
        (inj₁ (Q′ , Q⟶Q′ , S∼!Q∣Q′)) 
          ! (P  Q)         ⟶⟨ replication (par-right (choice-right Q⟶Q′)) ⟩ʳˡ
          ! (P  Q)  Q′    ∼⟨ right-lemma 
          ! P  (! Q  Q′)  ∼⟨ reflexive ∣-cong symmetric S∼!Q∣Q′ ⟩■
          ! P  S

        (inj₂ (refl , Q′ , Q″ , a , Q⟶Q′ , Q⟶Q″ , S∼!Q∣Q′∣Q″)) 
          ! (P  Q)                [ τ ]⟶⟨ replication (par-τ (replication (par-right (choice-right Q⟶Q′)))
                                                              (choice-right Q⟶Q″)) ⟩ʳˡ
          (! (P  Q)  Q′)  Q″    ∼⟨ τ-lemma₃ 
          ! P  ((! Q  Q′)  Q″)  ∼⟨ reflexive ∣-cong symmetric S∼!Q∣Q′∣Q″ ⟩■
          ! P  S

    rl {P} {Q} (par-τ {P′ = S} {Q′ = S′} !P⟶S !Q⟶S′) =
      case 6-1-3-2 !P⟶S ,′ 6-1-3-2 !Q⟶S′ of λ where
        (inj₁ (P′ , P⟶P′ , S∼!P∣P′) ,
         inj₁ (Q′ , Q⟶Q′ , S′∼!Q∣Q′)) 
          ! (P  Q)                [ τ ]⟶⟨ replication (par-τ (replication (par-right (choice-left P⟶P′)))
                                                                                      (choice-right Q⟶Q′)) ⟩ʳˡ
          (! (P  Q)  P′)  Q′    ∼⟨ τ-lemma₂ 
          (! P  P′)  (! Q  Q′)  ∼⟨ symmetric (S∼!P∣P′ ∣-cong S′∼!Q∣Q′) ⟩■
          S  S′

        (inj₁ _ , inj₂ (() , _))
        (inj₂ (() , _) , _)

  6-2-17-2′ :  {i P Q}  [ i ] ! (P  Q) ∼′ ! P  ! Q
  force 6-2-17-2′ = 6-2-17-2

6-2-17-3 :  {P}  ! P  ! P  ! P
6-2-17-3 {P} =
  ! P  ! P  ∼⟨ symmetric 6-2-17-2 
  ! (P  P)  ∼⟨ !-cong ⊕-idempotent ⟩■
  ! P

-- A result mentioned in the proof of 6.2.17 (4) in "Enhancements of
-- the bisimulation proof method".

6-2-17-4-lemma :  {P Q μ}  ! P [ μ ]⟶ Q  Q  ! P  Q
6-2-17-4-lemma {P} {Q} !P⟶Q = case 6-1-3-2 !P⟶Q of λ where
  (inj₁ (P′ , P⟶P′ , Q∼!P∣P′)) 
    Q                 ∼⟨ Q∼!P∣P′ 
    ! P  P′          ∼⟨ symmetric 6-2-17-3 ∣-cong reflexive 
    (! P  ! P)  P′  ∼⟨ symmetric ∣-assoc 
    ! P  (! P  P′)  ∼⟨ reflexive ∣-cong symmetric Q∼!P∣P′ ⟩■
    ! P  Q

  (inj₂ (_ , P′ , P″ , _ , P⟶P′ , P⟶P″ , Q∼!P∣P′∣P″)) 
    Q                        ∼⟨ Q∼!P∣P′∣P″ 
    (! P  P′)  P″          ∼⟨ symmetric ∣-assoc 
    ! P  (P′  P″)          ∼⟨ symmetric 6-2-17-3 ∣-cong reflexive 
    (! P  ! P)  (P′  P″)  ∼⟨ symmetric ∣-assoc 
    ! P  (! P  (P′  P″))  ∼⟨ reflexive ∣-cong ∣-assoc 
    ! P  ((! P  P′)  P″)  ∼⟨ reflexive ∣-cong symmetric Q∼!P∣P′∣P″ ⟩■
    ! P  Q

mutual

  6-2-17-4 :  {P i}  [ i ] ! ! P  ! P
  6-2-17-4 {P} {i} =  lr , rl 
    where
    lemma = λ {Q μ} (!P⟶Q : ! P [ μ ]⟶ Q)  ∼′:
      ! ! P  Q  ∼⟨ 6-2-17-4′ {i = i} ∣-cong′ reflexive 
      ! P  Q    ∼⟨ symmetric (6-2-17-4-lemma !P⟶Q) ⟩■
      Q

    lr :  {Q μ} 
         ! ! P [ μ ]⟶ Q 
          λ Q′  ! P [ μ ]⟶ Q′ × [ i ] Q ∼′ Q′
    lr {Q} !!P⟶Q = case 6-1-3-2 !!P⟶Q of λ where
      (inj₁ (Q′ , !P⟶Q′ , Q∼!!P∣Q′)) 
        Q           ∼⟨ Q∼!!P∣Q′ 
        ! ! P  Q′  ∼⟨ lemma !P⟶Q′ ⟩■
        Q′          ⟵⟨ !P⟶Q′ 
        ! P

      (inj₂ (refl , Q′ , Q″ , a , !P⟶Q′ , !P⟶Q″ , Q∼!!P∣Q′∣Q″)) 
        case 6-1-3-2 !P⟶Q″ of λ where
          (inj₂ (() , _))
          (inj₁ (Q‴ , P⟶Q‴ , Q″∼!P∣Q‴)) 
            let !P⟶Q′∣Q″ =
                  ! P      [ τ ]⟶⟨ replication (par-τ !P⟶Q′ P⟶Q‴) 
                  Q′  Q‴
            in
            Q                          ∼⟨ Q∼!!P∣Q′∣Q″ 
            (! ! P  Q′)  Q″          ∼⟨ reflexive ∣-cong Q″∼!P∣Q‴ 
            (! ! P  Q′)  (! P  Q‴)  ∼⟨ swap-in-the-middle 
            (! ! P  ! P)  (Q′  Q‴)  ∼⟨ 6-1-2 ∣-cong reflexive 
            ! ! P  (Q′  Q‴)          ∼⟨ lemma !P⟶Q′∣Q″ ⟩■
            Q′  Q‴                    [ τ ]⟵⟨ !P⟶Q′∣Q″ 
            ! P

    rl :  {Q μ} 
         ! P [ μ ]⟶ Q 
          λ Q′  ! ! P [ μ ]⟶ Q′ × [ i ] Q′ ∼′ Q
    rl {Q} !P⟶Q =
      ! ! P      ⟶⟨ replication (par-right !P⟶Q) ⟩ʳˡ
      ! ! P  Q  ∼⟨ lemma !P⟶Q ⟩■
      Q

  6-2-17-4′ :  {P i}  [ i ] ! ! P ∼′ ! P
  force 6-2-17-4′ = 6-2-17-4

------------------------------------------------------------------------
-- An example from "Coinduction All the Way Up" by Pous

module _ (a b : Name-with-kind) where

  A B C D :  {i}  Proc i

  A = name a · name b · D
  B = name a · name b · C

  C = name (co a) ·′ λ { .force  A  C }
  D = name (co a) ·′ λ { .force  B  D }

  mutual

    A∼B :  {i}  [ i ] A  B
    A∼B = refl ·-cong (refl ·-cong symmetric C∼D)

    C∼D :  {i}  [ i ] C  D
    C∼D = refl ·′-cong λ { .force  A∼B ∣-cong C∼D }

------------------------------------------------------------------------
-- Some other examples

Restricted : Name  Proc 
Restricted a = ν a (name (a , true) · )

Restricted∼∅ :  {a}  Restricted a  
Restricted∼∅ =
    { (restriction x≢x action)  ⊥-elim (x≢x refl) })
  ,  ())
  

module Another-example (a : Name) (μ : Action) where

  P :  {i}  Proc i
  P = Restricted a  (μ ·′ λ { .force  P })

  Q :  {i}  Proc i
  Q = μ ·′ λ { .force  Q }

  P∼Q :  {i}  [ i ] P  Q
  P∼Q = P      ∼⟨ Restricted∼∅ ∣-cong (refl ·′-cong λ { .force  P∼Q }) 
          Q  ∼⟨ ∣-left-identity ⟩■
        Q