setoid

formal source

  74      _ = (e * b) * d := by rw [mul_assoc', mul_comm' d b, ← mul_assoc']
  75  exact mul_right_cancel hd key
  76
  77instance setoid : Setoid PreRat := ⟨ratRel, ratRel_refl, ratRel_symm, ratRel_trans⟩
  78
  79/-! ## 2. The Type of Logic-Native Rationals -/
  80
  81/-- `LogicRat` is the field of fractions of `LogicInt`. -/
  82def LogicRat : Type := Quotient (setoid : Setoid PreRat)
  83
  84namespace LogicRat
  85
  86/-- Constructor: form a rational from a pair with non-zero denominator. -/
  87def mk (a b : LogicInt) (hb : b ≠ 0) : LogicRat :=
  88  Quotient.mk' ⟨a, b, hb⟩
  89
  90theorem sound (a b c d : LogicInt) (hb : b ≠ 0) (hd : d ≠ 0)
  91    (h : a * d = c * b) : mk a b hb = mk c d hd := by
  92  apply Quotient.sound
  93  show a * d = c * b
  94  exact h
  95
  96/-! ## 3. Embedding LogicInt into LogicRat -/
  97
  98/-- The natural injection `LogicInt ↪ LogicRat` sending `n` to `n/1`. -/
  99def ofLogicInt (n : LogicInt) : LogicRat :=
 100  mk n 1 (by
 101    intro h
 102    have : toInt (1 : LogicInt) = toInt (0 : LogicInt) := congrArg toInt h
 103    rw [toInt_one, toInt_zero] at this
 104    exact one_ne_zero this)
 105
 106/-! ## 4. Zero, One, Negation, Addition, Multiplication -/
 107