@[reducible, inline]

abbrev Chapter2.Nat.add (n m : Nat) : Nat

Definition 2.2.1. (Addition of natural numbers). Compare with Mathlib's Nat.add

Equations

• n.add m = Chapter2.Nat.recurse (fun (x sum : Chapter2.Nat) => sum++) m n

@[implicit_reducible]

instance Chapter2.Nat.instAdd : Add Nat

This instance allows for the + notation to be used for natural number addition.

Equations

• Chapter2.Nat.instAdd = { add := Chapter2.Nat.add }

@[simp]

theorem Chapter2.Nat.zero_add (m : Nat) : 0 + m = m

Compare with Mathlib's Nat.zero_add.

theorem Chapter2.Nat.succ_add (n m : Nat) : n++ + m = (n + m)++

Compare with Mathlib's Nat.succ_add.

theorem Chapter2.Nat.one_add (m : Nat) : 1 + m = m++

Compare with Mathlib's Nat.one_add.

theorem Chapter2.Nat.two_add (m : Nat) : 2 + m = m++++

@[simp]

theorem Chapter2.Nat.add_zero (n : Nat) : n + 0 = n

Lemma 2.2.2 (n + 0 = n). Compare with Mathlib's Nat.add_zero.

theorem Chapter2.Nat.add_succ (n m : Nat) : n + m++ = (n + m)++

Lemma 2.2.3 (n+(m++) = (n+m)++). Compare with Mathlib's Nat.add_succ.

theorem Chapter2.Nat.succ_eq_add_one (n : Nat) : n++ = n + 1

n++ = n + 1 (Why?). Compare with Mathlib's Nat.succ_eq_add_one

theorem Chapter2.Nat.add_comm (n m : Nat) : n + m = m + n

Proposition 2.2.4 (Addition is commutative). Compare with Mathlib's Nat.add_comm

theorem Chapter2.Nat.add_assoc (a b c : Nat) : a + b + c = a + (b + c)

Proposition 2.2.5 (Addition is associative) / Exercise 2.2.1 Compare with Mathlib's Nat.add_assoc.

theorem Chapter2.Nat.add_left_cancel (a b c : Nat) (habc : a + b = a + c) : b = c

Proposition 2.2.6 (Cancellation law). Compare with Mathlib's Nat.add_left_cancel.

@[implicit_reducible]

instance Chapter2.Nat.addCommMonoid : AddCommMonoid Nat

(Not from textbook) Nat can be given the structure of a commutative additive monoid. This permits tactics such as abel to apply to the Chapter 2 natural numbers.

Equations

• One or more equations did not get rendered due to their size.

def Chapter2.Nat.IsPos (n : Nat) : Prop

Definition 2.2.7 (Positive natural numbers).

Equations

• n.IsPos = (n ≠ 0)

theorem Chapter2.Nat.isPos_iff (n : Nat) : n.IsPos ↔ n ≠ 0

theorem Chapter2.Nat.add_pos_left {a : Nat} (b : Nat) (ha : a.IsPos) : (a + b).IsPos

Proposition 2.2.8 (positive plus natural number is positive). Compare with Mathlib's Nat.add_pos_left.

theorem Chapter2.Nat.add_pos_right {a : Nat} (b : Nat) (ha : a.IsPos) : (b + a).IsPos

Compare with Mathlib's Nat.add_pos_right.

This theorem is a consequence of the previous theorem and add_comm, and grind can automatically discover such proofs.

theorem Chapter2.Nat.add_eq_zero (a b : Nat) (hab : a + b = 0) : a = 0 ∧ b = 0

Corollary 2.2.9 (if sum vanishes, then summands vanish). Compare with Mathlib's Nat.add_eq_zero.

theorem Chapter2.Nat.uniq_succ_eq (a : Nat) (ha : a.IsPos) : ∃! b : Nat, b++ = a

Lemma 2.2.10 (unique predecessor) / Exercise 2.2.2

@[implicit_reducible]

instance Chapter2.Nat.instLE : LE Nat

Definition 2.2.11 (Ordering of the natural numbers). This defines the ≤ notation on the natural numbers.

Equations

• Chapter2.Nat.instLE = { le := fun (n m : Chapter2.Nat) => ∃ (a : Chapter2.Nat), m = n + a }

@[implicit_reducible]

instance Chapter2.Nat.instLT : LT Nat

Definition 2.2.11 (Ordering of the natural numbers). This defines the < notation on the natural numbers.

Equations

• Chapter2.Nat.instLT = { lt := fun (n m : Chapter2.Nat) => n ≤ m ∧ n ≠ m }

theorem Chapter2.Nat.le_iff (n m : Nat) : n ≤ m ↔ ∃ (a : Nat), m = n + a

Compare with Mathlib's le_iff_exists_add.

theorem Chapter2.Nat.lt_iff (n m : Nat) : n < m ↔ (∃ (a : Nat), m = n + a) ∧ n ≠ m

theorem Chapter2.Nat.ge_iff_le (n m : Nat) : n ≥ m ↔ m ≤ n

Compare with Mathlib's ge_iff_le.

theorem Chapter2.Nat.gt_iff_lt (n m : Nat) : n > m ↔ m < n

Compare with Mathlib's gt_iff_lt.

theorem Chapter2.Nat.le_of_lt {n m : Nat} (hnm : n < m) : n ≤ m

Compare with Mathlib's Nat.le_of_lt.

theorem Chapter2.Nat.le_iff_lt_or_eq (n m : Nat) : n ≤ m ↔ n < m ∨ n = m

Compare with Mathlib's Nat.le_iff_lt_or_eq.

theorem Chapter2.Nat.succ_gt_self (n : Nat) : n++ > n

Compare with Mathlib's Nat.lt_succ_self.

theorem Chapter2.Nat.ge_refl (a : Nat) : a ≥ a

Proposition 2.2.12 (Basic properties of order for natural numbers) / Exercise 2.2.3

(a) (Order is reflexive). Compare with Mathlib's Nat.le_refl.

theorem Chapter2.Nat.le_refl (a : Nat) : a ≤ a

theorem Chapter2.Nat.ge_trans {a b c : Nat} (hab : a ≥ b) (hbc : b ≥ c) : a ≥ c

(b) (Order is transitive). The obtain tactic will be useful here. Compare with Mathlib's Nat.le_trans.

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

theorem Chapter2.Nat.ge_antisymm {a b : Nat} (hab : a ≥ b) (hba : b ≥ a) : a = b

(c) (Order is anti-symmetric). Compare with Mathlib's Nat.le_antisymm.

theorem Chapter2.Nat.add_ge_add_right (a b c : Nat) : a ≥ b ↔ a + c ≥ b + c

(d) (Addition preserves order). Compare with Mathlib's Nat.add_le_add_right.

theorem Chapter2.Nat.add_ge_add_left (a b c : Nat) : a ≥ b ↔ c + a ≥ c + b

(d) (Addition preserves order). Compare with Mathlib's Nat.add_le_add_left.

theorem Chapter2.Nat.add_le_add_right (a b c : Nat) : a ≤ b ↔ a + c ≤ b + c

(d) (Addition preserves order). Compare with Mathlib's Nat.add_le_add_right.

theorem Chapter2.Nat.add_le_add_left (a b c : Nat) : a ≤ b ↔ c + a ≤ c + b

(d) (Addition preserves order). Compare with Mathlib's Nat.add_le_add_left.

theorem Chapter2.Nat.lt_iff_succ_le (a b : Nat) : a < b ↔ a++ ≤ b

(e) a < b iff a++ ≤ b. Compare with Mathlib's Nat.succ_le_iff.

theorem Chapter2.Nat.lt_iff_add_pos (a b : Nat) : a < b ↔ ∃ (d : Nat), d.IsPos ∧ b = a + d

(f) a < b if and only if b = a + d for positive d.

theorem Chapter2.Nat.ne_of_lt (a b : Nat) : a < b → a ≠ b

If a < b then a ̸= b,

theorem Chapter2.Nat.ne_of_gt (a b : Nat) : a > b → a ≠ b

if a > b then a ̸= b.

theorem Chapter2.Nat.not_lt_of_gt (a b : Nat) : a < b ∧ a > b → False

If a > b and a < b then contradiction

theorem Chapter2.Nat.not_lt_self {a : Nat} (h : a < a) : False

theorem Chapter2.Nat.lt_of_le_of_lt {a b c : Nat} (hab : a ≤ b) (hbc : b < c) : a < c

theorem Chapter2.Nat.zero_le (a : Nat) : 0 ≤ a

This lemma was a why? statement from Proposition 2.2.13, but is more broadly useful, so is extracted here.

theorem Chapter2.Nat.trichotomous (a b : Nat) : a < b ∨ a = b ∨ a > b

Proposition 2.2.13 (Trichotomy of order for natural numbers) / Exercise 2.2.4 Compare with Mathlib's trichotomous. Parts of this theorem have been placed in the preceding Lean theorems.

def Chapter2.Nat.decLe (a b : Nat) : Decidable (a ≤ b)

(Not from textbook) Establish the decidability of this order computably. The portion of the proof involving decidability has been provided; the remaining sorries involve claims about the natural numbers. One could also have established this result by the classical tactic followed by exact Classical.decRel _, but this would make this definition (as well as some instances below) noncomputable.

Compare with Mathlib's Nat.decLe.

Equations

• One or more equations did not get rendered due to their size.
• Chapter2.Nat.zero.decLe x✝ = isTrue ⋯

@[implicit_reducible]

instance Chapter2.Nat.decidableRel : DecidableRel fun (x1 x2 : Nat) => x1 ≤ x2

Equations

• Chapter2.Nat.decidableRel = Chapter2.Nat.decLe

@[implicit_reducible]

instance Chapter2.Nat.instLinearOrder : LinearOrder Nat

(Not from textbook) Nat has the structure of a linear ordering. This allows for tactics such as order and calc to be applicable to the Chapter 2 natural numbers.

Equations

• One or more equations did not get rendered due to their size.

instance Chapter2.Nat.isOrderedAddMonoid : IsOrderedAddMonoid Nat

(Not from textbook) Nat has the structure of an ordered monoid. This allows for tactics such as gcongr to be applicable to the Chapter 2 natural numbers.

theorem Chapter2.Nat.strong_induction {m₀ : Nat} {P : Nat → Prop} (hind : ∀ m ≥ m₀, (∀ (m' : Nat), m₀ ≤ m' ∧ m' < m → P m') → P m) (m : Nat) : m ≥ m₀ → P m

Proposition 2.2.14 (Strong principle of induction) / Exercise 2.2.5 Compare with Mathlib's Nat.strong_induction_on.

theorem Chapter2.Nat.backwards_induction {n : Nat} {P : Nat → Prop} (hind : ∀ (m : Nat), P (m++) → P m) (hn : P n) (m : Nat) : m ≤ n → P m

Exercise 2.2.6 (backwards induction) Compare with Mathlib's Nat.decreasingInduction.

theorem Chapter2.Nat.induction_from {n : Nat} {P : Nat → Prop} (hind : ∀ (m : Nat), P m → P (m++)) : P n → ∀ m ≥ n, P m

Exercise 2.2.7 (induction from a starting point) Compare with Mathlib's Nat.le_induction.