Grace/Cumulus/Int/Sign.g17

Open in Workbench Download source

Imports

AbsoluteValueOrder

Declarations

Source

1-- The sign of an integer2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Int.Sign8import AbsoluteValueOrder910theorem integerOne.ne_zero11  shows integerOne ≠ integerZero12proof13  intro same14  have strict := integerLess.zero_one15  rw same at strict16  exact integerLess.irreflexive with strict1718theorem integerOne.neg_ne_zero19  shows -integerOne ≠ integerZero20proof21  intro same22  have restore : integerOne = -(-integerOne) by ring23  rw same at restore24  have zeroNeg : -integerZero = integerZero by ring25  rw zeroNeg at restore26  exact integerOne.ne_zero with restore2728defunique integerSign (z : Set) (s ∈ ℤ) :=29  (z = integerZero ∧ s = integerZero) ∨30  (integerLess(integerZero, z) ∧ s = integerOne) ∨31  (integerLess(z, integerZero) ∧ s = -integerOne)32requires integer : Integer(z)33proof34  have zeroMember : integerZero ∈ ℤ := integerZero.integer35  have oneMember : integerOne ∈ ℤ := integerOne.integer36  have negInteger := integerNegValue.integer at integerOne37  have negMember : -integerOne ∈ ℤ := negInteger38  have split := integerLess.trichotomy at integerZero, z39  rcases split with positive | zero | negative40  . refine ⟨integerOne, oneMember, ?_⟩41    right42    left43    exact ⟨positive, rfl⟩44  . refine ⟨integerZero, zeroMember, ?_⟩45    left46    symm at zero47    exact ⟨zero, rfl⟩48  . refine ⟨-integerOne, negMember, ?_⟩49    right50    right51    exact ⟨negative, rfl⟩5253uniqueness54  intros s sMember first t tMember second55  rcases first with zeroS | positiveS | negativeS56  . rcases second with zeroT | positiveT | negativeT57    . cc58    . rw zeroS.left at positiveT59      exfalso60      exact integerLess.irreflexive with positiveT.left61    . rw zeroS.left at negativeT62      exfalso63      exact integerLess.irreflexive with negativeT.left64  . rcases second with zeroT | positiveT | negativeT65    . rw zeroT.left at positiveS66      exfalso67      exact integerLess.irreflexive with positiveS.left68    . cc69    . exfalso70      exact integerLess.asymmetric with positiveS.left, negativeT.left71  . rcases second with zeroT | positiveT | negativeT72    . rw zeroT.left at negativeS73      exfalso74      exact integerLess.irreflexive with negativeS.left75    . exfalso76      exact integerLess.asymmetric with negativeS.left, positiveT.left77    . cc7879theorem integerSign.integer (z : Integer)80  shows Integer(integerSign(z))81proof82  have selected := integerSign.selected at z with *83  exact selected.left8485theorem integerSign.zero86  shows integerSign(integerZero) = integerZero87proof88  have selected := integerSign.selected at integerZero with *89  rcases selected with ⟨member, property⟩90  rcases property with zero | positive | negative91  . exact zero.right92  . exfalso93    exact integerLess.irreflexive with positive.left94  . exfalso95    exact integerLess.irreflexive with negative.left9697theorem integerSign.of_positive (z : Integer)98  requires positive : 0 < z99  shows integerSign(z) = integerOne100proof101  have selected := integerSign.selected at z with *102  rcases selected with ⟨member, property⟩103  rcases property with zero | isPositive | negative104  . rw zero.left at positive105    exfalso106    exact integerLess.irreflexive with positive107  . exact isPositive.right108  . exfalso109    exact integerLess.asymmetric with positive, negative.left110111theorem integerSign.of_negative (z : Integer)112  requires negative : z < 0113  shows integerSign(z) = -integerOne114proof115  have selected := integerSign.selected at z with *116  rcases selected with ⟨member, property⟩117  rcases property with zero | positive | isNegative118  . rw zero.left at negative119    exfalso120    exact integerLess.irreflexive with negative121  . exfalso122    exact integerLess.asymmetric with negative, positive.left123  . exact isNegative.right124125theorem integerSign.of_zero (z : Integer)126  requires zero : z = 0127  shows integerSign(z) = integerZero128proof129  rw zero130  exact integerSign.zero131132theorem integerSign.cases (z : Integer)133  shows integerSign(z) = integerZero ∨ integerSign(z) = integerOne ∨134    integerSign(z) = -integerOne135proof136  have split := integerLess.trichotomy at integerZero, z137  rcases split with positive | zero | negative138  . right139    left140    exact integerSign.of_positive with positive141  . left142    symm at zero143    exact integerSign.of_zero with zero144  . right145    right146    exact integerSign.of_negative with negative147148theorem integerSign.one149  shows integerSign(integerOne) = integerOne150proof151  have positive := integerLess.zero_one152  exact integerSign.of_positive with positive153154theorem integerSign.ofNat_add_one (n : Nat)155  shows integerSign(integerOfNat(n + 1)) = integerOne156proof157  have positive := IntegerPositive.ofNat_add_one at n158  have strict := integerLess.zero_iff_positive.backward with positive159  exact integerSign.of_positive with strict160161theorem integerSign.neg (z : Integer)162  shows integerSign(-z) = -integerSign(z)163proof164  have split := integerLess.trichotomy at integerZero, z165  rcases split with positive | zero | negative166  . have flipped := integerLess.neg.forward with positive167    have zeroNeg : -integerZero = integerZero by ring168    rw zeroNeg at flipped169    have left := integerSign.of_negative with flipped170    have right := integerSign.of_positive with positive171    rw [left, right]172    rfl173  . rw ← zero174    have zeroNeg : -integerZero = integerZero by ring175    rw [zeroNeg, integerSign.zero]176    ring177  . have flipped := integerLess.neg.forward with negative178    have zeroNeg : -integerZero = integerZero by ring179    rw zeroNeg at flipped180    have left := integerSign.of_positive with flipped181    have right := integerSign.of_negative with negative182    rw [left, right]183    ring184185theorem integerSign.mul_abs (z : Integer)186  shows integerSign(z) * integerAbs(z) = z187proof188  have split := integerLess.trichotomy at integerZero, z189  rcases split with positive | zero | negative190  . have sign := integerSign.of_positive with positive191    have abs := integerAbs.of_nonneg with (integerLess.implies_le with positive)192    rw [sign, abs]193    ring194  . rw ← zero195    rw [integerSign.zero, integerAbs.zero]196    ring197  . have sign := integerSign.of_negative with negative198    have abs := integerAbs.of_nonpos with (integerLess.implies_le with negative)199    rw [sign, abs]200    ring201202theorem integerSign.mul_self (z : Integer)203  shows integerSign(z) * z = integerAbs(z)204proof205  have split := integerLess.trichotomy at integerZero, z206  rcases split with positive | zero | negative207  . have sign := integerSign.of_positive with positive208    have abs := integerAbs.of_nonneg with (integerLess.implies_le with positive)209    rw [sign, abs]210    ring211  . rw ← zero212    rw [integerSign.zero, integerAbs.zero]213    ring214  . have sign := integerSign.of_negative with negative215    have abs := integerAbs.of_nonpos with (integerLess.implies_le with negative)216    rw [sign, abs]217    ring218219theorem integerSign.square (z : Integer)220  requires nonzero : z ≠ 0221  shows integerSign(z) * integerSign(z) = integerOne222proof223  have split := integerLess.trichotomy at integerZero, z224  rcases split with positive | zero | negative225  . have sign := integerSign.of_positive with positive226    rw sign227    ring228  . symm at zero229    exfalso230    exact nonzero with zero231  . have sign := integerSign.of_negative with negative232    rw sign233    ring234235theorem integerSign.eq_zero_iff (z : Integer)236  shows integerSign(z) = integerZero ↔ z = 0237proof238  constructor239  . intro zero240    have split := integerLess.trichotomy at integerZero, z241    rcases split with positive | same | negative242    . have sign := integerSign.of_positive with positive243      rw sign at zero244      exfalso245      exact integerOne.ne_zero with zero246    . symm247      exact same248    . have sign := integerSign.of_negative with negative249      rw sign at zero250      exfalso251      exact integerOne.neg_ne_zero with zero252  . intro zero253    exact integerSign.of_zero with zero254255theorem integerSign.mul (x y : Integer)256  shows integerSign(x * y) = integerSign(x) * integerSign(y)257proof258  have xSplit := integerLess.trichotomy at integerZero, x259  have ySplit := integerLess.trichotomy at integerZero, y260  rcases xSplit with xPositive | xZero | xNegative261  . have xSign := integerSign.of_positive with xPositive262    rcases ySplit with yPositive | yZero | yNegative263    . have ySign := integerSign.of_positive with yPositive264      have product := integerLess.mul_positive with xPositive, yPositive265      have sign := integerSign.of_positive with product266      rw [sign, xSign, ySign]267      ring268    . rw ← yZero269      have vanish : x * integerZero = integerZero by ring270      rw [vanish, integerSign.zero, xSign]271      ring272    . have ySign := integerSign.of_negative with yNegative273      have product := integerLess.mul_negative with xPositive, yNegative274      have sign := integerSign.of_negative with product275      rw [sign, xSign, ySign]276      ring277  . rw ← xZero278    have vanish : integerZero * y = integerZero by ring279    rw [vanish, integerSign.zero]280    ring281  . have xSign := integerSign.of_negative with xNegative282    rcases ySplit with yPositive | yZero | yNegative283    . have ySign := integerSign.of_positive with yPositive284      have swapped := integerLess.mul_negative with yPositive, xNegative285      have shape : y * x = x * y by ring286      rw shape at swapped287      have sign := integerSign.of_negative with swapped288      rw [sign, xSign, ySign]289      ring290    . rw ← yZero291      have vanish : x * integerZero = integerZero by ring292      rw [vanish, integerSign.zero, xSign]293      ring294    . have ySign := integerSign.of_negative with yNegative295      have product :=296        integerLess.mul_negative_negative with xNegative, yNegative297      have sign := integerSign.of_positive with product298      rw [sign, xSign, ySign]299      ring300