------------------------------------------------------------------------
-- Infinite transition sequences
------------------------------------------------------------------------

module Infinite where

open import Relation.Nullary
open import Relation.Unary
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Data.Product
open import Data.Star hiding (return)
open import Data.Function
open import Data.Empty
open import Data.Nat
open import Data.Unit

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

infixr  _◅∞_

-- Infinite _⟶_ x means that there is an infinite transition sequence
-- starting at x.

codata Infinite {S : Set} (_⟶_ : Rel S) (x : S) : Set where
  _◅∞_ : ∀ {y} (x⟶y : x ⟶ y) (y⟶∞ : Infinite _⟶_ y) → Infinite _⟶_ x

-- A representation of infinite sequences as functions from natural
-- numbers.

Infinite-ℕ⟶ : {S : Set} → Rel S → Pred S
Infinite-ℕ⟶ {S} _⟶_ x =
  Σ (ℕ → S) λ step → x ≡ step  × (∀ n → step n ⟶ step (suc n))

-- A coinductive representation of sequences which either end in an
-- element satisfying a given predicate, or never end.

codata MaybeInfinite {S : Set} (_⟶_ : Rel S) (x : S) (P : Pred S) : Set
  where
  ε    : (x∈P : x ∈ P) → MaybeInfinite _⟶_ x P
  _◅∞_ : ∀ {y} (x⟶y : x ⟶ y) (y⟶⋆∞z : MaybeInfinite _⟶_ y P) →
         MaybeInfinite _⟶_ x P

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

∞⇒⋆∞ : ∀ {S} {_⟶_ : Rel S} {P x} →
       Infinite _⟶_ x → MaybeInfinite _⟶_ x P
∞⇒⋆∞ (x⟶y ◅∞ y⟶∞) ~ x⟶y ◅∞ ∞⇒⋆∞ y⟶∞

⋆∞⇒∞ : ∀ {S} {_⟶_ : Rel S} {P x} →
       MaybeInfinite _⟶_ x P →
       ∄ (λ y → Star _⟶_ x y × y ∈ P) →
       Infinite _⟶_ x
⋆∞⇒∞                   (ε x∈P)       x↛⋆P = ⊥-elim (x↛⋆P (_ , ε , x∈P))
⋆∞⇒∞ {S} {_⟶_} {P} {x} (x⟶y ◅∞ y⟶∞z) x↛⋆P ~ x⟶y ◅∞ ⋆∞⇒∞ y⟶∞z (helper x⟶y)
  where
  helper : ∀ {y} → x ⟶ y → ∄ λ z → Star _⟶_ y z × z ∈ P
  helper x⟶y (z , y⟶⋆z , z∈P) = x↛⋆P (z , x⟶y ◅ y⟶⋆z , z∈P)

⋆∞⇒∞′ : ∀ {S} {_⟶_ : Rel S} {P x} →
        MaybeInfinite _⟶_ x P → Empty P → Infinite _⟶_ x
⋆∞⇒∞′ ⟶⋆∞ P=∅ = ⋆∞⇒∞ ⟶⋆∞ (λ x⟶y∈P → P=∅ _ (proj₂ (proj₂ x⟶y∈P)))

∞⇒∞ℕ⟶ : ∀ {S} {_⟶_ : Rel S} {x} →
        Infinite _⟶_ x → Infinite-ℕ⟶ _⟶_ x
∞⇒∞ℕ⟶ {S} {_⟶_} x⟶∞ = (step x⟶∞ , ≡-refl , seq x⟶∞)
  where
  step : ∀ {x} → Infinite _⟶_ x → ℕ → S
  step {x} _            zero    = x
  step     (x⟶y ◅∞ y⟶∞) (suc n) = step y⟶∞ n

  seq : ∀ {x} (x⟶∞ : Infinite _⟶_ x) (n : ℕ) →
        step x⟶∞ n ⟶ step x⟶∞ (suc n)
  seq (x⟶y ◅∞ y⟶∞) zero    = x⟶y
  seq (x⟶y ◅∞ y⟶∞) (suc n) = seq y⟶∞ n

∞ℕ⟶⇒∞ : ∀ {S} {_⟶_ : Rel S} {x} →
        Infinite-ℕ⟶ _⟶_ x → Infinite _⟶_ x
∞ℕ⟶⇒∞ (step , ≡-refl , seq) ~
  seq  ◅∞ ∞ℕ⟶⇒∞ (step ∘ suc , ≡-refl , seq ∘ suc)

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

map∞ : ∀ {S₁ S₂} {R₁ : Rel S₁} {R₂ : Rel S₂}
       (F : S₁ → S₂) → R₁ =[ F ]⇒ R₂ →
       ∀ {x} → Infinite R₁ x → Infinite R₂ (F x)
map∞ F f (x⟶y ◅∞ y⟶∞) ~ f x⟶y ◅∞ map∞ F f y⟶∞

map-append⋆∞ :
  ∀ {S₁ S₂} {R₁ : Rel S₁} {R₂ : Rel S₂}
            {P₁ : Pred S₁} {P₂ : Pred S₂}
  (F : S₁ → S₂) → R₁ =[ F ]⇒ R₂ →
  (∀ {x} → x ∈ P₁ → MaybeInfinite R₂ (F x) P₂) →
  ∀ {x} → MaybeInfinite R₁ x P₁ → MaybeInfinite R₂ (F x) P₂
map-append⋆∞ F f g (ε x∈P)      = g x∈P
map-append⋆∞ F f g (x⟶y ◅∞ y⟶∞) ~ f x⟶y ◅∞ map-append⋆∞ F f g y⟶∞

map⋆∞ : ∀ {S₁ S₂} {R₁ : Rel S₁} {R₂ : Rel S₂}
                  {P₁ : Pred S₁} {P₂ : Pred S₂}
        (F : S₁ → S₂) →
        R₁ =[ F ]⇒ R₂ →
        (∀ {x} → x ∈ P₁ → F x ∈ P₂) →
        ∀ {x} → MaybeInfinite R₁ x P₁ → MaybeInfinite R₂ (F x) P₂
map⋆∞ F f g x⟶∞ = map-append⋆∞ F f (λ x∈P₁ → ε (g x∈P₁)) x⟶∞

private
 module Dummy {S} {_⟶_ : Rel S} where

  infix  _loops

  _loops : ∀ {x} → x ⟶ x → Infinite _⟶_ x
  x⟶x loops ~ x⟶x ◅∞ x⟶x loops

  append⋆∞ : ∀ {P Q x} → MaybeInfinite _⟶_ x P →
             (∀ {y} → y ∈ P → MaybeInfinite _⟶_ y Q) →
             MaybeInfinite _⟶_ x Q
  append⋆∞ x⟶∞ hyp = map-append⋆∞ id id hyp x⟶∞

  infixr  _◅◅⋆∞_

  _◅◅⋆∞_ : ∀ {P x y} → Star _⟶_ x y → MaybeInfinite _⟶_ y P →
           MaybeInfinite _⟶_ x P
  ε            ◅◅⋆∞ z⟶∞ = z⟶∞
  (x⟶y ◅ y⟶⋆z) ◅◅⋆∞ z⟶∞ = x⟶y ◅∞ y⟶⋆z ◅◅⋆∞ z⟶∞

  unbounded-loops : (∀ x → Dec (∃ λ y → x ⟶ y)) →
                    ∀ x → ∄ (λ y → Star _⟶_ x y × ∄ λ z → y ⟶ z) →
                    Infinite _⟶_ x
  unbounded-loops _⟶? x hyp with x ⟶?
  unbounded-loops _⟶? x hyp | no x↛         = ⊥-elim (hyp (x , ε , x↛))
  unbounded-loops _⟶? x hyp | yes (u , x⟶u) ~
    x⟶u ◅∞ unbounded-loops _⟶? u hyp'
    where
    hyp' : ∄ (λ y → Star _⟶_ u y × ∄ λ z → y ⟶ z)
    hyp' (y , u⟶⋆y , y↛) = hyp (y , x⟶u ◅ u⟶⋆y , y↛)

open Dummy public

------------------------------------------------------------------------
-- An encoding of guarded definitions for Infinite

-- ʳ stands for right-hand side.

-- This idea comes from Hancock and Setzer (Interactive Programs in
-- Dependent Type Theory). Conor McBride pointed me to their approach,
-- and the general idea of this formulation. I have taken their ideas
-- to a more dependently typed setting, made it possible to map over
-- the resulting values without having to manipulate the seed, and
-- made the return constructor superfluous by switching to a
-- coinductive type for right-hand sides.

data Guardedness : Set where
  guarded   : Guardedness
  unguarded : Guardedness

codata Infiniteʳ {I S : Set} (R : I → Rel S) (P : I → Pred S) :
                 Guardedness → I → S → Set where
  _◅∞_   : ∀ {g i x y}
           (x⟶y : R i x y) (y⟶∞ : Infiniteʳ R P guarded i y) →
           Infiniteʳ R P g i x
  grec   : ∀ {i j} (F : S → S) (f : R i =[ F ]⇒ R j)
           {x} (p : P i x) → Infiniteʳ R P guarded j (F x)

return : ∀ {I S R g i x} {P : I → Pred S} →
         Infinite (R i) x → Infiniteʳ R P g i x
return (x⟶y ◅∞ y⟶∞) ~ x⟶y ◅∞ return y⟶∞

rec : ∀ {I S R i x} {P : I → Pred S} →
      P i x → Infiniteʳ R P guarded i x
rec = grec id id

map∞ʳ : ∀ {I S R P g x} {i j : I}
        (F : S → S) → R i =[ F ]⇒ R j →
        Infiniteʳ R P g i x → Infiniteʳ R P g j (F x)
map∞ʳ F f (x⟶y ◅∞ y⟶∞)   ~ f x⟶y ◅∞ map∞ʳ F f y⟶∞
map∞ʳ F f (grec F' f' p) = grec (F ∘ F') (f ∘ f') p

Stepper : {I S : Set} → (I → Rel S) → (I → Pred S) → Guardedness → Set
Stepper R P g = ∀ {i x} → P i x → Infiniteʳ R P g i x

unfold1 : ∀ {I S R g i x} {P : I → Pred S} →
          Stepper R P g →
          Infiniteʳ R P guarded i x →
          Infiniteʳ R P g       i x
unfold1 step (x⟶y ◅∞ y⟶∞) = x⟶y ◅∞ y⟶∞
unfold1 step (grec F f p) = map∞ʳ F f (step p)

produce : ∀ {I S R i x} {P : I → Pred S} →
          Stepper R P unguarded →
          Infiniteʳ R P unguarded i x →
          Infinite (R i) x
produce step (x⟶y ◅∞ y⟶∞) ~ x⟶y ◅∞ produce step (unfold1 step y⟶∞)

unfold : ∀ {I S R i x} {P : I → Pred S} →
         Stepper R P unguarded →
         P i x → Infinite (R i) x
unfold step p = produce step (step p)

lift : ∀ {I S R i j x y g} →
       ({P : I → Pred S} → Infiniteʳ R P g         i x →
                           Infiniteʳ R P unguarded j y) →
       (Infinite (R i) x → Infinite (R j) y)
lift f ⟶∞ = produce {P = λ _ _ → ⊥} ⊥-elim (f (return ⟶∞))

weaken : ∀ {I S R i x g} {P : I → Pred S} →
         Infiniteʳ R P g       i x →
         Infiniteʳ R P guarded i x
weaken (x⟶y ◅∞ y⟶∞) = x⟶y ◅∞ y⟶∞
weaken (grec F f p) = grec F f p

------------------------------------------------------------------------
-- More lemmas

infixr  _◅◅∞ʳ_

_◅◅∞ʳ_ : ∀ {I S R i x y g} {P : I → Pred S} →
         Star (R i) x y → Infiniteʳ R P g i y →
         Infiniteʳ R P g i x
ε        ◅◅∞ʳ ⟶∞ = ⟶∞
(x ◅ xs) ◅◅∞ʳ ⟶∞ = x ◅∞ weaken (xs ◅◅∞ʳ ⟶∞)

infixr  _◅◅∞_

_◅◅∞_ : ∀ {S} {R : Rel S} {x y} →
        Star R x y → Infinite R y → Infinite R x
_◅◅∞_ {R = R} ⟶⋆ ⟶∞ =
  lift {I = ⊤} {R = λ _ → R} (λ ⟶∞ → ⟶⋆ ◅◅∞ʳ ⟶∞) ⟶∞

------------------------------------------------------------------------
-- Another way to handle not obviously productive definitions

-- More of a hack, perhaps, but easier to use.

infixr  _◅◅∞′_
infix   ↓_

mutual

  codata Infinite′ {S : Set} (R : Rel S) (x : S) : Set1 where
    _◅∞_  : ∀ {y} (x⟶y  : R x y) (y⟶∞ : Infinite″ R y) →
            Infinite′ R x

  data Infinite″ {S : Set} (R : Rel S) : S → Set1 where
    ↓_     : ∀ {x} (x⟶∞ : Infinite′ R x) → Infinite″ R x
    _◅◅∞′_ : ∀ {x y} (x⟶⋆y : Star R x y) (y⟶∞ : Infinite″ R y) →
             Infinite″ R x
    map∞′  : ∀ {S' x} {R' : Rel S'}
             (F : S' → S) (f : R' =[ F ]⇒ R)
             (x⟶∞ : Infinite″ R' x) → Infinite″ R (F x)

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

∞″→∞′ : ∀ {S x} {R : Rel S} → Infinite″ R x → Infinite′ R x
∞″→∞′ (↓ x⟶∞)                 = x⟶∞
∞″→∞′ (ε            ◅◅∞′ x⟶∞) = ∞″→∞′ x⟶∞
∞″→∞′ ((x⟶y ◅ y⟶⋆z) ◅◅∞′ z⟶∞) = x⟶y ◅∞ y⟶⋆z ◅◅∞′ z⟶∞
∞″→∞′ (map∞′ F f x⟶∞)         with ∞″→∞′ x⟶∞
∞″→∞′ (map∞′ F f x⟶∞)         | x⟶y ◅∞ y⟶∞ = f x⟶y ◅∞ map∞′ F f y⟶∞

-- Infinite and Infinite′ are equivalent.

mutual

  ∞′→∞ : ∀ {S x} {R : Rel S} → Infinite′ R x → Infinite R x
  ∞′→∞ (x⟶y ◅∞ y⟶∞) ~ x⟶y ◅∞ ∞″→∞ y⟶∞

  ∞″→∞ : ∀ {S x} {R : Rel S} → Infinite″ R x → Infinite R x
  ∞″→∞ x⟶∞ = ∞′→∞ (∞″→∞′ x⟶∞)

∞→∞′ : ∀ {S x} {R : Rel S} → Infinite R x → Infinite′ R x
∞→∞′ (x⟶y ◅∞ y⟶∞) ~ x⟶y ◅∞ (↓ ∞→∞′ y⟶∞)

------------------------------------------------------------------------
-- The same trick applied to MaybeInfinite

mutual

  infixr  _⇓_
  infixr  _◅⟨_⟩_
  infix   _∈⟨_⟩
  infix   _∶⟨_⟩

  codata MaybeInfinite′ {S : Set} (R : Rel S) : S → Pred S → Set1 where
    _∈⟨_⟩  : ∀ x {P} (x∈P : x ∈ P) → MaybeInfinite′ R x P
    _◅⟨_⟩_ : ∀ x {y P} (x⟶y  : R x y) (y⟶∞ : MaybeInfinite″ R y P) →
             MaybeInfinite′ R x P

  data MaybeInfinite″ {S : Set} (R : Rel S) : S → Pred S → Set1 where
    _⇓_ : ∀ {x P} (dummy : ⊤)
          (x⟶∞ : MaybeInfinite′ R x P) → MaybeInfinite″ R x P
    map-append⋆∞′ :
      ∀ {S′} {R′ : Rel S′} {P′ P}
      (F : S′ → S) → R′ =[ F ]⇒ R →
      (∀ {x} → x ∈ P′ → MaybeInfinite″ R (F x) P) →
      ∀ {x} → MaybeInfinite″ R′ x P′ → MaybeInfinite″ R (F x) P
    -- _∶⟨_⟩ is included only to make the code more informative.
    _∶⟨_⟩ : ∀ x {P} (x⟶∞ : MaybeInfinite″ R x P) → MaybeInfinite″ R x P

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

⋆∞″→⋆∞′ : ∀ {S x P} {R : Rel S} →
          MaybeInfinite″ R x P → MaybeInfinite′ R x P
⋆∞″→⋆∞′ (_ ⇓ x⟶∞)                 = x⟶∞
⋆∞″→⋆∞′ (map-append⋆∞′ F f g x⟶∞) with ⋆∞″→⋆∞′ x⟶∞
⋆∞″→⋆∞′ (map-append⋆∞′ F f g x⟶∞) | x ∈⟨ x∈P ⟩     = ⋆∞″→⋆∞′ (g x∈P)
⋆∞″→⋆∞′ (map-append⋆∞′ F f g x⟶∞) | x ◅⟨ x⟶y ⟩ y⟶∞ =
  F x ◅⟨ f x⟶y ⟩ map-append⋆∞′ F f g y⟶∞
⋆∞″→⋆∞′ (x ∶⟨ x⟶∞ ⟩)              = ⋆∞″→⋆∞′ x⟶∞

-- MaybeInfinite and MaybeInfinite′ are equivalent.

mutual

  ⋆∞′→⋆∞ : ∀ {S x P} {R : Rel S} →
           MaybeInfinite′ R x P → MaybeInfinite R x P
  ⋆∞′→⋆∞ (x ∈⟨ x∈P ⟩)     = ε x∈P
  ⋆∞′→⋆∞ (_ ◅⟨ x⟶y ⟩ y⟶∞) ~ x⟶y ◅∞ ⋆∞″→⋆∞ y⟶∞

  ⋆∞″→⋆∞ : ∀ {S x P} {R : Rel S} →
           MaybeInfinite″ R x P → MaybeInfinite R x P
  ⋆∞″→⋆∞ x⟶∞ = ⋆∞′→⋆∞ (⋆∞″→⋆∞′ x⟶∞)

⋆∞→⋆∞′ : ∀ {S x P} {R : Rel S} →
         MaybeInfinite R x P → MaybeInfinite′ R x P
⋆∞→⋆∞′ (ε x∈P)      = _ ∈⟨ x∈P ⟩
⋆∞→⋆∞′ (x⟶y ◅∞ y⟶∞) ~ _ ◅⟨ x⟶y ⟩ _ ⇓ ⋆∞→⋆∞′ y⟶∞