-- The sign of an integer
-- 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.Int.Sign
import AbsoluteValueOrder

theorem integerOne.ne_zero
  shows integerOne ≠ integerZero
proof
  intro same
  have strict := integerLess.zero_one
  rw same at strict
  exact integerLess.irreflexive with strict

theorem integerOne.neg_ne_zero
  shows -integerOne ≠ integerZero
proof
  intro same
  have restore : integerOne = -(-integerOne) by ring
  rw same at restore
  have zeroNeg : -integerZero = integerZero by ring
  rw zeroNeg at restore
  exact integerOne.ne_zero with restore

defunique integerSign (z : Set) (s ∈ ℤ) :=
  (z = integerZero ∧ s = integerZero) ∨
  (integerLess(integerZero, z) ∧ s = integerOne) ∨
  (integerLess(z, integerZero) ∧ s = -integerOne)
requires integer : Integer(z)
proof
  have zeroMember : integerZero ∈ ℤ := integerZero.integer
  have oneMember : integerOne ∈ ℤ := integerOne.integer
  have negInteger := integerNegValue.integer at integerOne
  have negMember : -integerOne ∈ ℤ := negInteger
  have split := integerLess.trichotomy at integerZero, z
  rcases split with positive | zero | negative
  . refine ⟨integerOne, oneMember, ?_⟩
    right
    left
    exact ⟨positive, rfl⟩
  . refine ⟨integerZero, zeroMember, ?_⟩
    left
    symm at zero
    exact ⟨zero, rfl⟩
  . refine ⟨-integerOne, negMember, ?_⟩
    right
    right
    exact ⟨negative, rfl⟩

uniqueness
  intros s sMember first t tMember second
  rcases first with zeroS | positiveS | negativeS
  . rcases second with zeroT | positiveT | negativeT
    . cc
    . rw zeroS.left at positiveT
      exfalso
      exact integerLess.irreflexive with positiveT.left
    . rw zeroS.left at negativeT
      exfalso
      exact integerLess.irreflexive with negativeT.left
  . rcases second with zeroT | positiveT | negativeT
    . rw zeroT.left at positiveS
      exfalso
      exact integerLess.irreflexive with positiveS.left
    . cc
    . exfalso
      exact integerLess.asymmetric with positiveS.left, negativeT.left
  . rcases second with zeroT | positiveT | negativeT
    . rw zeroT.left at negativeS
      exfalso
      exact integerLess.irreflexive with negativeS.left
    . exfalso
      exact integerLess.asymmetric with negativeS.left, positiveT.left
    . cc

theorem integerSign.integer (z : Integer)
  shows Integer(integerSign(z))
proof
  have selected := integerSign.selected at z with *
  exact selected.left

theorem integerSign.zero
  shows integerSign(integerZero) = integerZero
proof
  have selected := integerSign.selected at integerZero with *
  rcases selected with ⟨member, property⟩
  rcases property with zero | positive | negative
  . exact zero.right
  . exfalso
    exact integerLess.irreflexive with positive.left
  . exfalso
    exact integerLess.irreflexive with negative.left

theorem integerSign.of_positive (z : Integer)
  requires positive : 0 < z
  shows integerSign(z) = integerOne
proof
  have selected := integerSign.selected at z with *
  rcases selected with ⟨member, property⟩
  rcases property with zero | isPositive | negative
  . rw zero.left at positive
    exfalso
    exact integerLess.irreflexive with positive
  . exact isPositive.right
  . exfalso
    exact integerLess.asymmetric with positive, negative.left

theorem integerSign.of_negative (z : Integer)
  requires negative : z < 0
  shows integerSign(z) = -integerOne
proof
  have selected := integerSign.selected at z with *
  rcases selected with ⟨member, property⟩
  rcases property with zero | positive | isNegative
  . rw zero.left at negative
    exfalso
    exact integerLess.irreflexive with negative
  . exfalso
    exact integerLess.asymmetric with negative, positive.left
  . exact isNegative.right

theorem integerSign.of_zero (z : Integer)
  requires zero : z = 0
  shows integerSign(z) = integerZero
proof
  rw zero
  exact integerSign.zero

theorem integerSign.cases (z : Integer)
  shows integerSign(z) = integerZero ∨ integerSign(z) = integerOne ∨
    integerSign(z) = -integerOne
proof
  have split := integerLess.trichotomy at integerZero, z
  rcases split with positive | zero | negative
  . right
    left
    exact integerSign.of_positive with positive
  . left
    symm at zero
    exact integerSign.of_zero with zero
  . right
    right
    exact integerSign.of_negative with negative

theorem integerSign.one
  shows integerSign(integerOne) = integerOne
proof
  have positive := integerLess.zero_one
  exact integerSign.of_positive with positive

theorem integerSign.ofNat_add_one (n : Nat)
  shows integerSign(integerOfNat(n + 1)) = integerOne
proof
  have positive := IntegerPositive.ofNat_add_one at n
  have strict := integerLess.zero_iff_positive.backward with positive
  exact integerSign.of_positive with strict

theorem integerSign.neg (z : Integer)
  shows integerSign(-z) = -integerSign(z)
proof
  have split := integerLess.trichotomy at integerZero, z
  rcases split with positive | zero | negative
  . have flipped := integerLess.neg.forward with positive
    have zeroNeg : -integerZero = integerZero by ring
    rw zeroNeg at flipped
    have left := integerSign.of_negative with flipped
    have right := integerSign.of_positive with positive
    rw [left, right]
    rfl
  . rw ← zero
    have zeroNeg : -integerZero = integerZero by ring
    rw [zeroNeg, integerSign.zero]
    ring
  . have flipped := integerLess.neg.forward with negative
    have zeroNeg : -integerZero = integerZero by ring
    rw zeroNeg at flipped
    have left := integerSign.of_positive with flipped
    have right := integerSign.of_negative with negative
    rw [left, right]
    ring

theorem integerSign.mul_abs (z : Integer)
  shows integerSign(z) * integerAbs(z) = z
proof
  have split := integerLess.trichotomy at integerZero, z
  rcases split with positive | zero | negative
  . have sign := integerSign.of_positive with positive
    have abs := integerAbs.of_nonneg with (integerLess.implies_le with positive)
    rw [sign, abs]
    ring
  . rw ← zero
    rw [integerSign.zero, integerAbs.zero]
    ring
  . have sign := integerSign.of_negative with negative
    have abs := integerAbs.of_nonpos with (integerLess.implies_le with negative)
    rw [sign, abs]
    ring

theorem integerSign.mul_self (z : Integer)
  shows integerSign(z) * z = integerAbs(z)
proof
  have split := integerLess.trichotomy at integerZero, z
  rcases split with positive | zero | negative
  . have sign := integerSign.of_positive with positive
    have abs := integerAbs.of_nonneg with (integerLess.implies_le with positive)
    rw [sign, abs]
    ring
  . rw ← zero
    rw [integerSign.zero, integerAbs.zero]
    ring
  . have sign := integerSign.of_negative with negative
    have abs := integerAbs.of_nonpos with (integerLess.implies_le with negative)
    rw [sign, abs]
    ring

theorem integerSign.square (z : Integer)
  requires nonzero : z ≠ 0
  shows integerSign(z) * integerSign(z) = integerOne
proof
  have split := integerLess.trichotomy at integerZero, z
  rcases split with positive | zero | negative
  . have sign := integerSign.of_positive with positive
    rw sign
    ring
  . symm at zero
    exfalso
    exact nonzero with zero
  . have sign := integerSign.of_negative with negative
    rw sign
    ring

theorem integerSign.eq_zero_iff (z : Integer)
  shows integerSign(z) = integerZero ↔ z = 0
proof
  constructor
  . intro zero
    have split := integerLess.trichotomy at integerZero, z
    rcases split with positive | same | negative
    . have sign := integerSign.of_positive with positive
      rw sign at zero
      exfalso
      exact integerOne.ne_zero with zero
    . symm
      exact same
    . have sign := integerSign.of_negative with negative
      rw sign at zero
      exfalso
      exact integerOne.neg_ne_zero with zero
  . intro zero
    exact integerSign.of_zero with zero

theorem integerSign.mul (x y : Integer)
  shows integerSign(x * y) = integerSign(x) * integerSign(y)
proof
  have xSplit := integerLess.trichotomy at integerZero, x
  have ySplit := integerLess.trichotomy at integerZero, y
  rcases xSplit with xPositive | xZero | xNegative
  . have xSign := integerSign.of_positive with xPositive
    rcases ySplit with yPositive | yZero | yNegative
    . have ySign := integerSign.of_positive with yPositive
      have product := integerLess.mul_positive with xPositive, yPositive
      have sign := integerSign.of_positive with product
      rw [sign, xSign, ySign]
      ring
    . rw ← yZero
      have vanish : x * integerZero = integerZero by ring
      rw [vanish, integerSign.zero, xSign]
      ring
    . have ySign := integerSign.of_negative with yNegative
      have product := integerLess.mul_negative with xPositive, yNegative
      have sign := integerSign.of_negative with product
      rw [sign, xSign, ySign]
      ring
  . rw ← xZero
    have vanish : integerZero * y = integerZero by ring
    rw [vanish, integerSign.zero]
    ring
  . have xSign := integerSign.of_negative with xNegative
    rcases ySplit with yPositive | yZero | yNegative
    . have ySign := integerSign.of_positive with yPositive
      have swapped := integerLess.mul_negative with yPositive, xNegative
      have shape : y * x = x * y by ring
      rw shape at swapped
      have sign := integerSign.of_negative with swapped
      rw [sign, xSign, ySign]
      ring
    . rw ← yZero
      have vanish : x * integerZero = integerZero by ring
      rw [vanish, integerSign.zero, xSign]
      ring
    . have ySign := integerSign.of_negative with yNegative
      have product :=
        integerLess.mul_negative_negative with xNegative, yNegative
      have sign := integerSign.of_positive with product
      rw [sign, xSign, ySign]
      ring