mathlib documentation

lean_problem_sheets / 2020.integers.int_def_solns

source
def nat2.R (a b : ℕ × ℕ) :
Prop

The equivalence relation on ℕ² such that equivalence classes are ℤ

Equations
source
@[protected, instance]
def prod.has_equiv  :
has_equiv (ℕ × ℕ)
Equations
source
@[simp]
theorem nat2.R.equiv_def {i j k l : ℕ} :
(i, j) ≈ (k, l) ↔ i + l = k + j
source
theorem nat2.R.practice  :
(3, 5) ≈ (4, 6)
source
theorem nat2.R.reflexive (x : ℕ × ℕ) :
x ≈ x
source
theorem nat2.R.symmetric (x y : ℕ × ℕ) :
x ≈ y → y ≈ x
source
theorem nat2.R.transitive (x y z : ℕ × ℕ) :
x ≈ y → y ≈ z → x ≈ z
source
@[protected, instance]
def nat2.R.setoid  :
setoid (ℕ × ℕ)
Equations
source
def myint  :
Type

The integers are the equivalence classes of the equivalence relation we just defined on ℕ²

Equations

zero #

source
def myint.zero  :
quotient nat2.R.setoid
Equations
source
@[protected, instance]
def myint.has_zero  :
has_zero myint
Equations
source
theorem myint.zero_def  :
0 = ⟦(0, 0)⟧

negation (additive inverse) #

source
def myint.neg_aux (x : ℕ × ℕ) :
myint
Equations
source
theorem myint.neg_aux_def (i j : ℕ) :
myint.neg_aux (i, j) = ⟦(j, i)⟧

Well-definedness #

OK now here's the concrete problem. We would like to define a negation map ℤ → ℤ sending z to -z. We want to do this in the following way: Say z ∈ ℤ. Choose a=(i,j) ∈ ℕ² representing z (i.e. such that cl(i,j) = ⟦(i,j)⟧ = z) Now apply neg_aux to a, and define -z to be the result.

The problem with this is that what if b is a different element of the equivalence class? Then we also want -z to be neg_aux b.

Indeed, in Lean this construction is called quotient.lift, and if you uncomment the below code

source
theorem myint.neg_aux_lemma (x y : ℕ × ℕ) :
x ≈ y → myint.neg_aux x = myint.neg_aux y
source
def myint.neg  :
myint → myint

Negation on on the integers. The function sending z to -z.

Equations
source
@[protected, instance]
def myint.has_neg  :
has_neg myint
Equations
source
theorem myint.neg_def (i j : ℕ) :
-⟦(i, j)⟧ = ⟦(j, i)⟧

addition #

Our final construction: we want to define addition on myint. Here we have the same problem. Say z₁ and z₂ are integers. Choose elements a₁=(i,j) and a₂=(k,l) in ℕ². We want to define z₁ + z₂ to be ⟦(i+k,j+l)⟧, the equivalence class of a₁ + a₂. Let's make this definition now.

source
def myint.add_aux (x y : ℕ × ℕ) :
myint

An auxiliary function taking two elements of ℕ² and returning the equivalence class of their sum.

Equations
source
theorem myint.add_aux_def (i j k l : ℕ) :
myint.add_aux (i, j) (k, l) = ⟦(i + k, j + l)⟧
source
theorem myint.add_aux_lemma (x₁ x₂ y₁ y₂ : ℕ × ℕ) :
x₁ ≈ y₁ → x₂ ≈ y₂ → myint.add_aux x₁ x₂ = myint.add_aux y₁ y₂
source
def myint.add  :
myint → myint → myint

Addition on the integers

Equations
source
@[protected, instance]
def myint.has_add  :
has_add myint
Equations
source
theorem myint.add_def (i j k l : ℕ) :
⟦(i, j)⟧ + ⟦(k, l)⟧ = ⟦(i + k, j + l)⟧
source
theorem myint.zero_add (x : myint) :
0 + x = x
source
theorem myint.add_zero (x : myint) :
x + 0 = x
source
theorem myint.add_left_neg (x : myint) :
-x + x = 0
source
theorem myint.add_comm (x y : myint) :
x + y = y + x
source
theorem myint.add_assoc (x y z : myint) :
x + y + z = x + (y + z)
source
@[protected, instance]
def myint.add_comm_group  :
add_comm_group myint
Equations

multiplication #

What's left to define is 1 and multiplication (note that we don't need multiplicative inverses -- if a is a non-zero integer then a⁻¹ is typially not an integer)

source
def myint.mul_aux (x y : ℕ × ℕ) :
myint
Equations
source
theorem myint.mul_aux_def (i j k l : ℕ) :
myint.mul_aux (i, j) (k, l) = ⟦(i * k + j * l, i * l + j * k)⟧
source
theorem myint.mul_aux_lemma (x₁ x₂ y₁ y₂ : ℕ × ℕ) :
x₁ ≈ y₁ → x₂ ≈ y₂ → myint.mul_aux x₁ x₂ = myint.mul_aux y₁ y₂
source
def myint.mul  :
myint → myint → myint
Equations
source
@[protected, instance]
def myint.has_mul  :
has_mul myint
Equations
source
theorem myint.mul_def (i j k l : ℕ) :
⟦(i, j)⟧ * ⟦(k, l)⟧ = ⟦(i * k + j * l, i * l + j * k)⟧
source
theorem myint.mul_assoc (x y z : myint) :
(x * y) * z = x * y * z
source
def myint.one  :
myint
Equations
source
@[protected, instance]
def myint.has_one  :
has_one myint
Equations
source
theorem myint.one_def  :
1 = ⟦(37, 36)⟧
source
theorem myint.one_mul (x : myint) :
1 * x = x
source
theorem myint.mul_one (x : myint) :
x * 1 = x
source
theorem myint.mul_comm (x y : myint) :
x * y = y * x
source
theorem myint.mul_add (x y z : myint) :
x * (y + z) = x * y + x * z
source
theorem myint.add_mul (x y z : myint) :
(x + y) * z = x * z + y * z
source
@[protected, instance]
def myint.comm_ring  :
comm_ring myint
Equations