-- The integers inside the reals: the embedding realInt sends the class of
-- (a, b) to a - b; it is an injective ring homomorphism agreeing with
-- realNat on the naturals, and its image is the set of differences of
-- naturals
-- 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.Real.Integer
import RootTwo
import Int

-- The real number of an integer: the class of (a, b) goes to a - b, which
-- does not depend on the representative.
defunique realInt (z : Set) (x ∈ ℝ) :=
  ∃ a, Nat(a) ∧ ∃ b, Nat(b) ∧ z = integerClass(a, b) ∧
    x = (realNat(a):R) - (realNat(b):R)
requires integer : Integer(z)
proof
  obtain ⟨a, ha, b, hb, shape⟩ := Integer.representatives at z with *
  have realA := realNat.real at a with ha
  have realB := realNat.real at b with hb
  have value : (realNat(a):R) - (realNat(b):R) ∈ ℝ by typecheck
  refine ⟨(realNat(a):R) - (realNat(b):R), value, a, ha, b, hb, shape, rfl⟩
uniqueness
  intros u hu first v hv second
  obtain ⟨a, ha, b, hb, shapeA, valueA⟩ := first
  obtain ⟨c, hc, d, hd, shapeC, valueC⟩ := second
  have same : integerClass(a, b) = integerClass(c, d)
    rw [← shapeA, ← shapeC]
    rfl
  have cross := integerClass.equivalent_of_eq at a, b, c, d with ha, hb, hc, hd, same
  have realA := realNat.real at a with ha
  have realB := realNat.real at b with hb
  have realC := realNat.real at c with hc
  have realD := realNat.real at d with hd
  have realCross : (realNat(a):R) + (realNat(d):R) = (realNat(c):R) + (realNat(b):R)
    rw [← realNat.add, ← realNat.add, cross]
    rfl
  rw [valueA, valueC]
  linarith

theorem realInt.real (z : Integer)
  shows realInt(z) ∈ ℝ
proof
  have selected := realInt.selected at z with *
  exact selected.left

-- The value on a class.
theorem realInt.class (a b : Nat)
  shows realInt(integerClass(a, b)) = (realNat(a):R) - (realNat(b):R)
proof
  have integer := integerClass.integer at a, b with *
  have selected := realInt.selected at integerClass(a, b) with integer
  obtain ⟨c, hc, d, hd, same, value⟩ := selected.right
  have cross := integerClass.equivalent_of_eq at a, b, c, d with *
  have realA := realNat.real at a
  have realB := realNat.real at b
  have realC := realNat.real at c with hc
  have realD := realNat.real at d with hd
  have realCross : (realNat(a):R) + (realNat(d):R) = (realNat(c):R) + (realNat(b):R)
    rw [← realNat.add, ← realNat.add, cross]
    rfl
  rw value
  linarith

-- Agreement with realNat on the naturals, and the values at 0 and 1.
theorem realInt.nat (n : Nat)
  shows realInt(integerOfNat(n)) = realNat(n)
proof
  have realN := realNat.real at n
  unfold integerOfNat
  rw [realInt.class, realNat.zero]
  ring

theorem realInt.zero
  shows realInt(integerZero) = (0:R)
proof
  unfold integerZero
  rw [realInt.class, realNat.zero]
  ring

theorem realInt.one
  shows realInt(integerOne) = (1:R)
proof
  unfold integerOne
  rw [realInt.nat, realNat.one]
  rfl

-- The ring homomorphism laws.
theorem realInt.add (m n : Integer)
  shows realInt(m + n) = (realInt(m):R) + (realInt(n):R)
proof
  obtain ⟨a, ha, b, hb, shapeM⟩ := Integer.representatives at m with *
  obtain ⟨c, hc, d, hd, shapeN⟩ := Integer.representatives at n with *
  have realA := realNat.real at a with ha
  have realB := realNat.real at b with hb
  have realC := realNat.real at c with hc
  have realD := realNat.real at d with hd
  have sum := integerAddValue.classes at a, b, c, d with *
  rw [shapeM, shapeN, sum]
  unfold integerClassSum
  rw [realInt.class, realInt.class, realInt.class, realNat.add, realNat.add]
  ring

theorem realInt.neg (n : Integer)
  shows realInt(-n) = -(realInt(n):R)
proof
  obtain ⟨c, hc, d, hd, shapeN⟩ := Integer.representatives at n with *
  have realC := realNat.real at c with hc
  have realD := realNat.real at d with hd
  have negative := integerNegValue.classes at c, d with *
  rw [shapeN, negative]
  unfold integerClassNeg
  rw [realInt.class, realInt.class]
  ring

theorem realInt.mul (m n : Integer)
  shows realInt(m * n) = (realInt(m):R) * (realInt(n):R)
proof
  obtain ⟨a, ha, b, hb, shapeM⟩ := Integer.representatives at m with *
  obtain ⟨c, hc, d, hd, shapeN⟩ := Integer.representatives at n with *
  have realA := realNat.real at a with ha
  have realB := realNat.real at b with hb
  have realC := realNat.real at c with hc
  have realD := realNat.real at d with hd
  have product := integerMulValue.classes at a, b, c, d with *
  rw [shapeM, shapeN, product]
  unfold integerClassMul
  rw [realInt.class, realInt.class, realInt.class, realNat.add, realNat.add,
    realNat.mul, realNat.mul, realNat.mul, realNat.mul]
  ring

theorem realInt.sub (m n : Integer)
  shows realInt(m - n) = (realInt(m):R) - (realInt(n):R)
proof
  have negative := integerNegValue.integer at n with *
  have realM := realInt.real at m with *
  have realN := realInt.real at n with *
  unfold integerSubValue
  rw [integerAddValue.notation, integerNegValue.notation, realInt.add, realInt.neg]
  ring

-- The embedding is injective.
theorem realInt.injective (m n : Integer)
  requires equal : realInt(m) = realInt(n)
  shows m = n
proof
  obtain ⟨a, ha, b, hb, shapeM⟩ := Integer.representatives at m with *
  obtain ⟨c, hc, d, hd, shapeN⟩ := Integer.representatives at n with *
  have realA := realNat.real at a with ha
  have realB := realNat.real at b with hb
  have realC := realNat.real at c with hc
  have realD := realNat.real at d with hd
  rw [shapeM, shapeN, realInt.class, realInt.class] at equal
  have cross : (realNat(a):R) + (realNat(d):R) = (realNat(c):R) + (realNat(b):R)
    linarith
  rw [← realNat.add, ← realNat.add] at cross
  have natural := realNat.injective at a + d, c + b with cross
  rw [shapeM, shapeN]
  exact integerClass.eq at a, b, c, d with natural

-- An integer is written as a real wherever a real is expected.
notation coercion realInt for Integer, Real

-- The image of ℤ in ℝ is the set of differences of naturals.
theorem realInt.range (x : Set)
  shows (∃ z ∈ ℤ, x = realInt(z)) ↔
    ∃ m ∈ ℕ, ∃ n ∈ ℕ, x = (realNat(m):R) - (realNat(n):R)
proof
  constructor
  . intro image
    obtain ⟨z, hz, shape⟩ := image
    obtain ⟨a, ha, b, hb, zShape⟩ := Integer.representatives at z with hz
    have value := realInt.class at a, b with ha, hb
    rw [zShape, value] at shape
    have aIn := nat.omega.forward with ha
    have bIn := nat.omega.forward with hb
    refine ⟨a, aIn, b, bIn, shape⟩
  . intro difference
    obtain ⟨m, hm, n, hn, shape⟩ := difference
    have natM := nat.omega.backward with hm
    have natN := nat.omega.backward with hn
    have integer := integerClass.integer at m, n with natM, natN
    have value := realInt.class at m, n with natM, natN
    refine ⟨integerClass(m, n), integer, ?_⟩
    rw [shape, value]
    rfl