fromInt_toInt

proof body

Tactic-mode proof.

 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.
 238      -- We have: (toNat a : Int) - toNat b = k as Int, so toNat a = toNat b + k in Nat.
 239      have hknat : (k : Int) = (toNat a : Int) - toNat b := hk.symm
 240      have hknat' : toNat a = toNat b + k := by
 241        have : (toNat a : Int) = toNat b + k := by linarith
 242        exact_mod_cast this
 243      show LogicNat.fromNat k + b = a + LogicNat.zero
 244      rw [LogicNat.add_zero]
 245      have hcast := congrArg fromNat hknat'
 246      rw [LogicNat.fromNat_toNat] at hcast
 247      -- hcast : a = fromNat (toNat b + k)
 248      -- We need: fromNat k + b = a
 249      have : LogicNat.fromNat (toNat b + k) = LogicNat.fromNat (toNat b) + LogicNat.fromNat k := by
 250        -- fromNat is an additive homomorphism. Prove directly.
 251        have hh : toNat (LogicNat.fromNat (toNat b) + LogicNat.fromNat k)
 252                  = toNat b + k := by
 253          rw [LogicNat.toNat_add, LogicNat.toNat_fromNat, LogicNat.toNat_fromNat]
 254        have := congrArg LogicNat.fromNat hh
 255        rw [LogicNat.fromNat_toNat] at this
 256        exact this.symm
 257      rw [hcast, this, LogicNat.fromNat_toNat, LogicNat.add_comm]
 258    · -- Negative case
 259      push_neg at h
 260      have hlt : (toNat a : Int) < toNat b := by exact_mod_cast h
 261      have hltz : (toNat a : Int) - toNat b < 0 := by linarith
 262      have hsub_pos : 0 < toNat b - toNat a := Nat.sub_pos_of_lt h
 263      -- (toNat a : Int) - toNat b = -(toNat b - toNat a) and is Int.negSucc of (toNat b - toNat a - 1).
 264      set m := toNat b - toNat a - 1 with hm_def
 265      have hsucc : Nat.succ m = toNat b - toNat a := by
 266        rw [hm_def]
 267        omega
 268      have heq : (toNat a : Int) - toNat b = Int.negSucc m := by
 269        rw [Int.negSucc_eq]
 270        have h1 : ((Nat.succ m : Int)) = (toNat b - toNat a : Int) := by
 271          rw [hsucc]
 272          push_cast
 273          omega
 274        push_cast at h1
 275        linarith
 276      rw [heq]
 277      show fromInt (Int.negSucc m) = mk a b
 278      show mk LogicNat.zero (LogicNat.fromNat (Nat.succ m)) = mk a b
 279      apply sound
 280      -- Want: 0 + b = a + fromNat (succ m), i.e. b = a + fromNat (succ m).
 281      show LogicNat.zero + b = a + LogicNat.fromNat (Nat.succ m)
 282      rw [LogicNat.zero_add]
 283      -- toNat b = toNat a + Nat.succ m by hsucc.
 284      have hbnat : toNat b = toNat a + Nat.succ m := by
 285        rw [hsucc]; omega
 286      have hcast := congrArg LogicNat.fromNat hbnat
 287      rw [LogicNat.fromNat_toNat] at hcast
 288      have hadd_morph : LogicNat.fromNat (toNat a + Nat.succ m)
 289                        = LogicNat.fromNat (toNat a) + LogicNat.fromNat (Nat.succ m) := by
 290        have hh : toNat (LogicNat.fromNat (toNat a) + LogicNat.fromNat (Nat.succ m))
 291                  = toNat a + Nat.succ m := by
 292          rw [LogicNat.toNat_add, LogicNat.toNat_fromNat, LogicNat.toNat_fromNat]
 293        have := congrArg LogicNat.fromNat hh
 294        rw [LogicNat.fromNat_toNat] at this
 295        exact this.symm
 296      rw [hcast, hadd_morph, LogicNat.fromNat_toNat]
 297
 298/-- **Recovery theorem (carrier)**: `LogicInt` and `Int` are in
 299bijection via `toInt` and `fromInt`. -/