------------------------------------------------------------------------
-- The barred-by relation
------------------------------------------------------------------------

open import Relation.Binary

module Bar {S : Set} (_⟶_ : Rel S) where

open import Data.Product
open import Data.Sum
open import Data.Star
open import Data.Function
open import Data.Empty
open import Relation.Nullary
open import Relation.Unary

open import Infinite hiding (∞′→∞; ∞″→∞; ∞″→∞′; ∞→∞′)

------------------------------------------------------------------------
-- Types

-- x ⟶ means that x is not stuck.

_⟶ : S -> Set
x ⟶ = ∃ \y -> x ⟶ y

-- x ↛ means that x is stuck.

_↛ : S -> Set
x ↛ = ¬ (x ⟶)

-- x ◁ P ("x is barred by P") means that at least one state in P will
-- be reached.

-- Note that the definition used in the paper is incorrect. If, for
-- instance, _⟶_ contains a transition to some stuck state s from all
-- other states, then s ◁ P (as defined in the paper, i.e. without
-- "x ⟶") is trivially satisfied for any s and P.

data _◁_ (x : S) (P : Pred S) : Set where
  -- P will be reached because we are already there.
  directly : (x∈P : x ∈ P) -> x ◁ P
  -- P will be reached because
  --   ⑴ we can take a step, and
  --   ⑵ no matter which step we take we will reach P.
  via : (x⟶ : x ⟶) (x⟶y◁P : forall {y} -> x ⟶ y -> y ◁ P) -> x ◁ P

-- x ◁∞ P means that every finite reduction path (which is not part of
-- an infinite path) contains a state in P.

codata _◁∞_ (x : S) (P : Pred S) : Set where
  directly : (x∈P : x ∈ P) -> x ◁∞ P
  via : (x⟶ : x ⟶) (x⟶y◁∞P : forall {y} -> x ⟶ y -> y ◁∞ P) -> x ◁∞ P

------------------------------------------------------------------------
-- Conversions

◁⇒◁∞ : forall {x P} -> x ◁ P -> x ◁∞ P
◁⇒◁∞ (directly x∈P) = directly x∈P
◁⇒◁∞ (via x⟶ x⟶y◁P) = via x⟶ (\x⟶y -> ◁⇒◁∞ (x⟶y◁P x⟶y))

bounded-is-finite : forall {x} -> x ◁ _↛ -> ¬ Infinite _⟶_ x
bounded-is-finite (directly x∈P) (x⟶y ◅∞ y⟶∞) = x∈P (, x⟶y)
bounded-is-finite (via _ x⟶y◁P)  (x⟶y ◅∞ y⟶∞) =
  bounded-is-finite (x⟶y◁P x⟶y) y⟶∞

------------------------------------------------------------------------
-- Some lemmas

-- Sanity check.

can-be-reached : forall {P x} ->
                 x ◁ P -> ∃ \y -> Star _⟶_ x y × y ∈ P
can-be-reached {x = x} (directly x∈P) = (x , ε , x∈P)
can-be-reached (via (y , x⟶y) x⟶◁P)
  with can-be-reached (x⟶◁P x⟶y)
... | (z , y⟶⋆z , z∈P) = (z , x⟶y ◅ y⟶⋆z , z∈P)

◁-trans : forall {x P Q} ->
          x ◁ P -> (forall {y} -> y ∈ P -> y ◁ Q) -> x ◁ Q
◁-trans (directly x∈P) P◁Q = P◁Q x∈P
◁-trans (via x⟶ x⟶y◁P) P◁Q = via x⟶ (\x⟶y -> ◁-trans (x⟶y◁P x⟶y) P◁Q)

◁∞-trans : forall {x P Q} ->
           x ◁∞ P -> (forall {y} -> y ∈ P -> y ◁∞ Q) -> x ◁∞ Q
◁∞-trans (directly x∈P) P◁Q ~ P◁Q x∈P
◁∞-trans (via x⟶ x⟶y◁P) P◁Q ~ via x⟶ (\x⟶y -> ◁∞-trans (x⟶y◁P x⟶y) P◁Q)

◁-map : forall {x P Q} -> P ⊆ Q -> x ◁ P -> x ◁ Q
◁-map P⊆Q (directly x∈P) = directly (P⊆Q _ x∈P)
◁-map P⊆Q (via x⟶ x⟶◁P)  = via x⟶ (\x⟶y -> ◁-map P⊆Q (x⟶◁P x⟶y))

◁∞-map : forall {x P Q} -> P ⊆ Q -> x ◁∞ P -> x ◁∞ Q
◁∞-map P⊆Q (directly x∈P) ~ directly (P⊆Q _ x∈P)
◁∞-map P⊆Q (via x⟶ x⟶◁∞P) ~ via x⟶ (\x⟶y -> ◁∞-map P⊆Q (x⟶◁∞P x⟶y))

bar∞-lemma : forall {x P y} ->
             (forall {z} -> z ∈ P -> z ↛) ->
             x ◁∞ P ->
             x ⟨ Star _⟶_ ⟩₁ y -> y ↛ -> y ∈ P
bar∞-lemma P↛ (directly x∈P)    ε            x↛ = x∈P
bar∞-lemma P↛ (via x⟶ _)        ε            x↛ = ⊥-elim (x↛ x⟶)
bar∞-lemma P↛ (directly x∈P)    (x⟶z ◅ z⟶⋆y) y↛ = ⊥-elim (P↛ x∈P (, x⟶z))
bar∞-lemma P↛ (via _ x⟶y◁P)     (x⟶z ◅ z⟶⋆y) y↛ =
  bar∞-lemma P↛ (x⟶y◁P x⟶z) z⟶⋆y y↛

bar-lemma : forall {x P y} ->
            (forall {z} -> z ∈ P -> z ↛) ->
            x ◁ P ->
            x ⟨ Star _⟶_ ⟩₁ y -> y ↛ -> y ∈ P
bar-lemma P↛ x◁P = bar∞-lemma P↛ (◁⇒◁∞ x◁P)

bounded-or-infinite : (forall x -> Dec (x ⟶)) -> forall x -> x ◁∞ _↛
bounded-or-infinite dec x with dec x
bounded-or-infinite dec x | no  x↛ ~ directly x↛
bounded-or-infinite dec x | yes x⟶ ~
  via x⟶ (\{y} _ -> bounded-or-infinite dec y)

------------------------------------------------------------------------
-- The code below can be used to handle some not obviously productive
-- definitions

mutual

  codata _◁∞′_ (x : S) (P : Pred S) : Set1 where
    directly : (x∈P : x ∈ P) -> x ◁∞′ P
    via      : (x⟶ : x ⟶) (x⟶y◁∞P : forall {y} -> x ⟶ y -> y ◁∞″ P) ->
               x ◁∞′ P

  data _◁∞″_ (x : S) (P : Pred S) : Set1 where
    ↓_        : (x◁∞P : x ◁∞′ P) -> x ◁∞″ P
    ◁∞′-trans : forall {Q}
                (x◁∞Q : x ◁∞″ Q)
                (Q◁∞P : forall {y} -> y ∈ Q -> y ◁∞″ P) ->
                x ◁∞″ P

-- The first constructor can be accessed in finite time.

∞″→∞′ : forall {x P} -> x ◁∞″ P -> x ◁∞′ P
∞″→∞′ (↓ x◁∞P)              = x◁∞P
∞″→∞′ (◁∞′-trans x◁∞Q Q◁∞P) with ∞″→∞′ x◁∞Q
∞″→∞′ (◁∞′-trans x◁∞Q Q◁∞P) | directly x∈P  = ∞″→∞′ (Q◁∞P x∈P)
∞″→∞′ (◁∞′-trans x◁∞Q Q◁∞P) | via x⟶ x⟶y◁∞P =
  via x⟶ (\x⟶y -> ◁∞′-trans (x⟶y◁∞P x⟶y) Q◁∞P)

-- _◁∞_ and _◁∞′_ are equivalent.

mutual

  ∞′→∞ : forall {x P} -> x ◁∞′ P -> x ◁∞ P
  ∞′→∞ (directly x∈P)  ~ directly x∈P
  ∞′→∞ (via x⟶ x⟶y◁∞P) ~ via x⟶ (\x⟶y -> ∞″→∞ (x⟶y◁∞P x⟶y))

  ∞″→∞ : forall {x P} -> x ◁∞″ P -> x ◁∞ P
  ∞″→∞ x◁∞P ~ ∞′→∞ (∞″→∞′ x◁∞P)

∞→∞′ : forall {x P} -> x ◁∞ P -> x ◁∞′ P
∞→∞′ (directly x∈P)  ~ directly x∈P
∞→∞′ (via x⟶ x⟶y◁∞P) ~ via x⟶ (\x⟶y -> ↓ ∞→∞′ (x⟶y◁∞P x⟶y))