Grace/Cumulus/Int/Embedding.g17

Open in Workbench Download source

Imports

MinMax · Nat.Distance

Declarations

• integerOfNat.one theorem derivation
• integerOfNat.add_one theorem derivation
• integerOfNat.injective_iff theorem derivation
• integerOfNat.eq_zero_iff theorem derivation
• integerOfNat.positive_iff theorem derivation
• integerClass.difference theorem derivation
• integerNegativeOfNat.eq_neg theorem derivation
• integerNegativeOfNat.add theorem derivation
• integerNegativeOfNat.le_iff theorem derivation
• integerOfNat.sub theorem derivation
• integerOfNat.sub_of_le theorem derivation
• integerNatAbs.ofNat_sub theorem derivation
• integerAbs.ofNat_sub theorem derivation
• integerOfNat.natMin theorem derivation
• integerOfNat.natMax theorem derivation
• integerOfNat.monotone theorem derivation
• integerOfNat.strict_monotone theorem derivation
• integerNatAbs.le_of_le theorem derivation

Source

1-- The embedding of the natural numbers in the integers: order, subtraction,2-- distance, minimum, and maximum3-- Part of Cumulus, the Grace17 mathematics library.4-- Copyright (c) 2026 Grant Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78module Grace.Cumulus.Int.Embedding9import MinMax10import Nat.Distance1112theorem integerOfNat.one13  shows integerOfNat(1) = integerOne14proof15  unfold integerOne16  rfl1718theorem integerOfNat.add_one (n : Nat)19  shows integerOfNat(n + 1) = integerOfNat(n) + 120proof21  have sum := integerOfNat.add at n, 122  rw [sum, integerOfNat.one]23  rfl2425theorem integerOfNat.injective_iff (a b : Nat)26  shows integerOfNat(a) = integerOfNat(b) ↔ a = b27proof28  constructor29  . intro same30    exact integerOfNat.injective with same31  . intro same32    rw same33    rfl3435theorem integerOfNat.eq_zero_iff (n : Nat)36  shows integerOfNat(n) = integerZero ↔ n = 037proof38  rw ← integerOfNat.zero39  exact integerOfNat.injective_iff at n, 04041theorem integerOfNat.positive_iff (n : Nat)42  shows integerZero < integerOfNat(n) ↔ 0 < n43proof44  rw ← integerOfNat.zero45  exact integerLess.ofNat_iff at 0, n4647theorem integerClass.difference (a b : Nat)48  shows integerClass(a, b) = integerOfNat(a) - integerOfNat(b)49proof50  have negated := integerOfNat.neg at b51  have shape : integerOfNat(a) - integerOfNat(b) =52      integerOfNat(a) + (-integerOfNat(b))53    ring54  rw [shape, negated]55  unfold integerOfNat56  unfold integerNegativeOfNat57  rw integerAddValue.classes58  unfold integerClassSum59  have left := add.right_unit at a60  have right := add.left_unit at b61  rw [left, right]62  rfl6364theorem integerNegativeOfNat.eq_neg (n : Nat)65  shows integerNegativeOfNat(n) = -integerOfNat(n)66proof67  symm68  exact integerOfNat.neg with *6970theorem integerNegativeOfNat.add (a b : Nat)71  shows72    integerNegativeOfNat(a + b) =73      integerNegativeOfNat(a) + integerNegativeOfNat(b)74proof75  have sum := integerOfNat.add at a, b76  rw [integerNegativeOfNat.eq_neg, integerNegativeOfNat.eq_neg]77  rw [integerNegativeOfNat.eq_neg, sum]78  ring7980theorem integerNegativeOfNat.le_iff (a b : Nat)81  shows integerNegativeOfNat(a) ≤ integerNegativeOfNat(b) ↔ b ≤ a82proof83  have flipped := integerLe.neg at integerOfNat(b), integerOfNat(a)84  have bridge := integerLe.ofNat_iff at b, a85  rw [integerNegativeOfNat.eq_neg, integerNegativeOfNat.eq_neg]86  constructor87  . intro below88    have lifted := flipped.backward with below89    exact bridge.forward with lifted90  . intro below91    have lifted := bridge.backward with below92    exact flipped.forward with lifted9394theorem integerOfNat.sub (a b : Nat)95  requires below : b ≤ a96  shows integerOfNat(a - b) = integerOfNat(a) - integerOfNat(b)97proof98  have subNat := sub.closed at a, b99  have cancel := sub.add_cancel with below100  have sum := integerOfNat.add at a - b, b101  rw [← cancel, sum]102  have restore : (a - b) + b - b = a - b by arith103  rw restore104  ring105106theorem integerOfNat.sub_of_le (a b : Nat)107  requires below : a ≤ b108  shows integerOfNat(a) - integerOfNat(b) = integerNegativeOfNat(b - a)109proof110  have lifted := integerOfNat.sub at b, a with below111  rw [integerNegativeOfNat.eq_neg, lifted]112  ring113114theorem integerNatAbs.ofNat_sub (a b : Nat)115  shows integerNatAbs(integerOfNat(a) - integerOfNat(b)) = natDist(a, b)116proof117  have total := LessEqual.total at b, a118  cases total with below | above119  . have lifted := integerOfNat.sub with below120    have subNat := sub.closed at a, b121    have value := natDist.of_ge with below122    rw [← lifted, integerNatAbs.ofNat, value]123    rfl124  . have lifted := integerOfNat.sub_of_le with above125    have subNat := sub.closed at b, a126    have value := natDist.of_le with above127    rw [lifted, integerNatAbs.ofNegativeNat, value]128    rfl129130theorem integerAbs.ofNat_sub (a b : Nat)131  shows132    integerAbs(integerOfNat(a) - integerOfNat(b)) = integerOfNat(natDist(a, b))133proof134  have difference := integerSubValue.integer at integerOfNat(a), integerOfNat(b)135  rw [integerAbs.value, integerNatAbs.ofNat_sub]136  rfl137138theorem integerOfNat.natMin (a b : Nat)139  shows140    integerOfNat(natMin(a, b)) = integerMin(integerOfNat(a), integerOfNat(b))141proof142  have total := LessEqual.total at a, b143  cases total with below | above144  . have lifted := integerLe.ofNat_iff.backward with below145    have left := natMin.of_le with below146    have right := integerMin.of_le with lifted147    rw [left, right]148    rfl149  . have lifted := integerLe.ofNat_iff.backward with above150    have left := natMin.of_ge with above151    have right := integerMin.of_ge with lifted152    rw [left, right]153    rfl154155theorem integerOfNat.natMax (a b : Nat)156  shows157    integerOfNat(natMax(a, b)) = integerMax(integerOfNat(a), integerOfNat(b))158proof159  have total := LessEqual.total at a, b160  cases total with below | above161  . have lifted := integerLe.ofNat_iff.backward with below162    have left := natMax.of_le with below163    have right := integerMax.of_le with lifted164    rw [left, right]165    rfl166  . have lifted := integerLe.ofNat_iff.backward with above167    have left := natMax.of_ge with above168    have right := integerMax.of_ge with lifted169    rw [left, right]170    rfl171172theorem integerOfNat.monotone (a b : Nat)173  requires below : a ≤ b174  shows integerOfNat(a) ≤ integerOfNat(b)175proof176  exact integerLe.ofNat_iff.backward with below177178theorem integerOfNat.strict_monotone (a b : Nat)179  requires below : a < b180  shows integerOfNat(a) < integerOfNat(b)181proof182  exact integerLess.ofNat_iff.backward with below183184theorem integerNatAbs.le_of_le (x y : Integer)185  requires nonnegative : 0 ≤ x186  requires below : x ≤ y187  shows integerNatAbs(x) ≤ integerNatAbs(y)188proof189  have xNat := integerNatAbs.natural at x190  have yNat := integerNatAbs.natural at y191  have bound := integerAbs.monotone_nonneg with nonnegative, below192  rw [integerAbs.value, integerAbs.value] at bound193  exact integerLe.ofNat_iff.forward with bound194