toInt_add
open lean source
IndisputableMonolith.Foundation.IntegersFromLogic on GitHub at line 323.
browse module
All declarations in this module, on Recognition.
plain-language theorem explainer
The recovery map from the Grothendieck completion of LogicNat to the integers preserves addition. Authors proving the ring axioms on LogicInt cite it to reduce identities to the standard integers via the transfer equivalence. The argument proceeds by double quotient induction on representatives, reduction through the natural-number addition recovery, and ring normalization.
Claim. Let $I$ be the Grothendieck completion of LogicNat under addition, with recovery map toInt : $I$ → ℤ defined by lifting the core difference map. Then toInt($a + b$) = toInt($a$) + toInt($b$) for all $a, b$ ∈ $I$.
background
LogicInt is the quotient of LogicNat × LogicNat by the setoid equivalence, serving as the Grothendieck completion of LogicNat under addition. The constructor mk forms an element from a pair of logic naturals, and toInt is the lift of toIntCore that sends the class of (a, b) to toNat a − toNat b. The upstream result toNat_add states that the addition LogicNat carries agrees with Nat addition under the equivalence.
proof idea
The proof applies Quotient.inductionOn to both arguments. After rcasing the representatives to pairs, it rewrites using toInt_mk three times and toNat_add twice. The push_cast and ring tactics then close the algebraic identity.
why it matters
This result is invoked by add_assoc', add_comm', add_zero', add_left_neg', mul_add' and add_mul' through the transfer principle that an equation in LogicInt holds iff it holds under toInt. It completes the addition-homomorphism step in the integer construction, allowing LogicInt to inherit the ring structure of Int before the rational layer is built.
depends on
used by
formal source
320 rw [toInt_mk, toNat_succ, toNat_zero]
321 norm_num
322
323theorem toInt_add (a b : LogicInt) : toInt (a + b) = toInt a + toInt b := by
324 induction a using Quotient.inductionOn with
325 | h p =>
326 induction b using Quotient.inductionOn with
327 | h q =>
328 rcases p with ⟨a, b⟩
329 rcases q with ⟨c, d⟩
330 show toInt (mk (a + c) (b + d)) = toInt (mk a b) + toInt (mk c d)
331 rw [toInt_mk, toInt_mk, toInt_mk]
332 rw [toNat_add, toNat_add]
333 push_cast
334 ring
335
336theorem toInt_neg (a : LogicInt) : toInt (-a) = -toInt a := by
337 induction a using Quotient.inductionOn with
338 | h p =>
339 rcases p with ⟨a, b⟩
340 show toInt (mk b a) = -toInt (mk a b)
341 rw [toInt_mk, toInt_mk]
342 ring
343
344theorem toInt_mul (a b : LogicInt) : toInt (a * b) = toInt a * toInt b := by
345 induction a using Quotient.inductionOn with
346 | h p =>
347 induction b using Quotient.inductionOn with
348 | h q =>
349 rcases p with ⟨a, b⟩
350 rcases q with ⟨c, d⟩
351 show toInt (mk (a * c + b * d) (a * d + b * c)) = toInt (mk a b) * toInt (mk c d)
352 rw [toInt_mk, toInt_mk, toInt_mk]
353 rw [toNat_add, toNat_add, toNat_mul, toNat_mul, toNat_mul, toNat_mul]