intRel_refl

formal source

  42def intRel : (LogicNat × LogicNat) → (LogicNat × LogicNat) → Prop :=
  43  fun p q => p.1 + q.2 = q.1 + p.2
  44
  45theorem intRel_refl : ∀ p : LogicNat × LogicNat, intRel p p := by
  46  intro p
  47  show p.1 + p.2 = p.1 + p.2
  48  rfl
  49
  50theorem intRel_symm : ∀ {p q : LogicNat × LogicNat}, intRel p q → intRel q p := by
  51  intro p q h
  52  show q.1 + p.2 = p.1 + q.2
  53  exact h.symm
  54
  55theorem intRel_trans : ∀ {p q r : LogicNat × LogicNat},
  56    intRel p q → intRel q r → intRel p r := by
  57  rintro ⟨a, b⟩ ⟨c, d⟩ ⟨e, f⟩ hpq hqr
  58  show a + f = e + b
  59  rw [eq_iff_toNat_eq, toNat_add, toNat_add]
  60  have hpq' : toNat a + toNat d = toNat c + toNat b := by
  61    have := congrArg toNat (show a + d = c + b from hpq)
  62    rwa [toNat_add, toNat_add] at this
  63  have hqr' : toNat c + toNat f = toNat e + toNat d := by
  64    have := congrArg toNat (show c + f = e + d from hqr)
  65    rwa [toNat_add, toNat_add] at this
  66  omega
  67
  68/-- The setoid structure on `LogicNat × LogicNat` for Grothendieck
  69completion. -/
  70instance setoid : Setoid (LogicNat × LogicNat) :=
  71  ⟨intRel, intRel_refl, intRel_symm, intRel_trans⟩
  72
  73/-! ## 2. The Type of Logic-Native Integers -/
  74
  75/-- `LogicInt` is the Grothendieck completion of `LogicNat` under