toIntCore

formal source

 177/-- Map a pair `(a, b) : LogicNat × LogicNat` to `a - b : Int` via the
 178underlying `Nat` representation. Well-defined on the quotient because
 179`a + d = c + b` implies `(a : Int) - b = (c : Int) - d`. -/
 180def toIntCore : LogicNat × LogicNat → Int :=
 181  fun p => (toNat p.1 : Int) - (toNat p.2 : Int)
 182
 183theorem toIntCore_respects :
 184    ∀ p q : LogicNat × LogicNat, p ≈ q → toIntCore p = toIntCore q := by
 185  rintro ⟨a, b⟩ ⟨c, d⟩ h
 186  -- h : a + d = c + b
 187  show (toNat a : Int) - toNat b = (toNat c : Int) - toNat d
 188  have hcast := congrArg toNat h
 189  rw [toNat_add, toNat_add] at hcast
 190  -- toNat a + toNat d = toNat c + toNat b in Nat.
 191  -- In Int: (toNat a) + (toNat d) = (toNat c) + (toNat b), so subtract to get the goal.
 192  have : (toNat a : Int) + toNat d = (toNat c : Int) + toNat b := by exact_mod_cast hcast
 193  linarith
 194
 195/-- The recovery map `LogicInt → Int`. -/
 196def toInt : LogicInt → Int := Quotient.lift toIntCore toIntCore_respects
 197
 198/-- The inverse `Int → LogicInt`. Maps non-negative `n ≥ 0` to `[n, 0]`
 199and negative `-n < 0` to `[0, n]`. -/
 200def fromInt : Int → LogicInt
 201  | Int.ofNat n   => mk (LogicNat.fromNat n) LogicNat.zero
 202  | Int.negSucc n => mk LogicNat.zero (LogicNat.fromNat (Nat.succ n))
 203
 204@[simp] theorem toInt_mk (a b : LogicNat) :
 205    toInt (mk a b) = (toNat a : Int) - toNat b := rfl
 206
 207theorem toInt_fromInt : ∀ n : Int, toInt (fromInt n) = n := by
 208  intro n
 209  cases n with
 210  | ofNat n =>