toInt_fromInt

formal source

 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
 235      show mk (LogicNat.fromNat k) LogicNat.zero = mk a b
 236      apply sound
 237      -- LogicNat.fromNat k + b = a + 0 = a in LogicNat.