-- An up-to technique for weak similarity

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

open import Labelled-transition-system

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

open import Logical-equivalence using (_⇔_)
open import Prelude

open import Equational-reasoning
open import Expansion lts using (Expansion)
open import Relation
open import Similarity.Weak lts
import Similarity.Weak.Equational-reasoning-instances
import Up-to

open LTS lts

-- The general up-to machinery, instantiated with the StepC container

open Up-to StepC public

-- An example

-- Up to expansion to the left and weak similarity to the right.
-- This is a generalisation of the non-symmetric up-to technique
-- presented by Pous and Sangiorgi in Section of "Enhancements
-- of the bisimulation proof method".

Up-to-expansion-and-weak-similarity : Trans₂  Proc
Up-to-expansion-and-weak-similarity R =
  Expansion   R  Weak-similarity 

-- The relation transformer is monotone.

up-to-expansion-and-weak-similarity-monotone :
  Monotone Up-to-expansion-and-weak-similarity
up-to-expansion-and-weak-similarity-monotone R⊆S =
  Σ-map id (Σ-map id (Σ-map id (Σ-map R⊆S id)))

-- The relation transformer is size-preserving.

up-to-expansion-and-weak-similarity-size-preserving :
  Size-preserving Up-to-expansion-and-weak-similarity
up-to-expansion-and-weak-similarity-size-preserving =
  _⇔_.from (monotone→⇔ up-to-expansion-and-weak-similarity-monotone)
       {x = p , q} (r , p≳r , s , r≼s , s≼q) 
         p  ∼⟨ p≳r 
         r  ∼′⟨ r≼s  ≼:
         s  ∼⟨ s≼q ⟩■