doc(examples/lean): add theorem sent by Jeremy Avigad
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura
parent
1796c2b992
commit
fddaa7bc3a
1 changed files with 550 additions and 0 deletions
550
examples/lean/primes.lean
Normal file
550
examples/lean/primes.lean
Normal file
|
|
@ -0,0 +1,550 @@
|
|||
----------------------------------------------------------------------------------------------------
|
||||
--
|
||||
-- theory primes.lean
|
||||
-- author: Jeremy Avigad
|
||||
--
|
||||
-- Experimenting with Lean.
|
||||
--
|
||||
----------------------------------------------------------------------------------------------------
|
||||
|
||||
import macros
|
||||
import tactic
|
||||
using Nat
|
||||
|
||||
--
|
||||
-- could go in kernel
|
||||
--
|
||||
|
||||
theorem or_imp (p q : Bool) : (p ∨ q) ↔ (¬ p → q)
|
||||
:= subst (symm (imp_or (¬ p) q)) (not_not_eq p)
|
||||
|
||||
--
|
||||
-- fundamental properties of Nat
|
||||
--
|
||||
|
||||
theorem cases_on {P : Nat → Bool} (a : Nat) (H1 : P 0) (H2 : ∀ (n : Nat), P (n + 1)) : P a
|
||||
:= induction_on a H1 (take n : Nat, assume ih : P n, H2 n)
|
||||
|
||||
theorem strong_induction_on {P : Nat → Bool} (a : Nat) (H : ∀ n, (∀ m, m < n → P m) → P n) : P a
|
||||
:= @strong_induction P H a
|
||||
|
||||
-- in hindsight, now I know I don't need these
|
||||
theorem one_ne_zero : 1 ≠ 0 := succ_nz 0
|
||||
theorem two_ne_zero : 2 ≠ 0 := succ_nz 1
|
||||
|
||||
--
|
||||
-- observation: the proof of lt_le_trans in Nat is not needed
|
||||
--
|
||||
|
||||
theorem lt_le_trans2 {a b c : Nat} (H1 : a < b) (H2 : b ≤ c) : a < c
|
||||
:= le_trans H1 H2
|
||||
|
||||
--
|
||||
-- also, contrapos and mt are the same theorem
|
||||
--
|
||||
|
||||
theorem contrapos2 {a b : Bool} (H : a → b) : ¬ b → ¬ a
|
||||
:= mt H
|
||||
|
||||
--
|
||||
-- properties of lt and le
|
||||
--
|
||||
|
||||
theorem succ_le_succ {a b : Nat} (H : a + 1 ≤ b + 1) : a ≤ b
|
||||
:=
|
||||
obtain (x : Nat) (Hx : a + 1 + x = b + 1), from lt_elim H,
|
||||
have H2 : a + x + 1 = b + 1, from (calc
|
||||
a + x + 1 = a + (x + 1) : add_assoc _ _ _
|
||||
... = a + (1 + x) : { add_comm x 1 }
|
||||
... = a + 1 + x : symm (add_assoc _ _ _)
|
||||
... = b + 1 : Hx),
|
||||
have H3 : a + x = b, from (succ_inj H2),
|
||||
show a ≤ b, from (le_intro H3)
|
||||
|
||||
-- should we keep this duplication or < and <=?
|
||||
theorem lt_succ {a b : Nat} (H : a < b + 1) : a ≤ b
|
||||
:= succ_le_succ H
|
||||
|
||||
theorem succ_le_succ_eq (a b : Nat) : a + 1 ≤ b + 1 ↔ a ≤ b
|
||||
:= iff_intro succ_le_succ (assume H : a ≤ b, le_add H 1)
|
||||
|
||||
theorem lt_succ_eq (a b : Nat) : a < b + 1 ↔ a ≤ b
|
||||
:= succ_le_succ_eq a b
|
||||
|
||||
theorem le_or_lt (a : Nat) : ∀ b : Nat, a ≤ b ∨ b < a
|
||||
:=
|
||||
induction_on a (
|
||||
show ∀b, 0 ≤ b ∨ b < 0,
|
||||
from take b, or_introl (le_zero b) _
|
||||
) (
|
||||
take a,
|
||||
assume ih : ∀b, a ≤ b ∨ b < a,
|
||||
show ∀b, a + 1 ≤ b ∨ b < a + 1,
|
||||
from
|
||||
take b,
|
||||
cases_on b (
|
||||
show a + 1 ≤ 0 ∨ 0 < a + 1,
|
||||
from or_intror _ (le_add (le_zero a) 1)
|
||||
) (
|
||||
take b,
|
||||
have H : a ≤ b ∨ b < a, from ih b,
|
||||
show a + 1 ≤ b + 1 ∨ b + 1 < a + 1,
|
||||
from or_elim H (
|
||||
assume H1 : a ≤ b,
|
||||
or_introl (le_add H1 1) (b + 1 < a + 1)
|
||||
) (
|
||||
assume H2 : b < a,
|
||||
or_intror (a + 1 ≤ b + 1) (le_add H2 1)
|
||||
)
|
||||
)
|
||||
)
|
||||
|
||||
theorem not_le_lt {a b : Nat} : ¬ a ≤ b → b < a
|
||||
:= (or_imp _ _) ◂ le_or_lt a b
|
||||
|
||||
theorem not_lt_le {a b : Nat} : ¬ a < b → b ≤ a
|
||||
:= (or_imp _ _) ◂ (or_comm _ _ ◂ le_or_lt b a)
|
||||
|
||||
theorem lt_not_le {a b : Nat} (H : a < b) : ¬ b ≤ a
|
||||
:= not_intro (take H1 : b ≤ a, absurd (lt_le_trans H H1) (lt_nrefl a))
|
||||
|
||||
theorem le_not_lt {a b : Nat} (H : a ≤ b) : ¬ b < a
|
||||
:= not_intro (take H1 : b < a, absurd H (lt_not_le H1))
|
||||
|
||||
theorem not_le_iff {a b : Nat} : ¬ a ≤ b ↔ b < a
|
||||
:= iff_intro (@not_le_lt a b) (@lt_not_le b a)
|
||||
|
||||
theorem not_lt_iff {a b : Nat} : ¬ a < b ↔ b ≤ a
|
||||
:= iff_intro (@not_lt_le a b) (@le_not_lt b a)
|
||||
|
||||
theorem le_iff {a b : Nat} : a ≤ b ↔ a < b ∨ a = b
|
||||
:=
|
||||
iff_intro (
|
||||
assume H : a ≤ b,
|
||||
show a < b ∨ a = b,
|
||||
from or_elim (em (a = b)) (
|
||||
take H1 : a = b,
|
||||
show a < b ∨ a = b, from or_intror _ H1
|
||||
) (
|
||||
take H2 : a ≠ b,
|
||||
have H3 : ¬ b ≤ a,
|
||||
from not_intro (take H4: b ≤ a, absurd (le_antisym H H4) H2),
|
||||
have H4 : a < b, from resolve1 (le_or_lt b a) H3,
|
||||
show a < b ∨ a = b, from or_introl H4 _
|
||||
)
|
||||
)(
|
||||
assume H : a < b ∨ a = b,
|
||||
show a ≤ b,
|
||||
from or_elim H (
|
||||
take H1 : a < b, lt_le H1
|
||||
) (
|
||||
take H1 : a = b, subst (le_refl a) H1
|
||||
)
|
||||
)
|
||||
|
||||
theorem ne_symm_iff {A : (Type U)} (a b : A) : a ≠ b ↔ b ≠ a
|
||||
:= iff_intro ne_symm ne_symm
|
||||
|
||||
theorem lt_iff (a b : Nat) : a < b ↔ a ≤ b ∧ a ≠ b
|
||||
:=
|
||||
calc
|
||||
a < b = ¬ b ≤ a : symm (not_le_iff)
|
||||
... = ¬ (b < a ∨ b = a) : { le_iff }
|
||||
... = ¬ b < a ∧ b ≠ a : not_or _ _
|
||||
... = a ≤ b ∧ b ≠ a : { not_lt_iff }
|
||||
... = a ≤ b ∧ a ≠ b : { ne_symm_iff _ _ }
|
||||
|
||||
theorem ne_zero_ge_one {x : Nat} (H : x ≠ 0) : x ≥ 1
|
||||
:= resolve2 (le_iff ◂ (le_zero x)) (ne_symm H)
|
||||
|
||||
theorem ne_zero_one_ge_two {x : Nat} (H0 : x ≠ 0) (H1 : x ≠ 1) : x ≥ 2
|
||||
:= resolve2 (le_iff ◂ (ne_zero_ge_one H0)) (ne_symm H1)
|
||||
|
||||
-- the forward direction can be replaced by ne_zero_ge_one, but
|
||||
-- note the comments below
|
||||
theorem ne_zero_iff (n : Nat) : n ≠ 0 ↔ n > 0
|
||||
:=
|
||||
iff_intro (
|
||||
assume H : n ≠ 0,
|
||||
refute (
|
||||
assume H1 : ¬ n > 0,
|
||||
-- curious: if you make the arguments implicit in the next line,
|
||||
-- it fails (the evaluator is getting in the way, I think)
|
||||
have H2 : n = 0, from le_antisym (@not_lt_le 0 n H1) (le_zero n),
|
||||
absurd H2 H
|
||||
)
|
||||
) (
|
||||
-- here too
|
||||
assume H : n > 0, ne_symm (@lt_ne 0 n H)
|
||||
)
|
||||
|
||||
-- Note: this differs from Leo's naming conventions
|
||||
theorem mul_right_mono {x y : Nat} (H : x ≤ y) (z : Nat) : x * z ≤ y * z
|
||||
:=
|
||||
obtain (w : Nat) (Hw : x + w = y),
|
||||
from le_elim H,
|
||||
le_intro (
|
||||
show x * z + w * z = y * z,
|
||||
from calc
|
||||
x * z + w * z = (x + w) * z : symm (distributel x w z)
|
||||
... = y * z : { Hw }
|
||||
)
|
||||
|
||||
theorem mul_left_mono (x : Nat) {y z : Nat} (H : y ≤ z) : x * y ≤ x * z
|
||||
:= subst (subst (mul_right_mono H x) (mul_comm y x)) (mul_comm z x)
|
||||
|
||||
theorem le_addr (a b : Nat) : a ≤ a + b
|
||||
:= le_intro (refl (a + b))
|
||||
|
||||
theorem le_addl (a b : Nat) : a ≤ b + a
|
||||
:= subst (le_addr a b) (add_comm a b)
|
||||
|
||||
theorem add_left_mono {a b : Nat} (c : Nat) (H : a ≤ b) : c + a ≤ c + b
|
||||
:= subst (subst (le_add H c) (add_comm a c)) (add_comm b c)
|
||||
|
||||
theorem mul_right_strict_mono {x y z : Nat} (H : x < y) (znez : z ≠ 0) : x * z < y * z
|
||||
:=
|
||||
obtain (w : Nat) (Hw : x + 1 + w = y),
|
||||
from le_elim H,
|
||||
have H1 : y * z = x * z + w * z + z,
|
||||
from calc
|
||||
y * z = (x + 1 + w) * z : { symm Hw }
|
||||
... = (x + (1 + w)) * z : { add_assoc _ _ _ }
|
||||
... = (x + (w + 1)) * z : { add_comm _ _ }
|
||||
... = (x + w + 1) * z : { symm (add_assoc _ _ _) }
|
||||
... = (x + w) * z + 1 * z : distributel _ _ _
|
||||
... = (x + w) * z + z : { mul_onel _ }
|
||||
... = x * z + w * z + z : { distributel _ _ _ },
|
||||
have H2 : x * z ≤ x * z + w * z, from le_addr _ _,
|
||||
have H3 : x * z + w * z < x * z + w * z + z, from add_left_mono _ (ne_zero_ge_one znez),
|
||||
show x * z < y * z, from subst (le_lt_trans H2 H3) (symm H1)
|
||||
|
||||
theorem mul_left_strict_mono {x y z : Nat} (H : x < y) (znez : z ≠ 0) : z * x < z * y
|
||||
:= subst (subst (mul_right_strict_mono H znez) (mul_comm x z)) (mul_comm y z)
|
||||
|
||||
theorem mul_left_le_cancel {a b c : Nat} (H : a * b ≤ a * c) (anez : a ≠ 0) : b ≤ c
|
||||
:=
|
||||
refute (
|
||||
assume H1 : ¬ b ≤ c,
|
||||
have H2 : a * c < a * b, from mul_left_strict_mono (not_le_lt H1) anez,
|
||||
show false, from absurd H (lt_not_le H2)
|
||||
)
|
||||
|
||||
theorem mul_right_le_cancel {a b c : Nat} (H : b * a ≤ c * a) (anez : a ≠ 0) : b ≤ c
|
||||
:= mul_left_le_cancel (subst (subst H (mul_comm b a)) (mul_comm c a)) anez
|
||||
|
||||
theorem mul_left_lt_cancel {a b c : Nat} (H : a * b < a * c) : b < c
|
||||
:=
|
||||
refute (
|
||||
assume H1 : ¬ b < c,
|
||||
have H2 : a * c ≤ a * b, from mul_left_mono a (not_lt_le H1),
|
||||
show false, from absurd H (le_not_lt H2)
|
||||
)
|
||||
|
||||
theorem mul_right_lt_cancel {a b c : Nat} (H : b * a < c * a) : b < c
|
||||
:= mul_left_lt_cancel (subst (subst H (mul_comm b a)) (mul_comm c a))
|
||||
|
||||
theorem add_right_comm (a b c : Nat) : a + b + c = a + c + b
|
||||
:=
|
||||
calc
|
||||
a + b + c = a + (b + c) : add_assoc _ _ _
|
||||
... = a + (c + b) : { add_comm b c }
|
||||
... = a + c + b : symm (add_assoc _ _ _)
|
||||
|
||||
theorem add_left_le_cancel {a b c : Nat} (H : a + c ≤ b + c) : a ≤ b
|
||||
:=
|
||||
obtain (d : Nat) (Hd : a + c + d = b + c), from le_elim H,
|
||||
le_intro (add_injl (subst Hd (add_right_comm a c d)))
|
||||
|
||||
theorem add_right_le_cancel {a b c : Nat} (H : c + a ≤ c + b) : a ≤ b
|
||||
:= add_left_le_cancel (subst (subst H (add_comm c a)) (add_comm c b))
|
||||
|
||||
--
|
||||
-- more properties of multiplication
|
||||
--
|
||||
|
||||
theorem mul_left_cancel {a b c : Nat} (H : a * b = a * c) (anez : a ≠ 0) : b = c
|
||||
:=
|
||||
have H1 : a * b ≤ a * c, from subst (le_refl _) H,
|
||||
have H2 : a * c ≤ a * b, from subst (le_refl _) H,
|
||||
le_antisym (mul_left_le_cancel H1 anez) (mul_left_le_cancel H2 anez)
|
||||
|
||||
theorem mul_right_cancel {a b c : Nat} (H : b * a = c * a) (anez : a ≠ 0) : b = c
|
||||
:= mul_left_cancel (subst (subst H (mul_comm b a)) (mul_comm c a)) anez
|
||||
|
||||
|
||||
--
|
||||
-- divisibility
|
||||
--
|
||||
|
||||
definition dvd (a b : Nat) : Bool := ∃ c, a * c = b
|
||||
|
||||
infix 50 | : dvd
|
||||
|
||||
theorem dvd_intro {a b c : Nat} (H : a * c = b) : a | b
|
||||
:= exists_intro c H
|
||||
|
||||
theorem dvd_elim {a b : Nat} (H : a | b) : ∃ c, a * c = b
|
||||
:= H
|
||||
|
||||
theorem dvd_self (n : Nat) : n | n := dvd_intro (mul_oner n)
|
||||
|
||||
theorem one_dvd (a : Nat) : 1 | a
|
||||
:= dvd_intro (mul_onel a)
|
||||
|
||||
theorem zero_dvd {a : Nat} (H: 0 | a) : a = 0
|
||||
:=
|
||||
obtain (w : Nat) (H1 : 0 * w = a), from H,
|
||||
subst (symm H1) (mul_zerol _)
|
||||
|
||||
theorem dvd_zero (a : Nat) : a | 0
|
||||
:= exists_intro 0 (mul_zeror _)
|
||||
|
||||
theorem dvd_trans {a b c} (H1 : a | b) (H2 : b | c) : a | c
|
||||
:=
|
||||
obtain (w1 : Nat) (Hw1 : a * w1 = b), from H1,
|
||||
obtain (w2 : Nat) (Hw2 : b * w2 = c), from H2,
|
||||
exists_intro (w1 * w2)
|
||||
calc a * (w1 * w2) = a * w1 * w2 : symm (mul_assoc a w1 w2)
|
||||
... = b * w2 : { Hw1 }
|
||||
... = c : Hw2
|
||||
|
||||
theorem dvd_le {x y : Nat} (H : x | y) (ynez : y ≠ 0) : x ≤ y
|
||||
:=
|
||||
obtain (w : Nat) (Hw : x * w = y), from H,
|
||||
have wnez : w ≠ 0, from
|
||||
not_intro (take H1 : w = 0, absurd (
|
||||
calc y = x * w : symm Hw
|
||||
... = x * 0 : { H1 }
|
||||
... = 0 : mul_zeror x
|
||||
) ynez),
|
||||
have H2 : x * 1 ≤ x * w, from mul_left_mono x (ne_zero_ge_one wnez),
|
||||
show x ≤ y, from subst (subst H2 (mul_oner x)) Hw
|
||||
|
||||
theorem dvd_mul_right {a b : Nat} (H : a | b) (c : Nat) : a | b * c
|
||||
:=
|
||||
obtain (d : Nat) (Hd : a * d = b), from dvd_elim H,
|
||||
dvd_intro (
|
||||
calc
|
||||
a * (d * c) = (a * d) * c : symm (mul_assoc _ _ _)
|
||||
... = b * c : { Hd }
|
||||
)
|
||||
|
||||
theorem dvd_mul_left {a b : Nat} (H : a | b) (c : Nat) : a | c * b
|
||||
:= subst (dvd_mul_right H c) (mul_comm b c)
|
||||
|
||||
theorem dvd_add {a b c : Nat} (H1 : a | b) (H2 : a | c) : a | b + c
|
||||
:=
|
||||
obtain (w1 : Nat) (Hw1 : a * w1 = b), from H1,
|
||||
obtain (w2 : Nat) (Hw2 : a * w2 = c), from H2,
|
||||
exists_intro (w1 + w2)
|
||||
calc a * (w1 + w2) = a * w1 + a * w2 : distributer _ _ _
|
||||
... = b + a * w2 : { Hw1 }
|
||||
... = b + c : { Hw2 }
|
||||
|
||||
theorem dvd_add_cancel {a b c : Nat} (H1 : a | b + c) (H2 : a | b) : a | c
|
||||
:=
|
||||
or_elim (em (a = 0)) (
|
||||
assume az : a = 0,
|
||||
have H3 : c = 0, from
|
||||
calc c = 0 + c : symm (add_zerol _)
|
||||
... = b + c : { symm (zero_dvd (subst H2 az)) }
|
||||
... = 0 : zero_dvd (subst H1 az),
|
||||
show a | c, from subst (dvd_zero a) (symm H3)
|
||||
) (
|
||||
assume anz : a ≠ 0,
|
||||
obtain (w1 : Nat) (Hw1 : a * w1 = b + c), from H1,
|
||||
obtain (w2 : Nat) (Hw2 : a * w2 = b), from H2,
|
||||
have H3 : a * w1 = a * w2 + c, from subst Hw1 (symm Hw2),
|
||||
have H4 : a * w2 ≤ a * w1, from le_intro (symm H3),
|
||||
have H5 : w2 ≤ w1, from mul_left_le_cancel H4 anz,
|
||||
obtain (w3 : Nat) (Hw3 : w2 + w3 = w1), from le_elim H5,
|
||||
have H6 : b + a * w3 = b + c, from
|
||||
calc
|
||||
b + a * w3 = a * w2 + a * w3 : { symm Hw2 }
|
||||
... = a * (w2 + w3) : symm (distributer _ _ _)
|
||||
... = a * w1 : { Hw3 }
|
||||
... = b + c : Hw1,
|
||||
have H7 : a * w3 = c, from add_injr H6,
|
||||
show a | c, from dvd_intro H7
|
||||
)
|
||||
|
||||
--
|
||||
-- primes
|
||||
--
|
||||
|
||||
definition prime p := p ≥ 2 ∧ forall m, m | p → m = 1 ∨ m = p
|
||||
|
||||
theorem not_prime_has_divisor {n : Nat} (H1 : n ≥ 2) (H2 : ¬ prime n) : ∃ m, m | n ∧ m ≠ 1 ∧ m ≠ n
|
||||
:=
|
||||
have H3 : ¬ n ≥ 2 ∨ ¬ (∀ m : Nat, m | n → m = 1 ∨ m = n),
|
||||
from not_and _ _ ◂ H2,
|
||||
have H4 : ¬ ¬ n ≥ 2,
|
||||
from (symm (not_not_eq _)) ◂ H1,
|
||||
obtain (m : Nat) (H5 : ¬ (m | n → m = 1 ∨ m = n)),
|
||||
from not_forall_elim (resolve1 H3 H4),
|
||||
have H6 : m | n ∧ ¬ (m = 1 ∨ m = n),
|
||||
from (not_implies _ _) ◂ H5,
|
||||
have H7 : ¬ (m = 1 ∨ m = n) ↔ (m ≠ 1 ∧ m ≠ n),
|
||||
from not_or (m = 1) (m = n),
|
||||
have H8 : m | n ∧ m ≠ 1 ∧ m ≠ n,
|
||||
from subst H6 H7,
|
||||
show ∃ m, m | n ∧ m ≠ 1 ∧ m ≠ n,
|
||||
from exists_intro m H8
|
||||
|
||||
theorem not_prime_has_divisor2 {n : Nat} (H1 : n ≥ 2) (H2 : ¬ prime n) :
|
||||
∃ m, m | n ∧ m ≥ 2 ∧ m < n
|
||||
:=
|
||||
have n_ne_0 : n ≠ 0, from
|
||||
not_intro (take n0 : n = 0, substp (fun n, n ≥ 2) H1 n0),
|
||||
obtain (m : Nat) (Hm : m | n ∧ m ≠ 1 ∧ m ≠ n),
|
||||
from not_prime_has_divisor H1 H2,
|
||||
let m_dvd_n := and_eliml Hm in
|
||||
let m_ne_1 := and_eliml (and_elimr Hm) in
|
||||
let m_ne_n := and_elimr (and_elimr Hm) in
|
||||
have m_ne_0 : m ≠ 0, from
|
||||
not_intro (
|
||||
take m0 : m = 0,
|
||||
have n0 : n = 0, from zero_dvd (subst m_dvd_n m0),
|
||||
absurd n0 n_ne_0
|
||||
),
|
||||
exists_intro m (
|
||||
and_intro m_dvd_n (
|
||||
and_intro (
|
||||
show m ≥ 2, from ne_zero_one_ge_two m_ne_0 m_ne_1
|
||||
) (
|
||||
have m_le_n : m ≤ n, from dvd_le m_dvd_n n_ne_0,
|
||||
show m < n, from resolve2 (le_iff ◂ m_le_n) m_ne_n
|
||||
)
|
||||
)
|
||||
)
|
||||
|
||||
theorem has_prime_divisor {n : Nat} : n ≥ 2 → ∃ p, prime p ∧ p | n
|
||||
:=
|
||||
strong_induction_on n (
|
||||
take n,
|
||||
assume ih : ∀ m, m < n → m ≥ 2 → ∃ p, prime p ∧ p | m,
|
||||
assume n_ge_2 : n ≥ 2,
|
||||
show ∃ p, prime p ∧ p | n, from
|
||||
or_elim (em (prime n)) (
|
||||
assume H : prime n,
|
||||
exists_intro n (and_intro H (dvd_self n))
|
||||
) (
|
||||
assume H : ¬ prime n,
|
||||
obtain (m : Nat) (Hm : m | n ∧ m ≥ 2 ∧ m < n),
|
||||
from not_prime_has_divisor2 n_ge_2 H,
|
||||
obtain (p : Nat) (Hp : prime p ∧ p | m),
|
||||
from ih m (and_elimr (and_elimr Hm)) (and_eliml (and_elimr Hm)),
|
||||
have p_dvd_n : p | n, from dvd_trans (and_elimr Hp) (and_eliml Hm),
|
||||
exists_intro p (and_intro (and_eliml Hp) p_dvd_n)
|
||||
)
|
||||
)
|
||||
|
||||
--
|
||||
-- factorial
|
||||
--
|
||||
|
||||
variable fact : Nat → Nat
|
||||
|
||||
axiom fact_0 : fact 0 = 1
|
||||
|
||||
axiom fact_succ : ∀ n, fact (n + 1) = (n + 1) * fact n
|
||||
|
||||
-- can the simplifier do this?
|
||||
theorem fact_1 : fact 1 = 1
|
||||
:=
|
||||
calc
|
||||
fact 1 = fact (0 + 1) : { symm (add_zerol 1) }
|
||||
... = (0 + 1) * fact 0 : fact_succ _
|
||||
... = 1 * fact 0 : { add_zerol 1 }
|
||||
... = 1 * 1 : { fact_0 }
|
||||
... = 1 : mul_oner _
|
||||
|
||||
theorem fact_ne_0 (n : Nat) : fact n ≠ 0
|
||||
:=
|
||||
induction_on n (
|
||||
not_intro (
|
||||
assume H : fact 0 = 0,
|
||||
have H1 : 1 = 0, from (subst H fact_0),
|
||||
absurd H1 one_ne_zero
|
||||
)
|
||||
) (
|
||||
take n,
|
||||
assume ih : fact n ≠ 0,
|
||||
not_intro (
|
||||
assume H : fact (n + 1) = 0,
|
||||
have H1 : n + 1 = 0, from
|
||||
mul_right_cancel (
|
||||
calc
|
||||
(n + 1) * fact n = fact (n + 1) : symm (fact_succ n)
|
||||
... = 0 : H
|
||||
... = 0 * fact n : symm (mul_zerol _)
|
||||
) ih,
|
||||
absurd H1 (succ_nz _)
|
||||
)
|
||||
)
|
||||
|
||||
theorem dvd_fact {m n : Nat} (m_gt_0 : m > 0) (m_le_n : m ≤ n) : m | fact n
|
||||
:=
|
||||
obtain (m' : Nat) (Hm' : 1 + m' = m), from le_elim m_gt_0,
|
||||
obtain (n' : Nat) (Hn' : 1 + n' = n), from le_elim (le_trans m_gt_0 m_le_n),
|
||||
have m'_le_n' : m' ≤ n',
|
||||
from add_right_le_cancel (subst (subst m_le_n (symm Hm')) (symm Hn')),
|
||||
have H : ∀ n' m', m' ≤ n' → m' + 1 | fact (n' + 1), from
|
||||
induction (
|
||||
take m' ,
|
||||
assume m'_le_0 : m' ≤ 0,
|
||||
have Hm' : m' + 1 = 1,
|
||||
from calc
|
||||
m' + 1 = 0 + 1 : { le_antisym m'_le_0 (le_zero m') }
|
||||
... = 1 : add_zerol _,
|
||||
show m' + 1 | fact (0 + 1), from subst (one_dvd _) (symm Hm')
|
||||
) (
|
||||
take n',
|
||||
assume ih : ∀m', m' ≤ n' → m' + 1 | fact (n' + 1),
|
||||
take m',
|
||||
assume Hm' : m' ≤ n' + 1,
|
||||
have H1 : m' < n' + 1 ∨ m' = n' + 1, from le_iff ◂ Hm',
|
||||
or_elim H1 (
|
||||
assume H2 : m' < n' + 1,
|
||||
have H3 : m' ≤ n', from lt_succ H2,
|
||||
have H4 : m' + 1 | fact (n' + 1), from ih _ H3,
|
||||
have H5 : m' + 1 | (n' + 1 + 1) * fact (n' + 1), from dvd_mul_left H4 _,
|
||||
show m' + 1 | fact (n' + 1 + 1), from subst H5 (symm (fact_succ _))
|
||||
) (
|
||||
assume H2 : m' = n' + 1,
|
||||
have H3 : m' + 1 | n' + 1 + 1, from subst (dvd_self _) H2,
|
||||
have H4 : m' + 1 | (n' + 1 + 1) * fact (n' + 1), from dvd_mul_right H3 _,
|
||||
show m' + 1 | fact (n' + 1 + 1), from subst H4 (symm (fact_succ _))
|
||||
)
|
||||
),
|
||||
have H1 : m' + 1 | fact (n' + 1), from H _ _ m'_le_n',
|
||||
show m | fact n,
|
||||
from (subst (subst (subst (subst H1 (add_comm m' 1)) Hm') (add_comm n' 1)) Hn')
|
||||
|
||||
theorem primes_infinite (n : Nat) : ∃ p, p ≥ n ∧ prime p
|
||||
:=
|
||||
let m := fact (n + 1) in
|
||||
have Hn1 : n + 1 ≥ 1, from le_addl _ _,
|
||||
have m_ge_1 : m ≥ 1, from ne_zero_ge_one (fact_ne_0 _),
|
||||
have m1_ge_2 : m + 1 ≥ 2, from le_add m_ge_1 1,
|
||||
obtain (p : Nat) (Hp : prime p ∧ p | m + 1), from has_prime_divisor m1_ge_2,
|
||||
let prime_p := and_eliml Hp in
|
||||
let p_dvd_m1 := and_elimr Hp in
|
||||
have p_ge_2 : p ≥ 2, from and_eliml prime_p,
|
||||
have two_gt_0 : 2 > 0, from (ne_zero_iff 2) ◂ (succ_nz 1),
|
||||
-- fails if arguments are left implicit
|
||||
have p_gt_0 : p > 0, from @lt_le_trans 0 2 p two_gt_0 p_ge_2,
|
||||
have p_ge_n : p ≥ n, from
|
||||
refute (
|
||||
assume H1 : ¬ p ≥ n,
|
||||
have H2 : p < n, from not_le_lt H1,
|
||||
have H3 : p ≤ n + 1, from lt_le (lt_le_trans H2 (le_addr n 1)),
|
||||
have H4 : p | m, from dvd_fact p_gt_0 H3,
|
||||
have H5 : p | 1, from dvd_add_cancel p_dvd_m1 H4,
|
||||
have H6 : p ≤ 1, from dvd_le H5 (succ_nz 0),
|
||||
have H7 : 2 ≤ 1, from le_trans p_ge_2 H6,
|
||||
absurd H7 (lt_nrefl 1)
|
||||
),
|
||||
exists_intro p (and_intro p_ge_n prime_p)
|
||||
|
||||
Loading…
Reference in a new issue