module My.SetTheory.Induction.Nat where

-- §──────────────────────────────────────────────────────────────────
-- This module was written to help me understand Induction.Nat from
-- stdlib.
-- §──────────────────────────────────────────────────────────────────

-- §──────────────────────────────────────────────────────────────────
-- Required modules
-- §──────────────────────────────────────────────────────────────────

import Data.Nat as DN
import Level as L
import Relation.Unary as RU

open DN using (_+_ ; _<′_)

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

-- §──────────────────────────────────────────────────────────────────
-- Weak induction on ℕ
-- §──────────────────────────────────────────────────────────────────

-- My definition.

weakInduction : {𝓁 : L.Level} → (P : RU.Pred DN.ℕ 𝓁) → (base : P 0) →
  (ihyp : (n : DN.ℕ) → P n → P (DN.suc n)) → (n : DN.ℕ) → P n
weakInduction P base ihyp 0 = base
weakInduction P base ihyp (DN.suc n) =
  ihyp n (weakInduction P base ihyp n)

-- §──────────────────────────────────────────────────────────────────
-- _<′_ is a well-founded relation on ℕ.  Shin-Cheng Mu, Well-founded
-- recursion and accessibility, http://www.iis.sinica.edu.tw/~scm/
-- well-founded-recursion-and-accessibility/
-- §──────────────────────────────────────────────────────────────────

<′-ihyp : (n : DN.ℕ) → (m : DN.ℕ) → m <′ n → MySTIWF.Acc m
<′-ihyp 0 m ()
<′-ihyp (DN.suc n) .n DN.≤′-refl = MySTIWF.acc (<′-ihyp n)
<′-ihyp (DN.suc n) m (DN.≤′-step m<n) = <′-ihyp n m m<n

<′-well-founded : MySTIWF.WellFounded
<′-well-founded n = MySTIWF.acc (<′-ihyp n)

-- §──────────────────────────────────────────────────────────────────
-- Strong induction on ℕ.  Same as <′-rec in Induction.Nat .
-- §──────────────────────────────────────────────────────────────────

strongInduction : {𝓃 : L.Level} → (P : RU.Pred DN.ℕ 𝓃) →
  (ihyp : (n : DN.ℕ) → ((m : DN.ℕ) → m <′ n → P m) → P n) → (n : DN.ℕ) → P n
strongInduction = MySTIWF.wfRec <′-well-founded

-- §──────────────────────────────────────────────────────────────────
-- Examples
-- §──────────────────────────────────────────────────────────────────

private
  module Examples where

  import Function as F
  import Relation.Binary.PropositionalEquality as RBPE

  open F using (_∘_)
  open RBPE using (_≡_)

  P : RU.Pred DN.ℕ L.zero
  P n = DN.ℕ

  twice-base = 0

  twiceIhyp : (n : DN.ℕ) → (pn : P n)  → P (DN.suc n)
  twiceIhyp n pn = DN.suc (DN.suc pn)

  twice : DN.ℕ → DN.ℕ
  twice = weakInduction P twice-base twiceIhyp

  halfIhyp : (n : DN.ℕ) → ((m : DN.ℕ) → m <′ n → P m) → P n
  halfIhyp 0 f = 0
  halfIhyp 1 f = 0
  halfIhyp (DN.suc (DN.suc n)) f = DN.suc (f n (DN.≤′-step DN.≤′-refl))

  half : DN.ℕ → DN.ℕ
  half = strongInduction P halfIhyp

  Q : RU.Pred DN.ℕ L.zero
  Q n = half (twice n) ≡ n

  halfTwiceIhyp : (n : DN.ℕ) → ((m : DN.ℕ) → m <′ n → Q m) → Q n
  halfTwiceIhyp 0 f = RBPE.refl
  halfTwiceIhyp 1 f = RBPE.refl
  halfTwiceIhyp (DN.suc (DN.suc n)) f =
    RBPE.cong (DN.suc ∘ DN.suc) (f n (DN.≤′-step DN.≤′-refl))

  halfTwice : (n : DN.ℕ) → Q n
  halfTwice = strongInduction Q halfTwiceIhyp

  half2+ : (n : DN.ℕ) → half (2 + n) ≡ 1 + half n
  half2+ n =
    begin
      half (2 + n)                                                        ≡⟨⟩
      strongInduction P halfIhyp (2 + n)                                  ≡⟨⟩
      MySTIWF.wfRec <′-well-founded P halfIhyp (2 + n)                    ≡⟨⟩
      MySTIWF.accRec P halfIhyp (2 + n) (<′-well-founded (2 + n))         ≡⟨⟩
      MySTIWF.accRec P halfIhyp (2 + n) (MySTIWF.acc φ)                   ≡⟨⟩
      halfIhyp (2 + n) ψ                                                  ≡⟨⟩
      DN.suc (ψ n w)                                                      ≡⟨⟩
      DN.suc (MySTIWF.accRec P halfIhyp n (φ n w))                        ≡⟨⟩
      DN.suc (MySTIWF.accRec P halfIhyp n (<′-ihyp (2 + n) n w))          ≡⟨⟩
      DN.suc (MySTIWF.accRec P halfIhyp n (<′-ihyp (1 + n) n DN.≤′-refl)) ≡⟨⟩
      DN.suc (MySTIWF.accRec P halfIhyp n (MySTIWF.acc (<′-ihyp n)))      ≡⟨⟩
      DN.suc (MySTIWF.accRec P halfIhyp n (<′-well-founded n))            ≡⟨⟩
      DN.suc (MySTIWF.wfRec <′-well-founded P halfIhyp n)                 ≡⟨⟩
      DN.suc (strongInduction P halfIhyp n)                               ≡⟨⟩
      DN.suc (half n) ∎
    where
      open RBPE.≡-Reasoning
      φ : (m : DN.ℕ) → m <′ 2 + n → MySTIWF.Acc m
      φ = <′-ihyp (2 + n)
      ψ : (m : DN.ℕ) → (w : m <′ 2 + n) → P m
      ψ m w = MySTIWF.accRec P halfIhyp m (φ m w)
      w : n <′ 2 + n
      w = DN.≤′-step DN.≤′-refl