module AdmissibleButNotPostulable where
open import Coinduction using (∞; ♯_; ♭)
open import Data.Nat
open import Data.Product as Prod
open import Function
open import Relation.Binary.PropositionalEquality as P using (_≡_; [_])
open import Relation.Nullary using (¬_)
data _⊥ (A : Set) : Set where
now : (v : A) → A ⊥
later : (x : ∞ (A ⊥)) → A ⊥
module WeakEquality where
infix 4 _≈_
data _≈_ {A : Set} : A ⊥ → A ⊥ → Set where
now : ∀ {v} → now v ≈ now v
later : ∀ {x y} (x≈y : ∞ (♭ x ≈ ♭ y)) → later x ≈ later y
laterʳ : ∀ {x y} (x≈y : x ≈ ♭ y ) → x ≈ later y
laterˡ : ∀ {x y} (x≈y : ♭ x ≈ y ) → later x ≈ y
laterʳ⁻¹ : ∀ {A : Set} {x : A ⊥} {y} → x ≈ later y → x ≈ ♭ y
laterʳ⁻¹ (later x≈y) = laterˡ (♭ x≈y)
laterʳ⁻¹ (laterʳ x≈y) = x≈y
laterʳ⁻¹ (laterˡ x≈ly) = laterˡ (laterʳ⁻¹ x≈ly)
laterˡ⁻¹ : ∀ {A : Set} {x} {y : A ⊥} → later x ≈ y → ♭ x ≈ y
laterˡ⁻¹ (later x≈y) = laterʳ (♭ x≈y)
laterˡ⁻¹ (laterʳ lx≈y) = laterʳ (laterˡ⁻¹ lx≈y)
laterˡ⁻¹ (laterˡ x≈y) = x≈y
refl : {A : Set} (x : A ⊥) → x ≈ x
refl (now v) = now
refl (later x) = later (♯ refl (♭ x))
sym : {A : Set} {x y : A ⊥} → x ≈ y → y ≈ x
sym now = now
sym (later x≈y) = later (♯ sym (♭ x≈y))
sym (laterʳ x≈y) = laterˡ (sym x≈y)
sym (laterˡ x≈y) = laterʳ (sym x≈y)
trans : {A : Set} {x y z : A ⊥} → x ≈ y → y ≈ z → x ≈ z
trans {x = now v} {z = z} p q = tr p q
where
tr : ∀ {y} → now v ≈ y → y ≈ z → now v ≈ z
tr now y≈z = y≈z
tr (laterʳ v≈y) ly≈z = tr v≈y (laterˡ⁻¹ ly≈z)
trans {x = later x} lx≈y y≈z = tr lx≈y y≈z
where
tr : ∀ {y z} → later x ≈ y → y ≈ z → later x ≈ z
tr lx≈ly (later y≈z) = later (♯ trans (laterˡ⁻¹ lx≈ly) (laterˡ (♭ y≈z)))
tr lx≈y (laterʳ y≈z) = later (♯ trans (laterˡ⁻¹ lx≈y) y≈z )
tr lx≈ly (laterˡ y≈z) = tr (laterʳ⁻¹ lx≈ly) y≈z
tr (laterˡ x≈y) y≈z = laterˡ ( trans x≈y y≈z )
never : {A : Set} → A ⊥
never = later (♯ never)
non-trivial : {A : Set} {v : A} → ¬ now v ≈ never
non-trivial (laterʳ v≈⊥) = non-trivial v≈⊥
module ExtendedWeakEquality where
infix 4 _≈_
infix 3 _∎
infixr 2 _≈⟨_⟩_
data _≈_ {A : Set} : A ⊥ → A ⊥ → Set where
now : ∀ {v} → now v ≈ now v
later : ∀ {x y} (x≈y : ∞ (♭ x ≈ ♭ y)) → later x ≈ later y
laterʳ : ∀ {x y} (x≈y : x ≈ ♭ y ) → x ≈ later y
laterˡ : ∀ {x y} (x≈y : ♭ x ≈ y ) → later x ≈ y
_≈⟨_⟩_ : ∀ x {y z} (x≈y : x ≈ y) (y≈z : y ≈ z) → x ≈ z
_∎ : {A : Set} (x : A ⊥) → x ≈ x
now v ∎ = now
later x ∎ = later (♯ (♭ x ∎))
trivial : {A : Set} (x y : A ⊥) → x ≈ y
trivial x y =
x ≈⟨ laterʳ (x ∎) ⟩
later (♯ x) ≈⟨ later (♯ trivial x y) ⟩
later (♯ y) ≈⟨ laterˡ (y ∎) ⟩
y ∎
module Capretta'sEquality where
infix 4 _⇓_ _≈_
data _⇓_ {A : Set} : A ⊥ → A → Set where
now : ∀ {v} → now v ⇓ v
later : ∀ {x v} (x⇓v : ♭ x ⇓ v) → later x ⇓ v
data _≈_ {A : Set} : A ⊥ → A ⊥ → Set where
now : ∀ {x y v} (x⇓v : x ⇓ v) (y⇓v : y ⇓ v) → x ≈ y
later : ∀ {x y} (x≈y : ∞ (♭ x ≈ ♭ y)) → later x ≈ later y
open WeakEquality using () renaming (_≈_ to _≋_)
sound : {A : Set} {x y : A ⊥} → x ≈ y → x ≋ y
sound (later x≈y) = WeakEquality.later (♯ sound (♭ x≈y))
sound (now x⇓v y⇓v) = nw x⇓v y⇓v
where
nw : ∀ {A : Set} {x y : A ⊥} {v} → x ⇓ v → y ⇓ v → x ≋ y
nw now now = WeakEquality.now
nw x⇓v (later y⇓v) = WeakEquality.laterʳ (nw x⇓v y⇓v)
nw (later x⇓v) y⇓v = WeakEquality.laterˡ (nw x⇓v y⇓v)
data _≈P_ {A : Set} : A ⊥ → A ⊥ → Set where
now : ∀ {x y v} (x⇓v : x ⇓ v) (y⇓v : y ⇓ v) → x ≈P y
later : ∀ {x y} (x≈y : ∞ (♭ x ≈P ♭ y)) → later x ≈P later y
laterʳ : ∀ {x y} (x≈y : x ≈P ♭ y ) → x ≈P later y
laterˡ : ∀ {x y} (x≈y : ♭ x ≈P y ) → later x ≈P y
data _≈W_ {A : Set} : A ⊥ → A ⊥ → Set where
now : ∀ {x y v} (x⇓v : x ⇓ v) (y⇓v : y ⇓ v) → x ≈W y
later : ∀ {x y} (x≈y : ♭ x ≈P ♭ y) → later x ≈W later y
laterʳW : ∀ {A : Set} {x : A ⊥} {y} → x ≈W ♭ y → x ≈W later y
laterʳW {y = y} x≈y with ♭ y | P.inspect ♭ y
laterʳW x≈y | y′ | [ eq ] with x≈y
laterʳW x≈y | y′ | [ eq ] | now {v = v} x⇓v y⇓v =
now x⇓v (later (P.subst (λ y → y ⇓ v) (P.sym eq) y⇓v))
laterʳW x≈y | later y′ | [ eq ] | later x′≈y′ =
later (P.subst (_≈P_ _) (P.sym eq) (laterʳ x′≈y′))
laterˡW : ∀ {A : Set} {x} {y : A ⊥} → ♭ x ≈W y → later x ≈W y
laterˡW {x = x} x≈y with ♭ x | P.inspect ♭ x
laterˡW x≈y | x′ | [ eq ] with x≈y
laterˡW x≈y | x′ | [ eq ] | now {v = v} x⇓v y⇓v =
now (later (P.subst (λ x → x ⇓ v) (P.sym eq) x⇓v)) y⇓v
laterˡW x≈y | later x′ | [ eq ] | later {y = y′} x′≈y′ =
later (P.subst (λ x → x ≈P ♭ y′) (P.sym eq) (laterˡ x′≈y′))
whnf : {A : Set} {x y : A ⊥} → x ≈P y → x ≈W y
whnf (now x⇓v y⇓v) = now x⇓v y⇓v
whnf (later x≈y) = later (♭ x≈y)
whnf (laterʳ x≈y) = laterʳW (whnf x≈y)
whnf (laterˡ x≈y) = laterˡW (whnf x≈y)
mutual
⟦_⟧W : {A : Set} {x y : A ⊥} → x ≈W y → x ≈ y
⟦ now x⇓v y⇓v ⟧W = now x⇓v y⇓v
⟦ later x≈y ⟧W = later (♯ ⟦ x≈y ⟧P)
⟦_⟧P : {A : Set} {x y : A ⊥} → x ≈P y → x ≈ y
⟦ x≈y ⟧P = ⟦ whnf x≈y ⟧W
complete : {A : Set} {x y : A ⊥} → x ≋ y → x ≈ y
complete x≋y = ⟦ completeP x≋y ⟧P
where
completeP : {A : Set} {x y : A ⊥} → x ≋ y → x ≈P y
completeP WeakEquality.now = now now now
completeP (WeakEquality.later x≈y) = later (♯ completeP (♭ x≈y))
completeP (WeakEquality.laterʳ x≈y) = laterʳ (completeP x≈y)
completeP (WeakEquality.laterˡ x≈y) = laterˡ (completeP x≈y)
module WeakBisimilarity {A : Set} where
drop : ℕ → A ⊥ → A ⊥
drop zero x = x
drop _ (now v) = now v
drop (suc n) (later x) = drop n (♭ x)
record IsWeakSimulation (_R_ : A ⊥ → A ⊥ → Set) : Set where
field
match-later : ∀ {x y} → later x R y → ∃ λ n → ♭ x R drop n y
match-now : ∀ {v y} → now v R y → ∃ λ n → now v ≡ drop n y
record IsWeakBisimulation (_R_ : A ⊥ → A ⊥ → Set) : Set where
field
left : IsWeakSimulation _R_
right : IsWeakSimulation (flip _R_)
record _≈_ (x y : A ⊥) : Set₁ where
field
_R_ : A ⊥ → A ⊥ → Set
xRy : x R y
bisim : IsWeakBisimulation _R_
open WeakEquality hiding (module _≈_) renaming (_≈_ to _≋_)
complete : ∀ {x y} → x ≋ y → x ≈ y
complete x≋y = record
{ _R_ = _≋_
; xRy = x≋y
; bisim = record
{ left = record
{ match-later = λ lx≋y → (0 , laterˡ⁻¹ lx≋y)
; match-now = match-now
}
; right = record
{ match-later = λ x≋ly → (0 , laterʳ⁻¹ x≋ly)
; match-now = match-now ∘ sym
}
}
}
where
match-now : ∀ {v y} → now v ≋ y → ∃ λ n → now v ≡ drop n y
match-now now = (0 , P.refl)
match-now (laterʳ v≋y) = Prod.map suc id (match-now v≋y)
module Sound {x y} (x≈y : x ≈ y) where
open _≈_ x≈y
open IsWeakBisimulation
open IsWeakSimulation
helper₁ : ∀ {x} y → (∃ λ n → now x ≡ drop n y) → now x ≋ y
helper₁ (now y) (zero , P.refl) = now
helper₁ (now y) (suc n , P.refl) = now
helper₁ (later y) (zero , ())
helper₁ (later y) (suc n , nx≡y-n) =
laterʳ (helper₁ (♭ y) (n , nx≡y-n))
mutual
helper₂ : ∀ {x} y → (∃ λ n → x R drop n y) → x ≋ y
helper₂ y (zero , xRy) = sound _ _ xRy
helper₂ (now y) (suc n , xRny) = sound _ _ xRny
helper₂ (later y) (suc n , xRy-n) =
laterʳ (helper₂ (♭ y) (n , xRy-n))
helper₃ : ∀ x {y} → (∃ λ n → drop (suc n) x R y) → x ≋ y
helper₃ (now x) (n , nxRy) = sound _ _ nxRy
helper₃ (later x) (zero , xRy) = laterˡ (sound _ _ xRy)
helper₃ (later x) (suc n , x-nRy) =
laterˡ (helper₃ (♭ x) (n , x-nRy))
sound : ∀ x y → x R y → x ≋ y
sound (now x) y nxRy = helper₁ y $ match-now (left bisim) nxRy
sound (later x) (now y) lxRny =
sym $ helper₁ (later x) $ match-now (right bisim) lxRny
sound (later x) (later y) lxRly
with match-later (left bisim) lxRly
... | (suc n , xRy-n) = later (♯ helper₂ (♭ y) (n , xRy-n))
... | (zero , xRly) with match-later (right bisim) xRly
... | (zero , xRy) = later (♯ sound _ _ xRy)
... | (suc n , x-1+nRy) =
later (♯ helper₃ (♭ x) (n , x-1+nRy))
sound : ∀ {x y} → x ≈ y → x ≋ y
sound x≈y = Sound.sound x≈y _ _ (_≈_.xRy x≈y)