------------------------------------------------------------------------
-- The partiality monad
------------------------------------------------------------------------

module Category.Monad.Partiality where

open import Coinduction
open import Category.Monad
open import Data.Bool
open import Data.Nat using (; zero; suc; _+_)
open import Data.Product as Prod
open import Data.Sum
open import Function
open import Function.Equivalence using (_⇔_; equivalent)
open import Level
open import Relation.Binary as B hiding (Rel)
open import Relation.Binary.PropositionalEquality as P using (_≡_)
open import Relation.Nullary
open import Relation.Nullary.Decidable
open import Relation.Nullary.Negation

------------------------------------------------------------------------
-- The partiality monad

data _⊥ (A : Set) : Set where
  now   : (x : A)  A 
  later : (x :  (A ))  A 

monad : RawMonad _⊥
monad = record
  { return = now
  ; _>>=_  = _>>=_
  }
  where
  _>>=_ :  {A B}  A   (A  B )  B 
  now x   >>= f = f x
  later x >>= f = later ( ( x >>= f))

private module M = RawMonad monad

-- Non-termination.

never : {A : Set}  A 
never = later ( never)

-- run x for n steps peels off at most n "later" constructors from x.

run_for_steps :  {A}  A     A 
run now   x for n     steps = now x
run later x for zero  steps = later x
run later x for suc n steps = run  x for n steps

-- Is the computation done?

isNow :  {A}  A   Bool
isNow (now x)   = true
isNow (later x) = false

------------------------------------------------------------------------
-- Kinds

-- The partiality monad comes with two forms of equality (weak and
-- strong) and one ordering. Strong equality is stronger than the
-- ordering, which is stronger than weak equality.

-- The three relations are defined using a single data type, indexed
-- by a "kind".

data OtherKind : Set where
  geq weak : OtherKind

data Kind : Set where
  strong : Kind
  other  : (k : OtherKind)  Kind

-- Kind equality is decidable.

_≟-Kind_ : Decidable (_≡_ {A = Kind})
_≟-Kind_ strong       strong       = yes P.refl
_≟-Kind_ strong       (other k)    = no λ()
_≟-Kind_ (other k)    strong       = no λ()
_≟-Kind_ (other geq)  (other geq)  = yes P.refl
_≟-Kind_ (other geq)  (other weak) = no λ()
_≟-Kind_ (other weak) (other geq)  = no λ()
_≟-Kind_ (other weak) (other weak) = yes P.refl

-- A predicate which is satisfied only for equalities. Note that, for
-- concrete inputs, this predicate evaluates to ⊤ or ⊥.

Equality : Kind  Set
Equality k = False (k ≟-Kind other geq)

------------------------------------------------------------------------
-- Equality/ordering

module Equality {A : Set} -- The "return type".
                (_R_ : A  A  Set) where

  -- The three relations.

  data Rel : Kind  A   A   Set where
    now    :  {k x y} (xRy : x R y)                          Rel k         (now   x) (now   y)
    later  :  {k x y} (x∼y :  (Rel k         ( x) ( y)))  Rel k         (later x) (later y)
    laterʳ :  {x y}   (x≈y :    Rel (other weak) x  ( y) )  Rel (other weak)     x  (later y)
    laterˡ :  {k x y} (x∼y :    Rel (other k) ( x)    y  )  Rel (other k) (later x)        y

  infix 4 _≅_ _≳_ _≲_ _≈_

  _≅_ : A   A   Set
  _≅_ = Rel strong

  _≳_ : A   A   Set
  _≳_ = Rel (other geq)

  _≲_ : A   A   Set
  _≲_ = flip _≳_

  _≈_ : A   A   Set
  _≈_ = Rel (other weak)

------------------------------------------------------------------------
-- Lemmas relating the three relations

  -- All relations include strong equality.

  ≅⇒ :  {k} {x y : A }  x  y  Rel k x y
  ≅⇒ (now xRy)   = now xRy
  ≅⇒ (later x≅y) = later ( ≅⇒ ( x≅y))

  -- The weak equality includes the ordering.

  ≳⇒ :  {k} {x y : A }  x  y  Rel (other k) x y
  ≳⇒ (now xRy)    = now xRy
  ≳⇒ (later  x≳y) = later ( ≳⇒ ( x≳y))
  ≳⇒ (laterˡ x≳y) = laterˡ  (≳⇒    x≳y )

  -- Weak equality includes the other relations.

  ⇒≈ :  {k} {x y : A }  Rel k x y  x  y
  ⇒≈ {strong}     = ≅⇒
  ⇒≈ {other geq}  = ≳⇒
  ⇒≈ {other weak} = id

  -- The relations agree for non-terminating computations.

  never⇒never :  {k₁ k₂} {x : A } 
                Rel k₁ x never  Rel k₂ x never
  never⇒never (later  x∼never) = later ( never⇒never ( x∼never))
  never⇒never (laterʳ x≈never) =          never⇒never    x≈never
  never⇒never (laterˡ x∼never) = later ( never⇒never    x∼never)

  -- The "other" relations agree when the right-hand side is a value.

  now⇒now :  {k₁ k₂} {x} {y : A} 
            Rel (other k₁) x (now y)  Rel (other k₂) x (now y)
  now⇒now (now xRy)      = now xRy
  now⇒now (laterˡ x∼now) = laterˡ (now⇒now x∼now)

------------------------------------------------------------------------
-- Later can be dropped

  laterʳ⁻¹ :  {k} {x : A } {y} 
             Rel (other k) x (later y)  Rel (other k) x ( y)
  laterʳ⁻¹ (later  x∼y)  = laterˡ        ( x∼y)
  laterʳ⁻¹ (laterʳ x≈y)  = x≈y
  laterʳ⁻¹ (laterˡ x∼ly) = laterˡ (laterʳ⁻¹ x∼ly)

  laterˡ⁻¹ :  {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

  later⁻¹ :  {k} {x y :  (A )} 
            Rel k (later x) (later y)  Rel k ( x) ( y)
  later⁻¹ (later  x∼y)  =  x∼y
  later⁻¹ (laterʳ lx≈y) = laterˡ⁻¹ lx≈y
  later⁻¹ (laterˡ x∼ly) = laterʳ⁻¹ x∼ly

------------------------------------------------------------------------
-- Terminating computations

  -- x ⇓ y means that x terminates with y.

  infix 4 _⇓[_]_ _⇓_

  _⇓[_]_ : A   Kind  A  Set
  x ⇓[ k ] y = Rel k x (now y)

  _⇓_ : A   A  Set
  x  y = x ⇓[ other weak ] y

  -- The number of later constructors (steps) in the terminating
  -- computation x.

  steps :  {k} {x : A } {y}  x ⇓[ k ] y  
  steps                (now _)             = zero
  steps .{x = later x} (laterˡ {x = x} x⇓) = suc (steps {x =  x} x⇓)

------------------------------------------------------------------------
-- Non-terminating computations

  -- x ⇑ means that x does not terminate.

  infix 4 _⇑[_] _⇑

  _⇑[_] : A   Kind  Set
  x ⇑[ k ] = Rel k x never

  _⇑ : A   Set
  x  = x ⇑[ other weak ]

------------------------------------------------------------------------
-- The relations are equivalences or partial orders

-- The precondition that the underlying relation is an equivalence can
-- be weakened for some of the properties.

module Properties (S : Setoid zero zero) where

  private
    open module R = Setoid S
      using () renaming (Carrier to A; _≈_ to _R_)
    open Equality _R_

  -- All the relations are preorders.

  preorder : Kind  Preorder _ _ _
  preorder k = record
    { Carrier    = A 
    ; _≈_        = _≡_
    ; _∼_        = Rel k
    ; isPreorder = record
      { isEquivalence = P.isEquivalence
      ; reflexive     = refl _
      ; trans         = trans
      }
    }
    where
    refl :  {k} (x : A ) {y}  x  y  Rel k x y
    refl (now v)   P.refl = now R.refl
    refl (later x) P.refl = later ( refl ( x) P.refl)

    now-R-trans :  {k x} {y z : A} 
                  Rel k x (now y)  y R z  Rel k x (now z)
    now-R-trans (now xRy)    yRz = now (R.trans xRy yRz)
    now-R-trans (laterˡ x∼y) yRz = laterˡ (now-R-trans x∼y yRz)

    now-trans :  {k x y} {v : A} 
                Rel k x y  Rel k y (now v)  Rel k x (now v)
    now-trans x∼ly (laterˡ y∼z) = now-trans (laterʳ⁻¹ x∼ly) y∼z
    now-trans x∼y  (now yRz)    = now-R-trans x∼y yRz

    mutual

      later-trans :  {k} {x y : A } {z} 
                    Rel k x y  Rel k y (later z)  Rel k x (later z)
      later-trans (later  x∼y) (later  y∼z)  = later  ( trans ( x∼y)         ( y∼z))
      later-trans (later  x∼y) (laterˡ y∼lz) = later  ( trans ( x∼y) (laterʳ⁻¹  y∼lz))
      later-trans (laterˡ x∼y)         y∼lz  = later  ( trans    x∼y  (laterʳ⁻¹  y∼lz))
      later-trans (laterʳ x≈y)        ly≈lz  =     later-trans    x≈y  (laterˡ⁻¹ ly≈lz)
      later-trans         x≈y  (laterʳ y≈z)  = laterʳ (  trans    x≈y             y≈z )

      trans :  {k} {x y z : A }  Rel k x y  Rel k y z  Rel k x z
      trans {z = now v}   x∼y y∼v  = now-trans   x∼y y∼v
      trans {z = later z} x∼y y∼lz = later-trans x∼y y∼lz

  private module Pre {k} = Preorder (preorder k)

  -- The two equalities are equivalence relations.

  setoid : (k : Kind) {eq : Equality k}  Setoid _ _
  setoid k {eq} = record
    { Carrier       = A 
    ; _≈_           = Rel k
    ; isEquivalence = record
      { refl  = Pre.refl
      ; sym   = sym eq
      ; trans = Pre.trans
      }
    }
    where
    sym :  {k} {x y : A }  Equality k  Rel k x y  Rel k y x
    sym eq (now xRy)           = now (R.sym xRy)
    sym eq (later         x∼y) = later ( sym eq ( x∼y))
    sym eq (laterʳ        x≈y) = laterˡ  (sym eq    x≈y )
    sym eq (laterˡ {weak} x≈y) = laterʳ  (sym eq    x≈y )
    sym () (laterˡ {geq}  x≳y)

  private module S {k} {eq} = Setoid (setoid k {eq})

  -- The order is a partial order, with strong equality as the
  -- underlying equality.

  ≳-poset : Poset _ _ _
  ≳-poset = record
    { Carrier        = A 
    ; _≈_            = _≅_
    ; _≤_            = _≳_
    ; isPartialOrder = record
      { antisym    = antisym
      ; isPreorder = record
        { isEquivalence = S.isEquivalence
        ; reflexive     = ≅⇒
        ; trans         = Pre.trans
        }
      }
    }
    where
    antisym : {x y : A }  x  y  x  y  x  y
    antisym (now    xRy)  (now    _)    = now xRy
    antisym (later  x≳y)  (later  x≲y)  = later ( antisym        ( x≳y)         ( x≲y))
    antisym (later  x≳y)  (laterˡ x≲ly) = later ( antisym        ( x≳y)  (laterʳ⁻¹ x≲ly))
    antisym (laterˡ x≳ly) (later  x≲y)  = later ( antisym (laterʳ⁻¹ x≳ly)        ( x≲y))
    antisym (laterˡ x≳ly) (laterˡ x≲ly) = later ( antisym (laterʳ⁻¹ x≳ly) (laterʳ⁻¹ x≲ly))

  -- Equational reasoning.

  module Reasoning where

    infix  2 _∎
    infixr 2 _≅⟨_⟩_ _≳⟨_⟩_ _≈⟨_⟩_

    _≅⟨_⟩_ :  {k} x {y z : A }  x  y  Rel k y z  Rel k x z
    _ ≅⟨ x≅y  y∼z = Pre.trans (≅⇒ x≅y) y∼z

    _≳⟨_⟩_ :  {k} x {y z : A } 
             x  y  Rel (other k) y z  Rel (other k) x z
    _ ≳⟨ x≳y  y∼z = Pre.trans (≳⇒ x≳y) y∼z

    _≈⟨_⟩_ :  x {y z : A }  x  y  y  z  x  z
    _ ≈⟨ x≈y  y≈z = Pre.trans x≈y y≈z

    sym :  {k} {eq : Equality k} {x y : A } 
          Rel k x y  Rel k y x
    sym {eq = eq} = S.sym {eq = eq}

    _∎ :  {k} (x : A )  Rel k x x
    x  = Pre.refl

------------------------------------------------------------------------
-- Lemmas related to now and never

  -- Now is not never.

  now≉never :  {k} {x : A}  ¬ Rel k (now x) never
  now≉never (laterʳ hyp) = now≉never hyp

  -- A partial value is either now or never (classically).

  now-or-never :  {k} (x : A ) 
                 ¬ ¬ (( λ y  x ⇓[ other k ] y)  x ⇑[ other k ])
  now-or-never x = helper <$> excluded-middle
    where
    open RawMonad ¬¬-Monad

    not-now-is-never : (x : A )  ( λ y  x  now y)  x  never
    not-now-is-never (now x)   hyp with hyp (, now R.refl)
    ... | ()
    not-now-is-never (later x) hyp =
      later ( not-now-is-never ( x) (hyp  Prod.map id laterˡ))

    helper : Dec ( λ y  x  now y)  _
    helper (yes ≳now) = inj₁ $ Prod.map id ≳⇒ ≳now
    helper (no  ≵now) = inj₂ $ ≳⇒ $ not-now-is-never x ≵now

------------------------------------------------------------------------
-- Lemmas related to steps

  module Steps where

    open P.≡-Reasoning
    open Reasoning using (_≅⟨_⟩_)

    private

      lemma :  {k x y} {z : A}
              (x∼y : Rel (other k) ( x) y)
              (y⇓z : y ⇓[ other k ] z) 
              steps (Pre.trans (laterˡ {x = x} x∼y) y⇓z) 
              suc (steps (Pre.trans x∼y y⇓z))
      lemma x∼y (now yRz)    = P.refl
      lemma x∼y (laterˡ y⇓z) = begin
        steps (Pre.trans (laterˡ (laterʳ⁻¹ x∼y)) y⇓z)  ≡⟨ lemma (laterʳ⁻¹ x∼y) y⇓z 
        suc (steps (Pre.trans (laterʳ⁻¹ x∼y) y⇓z))     

    left-identity :  {k x y} {z : A}
                    (x≅y : x  y) (y⇓z : y ⇓[ k ] z) 
                    steps (x ≅⟨ x≅y  y⇓z)  steps y⇓z
    left-identity (now _)     (now _)      = P.refl
    left-identity (later x≅y) (laterˡ y⇓z) = begin
      steps (Pre.trans (laterˡ (≅⇒ ( x≅y))) y⇓z)  ≡⟨ lemma (≅⇒ ( x≅y)) y⇓z 
      suc (steps (_ ≅⟨  x≅y  y⇓z))               ≡⟨ P.cong suc $ left-identity ( x≅y) y⇓z 
      suc (steps y⇓z)                              

    right-identity :  {k x} {y z : A}
                     (x⇓y : x ⇓[ k ] y) (y≈z : now y ⇓[ k ] z) 
                     steps (Pre.trans x⇓y y≈z)  steps x⇓y
    right-identity (now xRy)    (now yRz) = P.refl
    right-identity (laterˡ x∼y) (now yRz) =
      P.cong suc $ right-identity x∼y (now yRz)

------------------------------------------------------------------------
-- Laws related to bind

  -- Never is a left and right "zero" of bind.

  left-zero : {B : Set} (f : B  A )  let open M in
              (never >>= f)  never
  left-zero f = later ( left-zero f)

  right-zero : {B : Set} (x : B )  let open M in
               (x >>= λ _  never)  never
  right-zero (now   x) = S.refl
  right-zero (later x) = later ( right-zero ( x))

  -- Now is a left and right identity of bind.

  left-identity : {B : Set} (x : B) (f : B  A )  let open M in
                  (now x >>= f)  f x
  left-identity x f = S.refl

  right-identity : (x : A )  let open M in
                   (x >>= now)  x
  right-identity (now   x) = now R.refl
  right-identity (later x) = later ( right-identity ( x))

  -- Bind is associative.

  associative : {B C : Set} (x : C ) (f : C  B ) (g : B  A ) 
                let open M in
                (x >>= f >>= g)  (x >>= λ y  f y >>= g)
  associative (now x)   f g = S.refl
  associative (later x) f g = later ( associative ( x) f g)

module Properties₂ (S₁ S₂ : Setoid zero zero) where

  open Setoid S₁ renaming (Carrier to A; _≈_ to _≈A_)
  open Setoid S₂ renaming (Carrier to B; _≈_ to _≈B_)
  open Equality
  private
    open module EqA = Equality _≈A_ using () renaming (_⇓[_]_ to _⇓[_]A_; _⇑[_] to _⇑[_]A)
    open module EqB = Equality _≈B_ using () renaming (_⇓[_]_ to _⇓[_]B_; _⇑[_] to _⇑[_]B)
    module PropA = Properties S₁
  open PropA.Reasoning

  -- Bind preserves all the relations.

  _>>=-cong_ :
     {k} {x₁ x₂ : A } {f₁ f₂ : A  B }  let open M in
    EqA.Rel k x₁ x₂ 
    (∀ {x₁ x₂}  x₁ ≈A x₂  EqB.Rel k (f₁ x₁) (f₂ x₂)) 
    EqB.Rel k (x₁ >>= f₁) (x₂ >>= f₂)
  now    x₁Rx₂ >>=-cong f₁∼f₂ = f₁∼f₂ x₁Rx₂
  later  x₁∼x₂ >>=-cong f₁∼f₂ = later ( ( x₁∼x₂ >>=-cong f₁∼f₂))
  laterʳ x₁≈x₂ >>=-cong f₁≈f₂ = laterʳ (x₁≈x₂ >>=-cong f₁≈f₂)
  laterˡ x₁∼x₂ >>=-cong f₁∼f₂ = laterˡ (x₁∼x₂ >>=-cong f₁∼f₂)

  -- Inversion lemmas for bind.

  >>=-inversion-⇓ :
     {k} x {f : A  B } {y}  let open M in
    (x>>=f⇓ : (x >>= f) ⇓[ k ]B y) 
     λ z  ∃₂ λ (x⇓ : x ⇓[ k ]A z) (fz⇓ : f z ⇓[ k ]B y) 
                 EqA.steps x⇓ + EqB.steps fz⇓  EqB.steps x>>=f⇓
  >>=-inversion-⇓ (now x) fx⇓ =
    (x , now (Setoid.refl S₁) , fx⇓ , P.refl)
  >>=-inversion-⇓ (later x) (laterˡ x>>=f⇓) =
    Prod.map id (Prod.map laterˡ (Prod.map id (P.cong suc))) $
      >>=-inversion-⇓ ( x) x>>=f⇓

  >>=-inversion-⇑ :  {k} x {f : A  B }  let open M in
                    EqB.Rel (other k) (x >>= f) never 
                    ¬ ¬ (x ⇑[ other k ]A 
                          λ y  x ⇓[ other k ]A y × f y ⇑[ other k ]B)
  >>=-inversion-⇑ {k} x {f} ∼never = helper <$> PropA.now-or-never x
    where
    open RawMonad ¬¬-Monad using (_<$>_)
    open M using (_>>=_)

    k≳ = other geq

    is-never :  {x y} 
               x ⇓[ k≳ ]A y  (x >>= f) ⇑[ k≳ ]B 
                λ z  y ≈A z × f z ⇑[ k≳ ]B
    is-never (now    xRy)  = λ fx⇑  (_ , Setoid.sym S₁ xRy , fx⇑)
    is-never (laterˡ ≳now) = is-never ≳now  EqB.later⁻¹

    helper : ( λ y  x ⇓[ k≳ ]A y)  x ⇑[ k≳ ]A 
             x ⇑[ other k ]A 
              λ y  x ⇓[ other k ]A y × f y ⇑[ other k ]B
    helper (inj₂ ≳never)     = inj₁ (EqA.≳⇒ ≳never)
    helper (inj₁ (y , ≳now)) with is-never ≳now (EqB.never⇒never ∼never)
    ... | (z , yRz , fz⇑) = inj₂ (z , EqA.≳⇒ (x     ≳⟨ ≳now 
                                              now y ≅⟨ now yRz 
                                              now z )
                                    , EqB.≳⇒ fz⇑)

------------------------------------------------------------------------
-- Instantiation of the modules above using propositional equality

module Propositional where
  private
    open module Eq {A : Set} = Equality (_≡_ {A = A}) public
    open module P₁ {A : Set} = Properties (P.setoid A) public
    open module P₂ {A B : Set} =
      Properties₂ (P.setoid A) (P.setoid B) public

  -- If a statement can be proved using propositional equality as the
  -- underlying relation, then it can also be proved for any other
  -- reflexive underlying relation.

  ≡⇒ :  {A : Set} {_≈_ : A  A  Set}  Reflexive _≈_ 
        {k x y}  Rel k x y  Equality.Rel _≈_ k x y
  ≡⇒ refl (now P.refl) = Equality.now refl
  ≡⇒ refl (later  x∼y) = Equality.later ( ≡⇒ refl ( x∼y))
  ≡⇒ refl (laterʳ x≈y) = Equality.laterʳ  (≡⇒ refl    x≈y)
  ≡⇒ refl (laterˡ x∼y) = Equality.laterˡ  (≡⇒ refl    x∼y)

------------------------------------------------------------------------
-- Productivity checker workaround

-- The monad can be awkward to use, due to the limitations of guarded
-- coinduction. The following code provides a (limited) workaround.

module Workaround where

  infixl 1 _>>=_

  data _⊥P : Set  Set₁ where
    now   :  {A} (x : A)  A ⊥P
    later :  {A} (x :  (A ⊥P))  A ⊥P
    _>>=_ :  {A B} (x : A ⊥P) (f : A  B ⊥P)  B ⊥P

  private

    data _⊥W : Set  Set₁ where
      now   :  {A} (x : A)  A ⊥W
      later :  {A} (x : A ⊥P)  A ⊥W

    mutual

      _>>=W_ :  {A B}  A ⊥W  (A  B ⊥P)  B ⊥W
      now   x >>=W f = whnf (f x)
      later x >>=W f = later (x >>= f)

      whnf :  {A}  A ⊥P  A ⊥W
      whnf (now   x) = now x
      whnf (later x) = later ( x)
      whnf (x >>= f) = whnf x >>=W f

  mutual

    private

      ⟦_⟧W :  {A}  A ⊥W  A 
       now   x ⟧W = now x
       later x ⟧W = later (  x ⟧P)

    ⟦_⟧P :  {A}  A ⊥P  A 
     x ⟧P =  whnf x ⟧W

  -- The definitions above make sense. ⟦_⟧P is homomorphic with
  -- respect to now, later and _>>=_.

  module Correct where

    open Propositional
    open Reasoning

    now-hom :  {A} (x : A)   now x ⟧P  now x
    now-hom x = now x 

    later-hom :  {A} (x :  (A ⊥P)) 
                 later x ⟧P  later (   x ⟧P)
    later-hom x = later ( (  x ⟧P ))

    mutual

      private

        >>=-homW :  {A B} (x : B ⊥W) (f : B  A ⊥P) 
                    x >>=W f ⟧W  M._>>=_  x ⟧W  y   f y ⟧P)
        >>=-homW (now   x) f =  f x ⟧P 
        >>=-homW (later x) f = later ( >>=-hom x f)

      >>=-hom :  {A B} (x : B ⊥P) (f : B  A ⊥P) 
                 x >>= f ⟧P  M._>>=_  x ⟧P  y   f y ⟧P)
      >>=-hom x f = >>=-homW (whnf x) f

------------------------------------------------------------------------
-- An alternative, but equivalent, formulation of equality/ordering

module AlternativeEquality where

  private

    El : Setoid zero zero  Set
    El = Setoid.Carrier

    Eq :  S  B.Rel (El S) _
    Eq = Setoid._≈_

  open Equality using (Rel)
  open Equality.Rel

  infix  4 _∣_≅P_ _∣_≳P_ _∣_≈P_
  infix  2 _∎
  infixr 2 _≅⟨_⟩_ _≳⟨_⟩_ _≳⟨_⟩≅_ _≳⟨_⟩≈_ _≈⟨_⟩≅_ _≈⟨_⟩≲_
  infixl 1 _>>=_

  mutual

    -- Proof "programs".

    _∣_≅P_ :  S  B.Rel (El S ) _
    _∣_≅P_ = flip RelP strong

    _∣_≳P_ :  S  B.Rel (El S ) _
    _∣_≳P_ = flip RelP (other geq)

    _∣_≈P_ :  S  B.Rel (El S ) _
    _∣_≈P_ = flip RelP (other weak)

    data RelP S : Kind  B.Rel (El S ) (suc zero) where

      -- Congruences.

      now   :  {k x y} (xRy : x  Eq S  y)  RelP S k (now x) (now y)
      later :  {k x y} (x∼y :  (RelP S k ( x) ( y))) 
              RelP S k (later x) (later y)
      _>>=_ :  {S′ : Setoid zero zero} {k} {x₁ x₂}
                {f₁ f₂ : El S′  El S } 
              let open M in
              (x₁∼x₂ : RelP S′ k x₁ x₂)
              (f₁∼f₂ :  {x y}  x  Eq S′  y 
                       RelP S k (f₁ x) (f₂ y)) 
              RelP S k (x₁ >>= f₁) (x₂ >>= f₂)

      -- Ordering/weak equality.

      laterʳ :    {x y} (x≈y : RelP S (other weak) x ( y))  RelP S (other weak)     x (later y)
      laterˡ :  {k x y} (x∼y : RelP S (other k) ( x)   y)   RelP S (other k) (later x)       y

      -- Equational reasoning. Note that including full transitivity
      -- for weak equality would make _∣_≈P_ trivial; a similar
      -- problem applies to _∣_≳P_ (A ∣ never ≳P now x would be
      -- provable). Instead the definition of RelP includes limited
      -- notions of transitivity, similar to weak bisimulation up-to
      -- various things.

      _∎      :  {k} x  RelP S k x x
      sym     :  {k x y} {eq : Equality k} (x∼y : RelP S k x y)  RelP S k y x
      _≅⟨_⟩_  :  {k} x {y z} (x≅y : S  x ≅P y) (y∼z : RelP S k y z)  RelP S k x z
      _≳⟨_⟩_  : let open Equality (Eq S) in
                     x {y z} (x≳y :     x   y) (y≳z : S  y ≳P z)  S  x ≳P z
      _≳⟨_⟩≅_ :      x {y z} (x≳y : S  x ≳P y) (y≅z : S  y ≅P z)  S  x ≳P z
      _≳⟨_⟩≈_ :      x {y z} (x≳y : S  x ≳P y) (y≈z : S  y ≈P z)  S  x ≈P z
      _≈⟨_⟩≅_ :      x {y z} (x≈y : S  x ≈P y) (y≅z : S  y ≅P z)  S  x ≈P z
      _≈⟨_⟩≲_ :      x {y z} (x≈y : S  x ≈P y) (y≲z : S  z ≳P y)  S  x ≈P z

      -- If any of the following transitivity-like rules were added to
      -- RelP, then RelP and Rel would no longer be equivalent:
      --
      --   x ≳P y → y ≳P z → x ≳P z
      --   x ≳P y → y ≳  z → x ≳P z
      --   x ≲P y → y ≈P z → x ≈P z
      --   x ≈P y → y ≳P z → x ≈P z
      --   x ≲  y → y ≈P z → x ≈P z
      --   x ≈P y → y ≳  z → x ≈P z
      --   x ≈P y → y ≈P z → x ≈P z
      --   x ≈P y → y ≈  z → x ≈P z
      --   x ≈  y → y ≈P z → x ≈P z
      --
      -- The reason is that any of these rules would make it possible
      -- to derive that never and now x are related.

  -- RelP is complete with respect to Rel.

  complete :  {S k} {x y : El S } 
             Equality.Rel (Eq S) k x y  RelP S k x y
  complete (now xRy)    = now xRy
  complete (later  x∼y) = later ( complete ( x∼y))
  complete (laterʳ x≈y) = laterʳ  (complete    x≈y)
  complete (laterˡ x∼y) = laterˡ  (complete    x∼y)

  -- RelP is sound with respect to Rel.

  private

    -- Proof WHNFs.

    data RelW S : Kind  B.Rel (El S ) (suc zero) where
      now    :  {k x y} (xRy : x  Eq S  y)                  RelW S k         (now   x) (now   y)
      later  :  {k x y} (x∼y : RelP S k         ( x) ( y))  RelW S k         (later x) (later y)
      laterʳ :    {x y} (x≈y : RelW S (other weak) x  ( y))  RelW S (other weak)     x  (later y)
      laterˡ :  {k x y} (x∼y : RelW S (other k) ( x)    y)   RelW S (other k) (later x)        y

    -- WHNFs can be turned into programs.

    program :  {S k x y}  RelW S k x y  RelP S k x y
    program (now    xRy) = now xRy
    program (later  x∼y) = later ( x∼y)
    program (laterˡ x∼y) = laterˡ (program x∼y)
    program (laterʳ x≈y) = laterʳ (program x≈y)

    -- Lemmas for WHNFs.

    _>>=W_ :  {A B k x₁ x₂} {f₁ f₂ : El A  El B } 
             RelW A k x₁ x₂ 
             (∀ {x y}  x  Eq A  y  RelW B k (f₁ x) (f₂ y)) 
             RelW B k (M._>>=_ x₁ f₁) (M._>>=_ x₂ f₂)
    now    xRy >>=W f₁∼f₂ = f₁∼f₂ xRy
    later  x∼y >>=W f₁∼f₂ = later  (x∼y >>= program  f₁∼f₂)
    laterʳ x≈y >>=W f₁≈f₂ = laterʳ (x≈y >>=W f₁≈f₂)
    laterˡ x∼y >>=W f₁∼f₂ = laterˡ (x∼y >>=W f₁∼f₂)

    reflW :  {S k} x  RelW S k x x
    reflW {S} (now   x) = now (Setoid.refl S)
    reflW     (later x) = later ( x )

    symW :  {S k x y}  Equality k  RelW S k x y  RelW S k y x
    symW {S} eq (now           xRy) = now (Setoid.sym S xRy)
    symW     eq (later         x≈y) = later  (sym {eq = eq} x≈y)
    symW     eq (laterʳ        x≈y) = laterˡ (symW      eq  x≈y)
    symW     eq (laterˡ {weak} x≈y) = laterʳ (symW      eq  x≈y)
    symW     () (laterˡ {geq}  x≈y)

    trans≅W :  {S x y z} 
              RelW S strong x y  RelW S strong y z  RelW S strong x z
    trans≅W {S} (now   xRy) (now   yRz) = now (Setoid.trans S xRy yRz)
    trans≅W     (later x≅y) (later y≅z) = later (_ ≅⟨ x≅y  y≅z)

    trans≳-W :  {S x y z}  let open Equality (Eq S) in
               x  y  RelW S (other geq) y z  RelW S (other geq) x z
    trans≳-W {S} (now    xRy) (now    yRz) = now (Setoid.trans S xRy yRz)
    trans≳-W     (later  x≳y) (later  y≳z) = later (_ ≳⟨  x≳y  y≳z)
    trans≳-W     (later  x≳y) (laterˡ y≳z) = laterˡ (trans≳-W ( x≳y) y≳z)
    trans≳-W     (laterˡ x≳y)         y≳z  = laterˡ (trans≳-W    x≳y  y≳z)

    -- Strong equality programs can be turned into WHNFs.

    whnf≅ :  {S x y}  S  x ≅P y  RelW S strong x y
    whnf≅ (now xRy)         = now xRy
    whnf≅ (later x≅y)       = later ( x≅y)
    whnf≅ (x₁≅x₂ >>= f₁≅f₂) = whnf≅ x₁≅x₂ >>=W λ xRy  whnf≅ (f₁≅f₂ xRy)
    whnf≅ (x )             = reflW x
    whnf≅ (sym x≅y)         = symW _ (whnf≅ x≅y)
    whnf≅ (x ≅⟨ x≅y  y≅z)  = trans≅W (whnf≅ x≅y) (whnf≅ y≅z)

    -- More transitivity lemmas.

    _⟨_⟩≅_ :  {S k} x {y z} 
             RelP S k x y  S  y ≅P z  RelP S k x z
    _⟨_⟩≅_ {k = strong}     x x≅y y≅z = x ≅⟨ x≅y   y≅z
    _⟨_⟩≅_ {k = other geq}  x x≳y y≅z = x ≳⟨ x≳y ⟩≅ y≅z
    _⟨_⟩≅_ {k = other weak} x x≈y y≅z = x ≈⟨ x≈y ⟩≅ y≅z

    trans∼≅W :  {S k x y z} 
               RelW S k x y  RelW S strong y z  RelW S k x z
    trans∼≅W {S} (now    xRy) (now   yRz) = now (Setoid.trans S xRy yRz)
    trans∼≅W     (later  x∼y) (later y≅z) = later (_  x∼y ⟩≅ y≅z)
    trans∼≅W     (laterʳ x≈y) (later y≅z) = laterʳ (trans∼≅W x≈y (whnf≅ y≅z))
    trans∼≅W     (laterˡ x∼y)        y≅z  = laterˡ (trans∼≅W x∼y        y≅z)

    trans≅∼W :  {S k x y z} 
               RelW S strong x y  RelW S k y z  RelW S k x z
    trans≅∼W {S} (now   xRy) (now     yRz) = now (Setoid.trans S xRy yRz)
    trans≅∼W     (later x≅y) (later   y∼z) = later (_ ≅⟨ x≅y  y∼z)
    trans≅∼W     (later x≅y) (laterˡ  y∼z) = laterˡ (trans≅∼W (whnf≅ x≅y) y∼z)
    trans≅∼W            x≅y  (laterʳ ly≈z) = laterʳ (trans≅∼W        x≅y ly≈z)

    -- Order programs can be turned into WHNFs.

    whnf≳ :  {S x y}  S  x ≳P y  RelW S (other geq) x y
    whnf≳ (now xRy)           = now xRy
    whnf≳ (later  x∼y)        = later ( x∼y)
    whnf≳ (laterˡ x≲y)        = laterˡ (whnf≳ x≲y)
    whnf≳ (x₁∼x₂ >>= f₁∼f₂)   = whnf≳ x₁∼x₂ >>=W λ xRy  whnf≳ (f₁∼f₂ xRy)
    whnf≳ (x )               = reflW x
    whnf≳ (sym {eq = ()} x≅y)
    whnf≳ (x ≅⟨ x≅y   y≳z)   = trans≅∼W (whnf≅ x≅y) (whnf≳ y≳z)
    whnf≳ (x ≳⟨ x≳y   y≳z)   = trans≳-W        x≳y  (whnf≳ y≳z)
    whnf≳ (x ≳⟨ x≳y ⟩≅ y≅z)   = trans∼≅W (whnf≳ x≳y) (whnf≅ y≅z)

    -- Another transitivity lemma.

    trans≳≈W :  {S x y z} 
               RelW S (other geq) x y  RelW S (other weak) y z 
               RelW S (other weak) x z
    trans≳≈W {S} (now    xRy) (now    yRz) = now (Setoid.trans S xRy yRz)
    trans≳≈W     (later  x≳y) (later  y≈z) = later (_ ≳⟨ x≳y ⟩≈ y≈z)
    trans≳≈W     (laterˡ x≳y)         y≈z  = laterˡ (trans≳≈W        x≳y  y≈z)
    trans≳≈W             x≳y  (laterʳ y≈z) = laterʳ (trans≳≈W        x≳y  y≈z)
    trans≳≈W     (later  x≳y) (laterˡ y≈z) = laterˡ (trans≳≈W (whnf≳ x≳y) y≈z)

    -- All programs can be turned into WHNFs.

    whnf :  {S k x y}  RelP S k x y  RelW S k x y
    whnf (now xRy)           = now xRy
    whnf (later  x∼y)        = later     ( x∼y)
    whnf (laterʳ x≈y)        = laterʳ (whnf x≈y)
    whnf (laterˡ x∼y)        = laterˡ (whnf x∼y)
    whnf (x₁∼x₂ >>= f₁∼f₂)   = whnf x₁∼x₂ >>=W λ xRy  whnf (f₁∼f₂ xRy)
    whnf (x )               = reflW x
    whnf (sym {eq = eq} x≈y) = symW eq (whnf x≈y)
    whnf (x ≅⟨ x≅y   y∼z)   = trans≅∼W (whnf x≅y) (whnf y∼z)
    whnf (x ≳⟨ x≳y   y≳z)   = trans≳-W       x≳y  (whnf y≳z)
    whnf (x ≳⟨ x≳y ⟩≅ y≅z)   = trans∼≅W (whnf x≳y) (whnf y≅z)
    whnf (x ≳⟨ x≳y ⟩≈ y≈z)   = trans≳≈W (whnf x≳y) (whnf y≈z)
    whnf (x ≈⟨ x≈y ⟩≅ y≅z)   = trans∼≅W (whnf x≈y) (whnf y≅z)
    whnf (x ≈⟨ x≈y ⟩≲ y≲z)   = symW _ (trans≳≈W (whnf y≲z) (symW _ (whnf x≈y)))

  mutual

    -- Soundness.

    private

      soundW :  {S k x y}  RelW S k x y  Rel (Eq S) k x y
      soundW (now    xRy) = now xRy
      soundW (later  x∼y) = later ( sound  x∼y)
      soundW (laterʳ x≈y) = laterʳ  (soundW x≈y)
      soundW (laterˡ x∼y) = laterˡ  (soundW x∼y)

    sound :  {S k x y}  RelP S k x y  Rel (Eq S) k x y
    sound x∼y = soundW (whnf x∼y)

  -- RelP and Rel are equivalent (when the underlying relation is an
  -- equivalence).

  correct :  {S k x y}  RelP S k x y  Rel (Eq S) k x y
  correct = equivalent sound complete

------------------------------------------------------------------------
-- Example

private
 module Example where

  open Data.Nat
  open Workaround

  -- McCarthy's f91:

  f91′ :    ⊥P
  f91′ n with n ≤? 100
  ... | yes _ = later ( (f91′ (11 + n) >>= f91′))
  ... | no  _ = now (n  10)

  f91 :    
  f91 n =  f91′ n ⟧P