Grace/Cumulus/Int/Ring.g17

Open in Workbench Download source

Imports

Arithmetic · Algebra.Ring.Core

Declarations

Source

1-- Commutative-ring interface for 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.Ring8import Arithmetic9import Algebra.Ring.Core1011defunique integerAddPairValue (p : Set) (z ∈ ℤ) :=12  ∃ x ∈ ℤ, ∃ y ∈ ℤ, p = (x, y) ∧ z = integerAddValue(x, y)13requires pair : p ∈ ℤ × ℤ14proof15  have shape := product.membership.forward at ℤ, ℤ, p with pair16  rcases shape with ⟨bound, x, xMember, y, yMember, equation⟩17  have xInteger : Integer(x)18  . typecheck19  have yInteger : Integer(y)20  . typecheck21  have result := integerAddValue.integer at x, y with *22  unfold Integer at result23  witness integerAddValue(x, y)24  refine ⟨result, x, xMember, y, yMember, equation, rfl⟩2526uniqueness27  intros z zMember zProperty w wMember wProperty28  obtain ⟨a, aMember, b, bMember, shape, value⟩ := zProperty29  obtain ⟨c, cMember, d, dMember, otherShape, otherValue⟩ := wProperty30  have same : (a, b) = (c, d)31    cc32  have coordinates := orderedPair.injective at a, b, c, d with same33  rcases coordinates with ⟨left, right⟩34  cc3536defgraph integerAdd (p ∈ ℤ × ℤ) : ℤ := integerAddPairValue(p)37proof38  have selected := integerAddPairValue.selected at p with member39  tauto4041theorem integerAddValue.notation (x y : Integer)42  shows call2(integerAdd, x, y) = integerAddValue(x, y)43proof44  have xMember : x ∈ ℤ45  . settle with Integer46  have yMember : y ∈ ℤ47  . settle with Integer48  have pair := product.pair at x, y, ℤ, ℤ with *49  have evaluated := integerAdd.value at (x, y) with *50  have selected := integerAddPairValue.selected at (x, y) with *51  rcases selected with ⟨member, a, aMember, b, bMember, shape, value⟩52  obtain ⟨left, right⟩ := orderedPair.injective with shape53  unfold call254  cc5556defunique integerMulPairValue (p : Set) (z ∈ ℤ) :=57  ∃ x ∈ ℤ, ∃ y ∈ ℤ, p = (x, y) ∧ z = integerMulValue(x, y)58requires pair : p ∈ ℤ × ℤ59proof60  obtain ⟨bound, x, xMember, y, yMember, equation⟩ := product.membership.forward with pair61  have xInteger : Integer(x)62  . typecheck63  have yInteger : Integer(y)64  . typecheck65  have result := integerMulValue.integer at x, y with *66  witness integerMulValue(x, y)67  refine ⟨result, x, xMember, y, yMember, equation, rfl⟩6869uniqueness70  intros z zMember zProperty w wMember wProperty71  obtain ⟨a, aMember, b, bMember, shape, value⟩ := zProperty72  obtain ⟨c, cMember, d, dMember, otherShape, otherValue⟩ := wProperty73  have same : (a, b) = (c, d) by cc74  obtain ⟨left, right⟩ := orderedPair.injective with same75  cc7677defgraph integerMul (p ∈ ℤ × ℤ) : ℤ := integerMulPairValue(p)78proof79  have selected := integerMulPairValue.selected with member80  tauto8182theorem integerMulValue.notation (x y : Integer)83  shows call2(integerMul, x, y) = integerMulValue(x, y)84proof85  have xMember : x ∈ ℤ86  . settle with Integer87  have yMember : y ∈ ℤ88  . settle with Integer89  have pair := product.pair at x, y, ℤ, ℤ with *90  have evaluated := integerMul.value at (x, y) with *91  have selected := integerMulPairValue.selected at (x, y) with *92  rcases selected with ⟨member, a, aMember, b, bMember, shape, value⟩93  obtain ⟨left, right⟩ := orderedPair.injective with shape94  unfold call295  cc9697defgraph integerNeg (x ∈ ℤ) : ℤ := integerNegValue(x)98proof99  . typecheck100101theorem integerNegValue.notation (x : Integer)102  shows integerNeg(x) = integerNegValue(x)103proof104  have member : x ∈ ℤ105  . settle with Integer106  exact integerNeg.value at x with *107108def integerOne : Integer := integerOfNat(1)109110theorem integerOne.integer111  shows Integer(integerOne)112proof113  unfold integerOne114  exact integerOfNat.integer with *115116theorem integerAddValue.zero_left (x : Integer)117  shows integerZero + x = x118proof119  rw integerAddValue.commutative120  exact integerAddValue.zero_right with *121122theorem integerAddValue.neg_left (x : Integer)123  shows (-x) + x = integerZero124proof125  rw integerAddValue.commutative126  exact integerAddValue.neg_right with *127128theorem integerMulValue.one_right (x : Integer)129  shows x * integerOne = x130proof131  obtain ⟨a, aNat, b, bNat, shape⟩ := Integer.representatives at x with *132  simp [integerOne, integerOfNat, integerMulValue.classes, integerClassMul, mul.right_unit, mul.right_zero, add.right_unit, add]133134theorem integerMulValue.one_left (x : Integer)135  shows integerOne * x = x136proof137  rw integerMulValue.commutative138  exact integerMulValue.one_right with *139140theorem integerMulValue.distribute_left (x y z : Integer)141  shows (x + y) * z = x * z + y * z142proof143  have left := integerMulValue.commutative at x, z with *144  have right := integerMulValue.commutative at y, z with *145  have outer := integerMulValue.commutative at x + y, z with *146  have distribution := integerMulValue.distribute_right at z, x, y with *147  rw [outer, distribution, ← left, ← right]148  rfl149150instance integerAdd.comm_monoid151  shows IsCommMonoid(ℤ, integerAdd, integerZero)152proof153  constructor154    constructor155      constructor156        exact integerAdd.function157        intros A integerA B integerB C integerC158        have typedA : Integer(A) by typecheck159        have typedB : Integer(B) by typecheck160        have typedC : Integer(C) by typecheck161        simpa [integerAddValue.notation] using integerAddValue.associative at A, B, C with typedA, typedB, typedC162      constructor163      . exact integerZero.integer164      . intros A integerA165        have typedA : Integer(A) by typecheck166        constructor167        . simpa [integerAddValue.notation] using integerAddValue.zero_left at A with typedA168        . simpa [integerAddValue.notation] using integerAddValue.zero_right at A with typedA169    intros A integerA B integerB170    have typedA : Integer(A) by typecheck171    have typedB : Integer(B) by typecheck172    simpa [integerAddValue.notation] using integerAddValue.commutative at A, B with typedA, typedB173174instance integerAdd.abelian_group175  shows IsAbelianGroup(ℤ, integerAdd, integerZero, integerNeg)176proof177  constructor178    constructor179    . have additive := integerAdd.comm_monoid180      simp [IsCommMonoid]181      constructor182      . exact integerNeg.function183      . intros A integerA184        have typedA : Integer(A) by typecheck185        constructor186        . simpa [integerAddValue.notation, integerNegValue.notation] using integerAddValue.neg_left at A with typedA187        . simpa [integerAddValue.notation, integerNegValue.notation] using integerAddValue.neg_right at A with typedA188  . have additive := integerAdd.comm_monoid189    simp [IsCommMonoid]190191instance integerMul.monoid192  shows IsMonoid(ℤ, integerMul, integerOne)193proof194  constructor195    constructor196      exact integerMul.function197      intros A integerA B integerB C integerC198      have typedA : Integer(A) by typecheck199      have typedB : Integer(B) by typecheck200      have typedC : Integer(C) by typecheck201      simpa [integerMulValue.notation] using integerMulValue.associative at A, B, C with typedA, typedB, typedC202    constructor203    . exact integerOne.integer204    . intros A integerA205      have typedA : Integer(A) by typecheck206      constructor207      . simpa [integerMulValue.notation] using integerMulValue.one_left at A with typedA208      . simpa [integerMulValue.notation] using integerMulValue.one_right at A with typedA209210instance integerMul.distributive211  shows Distributive(ℤ, integerAdd, integerMul)212proof213  intros A integerA B integerB C integerC214  have typedA : Integer(A) by typecheck215  have typedB : Integer(B) by typecheck216  have typedC : Integer(C) by typecheck217  constructor218  . simpa [integerAddValue.notation, integerMulValue.notation] using integerMulValue.distribute_right at A, B, C with typedA, typedB, typedC219  . simpa [integerAddValue.notation, integerMulValue.notation] using integerMulValue.distribute_left at A, B, C with typedA, typedB, typedC220221instance integerMul.commutative222  shows Commutative(ℤ, integerMul)223proof224  intros A integerA B integerB225  have typedA : Integer(A) by typecheck226  have typedB : Integer(B) by typecheck227  simpa [integerMulValue.notation] using integerMulValue.commutative at A, B with typedA, typedB228229instance integers.comm_ring230  shows IsCommRing(ℤ, integerAdd, integerZero, integerNeg, integerMul,231    integerOne)232proof233  constructor234    constructor235    . exact integerAdd.abelian_group236    . constructor237      . exact integerMul.monoid238      . exact integerMul.distributive239  . exact integerMul.commutative240241242instance integerZero.of_nat243  shows OfNat(ℤ, 0, integerZero)244proof245  constructor246  . typecheck247  . exact integerZero.integer248249instance integerOne.of_nat250  shows OfNat(ℤ, 1, integerOne)251proof252  constructor253  . typecheck254  . exact integerOne.integer255256notation numeral "0" via OfNat(ℤ, 0, _) for Integer257notation numeral "1" via OfNat(ℤ, 1, _) for Integer258259def integerSubValue (x y : Integer) : Integer := call2(integerAdd, x, integerNeg(y))260notation infixl 60 "-" => integerSubValue for Integer261262theorem integerSubValue.integer (x y : Integer)263  shows Integer(x - y)264proof265  have sum := integerAddValue.integer at x, integerNegValue(y) with *266  simpa [integerSubValue, integerAddValue.notation, integerNegValue.notation] using sum267