Grace/Cumulus/Int/Arithmetic.g17

Open in Workbench Download source

Imports

Operations

Declarations

Source

1-- Arithmetic on quotient integers, independent of representatives2-- 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.Arithmetic8import Operations910-- The output class is unique by representative independence.11-- Extract it in ZF; no representative selector or Choice axiom is used.12defunique selectedIntegerSum (x y : Set) (z ∈ ℤ) :=13  ∃ a, Nat(a) ∧ ∃ b, Nat(b) ∧ ∃ c, Nat(c) ∧ ∃ d, Nat(d) ∧14    x = integerClass(a, b) ∧ y = integerClass(c, d) ∧ z = integerClassSum(a, b, c, d)15requires xInteger : Integer(x)16requires yInteger : Integer(y)17proof18  obtain ⟨a, aNat, b, bNat, xShape⟩ := Integer.representatives at x with xInteger19  obtain ⟨c, cNat, d, dNat, yShape⟩ := Integer.representatives at y with yInteger20  have result := integerClassSum.integer at a, b, c, d with *21  unfold Integer at result22  witness integerClassSum(a, b, c, d)23  refine ⟨result, a, aNat, b, bNat, c, cNat, d, dNat, xShape, yShape, rfl⟩2425uniqueness26  intros z zMember zProperty w wMember wProperty27  obtain ⟨a, aNat, b, bNat, c, cNat, d, dNat, xShape, yShape, zShape⟩ := zProperty28  obtain ⟨e, eNat, f, fNat, g, gNat, h, hNat, xOther, yOther, wShape⟩ := wProperty29  have xSame : integerClass(a, b) = integerClass(e, f)30    cc31  have ySame : integerClass(c, d) = integerClass(g, h)32    cc33  have left := integerClass.equivalent_of_eq at a, b, e, f with *34  have right := integerClass.equivalent_of_eq at c, d, g, h with *35  have independent := integerClassSum.well_defined at a, b, e, f, c, d, g, h with *36  cc3738def integerAddValue (x y : Integer) : Integer := selectedIntegerSum(x, y)3940theorem integerAddValue.integer (x y : Integer)41  shows Integer(integerAddValue(x, y))42proof43  have selected := selectedIntegerSum.selected at x, y with *44  unfold integerAddValue45  unfold Integer46  tauto4748theorem integerAddValue.classes (a b c d : Nat)49  shows integerAddValue(integerClass(a, b), integerClass(c, d)) = integerClassSum(a, b, c, d)50proof51  have selected := selectedIntegerSum.selected at integerClass(a, b), integerClass(c, d) with *52  rcases selected with ⟨integer, a2, a2Nat, b2, b2Nat, c2, c2Nat, d2, d2Nat, xShape, yShape, value⟩53  have left := integerClass.equivalent_of_eq at a, b, a2, b2 with *54  have right := integerClass.equivalent_of_eq at c, d, c2, d2 with *55  have independent := integerClassSum.well_defined at a, b, a2, b2, c, d, c2, d2 with *56  unfold integerAddValue57  rw independent58  exact value5960defunique selectedIntegerProduct (x y : Set) (z ∈ ℤ) :=61  ∃ a, Nat(a) ∧ ∃ b, Nat(b) ∧ ∃ c, Nat(c) ∧ ∃ d, Nat(d) ∧62    x = integerClass(a, b) ∧ y = integerClass(c, d) ∧ z = integerClassMul(a, b, c, d)63requires xInteger : Integer(x)64requires yInteger : Integer(y)65proof66  obtain ⟨a, aNat, b, bNat, xShape⟩ := Integer.representatives with xInteger67  obtain ⟨c, cNat, d, dNat, yShape⟩ := Integer.representatives with yInteger68  have result := integerClassMul.integer at a, b, c, d with *69  witness integerClassMul(a, b, c, d)70  refine ⟨result, a, aNat, b, bNat, c, cNat, d, dNat, xShape, yShape, rfl⟩7172uniqueness73  intros z zMember zProperty w wMember wProperty74  obtain ⟨a, aNat, b, bNat, c, cNat, d, dNat, xShape, yShape, zShape⟩ := zProperty75  obtain ⟨e, eNat, f, fNat, g, gNat, h, hNat, xOther, yOther, wShape⟩ := wProperty76  have xSame : integerClass(a, b) = integerClass(e, f) by cc77  have ySame : integerClass(c, d) = integerClass(g, h) by cc78  have left := integerClass.equivalent_of_eq at a, b, e, f with *79  have right := integerClass.equivalent_of_eq at c, d, g, h with *80  have independent := integerClassMul.well_defined at a, b, e, f, c, d, g, h with *81  cc8283def integerMulValue (x y : Integer) : Integer := selectedIntegerProduct(x, y)8485theorem integerMulValue.integer (x y : Integer)86  shows Integer(integerMulValue(x, y))87proof88  have selected := selectedIntegerProduct.selected at x, y with *89  unfold integerMulValue90  unfold Integer91  tauto9293theorem integerMulValue.classes (a b c d : Nat)94  shows integerMulValue(integerClass(a, b), integerClass(c, d)) = integerClassMul(a, b, c, d)95proof96  have selected := selectedIntegerProduct.selected at integerClass(a, b), integerClass(c, d) with *97  rcases selected with ⟨integer, a2, a2Nat, b2, b2Nat, c2, c2Nat, d2, d2Nat, xShape, yShape, value⟩98  have left := integerClass.equivalent_of_eq at a, b, a2, b2 with *99  have right := integerClass.equivalent_of_eq at c, d, c2, d2 with *100  have independent := integerClassMul.well_defined at a, b, a2, b2, c, d, c2, d2 with *101  unfold integerMulValue102  rw independent103  exact value104105defunique selectedIntegerNegative (x : Set) (z ∈ ℤ) :=106  ∃ a, Nat(a) ∧ ∃ b, Nat(b) ∧ x = integerClass(a, b) ∧ z = integerClassNeg(a, b)107requires xInteger : Integer(x)108proof109  obtain ⟨a, aNat, b, bNat, xShape⟩ := Integer.representatives with xInteger110  have result := integerClassNeg.integer at a, b with *111  witness integerClassNeg(a, b)112  refine ⟨result, a, aNat, b, bNat, xShape, rfl⟩113114uniqueness115  intros z zMember zProperty w wMember wProperty116  obtain ⟨a, aNat, b, bNat, xShape, zShape⟩ := zProperty117  obtain ⟨c, cNat, d, dNat, xOther, wShape⟩ := wProperty118  have same : integerClass(a, b) = integerClass(c, d) by cc119  have equivalent := integerClass.equivalent_of_eq with *120  have independent := integerClassNeg.well_defined with *121  cc122123def integerNegValue (x : Integer) : Integer := selectedIntegerNegative(x)124125theorem integerNegValue.integer (x : Integer)126  shows Integer(integerNegValue(x))127proof128  have selected := selectedIntegerNegative.selected at x with *129  unfold integerNegValue130  unfold Integer131  tauto132133theorem integerNegValue.classes (a b : Nat)134  shows integerNegValue(integerClass(a, b)) = integerClassNeg(a, b)135proof136  have selected := selectedIntegerNegative.selected at integerClass(a, b) with *137  rcases selected with ⟨integer, a2, a2Nat, b2, b2Nat, xShape, value⟩138  have equivalent := integerClass.equivalent_of_eq with *139  have independent := integerClassNeg.well_defined with *140  unfold integerNegValue141  rw independent142  exact value143144-- Operations retain the existing quotient integer carrier.145notation infixl 60 "+" => integerAddValue for Integer146notation infixl 70 "*" => integerMulValue for Integer147notation prefix 75 "-" => integerNegValue for Integer148149theorem integerAddValue.commutative (x y : Integer)150  shows x + y = y + x151proof152  obtain ⟨a, aNat, b, bNat, xShape⟩ := Integer.representatives at x with *153  obtain ⟨c, cNat, d, dNat, yShape⟩ := Integer.representatives at y with *154  simp [integerAddValue.classes]155  exact integerClassSum.commutative with *156157theorem integerMulValue.commutative (x y : Integer)158  shows x * y = y * x159proof160  obtain ⟨a, aNat, b, bNat, xShape⟩ := Integer.representatives at x with *161  obtain ⟨c, cNat, d, dNat, yShape⟩ := Integer.representatives at y with *162  simp [integerMulValue.classes]163  exact integerClassMul.commutative with *164165theorem integerAddValue.zero_right (x : Integer)166  shows x + integerZero = x167proof168  obtain ⟨a, aNat, b, bNat, xShape⟩ := Integer.representatives at x with *169  simp [integerZero, integerAddValue.classes, integerClassSum.zero_right]170171theorem integerAddValue.neg_right (x : Integer)172  shows x + (-x) = integerZero173proof174  obtain ⟨a, aNat, b, bNat, xShape⟩ := Integer.representatives at x with *175  simp [integerNegValue.classes, integerClassNeg, integerAddValue.classes, integerClassSum.neg_right]176177theorem integerNegValue.involutive (x : Integer)178  shows -(-x) = x179proof180  obtain ⟨a, aNat, b, bNat, xShape⟩ := Integer.representatives at x with *181  simp [integerNegValue.classes, integerClassNeg]182183theorem integerAddValue.associative (x y z : Integer)184  shows (x + y) + z = x + (y + z)185proof186  obtain ⟨a, aNat, b, bNat, xShape⟩ := Integer.representatives at x with *187  obtain ⟨c, cNat, d, dNat, yShape⟩ := Integer.representatives at y with *188  obtain ⟨e, eNat, f, fNat, zShape⟩ := Integer.representatives at z with *189  simp [integerAddValue.classes, integerClassSum]190  apply integerClass.eq with *{4}191  ring192193theorem integerMulValue.associative (x y z : Integer)194  shows (x * y) * z = x * (y * z)195proof196  obtain ⟨a, aNat, b, bNat, xShape⟩ := Integer.representatives at x with *197  obtain ⟨c, cNat, d, dNat, yShape⟩ := Integer.representatives at y with *198  obtain ⟨e, eNat, f, fNat, zShape⟩ := Integer.representatives at z with *199  simp [integerMulValue.classes, integerClassMul]200  apply integerClass.eq with *{4}201  ring202203theorem integerMulValue.distribute_right (x y z : Integer)204  shows x * (y + z) = x * y + x * z205proof206  obtain ⟨a, aNat, b, bNat, xShape⟩ := Integer.representatives at x with *207  obtain ⟨c, cNat, d, dNat, yShape⟩ := Integer.representatives at y with *208  obtain ⟨e, eNat, f, fNat, zShape⟩ := Integer.representatives at z with *209  simp [integerAddValue.classes, integerClassSum, integerMulValue.classes, integerClassMul]210  apply integerClass.eq with *{4}211  ring212213theorem integerOfNat.add (a b : Nat)214  shows integerOfNat(a + b) = integerAddValue(integerOfNat(a), integerOfNat(b))215proof216  simp [integerOfNat, integerAddValue.classes, integerClassSum, add]217218theorem integerOfNat.mul (a b : Nat)219  shows integerOfNat(a * b) = integerMulValue(integerOfNat(a), integerOfNat(b))220proof221  simp [integerOfNat, integerMulValue.classes, integerClassMul, mul.right_zero, mul, add.right_unit, add]222223theorem integerMulValue.neg_left (x y : Integer)224  shows (-x) * y = -(x * y)225proof226  obtain ⟨a, aNat, b, bNat, xShape⟩ := Integer.representatives at x with *227  obtain ⟨c, cNat, d, dNat, yShape⟩ := Integer.representatives at y with *228  simp [integerNegValue.classes, integerClassNeg, integerMulValue.classes, integerClassMul]229  apply integerClass.eq with *{4}230  ring231232theorem integerMulValue.neg_right (x y : Integer)233  shows x * (-y) = -(x * y)234proof235  obtain ⟨a, aNat, b, bNat, xShape⟩ := Integer.representatives at x with *236  obtain ⟨c, cNat, d, dNat, yShape⟩ := Integer.representatives at y with *237  simp [integerNegValue.classes, integerClassNeg, integerMulValue.classes, integerClassMul]238239theorem integerMulValue.neg_both (x y : Integer)240  shows (-x) * (-y) = x * y241proof242  simp [integerMulValue.neg_left, integerMulValue.neg_right, integerNegValue.involutive]243244theorem integerMulValue.ofNat (m n : Nat)245  shows integerOfNat(m) * integerOfNat(n) = integerOfNat(m * n)246proof247  symm248  exact integerOfNat.mul with *249250theorem integerMulValue.ofNat_negative (m n : Nat)251  shows integerOfNat(m) * integerNegativeOfNat(n) = integerNegativeOfNat(m * n)252proof253  simp [integerOfNat, integerNegativeOfNat, integerMulValue.classes, integerClassMul, mul.right_zero, mul, add.right_unit, add]254255theorem integerMulValue.negative_ofNat (m n : Nat)256  shows integerNegativeOfNat(m) * integerOfNat(n) = integerNegativeOfNat(m * n)257proof258  simp [integerOfNat, integerNegativeOfNat, integerMulValue.classes, integerClassMul, mul.right_zero, mul, add.right_unit, add]259260theorem integerMulValue.negative_negative (m n : Nat)261  shows integerNegativeOfNat(m) * integerNegativeOfNat(n) = integerOfNat(m * n)262proof263  simp [integerOfNat, integerNegativeOfNat, integerMulValue.classes, integerClassMul, mul.right_zero, mul, add.right_unit, add]264