instance
definition
setoid
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Foundation.IntegersFromLogic on GitHub at line 70.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
of -
LogicNat -
of -
intRel -
intRel_refl -
intRel_symm -
intRel_trans -
LogicInt -
is -
of -
setoid -
is -
of -
is -
of -
is -
LogicInt
used by
formal source
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
76addition. -/
77def LogicInt : Type := Quotient (setoid : Setoid (LogicNat × LogicNat))
78
79namespace LogicInt
80
81/-- Constructor: form an integer from a pair of naturals. -/
82def mk (a b : LogicNat) : LogicInt := Quotient.mk' (a, b)
83
84/-- Notation `[a, b]ₗ` for the integer `a − b`. Avoids clash with
85list and matrix notations. -/
86notation:max "[" a ", " b "]ₗ" => mk a b
87
88theorem sound (a b c d : LogicNat) (h : a + d = c + b) :
89 mk a b = mk c d := by
90 apply Quotient.sound
91 show a + d = c + b
92 exact h
93
94/-! ## 3. Embedding LogicNat into LogicInt -/
95
96/-- The natural injection `LogicNat ↪ LogicInt` sending `n` to `[n, 0]`.
97This is the inclusion of the additive monoid into its Grothendieck group. -/
98def ofLogicNat (n : LogicNat) : LogicInt := mk n LogicNat.zero
99
100@[simp] theorem ofLogicNat_zero : ofLogicNat LogicNat.zero = mk LogicNat.zero LogicNat.zero := rfl