2014-12-23 22:34:16 +00:00
|
|
|
|
/-
|
|
|
|
|
Copyright (c) 2014 Floris van Doorn. All rights reserved.
|
|
|
|
|
Released under Apache 2.0 license as described in the file LICENSE.
|
|
|
|
|
Authors: Floris van Doorn, Leonardo de Moura, Jeremy Avigad
|
|
|
|
|
|
|
|
|
|
Basic operations on the natural numbers.
|
|
|
|
|
-/
|
2015-02-01 14:55:12 +00:00
|
|
|
|
import logic.connectives data.num algebra.binary algebra.ring
|
2015-01-08 20:12:30 +00:00
|
|
|
|
open binary eq.ops
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
2014-09-04 22:03:59 +00:00
|
|
|
|
namespace nat
|
|
|
|
|
|
2014-12-23 22:34:16 +00:00
|
|
|
|
/- a variant of add, defined by recursion on the first argument -/
|
|
|
|
|
|
2014-11-18 05:58:42 +00:00
|
|
|
|
definition addl (x y : ℕ) : ℕ :=
|
|
|
|
|
nat.rec y (λ n r, succ r) x
|
2015-09-30 15:06:31 +00:00
|
|
|
|
infix ` ⊕ `:65 := addl
|
2014-11-18 05:58:42 +00:00
|
|
|
|
|
2015-04-18 17:50:30 +00:00
|
|
|
|
theorem addl_succ_right (n m : ℕ) : n ⊕ succ m = succ (n ⊕ m) :=
|
2014-11-18 05:58:42 +00:00
|
|
|
|
nat.induction_on n
|
|
|
|
|
rfl
|
|
|
|
|
(λ n₁ ih, calc
|
|
|
|
|
succ n₁ ⊕ succ m = succ (n₁ ⊕ succ m) : rfl
|
|
|
|
|
... = succ (succ (n₁ ⊕ m)) : ih
|
|
|
|
|
... = succ (succ n₁ ⊕ m) : rfl)
|
|
|
|
|
|
|
|
|
|
theorem add_eq_addl (x : ℕ) : ∀y, x + y = x ⊕ y :=
|
|
|
|
|
nat.induction_on x
|
|
|
|
|
(λ y, nat.induction_on y
|
|
|
|
|
rfl
|
|
|
|
|
(λ y₁ ih, calc
|
2015-10-13 20:16:19 +00:00
|
|
|
|
0 + succ y₁ = succ (0 + y₁) : rfl
|
|
|
|
|
... = succ (0 ⊕ y₁) : {ih}
|
|
|
|
|
... = 0 ⊕ (succ y₁) : rfl))
|
2014-11-18 05:58:42 +00:00
|
|
|
|
(λ x₁ ih₁ y, nat.induction_on y
|
|
|
|
|
(calc
|
2015-10-13 20:16:19 +00:00
|
|
|
|
succ x₁ + 0 = succ (x₁ + 0) : rfl
|
|
|
|
|
... = succ (x₁ ⊕ 0) : {ih₁ 0}
|
|
|
|
|
... = succ x₁ ⊕ 0 : rfl)
|
2014-11-18 05:58:42 +00:00
|
|
|
|
(λ y₁ ih₂, calc
|
|
|
|
|
succ x₁ + succ y₁ = succ (succ x₁ + y₁) : rfl
|
|
|
|
|
... = succ (succ x₁ ⊕ y₁) : {ih₂}
|
2015-04-18 17:50:30 +00:00
|
|
|
|
... = succ x₁ ⊕ succ y₁ : addl_succ_right))
|
2014-11-18 05:58:42 +00:00
|
|
|
|
|
2014-12-23 22:34:16 +00:00
|
|
|
|
/- successor and predecessor -/
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
2014-10-02 01:50:17 +00:00
|
|
|
|
theorem succ_ne_zero (n : ℕ) : succ n ≠ 0 :=
|
2015-04-30 20:56:12 +00:00
|
|
|
|
by contradiction
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
|
|
|
|
-- add_rewrite succ_ne_zero
|
|
|
|
|
|
2015-07-22 16:01:42 +00:00
|
|
|
|
theorem pred_zero [simp] : pred 0 = 0 :=
|
2014-11-22 08:15:51 +00:00
|
|
|
|
rfl
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
2015-07-22 16:01:42 +00:00
|
|
|
|
theorem pred_succ [simp] (n : ℕ) : pred (succ n) = n :=
|
2014-11-22 08:15:51 +00:00
|
|
|
|
rfl
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
2014-12-23 22:34:16 +00:00
|
|
|
|
theorem eq_zero_or_eq_succ_pred (n : ℕ) : n = 0 ∨ n = succ (pred n) :=
|
2015-02-11 20:49:27 +00:00
|
|
|
|
nat.induction_on n
|
2014-09-05 04:25:21 +00:00
|
|
|
|
(or.inl rfl)
|
|
|
|
|
(take m IH, or.inr
|
2015-01-07 01:54:15 +00:00
|
|
|
|
(show succ m = succ (pred (succ m)), from congr_arg succ !pred_succ⁻¹))
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
2014-12-26 21:25:05 +00:00
|
|
|
|
theorem exists_eq_succ_of_ne_zero {n : ℕ} (H : n ≠ 0) : ∃k : ℕ, n = succ k :=
|
|
|
|
|
exists.intro _ (or_resolve_right !eq_zero_or_eq_succ_pred H)
|
|
|
|
|
|
2015-06-15 11:10:03 +00:00
|
|
|
|
theorem succ.inj {n m : ℕ} (H : succ n = succ m) : n = m :=
|
2015-07-24 15:56:18 +00:00
|
|
|
|
nat.no_confusion H imp.id
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
2015-06-15 11:10:03 +00:00
|
|
|
|
abbreviation eq_of_succ_eq_succ := @succ.inj
|
|
|
|
|
|
2015-04-18 17:50:30 +00:00
|
|
|
|
theorem succ_ne_self {n : ℕ} : succ n ≠ n :=
|
2015-02-11 20:49:27 +00:00
|
|
|
|
nat.induction_on n
|
2014-08-02 01:40:24 +00:00
|
|
|
|
(take H : 1 = 0,
|
2014-10-02 01:50:17 +00:00
|
|
|
|
have ne : 1 ≠ 0, from !succ_ne_zero,
|
2014-08-02 01:40:24 +00:00
|
|
|
|
absurd H ne)
|
2015-06-15 11:10:03 +00:00
|
|
|
|
(take k IH H, IH (succ.inj H))
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
2014-11-22 08:15:51 +00:00
|
|
|
|
theorem discriminate {B : Prop} {n : ℕ} (H1: n = 0 → B) (H2 : ∀m, n = succ m → B) : B :=
|
2015-02-11 20:49:27 +00:00
|
|
|
|
have H : n = n → B, from nat.cases_on n H1 H2,
|
2014-12-23 22:34:16 +00:00
|
|
|
|
H rfl
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
|
|
|
|
theorem two_step_induction_on {P : ℕ → Prop} (a : ℕ) (H1 : P 0) (H2 : P 1)
|
|
|
|
|
(H3 : ∀ (n : ℕ) (IH1 : P n) (IH2 : P (succ n)), P (succ (succ n))) : P a :=
|
|
|
|
|
have stronger : P a ∧ P (succ a), from
|
2015-02-11 20:49:27 +00:00
|
|
|
|
nat.induction_on a
|
2014-09-04 23:36:06 +00:00
|
|
|
|
(and.intro H1 H2)
|
2014-08-02 01:40:24 +00:00
|
|
|
|
(take k IH,
|
2014-09-05 00:44:53 +00:00
|
|
|
|
have IH1 : P k, from and.elim_left IH,
|
|
|
|
|
have IH2 : P (succ k), from and.elim_right IH,
|
2014-09-04 23:36:06 +00:00
|
|
|
|
and.intro IH2 (H3 k IH1 IH2)),
|
2014-09-05 00:44:53 +00:00
|
|
|
|
and.elim_left stronger
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
|
|
|
|
theorem sub_induction {P : ℕ → ℕ → Prop} (n m : ℕ) (H1 : ∀m, P 0 m)
|
|
|
|
|
(H2 : ∀n, P (succ n) 0) (H3 : ∀n m, P n m → P (succ n) (succ m)) : P n m :=
|
2015-07-24 15:56:18 +00:00
|
|
|
|
have general : ∀m, P n m, from nat.induction_on n H1
|
2014-08-02 01:40:24 +00:00
|
|
|
|
(take k : ℕ,
|
|
|
|
|
assume IH : ∀m, P k m,
|
|
|
|
|
take m : ℕ,
|
2015-02-11 20:49:27 +00:00
|
|
|
|
nat.cases_on m (H2 k) (take l, (H3 k l (IH l)))),
|
2014-12-23 22:34:16 +00:00
|
|
|
|
general m
|
|
|
|
|
|
|
|
|
|
/- addition -/
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
2015-10-14 19:27:09 +00:00
|
|
|
|
protected theorem add_zero [simp] (n : ℕ) : n + 0 = n :=
|
2014-11-22 08:15:51 +00:00
|
|
|
|
rfl
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
2015-07-22 16:01:42 +00:00
|
|
|
|
theorem add_succ [simp] (n m : ℕ) : n + succ m = succ (n + m) :=
|
2014-11-22 08:15:51 +00:00
|
|
|
|
rfl
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
2015-10-14 19:27:09 +00:00
|
|
|
|
protected theorem zero_add [simp] (n : ℕ) : 0 + n = n :=
|
2015-02-11 20:49:27 +00:00
|
|
|
|
nat.induction_on n
|
2015-10-14 19:27:09 +00:00
|
|
|
|
!nat.add_zero
|
2014-08-02 01:40:24 +00:00
|
|
|
|
(take m IH, show 0 + succ m = succ m, from
|
|
|
|
|
calc
|
2014-12-23 22:34:16 +00:00
|
|
|
|
0 + succ m = succ (0 + m) : add_succ
|
2014-10-31 15:29:46 +00:00
|
|
|
|
... = succ m : IH)
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
2015-07-22 16:01:42 +00:00
|
|
|
|
theorem succ_add [simp] (n m : ℕ) : (succ n) + m = succ (n + m) :=
|
2015-02-11 20:49:27 +00:00
|
|
|
|
nat.induction_on m
|
2015-10-14 19:27:09 +00:00
|
|
|
|
(!nat.add_zero ▸ !nat.add_zero)
|
2014-08-27 01:47:36 +00:00
|
|
|
|
(take k IH, calc
|
2014-12-23 22:34:16 +00:00
|
|
|
|
succ n + succ k = succ (succ n + k) : add_succ
|
2014-10-31 15:29:46 +00:00
|
|
|
|
... = succ (succ (n + k)) : IH
|
2014-12-23 22:34:16 +00:00
|
|
|
|
... = succ (n + succ k) : add_succ)
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
2015-10-14 19:27:09 +00:00
|
|
|
|
protected theorem add_comm [simp] (n m : ℕ) : n + m = m + n :=
|
2015-02-11 20:49:27 +00:00
|
|
|
|
nat.induction_on m
|
2015-10-14 19:27:09 +00:00
|
|
|
|
(by rewrite [nat.add_zero, nat.zero_add])
|
2014-08-27 01:47:36 +00:00
|
|
|
|
(take k IH, calc
|
2014-12-23 22:34:16 +00:00
|
|
|
|
n + succ k = succ (n+k) : add_succ
|
2014-10-31 15:29:46 +00:00
|
|
|
|
... = succ (k + n) : IH
|
2015-04-18 17:50:30 +00:00
|
|
|
|
... = succ k + n : succ_add)
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
2015-02-25 18:32:50 +00:00
|
|
|
|
theorem succ_add_eq_succ_add (n m : ℕ) : succ n + m = n + succ m :=
|
2015-04-18 17:50:30 +00:00
|
|
|
|
!succ_add ⬝ !add_succ⁻¹
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
2015-10-14 19:27:09 +00:00
|
|
|
|
protected theorem add_assoc [simp] (n m k : ℕ) : (n + m) + k = n + (m + k) :=
|
2015-02-11 20:49:27 +00:00
|
|
|
|
nat.induction_on k
|
2015-10-14 19:27:09 +00:00
|
|
|
|
(by rewrite +nat.add_zero)
|
2014-08-02 01:40:24 +00:00
|
|
|
|
(take l IH,
|
|
|
|
|
calc
|
2014-12-23 22:34:16 +00:00
|
|
|
|
(n + m) + succ l = succ ((n + m) + l) : add_succ
|
2014-10-31 15:29:46 +00:00
|
|
|
|
... = succ (n + (m + l)) : IH
|
2014-12-23 22:34:16 +00:00
|
|
|
|
... = n + succ (m + l) : add_succ
|
|
|
|
|
... = n + (m + succ l) : add_succ)
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
2015-10-22 21:35:27 +00:00
|
|
|
|
protected theorem add_left_comm : Π (n m k : ℕ), n + (m + k) = m + (n + k) :=
|
2015-10-14 19:27:09 +00:00
|
|
|
|
left_comm nat.add_comm nat.add_assoc
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
2015-10-22 21:35:27 +00:00
|
|
|
|
protected theorem add_right_comm : Π (n m k : ℕ), n + m + k = n + k + m :=
|
2015-10-14 19:27:09 +00:00
|
|
|
|
right_comm nat.add_comm nat.add_assoc
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
2015-10-22 21:35:27 +00:00
|
|
|
|
protected theorem add_left_cancel {n m k : ℕ} : n + m = n + k → m = k :=
|
2015-02-11 20:49:27 +00:00
|
|
|
|
nat.induction_on n
|
2014-08-02 01:40:24 +00:00
|
|
|
|
(take H : 0 + m = 0 + k,
|
2015-10-14 19:27:09 +00:00
|
|
|
|
!nat.zero_add⁻¹ ⬝ H ⬝ !nat.zero_add)
|
2014-08-02 01:40:24 +00:00
|
|
|
|
(take (n : ℕ) (IH : n + m = n + k → m = k) (H : succ n + m = succ n + k),
|
2015-07-18 18:36:05 +00:00
|
|
|
|
have succ (n + m) = succ (n + k),
|
2014-08-02 01:40:24 +00:00
|
|
|
|
from calc
|
2015-04-18 17:50:30 +00:00
|
|
|
|
succ (n + m) = succ n + m : succ_add
|
2014-08-27 01:47:36 +00:00
|
|
|
|
... = succ n + k : H
|
2015-04-18 17:50:30 +00:00
|
|
|
|
... = succ (n + k) : succ_add,
|
2015-07-18 18:36:05 +00:00
|
|
|
|
have n + m = n + k, from succ.inj this,
|
|
|
|
|
IH this)
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
2015-10-22 21:35:27 +00:00
|
|
|
|
protected theorem add_right_cancel {n m k : ℕ} (H : n + m = k + m) : n = k :=
|
2015-10-14 19:27:09 +00:00
|
|
|
|
have H2 : m + n = m + k, from !nat.add_comm ⬝ H ⬝ !nat.add_comm,
|
2015-10-22 21:35:27 +00:00
|
|
|
|
nat.add_left_cancel H2
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
2014-12-23 22:34:16 +00:00
|
|
|
|
theorem eq_zero_of_add_eq_zero_right {n m : ℕ} : n + m = 0 → n = 0 :=
|
2015-02-11 20:49:27 +00:00
|
|
|
|
nat.induction_on n
|
2014-09-04 23:36:06 +00:00
|
|
|
|
(take (H : 0 + m = 0), rfl)
|
2014-08-02 01:40:24 +00:00
|
|
|
|
(take k IH,
|
2014-08-27 01:47:36 +00:00
|
|
|
|
assume H : succ k + m = 0,
|
2014-08-28 01:34:09 +00:00
|
|
|
|
absurd
|
2014-08-27 01:47:36 +00:00
|
|
|
|
(show succ (k + m) = 0, from calc
|
2015-04-18 17:50:30 +00:00
|
|
|
|
succ (k + m) = succ k + m : succ_add
|
2014-08-27 01:47:36 +00:00
|
|
|
|
... = 0 : H)
|
2014-10-02 01:50:17 +00:00
|
|
|
|
!succ_ne_zero)
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
2014-12-23 22:34:16 +00:00
|
|
|
|
theorem eq_zero_of_add_eq_zero_left {n m : ℕ} (H : n + m = 0) : m = 0 :=
|
2015-10-14 19:27:09 +00:00
|
|
|
|
eq_zero_of_add_eq_zero_right (!nat.add_comm ⬝ H)
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
2015-04-18 17:50:30 +00:00
|
|
|
|
theorem eq_zero_and_eq_zero_of_add_eq_zero {n m : ℕ} (H : n + m = 0) : n = 0 ∧ m = 0 :=
|
2014-12-23 22:34:16 +00:00
|
|
|
|
and.intro (eq_zero_of_add_eq_zero_right H) (eq_zero_of_add_eq_zero_left H)
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
2015-10-22 19:31:58 +00:00
|
|
|
|
theorem add_one [simp] (n : ℕ) : n + 1 = succ n := rfl
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
2014-12-23 22:34:16 +00:00
|
|
|
|
theorem one_add (n : ℕ) : 1 + n = succ n :=
|
2015-10-14 19:27:09 +00:00
|
|
|
|
!nat.zero_add ▸ !succ_add
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
2014-12-23 22:34:16 +00:00
|
|
|
|
/- multiplication -/
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
2015-10-14 19:27:09 +00:00
|
|
|
|
protected theorem mul_zero [simp] (n : ℕ) : n * 0 = 0 :=
|
2014-11-22 08:15:51 +00:00
|
|
|
|
rfl
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
2015-07-22 16:01:42 +00:00
|
|
|
|
theorem mul_succ [simp] (n m : ℕ) : n * succ m = n * m + n :=
|
2014-11-22 08:15:51 +00:00
|
|
|
|
rfl
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
2014-12-24 00:46:48 +00:00
|
|
|
|
-- commutativity, distributivity, associativity, identity
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
2015-10-14 19:27:09 +00:00
|
|
|
|
protected theorem zero_mul [simp] (n : ℕ) : 0 * n = 0 :=
|
2015-02-11 20:49:27 +00:00
|
|
|
|
nat.induction_on n
|
2015-10-14 19:27:09 +00:00
|
|
|
|
!nat.mul_zero
|
|
|
|
|
(take m IH, !mul_succ ⬝ !nat.add_zero ⬝ IH)
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
2015-07-22 16:01:42 +00:00
|
|
|
|
theorem succ_mul [simp] (n m : ℕ) : (succ n) * m = (n * m) + m :=
|
2015-02-11 20:49:27 +00:00
|
|
|
|
nat.induction_on m
|
2015-10-14 19:27:09 +00:00
|
|
|
|
(by rewrite nat.mul_zero)
|
2014-08-27 01:47:36 +00:00
|
|
|
|
(take k IH, calc
|
2014-12-23 22:34:16 +00:00
|
|
|
|
succ n * succ k = succ n * k + succ n : mul_succ
|
|
|
|
|
... = n * k + k + succ n : IH
|
2015-10-14 19:27:09 +00:00
|
|
|
|
... = n * k + (k + succ n) : nat.add_assoc
|
|
|
|
|
... = n * k + (succ n + k) : nat.add_comm
|
2015-02-25 18:32:50 +00:00
|
|
|
|
... = n * k + (n + succ k) : succ_add_eq_succ_add
|
2015-10-14 19:27:09 +00:00
|
|
|
|
... = n * k + n + succ k : nat.add_assoc
|
2014-12-23 22:34:16 +00:00
|
|
|
|
... = n * succ k + succ k : mul_succ)
|
2014-08-27 01:47:36 +00:00
|
|
|
|
|
2015-10-14 19:27:09 +00:00
|
|
|
|
protected theorem mul_comm [simp] (n m : ℕ) : n * m = m * n :=
|
2015-02-11 20:49:27 +00:00
|
|
|
|
nat.induction_on m
|
2015-10-14 19:27:09 +00:00
|
|
|
|
(!nat.mul_zero ⬝ !nat.zero_mul⁻¹)
|
2014-08-27 01:47:36 +00:00
|
|
|
|
(take k IH, calc
|
2014-12-23 22:34:16 +00:00
|
|
|
|
n * succ k = n * k + n : mul_succ
|
2014-10-31 15:29:46 +00:00
|
|
|
|
... = k * n + n : IH
|
2014-12-23 22:34:16 +00:00
|
|
|
|
... = (succ k) * n : succ_mul)
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
2015-10-14 19:27:09 +00:00
|
|
|
|
protected theorem right_distrib (n m k : ℕ) : (n + m) * k = n * k + m * k :=
|
2015-02-11 20:49:27 +00:00
|
|
|
|
nat.induction_on k
|
2014-08-02 01:40:24 +00:00
|
|
|
|
(calc
|
2015-10-14 19:27:09 +00:00
|
|
|
|
(n + m) * 0 = 0 : nat.mul_zero
|
|
|
|
|
... = 0 + 0 : nat.add_zero
|
|
|
|
|
... = n * 0 + 0 : nat.mul_zero
|
|
|
|
|
... = n * 0 + m * 0 : nat.mul_zero)
|
2014-08-02 01:40:24 +00:00
|
|
|
|
(take l IH, calc
|
2014-12-23 22:34:16 +00:00
|
|
|
|
(n + m) * succ l = (n + m) * l + (n + m) : mul_succ
|
2014-10-31 15:29:46 +00:00
|
|
|
|
... = n * l + m * l + (n + m) : IH
|
2015-10-14 19:27:09 +00:00
|
|
|
|
... = n * l + m * l + n + m : nat.add_assoc
|
2015-10-22 21:35:27 +00:00
|
|
|
|
... = n * l + n + m * l + m : nat.add_right_comm
|
2015-10-14 19:27:09 +00:00
|
|
|
|
... = n * l + n + (m * l + m) : nat.add_assoc
|
2014-12-23 22:34:16 +00:00
|
|
|
|
... = n * succ l + (m * l + m) : mul_succ
|
|
|
|
|
... = n * succ l + m * succ l : mul_succ)
|
2014-08-27 01:47:36 +00:00
|
|
|
|
|
2015-10-14 19:27:09 +00:00
|
|
|
|
protected theorem left_distrib (n m k : ℕ) : n * (m + k) = n * m + n * k :=
|
2014-08-02 01:40:24 +00:00
|
|
|
|
calc
|
2015-10-14 19:27:09 +00:00
|
|
|
|
n * (m + k) = (m + k) * n : nat.mul_comm
|
|
|
|
|
... = m * n + k * n : nat.right_distrib
|
|
|
|
|
... = n * m + k * n : nat.mul_comm
|
|
|
|
|
... = n * m + n * k : nat.mul_comm
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
2015-10-14 19:27:09 +00:00
|
|
|
|
protected theorem mul_assoc [simp] (n m k : ℕ) : (n * m) * k = n * (m * k) :=
|
2015-02-11 20:49:27 +00:00
|
|
|
|
nat.induction_on k
|
2014-08-02 01:40:24 +00:00
|
|
|
|
(calc
|
2015-10-14 19:27:09 +00:00
|
|
|
|
(n * m) * 0 = n * (m * 0) : nat.mul_zero)
|
2014-08-02 01:40:24 +00:00
|
|
|
|
(take l IH,
|
|
|
|
|
calc
|
2014-12-23 22:34:16 +00:00
|
|
|
|
(n * m) * succ l = (n * m) * l + n * m : mul_succ
|
2014-10-31 15:29:46 +00:00
|
|
|
|
... = n * (m * l) + n * m : IH
|
2015-10-14 19:27:09 +00:00
|
|
|
|
... = n * (m * l + m) : nat.left_distrib
|
2014-12-23 22:34:16 +00:00
|
|
|
|
... = n * (m * succ l) : mul_succ)
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
2015-10-14 19:27:09 +00:00
|
|
|
|
protected theorem mul_one [simp] (n : ℕ) : n * 1 = n :=
|
2014-08-02 01:40:24 +00:00
|
|
|
|
calc
|
2014-12-23 22:34:16 +00:00
|
|
|
|
n * 1 = n * 0 + n : mul_succ
|
2015-10-14 19:27:09 +00:00
|
|
|
|
... = 0 + n : nat.mul_zero
|
|
|
|
|
... = n : nat.zero_add
|
2014-08-02 01:40:24 +00:00
|
|
|
|
|
2015-10-14 19:27:09 +00:00
|
|
|
|
protected theorem one_mul [simp] (n : ℕ) : 1 * n = n :=
|
2014-08-02 01:40:24 +00:00
|
|
|
|
calc
|
2015-10-14 19:27:09 +00:00
|
|
|
|
1 * n = n * 1 : nat.mul_comm
|
|
|
|
|
... = n : nat.mul_one
|
2014-12-23 22:34:16 +00:00
|
|
|
|
|
|
|
|
|
theorem eq_zero_or_eq_zero_of_mul_eq_zero {n m : ℕ} : n * m = 0 → n = 0 ∨ m = 0 :=
|
2015-02-11 20:49:27 +00:00
|
|
|
|
nat.cases_on n
|
2014-12-23 22:34:16 +00:00
|
|
|
|
(assume H, or.inl rfl)
|
|
|
|
|
(take n',
|
2015-02-11 20:49:27 +00:00
|
|
|
|
nat.cases_on m
|
2014-12-23 22:34:16 +00:00
|
|
|
|
(assume H, or.inr rfl)
|
|
|
|
|
(take m',
|
|
|
|
|
assume H : succ n' * succ m' = 0,
|
|
|
|
|
absurd
|
2015-07-20 04:15:20 +00:00
|
|
|
|
(calc
|
2014-12-23 22:34:16 +00:00
|
|
|
|
0 = succ n' * succ m' : H
|
|
|
|
|
... = succ n' * m' + succ n' : mul_succ
|
2015-07-20 04:15:20 +00:00
|
|
|
|
... = succ (succ n' * m' + n') : add_succ)⁻¹
|
2014-12-23 22:34:16 +00:00
|
|
|
|
!succ_ne_zero))
|
2015-02-01 14:55:12 +00:00
|
|
|
|
|
2015-12-06 07:27:46 +00:00
|
|
|
|
protected definition comm_semiring [reducible] [trans_instance] : comm_semiring nat :=
|
|
|
|
|
⦃comm_semiring,
|
2015-10-07 23:44:47 +00:00
|
|
|
|
add := nat.add,
|
2015-10-14 19:27:09 +00:00
|
|
|
|
add_assoc := nat.add_assoc,
|
2015-10-07 23:44:47 +00:00
|
|
|
|
zero := nat.zero,
|
2015-10-14 19:27:09 +00:00
|
|
|
|
zero_add := nat.zero_add,
|
|
|
|
|
add_zero := nat.add_zero,
|
|
|
|
|
add_comm := nat.add_comm,
|
2015-10-07 23:44:47 +00:00
|
|
|
|
mul := nat.mul,
|
2015-10-14 19:27:09 +00:00
|
|
|
|
mul_assoc := nat.mul_assoc,
|
2015-10-07 23:44:47 +00:00
|
|
|
|
one := nat.succ nat.zero,
|
2015-10-14 19:27:09 +00:00
|
|
|
|
one_mul := nat.one_mul,
|
|
|
|
|
mul_one := nat.mul_one,
|
|
|
|
|
left_distrib := nat.left_distrib,
|
|
|
|
|
right_distrib := nat.right_distrib,
|
|
|
|
|
zero_mul := nat.zero_mul,
|
|
|
|
|
mul_zero := nat.mul_zero,
|
|
|
|
|
mul_comm := nat.mul_comm⦄
|
2014-08-20 02:32:44 +00:00
|
|
|
|
end nat
|
2015-09-16 00:29:54 +00:00
|
|
|
|
|
|
|
|
|
section
|
|
|
|
|
open nat
|
|
|
|
|
definition iterate {A : Type} (op : A → A) : ℕ → A → A
|
|
|
|
|
| 0 := λ a, a
|
|
|
|
|
| (succ k) := λ a, op (iterate k a)
|
|
|
|
|
|
|
|
|
|
notation f`^[`n`]` := iterate f n
|
|
|
|
|
end
|