------------------------------------------------------------------------
-- The accessibility predicate
------------------------------------------------------------------------

-- Partly based on "Constructing Recursion Operators in Intuitionistic
-- Type Theory" by Lawrence C Paulson.

{-# OPTIONS --cubical-compatible --safe #-}

open import Equality

module Accessibility {e⁺} (eq : ∀ {a p} → Equality-with-J a p e⁺) where

open Derived-definitions-and-properties eq

open import Prelude

open import Extensionality eq
open import Function-universe eq hiding (id; _∘_)
open import H-level.Closure eq
import Nat eq as Nat
open import Preimage eq using (_⁻¹_)

private
  variable
    a b ℓ p q r r₁ r₂ : Level
    A                 : Type a
    P                 : A → Type p
    x z               : A

------------------------------------------------------------------------
-- Accessibility and well-founded relations

-- The accessibility predicate.
--
-- The element x is accessible with respect to _<_ if every element
-- that is below x is accessible.

data Acc {A : Type a} (_<_ : A → A → Type r) (x : A) :
         Type (a ⊔ r) where
  acc : (∀ y → y < x → Acc _<_ y) → Acc _<_ x

-- A relation is well-founded if every element is accessible.

Well-founded : {A : Type a} → (A → A → Type r) → Type (a ⊔ r)
Well-founded _<_ = ∀ x → Acc _<_ x

-- The accessibility predicate is propositional (assuming
-- extensionality).

Acc-propositional :
  {A : Type a} {_<_ : A → A → Type r} {x : A} →
  Extensionality (a ⊔ r) (a ⊔ r) →
  Is-proposition (Acc _<_ x)
Acc-propositional {a} {r} ext (acc f) (acc g) =
  cong acc $
  apply-ext (lower-extensionality r lzero ext) λ y →
  apply-ext (lower-extensionality a lzero ext) λ y<x →
  Acc-propositional ext (f y y<x) (g y y<x)

-- Well-founded is pointwise propositional (assuming extensionality).

Well-founded-propositional :
  {A : Type a} {_<_ : A → A → Type r} →
  Extensionality (a ⊔ r) (a ⊔ r) →
  Is-proposition (Well-founded _<_)
Well-founded-propositional {r} ext =
  Π-closure (lower-extensionality r lzero ext)  λ _ →
  Acc-propositional ext

------------------------------------------------------------------------
-- Specific examples of well-founded relations

-- The always undefined relation is well-founded.

Well-founded-⊥ : Well-founded (λ (_ _ : A) → ⊥ {ℓ = ℓ})
Well-founded-⊥ _ = acc λ _ ()

-- The relation Nat._<_ is well-founded.

Well-founded-ℕ : Well-founded Nat._<_
Well-founded-ℕ m = acc (helper m)
  where
  helper : ∀ m n → n Nat.< m → Acc Nat._<_ n
  helper zero    n (Nat.≤-refl′ eq)   = ⊥-elim (Nat.0≢+ (sym eq))
  helper zero    n (Nat.≤-step′ _ eq) = ⊥-elim (Nat.0≢+ (sym eq))
  helper (suc m) n (Nat.≤-refl′ eq)   =
    subst (Acc Nat._<_) (sym (Nat.cancel-suc eq)) (Well-founded-ℕ m)
  helper (suc m) n (Nat.≤-step′ p eq) =
    helper m n (subst (n Nat.<_) (Nat.cancel-suc eq) p)

-- The value x is below sup y f if x is equal to f z for some z.

_<W_ :
  {A : Type a} {P : A → Type p} →
  W A P → W A P → Type (a ⊔ p)
x <W sup _ f = f ⁻¹ x

-- The relation _<W_ is well-founded.

Well-founded-W : Well-founded {A = W A P} _<W_
Well-founded-W (sup _ f) = acc λ where
  (sup x g) (y , eq) → subst (Acc _) eq (Well-founded-W (f y))

------------------------------------------------------------------------
-- Transitive closure

-- The transitive closure of a relation.

infix   _[_]⋆_
infixr  _∷_

data _[_]⋆_
       {A : Type a}
       (x : A)
       (_<_ : A → A → Type r)
       (y : A) :
       Type (a ⊔ r) where
  [_] : x < y → x [ _<_ ]⋆ y
  _∷_ : x < z → z [ _<_ ]⋆ y → x [ _<_ ]⋆ y

-- A relation contains a cycle if its transitive closure contains a
-- loop.

Cycle : {A : Type a} → (A → A → Type r) → Type (a ⊔ r)
Cycle _<_ = ∃ λ x → x [ _<_ ]⋆ x

------------------------------------------------------------------------
-- Lemmas that can be used to prove that relations are well-founded,
-- or that values are accessible

-- If _<₂_ is contained in _<₁_, then Acc _<₁_ x implies Acc _<₂_ x.

Acc-map :
  {@ A : Type a} {x : A}
  {@ _<₁_ : A → A → Type r₁}
  {@ _<₂_ : A → A → Type r₂} →
  (∀ {x y} → x <₂ y → x <₁ y) →
  Acc _<₁_ x → Acc _<₂_ x
Acc-map f (acc g) = acc λ y y<₂x → Acc-map f (g y (f y<₂x))

-- If _<₂_ is contained in _<₁_, then Well-founded _<₁_ implies
-- Well-founded _<₂_.

Well-founded-map :
  {@ A : Type a}
  {@ _<₁_ : A → A → Type r₁}
  {@ _<₂_ : A → A → Type r₂} →
  (∀ {x y} → x <₂ y → x <₁ y) →
  Well-founded _<₁_ → Well-founded _<₂_
Well-founded-map f wf x = Acc-map f (wf x)

-- If f x is accessible with respect to _<_, then x is accessible with
-- respect to _<_ on f.

Acc-on :
  {@ A : Type a} {@ B : Type b} {f : A → B}
  {@ _<_ : B → B → Type r} {@ x : A} →
  Acc _<_ (f x) → Acc (_<_ on f) x
Acc-on {f} (acc g) = acc λ y fy<fx → Acc-on (g (f y) fy<fx)

-- If _<_ is well-founded, then _<_ on f is well-founded.

Well-founded-on :
  {@ A : Type a} {@ B : Type b} {f : A → B}
  {@ _<_ : B → B → Type r} →
  Well-founded _<_ → Well-founded (_<_ on f)
Well-founded-on {f} wf x = Acc-on (wf (f x))

-- If x is accessible with respect to _<_, then x is also accessible
-- with respect to the transitive closure of _<_.

Acc-⋆ :
  {@ A : Type a} {@ _<_ : A → A → Type r} {@ x : A} →
  Acc _<_ x → Acc _[ _<_ ]⋆_ x
Acc-⋆ {_<_} {x} (acc f) = acc helper
  where
  helper : ∀ y → y [ _<_ ]⋆ x → Acc _[ _<_ ]⋆_ y
  helper y [ y<x ]      = Acc-⋆ (f y y<x)
  helper y (y<z ∷ z<⋆x) = case helper _ z<⋆x of λ where
    (acc f) → f y [ y<z ]

-- If a relation is well-founded, then its transitive closure is also
-- well-founded.

Well-founded-⋆ :
  {@ A : Type a} {@ _<_ : A → A → Type r} →
  Well-founded _<_ →
  Well-founded _[ _<_ ]⋆_
Well-founded-⋆ wf x = Acc-⋆ (wf x)

-- Acc _<_ x is equivalent to Acc (λ x y → ↑ ℓ (x < y)) x (assuming
-- extensionality).

Acc-↑ :
  ∀ {A : Type a} {_<_ : A → A → Type r} {x} →
  Acc _<_ x ↝[ a ⊔ ℓ ⊔ r ∣ a ⊔ ℓ ⊔ r ]
  Acc (λ x y → ↑ ℓ (x < y)) x
Acc-↑ {a} {r} {ℓ} {_<_} =
  generalise-ext?
    (record { to = to; from = from })
    (λ ext → to-from ext , from-to ext)
  where
  to : ∀ {@ x} → Acc _<_ x → Acc (λ x y → ↑ ℓ (x < y)) x
  to (acc f) = acc λ y y<x → to (f y (lower y<x))

  from : ∀ {@ x} → Acc (λ x y → ↑ ℓ (x < y)) x → Acc _<_ x
  from (acc f) = acc λ y y<x → from (f y (lift y<x))

  module _ (ext : Extensionality (a ⊔ ℓ ⊔ r) (a ⊔ ℓ ⊔ r)) where
    to-from : (p : Acc (λ x y → ↑ ℓ (x < y)) x) → to (from p) ≡ p
    to-from (acc f) =
      cong acc $
      apply-ext (lower-extensionality (ℓ ⊔ r) lzero ext) λ y   →
      apply-ext (lower-extensionality a       lzero ext) λ y<x →
      to-from (f y y<x)

    from-to : (p : Acc _<_ x) → from (to p) ≡ p
    from-to (acc f) =
      cong acc $
      apply-ext (lower-extensionality (ℓ ⊔ r) ℓ ext) λ y   →
      apply-ext (lower-extensionality (a ⊔ ℓ) ℓ ext) λ y<x →
      from-to (f y y<x)

-- Well-founded _<_ is equivalent to
-- Well-founded (λ x y → ↑ ℓ (x < y)) (assuming extensionality).

Well-founded-↑ :
  ∀ {A : Type a} {_<_ : A → A → Type r} →
  Well-founded _<_ ↝[ a ⊔ ℓ ⊔ r ∣ a ⊔ ℓ ⊔ r ]
  Well-founded (λ x y → ↑ ℓ (x < y))
Well-founded-↑ {r} {ℓ} {_<_} {k} ext =
  (∀ x → Acc _<_ x)                    ↝⟨ (∀-cong (lower-extensionality? k (ℓ ⊔ r) lzero ext) λ _ → Acc-↑ ext) ⟩□
  (∀ x → Acc (λ x y → ↑ ℓ (x < y)) x)  □

------------------------------------------------------------------------
-- Some negative results

-- If x < x, then x is not accessible with respect to _<_.

<→¬-Acc :
  {@ A : Type a} {@ _<_ : A → A → Type r} {x : A} →
  x < x → ¬ Acc _<_ x
<→¬-Acc x<x (acc f) = <→¬-Acc x<x (f _ x<x)

-- If x < x, then _<_ is not well-founded.

<→¬-Well-founded :
  {@ A : Type a} {@ _<_ : A → A → Type r} {x : A} →
  x < x → ¬ Well-founded _<_
<→¬-Well-founded x<x wf = <→¬-Acc x<x (wf _)

-- If a relation contains a cycle, then it is not well-founded.

Cycle→¬-Well-founded :
  {@ A : Type a} {@ _<_ : A → A → Type r} →
  Cycle _<_ → ¬ Well-founded _<_
Cycle→¬-Well-founded {_<_} (x , x<⋆x) =
                             $⟨ x<⋆x ⟩
  x [ _<_ ]⋆ x               →⟨ <→¬-Well-founded ⟩
  ¬ Well-founded _[ _<_ ]⋆_  →⟨ _∘ (λ wf → Well-founded-⋆ wf) ⟩□
  ¬ Well-founded _<_         □