Grace/Cumulus/Nat/Foundation.g17

Open in Workbench Download source

Imports

Core.Nat · Set.Ordinal

Declarations

Source

1-- Natural numbers as von Neumann ordinals2-- 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.Foundation8import Core.Nat9import Set.Ordinal1011-- Natural numbers compute compactly, while these theorems expose their12-- von Neumann set interpretation whenever a proof needs raw membership.13lemma membership.successor (m n : Nat)14  shows m ∈ succ(n) ↔ (m ∈ n ∨ m = n)15proof16  simp1718lemma membership.successor_set (x : Set) {n : Nat}19  shows x ∈ succ(n) ↔ (x ∈ n ∨ x = n)20proof21  simp2223lemma membership.successor_forward (x : Set) {n : Nat}24  requires h : x ∈ succ(n)25  shows x ∈ n ∨ x = n26proof27  simp2829lemma membership.successor_backward (x : Set) {n : Nat}30  requires h : x ∈ n ∨ x = n31  shows x ∈ succ(n)32proof33  simp3435-- Every position in a finite ordinal is itself a natural number.36theorem natural.member (n : Nat)37  shows ∀ i ∈ n, Nat(i)38proof39  induction n40  | zero =>41    intros i hi42    rw nat.zero at hi43    exfalso44    exact set.empty with hi45  | succ(k) using ih =>46    intros i hi47    have alternatives := membership.successor_forward{n := k} with hi48    cases alternatives with before | equal49    . exact ih with i, before50    . rw equal51      assumption5253lemma membership.self_successor (n : Nat)54  shows n ∈ succ(n)55proof56  simp5758lemma membership.two_in_five59  shows 2 ∈ 560proof61  simp [next.natural, next.membership]6263theorem membership.one (x : Set)64  shows x ∈ 1 ↔ x = 065proof66  have successorZero := next.natural at 067  rw successorZero68  simp [next.membership, nat.zero, set.empty]6970theorem membership.two (x : Set)71  shows x ∈ 2 ↔ (x = 0 ∨ x = 1)72proof73  have split := membership.successor_set{n := 1} at x74  have one := membership.one at x75  tauto7677theorem membership.three (x : Set)78  shows x ∈ 3 ↔ (x = 0 ∨ x = 1 ∨ x = 2)79proof80  have split := membership.successor_set{n := 2} at x81  have two := membership.two at x82  tauto8384theorem natural.zero_one_or_above_one (n : Nat)85  shows n = 0 ∨ n = 1 ∨ 1 ∈ n86proof87  induction n88  | zero =>89    left90    rfl91  | succ(k) using ih =>92    cases ih with hkZero | hkRest93    . right94      left95      rw hkZero96      rfl97    . cases hkRest with hkOne | hkAbove98      . right99        right100        rw hkOne101        settle with membership.successor,102          Naturals.constructor.zero, Naturals.constructor.succ103      . right104        right105        settle with membership.successor, hkAbove,106          Naturals.constructor.zero, Naturals.constructor.succ107108theorem natural.zero_or_successor (n : Nat)109  shows n = 0 ∨ ∃ k, Nat(k) ∧ n = succ(k)110proof111  induction n112  | zero =>113    left114    rfl115  | succ(k) using ih =>116    right117    refine ⟨k, assumption, rfl⟩118119-- Every member of a natural number is a natural number.120theorem natural.member_natural (n : Nat)121  shows ∀ x ∈ n, Nat(x)122proof123  induction n124  | zero =>125    intros x hx126    have z := nat.zero127    rw z at hx128    exfalso129    exact set.empty with hx130  | succ(k) using ih =>131    intros x hx132    have d := membership.successor_forward{n := k} with hx133    cases d with inner | same134    . exact ih with x, inner135    . rw same136      assumption137138-- ω, the set of all natural numbers, is an ordinal: it is transitive, and139-- so is each of its members.140theorem Ordinal.omega141  shows ω ∈ Ordinal142proof143  constructor144    intros n hn x hx145    have hnat := nat.omega.backward with hn146    have members := natural.member_natural with hnat147    have xnat := members with x, hx148    exact nat.omega.forward with xnat149  . intros n hn150    have hnat := nat.omega.backward with hn151    have ord := Ordinal.natural with hnat152    exact Ordinal.transitive with ord153154-- ω is a limit ordinal: nonempty and closed under successor.155theorem Limit.omega156  shows Limit(ω)157proof158  constructor159  . exact Ordinal.omega160  . constructor161    . intro e162      have zeroNat := Naturals.constructor.zero163      have z := nat.omega.forward with zeroNat164      rw e at z165      exact set.empty with z166    . intros n hn167      have hnat := nat.omega.backward with hn168      have step := next.natural with hnat169      rw ← step170      have snat := Naturals.constructor.succ with hnat171      exact nat.omega.forward with snat172