Grace/Cumulus/Real/Natural.g17

Open in Workbench Download source

Imports

Ring · Algebra.Ring.Numeral

Declarations

• realNat def
• realNat.zero theorem derivation
• realNat.succ theorem derivation
• realNat.real theorem derivation
• realNat.one theorem derivation
• realNat.numeral theorem derivation
• realNumeral def
• realNumeral.nat theorem derivation
• realNumeral.real theorem derivation
• realNumeral.numeral theorem derivation
• realNumeral.zero theorem derivation
• realNumeral.succ theorem derivation
• realNat.add theorem derivation
• realNat.mul theorem derivation
• realNat.zero_le theorem derivation
• realNat.positive_succ theorem derivation
• realNat.positive theorem derivation
• realNat.le_of_natural_le theorem derivation
• realNat.ne_zero theorem derivation

Source

1-- Natural numbers as reals: the embedding, its numerals, and its order2-- 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.Real.Natural8import Ring9import Algebra.Ring.Numeral1011def realNat (n : Nat) → Set12  | zero => realZero13  | succ(k) => realAddValue(realNat(k), realOne)1415theorem realNat.zero16  shows realNat(0) = (0:R)17proof18  simp1920theorem realNat.succ (n : Nat)21  shows realNat(succ(n)) = realAddValue(realNat(n), realOne)22proof23  rw realNat24  rfl2526theorem realNat.real (n : Nat)27  shows Real(realNat(n))28proof29  induction n30  | zero =>31    rw realNat32    exact realZero.real33  | succ(k) using ih =>34    rw realNat35    have typed := realAddValue.real with ih, realOne.real36    unfold call2 at typed37    unfold realAddValue38    exact typed3940theorem realNat.one41  shows realNat(1) = (1:R)42proof43  rw [realNat.succ, realNat.zero]44  have zero := realAddValue.zero_left with realOne.real45  unfold call2 at zero46  unfold realAddValue47  exact zero4849theorem realNat.numeral (n : Nat)50  shows realNat(n) = ringNat(realAdd, realZero, realOne, n)51proof52  induction n53  | zero =>54    rw [realNat.zero, ringNat.zero]55    rfl56  | succ(k) using ih =>57    rw [realNat.succ, ringNat.succ, ih]58    unfold realAddValue59    unfold call260    rfl6162-- The real numeral: every literal above one elaborates to realNumeral(n), a63-- name of its own so that rewriting zero, one, or realNat leaves numerals64-- intact. The bridge to ringNat lets ring read it as the n-fold sum of one.65def realNumeral (n : Nat) : Set := realNat(n)6667theorem realNumeral.nat (n : Nat)68  shows realNumeral(n) = realNat(n)69proof70  unfold realNumeral71  rfl7273theorem realNumeral.real (n : Nat)74  shows Real(realNumeral(n))75proof76  rw realNumeral.nat77  exact realNat.real7879theorem realNumeral.numeral (n : Nat)80  shows realNumeral(n) = ringNat(realAdd, realZero, realOne, n)81proof82  rw [realNumeral.nat, realNat.numeral]83  rfl8485notation numeral _ => realNumeral(_) for Real8687-- A natural number in a real position, an operand of a real operation or88-- comparison or one side of a real equation, is read as realNat(n) and89-- prints without the cast: n! * X is realNat(n!) * X.90notation coercion realNat for Nat, Real9192theorem realNumeral.zero93  shows (0:R) = realZero94proof95  rfl9697theorem realNumeral.succ (k : Nat)98  shows realNumeral(succ(k)) = realNumeral(k) + (1:R)99proof100  rw [realNumeral.numeral, ringNat.succ, realNumeral.numeral]101  rfl102103theorem realNat.add (m n : Nat)104  shows realNat(add(m, n)) = (realNat(m):R) + (realNat(n):R)105proof106  induction m107  | zero =>108    rw [add, realNat.zero]109    ring110  | succ(k) using ih =>111    rw [add, realNat.succ, ih, realNat.succ]112    ring113114theorem realNat.mul (m n : Nat)115  shows realNat(mul(m, n)) = (realNat(m):R) * (realNat(n):R)116proof117  induction m118  | zero =>119    rw [mul, realNat.zero]120    ring121  | succ(k) using ih =>122    rw [mul, realNat.add, ih, realNat.succ]123    ring124125-- Natural numbers embedded in the reals are nonnegative, and positive126-- above zero.127theorem realNat.zero_le (n : Nat)128  shows (0:R) ≤ (realNat(n):R)129proof130  induction n131  | zero =>132    rw realNat.zero133    exact realLe.reflexive with realZero.real134  | succ(k) using ih =>135    have natural := realNat.real at k136    rw realNat.succ137    linarith138139theorem realNat.positive_succ (n : Nat)140  shows (0:R) < (realNat(succ(n)):R)141proof142  have natural := realNat.real at n143  have nonnegative := realNat.zero_le at n144  rw realNat.succ145  linarith146147theorem realNat.positive (n : Nat)148  requires nonzero : n ≠ 0149  shows (0:R) < (realNat(n):R)150proof151  have alternatives := natural.zero_or_successor at n152  cases alternatives with zero | successor153  . exfalso154    exact nonzero with zero155  . obtain ⟨k, natural, shape⟩ := successor156    rw shape157    exact realNat.positive_succ at k158159theorem realNat.le_of_natural_le (m n : Nat)160  requires le : m ≤ n161  shows (realNat(m):R) ≤ (realNat(n):R)162proof163  obtain ⟨d, natural, split⟩ := le164  have naturalM := realNat.real at m165  have naturalD := realNat.real at d166  have nonnegative := realNat.zero_le at d167  have sum := realNat.add at m, d168  rw split at sum169  rw sum170  linarith171172theorem realNat.ne_zero (n : Nat)173  requires nonzero : n ≠ 0174  shows (realNat(n):R) ≠ 0175proof176  have positive := realNat.positive with nonzero177  intro zero178  rw zero at positive179  linarith180