Grace/Cumulus/Nat/Order.g17

Open in Workbench Download source

Imports

Core · Foundation

Declarations

Source

1-- Natural-number order and its von Neumann membership interpretation2-- 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.Order8import Core9import Foundation1011theorem LessEqual.zero (a : Nat)12  shows 0 ≤ a13proof14  witness a15  simp [add]1617-- These four addition laws are the small proof-producing certificate basis18-- used by linear arithmetic automation.  They are Cumulus19-- theorems: an arithmetic oracle may search for combinations, but the kernel20-- sees only applications of these checked laws.21theorem LessEqual.add (a b c d : Nat)22  requires hab : a ≤ b23  requires hcd : c ≤ d24  shows a + c ≤ b + d25proof26  obtain ⟨k, hkNat, hkEq⟩ := hab27  obtain ⟨l, hlNat, hlEq⟩ := hcd28  witness k + l29  have shuffle := add.four_shuffle at a, c, k, l30  rw [shuffle, hkEq, hlEq]31  rfl3233theorem Less.add_LessEqual (a b c d : Nat)34  requires hab : a < b35  requires hcd : c ≤ d36  shows a + c < b + d37proof38  unfold Less at hab39  have haSucc := Naturals.constructor.succ at a40  have sum := LessEqual.add with hab, hcd41  unfold Less42  simpa [add] using sum4344theorem LessEqual.add_Less (a b c d : Nat)45  requires hab : a ≤ b46  requires hcd : c < d47  shows a + c < b + d48proof49  unfold Less at hcd50  have sum := LessEqual.add at a, b, succ(c), d with *51  unfold Less52  simpa [add.succ_right] using sum5354theorem Less.add (a b c d : Nat)55  requires hab : a < b56  requires hcd : c < d57  shows a + c < b + d58proof59  simp [Less.implies_LessEqual, Less.add_LessEqual]6061-- Adding a nonzero natural number moves strictly to the right.  This compact62-- certificate is useful when polynomial normalization has isolated a positive63-- remainder.64theorem Less.add_positive (a k : Nat)65  requires nonzero : k ≠ 066  shows a < a + k67proof68  have shape := natural.zero_or_successor at k69  cases shape with zero | successor70  . exfalso71    exact nonzero with zero72  . obtain ⟨j, jNatural, kShape⟩ := successor73    rw kShape74    witness j75    simp [add.successor_shift]7677theorem LessEqual.mul_left (a b k : Nat)78  requires hab : a ≤ b79  shows k * a ≤ k * b80proof81  induction k82  | zero =>83    have zeroA := mul.left_zero at a84    have zeroB := mul.left_zero at b85    rw [zeroA, zeroB]86    apply LessEqual.reflexive87  | succ(j) using ih =>88    have leftStep := mul.succ_left at j, a with h_j89    have rightStep := mul.succ_left at j, b with h_j90    rw [leftStep, rightStep]91    have products := ih92    apply LessEqual.add93    . assumption94    . assumption9596theorem Less.mul_left (a b k : Nat)97  requires positive : k ≠ 098  requires hab : a < b99  shows k * a < k * b100proof101  have shape := natural.zero_or_successor at k102  cases shape with zero | successor103  . exfalso104    apply positive105    exact zero106  . obtain ⟨j, hj⟩ := successor107    rcases hj with ⟨hjNat, kShape⟩108    rw kShape109    have leftStep := mul.succ_left at j, a with hjNat110    have rightStep := mul.succ_left at j, b with hjNat111    rw [leftStep, rightStep]112    have weak := Less.implies_LessEqual with *113    have products := LessEqual.mul_left at a, b, j with hjNat, weak114    apply Less.add_LessEqual115    . assumption116    . assumption117118theorem LessEqual.add_right_cancel (a b c : Nat)119  requires hab : a + c ≤ b + c120  shows a ≤ b121proof122  obtain ⟨k, hkNat, hkEq⟩ := hab123  witness k124  apply add.right_cancel at a + k, b, c125  . have shuffle := add.swap_last at a, c, k with hkNat126    rwa ← shuffle127128theorem LessEqual.add_left_cancel (a b c : Nat)129  requires hab : c + a ≤ c + b130  shows a ≤ b131proof132  have left := add.commutative at a, c with *133  rw left at hab134  have right := add.commutative at b, c with *135  rw right at hab136  apply LessEqual.add_right_cancel137  . assumption138139theorem Less.add_right_cancel (a b c : Nat)140  requires hab : a + c < b + c141  shows a < b142proof143  have shift : succ(a + c) = succ(a) + c by simp [add]144  unfold Less at hab145  unfold Less146  apply LessEqual.add_right_cancel at succ(a), b, c147  . settle with Naturals.constructor.succ148149theorem Less.gap (a b : Nat)150  shows a < b ↔ a + 1 ≤ b151proof152  simp [Less, add.right_one]153154-- Users reason with `<`; this bridge reveals that it is membership for the155-- von Neumann implementation of Nat only when set-theoretic access is useful.156theorem Less.of_membership (a b : Nat)157  shows a ∈ b → a < b158proof159  induction b160  | zero =>161    intro h162    exfalso163    settle with nat.zero, set.empty164  | succ(k) using ih =>165    intro h166    have shape := membership.successor_forward{n := k} at a167    cases shape with hEarlier | hEqual168    . have earlier := ih with hEarlier169      unfold Less at earlier170      unfold Less171      apply LessEqual.transitive172      . exact earlier173      . apply LessEqual.successor at k174    . rw hEqual175      unfold Less176      apply LessEqual.reflexive177178-- The converse bridge is kept here, at the explicit boundary between the179-- Nat order API and its von Neumann implementation.180lemma membership.add_right_successor (a : Set, k : Nat)181  requires haNat : Nat(a)182  shows a ∈ add(k, succ(a))183proof184  induction k185  | zero =>186    settle with add, membership.self_successor187  | succ(j) using ih =>188    have haSucc := Naturals.constructor.succ with haNat189    have sumNat := add.closed with haSucc, h_j190    settle with add, membership.successor_backward, ih, sumNat191192theorem membership.of_Less (a b : Set)193  requires haNat : Nat(a)194  requires hbNat : Nat(b)195  shows a < b → a ∈ b196proof197  intro h198  obtain ⟨k, hkNat, hSum⟩ := h199  rw ← hSum200  have haSucc := Naturals.constructor.succ with haNat201  have commute := add.commutative with hkNat, haSucc202  rw commute203  apply membership.add_right_successor at a, k204205theorem Less.trichotomy (a b : Set)206  requires haNat : Nat(a)207  requires hbNat : Nat(b)208  shows a < b ∨ a = b ∨ b < a209proof210  simp [Ordinal.natural, Ordinal.trichotomy, Less.of_membership]211212theorem Less.irreflexive (a : Nat)213  shows ¬a < a214proof215  intro h216  have member := membership.of_Less with *, h217  have irreflexive := membership.irreflexive at a218  apply irreflexive219  exact member220221theorem mul.left_cancel_positive (a b k : Nat)222  requires positive : k ≠ 0223  requires products : k * a = k * b224  shows a = b225proof226  have comparison := Less.trichotomy at a, b with *227  cases comparison with hab | rest228  . have strict := Less.mul_left with positive, hab229    rw products at strict230    have productNat := mul.closed at b, k with *231    have impossible := Less.irreflexive with productNat232    exfalso233    apply impossible234    exact strict235  . cases rest with equal | hba236    . exact equal237    . have strict := Less.mul_left with positive, hba238      rw products at strict239      have productNat := mul.closed at b, k with *240      have impossible := Less.irreflexive with productNat241      exfalso242      apply impossible243      exact strict244245theorem Less.mul_left_cancel_positive (a b k : Nat)246  requires positive : k ≠ 0247  requires products : k * a < k * b248  shows a < b249proof250  have comparison := Less.trichotomy at a, b with *251  cases comparison with less | rest252  . exact less253  . cases rest with equal | greater254    . rw equal at products255      have productNat := mul.closed at b, k with *256      have impossible := Less.irreflexive with productNat257      exfalso258      apply impossible259      exact products260    . have reverseProducts := Less.mul_left with positive, greater261      have productANat : Nat(k * a) by simp [mul.closed]262      have reverseWeak := Less.implies_LessEqual with reverseProducts263      have cycle : k * a < k * a264        unfold Less265        apply LessEqual.transitive266        . exact products267        . exact reverseWeak268      have impossible := Less.irreflexive with productANat269      exfalso270      apply impossible271      exact cycle272273theorem Less.transitive_LessEqual (a b c : Nat)274  requires hab : a < b275  requires hbc : b ≤ c276  shows a < c277proof278  unfold Less at hab279  unfold Less280  apply LessEqual.transitive281  . settle with Naturals.constructor.succ282  . assumption283284theorem Less.transitive (a b c : Nat)285  requires hab : a < b286  requires hbc : b < c287  shows a < c288proof289  have weak := Less.implies_LessEqual at b, c with *290  exact Less.transitive_LessEqual with *291292theorem LessEqual.transitive_Less (a b c : Nat)293  requires hab : a ≤ b294  requires hbc : b < c295  shows a < c296proof297  have shifted := LessEqual.add_monotone_right at a, b, 1 with *298  simp [add.succ_right, add.right_unit] at shifted299  unfold Less at hbc300  unfold Less301  apply LessEqual.transitive302  . settle with Naturals.constructor.succ303  . settle with Naturals.constructor.succ304305theorem LessEqual.antisymmetric (a b : Nat)306  requires hab : a ≤ b307  requires hba : b ≤ a308  shows a = b309proof310  have tri := Less.trichotomy at a, b with *311  cases tri with habStrict | rest312  . have cycle := Less.transitive_LessEqual with habStrict, hba313    have impossible := Less.irreflexive at a314    exfalso315    apply impossible316    exact cycle317  . cases rest with equal | hbaStrict318    . exact equal319    . have cycle := Less.transitive_LessEqual with hbaStrict, hab320      have impossible := Less.irreflexive at b321      exfalso322      apply impossible323      exact cycle324325theorem Less.of_not_LessEqual (a b : Nat)326  requires h : ¬a ≤ b327  shows b < a328proof329  have tri := Less.trichotomy at a, b with *330  cases tri with hab | rest331  . exfalso332    apply h333    apply Less.implies_LessEqual334    . exact hab335  . cases rest with eqab | hba336    . exfalso337      apply h338      rw eqab339      apply LessEqual.reflexive340      assumption341342theorem LessEqual.of_not_Less (a b : Nat)343  requires h : ¬a < b344  shows b ≤ a345proof346  have tri := Less.trichotomy at a, b with *347  cases tri with hab | rest348  . exfalso349    apply h350    exact hab351  . cases rest with eqab | hba352    . rw eqab353      apply LessEqual.reflexive354    . apply Less.implies_LessEqual at b, a355      . assumption356357-- These replacement laws package the ordered-additive reasoning used358-- after a denominator has been cleared. They keep client proofs focused on359-- the mathematical substitution rather than reassociation and cancellation.360theorem Less.replace_right (a b c d e f : Nat)361  requires less : a + d < b + c362  requires equal : c + f = d + e363  shows a + f < b + e364proof365  have reflexive := LessEqual.reflexive at f366  have augmented := Less.add_LessEqual with less, reflexive367  have leftShape : (a + d) + f = (a + f) + d by ring368  have rightShape : (b + c) + f = b + (c + f) by ring369  rw [leftShape, rightShape, equal] at augmented370  have finalShape : b + (d + e) = (b + e) + d by ring371  rw finalShape at augmented372  exact Less.add_right_cancel with augmented373374theorem Less.replace_left (a b c d e f : Nat)375  requires equal : a + f = b + e376  requires less : a + d < b + c377  shows d + e < c + f378proof379  have reflexive := LessEqual.reflexive at f380  have augmented := Less.add_LessEqual with less, reflexive381  have leftShape : (a + d) + f = (a + f) + d by ring382  have rightShape : (b + c) + f = (c + f) + b by ring383  rw [leftShape, rightShape, equal] at augmented384  have finalShape : (b + e) + d = (d + e) + b by ring385  rw finalShape at augmented386  exact Less.add_right_cancel with augmented387388theorem Less.cross_transitive (a b c d e f : Nat)389  requires left : a + d < b + c390  requires right : c + f < d + e391  shows a + f < b + e392proof393  have reflexiveF := LessEqual.reflexive at f394  have first := Less.add_LessEqual with left, reflexiveF395  have firstLeft : (a + d) + f = (a + f) + d by ring396  have firstRight : (b + c) + f = (c + f) + b by ring397  rw [firstLeft, firstRight] at first398  have reflexiveB := LessEqual.reflexive at b399  have second := Less.add_LessEqual with right, reflexiveB400  have secondRight : (d + e) + b = (b + e) + d by ring401  rw secondRight at second402  have secondWeak := Less.implies_LessEqual with second403  have composed := Less.transitive_LessEqual with first, secondWeak404  exact Less.add_right_cancel with composed405406-- A finite Boolean crossing on the naturals has a last included point.  The407-- set S need not itself be finite or downward closed; only the finite interval408-- from zero to the omitted endpoint is inspected.409theorem natural.exists_boundary (S : Set, n : Nat)410  shows 0 ∈ S → ¬(n ∈ S) →411    ∃ k, Nat(k) ∧ k ∈ S ∧ ¬(succ(k) ∈ S)412proof413  induction n414  | zero =>415    intros zeroIn nMissing416    exfalso417    exact nMissing with zeroIn418  | succ(j) using ih =>419    intros zeroIn nMissing420    have split : j ∈ S ∨ ¬(j ∈ S) by tauto421    cases split with jIn | jMissing422    . witness j423      refine ⟨jIn, nMissing⟩424    . exact ih with zeroIn, jMissing425426theorem membership.successor_monotone (a b x : Set)427  requires haNat : Nat(a)428  requires hbNat : Nat(b)429  requires hbInA : b ∈ a430  requires hx : x ∈ succ(b)431  shows x ∈ succ(a)432proof433  have shape := membership.successor_forward{n := b} at x434  apply membership.successor_backward{n := a} at x435  left436  cases shape with hxInB | hxEqB437  . have haOrdinal := Ordinal.natural at a with haNat438    have transitive := Ordinal.transitive with haOrdinal439    have bSubset := transitive with hbInA440    exact bSubset with x, hxInB441  . rw hxEqB442    exact hbInA443444theorem LessEqual.total (a b : Nat)445  shows a ≤ b ∨ b ≤ a446proof447  have comparison := Less.trichotomy at a, b with *448  rcases comparison with less | equal | greater449  . left450    arith451  . left452    rw equal453    exact LessEqual.reflexive with *454  . right455    arith456457theorem Less.successor_upper (a b : Nat)458  requires below : a < succ(b)459  shows a ≤ b460proof461  obtain ⟨d, natural, equation⟩ := below462  simp [add] at equation463  have cancelled := Naturals.injective.succ with equation464  unfold LessEqual465  refine ⟨d, natural, cancelled⟩466467theorem Less.successor_lower_of_ne (a b : Nat)468  requires below : a < b469  requires separated : b ≠ succ(a)470  shows succ(a) < b471proof472  have cases := Less.trichotomy at succ(a), b with *473  cases cases with less | remaining474  . exact less475  . cases remaining with equal | reverse476    . have same : b = succ(a)477        cc478      exfalso479      exact separated with same480    . have bound := Less.successor_upper with *481      have impossible : a < a by arith482      have excluded := Less.irreflexive at a with *483      exfalso484      exact excluded with impossible485486theorem Less.of_successor_upper_ne (a b : Nat)487  requires below : a < succ(b)488  requires separated : a ≠ b489  shows a < b490proof491  have member := membership.of_Less with *, below492  have shape := membership.successor_forward{n := b} with member493  cases shape with before | same494  . have bridge := Less.of_membership at a, b with *495    exact bridge with before496  . exfalso497    exact separated with same498