Grace/Cumulus/Nat/Induction.g17

Open in Workbench Download source

Imports

Least · Foundation

Declarations

• counterexamples def
• counterexamples.subset_naturals theorem derivation
• natural.induction theorem derivation

Source

1-- The principle of mathematical induction, proved from the least counterexample2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Nat.Induction8import Least9import Foundation1011-- The natural numbers that a set S leaves out.12def counterexamples (S : Set) : Set := { n ∈ ℕ | ¬(n ∈ S) }1314theorem counterexamples.subset_naturals (S : Set)15  shows counterexamples(S) ⊆ ℕ16proof17  simp1819-- A set that contains 0 and the successor of each of its members contains20-- every natural number. If it left some number out, the least such number21-- could not be 0, so it would be the successor of a number inside the set,22-- which puts it inside too.23theorem natural.induction (S : Set)24  requires base : 0 ∈ S25  requires step : ∀ n ∈ ℕ, n ∈ S → n + 1 ∈ S26  shows ∀ n ∈ ℕ, n ∈ S27proof28  intros n nMember29  by_contra absent30  have nIn : n ∈ counterexamples(S) by simp31  have inhabited : Nonempty(counterexamples(S)) := ⟨n, nIn⟩32  have naturals := counterexamples.subset_naturals at S33  have least := leastNatural.member with *34  obtain ⟨leastMember, leastAbsent⟩ := counterexamples.membership.forward with least35  have leastNat := nat.omega.backward with leastMember36  have shape := natural.zero_or_successor with leastNat37  cases shape with zero | successor38  . rw zero at leastAbsent39    exact leastAbsent with base40  . obtain ⟨k, kNat, equation⟩ := successor41    have kMember := nat.omega.forward with kNat42    have kIn : k ∈ S43      by_contra kAbsent44      have kCounter : k ∈ counterexamples(S) by simp [counterexamples.membership]45      have bound := leastNatural.least at counterexamples(S), k with *46      rw equation at bound47      arith48    have next := step with kMember, kIn49    have bound := add.right_one at k50    rw [bound, ← equation] at next51    exact leastAbsent with next52