Grace/Bootstrap/Nat.g17

Open in Workbench Download source

Imports

None

Declarations

• nat.zero theorem derivation
• nat.succ theorem derivation
• nat.omega theorem derivation
• Naturals.constructor.zero theorem derivation
• Naturals.constructor.succ theorem derivation
• bootstrap.singleton.membership theorem derivation
• bootstrap.union2.membership theorem derivation
• bootstrap.succ.membership theorem derivation
• bootstrap.succ.self theorem derivation
• Naturals.disjoint.zero.succ theorem derivation
• bootstrap.pair.left theorem derivation
• bootstrap.pair.right theorem derivation
• bootstrap.pair.nonempty theorem derivation
• bootstrap.membership.asymmetric theorem derivation
• Naturals.injective.succ theorem derivation

Source

1-- Checked bridge between the compact Nat datatype and von Neumann naturals.2-- Elaborated before the module graph, directly after Aliases.3-- Part of the Grace17 proof assistant for mathematics based on set theory.4-- Copyright (c) 2026 Grant Olney Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78theorem nat.zero9  shows zero = ∅10proof11  settle with zero1213theorem nat.succ (n : Set)14  requires hn : Nat(n)15  shows succ(n) = ⋃({n, pair(n, n)})16proof17  settle with succ1819theorem nat.omega (n : Set)20  shows Nat(n) ↔ n ∈ ℕ21proof22  settle with Nat2324theorem Naturals.constructor.zero25  shows Nat(zero)26proof27  have infinity := set.infinity28  unfold Nat29  rw nat.zero30  exact infinity.left3132theorem Naturals.constructor.succ (n : Set)33  requires hn : Nat(n)34  shows Nat(succ(n))35proof36  have infinity := set.infinity37  unfold Nat at hn38  unfold Nat39  rw nat.succ40  exact infinity.right with n, hn4142theorem bootstrap.singleton.membership (x a : Set)43  shows x ∈ {a} ↔ x = a44proof45  settle with singleton, pair.membership4647theorem bootstrap.union2.membership (x A B : Set)48  shows x ∈ A ∪ B ↔ (x ∈ A ∨ x ∈ B)49proof50  settle with union2, set.union, pair.membership5152-- The foundation has no primitive singleton: pair(n, n) is {n}, and the53-- successor is n ∪ pair(n, n).54theorem bootstrap.succ.membership (x n : Set)55  shows x ∈ succ(n) ↔ (x ∈ n ∨ x = n)56proof57  have fold : succ(n) = n ∪ pair(n, n) by simp [succ, union2]58  rw fold59  simp [bootstrap.union2.membership, pair.membership]6061theorem bootstrap.succ.self (n : Set)62  shows n ∈ succ(n)63proof64  settle with bootstrap.succ.membership6566theorem Naturals.disjoint.zero.succ (n : Set)67  shows zero ≠ succ(n)68proof69  intro h70  have self := bootstrap.succ.self at n71  rw ← h at self72  settle with zero, set.empty7374theorem bootstrap.pair.left (x y : Set)75  shows x ∈ {x, y}76proof77  settle with pair.membership7879theorem bootstrap.pair.right (x y : Set)80  shows y ∈ {x, y}81proof82  settle with pair.membership8384theorem bootstrap.pair.nonempty (a b : Set)85  shows {a, b} ≠ ∅86proof87  intro h88  have member := bootstrap.pair.left at a, b89  rw h at member90  settle with set.empty9192theorem bootstrap.membership.asymmetric (a b : Set)93  requires hab : a ∈ b94  shows b ∉ a95proof96  intro hba97  have nonempty := bootstrap.pair.nonempty at a, b98  obtain ⟨m, hmPair, minimal⟩ := foundation at {a, b} with nonempty99  simp [pair.membership] at hmPair100  cases hmPair with hma | hmb101  . rw ← hma at hba102    exact minimal with b, hba, (bootstrap.pair.right at a, b)103  . rw ← hmb at hab104    exact minimal with a, hab, (bootstrap.pair.left at a, b)105106theorem Naturals.injective.succ (a b : Set)107  requires h : succ(a) = succ(b)108  shows a = b109proof110  have aIn : a ∈ b ∨ a = b by rw ← bootstrap.succ.membership; rw ← h; simp111  have bIn : b ∈ a ∨ b = a by rw ← bootstrap.succ.membership; rw h; simp112  rcases aIn with hab | hab113  . rcases bIn with hba | hba114    . exfalso115      exact bootstrap.membership.asymmetric at a, b with hab, hba116    . cc117  . exact hab118