Grace/Cumulus/Int/Defs.g17

Open in Workbench Download source

Imports

Relation.Quotient · Nat

Declarations

Source

1-- Integers as a quotient of pairs of natural numbers2-- 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.Defs8import Relation.Quotient9import Nat1011-- The pair (a,b) represents the formal difference a - b.  Two pairs12-- represent the same integer precisely when their cross-sums agree.13def integerPairs : Set := ℕ × ℕ14def integerEquivalent : Set :=15  { p ∈ integerPairs × integerPairs |16    ∃ a ∈ ℕ, ∃ b ∈ ℕ,17    ∃ c ∈ ℕ, ∃ d ∈ ℕ,18      p = ((a, b), (c, d)) ∧19      add(a, d) = add(c, b) }2021def ℤ : Set := (integerPairs ⧸ integerEquivalent)22class Integer (z : Set) := z ∈ ℤ2324theorem integerPairs.membership (p : Set)25  shows p ∈ integerPairs ↔ p ∈ ℕ × ℕ26proof27  simp [integerPairs]2829theorem integerPairs.pair (a b : Nat)30  shows (a, b) ∈ integerPairs31proof32  simp [integerPairs, product.pair, nat.omega]3334theorem integerPairs.coordinates (p : Set)35  requires hp : p ∈ integerPairs36  shows ∃ a, Nat(a) ∧ ∃ b, Nat(b) ∧ p = (a, b)37proof38  unfold integerPairs at hp39  simp [product.membership] at hp40  rcases hp with ⟨bounded, a, haNat, b, hbNat, shape⟩41  witness a42  witness b43  exact shape4445theorem integerEquivalent.relates_pairs (a b c d : Nat)46  shows relates(integerEquivalent, (a, b), (c, d)) ↔ add(a, d) = add(c, b)47proof48  constructor49  . intro h50    unfold relates at h51    simp [integerEquivalent.membership] at h52    rcases h with ⟨bounded, w, hwNat, x, hxNat, y, hyNat, z, hzNat, shape, sums⟩53    obtain ⟨leftShape, rightShape⟩ := orderedPair.injective with shape54    have left := orderedPair.injective with leftShape55    have right := orderedPair.injective with rightShape56    rcases left with ⟨aw, bx⟩57    rcases right with ⟨cy, dz⟩58    simp59  . intro sums60    unfold relates61    apply integerEquivalent.membership.backward62    constructor63    . apply product.pair at (a, b), (c, d), integerPairs, integerPairs64      . exact integerPairs.pair with *{2}65      . exact integerPairs.pair with *{2}66    . witness a67      constructor68      . settle with nat.omega69      . witness b70        constructor71        . settle with nat.omega72        . witness c73          constructor74          . settle with nat.omega75          . witness d76            constructor77            . settle with nat.omega78            refine ⟨rfl, sums⟩7980theorem integerEquivalent.reflexive_pair (a b : Nat)81  shows relates(integerEquivalent, (a, b), (a, b))82proof83  unfold relates84  apply integerEquivalent.membership.backward85  constructor86  . apply product.pair at (a, b), (a, b), integerPairs, integerPairs87    . exact integerPairs.pair with *{2}88    . exact integerPairs.pair with *{2}89  . witness a90    constructor91    . settle with nat.omega92    . witness b93      constructor94      . settle with nat.omega95      . witness a96        constructor97        . settle with nat.omega98        . witness b99          constructor100          . settle with nat.omega101          refine ⟨rfl, rfl⟩102103theorem integerEquivalent.cross_symmetric (a b c d : Nat)104  requires h : add(a, d) = add(c, b)105  shows add(c, b) = add(a, d)106proof107  simp108109lemma integerEquivalent.cross_combined (a b c d e f : Nat)110  requires hxy : add(a, d) = add(c, b)111  requires hyz : add(c, f) = add(e, d)112  shows add(add(a, f), d) = add(add(e, b), d)113proof114  have leftSwap := add.swap_last at a, f, d with *115  have middleSwap := add.swap_last at c, b, f with *116  have rightSwap := add.swap_last at e, b, d with *117  simp118119theorem integerEquivalent.cross_transitive (a b c d e f : Nat)120  requires hxy : add(a, d) = add(c, b)121  requires hyz : add(c, f) = add(e, d)122  shows add(a, f) = add(e, b)123proof124  have combined := integerEquivalent.cross_combined at a, b, c, d, e, f with *125  exact add.right_cancel with combined126127theorem integerEquivalent.relation128  shows RelationOn(integerEquivalent, integerPairs)129proof130  intros p hp131  simp [integerEquivalent.membership] at hp132  rcases hp with ⟨bounded, witnesses⟩133  exact bounded134135theorem integerEquivalent.reflexive136  shows ReflexiveOn(integerPairs, integerEquivalent)137proof138  intros p hp139  obtain ⟨a, haNat, b, hbNat, shape⟩ := integerPairs.coordinates with hp140  rw shape141  exact integerEquivalent.reflexive_pair with haNat, hbNat142143theorem integerEquivalent.symmetric144  shows SymmetricOn(integerPairs, integerEquivalent)145proof146  intros p hp q hq hpq147  obtain ⟨a, haNat, b, hbNat, pShape⟩ := integerPairs.coordinates with hp148  obtain ⟨c, hcNat, d, hdNat, qShape⟩ := integerPairs.coordinates with hq149  rw [pShape, qShape] at hpq150  rw [pShape, qShape]151  have characterization := integerEquivalent.relates_pairs with haNat, hbNat, hcNat, hdNat152  have sums := characterization.forward with hpq153  have reverse := integerEquivalent.cross_symmetric with haNat, hbNat, hcNat, hdNat, sums154  have reverseCharacterization := integerEquivalent.relates_pairs with hcNat, hdNat, haNat, hbNat155  apply reverseCharacterization.backward156  exact reverse157158theorem integerEquivalent.transitive159  shows TransitiveOn(integerPairs, integerEquivalent)160proof161  intros p hp q hq r hr hpq hqr162  obtain ⟨a, haNat, b, hbNat, pShape⟩ := integerPairs.coordinates with hp163  obtain ⟨c, hcNat, d, hdNat, qShape⟩ := integerPairs.coordinates with hq164  obtain ⟨e, heNat, f, hfNat, rShape⟩ := integerPairs.coordinates with hr165  rw [pShape, qShape] at hpq166  rw [qShape, rShape] at hqr167  rw [pShape, rShape]168  have firstCharacterization := integerEquivalent.relates_pairs with haNat, hbNat, hcNat, hdNat169  have firstSums := firstCharacterization.forward with hpq170  have secondCharacterization := integerEquivalent.relates_pairs with hcNat, hdNat, heNat, hfNat171  have secondSums := secondCharacterization.forward with hqr172  have combined := integerEquivalent.cross_transitive with haNat, hbNat, hcNat, hdNat, heNat, hfNat, firstSums, secondSums173  have resultCharacterization := integerEquivalent.relates_pairs with haNat, hbNat, heNat, hfNat174  apply resultCharacterization.backward175  exact combined176177theorem integerEquivalent.equivalence178  shows Equivalence(integerPairs, integerEquivalent)179proof180  refine ⟨integerEquivalent.relation, integerEquivalent.reflexive, integerEquivalent.symmetric, integerEquivalent.transitive⟩181182theorem integers.membership (z : Set)183  shows z ∈ ℤ ↔ z ∈ (integerPairs ⧸ integerEquivalent)184proof185  simp [ℤ]186