Grace/Cumulus/Nat/MinMax.g17

Open in Workbench Download source

Imports

OrderLemmas

Declarations

Source

1-- Minimum and maximum of two 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.MinMax8import OrderLemmas910defunique natMin (a b : Nat) (m ∈ ℕ) :=11  (a ≤ b ∧ m = a) ∨ (b < a ∧ m = b)12proof13  have split := Less.or_LessEqual at b, a14  cases split with above | below15  . refine ⟨b, nat.omega.forward at b with *, ?_⟩16    right17    exact ⟨above, rfl⟩18  . refine ⟨a, nat.omega.forward at a with *, ?_⟩19    left20    exact ⟨below, rfl⟩2122uniqueness23  intros m mMember first n nMember second24  cases first with firstLow | firstHigh25  . cases second with secondLow | secondHigh26    . cc27    . exfalso28      exact LessEqual.not_Less with firstLow.left, secondHigh.left29  . cases second with secondLow | secondHigh30    . exfalso31      exact LessEqual.not_Less with secondLow.left, firstHigh.left32    . cc3334defunique natMax (a b : Nat) (m ∈ ℕ) :=35  (a ≤ b ∧ m = b) ∨ (b < a ∧ m = a)36proof37  have split := Less.or_LessEqual at b, a38  cases split with above | below39  . refine ⟨a, nat.omega.forward at a with *, ?_⟩40    right41    exact ⟨above, rfl⟩42  . refine ⟨b, nat.omega.forward at b with *, ?_⟩43    left44    exact ⟨below, rfl⟩4546uniqueness47  intros m mMember first n nMember second48  cases first with firstLow | firstHigh49  . cases second with secondLow | secondHigh50    . cc51    . exfalso52      exact LessEqual.not_Less with firstLow.left, secondHigh.left53  . cases second with secondLow | secondHigh54    . exfalso55      exact LessEqual.not_Less with secondLow.left, firstHigh.left56    . cc5758theorem natMin.natural (a b : Nat)59  shows Nat(natMin(a, b))60proof61  have selected := natMin.selected at a, b with *62  exact nat.omega.backward with selected.left6364theorem natMax.natural (a b : Nat)65  shows Nat(natMax(a, b))66proof67  have selected := natMax.selected at a, b with *68  exact nat.omega.backward with selected.left6970theorem natMin.of_le (a b : Nat)71  requires below : a ≤ b72  shows natMin(a, b) = a73proof74  have selected := natMin.selected at a, b with *75  rcases selected with ⟨member, property⟩76  cases property with low | high77  . exact low.right78  . exfalso79    exact LessEqual.not_Less with below, high.left8081theorem natMin.of_ge (a b : Nat)82  requires above : b ≤ a83  shows natMin(a, b) = b84proof85  have selected := natMin.selected at a, b with *86  rcases selected with ⟨member, property⟩87  cases property with low | high88  . have same := LessEqual.antisymmetric with low.left, above89    rw low.right90    exact same91  . exact high.right9293theorem natMax.of_le (a b : Nat)94  requires below : a ≤ b95  shows natMax(a, b) = b96proof97  have selected := natMax.selected at a, b with *98  rcases selected with ⟨member, property⟩99  cases property with low | high100  . exact low.right101  . exfalso102    exact LessEqual.not_Less with below, high.left103104theorem natMax.of_ge (a b : Nat)105  requires above : b ≤ a106  shows natMax(a, b) = a107proof108  have selected := natMax.selected at a, b with *109  rcases selected with ⟨member, property⟩110  cases property with low | high111  . have same := LessEqual.antisymmetric with low.left, above112    rw low.right113    symm114    exact same115  . exact high.right116117theorem natMin.self (a : Nat)118  shows natMin(a, a) = a119proof120  exact natMin.of_le with (LessEqual.reflexive at a)121122theorem natMax.self (a : Nat)123  shows natMax(a, a) = a124proof125  exact natMax.of_le with (LessEqual.reflexive at a)126127theorem natMin.commutative (a b : Nat)128  shows natMin(a, b) = natMin(b, a)129proof130  have total := LessEqual.total at a, b131  cases total with below | above132  . have left := natMin.of_le with below133    have right := natMin.of_ge at b, a with below134    rw [left, right]135    rfl136  . have left := natMin.of_ge with above137    have right := natMin.of_le at b, a with above138    rw [left, right]139    rfl140141theorem natMax.commutative (a b : Nat)142  shows natMax(a, b) = natMax(b, a)143proof144  have total := LessEqual.total at a, b145  cases total with below | above146  . have left := natMax.of_le with below147    have right := natMax.of_ge at b, a with below148    rw [left, right]149    rfl150  . have left := natMax.of_ge with above151    have right := natMax.of_le at b, a with above152    rw [left, right]153    rfl154155theorem natMin.cases (a b : Nat)156  shows natMin(a, b) = a ∨ natMin(a, b) = b157proof158  have total := LessEqual.total at a, b159  cases total with below | above160  . left161    exact natMin.of_le with below162  . right163    exact natMin.of_ge with above164165theorem natMax.cases (a b : Nat)166  shows natMax(a, b) = a ∨ natMax(a, b) = b167proof168  have total := LessEqual.total at a, b169  cases total with below | above170  . right171    exact natMax.of_le with below172  . left173    exact natMax.of_ge with above174175theorem natMin.le_left (a b : Nat)176  shows natMin(a, b) ≤ a177proof178  have total := LessEqual.total at a, b179  cases total with below | above180  . have value101 := natMin.of_le with below181    rw value101182    exact LessEqual.reflexive with *183  . have value102 := natMin.of_ge with above184    rw value102185    exact above186187theorem natMin.le_right (a b : Nat)188  shows natMin(a, b) ≤ b189proof190  have total := LessEqual.total at a, b191  cases total with below | above192  . have value103 := natMin.of_le with below193    rw value103194    exact below195  . have value104 := natMin.of_ge with above196    rw value104197    exact LessEqual.reflexive with *198199theorem natMax.ge_left (a b : Nat)200  shows a ≤ natMax(a, b)201proof202  have total := LessEqual.total at a, b203  cases total with below | above204  . have value105 := natMax.of_le with below205    rw value105206    exact below207  . have value106 := natMax.of_ge with above208    rw value106209    exact LessEqual.reflexive with *210211theorem natMax.ge_right (a b : Nat)212  shows b ≤ natMax(a, b)213proof214  have total := LessEqual.total at a, b215  cases total with below | above216  . have value107 := natMax.of_le with below217    rw value107218    exact LessEqual.reflexive with *219  . have value108 := natMax.of_ge with above220    rw value108221    exact above222223theorem natMin.le_natMax (a b : Nat)224  shows natMin(a, b) ≤ natMax(a, b)225proof226  have low := natMin.le_left at a, b227  have high := natMax.ge_left at a, b228  exact LessEqual.transitive with low, high229230theorem natMin.le_iff (a b c : Nat)231  shows c ≤ natMin(a, b) ↔ c ≤ a ∧ c ≤ b232proof233  have minNat := natMin.natural at a, b234  have low := natMin.le_left at a, b235  have high := natMin.le_right at a, b236  constructor237  . intro below238    constructor239    . exact LessEqual.transitive with below, low240    . exact LessEqual.transitive with below, high241  . intro both242    have total := LessEqual.total at a, b243    cases total with first | second244    . have value109 := natMin.of_le with first245      rw value109246      exact both.left247    . have value110 := natMin.of_ge with second248      rw value110249      exact both.right250251theorem natMin.le_iff_or (a b c : Nat)252  shows natMin(a, b) ≤ c ↔ a ≤ c ∨ b ≤ c253proof254  have minNat := natMin.natural at a, b255  constructor256  . intro below257    have split := natMin.cases at a, b258    cases split with first | second259    . left260      rw ← first261      exact below262    . right263      rw ← second264      exact below265  . intro split266    cases split with first | second267    . have low := natMin.le_left at a, b268      exact LessEqual.transitive with low, first269    . have high := natMin.le_right at a, b270      exact LessEqual.transitive with high, second271272theorem natMax.le_iff (a b c : Nat)273  shows natMax(a, b) ≤ c ↔ a ≤ c ∧ b ≤ c274proof275  have maxNat := natMax.natural at a, b276  have low := natMax.ge_left at a, b277  have high := natMax.ge_right at a, b278  constructor279  . intro below280    constructor281    . exact LessEqual.transitive with low, below282    . exact LessEqual.transitive with high, below283  . intro both284    have total := LessEqual.total at a, b285    cases total with first | second286    . have value111 := natMax.of_le with first287      rw value111288      exact both.right289    . have value112 := natMax.of_ge with second290      rw value112291      exact both.left292293theorem natMax.ge_iff_or (a b c : Nat)294  shows c ≤ natMax(a, b) ↔ c ≤ a ∨ c ≤ b295proof296  have maxNat := natMax.natural at a, b297  constructor298  . intro below299    have split := natMax.cases at a, b300    cases split with first | second301    . left302      rw ← first303      exact below304    . right305      rw ← second306      exact below307  . intro split308    cases split with first | second309    . have low := natMax.ge_left at a, b310      exact LessEqual.transitive with first, low311    . have high := natMax.ge_right at a, b312      exact LessEqual.transitive with second, high313314theorem natMin.lt_iff (a b c : Nat)315  shows c < natMin(a, b) ↔ c < a ∧ c < b316proof317  have minNat := natMin.natural at a, b318  have low := natMin.le_left at a, b319  have high := natMin.le_right at a, b320  constructor321  . intro below322    constructor323    . exact Less.transitive_LessEqual with below, low324    . exact Less.transitive_LessEqual with below, high325  . intro both326    have total := LessEqual.total at a, b327    cases total with first | second328    . have value113 := natMin.of_le with first329      rw value113330      exact both.left331    . have value114 := natMin.of_ge with second332      rw value114333      exact both.right334335theorem natMax.lt_iff (a b c : Nat)336  shows natMax(a, b) < c ↔ a < c ∧ b < c337proof338  have maxNat := natMax.natural at a, b339  have low := natMax.ge_left at a, b340  have high := natMax.ge_right at a, b341  constructor342  . intro below343    constructor344    . exact LessEqual.transitive_Less with low, below345    . exact LessEqual.transitive_Less with high, below346  . intro both347    have total := LessEqual.total at a, b348    cases total with first | second349    . have value115 := natMax.of_le with first350      rw value115351      exact both.right352    . have value116 := natMax.of_ge with second353      rw value116354      exact both.left355356theorem natMin.eq_left_iff (a b : Nat)357  shows natMin(a, b) = a ↔ a ≤ b358proof359  constructor360  . intro same361    have high := natMin.le_right at a, b362    rw same at high363    exact high364  . intro below365    exact natMin.of_le with below366367theorem natMin.eq_right_iff (a b : Nat)368  shows natMin(a, b) = b ↔ b ≤ a369proof370  constructor371  . intro same372    have low := natMin.le_left at a, b373    rw same at low374    exact low375  . intro above376    exact natMin.of_ge with above377378theorem natMax.eq_left_iff (a b : Nat)379  shows natMax(a, b) = a ↔ b ≤ a380proof381  constructor382  . intro same383    have high := natMax.ge_right at a, b384    rw same at high385    exact high386  . intro above387    exact natMax.of_ge with above388389theorem natMax.eq_right_iff (a b : Nat)390  shows natMax(a, b) = b ↔ a ≤ b391proof392  constructor393  . intro same394    have low := natMax.ge_left at a, b395    rw same at low396    exact low397  . intro below398    exact natMax.of_le with below399400theorem natMin.zero_left (a : Nat)401  shows natMin(0, a) = 0402proof403  have zero : 0 ≤ a by linarith404  exact natMin.of_le with zero405406theorem natMin.zero_right (a : Nat)407  shows natMin(a, 0) = 0408proof409  have zero : 0 ≤ a by linarith410  exact natMin.of_ge with zero411412theorem natMax.zero_left (a : Nat)413  shows natMax(0, a) = a414proof415  have zero : 0 ≤ a by linarith416  exact natMax.of_le with zero417418theorem natMax.zero_right (a : Nat)419  shows natMax(a, 0) = a420proof421  have zero : 0 ≤ a by linarith422  exact natMax.of_ge with zero423424theorem natMin.eq_zero_iff (a b : Nat)425  shows natMin(a, b) = 0 ↔ a = 0 ∨ b = 0426proof427  constructor428  . intro zero429    have split := natMin.cases at a, b430    cases split with first | second431    . left432      rw ← first433      exact zero434    . right435      rw ← second436      exact zero437  . intro split438    cases split with first | second439    . rw first440      exact natMin.zero_left with *441    . rw second442      exact natMin.zero_right with *443444theorem natMax.eq_zero_iff (a b : Nat)445  shows natMax(a, b) = 0 ↔ a = 0 ∧ b = 0446proof447  constructor448  . intro zero449    have low := natMax.ge_left at a, b450    have high := natMax.ge_right at a, b451    rw zero at low452    rw zero at high453    constructor454    . exact LessEqual.eq_zero with low455    . exact LessEqual.eq_zero with high456  . intro both457    rw [both.left, both.right]458    exact natMax.self with *459460theorem natMin.monotone (a b c d : Nat)461  requires first : a ≤ c462  requires second : b ≤ d463  shows natMin(a, b) ≤ natMin(c, d)464proof465  have low := natMin.le_left at a, b466  have high := natMin.le_right at a, b467  apply natMin.le_iff.backward468  constructor469  . exact LessEqual.transitive with low, first470  . exact LessEqual.transitive with high, second471472theorem natMax.monotone (a b c d : Nat)473  requires first : a ≤ c474  requires second : b ≤ d475  shows natMax(a, b) ≤ natMax(c, d)476proof477  have low := natMax.ge_left at c, d478  have high := natMax.ge_right at c, d479  apply natMax.le_iff.backward480  constructor481  . exact LessEqual.transitive with first, low482  . exact LessEqual.transitive with second, high483484theorem natMin.associative (a b c : Nat)485  shows natMin(natMin(a, b), c) = natMin(a, natMin(b, c))486proof487  have innerLeft := natMin.natural at a, b488  have innerRight := natMin.natural at b, c489  have total := LessEqual.total at a, b490  cases total with below | above491  . have value117 := natMin.of_le with below492    rw value117493    have totalAC := LessEqual.total at a, c494    cases totalAC with belowAC | aboveAC495    . have bound : a ≤ natMin(b, c)496        exact natMin.le_iff.backward with ⟨below, belowAC⟩497      have value1 := natMin.of_le with belowAC498      have value2 := natMin.of_le with bound499      rw [value1, value2]500      rfl501    . have bound : natMin(b, c) ≤ a502        have inner := natMin.le_right at b, c503        exact LessEqual.transitive with inner, aboveAC504      have value3 := natMin.of_ge with aboveAC505      have value4 := natMin.of_ge with bound506      rw [value3, value4]507      have totalBC := LessEqual.total at b, c508      cases totalBC with belowBC | aboveBC509      . have value118 := natMin.of_le with belowBC510        rw value118511        have bound2 : c ≤ b := LessEqual.transitive with aboveAC, below512        exact LessEqual.antisymmetric with bound2, belowBC513      . have value119 := natMin.of_ge with aboveBC514        rw value119515        rfl516  . have value120 := natMin.of_ge with above517    rw value120518    have totalBC := LessEqual.total at b, c519    cases totalBC with belowBC | aboveBC520    . have value121 := natMin.of_le with belowBC521      rw value121522      have value5 := natMin.of_ge with above523      rw value5524      rfl525    . have value122 := natMin.of_ge with aboveBC526      rw value122527      have bound : c ≤ a := LessEqual.transitive with aboveBC, above528      have value6 := natMin.of_ge with bound529      rw value6530      rfl531532theorem natMax.associative (a b c : Nat)533  shows natMax(natMax(a, b), c) = natMax(a, natMax(b, c))534proof535  have innerLeft := natMax.natural at a, b536  have innerRight := natMax.natural at b, c537  have total := LessEqual.total at a, b538  cases total with below | above539  . have value123 := natMax.of_le with below540    rw value123541    have totalBC := LessEqual.total at b, c542    cases totalBC with belowBC | aboveBC543    . have value124 := natMax.of_le with belowBC544      rw value124545      have bound : a ≤ c := LessEqual.transitive with below, belowBC546      have value7 := natMax.of_le with bound547      rw value7548      rfl549    . have value125 := natMax.of_ge with aboveBC550      rw value125551      have value8 := natMax.of_le with below552      rw value8553      rfl554  . have value126 := natMax.of_ge with above555    rw value126556    have totalAC := LessEqual.total at a, c557    cases totalAC with belowAC | aboveAC558    . have bound : a ≤ natMax(b, c)559        have inner := natMax.ge_right at b, c560        exact LessEqual.transitive with belowAC, inner561      have value9 := natMax.of_le with belowAC562      have value10 := natMax.of_le with bound563      rw [value9, value10]564      have totalBC := LessEqual.total at b, c565      cases totalBC with belowBC | aboveBC566      . have value127 := natMax.of_le with belowBC567        rw value127568        rfl569      . have value128 := natMax.of_ge with aboveBC570        rw value128571        have bound2 : b ≤ c := LessEqual.transitive with above, belowAC572        exact LessEqual.antisymmetric with aboveBC, bound2573    . have bound : natMax(b, c) ≤ a574        exact natMax.le_iff.backward with ⟨above, aboveAC⟩575      have value11 := natMax.of_ge with aboveAC576      have value12 := natMax.of_ge with bound577      rw [value11, value12]578      rfl579580theorem natMin.add_left (a b k : Nat)581  shows natMin(k + a, k + b) = k + natMin(a, b)582proof583  have total := LessEqual.total at a, b584  cases total with below | above585  . have shifted : k + a ≤ k + b by linarith586    have value13 := natMin.of_le with below587    have value14 := natMin.of_le with shifted588    rw [value13, value14]589    rfl590  . have shifted : k + b ≤ k + a by linarith591    have value15 := natMin.of_ge with above592    have value16 := natMin.of_ge with shifted593    rw [value15, value16]594    rfl595596theorem natMin.add_right (a b k : Nat)597  shows natMin(a + k, b + k) = natMin(a, b) + k598proof599  have total := LessEqual.total at a, b600  cases total with below | above601  . have shifted : a + k ≤ b + k by linarith602    have value17 := natMin.of_le with below603    have value18 := natMin.of_le with shifted604    rw [value17, value18]605    rfl606  . have shifted : b + k ≤ a + k by linarith607    have value19 := natMin.of_ge with above608    have value20 := natMin.of_ge with shifted609    rw [value19, value20]610    rfl611612theorem natMax.add_left (a b k : Nat)613  shows natMax(k + a, k + b) = k + natMax(a, b)614proof615  have total := LessEqual.total at a, b616  cases total with below | above617  . have shifted : k + a ≤ k + b by linarith618    have value21 := natMax.of_le with below619    have value22 := natMax.of_le with shifted620    rw [value21, value22]621    rfl622  . have shifted : k + b ≤ k + a by linarith623    have value23 := natMax.of_ge with above624    have value24 := natMax.of_ge with shifted625    rw [value23, value24]626    rfl627628theorem natMax.add_right (a b k : Nat)629  shows natMax(a + k, b + k) = natMax(a, b) + k630proof631  have total := LessEqual.total at a, b632  cases total with below | above633  . have shifted : a + k ≤ b + k by linarith634    have value25 := natMax.of_le with below635    have value26 := natMax.of_le with shifted636    rw [value25, value26]637    rfl638  . have shifted : b + k ≤ a + k by linarith639    have value27 := natMax.of_ge with above640    have value28 := natMax.of_ge with shifted641    rw [value27, value28]642    rfl643644theorem natMin.add_one (a b : Nat)645  shows natMin(a + 1, b + 1) = natMin(a, b) + 1646proof647  exact natMin.add_right at a, b, 1648649theorem natMax.add_one (a b : Nat)650  shows natMax(a + 1, b + 1) = natMax(a, b) + 1651proof652  exact natMax.add_right at a, b, 1653654theorem natMin.mul_left (a b k : Nat)655  shows natMin(k * a, k * b) = k * natMin(a, b)656proof657  have total := LessEqual.total at a, b658  cases total with below | above659  . have scaled := LessEqual.mul_left at a, b, k with below660    have value29 := natMin.of_le with below661    have value30 := natMin.of_le with scaled662    rw [value29, value30]663    rfl664  . have scaled := LessEqual.mul_left at b, a, k with above665    have value31 := natMin.of_ge with above666    have value32 := natMin.of_ge with scaled667    rw [value31, value32]668    rfl669670theorem natMin.mul_right (a b k : Nat)671  shows natMin(a * k, b * k) = natMin(a, b) * k672proof673  have total := LessEqual.total at a, b674  cases total with below | above675  . have scaled := LessEqual.mul_right at a, b, k with below676    have value33 := natMin.of_le with below677    have value34 := natMin.of_le with scaled678    rw [value33, value34]679    rfl680  . have scaled := LessEqual.mul_right at b, a, k with above681    have value35 := natMin.of_ge with above682    have value36 := natMin.of_ge with scaled683    rw [value35, value36]684    rfl685686theorem natMax.mul_left (a b k : Nat)687  shows natMax(k * a, k * b) = k * natMax(a, b)688proof689  have total := LessEqual.total at a, b690  cases total with below | above691  . have scaled := LessEqual.mul_left at a, b, k with below692    have value37 := natMax.of_le with below693    have value38 := natMax.of_le with scaled694    rw [value37, value38]695    rfl696  . have scaled := LessEqual.mul_left at b, a, k with above697    have value39 := natMax.of_ge with above698    have value40 := natMax.of_ge with scaled699    rw [value39, value40]700    rfl701702theorem natMax.mul_right (a b k : Nat)703  shows natMax(a * k, b * k) = natMax(a, b) * k704proof705  have total := LessEqual.total at a, b706  cases total with below | above707  . have scaled := LessEqual.mul_right at a, b, k with below708    have value41 := natMax.of_le with below709    have value42 := natMax.of_le with scaled710    rw [value41, value42]711    rfl712  . have scaled := LessEqual.mul_right at b, a, k with above713    have value43 := natMax.of_ge with above714    have value44 := natMax.of_ge with scaled715    rw [value43, value44]716    rfl717718theorem natMin.add_natMax (a b : Nat)719  shows natMin(a, b) + natMax(a, b) = a + b720proof721  have total := LessEqual.total at a, b722  cases total with below | above723  . have value129 := natMin.of_le with below724    have value130 := natMax.of_le with below725    rw [value129, value130]726    rfl727  . have value131 := natMin.of_ge with above728    have value132 := natMax.of_ge with above729    rw [value131, value132]730    ring731732theorem natMax.distribute_natMin (a b c : Nat)733  shows natMax(a, natMin(b, c)) = natMin(natMax(a, b), natMax(a, c))734proof735  have leftNat := natMax.natural at a, b736  have rightNat := natMax.natural at a, c737  have reflexive := LessEqual.reflexive at a738  have total := LessEqual.total at b, c739  cases total with below | above740  . have outer := natMax.monotone at a, b, a, c with reflexive, below741    have value45 := natMin.of_le with below742    have value46 := natMin.of_le with outer743    rw [value45, value46]744    rfl745  . have outer := natMax.monotone at a, c, a, b with reflexive, above746    have value47 := natMin.of_ge with above747    have value48 := natMin.of_ge with outer748    rw [value47, value48]749    rfl750751theorem natMin.distribute_natMax (a b c : Nat)752  shows natMin(a, natMax(b, c)) = natMax(natMin(a, b), natMin(a, c))753proof754  have leftNat := natMin.natural at a, b755  have rightNat := natMin.natural at a, c756  have reflexive := LessEqual.reflexive at a757  have total := LessEqual.total at b, c758  cases total with below | above759  . have outer := natMin.monotone at a, b, a, c with reflexive, below760    have value49 := natMax.of_le with below761    have value50 := natMax.of_le with outer762    rw [value49, value50]763    rfl764  . have outer := natMin.monotone at a, c, a, b with reflexive, above765    have value51 := natMax.of_ge with above766    have value52 := natMax.of_ge with outer767    rw [value51, value52]768    rfl769770theorem natMin.absorb_natMax (a b : Nat)771  shows natMin(a, natMax(a, b)) = a772proof773  have high := natMax.ge_left at a, b774  exact natMin.of_le with high775776theorem natMax.absorb_natMin (a b : Nat)777  shows natMax(a, natMin(a, b)) = a778proof779  have low := natMin.le_left at a, b780  exact natMax.of_ge with low781