`toInt_mk`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.IntegersFromLogic on GitHub at line 204.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

 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
 231        linarith
 232      obtain ⟨k, hk⟩ := Int.eq_ofNat_of_zero_le hge
 233      rw [hk]
 234      show fromInt (Int.ofNat k) = mk a b

papers checked against this theorem

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