Grace/Cumulus/NumberTheory/Divisibility.g17

Open in Workbench Download source

Imports

Nat

Declarations

Source

1-- Divisibility of 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.NumberTheory.Divisibility8import Nat910predicate Divides (a b : Nat) := ∃ k, Nat(k) ∧ mul(a, k) = b11notation infix 50 "∣" => Divides1213theorem divides.definition (a b : Nat)14  shows a ∣ b ↔ ∃ k, Nat(k) ∧ mul(a, k) = b15proof16  simp [Divides]1718theorem divides.reflexive (a : Nat)19  shows a ∣ a20proof21  witness 122  simp [mul.right_unit]2324theorem one.divides (a : Nat)25  shows 1 ∣ a26proof27  witness a28  simp [mul.left_unit]2930theorem divides.zero (a : Nat)31  shows a ∣ 032proof33  witness 034  simp [mul.right_zero]3536theorem zero.divides_only_zero (a : Nat)37  requires h : 0 ∣ a38  shows a = 039proof40  obtain ⟨k, hkNat, hkEq⟩ := h41  rw ← hkEq42  simp [mul.left_zero]4344theorem divides.one_only (a : Set)45  requires haNat : Nat(a)46  requires h : a ∣ 147  shows a = 148proof49  obtain ⟨k, hkNat, hProduct⟩ := h50  apply mul.left_factor_one at k, a51  . exact hProduct5253theorem divides.transitive (a b c : Nat)54  requires hab : a ∣ b55  requires hbc : b ∣ c56  shows a ∣ c57proof58  obtain ⟨k, hkNat, hkEq⟩ := hab59  obtain ⟨l, hlNat, hlEq⟩ := hbc60  witness mul(k, l)61  simp [mul.associative_reverse]6263theorem divides.multiply_right (a b c : Nat)64  requires hab : a ∣ b65  shows a ∣ mul(b, c)66proof67  obtain ⟨k, hkNat, hkEq⟩ := hab68  witness mul(k, c)69  simp [mul.associative_reverse]7071theorem divides.multiply_left (a b c : Set)72  requires haNat : Nat(a)73  requires hbNat : Nat(b)74  requires hcNat : Nat(c)75  requires hab : a ∣ b76  shows a ∣ mul(c, b)77proof78  have right := divides.multiply_right with haNat, hbNat, hcNat, hab79  have commute := mul.commutative with hcNat, hbNat80  rwa commute at right8182theorem divides.add (a b c : Nat)83  requires hab : a ∣ b84  requires hac : a ∣ c85  shows a ∣ add(b, c)86proof87  obtain ⟨k, hkNat, hkEq⟩ := hab88  obtain ⟨l, hlNat, hlEq⟩ := hac89  witness add(k, l)90  simp [mul.distributes_left]9192lemma divides.successor_product_one (p : Set, k : Nat)93  requires hpNat : Nat(p)94  shows p ∣ succ(mul(p, k)) → p = 195proof96  induction k97  | zero =>98    intro h99    have zero := mul.right_zero with hpNat100    rw zero at h101    apply divides.one_only102    . exact hpNat103    . exact h104  | succ(j) using ih =>105    intro h106    obtain ⟨l, hlNat, hEquation⟩ := h107    have lShape := natural.zero_or_successor with hlNat108    cases lShape with hlZero | hlSuccessor109    . exfalso110      rw hlZero at hEquation111      have productZero := mul.right_zero with hpNat112      rw productZero at hEquation113      have impossible := Naturals.disjoint.zero.succ at mul(p, succ(j))114      apply impossible115      exact hEquation116    . obtain ⟨q, hq⟩ := hlSuccessor117      rcases hq with ⟨hqNat, hlSucc⟩118      rw hlSucc at hEquation119      have leftStep := mul.succ_right with hqNat, hpNat120      rw leftStep at hEquation121      have innerStep := mul.succ_right with h_j, hpNat122      rw innerStep at hEquation123      have rightStep := add.succ_right at mul(p, j), p with hpNat124      rw ← rightStep at hEquation125      have cancel := add.left_cancel with hpNat, hEquation126      apply ih127      refine ⟨q, hqNat, cancel⟩128129-- This is the arithmetic fact Euclid's proof needs.  Its statement contains130-- no representation-level membership: common divisors of n and n+1 are one.131theorem divides.consecutive_one (p n : Set)132  requires hpNat : Nat(p)133  requires hnNat : Nat(n)134  requires hn : p ∣ n135  requires hNext : p ∣ succ(n)136  shows p = 1137proof138  obtain ⟨k, hkNat, hProduct⟩ := hn139  rw ← hProduct at hNext140  apply divides.successor_product_one at p, k141  . exact hNext142143theorem factorial.successor_divides (n : Nat)144  shows succ(n) ∣ succ(n)!145proof146  witness n!147  simp [factorial]148149-- Every positive natural at most n occurs among the factors of n!.150theorem factorial.divisible_through (p : Set, n : Nat)151  requires hpNat : Nat(p)152  shows 0 ∈ p → p ∈ succ(n) → p ∣ n!153proof154  induction n155  | zero =>156    intros hpPositive hpBound157    exfalso158    have membership := membership.one.forward at p with hpBound159    rw membership at hpPositive160    simp [nat.zero, set.empty]161  | succ(k) using ih =>162    intros hpPositive hpBound163    have bound := membership.successor_forward{n := succ(k)} at p164    cases bound with hpEarlier | hpNewest165    . have dividesPrevious := ih with hpPositive, hpEarlier166      settle with divides.multiply_left, factorial, factorial.closed,167        Naturals.constructor.succ168    . rw hpNewest169      simp [factorial.successor_divides]170171-- A nonzero multiple is at least its divisor.172theorem divides.le (a b : Nat)173  requires divides : a ∣ b174  requires nonzero : b ≠ 0175  shows a ≤ b176proof177  obtain ⟨k, kNat, product⟩ := divides178  have shape := natural.zero_or_successor at k with *179  cases shape with zero | successor180  . exfalso181    rw zero at product182    have value := mul.right_zero at a with *183    rw value at product184    apply nonzero185    symm186    exact product187  . obtain ⟨j, jNat, step⟩ := successor188    rw step at product189    witness a * j190    have expand := mul.succ_right at j, a with *191    rwa expand at product192193theorem divides.antisymmetric (a b : Nat)194  requires forward : a ∣ b195  requires backward : b ∣ a196  shows a = b197proof198  have splitA : a = 0 ∨ a ≠ 0199  . tauto200  cases splitA with az | az201  . rw az at forward202    have bz := zero.divides_only_zero with *203    simp204  . have splitB : b = 0 ∨ b ≠ 0205    . tauto206    cases splitB with bz | bz207    . rw bz at backward208      have aZero := zero.divides_only_zero with *209      simp210    . have ab := divides.le at a, b with *211      have ba := divides.le at b, a with *212      exact LessEqual.antisymmetric with *213214-- Cancel a known divisible summand without introducing signed naturals.215theorem divides.add_cancel_left (d a b : Nat)216  requires dividesLeft : d ∣ a217  requires dividesSum : d ∣ a + b218  shows d ∣ b219proof220  have splitD : d = 0 ∨ d ≠ 0221  . tauto222  cases splitD with dz | dz223  . rw dz at dividesSum224    have sumZero := zero.divides_only_zero with *225    have bZero := add.eq_zero_right with *, sumZero226    rw bZero227    exact divides.zero with *228  . obtain ⟨k, kNat, left⟩ := dividesLeft229    obtain ⟨l, lNat, sum⟩ := dividesSum230    have notLess : ¬l < k231    . intro less232      have strict := Less.mul_left with *233      rw [sum, left] at strict234      have bound : a ≤ a + b235        witness b236        rfl237      have cycle := Less.transitive_LessEqual with *238      exact Less.irreflexive with *, cycle239    have order := LessEqual.of_not_Less with *240    obtain ⟨r, rNat, gap⟩ := order241    have expanded : d * k + d * r = d * l242    . rw ← gap243      ring244    rw [left, sum] at expanded245    have remainder := add.left_cancel with *, expanded246    unfold Divides247    refine ⟨r, rNat, remainder⟩248249theorem divides.add_cancel_right (d a b : Nat)250  requires dividesRight : d ∣ b251  requires dividesSum : d ∣ a + b252  shows d ∣ a253proof254  have commute := add.commutative at a, b with *255  rw ← commute at dividesSum256  exact divides.add_cancel_left with *257258-- Common divisors are unchanged by a Euclidean remainder equation.259theorem divides.remainder_iff (d a b q r : Nat)260  requires equation : a = b * q + r261  requires dividesB : d ∣ b262  shows d ∣ a ↔ d ∣ r263proof264  have multiple := divides.multiply_right at d, b, q with *265  constructor266  . intro dividesA267    rw equation at dividesA268    exact divides.add_cancel_left with *269  . intro dividesR270    rw equation271    exact divides.add with *272273lemma divides.sample274  shows 7 ∣ 42275proof276  witness 6277  compute278