Grace/Cumulus/Nat/SubtractionLemmas.g17

Open in Workbench Download source

Imports

Subtraction · OrderLemmas

Declarations

• predecessor.le theorem derivation
• predecessor.add_one theorem derivation
• predecessor.add_one_of_positive theorem derivation
• predecessor.Less_of_positive theorem derivation
• predecessor.monotone theorem derivation
• sub.add_left theorem derivation
• sub.self theorem derivation
• sub.of_add_eq theorem derivation
• sub.of_add_eq_left theorem derivation
• sub.add_cancel theorem derivation
• sub.add_cancel_left theorem derivation
• sub.sub theorem derivation
• sub.swap theorem derivation
• sub.eq_zero_of_le theorem derivation
• sub.positive_of_Less theorem derivation
• sub.eq_zero_iff theorem derivation
• sub.positive_iff theorem derivation
• sub.le_self theorem derivation
• sub.monotone_left theorem derivation
• sub.antitone_right theorem derivation
• sub.Less_self theorem derivation
• sub.add_one_of_le theorem derivation
• sub.add_sub_assoc theorem derivation
• sub.sub_cancel theorem derivation
• sub.add_add theorem derivation
• sub.add_one_both theorem derivation
• sub.add_one_right theorem derivation
• sub.le_iff theorem derivation
• sub.Less_iff theorem derivation
• sub.eq_iff_of_le theorem derivation
• sub.Less_monotone_left theorem derivation
• sub.mul_right theorem derivation
• sub.mul_left theorem derivation
• sub.le_of_le_add theorem derivation
• sub.injective_of_le theorem derivation
• mul.split_sub theorem derivation

Source

1-- Laws of truncated subtraction on the 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.SubtractionLemmas8import Subtraction9import OrderLemmas1011theorem predecessor.le (n : Nat)12  shows predecessor(n) ≤ n13proof14  have shape := natural.zero_or_successor at n15  cases shape with zero | successor16  . rw [zero, predecessor.zero]17    exact LessEqual.reflexive with *18  . obtain ⟨k, kNat, equation⟩ := successor19    rw [equation, predecessor.succ]20    exact LessEqual.successor with *2122theorem predecessor.add_one (n : Nat)23  shows predecessor(n + 1) = n24proof25  have shape := add.right_one at n26  rw shape27  exact predecessor.succ with *2829theorem predecessor.add_one_of_positive (n : Nat)30  requires positive : 0 < n31  shows predecessor(n) + 1 = n32proof33  have shape := natural.zero_or_successor at n34  cases shape with zero | successor35  . rw zero at positive36    exfalso37    exact Less.irreflexive with positive38  . obtain ⟨k, kNat, equation⟩ := successor39    rw [equation, predecessor.succ]40    exact add.right_one with *4142theorem predecessor.Less_of_positive (n : Nat)43  requires positive : 0 < n44  shows predecessor(n) < n45proof46  have predNat := predecessor.closed at n47  have shape := predecessor.add_one_of_positive with positive48  have bound : predecessor(n) < predecessor(n) + 1 by linarith49  rw shape at bound50  exact bound5152theorem predecessor.monotone (m n : Nat)53  requires below : m ≤ n54  shows predecessor(m) ≤ predecessor(n)55proof56  have shape := natural.zero_or_successor at m57  cases shape with zero | successor58  . rw [zero, predecessor.zero]59    have predNat := predecessor.closed at n60    linarith61  . obtain ⟨k, kNat, equation⟩ := successor62    rw equation at below63    have nShape := natural.zero_or_successor at n64    cases nShape with nZero | nSuccessor65    . rw nZero at below66      exfalso67      have impossible : succ(k) ≤ 0 := below68      have positive : 0 < succ(k) by linarith69      exact Less.not_LessEqual with positive, impossible70    . obtain ⟨j, jNat, nEquation⟩ := nSuccessor71      rw nEquation at below72      rw [equation, nEquation, predecessor.succ, predecessor.succ]73      have stepK : succ(k) = k + 1 by ring74      have stepJ : succ(j) = j + 1 by ring75      rw [stepK, stepJ] at below76      linarith7778theorem sub.add_left (m n : Nat)79  shows (n + m) - n = m80proof81  have swap := add.commutative at m, n with *82  rw swap83  exact sub.add_right with *8485theorem sub.self (n : Nat)86  shows n - n = 087proof88  have shape := sub.add_right at 0, n89  have unit := add.left_unit at n90  rw unit at shape91  exact shape9293theorem sub.of_add_eq (a b c : Nat)94  requires sum : a + b = c95  shows c - b = a96proof97  rw ← sum98  exact sub.add_right with *99100theorem sub.of_add_eq_left (a b c : Nat)101  requires sum : a + b = c102  shows c - a = b103proof104  rw ← sum105  exact sub.add_left with *106107theorem sub.add_cancel (a b : Nat)108  requires below : b ≤ a109  shows a - b + b = a110proof111  obtain ⟨k, kNat, equation⟩ := below112  have value := sub.of_add_eq_left with equation113  rw value114  have swap := add.commutative at b, k with *115  rw swap116  exact equation117118theorem sub.add_cancel_left (a b : Nat)119  requires below : b ≤ a120  shows b + (a - b) = a121proof122  have subNat := sub.closed at a, b123  have cancel := sub.add_cancel with below124  have swap := add.commutative at a - b, b with *125  rw swap126  exact cancel127128theorem sub.sub (a b c : Nat)129  shows a - (b + c) = (a - b) - c130proof131  induction c132  | zero =>133    have unit := add.right_unit at b134    rw unit135    have subNat := sub.closed at a, b136    rw sub.zero_right137    rfl138  | succ(k) using ih =>139    have shape := add.succ_right at k, b140    rw shape141    have subNat := sub.closed at a, b142    have innerNat := sub.closed at a, b + k143    rw [sub.succ_right, ih, sub.succ_right]144    rfl145146theorem sub.swap (a b c : Nat)147  shows (a - b) - c = (a - c) - b148proof149  have first := sub.sub at a, b, c150  have second := sub.sub at a, c, b151  have swap := add.commutative at c, b with *152  rw [← first, ← second, swap]153  rfl154155theorem sub.eq_zero_of_le (a b : Nat)156  requires below : a ≤ b157  shows a - b = 0158proof159  obtain ⟨k, kNat, equation⟩ := below160  rw [← equation, sub.sub, sub.self]161  exact sub.zero_left with *162163theorem sub.positive_of_Less (a b : Nat)164  requires below : a < b165  shows 0 < b - a166proof167  have peeled := sub.succ_of_Less at a with b, below168  have innerNat := sub.closed at b, succ(a)169  rw peeled170  have step : succ(b - succ(a)) = (b - succ(a)) + 1 by ring171  rw step172  linarith173174theorem sub.eq_zero_iff (a b : Nat)175  shows a - b = 0 ↔ a ≤ b176proof177  constructor178  . intro zero179    have split := Less.or_LessEqual at b, a180    cases split with above | below181    . have positive := sub.positive_of_Less with above182      rw zero at positive183      exfalso184      exact Less.irreflexive with positive185    . exact below186  . intro below187    exact sub.eq_zero_of_le with below188189theorem sub.positive_iff (a b : Nat)190  shows 0 < b - a ↔ a < b191proof192  have subNat := sub.closed at b, a193  constructor194  . intro positive195    have split := Less.or_LessEqual at a, b196    cases split with below | above197    . exact below198    . have zero := sub.eq_zero_of_le with above199      rw zero at positive200      exfalso201      exact Less.irreflexive with positive202  . intro below203    exact sub.positive_of_Less with below204205theorem sub.le_self (a b : Nat)206  shows a - b ≤ a207proof208  induction b209  | zero =>210    rw sub.zero_right211    exact LessEqual.reflexive with *212  | succ(k) using ih =>213    have subNat := sub.closed at a, k214    have pred := predecessor.le at a - k215    rw sub.succ_right216    exact LessEqual.transitive with pred, ih217218theorem sub.monotone_left (a b c : Nat)219  requires below : a ≤ b220  shows a - c ≤ b - c221proof222  induction c223  | zero =>224    rw [sub.zero_right, sub.zero_right]225    exact below226  | succ(k) using ih =>227    have leftNat := sub.closed at a, k228    have rightNat := sub.closed at b, k229    rw [sub.succ_right, sub.succ_right]230    exact predecessor.monotone with ih231232theorem sub.antitone_right (a b c : Nat)233  requires below : b ≤ c234  shows a - c ≤ a - b235proof236  obtain ⟨k, kNat, equation⟩ := below237  have subNat := sub.closed at a, b238  rw [← equation, sub.sub]239  exact sub.le_self with *240241theorem sub.Less_self (a b : Nat)242  requires aPositive : 0 < a243  requires bPositive : 0 < b244  shows a - b < a245proof246  have one : 1 ≤ b by linarith247  have bound := sub.antitone_right at a, 1, b with one248  have oneShape := sub.one at a249  rw oneShape at bound250  have pred := predecessor.Less_of_positive with aPositive251  exact LessEqual.transitive_Less with bound, pred252253theorem sub.add_one_of_le (a b : Nat)254  requires below : b ≤ a255  shows (a + 1) - b = (a - b) + 1256proof257  obtain ⟨k, kNat, equation⟩ := below258  have value := sub.of_add_eq_left with equation259  rw [value, ← equation]260  have shape : b + k + 1 = (k + 1) + b by ring261  rw shape262  exact sub.add_right with *263264theorem sub.add_sub_assoc (a b c : Nat)265  requires below : c ≤ b266  shows a + (b - c) = (a + b) - c267proof268  obtain ⟨k, kNat, equation⟩ := below269  have value := sub.of_add_eq_left with equation270  rw [value, ← equation]271  have shape : a + (c + k) = (a + k) + c by ring272  rw shape273  symm274  exact sub.add_right with *275276theorem sub.sub_cancel (a b : Nat)277  requires below : b ≤ a278  shows a - (a - b) = b279proof280  obtain ⟨k, kNat, equation⟩ := below281  have value := sub.of_add_eq_left with equation282  rw [value, ← equation]283  exact sub.add_right with *284285theorem sub.add_add (a b c : Nat)286  shows (a + c) - (b + c) = a - b287proof288  have swap := add.commutative at c, b with *289  rw [swap, sub.sub]290  have cancel := sub.add_right at a, c291  rw cancel292  rfl293294theorem sub.add_one_both (a b : Nat)295  shows (a + 1) - (b + 1) = a - b296proof297  exact sub.add_add at a, b, 1298299theorem sub.add_one_right (n : Nat)300  shows (n + 1) - 1 = n301proof302  exact sub.add_right at n, 1303304theorem sub.le_iff (a b c : Nat)305  shows a - b ≤ c ↔ a ≤ b + c306proof307  have subNat := sub.closed at a, b308  constructor309  . intro below310    have split := LessEqual.total at b, a311    cases split with first | second312    . have cancel := sub.add_cancel_left with first313      rw ← cancel314      linarith315    . linarith316  . intro below317    have shifted := sub.monotone_left at a, b + c, b with below318    have cancel := sub.add_left at c, b319    rw cancel at shifted320    exact shifted321322theorem sub.Less_iff (a b c : Nat)323  requires below : b ≤ a324  shows a - b < c ↔ a < b + c325proof326  have subNat := sub.closed at a, b327  have cancel := sub.add_cancel_left with below328  constructor329  . intro strict330    rw ← cancel331    linarith332  . intro strict333    rw ← cancel at strict334    linarith335336theorem sub.eq_iff_of_le (a b c : Nat)337  requires below : b ≤ a338  shows a - b = c ↔ a = b + c339proof340  have subNat := sub.closed at a, b341  have cancel := sub.add_cancel_left with below342  constructor343  . intro same344    rw ← same345    symm346    exact cancel347  . intro same348    rw same349    exact sub.add_left with *350351theorem sub.Less_monotone_left (a b c : Nat)352  requires below : c ≤ a353  requires strict : a < b354  shows a - c < b - c355proof356  have leftNat := sub.closed at a, c357  have rightNat := sub.closed at b, c358  have weak : c ≤ b by linarith359  have leftCancel := sub.add_cancel_left with below360  have rightCancel := sub.add_cancel_left at b, c with weak361  rw [← leftCancel, ← rightCancel] at strict362  linarith363364theorem sub.mul_right (a b c : Nat)365  shows (a - b) * c = a * c - b * c366proof367  have split := LessEqual.total at b, a368  cases split with below | above369  . obtain ⟨k, kNat, equation⟩ := below370    have value := sub.of_add_eq_left with equation371    rw [value, ← equation]372    have shape : (b + k) * c = b * c + k * c by ring373    rw shape374    symm375    exact sub.add_left with *376  . have zero := sub.eq_zero_of_le with above377    have scaled := LessEqual.mul_right at a, b, c with above378    have productZero := sub.eq_zero_of_le with scaled379    rw [zero, productZero]380    exact mul.left_zero with *381382theorem sub.mul_left (a b c : Nat)383  shows c * (a - b) = c * a - c * b384proof385  have subNat := sub.closed at a, b386  have swap := mul.commutative at a - b, c with *387  have swapA := mul.commutative at a, c with *388  have swapB := mul.commutative at b, c with *389  rw [swap, swapA, swapB]390  exact sub.mul_right with *391392theorem sub.le_of_le_add (a b c : Nat)393  requires below : a ≤ b + c394  shows a - c ≤ b395proof396  have shifted := sub.monotone_left at a, b + c, c with below397  have cancel := sub.add_right at b, c398  rw cancel at shifted399  exact shifted400401theorem sub.injective_of_le (a b c : Nat)402  requires first : c ≤ a403  requires second : c ≤ b404  requires same : a - c = b - c405  shows a = b406proof407  have leftCancel := sub.add_cancel_left with first408  have rightCancel := sub.add_cancel_left at b, c with second409  rw [← leftCancel, ← rightCancel, same]410  rfl411412-- A product splits along a subtraction of the first factor.413theorem mul.split_sub (p q C : Nat)414  requires le : q ≤ p415  shows p * C = (p - q) * C + q * C416proof417  have pieces := sub.add_cancel with le418  have difference := sub.closed at p, q419  have expanded : (p - q + q) * C = (p - q) * C + q * C by ring420  rw pieces at expanded421  exact expanded422