Grace/Cumulus/Nat/Distance.g17

Open in Workbench Download source

Imports

SubtractionLemmas · MinMax

Declarations

Source

1-- Distance between natural numbers2-- 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.Distance8import SubtractionLemmas9import MinMax1011def natDist (a b : Nat) : Nat := (a - b) + (b - a)1213theorem natDist.value (a b : Nat)14  shows natDist(a, b) = (a - b) + (b - a)15proof16  simp [natDist]1718theorem natDist.natural (a b : Nat)19  shows Nat(natDist(a, b))20proof21  have left := sub.closed at a, b22  have right := sub.closed at b, a23  rw natDist.value24  typecheck2526theorem natDist.commutative (a b : Nat)27  shows natDist(a, b) = natDist(b, a)28proof29  have left := sub.closed at a, b30  have right := sub.closed at b, a31  rw [natDist.value, natDist.value]32  ring3334theorem natDist.self (a : Nat)35  shows natDist(a, a) = 036proof37  rw [natDist.value, sub.self]38  ring3940theorem natDist.of_le (a b : Nat)41  requires below : a ≤ b42  shows natDist(a, b) = b - a43proof44  have zero := sub.eq_zero_of_le with below45  have right := sub.closed at b, a46  rw [natDist.value, zero]47  exact add.left_unit with *4849theorem natDist.of_ge (a b : Nat)50  requires above : b ≤ a51  shows natDist(a, b) = a - b52proof53  have zero := sub.eq_zero_of_le with above54  have left := sub.closed at a, b55  rw [natDist.value, zero]56  exact add.right_unit with *5758theorem natDist.zero_right (a : Nat)59  shows natDist(a, 0) = a60proof61  have zero : 0 ≤ a by linarith62  have value1 := natDist.of_ge with zero63  rw [value1, sub.zero_right]64  rfl6566theorem natDist.zero_left (a : Nat)67  shows natDist(0, a) = a68proof69  rw natDist.commutative70  exact natDist.zero_right with *7172theorem natDist.eq_zero_iff (a b : Nat)73  shows natDist(a, b) = 0 ↔ a = b74proof75  constructor76  . intro zero77    have left := sub.closed at a, b78    have right := sub.closed at b, a79    rw natDist.value at zero80    have both := add.eq_zero with zero81    have below := sub.eq_zero_iff.forward with both.left82    have above := sub.eq_zero_iff.forward with both.right83    exact LessEqual.antisymmetric with below, above84  . intro same85    rw same86    exact natDist.self with *8788theorem natDist.positive_iff (a b : Nat)89  shows 0 < natDist(a, b) ↔ a ≠ b90proof91  have distNat := natDist.natural at a, b92  constructor93  . intro positive94    intro same95    have zero := natDist.eq_zero_iff.backward with same96    rw zero at positive97    exact Less.irreflexive with positive98  . intro distinct99    have nonzero : natDist(a, b) ≠ 0100      intro zero101      have same := natDist.eq_zero_iff.forward with zero102      exact distinct with same103    exact Less.positive_of_ne_zero with nonzero104105theorem natDist.eq_iff (a b d : Nat)106  shows natDist(a, b) = d ↔ b = a + d ∨ a = b + d107proof108  constructor109  . intro same110    have total := LessEqual.total at a, b111    cases total with below | above112    . left113      have value := natDist.of_le with below114      rw value at same115      have cancel := sub.add_cancel_left with below116      rw [← cancel, same]117      rfl118    . right119      have value := natDist.of_ge with above120      rw value at same121      have cancel := sub.add_cancel_left with above122      rw [← cancel, same]123      rfl124  . intro split125    cases split with first | second126    . have below : a ≤ b by linarith127      have value2 := natDist.of_le with below128      rw [value2, first]129      exact sub.add_left with *130    . have above : b ≤ a by linarith131      have value3 := natDist.of_ge with above132      rw [value3, second]133      exact sub.add_left with *134135theorem natDist.add_left (a b k : Nat)136  shows natDist(k + a, k + b) = natDist(a, b)137proof138  have swapA := add.commutative at a, k with *139  have swapB := add.commutative at b, k with *140  rw [natDist.value, natDist.value, swapA, swapB, sub.add_add, sub.add_add]141  rfl142143theorem natDist.add_right (a b k : Nat)144  shows natDist(a + k, b + k) = natDist(a, b)145proof146  rw [natDist.value, natDist.value, sub.add_add, sub.add_add]147  rfl148149theorem natDist.add_one (a b : Nat)150  shows natDist(a + 1, b + 1) = natDist(a, b)151proof152  exact natDist.add_right at a, b, 1153154theorem natDist.mul_left (a b k : Nat)155  shows natDist(k * a, k * b) = k * natDist(a, b)156proof157  have left := sub.closed at a, b158  have right := sub.closed at b, a159  have first := sub.mul_left at a, b, k160  have second := sub.mul_left at b, a, k161  rw [natDist.value, natDist.value, ← first, ← second]162  ring163164theorem natDist.mul_right (a b k : Nat)165  shows natDist(a * k, b * k) = natDist(a, b) * k166proof167  have distNat := natDist.natural at a, b168  have swapA := mul.commutative at k, a with *169  have swapB := mul.commutative at k, b with *170  have swap := mul.commutative at k, natDist(a, b) with *171  rw [swapA, swapB, swap]172  exact natDist.mul_left with *173174theorem natDist.le_add (a b : Nat)175  shows natDist(a, b) ≤ a + b176proof177  have left := sub.le_self at a, b178  have right := sub.le_self at b, a179  have leftNat := sub.closed at a, b180  have rightNat := sub.closed at b, a181  rw natDist.value182  linarith183184theorem natDist.triangle (a b c : Nat)185  shows natDist(a, c) ≤ natDist(a, b) + natDist(b, c)186proof187  have ab := sub.closed at a, b188  have ba := sub.closed at b, a189  have bc := sub.closed at b, c190  have cb := sub.closed at c, b191  have ac := sub.closed at a, c192  have ca := sub.closed at c, a193  have reflexiveAB := LessEqual.reflexive at a - b194  have reflexiveBC := LessEqual.reflexive at b - c195  have reflexiveCB := LessEqual.reflexive at c - b196  have reflexiveBA := LessEqual.reflexive at b - a197  have boundA : a ≤ b + (a - b) := sub.le_iff.forward with reflexiveAB198  have boundB : b ≤ c + (b - c) := sub.le_iff.forward with reflexiveBC199  have boundC : c ≤ b + (c - b) := sub.le_iff.forward with reflexiveCB200  have boundB2 : b ≤ a + (b - a) := sub.le_iff.forward with reflexiveBA201  have forward : a - c ≤ (a - b) + (b - c)202    apply sub.le_iff.backward203    linarith204  have backward : c - a ≤ (c - b) + (b - a)205    apply sub.le_iff.backward206    linarith207  rw [natDist.value, natDist.value, natDist.value]208  linarith209210theorem natDist.max_sub_min (a b : Nat)211  shows natDist(a, b) = natMax(a, b) - natMin(a, b)212proof213  have total := LessEqual.total at a, b214  cases total with below | above215  . have minValue := natMin.of_le with below216    have maxValue := natMax.of_le with below217    have value4 := natDist.of_le with below218    rw [value4, minValue, maxValue]219    rfl220  . have minValue := natMin.of_ge with above221    have maxValue := natMax.of_ge with above222    have value5 := natDist.of_ge with above223    rw [value5, minValue, maxValue]224    rfl225226theorem natMin.add_natDist (a b : Nat)227  shows natMin(a, b) + natDist(a, b) = natMax(a, b)228proof229  have total := LessEqual.total at a, b230  cases total with below | above231  . have minValue := natMin.of_le with below232    have maxValue := natMax.of_le with below233    have value6 := natDist.of_le with below234    rw [value6, minValue, maxValue]235    exact sub.add_cancel_left with below236  . have minValue := natMin.of_ge with above237    have maxValue := natMax.of_ge with above238    have value7 := natDist.of_ge with above239    rw [value7, minValue, maxValue]240    exact sub.add_cancel_left with above241