Grace/Cumulus/Int/Core.g17

Open in Workbench Download source

Imports

Defs

Declarations

• integerClass def
• integerZero def
• integerOfNat def
• integerNegativeOfNat def
• integerClass.membership theorem derivation
• integerClass.integer theorem derivation
• integerClass.eq theorem derivation
• integerZero.integer theorem derivation
• integerOfNat.integer theorem derivation
• integerNegativeOfNat.integer theorem derivation
• integerOfNat.zero theorem derivation
• Integer.representatives theorem derivation
• integerClass.equivalent_of_eq theorem derivation
• integerOfNat.injective theorem derivation

Source

1-- Canonical integer classes2-- 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.Core8import Defs910def integerClass (a b : Set) : Set :=11  ⟦(a, b)⟧[integerPairs, integerEquivalent]1213def integerZero : Integer := integerClass(0, 0)14def integerOfNat (n : Nat) : Integer := integerClass(n, 0)15def integerNegativeOfNat (n : Nat) : Integer := integerClass(0, n)1617theorem integerClass.membership (p a b : Set)18  shows p ∈ integerClass(a, b) ↔ (p ∈ integerPairs ∧ relates(integerEquivalent, (a, b), p))19proof20  simp [integerClass, equivalenceClass.membership]2122theorem integerClass.integer (a b : Nat)23  shows Integer(integerClass(a, b))24proof25  unfold Integer26  unfold ℤ27  unfold integerClass28  apply quotient.contains_class29  . exact integerEquivalent.equivalence30  . exact integerPairs.pair at a, b3132theorem integerClass.eq (a b c d : Nat)33  requires equivalent : add(a, d) = add(c, b)34  shows integerClass(a, b) = integerClass(c, d)35proof36  unfold integerClass37  apply equivalenceClass.eq38  . exact integerEquivalent.equivalence39  . exact integerPairs.pair at a, b40  . exact integerPairs.pair at c, d41  . have characterization := integerEquivalent.relates_pairs at a, b, c, d42    apply characterization.backward43    exact equivalent4445theorem integerZero.integer46  shows Integer(integerZero)47proof48  unfold integerZero49  exact integerClass.integer with Naturals.constructor.zero, Naturals.constructor.zero5051theorem integerOfNat.integer (n : Nat)52  shows Integer(integerOfNat(n))53proof54  unfold integerOfNat55  exact integerClass.integer with Naturals.constructor.zero5657theorem integerNegativeOfNat.integer (n : Nat)58  shows Integer(integerNegativeOfNat(n))59proof60  unfold integerNegativeOfNat61  exact integerClass.integer with Naturals.constructor.zero6263theorem integerOfNat.zero64  shows integerOfNat(0) = integerZero65proof66  simp6768-- Every integer is represented by a difference of two naturals.69theorem Integer.representatives (z : Set)70  requires integer : Integer(z)71  shows ∃ a, Nat(a) ∧ ∃ b, Nat(b) ∧ z = integerClass(a, b)72proof73  unfold Integer at integer74  unfold ℤ at integer75  obtain ⟨bounded, p, pair, shape⟩ := quotient.membership.forward with integer76  obtain ⟨a, aNat, b, bNat, coordinates⟩ := integerPairs.coordinates with pair77  witness a78  witness b79  unfold integerClass80  rw ← coordinates81  exact shape8283theorem integerClass.equivalent_of_eq (a b c d : Nat)84  requires same : integerClass(a, b) = integerClass(c, d)85  shows a + d = c + b86proof87  have left := integerPairs.pair at a, b with *88  have right := integerPairs.pair at c, d with *89  simp [integerClass] at same90  have related := equivalenceClass.related_of_eq with integerEquivalent.equivalence, left, right, same91  exact integerEquivalent.relates_pairs.forward with *9293theorem integerOfNat.injective (a b : Nat)94  requires same : integerOfNat(a) = integerOfNat(b)95  shows a = b96proof97  simp [integerOfNat] at same98  have sums := integerClass.equivalent_of_eq with *99  simpa [add.right_unit] using sums100