Documentation

Numbers.naturals

In this file we define our copy MyNat of the natural numbers. To check that we don't cheat using results already proved in mathlib we don't import any mathematics (the only import provides code actions, improving the editor experience). (Note that even if MyNat is defined here, the simple fact of, say, providing the Semiring instance allows to use a lot of results in mathlib.)

inductive MyNat :

Our copy of the natural numbers.

zero : MyNat
succ : MyNat → MyNat

Instances For

@[implicit_reducible]

instance MyNat.instZero :

The following is to activate the notation (0 : MyNat). Beware: if you just write 0, sometimes Lean thinks you mean the "usual" natural number 0.

Equations

MyNat.instZero = { zero := MyNat.zero }

theorem MyNat.zero_def :

def MyNat.one :

Equations

MyNat.one = MyNat.succ 0

Instances For

@[implicit_reducible]

instance MyNat.instOne :

Equations

MyNat.instOne = { one := MyNat.one }

theorem MyNat.one_def :

theorem MyNat.one_eq_succ_zero :

1 = succ 0

theorem MyNat.succ_ne_zero (a : MyNat) :

This is basically an axiom added by Lean when defining natural numbers (feel free to ask for more details if you want!)

theorem MyNat.one_ne_zero :

1 ≠ 0

theorem MyNat.zero_ne_one :

0 ≠ 1

def MyNat.add :

MyNat → MyNat → MyNat

Addition on MyNat.

Equations

x✝.add MyNat.zero = x✝
x✝.add b.succ = (x✝.add b).succ

Instances For

@[implicit_reducible]

instance MyNat.instAdd :

Equations

MyNat.instAdd = { add := MyNat.add }

theorem MyNat.add_zero (a : MyNat) :

a + 0 = a

theorem MyNat.add_succ (a b : MyNat) :

a + b.succ = (a + b).succ

theorem MyNat.succ_eq_add_one (a : MyNat) :

a.succ = a + 1

@[simp]

theorem MyNat.add_one_ne_zero (a : MyNat) :

a + 1 ≠ 0

theorem MyNat.zero_add (a : MyNat) :

0 + a = a

theorem MyNat.succ_add (a b : MyNat) :

a.succ + b = (a + b).succ

theorem MyNat.add_assoc (a b c : MyNat) :

a + b + c = a + (b + c)

theorem MyNat.add_comm (a b : MyNat) :

a + b = b + a

theorem MyNat.eq_zero_of_add_eq_zero {a b : MyNat} (h : a + b = 0) :

a = 0

def MyNat.mul :

MyNat → MyNat → MyNat

Multiplication on MyNat.

Equations

x✝.mul MyNat.zero = 0
x✝.mul b.succ = x✝.mul b + x✝

Instances For

@[implicit_reducible]

instance MyNat.instMul :

Equations

MyNat.instMul = { mul := MyNat.mul }

theorem MyNat.mul_zero (a : MyNat) :

a * 0 = 0

theorem MyNat.mul_succ (a b : MyNat) :

a * b.succ = a * b + a

theorem MyNat.succ_mul (a b : MyNat) :

a.succ * b = a * b + b

theorem MyNat.zero_mul (a : MyNat) :

0 * a = 0

theorem MyNat.left_distrib (a b c : MyNat) :

a * (b + c) = a * b + a * c

theorem MyNat.mul_one (a : MyNat) :

a * 1 = a

theorem MyNat.mul_comm (a b : MyNat) :

a * b = b * a

theorem MyNat.right_distrib (a b c : MyNat) :

(a + b) * c = a * c + b * c

theorem MyNat.one_mul (a : MyNat) :

1 * a = a

theorem MyNat.mul_assoc (a b c : MyNat) :

a * b * c = a * (b * c)

theorem MyNat.add_left_cancel {a b c : MyNat} (h : a + b = a + c) :

b = c

In this one you may find useful to use succ.inj, the succ function is injective.

theorem MyNat.mul_ne_zero {a b : MyNat} :

a ≠ 0 → b ≠ 0 → a * b ≠ 0

def MyNat.pred :

MyNat → MyNat

The predecessor function, with pred 0 = 0.

Equations

MyNat.zero.pred = 0
a.succ.pred = a

Instances For

@[simp]

theorem MyNat.pred_zero :

pred 0 = 0

theorem MyNat.pred_succ (a : MyNat) :

a.succ.pred = a

@[simp]

theorem MyNat.add_one_pred (a : MyNat) :

(a + 1).pred = a

theorem MyNat.succ_pred {a : MyNat} (ha : a ≠ 0) :

a.pred.succ = a

@[simp]

theorem MyNat.pred_add_one {a : MyNat} (ha : a ≠ 0) :

a.pred + 1 = a

def MyNat.le (a b : MyNat) :

The order relation on MyNat.

Equations

a.le b = ∃ (x : MyNat ), b = a + x

Instances For

@[implicit_reducible]

instance MyNat.instLE :

Equations

MyNat.instLE = { le := MyNat.le }

@[simp]

theorem MyNat.zero_le (a : MyNat) :

0 ≤ a

theorem MyNat.le_succ (a : MyNat) :

theorem MyNat.le_refl (a : MyNat) :

a ≤ a

theorem MyNat.le_trans {a b c : MyNat} (hab : a ≤ b) (hbc : b ≤ c) :

a ≤ c

theorem MyNat.le_antisymm {a b : MyNat} (hab : a ≤ b) (hba : b ≤ a) :

a = b

theorem MyNat.le_total (a b : MyNat) :

a ≤ b ∨ b ≤ a

theorem MyNat.le_self_add (a b : MyNat) :

a ≤ a + b

theorem MyNat.le_add_self (a b : MyNat) :

a ≤ b + a

@[simp]

theorem MyNat.le_succ_iff_eq_succ_or_le (a b : MyNat) :

a ≤ b.succ ↔ a = b.succ ∨ a ≤ b

def MyNat.lt (a b : MyNat) :

The obvious < relation.

Equations

a.lt b = (a ≤ b ∧ ¬b ≤ a)

Instances For

@[implicit_reducible]

instance MyNat.instLT :

Equations

MyNat.instLT = { lt := MyNat.lt }

theorem MyNat.lt_iff_le_and_ne {a b : MyNat} :

a < b ↔ a ≤ b ∧ a ≠ b

theorem MyNat.ne_zero_iff_pos (a : MyNat) :

a ≠ 0 ↔ 0 < a

theorem MyNat.lt_iff_ex_ne_zero (a b : MyNat) :

a < b ↔ ∃ (x : MyNat ), x ≠ 0 ∧ b = a + x

theorem MyNat.add_le_add_left {a b c : MyNat} (hab : a ≤ b) :

a + c ≤ b + c

theorem MyNat.mul_lt_mul_of_pos_left {a b c : MyNat} (hc : 0 < c) (hab : a < b) :

c * a < c * b

theorem MyNat.mul_lt_mul_of_pos_right {a b c : MyNat} (hc : 0 < c) (hab : a < b) :

a * c < b * c

theorem MyNat.le_of_add_le_add_left {a b c : MyNat} (h : a + b ≤ a + c) :

b ≤ c

theorem MyNat.mul_left_cancel_of_ne_zero {a b c : MyNat} (ha : a ≠ 0) (h : a * b = a * c) :

b = c

theorem MyNat.mul_right_cancel_of_ne_zero {a b c : MyNat} (ha : a ≠ 0) (h : b * a = c * a) :

b = c