{-# OPTIONS --without-K #-}
module Util.Induction.WellFounded where

open import Induction.WellFounded public using
  ( Acc ; acc ; WellFounded ; module Subrelation ; module InverseImage
  ; module TransitiveClosure ; module Lexicographic )

open import Relation.Binary using (Rel)

open import Util.HoTT.FunctionalExtensionality using (funext)
open import Util.HoTT.HLevel using (IsProp ; ∀-IsProp)
open import Util.Prelude


module _ {α β} {A : Set α} {_<_ : Rel A β} where


  Acc-IsProp : ∀ {x} → IsProp (Acc _<_ x)
  Acc-IsProp (acc rs₀) (acc rs₁)
    = cong acc (funext λ y → funext λ y<x → Acc-IsProp _ _)


  WellFounded-IsProp : IsProp (WellFounded _<_)
  WellFounded-IsProp = ∀-IsProp λ _ → Acc-IsProp


  wfInd-acc : ∀ {γ} (P : A → Set γ)
    → (∀ x → (∀ y → y < x → P y) → P x)
    → ∀ x → Acc _<_ x → P x
  wfInd-acc P f x (acc rs) = f x (λ y y<x → wfInd-acc P f y (rs y y<x))


  mutual
    wfIndΣ-acc : ∀ {γ} (P : A → Set γ)
      → (Q : ∀ x y → P x → P y → Set)
      → (f : ∀ x
          → (g : ∀ y → y < x → P y)
          → (∀ y y<x z z<x → Q y z (g y y<x) (g z z<x))
          → P x)
      → (∀ x g g-resp y h h-resp
          → (∀ z z<x z′ z′<y → Q z z′ (g z z<x) (h z′ z′<y))
          → Q x y (f x g g-resp) (f y h h-resp))
      → ∀ x → Acc _<_ x → P x
    wfIndΣ-acc P Q f f-resp x (acc rs)
      = f x
         (λ y y<x → wfIndΣ-acc P Q f f-resp y (rs y y<x))
         (λ y y<x z z<x
            → wfIndΣ-acc-resp P Q f f-resp y (rs y y<x) z (rs z z<x))


    wfIndΣ-acc-resp : ∀ {γ} (P : A → Set γ)
      → (Q : ∀ x y → P x → P y → Set)
      → (f : ∀ x
          → (g : ∀ y → y < x → P y)
          → (∀ y y<x z z<x → Q y z (g y y<x) (g z z<x))
          → P x)
      → (f-resp : ∀ x g g-resp y h h-resp
          → (∀ z z<x z′ z′<y → Q z z′ (g z z<x) (h z′ z′<y))
          → Q x y (f x g g-resp) (f y h h-resp))
      → ∀ x x-acc y y-acc
      → Q x y (wfIndΣ-acc P Q f f-resp x x-acc) (wfIndΣ-acc P Q f f-resp y y-acc)
    wfIndΣ-acc-resp P Q f f-resp x (acc rsx) y (acc rsy)
      = f-resp _ _ _ _ _ _ λ z z<x z′ z′<y
          → wfIndΣ-acc-resp P Q f f-resp z (rsx z z<x) z′ (rsy z′ z′<y)


  module Build (<-wf : WellFounded _<_) where


    wfInd : ∀ {γ} (P : A → Set γ)
      → (∀ x → (∀ y → y < x → P y) → P x)
      → ∀ x → P x
    wfInd P f x = wfInd-acc P f x (<-wf x)


    wfRec : ∀ {γ} {B : Set γ}
      → (∀ x → (∀ y → y < x → B) → B)
      → A → B
    wfRec = wfInd _


    wfInd-unfold : ∀ {γ} (P : A → Set γ)
      → (f : ∀ x → (∀ y → y < x → P y) → P x)
      → (x : A)
      → wfInd P f x ≡ f x (λ y _ → wfInd P f y)
    wfInd-unfold P f x with <-wf x
    ... | acc rs
      = cong (f x)
          (funext λ y → funext λ y<x →
            cong (wfInd-acc P f y) (Acc-IsProp (rs y y<x) (<-wf y)))


    wfRec-unfold : ∀ {γ} {B : Set γ}
      → (f : ∀ x → (∀ y → y < x → B) → B)
      → (x : A)
      → wfRec f x ≡ f x (λ y _ → wfRec f y)
    wfRec-unfold = wfInd-unfold _


    wfInd-ind : ∀ {γ} {P : A → Set γ}
      → (Q : ∀ x → P x → Set)
      → {f : ∀ x → (∀ y → y < x → P y) → P x}
      → (∀ x g
          → (∀ y y<x → Q y (g y y<x))
          → Q x (f x g))
      → {x : A}
      → Q x (wfInd P f x)
    wfInd-ind {P = P} Q {f} f-resp
      = wfInd (λ x → Q x (wfInd P f x))
          (λ x rec → subst (Q x) (sym (wfInd-unfold P f x))
            (f-resp _ _ rec))
          _


    module _ {γ} (P : A → Set γ)
      (Q : ∀ x y → P x → P y → Set)
      (f : ∀ x
        → (g : ∀ y → y < x → P y)
        → (∀ y y<x z z<x → Q y z (g y y<x) (g z z<x))
        → P x)
      (f-resp : ∀ x g g-resp y h h-resp
        → (∀ z z<x z′ z′<y → Q z z′ (g z z<x) (h z′ z′<y))
        → Q x y (f x g g-resp) (f y h h-resp))
      where

      wfIndΣ : Σ[ f ∈ (∀ x → P x) ] (∀ x y → Q x y (f x) (f y))
      wfIndΣ
        = (λ x → wfIndΣ-acc P Q f f-resp x (<-wf x))
        , λ x y → wfIndΣ-acc-resp P Q f f-resp x (<-wf x) y (<-wf y)


      wfIndΣ-unfold : ∀ {x}
        → wfIndΣ .proj₁ x
        ≡ f x (λ y y<x → wfIndΣ .proj₁ y)
            (λ y y<x z z<x → wfIndΣ .proj₂ y z)
      wfIndΣ-unfold {x} with <-wf x
      ... | acc rs
        = go rs (λ y y<x → <-wf y)
        where
          go : (p q : (y : A) → y < x → Acc _<_ y)
            → f x (λ y y<x → wfIndΣ-acc P Q f f-resp y (p y y<x))
                (λ y y<x z z<x
                  → wfIndΣ-acc-resp P Q f f-resp y (p y y<x) z (p z z<x))
            ≡ f x (λ y y<x → wfIndΣ-acc P Q f f-resp y (q y y<x))
                (λ y y<x z z<x
                  → wfIndΣ-acc-resp P Q f f-resp y (q y y<x) z (q z z<x))
          go p q
            rewrite (funext λ y → funext λ y<x → Acc-IsProp (p y y<x) (q y y<x))
            = refl


      wfIndΣ′ : Σ[ g ∈ (∀ x → P x) ]
        Σ[ g-param ∈ (∀ x y → Q x y (g x) (g y)) ]
          (∀ {x} → g x ≡ f x (λ y y<x → g y) (λ y y<x z z<x → g-param y z))
      wfIndΣ′ = wfIndΣ .proj₁ , wfIndΣ .proj₂ , wfIndΣ-unfold


  open Build public


module _ {α β γ δ} {A : Set α} {B : Set β} where

  ×-Rel : Rel A γ → Rel B δ → Rel (A × B) (γ ⊔ℓ δ)
  ×-Rel R S (a , b) (a′ , b′) = R a a′ × S b b′


  ×-wellFounded : {R : Rel A γ} {S : Rel B δ}
    → WellFounded R → WellFounded S → WellFounded (×-Rel R S)
  ×-wellFounded {R} {S} R-wf S-wf (a , b) = ×-acc (R-wf a) (S-wf b)
    where
      ×-acc : ∀ {x y} → Acc R x → Acc S y → Acc (×-Rel R S) (x , y)
      ×-acc (acc rsa) (acc rsb)
        = acc (λ { (a , b) (a<x , b<y) → ×-acc (rsa a a<x) (rsb b b<y) })


-- This is not in Build because the implementation uses wfInd at
-- (×-Rel _<_ _<_), but within Build, we can only use wfInd at
-- _<_.
wfInd-ind₂ : ∀ {α β} {A : Set α} {_<_ : Rel A β}
  → (<-wf : WellFounded _<_)
  → ∀ {γ} {P : A → Set γ}
  → (R : ∀ x y → P x → P y → Set)
  → {f : ∀ x → (∀ y → y < x → P y) → P x}
  → (∀ x x′ g g′
      → (∀ y y′ y<x y′<x → R y y′ (g y y<x) (g′ y′ y′<x))
      → R x x′ (f x g) (f x′ g′))
  → {x x′ : A}
  → R x x′ (wfInd <-wf P f x) (wfInd <-wf P f x′)
wfInd-ind₂ <-wf {P = P} R {f} f-resp
  = wfInd (×-wellFounded <-wf <-wf)
      (λ { (x , x′) → R x x′ (wfInd <-wf P f x) (wfInd <-wf P f x′)})
      (λ where
        (x , y) rec
          → subst₂ (R x y)
              (sym (wfInd-unfold <-wf P f x))
              (sym (wfInd-unfold <-wf P f y))
              (f-resp x y _ _ λ x′ y′ x′<x y′<y → rec (x′ , y′) (x′<x , y′<y)))
      _