-- Natural numbers as reals: the embedding, its numerals, and its order
-- 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.Natural
import Ring
import Algebra.Ring.Numeral

def realNat (n : Nat) → Set
  | zero => realZero
  | succ(k) => realAddValue(realNat(k), realOne)

theorem realNat.zero
  shows realNat(0) = (0:R)
proof
  simp

theorem realNat.succ (n : Nat)
  shows realNat(succ(n)) = realAddValue(realNat(n), realOne)
proof
  rw realNat
  rfl

theorem realNat.real (n : Nat)
  shows Real(realNat(n))
proof
  induction n
  | zero =>
    rw realNat
    exact realZero.real
  | succ(k) using ih =>
    rw realNat
    have typed := realAddValue.real with ih, realOne.real
    unfold call2 at typed
    unfold realAddValue
    exact typed

theorem realNat.one
  shows realNat(1) = (1:R)
proof
  rw [realNat.succ, realNat.zero]
  have zero := realAddValue.zero_left with realOne.real
  unfold call2 at zero
  unfold realAddValue
  exact zero

theorem realNat.numeral (n : Nat)
  shows realNat(n) = ringNat(realAdd, realZero, realOne, n)
proof
  induction n
  | zero =>
    rw [realNat.zero, ringNat.zero]
    rfl
  | succ(k) using ih =>
    rw [realNat.succ, ringNat.succ, ih]
    unfold realAddValue
    unfold call2
    rfl

-- The real numeral: every literal above one elaborates to realNumeral(n), a
-- name of its own so that rewriting zero, one, or realNat leaves numerals
-- intact. The bridge to ringNat lets ring read it as the n-fold sum of one.
def realNumeral (n : Nat) : Set := realNat(n)

theorem realNumeral.nat (n : Nat)
  shows realNumeral(n) = realNat(n)
proof
  unfold realNumeral
  rfl

theorem realNumeral.real (n : Nat)
  shows Real(realNumeral(n))
proof
  rw realNumeral.nat
  exact realNat.real

theorem realNumeral.numeral (n : Nat)
  shows realNumeral(n) = ringNat(realAdd, realZero, realOne, n)
proof
  rw [realNumeral.nat, realNat.numeral]
  rfl

notation numeral _ => realNumeral(_) for Real

-- A natural number in a real position, an operand of a real operation or
-- comparison or one side of a real equation, is read as realNat(n) and
-- prints without the cast: n! * X is realNat(n!) * X.
notation coercion realNat for Nat, Real

theorem realNumeral.zero
  shows (0:R) = realZero
proof
  rfl

theorem realNumeral.succ (k : Nat)
  shows realNumeral(succ(k)) = realNumeral(k) + (1:R)
proof
  rw [realNumeral.numeral, ringNat.succ, realNumeral.numeral]
  rfl

theorem realNat.add (m n : Nat)
  shows realNat(add(m, n)) = (realNat(m):R) + (realNat(n):R)
proof
  induction m
  | zero =>
    rw [add, realNat.zero]
    ring
  | succ(k) using ih =>
    rw [add, realNat.succ, ih, realNat.succ]
    ring

theorem realNat.mul (m n : Nat)
  shows realNat(mul(m, n)) = (realNat(m):R) * (realNat(n):R)
proof
  induction m
  | zero =>
    rw [mul, realNat.zero]
    ring
  | succ(k) using ih =>
    rw [mul, realNat.add, ih, realNat.succ]
    ring

-- Natural numbers embedded in the reals are nonnegative, and positive
-- above zero.
theorem realNat.zero_le (n : Nat)
  shows (0:R) ≤ (realNat(n):R)
proof
  induction n
  | zero =>
    rw realNat.zero
    exact realLe.reflexive with realZero.real
  | succ(k) using ih =>
    have natural := realNat.real at k
    rw realNat.succ
    linarith

theorem realNat.positive_succ (n : Nat)
  shows (0:R) < (realNat(succ(n)):R)
proof
  have natural := realNat.real at n
  have nonnegative := realNat.zero_le at n
  rw realNat.succ
  linarith

theorem realNat.positive (n : Nat)
  requires nonzero : n ≠ 0
  shows (0:R) < (realNat(n):R)
proof
  have alternatives := natural.zero_or_successor at n
  cases alternatives with zero | successor
  . exfalso
    exact nonzero with zero
  . obtain ⟨k, natural, shape⟩ := successor
    rw shape
    exact realNat.positive_succ at k

theorem realNat.le_of_natural_le (m n : Nat)
  requires le : m ≤ n
  shows (realNat(m):R) ≤ (realNat(n):R)
proof
  obtain ⟨d, natural, split⟩ := le
  have naturalM := realNat.real at m
  have naturalD := realNat.real at d
  have nonnegative := realNat.zero_le at d
  have sum := realNat.add at m, d
  rw split at sum
  rw sum
  linarith

theorem realNat.ne_zero (n : Nat)
  requires nonzero : n ≠ 0
  shows (realNat(n):R) ≠ 0
proof
  have positive := realNat.positive with nonzero
  intro zero
  rw zero at positive
  linarith