------------------------------------------------------------------------
-- The Agda standard library
--
-- Well-founded induction
------------------------------------------------------------------------

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

module Induction.WellFounded where

open import Data.Product.Base using (Σ; _,_; proj₁)
open import Function.Base using (_on_)
open import Induction
open import Level using (Level; _⊔_)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.Definitions
  using (Symmetric; _Respectsʳ_; _Respects_)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
open import Relation.Unary

private
  variable
    a b  ℓ₁ ℓ₂ r : Level
    A : Set a
    B : Set b

------------------------------------------------------------------------
-- Definitions

-- When using well-founded recursion you can recurse arbitrarily, as
-- long as the arguments become smaller, and "smaller" is
-- well-founded.

WfRec : Rel A r   {}  RecStruct A  _
WfRec _<_ P x =  y  y < x  P y

-- The accessibility predicate: x is accessible if everything which is
-- smaller than x is also accessible (inductively).

data Acc {A : Set a} (_<_ : Rel A ) (x : A) : Set (a  ) where
  acc : (rs : WfRec _<_ (Acc _<_) x)  Acc _<_ x

-- The accessibility predicate encodes what it means to be
-- well-founded; if all elements are accessible, then _<_ is
-- well-founded.

WellFounded : Rel A   Set _
WellFounded _<_ =  x  Acc _<_ x

------------------------------------------------------------------------
-- Basic properties

acc-inverse :  {_<_ : Rel A } {x : A} (q : Acc _<_ x) 
              (y : A)  y < x  Acc _<_ y
acc-inverse (acc rs) y y<x = rs y y<x

Acc-resp-≈ : {_≈_ : Rel A ℓ₁} {_<_ : Rel A ℓ₂}  Symmetric _≈_ 
             _<_ Respectsʳ _≈_  (Acc _<_) Respects _≈_
Acc-resp-≈ sym respʳ x≈y (acc rec) =
  acc  z z<y  rec z (respʳ (sym x≈y) z<y))

------------------------------------------------------------------------
-- Well-founded induction for the subset of accessible elements:

module Some {_<_ : Rel A r} {} where

  wfRecBuilder : SubsetRecursorBuilder (Acc _<_) (WfRec _<_ { = })
  wfRecBuilder P f x (acc rs) = λ y y<x 
    f y (wfRecBuilder P f y (rs y y<x))

  wfRec : SubsetRecursor (Acc _<_) (WfRec _<_)
  wfRec = subsetBuild wfRecBuilder

  unfold-wfRec : (P : Pred A ) (f : WfRec _<_ P ⊆′ P) {x : A} (q : Acc _<_ x) 
                 wfRec P f x q  f x  y y<x  wfRec P f y (acc-inverse q y y<x))
  unfold-wfRec P f (acc rs) = refl


------------------------------------------------------------------------
-- Well-founded induction for all elements, assuming they are all
-- accessible:

module All {_<_ : Rel A r} (wf : WellFounded _<_)  where

  wfRecBuilder : RecursorBuilder (WfRec _<_ { = })
  wfRecBuilder P f x = Some.wfRecBuilder P f x (wf x)

  wfRec : Recursor (WfRec _<_)
  wfRec = build wfRecBuilder

  wfRec-builder = wfRecBuilder

module FixPoint
  {_<_ : Rel A r} (wf : WellFounded _<_)
  (P : Pred A ) (f : WfRec _<_ P ⊆′ P)
  (f-ext : (x : A) {IH IH′ : WfRec _<_ P x}  (∀ {y} y<x  IH y y<x  IH′ y y<x)  f x IH  f x IH′)
  where

  some-wfRec-irrelevant :  x  (q q′ : Acc _<_ x)  Some.wfRec P f x q  Some.wfRec P f x q′
  some-wfRec-irrelevant = All.wfRec wf _
                                    x  (q q′ : Acc _<_ x)  Some.wfRec P f x q  Some.wfRec P f x q′)
                                    { x IH (acc rs) (acc rs′)  f-ext x  y<x  IH _ y<x (rs _ y<x) (rs′ _ y<x)) })

  open All wf 
  wfRecBuilder-wfRec :  {x y} y<x  wfRecBuilder P f x y y<x  wfRec P f y
  wfRecBuilder-wfRec {x} {y} y<x with wf x
  ... | acc rs = some-wfRec-irrelevant y (rs y y<x) (wf y)

  unfold-wfRec :  {x}  wfRec P f x  f x  y _  wfRec P f y)
  unfold-wfRec {x} = f-ext x wfRecBuilder-wfRec


------------------------------------------------------------------------
-- It might be useful to establish proofs of Acc or Well-founded using
-- combinators such as the ones below (see, for instance,
-- "Constructing Recursion Operators in Intuitionistic Type Theory" by
-- Lawrence C Paulson).

module Subrelation {_<₁_ : Rel A ℓ₁} {_<₂_ : Rel A ℓ₂}
                   (<₁⇒<₂ :  {x y}  x <₁ y  x <₂ y) where

  accessible : Acc _<₂_  Acc _<₁_
  accessible (acc rs) = acc  y y<x  accessible (rs y (<₁⇒<₂ y<x)))

  wellFounded : WellFounded _<₂_  WellFounded _<₁_
  wellFounded wf = λ x  accessible (wf x)


-- DEPRECATED in v1.4.
-- Please use proofs in `Relation.Binary.Construct.On` instead.
module InverseImage {_<_ : Rel B } (f : A  B) where

  accessible :  {x}  Acc _<_ (f x)  Acc (_<_ on f) x
  accessible (acc rs) = acc  y fy<fx  accessible (rs (f y) fy<fx))

  wellFounded : WellFounded _<_  WellFounded (_<_ on f)
  wellFounded wf = λ x  accessible (wf (f x))

  well-founded = wellFounded
  {-# WARNING_ON_USAGE accessible
  "Warning: accessible was deprecated in v1.4.
\ \Please use accessible from `Relation.Binary.Construct.On` instead."
  #-}
  {-# WARNING_ON_USAGE wellFounded
  "Warning: wellFounded was deprecated in v1.4.
\ \Please use wellFounded from `Relation.Binary.Construct.On` instead."
  #-}


-- DEPRECATED in v1.5.
-- Please use `TransClosure` from `Relation.Binary.Construct.Closure.Transitive` instead.
module TransitiveClosure {A : Set a} (_<_ : Rel A ) where

  infix 4 _<⁺_

  data _<⁺_ : Rel A (a  ) where
    [_]   :  {x y} (x<y : x < y)  x <⁺ y
    trans :  {x y z} (x<y : x <⁺ y) (y<z : y <⁺ z)  x <⁺ z

  downwardsClosed :  {x y}  Acc _<⁺_ y  x <⁺ y  Acc _<⁺_ x
  downwardsClosed (acc rs) x<y = acc  z z<x  rs z (trans z<x x<y))

  mutual

    accessible :  {x}  Acc _<_ x  Acc _<⁺_ x
    accessible acc-x = acc (accessible′ acc-x)

    accessible′ :  {x}  Acc _<_ x  WfRec _<⁺_ (Acc _<⁺_) x
    accessible′ (acc rs) y [ y<x ]         = accessible (rs y y<x)
    accessible′ acc-x    y (trans y<z z<x) =
      downwardsClosed (accessible′ acc-x _ z<x) y<z

  wellFounded : WellFounded _<_  WellFounded _<⁺_
  wellFounded wf = λ x  accessible (wf x)

  {-# WARNING_ON_USAGE _<⁺_
  "Warning: _<⁺_ was deprecated in v1.5.
\ \Please use TransClosure from Relation.Binary.Construct.Closure.Transitive instead."
  #-}


-- DEPRECATED in v1.3.
-- Please use `×-Lex` from `Data.Product.Relation.Binary.Lex.Strict` instead.
module Lexicographic {A : Set a} {B : A  Set b}
                     (RelA : Rel A ℓ₁)
                     (RelB :  x  Rel (B x) ℓ₂) where

  infix 4 _<_
  data _<_ : Rel (Σ A B) (a  b  ℓ₁  ℓ₂) where
    left  :  {x₁ y₁ x₂ y₂} (x₁<x₂ : RelA   x₁ x₂)  (x₁ , y₁) < (x₂ , y₂)
    right :  {x y₁ y₂}     (y₁<y₂ : RelB x y₁ y₂)  (x  , y₁) < (x  , y₂)

  mutual

    accessible :  {x y} 
                 Acc RelA x  (∀ {x}  WellFounded (RelB x)) 
                 Acc _<_ (x , y)
    accessible accA wfB = acc (accessible′ accA (wfB _) wfB)


    accessible′ :
       {x y} 
      Acc RelA x  Acc (RelB x) y  (∀ {x}  WellFounded (RelB x)) 
      WfRec _<_ (Acc _<_) (x , y)
    accessible′ (acc rsA) _    wfB ._ (left  x′<x) = accessible (rsA _ x′<x) wfB
    accessible′ accA (acc rsB) wfB ._ (right y′<y) =
      acc (accessible′ accA (rsB _ y′<y) wfB)

  wellFounded : WellFounded RelA  (∀ {x}  WellFounded (RelB x)) 
                WellFounded _<_
  wellFounded wfA wfB p = accessible (wfA (proj₁ p)) wfB

  well-founded = wellFounded

  {-# WARNING_ON_USAGE _<_
  "Warning: _<_ was deprecated in v1.3.
\ \Please use `×-Lex` from `Data.Product.Relation.Binary.Lex.Strict` instead."
  #-}
  {-# WARNING_ON_USAGE accessible
  "Warning: accessible was deprecated in v1.3."
  #-}
  {-# WARNING_ON_USAGE accessible′
  "Warning: accessible′ was deprecated in v1.3."
  #-}
  {-# WARNING_ON_USAGE wellFounded
  "Warning: wellFounded was deprecated in v1.3.
\ \Please use `×-wellFounded` from `Data.Product.Relation.Binary.Lex.Strict` instead."
  #-}



------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

-- Version 1.0

module Inverse-image = InverseImage
module Transitive-closure = TransitiveClosure