module My.SetTheory.Induction.Nat where
import Data.Nat as DN
import Level as L
import Relation.Unary as RU
open DN using (_+_ ; _<′_)
import My.SetTheory.Induction.WellFounded _<′_ as MySTIWF
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)
<′-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)
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
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