-- Integers as a quotient of pairs of natural numbers -- Part of Cumulus, the Grace17 mathematics library. -- Copyright (c) 2026 Grant Passmore. -- Released under the Apache License 2.0. See LICENSE in the repository root. -- Authors: Grant Passmore module Grace.Cumulus.Int.Defs import Relation.Quotient import Nat -- The pair (a,b) represents the formal difference a - b. Two pairs -- represent the same integer precisely when their cross-sums agree. def integerPairs : Set := ℕ × ℕ def integerEquivalent : Set := { p ∈ integerPairs × integerPairs | ∃ a ∈ ℕ, ∃ b ∈ ℕ, ∃ c ∈ ℕ, ∃ d ∈ ℕ, p = ((a, b), (c, d)) ∧ add(a, d) = add(c, b) } def ℤ : Set := (integerPairs ⧸ integerEquivalent) class Integer (z : Set) := z ∈ ℤ theorem integerPairs.membership (p : Set) shows p ∈ integerPairs ↔ p ∈ ℕ × ℕ proof simp [integerPairs] theorem integerPairs.pair (a b : Nat) shows (a, b) ∈ integerPairs proof simp [integerPairs, product.pair, nat.omega] theorem integerPairs.coordinates (p : Set) requires hp : p ∈ integerPairs shows ∃ a, Nat(a) ∧ ∃ b, Nat(b) ∧ p = (a, b) proof unfold integerPairs at hp simp [product.membership] at hp rcases hp with ⟨bounded, a, haNat, b, hbNat, shape⟩ witness a witness b exact shape theorem integerEquivalent.relates_pairs (a b c d : Nat) shows relates(integerEquivalent, (a, b), (c, d)) ↔ add(a, d) = add(c, b) proof constructor . intro h unfold relates at h simp [integerEquivalent.membership] at h rcases h with ⟨bounded, w, hwNat, x, hxNat, y, hyNat, z, hzNat, shape, sums⟩ obtain ⟨leftShape, rightShape⟩ := orderedPair.injective with shape have left := orderedPair.injective with leftShape have right := orderedPair.injective with rightShape rcases left with ⟨aw, bx⟩ rcases right with ⟨cy, dz⟩ simp . intro sums unfold relates apply integerEquivalent.membership.backward constructor . apply product.pair at (a, b), (c, d), integerPairs, integerPairs . exact integerPairs.pair with *{2} . exact integerPairs.pair with *{2} . witness a constructor . settle with nat.omega . witness b constructor . settle with nat.omega . witness c constructor . settle with nat.omega . witness d constructor . settle with nat.omega refine ⟨rfl, sums⟩ theorem integerEquivalent.reflexive_pair (a b : Nat) shows relates(integerEquivalent, (a, b), (a, b)) proof unfold relates apply integerEquivalent.membership.backward constructor . apply product.pair at (a, b), (a, b), integerPairs, integerPairs . exact integerPairs.pair with *{2} . exact integerPairs.pair with *{2} . witness a constructor . settle with nat.omega . witness b constructor . settle with nat.omega . witness a constructor . settle with nat.omega . witness b constructor . settle with nat.omega refine ⟨rfl, rfl⟩ theorem integerEquivalent.cross_symmetric (a b c d : Nat) requires h : add(a, d) = add(c, b) shows add(c, b) = add(a, d) proof simp lemma integerEquivalent.cross_combined (a b c d e f : Nat) requires hxy : add(a, d) = add(c, b) requires hyz : add(c, f) = add(e, d) shows add(add(a, f), d) = add(add(e, b), d) proof have leftSwap := add.swap_last at a, f, d with * have middleSwap := add.swap_last at c, b, f with * have rightSwap := add.swap_last at e, b, d with * simp theorem integerEquivalent.cross_transitive (a b c d e f : Nat) requires hxy : add(a, d) = add(c, b) requires hyz : add(c, f) = add(e, d) shows add(a, f) = add(e, b) proof have combined := integerEquivalent.cross_combined at a, b, c, d, e, f with * exact add.right_cancel with combined theorem integerEquivalent.relation shows RelationOn(integerEquivalent, integerPairs) proof intros p hp simp [integerEquivalent.membership] at hp rcases hp with ⟨bounded, witnesses⟩ exact bounded theorem integerEquivalent.reflexive shows ReflexiveOn(integerPairs, integerEquivalent) proof intros p hp obtain ⟨a, haNat, b, hbNat, shape⟩ := integerPairs.coordinates with hp rw shape exact integerEquivalent.reflexive_pair with haNat, hbNat theorem integerEquivalent.symmetric shows SymmetricOn(integerPairs, integerEquivalent) proof intros p hp q hq hpq obtain ⟨a, haNat, b, hbNat, pShape⟩ := integerPairs.coordinates with hp obtain ⟨c, hcNat, d, hdNat, qShape⟩ := integerPairs.coordinates with hq rw [pShape, qShape] at hpq rw [pShape, qShape] have characterization := integerEquivalent.relates_pairs with haNat, hbNat, hcNat, hdNat have sums := characterization.forward with hpq have reverse := integerEquivalent.cross_symmetric with haNat, hbNat, hcNat, hdNat, sums have reverseCharacterization := integerEquivalent.relates_pairs with hcNat, hdNat, haNat, hbNat apply reverseCharacterization.backward exact reverse theorem integerEquivalent.transitive shows TransitiveOn(integerPairs, integerEquivalent) proof intros p hp q hq r hr hpq hqr obtain ⟨a, haNat, b, hbNat, pShape⟩ := integerPairs.coordinates with hp obtain ⟨c, hcNat, d, hdNat, qShape⟩ := integerPairs.coordinates with hq obtain ⟨e, heNat, f, hfNat, rShape⟩ := integerPairs.coordinates with hr rw [pShape, qShape] at hpq rw [qShape, rShape] at hqr rw [pShape, rShape] have firstCharacterization := integerEquivalent.relates_pairs with haNat, hbNat, hcNat, hdNat have firstSums := firstCharacterization.forward with hpq have secondCharacterization := integerEquivalent.relates_pairs with hcNat, hdNat, heNat, hfNat have secondSums := secondCharacterization.forward with hqr have combined := integerEquivalent.cross_transitive with haNat, hbNat, hcNat, hdNat, heNat, hfNat, firstSums, secondSums have resultCharacterization := integerEquivalent.relates_pairs with haNat, hbNat, heNat, hfNat apply resultCharacterization.backward exact combined theorem integerEquivalent.equivalence shows Equivalence(integerPairs, integerEquivalent) proof refine ⟨integerEquivalent.relation, integerEquivalent.reflexive, integerEquivalent.symmetric, integerEquivalent.transitive⟩ theorem integers.membership (z : Set) shows z ∈ ℤ ↔ z ∈ (integerPairs ⧸ integerEquivalent) proof simp [ℤ]