-- The principle of mathematical induction, proved from the least counterexample
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Nat.Induction
import Least
import Foundation

-- The natural numbers that a set S leaves out.
def counterexamples (S : Set) : Set := { n ∈ ℕ | ¬(n ∈ S) }

theorem counterexamples.subset_naturals (S : Set)
  shows counterexamples(S) ⊆ ℕ
proof
  simp

-- A set that contains 0 and the successor of each of its members contains
-- every natural number. If it left some number out, the least such number
-- could not be 0, so it would be the successor of a number inside the set,
-- which puts it inside too.
theorem natural.induction (S : Set)
  requires base : 0 ∈ S
  requires step : ∀ n ∈ ℕ, n ∈ S → n + 1 ∈ S
  shows ∀ n ∈ ℕ, n ∈ S
proof
  intros n nMember
  by_contra absent
  have nIn : n ∈ counterexamples(S) by simp
  have inhabited : Nonempty(counterexamples(S)) := ⟨n, nIn⟩
  have naturals := counterexamples.subset_naturals at S
  have least := leastNatural.member with *
  obtain ⟨leastMember, leastAbsent⟩ := counterexamples.membership.forward with least
  have leastNat := nat.omega.backward with leastMember
  have shape := natural.zero_or_successor with leastNat
  cases shape with zero | successor
  . rw zero at leastAbsent
    exact leastAbsent with base
  . obtain ⟨k, kNat, equation⟩ := successor
    have kMember := nat.omega.forward with kNat
    have kIn : k ∈ S
      by_contra kAbsent
      have kCounter : k ∈ counterexamples(S) by simp [counterexamples.membership]
      have bound := leastNatural.least at counterexamples(S), k with *
      rw equation at bound
      arith
    have next := step with kMember, kIn
    have bound := add.right_one at k
    rw [bound, ← equation] at next
    exact leastAbsent with next