{-
NESTED WELLFOUNDED INDUCTION

The main result of this module is a statement corresponding to nested
accessibility (a.k.a. wellfounded) induction.
-}

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


open import Cubical.Foundations.Prelude

module squier.accessibility where

open import Cubical.Data.Sigma
open import Cubical.Induction.WellFounded
  renaming (WellFounded to isWellFounded;
            Acc to isAcc;
            Rel to BinRel)

private variable
  ℓ₀ ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level

{- The following is a version of the statement 'wfi', which is part
of the library, but marked as private. It is a special case of the
general accessibility induction (the type family here does not depend
on a proof of accessibility): -}
module _ (A : Type ℓ₀) (_<_ : A → A → Type ℓ₁) where
  acc-ind : (P : A → Type ℓ₂)
            → ((a : A) → isAcc _<_ a
                  → ((∀ a' → a' < a → P a') → P a))
            → (a : A)
            → isAcc _<_ a
            → P a
  acc-ind P ih a (acc wrec⟨a⟩) =
            ih a (acc wrec⟨a⟩) λ a' a'<a → acc-ind P ih a' (wrec⟨a⟩ a' a'<a)
  -- Note: It should also be possible to just use WFI.induction
  -- (which however assumes global accessibility)



-- "Double accessibility induction"
module _ {B : Type ℓ₀} (_<B_ : B → B → Type ℓ₁)
         {C : Type ℓ₂} (_<C_ : C → C → Type ℓ₃) where

  double-acc-ind :
    (P : B × C → Type ℓ₄) →
    ((b : B) → (isAcc _<B_ b) → (c : C) → (isAcc _<C_ c) →
      (∀ b' → b' <B b → P (b' , c)) →
      (∀ c' → c' <C c → P (b , c')) →
      P (b , c)) →
    (b : B) → (isAcc _<B_ b) → (c : C) → (isAcc _<C_ c) → P (b , c)
  double-acc-ind P ih b isAcc⟨b⟩ =
    -- "outer" accessibility induction: show statement by <B-induction
    -- for all c
    acc-ind B _<B_ (λ b₀ → (c : C) → isAcc _<C_ c → P (b₀ , c))
            inner-ind b isAcc⟨b⟩
    where
      inner-ind : (b₁ : B) → isAcc _<B_ b₁ →
                  ((b₁' : B) → b₁' <B b₁ → (c : C)
                        → isAcc _<C_ c → P (b₁' , c)) →
                  (c : C) → isAcc _<C_ c → P (b₁ , c)
      inner-ind b₁ isAcc⟨b₁⟩ ihb₁ c isAcc⟨c⟩ =
        -- "inner" accessibility induction: show statement by <C-induction,
        -- where b₁ is fixed
        acc-ind C _<C_ (λ c₁ → P (b₁ , c₁)) aux c isAcc⟨c⟩
          where
          aux : (c₁ : C) → isAcc _<C_ c₁ →
                    ((c₁' : C) → c₁' <C c₁ → P (b₁ , c₁')) → P (b₁ , c₁)
          aux c₁ isAcc⟨c₁⟩ ihc₁ = ih b₁ isAcc⟨b₁⟩ c₁ isAcc⟨c₁⟩
                                    (λ b' b'<b₁ → ihb₁ b' b'<b₁ c₁ isAcc⟨c₁⟩)
                                    ihc₁

open import squier.graphclosures

{- The transitive closure of a wellfounded relation is wellfounded. -}

module _ (A : Type ℓ₀) (_<_ : A → A → Type ℓ₁) (wf< : isWellFounded _<_) where

  _<⁺_ = TransClosure _<_

  multiple-steps : ∀ {a c} → c <⁺ a →
                     (∀ b → b < a → isAcc _<⁺_ b) → isAcc _<⁺_ c
  multiple-steps [ c<a ]⁺ ih = ih _ c<a
  multiple-steps (c<c₁ ∷⁺ c₁<⁺a) ih with multiple-steps c₁<⁺a ih
  multiple-steps (c<c₁ ∷⁺ c₁<⁺a) ih | acc <c₁-is-acc = <c₁-is-acc _ [ c<c₁ ]⁺

  transitive-wellfounded : isWellFounded (TransClosure _<_)
  transitive-wellfounded =
    WFI.induction wf< (λ a ih → acc (λ c c<⁺a → multiple-steps c<⁺a ih))

{- A monotone map reflects accessibility and wellfoundedness. -}

module _ (A : Type ℓ₀) (_<_ : BinRel A ℓ₂)
         (B : Type ℓ₁) (_≺_ : BinRel B ℓ₂)
         (f : A → B) (monotone : ∀ {x y} → x < y → f x ≺ f y) where

  acc-reflected : (a : A) → isAcc _≺_ (f a) → isAcc _<_ a
  acc-reflected a acc⟨fa⟩ =
    acc-ind B _≺_
            (λ b → (a : A) → (f a ≡ b) → isAcc _<_ a)
            (λ b₁ acc⟨b₁⟩ ih a₁ fa₁≡b₁ →
                  acc λ a₂ a₂<a₁ →
                      ih (f a₂) (subst (λ b' → f a₂ ≺ b')
                                        fa₁≡b₁
                                        (monotone a₂<a₁))
                                        a₂ refl)
            (f a) acc⟨fa⟩ a refl

  wf-reflected : isWellFounded _≺_ → isWellFounded _<_
  wf-reflected wf⟨≺⟩ = λ a → acc-reflected a (wf⟨≺⟩ (f a))

{- The transitive closure of a co-wellfounded (a.k.a Noetherian)
   relation is co-wellfounded. -}

module _ (A : Type ℓ₀) (_>_ : A → A → Type ℓ₁)
                       (noeth> : isWellFounded (λ x y → y > x)) where

  _>⁺_ = TransClosure _>_

  transitive-Noetherian : isWellFounded (λ x y → y >⁺ x)
  transitive-Noetherian = wf-reflected A (λ x y → y >⁺ x)
                                       A (TransClosure (λ x y → y > x))
                                       (λ a → a)
                                       revClosureComm
                                       (transitive-wellfounded A (λ x y → y > x) noeth>)