-- Natural-number order
-- Part of the Grace17 proof assistant for mathematics based on set theory.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Core.Nat.Order
namespace Grace.Core.Nat.Order
import Grace.Core.Nat.Algebra
export open Grace.Core.Nat.Order

predicate LessEqual (a b : Nat) := exists k, Nat(k) and add(a, k) = b
notation infix 50 "≤" => LessEqual for Nat
notation infix 50 "<=" => LessEqual for Nat
notation infix 50 "≥" => reverse LessEqual for Nat
notation infix 50 ">=" => reverse LessEqual for Nat

predicate Less (a b : Nat) := succ(a) ≤ b
notation infix 50 "<" => Less for Nat
notation infix 50 ">" => reverse Less

theorem LessEqual.reflexive (a : Nat)
  shows a ≤ a
proof
  simp [LessEqual, Naturals.constructor.zero, add.right_unit]

theorem LessEqual.zero (b : Nat)
  shows 0 ≤ b
proof
  witness b
  simp [add]

theorem LessEqual.add_right (a k : Nat)
  shows a ≤ add(a, k)
proof
  witness k
  reflexivity

theorem LessEqual.successor (a : Nat)
  shows a ≤ succ(a)
proof
  witness 1
  simp [Naturals.constructor.zero, Naturals.constructor.succ]
  simp [add.succ_right, add.right_unit]

theorem LessEqual.transitive (a b c : Nat)
  requires hab : a ≤ b
  requires hbc : b ≤ c
  shows a ≤ c
proof
  obtain ⟨k, hk⟩ := hab
  obtain ⟨l, hl⟩ := hbc
  witness add(k, l)
  simp [add.closed]
  simp [add.associative_reverse]

theorem LessEqual.add_monotone_right (a b c : Nat)
  requires hab : a ≤ b
  shows add(a, c) ≤ add(b, c)
proof
  obtain ⟨k, hk⟩ := hab
  witness k
  simp
  simp [add.associative, add.swap, add.commutative]

theorem Less.implies_LessEqual (a b : Nat)
  requires hab : a < b
  shows a ≤ b
proof
  obtain ⟨k, hk⟩ := hab
  witness succ(k)
  simp [Naturals.constructor.succ]
  simp [add.successor_shift]

-- The right side of a bound whose left side is a natural number is one too:
-- the arithmetic tactics type an opaque bounded term from these.
theorem LessEqual.natural_right (a : Nat, b : Set)
  requires hab : a ≤ b
  shows Nat(b)
proof
  obtain ⟨k, hk, sum⟩ := hab
  rw ← sum
  exact add.closed at k, a

theorem Less.natural_right (a : Nat, b : Set)
  requires hab : a < b
  shows Nat(b)
proof
  have natSucc : Nat(succ(a)) by simp [Naturals.constructor.succ]
  exact LessEqual.natural_right at succ(a), b with natSucc, hab

end Grace.Core.Nat.Order