Grace/Cumulus/Nat/Subtraction.g17

Open in Workbench Download source

Imports

OrderLemmas

Declarations

• sub def
• sub.one theorem derivation
• sub.zero_right theorem derivation
• sub.succ_right theorem derivation
• predecessor.zero theorem derivation
• predecessor.succ theorem derivation
• predecessor.closed theorem derivation
• sub.closed theorem derivation
• sub.zero_left theorem derivation
• sub.succ_succ theorem derivation
• sub.add_right theorem derivation
• sub.succ_of_Less theorem derivation

Source

1-- Truncated subtraction on the natural numbers: sub(m, n) is m − n when2-- n ≤ m and zero otherwise3-- Part of Cumulus, the Grace17 mathematics library.4-- Copyright (c) 2026 Grant Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78module Grace.Cumulus.Nat.Subtraction9import OrderLemmas1011-- Truncated subtraction: m - n is 0 whenever n exceeds m.12def sub (m n : Nat) → Nat13  | m, zero => m14  | m, succ(n) => predecessor(sub(m, n))15  descends n1617notation infixl 60 "-" => sub for Nat1819theorem sub.one (n : Nat)20  shows n - 1 = predecessor(n)21proof22  simp [sub]2324theorem sub.zero_right (m : Nat)25  shows m - 0 = m26proof27  simp [sub]2829theorem sub.succ_right (m n : Nat)30  shows m - succ(n) = predecessor(m - n)31proof32  simp [sub]3334theorem predecessor.zero35  shows predecessor(0) = 036proof37  compute3839theorem predecessor.succ (n : Nat)40  shows predecessor(succ(n)) = n41proof42  simp [predecessor]4344theorem predecessor.closed (n : Nat)45  shows Nat(predecessor(n))46proof47  induction n48  | zero =>49    rw predecessor.zero50    typecheck51  | succ(k) using ih =>52    rw predecessor.succ53    typecheck5455theorem sub.closed (m n : Nat)56  shows Nat(m - n)57proof58  induction n59  | zero =>60    rw sub.zero_right61    typecheck62  | succ(k) using ih =>63    rw sub.succ_right64    exact predecessor.closed at sub(m, k) with ih6566theorem sub.zero_left (n : Nat)67  shows 0 - n = 068proof69  induction n70  | zero => compute71  | succ(k) using ih =>72    rw [sub.succ_right, ih]73    exact predecessor.zero7475theorem sub.succ_succ (m n : Nat)76  shows succ(m) - succ(n) = m - n77proof78  induction n79  | zero =>80    rw [sub.succ_right, sub.zero_right, sub.zero_right]81    exact predecessor.succ at m82  | succ(k) using ih =>83    rw [sub.succ_right, ih]84    rw sub.succ_right85    rfl8687theorem sub.add_right (m n : Nat)88  shows (m + n) - n = m89proof90  induction n91  | zero =>92    have shape : m + 0 = m by ring93    rw shape94    exact sub.zero_right at m95  | succ(k) using ih =>96    have shape : m + succ(k) = succ(m + k) by ring97    rw [shape, sub.succ_succ]98    exact ih99100-- Peeling one unit off the subtrahend below the minuend.101theorem sub.succ_of_Less (k : Nat)102  shows ∀ n, Nat(n) → k < n → n - k = succ(n - succ(k))103proof104  induction k105  | zero =>106    intros n nNat below107    obtain ⟨d, dNat, shape⟩ := below108    have form : succ(0) + d = succ(d) by ring109    rw form at shape110    rw ← shape111    rw [sub.zero_right, sub.succ_succ, sub.zero_right]112    rfl113  | succ(j) using ih =>114    intros n nNat below115    obtain ⟨d, dNat, shape⟩ := below116    have form : succ(succ(j)) + d = succ(j + succ(d)) by ring117    rw form at shape118    have innerNat : Nat(j + succ(d)) by typecheck119    have innerBelow : j < j + succ(d)120      witness d121      ring122    have inner := ih with j + succ(d), innerNat, innerBelow123    rw ← shape124    rw [sub.succ_succ, sub.succ_succ]125    exact inner126