-- §──────────────────────────────────────────────────────────────────
-- Modules required to specify the parameters of this module.
-- §──────────────────────────────────────────────────────────────────

import Level as L
import Relation.Binary as RB

-- §──────────────────────────────────────────────────────────────────
-- This module
-- §──────────────────────────────────────────────────────────────────

module My.SetTheory.Induction.NoInfiniteDescent {𝓁 𝓂 : L.Level} {A : Set 𝓁}
  (_<_ : RB.Rel A 𝓂) where

-- §──────────────────────────────────────────────────────────────────
-- Other required modules
-- §──────────────────────────────────────────────────────────────────

import Data.Product as DP
import Function as F
import Relation.Nullary as RN
import Relation.Unary as RU

open DP using (_×_)
open F using (_∘_ ; _$_)
open L using (_⊔_)

import My.SetTheory.Induction.WellFounded _<_ as MySTIWF

-- §──────────────────────────────────────────────────────────────────
-- http://ncatlab.org/nlab/show/well-founded+relation
-- §──────────────────────────────────────────────────────────────────

-- NoMinimalElement : {𝓃 : L.Level} → RU.Pred A 𝓃 → Set (𝓁 ⊔ 𝓂 ⊔ 𝓃)
-- NoMinimalElement P = {a : A} → P a → DP.Σ[ b ∈ A ] b < a × P b

record notMinimal {𝓃 : L.Level} (P : RU.Pred A 𝓃) (a : A) : Set (𝓁 ⊔ 𝓂 ⊔ 𝓃)
  where
    field
      elt : A
      lessPf : elt < a
      eltPf : P elt

NoMinimalElt : {𝓃 : L.Level} → RU.Pred A 𝓃 → Set (𝓁 ⊔ 𝓂 ⊔ 𝓃)
NoMinimalElt P = {a : A} → P a → notMinimal P a

NoInfiniteDescent : (𝓃 : L.Level) → Set (𝓁 ⊔ 𝓂 ⊔ L.suc 𝓃)
NoInfiniteDescent 𝓃 = (P : RU.Pred A 𝓃) → NoMinimalElt P → (a : A) → RN.¬ P a

private
  lem : {𝓃 : L.Level} → (P : RU.Pred A 𝓃) → NoMinimalElt P →
    (a : A) → ((b : A) → b < a → RN.¬ P b) → RN.¬ P a
  lem P nomineltp a φ pa = φ N.elt N.lessPf N.eltPf
    where
      module N = notMinimal (nomineltp pa)

wellFounded⇒NoInfiniteDescent : MySTIWF.WellFounded → {𝓃 : L.Level} →
  NoInfiniteDescent 𝓃
wellFounded⇒NoInfiniteDescent wf {𝓃} P nomineltp = MySTIWF.wfRec wf Q ihyp
  where
    Q : RU.Pred A 𝓃
    Q = RN.¬_ ∘ P
    ihyp : (x : A) → ((y : A) → y < x → Q y) → Q x
    ihyp = lem P nomineltp