The strong induction principle for the natural numbers

module elementary-number-theory.strong-induction-natural-numbers where
Imports
open import elementary-number-theory.inequality-natural-numbers
open import elementary-number-theory.natural-numbers

open import foundation.cartesian-product-types
open import foundation.coproduct-types
open import foundation.dependent-pair-types
open import foundation.empty-types
open import foundation.function-extensionality
open import foundation.functions
open import foundation.identity-types
open import foundation.propositions
open import foundation.universe-levels

Idea

The strong induction principle allows one to assume in the inductive step that the inductive hypothesis is satisfied at all smaller values.

Definition

The -modality on families indexed by

□-≤-ℕ : {l : Level}  (  UU l)    UU l
□-≤-ℕ P n = (m : )  (m ≤-ℕ n)  P m

η-□-≤-ℕ : {l : Level} {P :   UU l}  ((n : )  P n)  (n : )  □-≤-ℕ P n
η-□-≤-ℕ f n m p = f m

ε-□-≤-ℕ :
  {l : Level} {P :   UU l}  ((n : )  □-≤-ℕ P n)  ((n : )  P n)
ε-□-≤-ℕ f n = f n n (refl-leq-ℕ n)

Theorem

The base case of the strong induction principle

zero-strong-ind-ℕ :
  {l : Level} (P :   UU l)  P zero-ℕ  □-≤-ℕ P zero-ℕ
zero-strong-ind-ℕ P p0 zero-ℕ t = p0

eq-zero-strong-ind-ℕ :
  {l : Level} (P :   UU l) (p0 : P zero-ℕ) (t : leq-ℕ zero-ℕ zero-ℕ) 
  zero-strong-ind-ℕ P p0 zero-ℕ t  p0
eq-zero-strong-ind-ℕ P p0 t = refl

The successor case of the strong induction principle

cases-succ-strong-ind-ℕ :
  {l : Level} (P :   UU l) (pS : (n : )  (□-≤-ℕ P n)  P (succ-ℕ n)) (n : )
  (H : □-≤-ℕ P n) (m : ) (c : (leq-ℕ m n) + (m  succ-ℕ n))  P m
cases-succ-strong-ind-ℕ P pS n H m (inl q) = H m q
cases-succ-strong-ind-ℕ P pS n H .(succ-ℕ n) (inr refl) = pS n H

succ-strong-ind-ℕ :
  {l : Level} (P :   UU l)  ((k : )  (□-≤-ℕ P k)  P (succ-ℕ k)) 
  (k : )  (□-≤-ℕ P k)  (□-≤-ℕ P (succ-ℕ k))
succ-strong-ind-ℕ P pS k H m p =
  cases-succ-strong-ind-ℕ P pS k H m (cases-leq-succ-ℕ p)

cases-htpy-succ-strong-ind-ℕ :
  {l : Level} (P :   UU l) (pS : (k : )  (□-≤-ℕ P k)  P (succ-ℕ k)) 
  (k : ) (H : □-≤-ℕ P k) (m : ) (c : (leq-ℕ m k) + (m  succ-ℕ k)) 
  (q : leq-ℕ m k) 
  ( cases-succ-strong-ind-ℕ P pS k H m c) 
  ( H m q)
cases-htpy-succ-strong-ind-ℕ P pS k H m (inl p) q =
  ap (H m) (eq-is-prop (is-prop-leq-ℕ m k))
cases-htpy-succ-strong-ind-ℕ P pS k H m (inr α) q =
  ex-falso (neg-succ-leq-ℕ k (concatenate-eq-leq-ℕ k (inv α) q))

htpy-succ-strong-ind-ℕ :
  {l : Level} (P :   UU l)  (pS : (k : )  (□-≤-ℕ P k)  P (succ-ℕ k)) 
  (k : ) (H : □-≤-ℕ P k) (m : ) (p : leq-ℕ m (succ-ℕ k)) (q : leq-ℕ m k) 
  ( succ-strong-ind-ℕ P pS k H m p) 
  ( H m q)
htpy-succ-strong-ind-ℕ P pS k H m p q =
  cases-htpy-succ-strong-ind-ℕ P pS k H m (cases-leq-succ-ℕ p) q

cases-eq-succ-strong-ind-ℕ :
  {l : Level} (P :   UU l) (pS : (k : )  (□-≤-ℕ P k)  P (succ-ℕ k)) 
  (k : ) (H : □-≤-ℕ P k)
  (c : (leq-ℕ (succ-ℕ k) k) + (succ-ℕ k  succ-ℕ k)) 
  ( (cases-succ-strong-ind-ℕ P pS k H (succ-ℕ k) c)) 
  ( pS k H)
cases-eq-succ-strong-ind-ℕ P pS k H (inl p) = ex-falso (neg-succ-leq-ℕ k p)
cases-eq-succ-strong-ind-ℕ P pS k H (inr α) =
  ap
    ( (cases-succ-strong-ind-ℕ P pS k H (succ-ℕ k))  inr)
    ( eq-is-prop' (is-set-ℕ (succ-ℕ k) (succ-ℕ k)) α refl)

eq-succ-strong-ind-ℕ :
  {l : Level} (P :   UU l) (pS : (k : )  (□-≤-ℕ P k)  P (succ-ℕ k)) 
  (k : ) (H : □-≤-ℕ P k) (p : leq-ℕ (succ-ℕ k) (succ-ℕ k)) 
  ( (succ-strong-ind-ℕ P pS k H (succ-ℕ k) p)) 
  ( pS k H)
eq-succ-strong-ind-ℕ P pS k H p =
  cases-eq-succ-strong-ind-ℕ P pS k H (cases-leq-succ-ℕ p)

The inductive step

induction-strong-ind-ℕ :
  {l : Level} (P :   UU l)  (□-≤-ℕ P zero-ℕ) 
  ((k : )  (□-≤-ℕ P k)  (□-≤-ℕ P (succ-ℕ k)))  (n : )  □-≤-ℕ P n
induction-strong-ind-ℕ P p0 pS zero-ℕ = p0
induction-strong-ind-ℕ P p0 pS (succ-ℕ n) =
  pS n (induction-strong-ind-ℕ P p0 pS n)

computation-succ-strong-ind-ℕ :
  {l : Level} (P :   UU l) (p0 : □-≤-ℕ P zero-ℕ) 
  (pS : (k : )  (□-≤-ℕ P k)  (□-≤-ℕ P (succ-ℕ k))) 
  (n : ) 
  ( induction-strong-ind-ℕ P p0 pS (succ-ℕ n)) 
  ( pS n (induction-strong-ind-ℕ P p0 pS n))
computation-succ-strong-ind-ℕ P p0 pS n = refl

The strong induction principle

strong-ind-ℕ :
  {l : Level}  (P :   UU l) (p0 : P zero-ℕ) 
  (pS : (k : )  (□-≤-ℕ P k)  P (succ-ℕ k)) (n : )  P n
strong-ind-ℕ P p0 pS =
  ε-□-≤-ℕ
    ( induction-strong-ind-ℕ P
      ( zero-strong-ind-ℕ P p0)
      ( succ-strong-ind-ℕ P pS))

compute-zero-strong-ind-ℕ :
  {l : Level} (P :   UU l) (p0 : P zero-ℕ) 
  (pS : (k : )  (□-≤-ℕ P k)  P (succ-ℕ k)) 
  strong-ind-ℕ P p0 pS zero-ℕ  p0
compute-zero-strong-ind-ℕ P p0 pS = refl

cases-eq-compute-succ-strong-ind-ℕ :
  { l : Level} (P :   UU l) (p0 : P zero-ℕ) 
  ( pS : (k : )  (□-≤-ℕ P k)  P (succ-ℕ k)) 
  ( n : ) 
  ( α :
    ( m : ) (p : leq-ℕ m n) 
    ( induction-strong-ind-ℕ P (zero-strong-ind-ℕ P p0)
      ( λ k z m₁ z₁ 
        cases-succ-strong-ind-ℕ P pS k z m₁ (cases-leq-succ-ℕ z₁))
      n m p) 
    ( strong-ind-ℕ P p0 pS m)) 
  ( m : ) (p : leq-ℕ m (succ-ℕ n)) 
  ( q : (leq-ℕ m n) + (m  succ-ℕ n)) 
  ( succ-strong-ind-ℕ P pS n
    ( induction-strong-ind-ℕ P
      ( zero-strong-ind-ℕ P p0)
      ( succ-strong-ind-ℕ P pS) n) m p) 
  ( strong-ind-ℕ P p0 pS m)
cases-eq-compute-succ-strong-ind-ℕ P p0 pS n α m p (inl x) =
  ( htpy-succ-strong-ind-ℕ P pS n
    ( induction-strong-ind-ℕ P
      ( zero-strong-ind-ℕ P p0)
      ( succ-strong-ind-ℕ P pS) n)
    m p x) 
  ( α m x)
cases-eq-compute-succ-strong-ind-ℕ P p0 pS n α .(succ-ℕ n) p (inr refl) =
  ( eq-succ-strong-ind-ℕ P pS n
    ( induction-strong-ind-ℕ P
      ( zero-strong-ind-ℕ P p0)
      ( succ-strong-ind-ℕ P pS) n)
    ( p)) 
  ( inv
    ( ap
      ( cases-succ-strong-ind-ℕ P pS n
        ( induction-strong-ind-ℕ P
          ( zero-strong-ind-ℕ P p0)
          ( λ k H m p₁ 
            cases-succ-strong-ind-ℕ P pS k H m (cases-leq-succ-ℕ p₁))
          n)
        ( succ-ℕ n))
      ( cases-leq-succ-reflexive-leq-ℕ)))

eq-compute-succ-strong-ind-ℕ :
  { l : Level} (P :   UU l) (p0 : P zero-ℕ) 
  ( pS : (k : )  (□-≤-ℕ P k)  P (succ-ℕ k)) 
  ( n : ) 
  ( m : ) (p : leq-ℕ m n) 
  ( induction-strong-ind-ℕ P (zero-strong-ind-ℕ P p0)
    ( λ k z m₁ z₁ 
      cases-succ-strong-ind-ℕ P pS k z m₁ (cases-leq-succ-ℕ z₁))
    n m p) 
  ( strong-ind-ℕ P p0 pS m)
eq-compute-succ-strong-ind-ℕ P p0 pS zero-ℕ zero-ℕ star = refl
eq-compute-succ-strong-ind-ℕ P p0 pS (succ-ℕ n) m p =
  cases-eq-compute-succ-strong-ind-ℕ P p0 pS n
    ( eq-compute-succ-strong-ind-ℕ P p0 pS n) m p
    ( cases-leq-succ-ℕ p)

compute-succ-strong-ind-ℕ :
  { l : Level} (P :   UU l) (p0 : P zero-ℕ) 
  ( pS : (k : )  (□-≤-ℕ P k)  P (succ-ℕ k)) 
  ( n : ) 
  strong-ind-ℕ P p0 pS (succ-ℕ n)  pS n  m p  strong-ind-ℕ P p0 pS m)
compute-succ-strong-ind-ℕ P p0 pS n =
  ( eq-succ-strong-ind-ℕ P pS n
    ( induction-strong-ind-ℕ P
      ( zero-strong-ind-ℕ P p0)
      ( succ-strong-ind-ℕ P pS)
      ( n))
    ( refl-leq-ℕ n)) 
  ( ap
    ( pS n)
    ( eq-htpy (eq-htpy  eq-compute-succ-strong-ind-ℕ P p0 pS n)))

total-strong-ind-ℕ :
  { l : Level} (P :   UU l) (p0 : P zero-ℕ) 
  ( pS : (k : )  (□-≤-ℕ P k)  P (succ-ℕ k)) 
  Σ ( (n : )  P n)
    ( λ h 
      ( h zero-ℕ  p0) ×
      ( (n : )  h (succ-ℕ n)  pS n  m p  h m)))
pr1 (total-strong-ind-ℕ P p0 pS) = strong-ind-ℕ P p0 pS
pr1 (pr2 (total-strong-ind-ℕ P p0 pS)) = compute-zero-strong-ind-ℕ P p0 pS
pr2 (pr2 (total-strong-ind-ℕ P p0 pS)) = compute-succ-strong-ind-ℕ P p0 pS

See also