------------------------------------------------------------------------
-- 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 = a} {r = 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 = r} ext =
  Π-closure (lower-extensionality r lzero ext) 1 λ _ 
  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  4 _[_]⋆_
infixr 5 _∷_

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 :
  {@0 A : Type a} {x : A}
  {@0 _<₁_ : A  A  Type r₁}
  {@0 _<₂_ : 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 :
  {@0 A : Type a}
  {@0 _<₁_ : A  A  Type r₁}
  {@0 _<₂_ : 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 :
  {@0 A : Type a} {@0 B : Type b} {f : A  B}
  {@0 _<_ : B  B  Type r} {@0 x : A} 
  Acc _<_ (f x)  Acc (_<_ on f) x
Acc-on {f = 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 :
  {@0 A : Type a} {@0 B : Type b} {f : A  B}
  {@0 _<_ : B  B  Type r} 
  Well-founded _<_  Well-founded (_<_ on f)
Well-founded-on {f = 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-⋆ :
  {@0 A : Type a} {@0 _<_ : A  A  Type r} {@0 x : A} 
  Acc _<_ x  Acc _[ _<_ ]⋆_ x
Acc-⋆ {_<_ = _<_} {x = 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-⋆ :
  {@0 A : Type a} {@0 _<_ : 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 = a} {r = r} { = } {_<_ = _<_} =
  generalise-ext?
    (record { to = to; from = from })
     ext  to-from ext , from-to ext)
  where
  to :  {@0 x}  Acc _<_ x  Acc  x y    (x < y)) x
  to (acc f) = acc λ y y<x  to (f y (lower y<x))

  from :  {@0 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 = r} { = } {_<_ = _<_} {k = 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 :
  {@0 A : Type a} {@0 _<_ : 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 :
  {@0 A : Type a} {@0 _<_ : 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 :
  {@0 A : Type a} {@0 _<_ : 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 _<_