{-# OPTIONS --without-K --safe #-}
open import Labelled-transition-system
module Similarity.Weak {ℓ} (lts : LTS ℓ) where
open import Equality.Propositional
open import Prelude
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 : Container (Proc × Proc) (Proc × Proc)
StepC = General.StepC
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
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
≈⇒≼ : ∀ {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
≤⇒≼ : ∀ {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-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
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
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)