fromRat

formal source

 223def toRat : LogicRat → ℚ := Quotient.lift toRatCore toRatCore_respects
 224
 225/-- The inverse `Rat → LogicRat`. -/
 226noncomputable def fromRat (q : ℚ) : LogicRat :=
 227  let n : LogicInt := fromInt q.num
 228  let d : LogicInt := fromInt q.den
 229  mk n d (by
 230    intro h
 231    have : toInt d = toInt 0 := congrArg toInt h
 232    rw [toInt_zero] at this
 233    have : toInt (fromInt q.den) = 0 := this
 234    rw [toInt_fromInt] at this
 235    have hpos : (0 : Int) < q.den := by exact_mod_cast q.den_pos
 236    have : (q.den : Int) = 0 := this
 237    have hne : (q.den : Int) ≠ 0 := ne_of_gt hpos
 238    exact hne this)
 239
 240@[simp] theorem toRat_mk (a b : LogicInt) (hb : b ≠ 0) :
 241    toRat (mk a b hb) = (toInt a : ℚ) / toInt b := rfl
 242
 243theorem toRat_fromRat : ∀ q : ℚ, toRat (fromRat q) = q := by
 244  intro q
 245  show toRat (mk (fromInt q.num) (fromInt q.den) _) = q
 246  rw [toRat_mk, toInt_fromInt, toInt_fromInt]
 247  exact_mod_cast q.num_div_den
 248
 249/-- The other round trip: every logic-native rational is recovered from
 250its image in Mathlib's `Rat`. This is the key injectivity theorem for
 251the transport API. -/
 252theorem fromRat_toRat : ∀ q : LogicRat, fromRat (toRat q) = q := by
 253  intro q
 254  induction q using Quotient.inductionOn with
 255  | h p =>
 256    rcases p with ⟨a, b, hb⟩