------------------------------------------------------------------------
-- 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.
  now : (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.
  later : (x⟶ : x ⟶) (x⟶y◁P : ∀ {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
  now   : (x∈P : x ∈ P) → x ◁∞ P
  later : (x⟶ : x ⟶) (x⟶y◁∞P : ∀ {y} → x ⟶ y → y ◁∞ P) → x ◁∞ P

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

◁⇒◁∞ : ∀ {x P} → x ◁ P → x ◁∞ P
◁⇒◁∞ (now x∈P)        = now x∈P
◁⇒◁∞ (later x⟶ x⟶y◁P) = later x⟶ (λ x⟶y → ◁⇒◁∞ (x⟶y◁P x⟶y))

bounded-is-finite : ∀ {x} → x ◁ _↛ → ¬ Infinite _⟶_ x
bounded-is-finite (now x∈P)       (x⟶y ◅∞ y⟶∞) = x∈P (, x⟶y)
bounded-is-finite (later _ x⟶y◁P) (x⟶y ◅∞ y⟶∞) =
  bounded-is-finite (x⟶y◁P x⟶y) y⟶∞

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

-- Sanity check.

can-be-reached : ∀ {P x} → x ◁ P → ∃ λ y → Star _⟶_ x y × y ∈ P
can-be-reached {x = x} (now x∈P) = (x , ε , x∈P)
can-be-reached (later (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 : ∀ {x P Q} → x ◁ P → (∀ {y} → y ∈ P → y ◁ Q) → x ◁ Q
◁-trans (now x∈P)        P◁Q = P◁Q x∈P
◁-trans (later x⟶ x⟶y◁P) P◁Q = later x⟶ (λ x⟶y → ◁-trans (x⟶y◁P x⟶y) P◁Q)

◁∞-trans : ∀ {x P Q} → x ◁∞ P → (∀ {y} → y ∈ P → y ◁∞ Q) → x ◁∞ Q
◁∞-trans (now x∈P)        P◁Q = P◁Q x∈P
◁∞-trans (later x⟶ x⟶y◁P) P◁Q ~ later x⟶ (λ x⟶y → ◁∞-trans (x⟶y◁P x⟶y) P◁Q)

◁-map : ∀ {x P Q} → P ⊆ Q → x ◁ P → x ◁ Q
◁-map P⊆Q (now x∈P)       = now (P⊆Q _ x∈P)
◁-map P⊆Q (later x⟶ x⟶◁P) = later x⟶ (λ x⟶y → ◁-map P⊆Q (x⟶◁P x⟶y))

◁∞-map : ∀ {x P Q} → P ⊆ Q → x ◁∞ P → x ◁∞ Q
◁∞-map P⊆Q (now x∈P)        = now (P⊆Q _ x∈P)
◁∞-map P⊆Q (later x⟶ x⟶◁∞P) ~ later x⟶ (λ x⟶y → ◁∞-map P⊆Q (x⟶◁∞P x⟶y))

bar∞-lemma : ∀ {x P y} →
             (∀ {z} → z ∈ P → z ↛) →
             x ◁∞ P →
             x ⟨ Star _⟶_ ⟩₁ y → y ↛ → y ∈ P
bar∞-lemma P↛ (now x∈P)       ε            x↛ = x∈P
bar∞-lemma P↛ (later x⟶ _)    ε            x↛ = ⊥-elim (x↛ x⟶)
bar∞-lemma P↛ (now x∈P)       (x⟶z ◅ z⟶⋆y) y↛ = ⊥-elim (P↛ x∈P (, x⟶z))
bar∞-lemma P↛ (later _ x⟶y◁P) (x⟶z ◅ z⟶⋆y) y↛ =
  bar∞-lemma P↛ (x⟶y◁P x⟶z) z⟶⋆y y↛

bar-lemma : ∀ {x P y} →
            (∀ {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 : (∀ x → Dec (x ⟶)) → ∀ x → x ◁∞ _↛
bounded-or-infinite dec x with dec x
bounded-or-infinite dec x | no  x↛ = now x↛
bounded-or-infinite dec x | yes x⟶ ~
  later 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
    now   : (x∈P : x ∈ P) → x ◁∞′ P
    later : (x⟶ : x ⟶) (x⟶y◁∞P : ∀ {y} → x ⟶ y → y ◁∞″ P) → x ◁∞′ P

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

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

∞″→∞′ : ∀ {x P} → x ◁∞″ P → x ◁∞′ P
∞″→∞′ (↓ x◁∞P)              = x◁∞P
∞″→∞′ (◁∞′-trans x◁∞Q Q◁∞P) with ∞″→∞′ x◁∞Q
∞″→∞′ (◁∞′-trans x◁∞Q Q◁∞P) | now x∈P         = ∞″→∞′ (Q◁∞P x∈P)
∞″→∞′ (◁∞′-trans x◁∞Q Q◁∞P) | later x⟶ x⟶y◁∞P =
  later x⟶ (λ x⟶y → ◁∞′-trans (x⟶y◁∞P x⟶y) Q◁∞P)

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

mutual

  ∞′→∞ : ∀ {x P} → x ◁∞′ P → x ◁∞ P
  ∞′→∞ (now x∈P)         = now x∈P
  ∞′→∞ (later x⟶ x⟶y◁∞P) ~ later x⟶ (λ x⟶y → ∞″→∞ (x⟶y◁∞P x⟶y))

  ∞″→∞ : ∀ {x P} → x ◁∞″ P → x ◁∞ P
  ∞″→∞ x◁∞P = ∞′→∞ (∞″→∞′ x◁∞P)

∞→∞′ : ∀ {x P} → x ◁∞ P → x ◁∞′ P
∞→∞′ (now x∈P)         = now x∈P
∞→∞′ (later x⟶ x⟶y◁∞P) ~ later x⟶ (λ x⟶y → ↓ ∞→∞′ (x⟶y◁∞P x⟶y))