lean2/library/data/nat/basic.lean
Leonardo de Moura dbaf81e16d refactor(library): remove unnecessary 'standard' subdirectory
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-23 18:08:09 -07:00

414 lines
13 KiB
Text
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

--- Copyright (c) 2014 Floris van Doorn. All rights reserved.
--- Released under Apache 2.0 license as described in the file LICENSE.
--- Author: Floris van Doorn
-- data.nat.basic
-- ==============
--
-- Basic operations on the natural numbers.
import logic data.num tools.tactic struc.binary tools.helper_tactics
using num tactic binary eq_ops
using decidable (hiding induction_on rec_on)
using relation -- for subst_iff
using helper_tactics
-- Definition of the type
-- ----------------------
namespace nat
inductive nat : Type :=
zero : nat,
succ : nat → nat
notation `` := nat
theorem nat_rec_zero {P : → Type} (x : P zero) (f : ∀m, P m → P (succ m)) : nat_rec x f zero = x
theorem nat_rec_succ {P : → Type} (x : P zero) (f : ∀m, P m → P (succ m)) (n : ) :
nat_rec x f (succ n) = f n (nat_rec x f n)
theorem induction_on {P : → Prop} (a : ) (H1 : P zero) (H2 : ∀ (n : ) (IH : P n), P (succ n)) :
P a :=
nat_rec H1 H2 a
definition rec_on {P : → Type} (n : ) (H1 : P zero) (H2 : ∀m, P m → P (succ m)) : P n :=
nat_rec H1 H2 n
-- Coercion from num
-- -----------------
abbreviation plus (x y : ) : :=
nat_rec x (λ n r, succ r) y
definition to_nat [coercion] [inline] (n : num) : :=
num_rec zero
(λ n, pos_num_rec (succ zero) (λ n r, plus r (plus r (succ zero))) (λ n r, plus r r) n) n
-- Successor and predecessor
-- -------------------------
theorem succ_ne_zero (n : ) : succ n ≠ 0 :=
assume H : succ n = 0,
have H2 : true = false, from
let f := (nat_rec false (fun a b, true)) in
calc
true = f (succ n) : rfl
... = f 0 : {H}
... = false : rfl,
absurd H2 true_ne_false
-- add_rewrite succ_ne_zero
definition pred (n : ) := nat_rec 0 (fun m x, m) n
theorem pred_zero : pred 0 = 0
theorem pred_succ (n : ) : pred (succ n) = n
opaque_hint (hiding pred)
theorem zero_or_succ_pred (n : ) : n = 0 n = succ (pred n) :=
induction_on n
(or_inl (refl 0))
(take m IH, or_inr
(show succ m = succ (pred (succ m)), from congr_arg succ (pred_succ m⁻¹)))
theorem zero_or_exists_succ (n : ) : n = 0 ∃k, n = succ k :=
or_imp_or (zero_or_succ_pred n) (assume H, H)
(assume H : n = succ (pred n), exists_intro (pred n) H)
theorem case {P : → Prop} (n : ) (H1: P 0) (H2 : ∀m, P (succ m)) : P n :=
induction_on n H1 (take m IH, H2 m)
theorem discriminate {B : Prop} {n : } (H1: n = 0 → B) (H2 : ∀m, n = succ m → B) : B :=
or_elim (zero_or_succ_pred n)
(take H3 : n = 0, H1 H3)
(take H3 : n = succ (pred n), H2 (pred n) H3)
theorem succ_inj {n m : } (H : succ n = succ m) : n = m :=
calc
n = pred (succ n) : pred_succ n⁻¹
... = pred (succ m) : {H}
... = m : pred_succ m
theorem succ_ne_self (n : ) : succ n ≠ n :=
induction_on n
(take H : 1 = 0,
have ne : 1 ≠ 0, from succ_ne_zero 0,
absurd H ne)
(take k IH H, IH (succ_inj H))
theorem decidable_eq [instance] (n m : ) : decidable (n = m) :=
have general : ∀n, decidable (n = m), from
rec_on m
(take n,
rec_on n
(inl (refl 0))
(λ m iH, inr (succ_ne_zero m)))
(λ (m' : ) (iH1 : ∀n, decidable (n = m')),
take n, rec_on n
(inr (ne_symm (succ_ne_zero m')))
(λ (n' : ) (iH2 : decidable (n' = succ m')),
have d1 : decidable (n' = m'), from iH1 n',
decidable.rec_on d1
(assume Heq : n' = m', inl (congr_arg succ Heq))
(assume Hne : n' ≠ m',
have H1 : succ n' ≠ succ m', from
assume Heq, absurd (succ_inj Heq) Hne,
inr H1))),
general n
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
induction_on a
(and_intro H1 H2)
(take k IH,
have IH1 : P k, from and_elim_left IH,
have IH2 : P (succ k), from and_elim_right IH,
and_intro IH2 (H3 k IH1 IH2)),
and_elim_left stronger
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 :=
have general : ∀m, P n m, from induction_on n
(take m : , H1 m)
(take k : ,
assume IH : ∀m, P k m,
take m : ,
discriminate
(assume Hm : m = 0,
Hm⁻¹ ▸ (H2 k))
(take l : ,
assume Hm : m = succ l,
Hm⁻¹ ▸ (H3 k l (IH l)))),
general m
-- Addition
-- --------
definition add (x y : ) : := plus x y
infixl `+` := add
theorem add_zero_right (n : ) : n + 0 = n
theorem add_succ_right (n m : ) : n + succ m = succ (n + m)
opaque_hint (hiding add)
theorem add_zero_left (n : ) : 0 + n = n :=
induction_on n
(add_zero_right 0)
(take m IH, show 0 + succ m = succ m, from
calc
0 + succ m = succ (0 + m) : add_succ_right _ _
... = succ m : {IH})
theorem add_succ_left (n m : ) : (succ n) + m = succ (n + m) :=
induction_on m
(calc
succ n + 0 = succ n : add_zero_right (succ n)
... = succ (n + 0) : {symm (add_zero_right n)})
(take k IH,
calc
succ n + succ k = succ (succ n + k) : add_succ_right _ _
... = succ (succ (n + k)) : {IH}
... = succ (n + succ k) : {symm (add_succ_right _ _)})
theorem add_comm (n m : ) : n + m = m + n :=
induction_on m
(trans (add_zero_right _) (symm (add_zero_left _)))
(take k IH,
calc
n + succ k = succ (n+k) : add_succ_right _ _
... = succ (k + n) : {IH}
... = succ k + n : symm (add_succ_left _ _))
theorem add_move_succ (n m : ) : succ n + m = n + succ m :=
calc
succ n + m = succ (n + m) : add_succ_left n m
... = n +succ m : symm (add_succ_right n m)
theorem add_comm_succ (n m : ) : n + succ m = m + succ n :=
calc
n + succ m = succ n + m : symm (add_move_succ n m)
... = m + succ n : add_comm (succ n) m
theorem add_assoc (n m k : ) : (n + m) + k = n + (m + k) :=
induction_on k
(calc
(n + m) + 0 = n + m : add_zero_right _
... = n + (m + 0) : {symm (add_zero_right m)})
(take l IH,
calc
(n + m) + succ l = succ ((n + m) + l) : add_succ_right _ _
... = succ (n + (m + l)) : {IH}
... = n + succ (m + l) : symm (add_succ_right _ _)
... = n + (m + succ l) : {symm (add_succ_right _ _)})
theorem add_left_comm (n m k : ) : n + (m + k) = m + (n + k) :=
left_comm add_comm add_assoc n m k
theorem add_right_comm (n m k : ) : n + m + k = n + k + m :=
right_comm add_comm add_assoc n m k
-- add_rewrite add_zero_left add_zero_right
-- add_rewrite add_succ_left add_succ_right
-- add_rewrite add_comm add_assoc add_left_comm
-- ### cancelation
theorem add_cancel_left {n m k : } : n + m = n + k → m = k :=
induction_on n
(take H : 0 + m = 0 + k,
calc
m = 0 + m : symm (add_zero_left m)
... = 0 + k : H
... = k : add_zero_left k)
(take (n : ) (IH : n + m = n + k → m = k) (H : succ n + m = succ n + k),
have H2 : succ (n + m) = succ (n + k),
from calc
succ (n + m) = succ n + m : symm (add_succ_left n m)
... = succ n + k : H
... = succ (n + k) : add_succ_left n k,
have H3 : n + m = n + k, from succ_inj H2,
IH H3)
theorem add_cancel_right {n m k : } (H : n + m = k + m) : n = k :=
have H2 : m + n = m + k,
from calc
m + n = n + m : add_comm m n
... = k + m : H
... = m + k : add_comm k m,
add_cancel_left H2
theorem add_eq_zero_left {n m : } : n + m = 0 → n = 0 :=
induction_on n
(take (H : 0 + m = 0), refl 0)
(take k IH,
assume (H : succ k + m = 0),
absurd_elim (succ k = 0)
(show succ (k + m) = 0, from
calc
succ (k + m) = succ k + m : symm (add_succ_left k m)
... = 0 : H)
(succ_ne_zero (k + m)))
theorem add_eq_zero_right {n m : } (H : n + m = 0) : m = 0 :=
add_eq_zero_left (trans (add_comm m n) H)
theorem add_eq_zero {n m : } (H : n + m = 0) : n = 0 ∧ m = 0 :=
and_intro (add_eq_zero_left H) (add_eq_zero_right H)
-- ### misc
theorem add_one (n : ) : n + 1 = succ n :=
calc
n + 1 = succ (n + 0) : add_succ_right _ _
... = succ n : {add_zero_right _}
theorem add_one_left (n : ) : 1 + n = succ n :=
calc
1 + n = succ (0 + n) : add_succ_left _ _
... = succ n : {add_zero_left _}
-- TODO: rename? remove?
theorem induction_plus_one {P : nat → Prop} (a : ) (H1 : P 0)
(H2 : ∀ (n : ) (IH : P n), P (n + 1)) : P a :=
nat_rec H1 (take n IH, (add_one n) ▸ (H2 n IH)) a
-- Multiplication
-- --------------
definition mul (n m : ) := nat_rec 0 (fun m x, x + n) m
infixl `*` := mul
theorem mul_zero_right (n:) : n * 0 = 0
theorem mul_succ_right (n m:) : n * succ m = n * m + n
opaque_hint (hiding mul)
-- ### commutativity, distributivity, associativity, identity
theorem mul_zero_left (n:) : 0 * n = 0 :=
induction_on n
(mul_zero_right 0)
(take m IH,
calc
0 * succ m = 0 * m + 0 : mul_succ_right _ _
... = 0 * m : add_zero_right _
... = 0 : IH)
theorem mul_succ_left (n m:) : (succ n) * m = (n * m) + m :=
induction_on m
(calc
succ n * 0 = 0 : mul_zero_right _
... = n * 0 : symm (mul_zero_right _)
... = n * 0 + 0 : symm (add_zero_right _))
(take k IH,
calc
succ n * succ k = (succ n * k) + succ n : mul_succ_right _ _
... = (n * k) + k + succ n : { IH }
... = (n * k) + (k + succ n) : add_assoc _ _ _
... = (n * k) + (n + succ k) : {add_comm_succ _ _}
... = (n * k) + n + succ k : symm (add_assoc _ _ _)
... = (n * succ k) + succ k : {symm (mul_succ_right n k)})
theorem mul_comm (n m:) : n * m = m * n :=
induction_on m
(trans (mul_zero_right _) (symm (mul_zero_left _)))
(take k IH,
calc
n * succ k = n * k + n : mul_succ_right _ _
... = k * n + n : {IH}
... = (succ k) * n : symm (mul_succ_left _ _))
theorem mul_distr_right (n m k : ) : (n + m) * k = n * k + m * k :=
induction_on k
(calc
(n + m) * 0 = 0 : mul_zero_right _
... = 0 + 0 : symm (add_zero_right _)
... = n * 0 + 0 : {symm (mul_zero_right _)}
... = n * 0 + m * 0 : {symm (mul_zero_right _)})
(take l IH, calc
(n + m) * succ l = (n + m) * l + (n + m) : mul_succ_right _ _
... = n * l + m * l + (n + m) : {IH}
... = n * l + m * l + n + m : symm (add_assoc _ _ _)
... = n * l + n + m * l + m : {add_right_comm _ _ _}
... = n * l + n + (m * l + m) : add_assoc _ _ _
... = n * succ l + (m * l + m) : {symm (mul_succ_right _ _)}
... = n * succ l + m * succ l : {symm (mul_succ_right _ _)})
theorem mul_distr_left (n m k : ) : n * (m + k) = n * m + n * k :=
calc
n * (m + k) = (m + k) * n : mul_comm _ _
... = m * n + k * n : mul_distr_right _ _ _
... = n * m + k * n : {mul_comm _ _}
... = n * m + n * k : {mul_comm _ _}
theorem mul_assoc (n m k:) : (n * m) * k = n * (m * k) :=
induction_on k
(calc
(n * m) * 0 = 0 : mul_zero_right _
... = n * 0 : symm (mul_zero_right _)
... = n * (m * 0) : {symm (mul_zero_right _)})
(take l IH,
calc
(n * m) * succ l = (n * m) * l + n * m : mul_succ_right _ _
... = n * (m * l) + n * m : {IH}
... = n * (m * l + m) : symm (mul_distr_left _ _ _)
... = n * (m * succ l) : {symm (mul_succ_right _ _)})
theorem mul_left_comm (n m k : ) : n * (m * k) = m * (n * k) :=
left_comm mul_comm mul_assoc n m k
theorem mul_right_comm (n m k : ) : n * m * k = n * k * m :=
right_comm mul_comm mul_assoc n m k
theorem mul_one_right (n : ) : n * 1 = n :=
calc
n * 1 = n * 0 + n : mul_succ_right n 0
... = 0 + n : {mul_zero_right n}
... = n : add_zero_left n
theorem mul_one_left (n : ) : 1 * n = n :=
calc
1 * n = n * 1 : mul_comm _ _
... = n : mul_one_right n
theorem mul_eq_zero {n m : } (H : n * m = 0) : n = 0 m = 0 :=
discriminate
(take Hn : n = 0, or_intro_left _ Hn)
(take (k : ),
assume (Hk : n = succ k),
discriminate
(take (Hm : m = 0), or_intro_right _ Hm)
(take (l : ),
assume (Hl : m = succ l),
have Heq : succ (k * succ l + l) = n * m, from
symm (calc
n * m = n * succ l : {Hl}
... = succ k * succ l : {Hk}
... = k * succ l + succ l : mul_succ_left _ _
... = succ (k * succ l + l) : add_succ_right _ _),
absurd_elim _ (trans Heq H) (succ_ne_zero _)))
---other inversion theorems appear below
-- add_rewrite mul_zero_left mul_zero_right mul_one_right mul_one_left
-- add_rewrite mul_succ_left mul_succ_right
-- add_rewrite mul_comm mul_assoc mul_left_comm
-- add_rewrite mul_distr_right mul_distr_left
end nat