Grace/Cumulus/Nat/Core.g17

Open in Workbench Download source

Imports

Core.Nat.Order

Declarations

• one.ne_zero theorem derivation
• add.left_cancel theorem derivation
• add.right_cancel theorem derivation
• add.swap_last theorem derivation
• add.four_shuffle theorem derivation
• add.eq_zero theorem derivation
• add.zero_successor_case lemma derivation
• add.eq_one theorem derivation
• add.eq_zero_right theorem derivation
• add.eq_zero_left theorem derivation
• mul.left_zero theorem derivation
• mul.succ_left theorem derivation
• mul.two_left theorem derivation
• mul.two_right theorem derivation
• mul.left_factor_one theorem derivation
• mul.eq_zero theorem derivation
• mul.nonzero theorem derivation
• mul.associative_reverse theorem derivation
• factorial.closed theorem derivation
• factorial.succ theorem derivation
• factorial.nonzero theorem derivation
• arithmetic.sample lemma derivation

Source

1-- Core natural-number mathematics2-- 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.Core8import Core.Nat.Order910-- Arithmetic lemmas belong in Cumulus; Core retains only the bootstrap laws.11theorem one.ne_zero12  shows 1 ≠ 013proof14  intro equal15  have distinct := Naturals.disjoint.zero.succ at 016  apply distinct17  symm18  exact equal1920theorem add.left_cancel (b c : Set, a : Nat)21  shows add(a, b) = add(a, c) → b = c22proof23  induction a24  | zero =>25    intro h26    simp [add] at h27    exact h28  | succ(k) using ih =>29    intro h30    simp [add] at h31    have inject := Naturals.injective.succ with h32    apply ih33    exact inject3435theorem add.right_cancel (a b c : Nat)36  shows add(a, c) = add(b, c) → a = b37proof38  intro h39  have cancel := add.left_cancel at a, b, c40  apply cancel41  have commuteA := add.commutative at a, c42  have commuteB := add.commutative at b, c43  rewrite commuteA44  rwa commuteB4546theorem add.swap_last (a b c : Nat)47  shows add(add(a, b), c) = add(add(a, c), b)48proof49  have left := add.associative at b, c, a50  have middle := add.commutative at c, b with *51  have right := add.associative at c, b, a52  simp5354theorem add.four_shuffle (a b c d : Nat)55  shows add(add(a, b), add(c, d)) = add(add(a, c), add(b, d))56proof57  simp [add.associative, add.swap]5859theorem add.eq_zero (b a : Nat)60  shows add(a, b) = 0 → (a = 0 ∧ b = 0)61proof62  induction a63  | zero =>64    intro h65    constructor66    rfl67    simp [add] at h68    exact h69  | succ(k) using ih =>70    intro h71    simp [add] at h72    exfalso73    have impossible := Naturals.disjoint.zero.succ at add(k, b)74    apply impossible75    simp7677lemma add.zero_successor_case (b : Set, a : Nat)78  requires hbNat : Nat(b)79  shows add(a, b) = 0 → (succ(a) = 1 ∧ b = 0)80proof81  induction a82  | zero =>83    intro h84    constructor85    . rfl86    . simp [add] at h87      exact h88  | succ(k) using ih =>89    intro h90    simp [add] at h91    exfalso92    have impossible := Naturals.disjoint.zero.succ at add(k, b)93    apply impossible94    simp9596theorem add.eq_one (b : Set, a : Nat)97  requires hbNat : Nat(b)98  shows add(a, b) = 1 → ((a = 0 ∧ b = 1) ∨ (a = 1 ∧ b = 0))99proof100  induction a101  | zero =>102    intro h103    left104    constructor105    . rfl106    . simp [add] at h107      exact h108  | succ(k) using ih =>109    intro h110    right111    simp [add] at h112    have inject := Naturals.injective.succ at add(k, b), 0 with h113    apply add.zero_successor_case at b, k114    . exact inject115116theorem add.eq_zero_right (b : Set, a : Nat)117  requires hbNat : Nat(b)118  shows add(a, b) = 0 → b = 0119proof120  induction a121  | zero =>122    intro h123    simp [add] at h124    exact h125  | succ(k) using ih =>126    intro h127    simp [add] at h128    exfalso129    have impossible := Naturals.disjoint.zero.succ at add(k, b)130    apply impossible131    simp132133theorem add.eq_zero_left (b : Set, a : Nat)134  requires hbNat : Nat(b)135  shows add(a, b) = 0 → a = 0136proof137  induction a138  | zero =>139    intro h140    rfl141  | succ(k) using ih =>142    intro h143    simp [add] at h144    exfalso145    have impossible := Naturals.disjoint.zero.succ at add(k, b)146    apply impossible147    simp148149theorem mul.left_zero (n : Nat)150  shows mul(0, n) = 0151proof152  simp [mul]153154theorem mul.succ_left (n m : Nat)155  shows mul(succ(n), m) = add(m, mul(n, m))156proof157  simp [mul]158159theorem mul.two_left (n : Nat)160  shows mul(2, n) = add(n, n)161proof162  simp [mul, add, add.right_unit]163164theorem mul.two_right (n : Nat)165  shows mul(n, 2) = add(n, n)166proof167  induction n168  | zero => settle with mul, add169  | succ(k) using ih => settle with mul, add, add.succ_right, ih170171theorem mul.left_factor_one (b : Set, a : Nat)172  requires hbNat : Nat(b)173  shows mul(a, b) = 1 → a = 1174proof175  induction a176  | zero =>177    intro h178    simp [mul] at h179  | succ(k) using ih =>180    intro h181    simp [mul] at h182    have productNat := mul.closed with hbNat, h_k183    have shape := add.eq_one with hbNat, productNat, h184    cases shape with hLeft | hRight185    . rcases hLeft with ⟨hbZero, hProductOne⟩186      exfalso187      rw hbZero at hProductOne188      have zero := mul.right_zero with h_k189      rw zero at hProductOne190      have impossible := Naturals.disjoint.zero.succ at 0191      apply impossible192      exact hProductOne193    . rcases hRight with ⟨hbOne, hProductZero⟩194      rw hbOne at hProductZero195      have unit := mul.right_unit with h_k196      rw unit at hProductZero197      rw hProductZero198      rfl199200theorem mul.eq_zero (b : Set, a : Nat)201  requires hbNat : Nat(b)202  shows mul(a, b) = 0 → (a = 0 ∨ b = 0)203proof204  induction a205  | zero =>206    intro h207    left208    rfl209  | succ(k) using ih =>210    intro h211    right212    simp [mul] at h213    apply add.eq_zero_left at mul(k, b), b214    . settle with mul.closed215216theorem mul.nonzero (a b : Nat)217  requires aNonzero : a ≠ 0218  requires bNonzero : b ≠ 0219  shows a * b ≠ 0220proof221  intro productZero222  have zeroFactor := mul.eq_zero with *, productZero223  cases zeroFactor with aZero | bZero224  . apply aNonzero225    exact aZero226  . apply bNonzero227    exact bZero228229theorem mul.associative_reverse (y z : Nat, x : Nat)230  shows mul(x, mul(y, z)) = mul(mul(x, y), z)231proof232  simp [mul.associative]233234theorem factorial.closed (n : Nat)235  shows Nat(n!)236proof237  induction n238  | zero => settle with factorial, Naturals.constructor.zero, Naturals.constructor.succ239  | succ(k) using ih => settle with factorial, mul.closed, Naturals.constructor.succ, ih240241-- The step law in the form a proof about n + 1 uses: (n + 1)! = (n + 1) · n!.242theorem factorial.succ (n : Nat)243  shows (n + 1)! = (n + 1) * n!244proof245  have one : n + 1 = succ(n) := add.right_one with *246  rw one247  simp [factorial]248249theorem factorial.nonzero (n : Nat)250  shows n! ≠ 0251proof252  induction n253  | zero =>254    intro h255    simp [factorial] at h256  | k + 1 using ih =>257    intro h258    have step := factorial.succ with *259    rw step at h260    have zeroProduct := mul.eq_zero with h261    cases zeroProduct with hSucc | hFact262    . have one := add.right_one with *263      rw one at hSucc264      have impossible := Naturals.disjoint.zero.succ at k265      apply impossible266      simp267    . exact ih with hFact268269lemma arithmetic.sample270  shows (17 + 25) * 3 = 126271proof272  compute273274eval (17 + 25) * 3275