------------------------------------------------------------------------ -- 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))