module AdmissibleButNotPostulable where
open import Coinduction 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
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ʳ⁻¹ : ∀ {A : Set} {x : A ⊥} {y} → x ≈P later y → x ≈P ♭ y
laterʳ⁻¹ (now x⇓v (later y⇓v)) = now x⇓v y⇓v
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 ≈P y → ♭ x ≈P y
laterˡ⁻¹ (now (later x⇓v) y⇓v) = now x⇓v y⇓v
laterˡ⁻¹ (later x≈y) = laterʳ (♭ x≈y)
laterˡ⁻¹ (laterʳ lx≈y) = laterʳ (laterˡ⁻¹ lx≈y)
laterˡ⁻¹ (laterˡ x≈y) = 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 {x = later x} (laterʳ x≈y) = later (laterˡ⁻¹ x≈y)
whnf {x = now v} (laterʳ x≈y) with whnf x≈y
... | now x⇓v y⇓v = now x⇓v (later y⇓v)
whnf {y = later y} (laterˡ x≈y) = later (laterʳ⁻¹ x≈y)
whnf {y = now v} (laterˡ x≈y) with whnf x≈y
... | now x⇓v y⇓v = now (later x⇓v) y⇓v
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)