`fromInt`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.IntegersFromLogic
domain: Foundation
line: 200 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.IntegersFromLogic on GitHub at line 200.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 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 =>
 211    show toInt (mk (LogicNat.fromNat n) LogicNat.zero) = (Int.ofNat n)
 212    rw [toInt_mk, toNat_fromNat, toNat_zero]
 213    simp [Int.ofNat]
 214  | negSucc n =>
 215    show toInt (mk LogicNat.zero (LogicNat.fromNat (Nat.succ n))) = Int.negSucc n
 216    rw [toInt_mk, toNat_zero, toNat_fromNat]
 217    simp [Int.negSucc_eq]
 218
 219theorem fromInt_toInt : ∀ z : LogicInt, fromInt (toInt z) = z := by
 220  intro z
 221  induction z using Quotient.inductionOn with
 222  | h p =>
 223    rcases p with ⟨a, b⟩
 224    show fromInt (toInt (mk a b)) = mk a b
 225    rw [toInt_mk]
 226    -- (toNat a : Int) - toNat b. Case on sign.
 227    by_cases h : toNat b ≤ toNat a
 228    · -- Non-negative case
 229      have hge : (0 : Int) ≤ (toNat a : Int) - toNat b := by
 230        have : (toNat b : Int) ≤ toNat a := by exact_mod_cast h

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.