Grace/Cumulus/Int/AbsoluteValue.g17

Open in Workbench Download source

Imports

Arithmetic

Declarations

Source

1-- Absolute values of the existing quotient integers2-- 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.Int.AbsoluteValue8import Arithmetic910theorem integerClass.positive_difference (a b d : Nat)11  requires difference : b + d = a12  shows integerClass(a, b) = integerOfNat(d)13proof14  unfold integerOfNat15  apply integerClass.eq with *{4}16  ring1718theorem integerClass.negative_difference (a b d : Nat)19  requires difference : a + d = b20  shows integerClass(a, b) = integerNegativeOfNat(d)21proof22  unfold integerNegativeOfNat23  apply integerClass.eq with *{4}24  ring2526theorem Integer.signed_natural (z : Integer)27  shows ∃ n, Nat(n) ∧ (z = integerOfNat(n) ∨ z = integerNegativeOfNat(n))28proof29  obtain ⟨a, aNat, b, bNat, shape⟩ := Integer.representatives at z with *30  rw under shape31  have total := LessEqual.total at a, b with *32  cases total with negative | positive33  . obtain ⟨d, dNat, difference⟩ := negative34    have value := integerClass.negative_difference with *35    witness d36    right37    exact value38  . obtain ⟨e, eNat, equation⟩ := positive39    have value := integerClass.positive_difference with *40    witness e41    left42    exact value4344theorem integerOfNat.neg (n : Nat)45  shows -(integerOfNat(n)) = integerNegativeOfNat(n)46proof47  simp [integerOfNat, integerNegativeOfNat, integerNegValue.classes, integerClassNeg]4849theorem integerNegativeOfNat.neg (n : Nat)50  shows -(integerNegativeOfNat(n)) = integerOfNat(n)51proof52  simp [integerOfNat, integerNegativeOfNat, integerNegValue.classes, integerClassNeg]5354theorem integerNegativeOfNat.injective (m n : Nat)55  requires same : integerNegativeOfNat(m) = integerNegativeOfNat(n)56  shows m = n57proof58  simp [integerNegativeOfNat] at same59  have sums := integerClass.equivalent_of_eq with *60  simp [add] at sums61  symm62  exact sums6364theorem integerOfNat.eq_negative (m n : Nat)65  requires same : integerOfNat(m) = integerNegativeOfNat(n)66  shows m = 0 ∧ n = 067proof68  simp [integerOfNat, integerNegativeOfNat] at same69  have sums := integerClass.equivalent_of_eq with *70  simp [add] at sums71  exact add.eq_zero with *, sums7273theorem integerMagnitude.unique_of_sign (z : Integer, m n : Nat)74  requires first : z = integerOfNat(m) ∨ z = integerNegativeOfNat(m)75  requires second : z = integerOfNat(n) ∨ z = integerNegativeOfNat(n)76  shows m = n77proof78  cases first with positiveM | negativeM79  . cases second with positiveN | negativeN80    . have same : integerOfNat(m) = integerOfNat(n)81      . cc82      exact integerOfNat.injective with *83    . have same : integerOfNat(m) = integerNegativeOfNat(n)84      . cc85      have zeros := integerOfNat.eq_negative with *86      cc87  . cases second with positiveN | negativeN88    . have same : integerOfNat(n) = integerNegativeOfNat(m)89      . cc90      have zeros := integerOfNat.eq_negative with *91      cc92    . have same : integerNegativeOfNat(m) = integerNegativeOfNat(n)93      . cc94      exact integerNegativeOfNat.injective with *9596-- Extract the unique natural magnitude in ZF, without Choice.97defunique integerMagnitude (z : Set) (n ∈ ℕ) :=98  z = integerOfNat(n) ∨ z = integerNegativeOfNat(n)99requires integer : Integer(z)100proof101  obtain ⟨n, nNat, sign⟩ := Integer.signed_natural at z with *102  have member := nat.omega.forward with nNat103  refine ⟨n, member, sign⟩104105uniqueness106  intros m mMember first n nMember second107  have mNat := nat.omega.backward with mMember108  have nNat := nat.omega.backward with nMember109  exact integerMagnitude.unique_of_sign with *110111def integerNatAbs (z : Integer) : Nat := integerMagnitude(z)112def integerAbs (z : Integer) : Integer := integerOfNat(integerNatAbs(z))113114theorem integerNatAbs.natural (z : Integer)115  shows Nat(integerNatAbs(z))116proof117  have selected := integerMagnitude.selected at z with *118  rcases selected with ⟨member, sign⟩119  unfold integerNatAbs120  exact nat.omega.backward with member121122theorem integerNatAbs.cases (z : Integer)123  shows z = integerOfNat(integerNatAbs(z)) ∨ z = integerNegativeOfNat(integerNatAbs(z))124proof125  have selected := integerMagnitude.selected at z with *126  rcases selected with ⟨member, sign⟩127  simpa [integerNatAbs] using sign128129theorem integerNatAbs.eq_of_sign (z : Integer, n : Nat)130  requires sign : z = integerOfNat(n) ∨ z = integerNegativeOfNat(n)131  shows integerNatAbs(z) = n132proof133  have selected := integerNatAbs.cases with *134  exact integerMagnitude.unique_of_sign with *135136theorem integerNatAbs.ofNat (n : Nat)137  shows integerNatAbs(integerOfNat(n)) = n138proof139  apply integerNatAbs.eq_of_sign with *{2}140  left141  rfl142143theorem integerNatAbs.ofNegativeNat (n : Nat)144  shows integerNatAbs(integerNegativeOfNat(n)) = n145proof146  apply integerNatAbs.eq_of_sign with *{2}147  right148  rfl149150theorem integerNatAbs.neg (z : Integer)151  shows integerNatAbs(-z) = integerNatAbs(z)152proof153  have sign := integerNatAbs.cases with *154  apply integerNatAbs.eq_of_sign with *{2}155  cases sign with positive | negative156  . right157    have negated := integerOfNat.neg at integerNatAbs(z) with *158    rwa ← positive at negated159  . left160    have negated := integerNegativeOfNat.neg at integerNatAbs(z) with *161    rwa ← negative at negated162163theorem integerAbs.integer (z : Integer)164  shows Integer(integerAbs(z))165proof166  unfold integerAbs167  exact integerOfNat.integer with *168169theorem integerAbs.neg (z : Integer)170  shows integerAbs(-z) = integerAbs(z)171proof172  have equal := integerNatAbs.neg with *173  simp [integerAbs]174175theorem integerAbs.idempotent (z : Integer)176  shows integerAbs(integerAbs(z)) = integerAbs(z)177proof178  simp [integerAbs, integerNatAbs.ofNat]179180theorem integerNatAbs.mul (x y : Integer)181  shows integerNatAbs(x * y) = integerNatAbs(x) * integerNatAbs(y)182proof183  obtain ⟨m, mNat, xSign⟩ := Integer.signed_natural at x with *184  obtain ⟨n, nNat, ySign⟩ := Integer.signed_natural at y with *185  cases xSign with xPositive | xNegative186  . cases ySign with yPositive | yNegative187    . simp [integerMulValue.ofNat, integerNatAbs.ofNat]188    . simp [integerMulValue.ofNat_negative, integerNatAbs.ofNat, integerNatAbs.ofNegativeNat]189  . cases ySign with yPositive | yNegative190    . simp [integerMulValue.negative_ofNat, integerNatAbs.ofNat, integerNatAbs.ofNegativeNat]191    . simp [integerMulValue.negative_negative, integerNatAbs.ofNat, integerNatAbs.ofNegativeNat]192193-- Adjust a coefficient when its input is represented with the opposite sign.194theorem integerMulValue.sign_adjust (u z : Integer, n : Nat)195  requires sign : z = integerOfNat(n) ∨ z = integerNegativeOfNat(n)196  shows ∃ v, Integer(v) ∧ v * z = u * integerOfNat(n)197proof198  cases sign with positive | negative199  . witness u200    rw positive201    rfl202  . have negativeInteger := integerNegValue.integer at u with *203    have product := integerMulValue.neg_both at u, integerOfNat(n) with *204    have flipped := integerOfNat.neg with *205    rw [flipped, ← negative] at product206    refine ⟨-u, negativeInteger, product⟩207208theorem integerNatAbs.zero209  shows integerNatAbs(integerZero) = 0210proof211  have value := integerNatAbs.ofNat at 0 with *212  simpa [integerZero, integerOfNat] using value213214theorem integerNatAbs.zero_iff (z : Integer)215  shows integerNatAbs(z) = 0 ↔ z = integerZero216proof217  constructor218  . intro zero219    have sign := integerNatAbs.cases with *220    rw zero at sign221    unfold integerZero222    cases sign with positive | negative223    . simpa [integerOfNat] using positive224    . simpa [integerNegativeOfNat] using negative225  . intro zero226    rw zero227    exact integerNatAbs.zero228