Grace/Cumulus/Real/Integer.g17

Open in Workbench Download source

Imports

RootTwo · Int

Declarations

• realInt defunique
• realInt.real theorem derivation
• realInt.class theorem derivation
• realInt.nat theorem derivation
• realInt.zero theorem derivation
• realInt.one theorem derivation
• realInt.add theorem derivation
• realInt.neg theorem derivation
• realInt.mul theorem derivation
• realInt.sub theorem derivation
• realInt.injective theorem derivation
• realInt.range theorem derivation

Source

1-- The integers inside the reals: the embedding realInt sends the class of2-- (a, b) to a - b; it is an injective ring homomorphism agreeing with3-- realNat on the naturals, and its image is the set of differences of4-- naturals5-- Part of Cumulus, the Grace17 mathematics library.6-- Copyright (c) 2026 Grant Passmore.7-- Released under the Apache License 2.0. See LICENSE in the repository root.8-- Authors: Grant Passmore910module Grace.Cumulus.Real.Integer11import RootTwo12import Int1314-- The real number of an integer: the class of (a, b) goes to a - b, which15-- does not depend on the representative.16defunique realInt (z : Set) (x ∈ ℝ) :=17  ∃ a, Nat(a) ∧ ∃ b, Nat(b) ∧ z = integerClass(a, b) ∧18    x = (realNat(a):R) - (realNat(b):R)19requires integer : Integer(z)20proof21  obtain ⟨a, ha, b, hb, shape⟩ := Integer.representatives at z with *22  have realA := realNat.real at a with ha23  have realB := realNat.real at b with hb24  have value : (realNat(a):R) - (realNat(b):R) ∈ ℝ by typecheck25  refine ⟨(realNat(a):R) - (realNat(b):R), value, a, ha, b, hb, shape, rfl⟩26uniqueness27  intros u hu first v hv second28  obtain ⟨a, ha, b, hb, shapeA, valueA⟩ := first29  obtain ⟨c, hc, d, hd, shapeC, valueC⟩ := second30  have same : integerClass(a, b) = integerClass(c, d)31    rw [← shapeA, ← shapeC]32    rfl33  have cross := integerClass.equivalent_of_eq at a, b, c, d with ha, hb, hc, hd, same34  have realA := realNat.real at a with ha35  have realB := realNat.real at b with hb36  have realC := realNat.real at c with hc37  have realD := realNat.real at d with hd38  have realCross : (realNat(a):R) + (realNat(d):R) = (realNat(c):R) + (realNat(b):R)39    rw [← realNat.add, ← realNat.add, cross]40    rfl41  rw [valueA, valueC]42  linarith4344theorem realInt.real (z : Integer)45  shows realInt(z) ∈ ℝ46proof47  have selected := realInt.selected at z with *48  exact selected.left4950-- The value on a class.51theorem realInt.class (a b : Nat)52  shows realInt(integerClass(a, b)) = (realNat(a):R) - (realNat(b):R)53proof54  have integer := integerClass.integer at a, b with *55  have selected := realInt.selected at integerClass(a, b) with integer56  obtain ⟨c, hc, d, hd, same, value⟩ := selected.right57  have cross := integerClass.equivalent_of_eq at a, b, c, d with *58  have realA := realNat.real at a59  have realB := realNat.real at b60  have realC := realNat.real at c with hc61  have realD := realNat.real at d with hd62  have realCross : (realNat(a):R) + (realNat(d):R) = (realNat(c):R) + (realNat(b):R)63    rw [← realNat.add, ← realNat.add, cross]64    rfl65  rw value66  linarith6768-- Agreement with realNat on the naturals, and the values at 0 and 1.69theorem realInt.nat (n : Nat)70  shows realInt(integerOfNat(n)) = realNat(n)71proof72  have realN := realNat.real at n73  unfold integerOfNat74  rw [realInt.class, realNat.zero]75  ring7677theorem realInt.zero78  shows realInt(integerZero) = (0:R)79proof80  unfold integerZero81  rw [realInt.class, realNat.zero]82  ring8384theorem realInt.one85  shows realInt(integerOne) = (1:R)86proof87  unfold integerOne88  rw [realInt.nat, realNat.one]89  rfl9091-- The ring homomorphism laws.92theorem realInt.add (m n : Integer)93  shows realInt(m + n) = (realInt(m):R) + (realInt(n):R)94proof95  obtain ⟨a, ha, b, hb, shapeM⟩ := Integer.representatives at m with *96  obtain ⟨c, hc, d, hd, shapeN⟩ := Integer.representatives at n with *97  have realA := realNat.real at a with ha98  have realB := realNat.real at b with hb99  have realC := realNat.real at c with hc100  have realD := realNat.real at d with hd101  have sum := integerAddValue.classes at a, b, c, d with *102  rw [shapeM, shapeN, sum]103  unfold integerClassSum104  rw [realInt.class, realInt.class, realInt.class, realNat.add, realNat.add]105  ring106107theorem realInt.neg (n : Integer)108  shows realInt(-n) = -(realInt(n):R)109proof110  obtain ⟨c, hc, d, hd, shapeN⟩ := Integer.representatives at n with *111  have realC := realNat.real at c with hc112  have realD := realNat.real at d with hd113  have negative := integerNegValue.classes at c, d with *114  rw [shapeN, negative]115  unfold integerClassNeg116  rw [realInt.class, realInt.class]117  ring118119theorem realInt.mul (m n : Integer)120  shows realInt(m * n) = (realInt(m):R) * (realInt(n):R)121proof122  obtain ⟨a, ha, b, hb, shapeM⟩ := Integer.representatives at m with *123  obtain ⟨c, hc, d, hd, shapeN⟩ := Integer.representatives at n with *124  have realA := realNat.real at a with ha125  have realB := realNat.real at b with hb126  have realC := realNat.real at c with hc127  have realD := realNat.real at d with hd128  have product := integerMulValue.classes at a, b, c, d with *129  rw [shapeM, shapeN, product]130  unfold integerClassMul131  rw [realInt.class, realInt.class, realInt.class, realNat.add, realNat.add,132    realNat.mul, realNat.mul, realNat.mul, realNat.mul]133  ring134135theorem realInt.sub (m n : Integer)136  shows realInt(m - n) = (realInt(m):R) - (realInt(n):R)137proof138  have negative := integerNegValue.integer at n with *139  have realM := realInt.real at m with *140  have realN := realInt.real at n with *141  unfold integerSubValue142  rw [integerAddValue.notation, integerNegValue.notation, realInt.add, realInt.neg]143  ring144145-- The embedding is injective.146theorem realInt.injective (m n : Integer)147  requires equal : realInt(m) = realInt(n)148  shows m = n149proof150  obtain ⟨a, ha, b, hb, shapeM⟩ := Integer.representatives at m with *151  obtain ⟨c, hc, d, hd, shapeN⟩ := Integer.representatives at n with *152  have realA := realNat.real at a with ha153  have realB := realNat.real at b with hb154  have realC := realNat.real at c with hc155  have realD := realNat.real at d with hd156  rw [shapeM, shapeN, realInt.class, realInt.class] at equal157  have cross : (realNat(a):R) + (realNat(d):R) = (realNat(c):R) + (realNat(b):R)158    linarith159  rw [← realNat.add, ← realNat.add] at cross160  have natural := realNat.injective at a + d, c + b with cross161  rw [shapeM, shapeN]162  exact integerClass.eq at a, b, c, d with natural163164-- An integer is written as a real wherever a real is expected.165notation coercion realInt for Integer, Real166167-- The image of ℤ in ℝ is the set of differences of naturals.168theorem realInt.range (x : Set)169  shows (∃ z ∈ ℤ, x = realInt(z)) ↔170    ∃ m ∈ ℕ, ∃ n ∈ ℕ, x = (realNat(m):R) - (realNat(n):R)171proof172  constructor173  . intro image174    obtain ⟨z, hz, shape⟩ := image175    obtain ⟨a, ha, b, hb, zShape⟩ := Integer.representatives at z with hz176    have value := realInt.class at a, b with ha, hb177    rw [zShape, value] at shape178    have aIn := nat.omega.forward with ha179    have bIn := nat.omega.forward with hb180    refine ⟨a, aIn, b, bIn, shape⟩181  . intro difference182    obtain ⟨m, hm, n, hn, shape⟩ := difference183    have natM := nat.omega.backward with hm184    have natN := nat.omega.backward with hn185    have integer := integerClass.integer at m, n with natM, natN186    have value := realInt.class at m, n with natM, natN187    refine ⟨integerClass(m, n), integer, ?_⟩188    rw [shape, value]189    rfl190