自然数游戏答案合集

自然数游戏（Natual Number Game）地址：https://game.leanprover.cn/

---

代码高亮使用 PrismJs PR #3765 方案

教程世界

rfl 策略

rfl

rw 策略

rw [h] 
rfl

数字

rw[two_eq_succ_one]
rw[one_eq_succ_zero]
rfl

逆向重写

rw[← one_eq_succ_zero]
rw[← two_eq_succ_one]
rfl

加零

-- rw[add_zero b]
-- rw[add_zero c]
repeat rw [add_zero]
rfl

精准重写

rw [add_zero b]
rw [add_zero c]
rfl

add_succ

rw [one_eq_succ_zero]
rw [add_succ n 0]
rw [add_zero]
rfl

2+2=4

nth_rewrite 2 [two_eq_succ_one]
rw [add_succ 2 1]
rw [← succ_eq_add_one]
rw [← three_eq_succ_two]
rw [four_eq_succ_three]
rfl

加法世界

zero_add

induction n with d hd

-- 0 + 0 = 0
rw [add_zero]
rfl

-- 0 + succ d = succ d
rw [add_succ]
rw [hd]
rfl

succ_add

induction b with d hd
-- succ a + 0 = succ (a + 0)
repeat rw [add_zero]
rfl
-- hd: succ a + d = succ (a + d); succ a + succ d = succ (a + succ d)
rw [add_succ]
rw [add_succ a d]
rw [hd]
rfl

add_comm（关卡Boss）

induction a with d hd
-- 0 + b = b + 0
rw [add_zero]
rw [zero_add]
rfl
-- hd: d+b=b+d; succ d + b = b + succ d
rw [add_succ b d]
rw [succ_add d b]
rw [hd]
rfl

add_assoc（加法结合律）

induction b with d hd
rw [zero_add]
rw [add_zero]
rfl
rw [add_succ]
repeat rw [succ_add]
rw [add_succ]
rw [hd]
rfl

add_right_comm

repeat rw [add_assoc]
rw [add_comm b c]
rfl

乘法世界

mul_one

rw [one_eq_succ_zero]
rw [mul_succ]
rw [mul_zero]
rw [zero_add]
rfl

zero_mul

induction m with d hd
apply mul_zero
rw [mul_succ, hd, zero_add]
rfl

succ_mul

induction b with c hc
repeat rw [mul_zero]
rw [zero_add]
rfl
repeat rw [mul_succ]
rw [hc]
repeat rw [add_succ]
rw [add_right_comm]
rfl

mul_comm

induction a with c hc
rw [zero_mul, mul_zero]
rfl
rw [succ_mul, mul_succ, hc]
rfl

one_mul

rw [one_eq_succ_zero, succ_mul, zero_mul, zero_add]
rfl

two_mul

rw [two_eq_succ_one, one_eq_succ_zero]
repeat rw [succ_mul]
rw [zero_mul, zero_add]
rfl

mul_add

induction b with d hd
rw [zero_add, mul_zero, zero_add]
rfl
rw [succ_add]
repeat rw [mul_succ]
rw [add_right_comm, hd]
rfl

add_mul

rw [mul_comm, mul_add, mul_comm, mul_comm c b]
rfl

mul_assoc

induction a with d hd
repeat rw [zero_mul]
rfl
repeat rw [succ_mul]
rw [add_mul, hd]
rfl

蕴含世界

exact 策略

exact h1

exact 练习

repeat rw [zero_add] at h
exact h

apply 策略

apply h2 at h1
exact h1

succ_inj ：后继数是单射的

rw [four_eq_succ_three] at h
rw [← succ_eq_add_one] at h
apply succ_inj at h
exact h

从后向前证明

apply succ_inj
rw [succ_eq_add_one]
rw [← four_eq_succ_three]
exact h

intro

intro h
exact h

练习 intro 策略

intro h
repeat rw [← succ_eq_add_one] at h
apply succ_inj at h
exact h

≠

apply h2
exact h1

zero_ne_succ

intro h
rw [one_eq_succ_zero] at h
apply zero_ne_succ at h
exact h

1 ≠ 0

symm
apply zero_ne_one

2 + 2 ≠ 5

repeat rw [succ_eq_add_one]
repeat rw [zero_add]
rw [← add_assoc]
repeat rw [← succ_eq_add_one]
repeat rw [one_eq_succ_zero]
intro h
repeat apply succ_inj at h
apply zero_ne_succ at h
exact h

幂世界

zero_pow_zero

rw [pow_zero]
rfl

zero_pow_succ

rw [pow_succ, mul_zero]
rfl

pow_one

rw [one_eq_succ_zero, pow_succ, pow_zero, one_mul]
rfl

one_pow

induction m with a ha
rw [pow_zero]
rfl
rw [pow_succ, mul_one, ha]
rfl

pow_two

rw [two_eq_succ_one, pow_succ, pow_one]
rfl

pow_add

induction n with b hb
rw [add_zero, pow_zero, mul_one]
rfl
rw [add_succ, pow_succ, hb, pow_succ,← mul_assoc]
rfl

mul_pow

induction n with c hc
repeat rw [pow_zero]
rw [one_mul]
rfl
repeat rw [pow_succ]
repeat rw [← mul_assoc]
nth_rewrite 5 [mul_comm]
rw [← mul_assoc]
nth_rewrite 6 [mul_comm]
rw [hc]
rfl

pow_pow

induction n with b hb
rw [mul_zero]
repeat rw [pow_zero]
rfl
rw [mul_succ, pow_add, pow_succ, hb]
rfl

add_sq

nth_rewrite 1 [two_eq_succ_one, pow_succ, pow_one, add_mul]
repeat rw [mul_add, ← pow_two]
nth_rewrite 2 [mul_comm]
rw [← add_assoc]
nth_rewrite 5 [two_eq_succ_one]
rw [succ_eq_add_one]
repeat rw [add_mul]
repeat rw [one_mul]
rw [add_right_comm]
nth_rewrite 2 [add_right_comm]
rw [add_assoc]
rfl

费马大定理

-- 这里空间太小，我写不下 /doge

高级加法世界

add_right_cancel

induction n with d hd
repeat rw [add_zero]
intro h
exact h
repeat rw [add_succ]
intro h
apply hd
apply succ_inj
exact h

add_left_cancel

rw [add_comm n a]
rw [add_comm n b]
intro h
apply add_right_cancel a b n
exact h

add_left_eq_self

nth_rewrite 2 [← zero_add y] 
exact add_right_cancel x 0 y

add_right_eq_self

rw [add_comm]
exact add_left_eq_self y x

add_right_eq_zero

cases b with d
rw [add_zero]
intro h
exact h
rw [add_succ]
intro h
symm at h
apply zero_ne_succ at h
cases h

add_left_eq_zero

rw [add_comm]
exact add_right_eq_zero b a

算法世界

add_left_comm

repeat rw [← add_assoc]
rw [add_comm b a]
rfl

让生活更轻松

repeat rw [add_assoc]
rw [add_left_comm b c, add_comm d b]
rfl

让生活变得简单

simp only [add_assoc, add_left_comm, add_comm]

最简单的方法

simp_add

pred

rw [← pred_succ a, h, pred]
rfl

is_zero

-- symm
-- apply zero_ne_succ
intro h
rw [← is_zero_succ a, h, is_zero_zero]
trivial

用于证明等价的算法

contrapose! h
apply succ_inj at h
exact h

decide

decide

还是 decide

decide

≤ 世界

use 策略

use 0
rw [add_zero]
rfl

0 ≤ x

use x
rw [zero_add]
rfl

x ≤ succ x

use 1
rw [succ_eq_add_one]
rfl

x ≤ y 且 y ≤ z 意味着 x ≤ z

cases hxy with a ha
cases hyz with b hb
rw [ha] at hb
rw [hb]
use a+b
rw [add_assoc]
rfl

x ≤ 0 → x = 0

cases hx with a ha
symm at ha
apply add_right_eq_zero at ha
exact ha

x ≤ y 且 y ≤ x 意味着 x = y

cases hxy with a ha
cases hyx with b hb
rw [hb, add_assoc] at ha
nth_rewrite 1 [← add_zero y] at ha
apply add_left_cancel at ha
symm at ha
apply add_right_eq_zero at ha
rw [ha, add_zero] at hb
exact hb

处理 or

cases h with hx hy
right
exact hx
left
exact hy

x ≤ y 或 y ≤ x

induction y with d hd
right
use x
rw [zero_add]
rfl
cases hd with h1 h2
left
cases h1 with e h1
use e+1
rw [h1, succ_eq_add_one, add_assoc]
rfl
cases h2 with e h2
cases e with a
left
use 1
rw [h2, succ_eq_add_one, add_zero]
rfl
right
use a
rw [h2, add_succ, succ_add]
rfl

succ x ≤ succ y → x ≤ y

cases hx with a ha
rw [succ_add] at ha
apply succ_inj at ha
use a
rw [ha]
rfl

x≤1

cases hx with a ha
cases x with b hb
left
rfl
rw [one_eq_succ_zero, succ_add] at ha
apply succ_inj at ha
symm at ha
apply add_right_eq_zero at ha
right
rw [one_eq_succ_zero, ha]
rfl

le_two

cases hx with a ha
cases x with b hb
left
rfl
cases b with c hc
right
left
rw [← one_eq_succ_zero]
rfl
repeat rw [succ_add] at ha
rw [two_eq_succ_one, one_eq_succ_zero] at ha
apply succ_inj at ha
apply succ_inj at ha
symm at ha
apply add_right_eq_zero at ha
right
right
rw [ha, ← one_eq_succ_zero, ← two_eq_succ_one]
rfl

高级乘法世界

mul_le_mul_right

cases h with c hc
use c*t
rw [hc, add_mul]
rfl

mul_left_ne_zero

contrapose! h
rw [h, mul_zero]
rfl

eq_succ_of_ne_zero

cases a with b hb
tauto
tauto

one_le_of_ne_zero

apply eq_succ_of_ne_zero at ha
cases ha with n hn
use n
rw [hn, succ_eq_add_one, add_comm]
rfl

le_mul_right

apply mul_left_ne_zero at h
apply eq_succ_of_ne_zero at h
cases h with c hc
use a*c
rw [hc, mul_succ, add_comm]
rfl

mul_right_eq_one

have h1 : x * y ≠ 0
rw [h]
exact one_ne_zero
apply le_mul_right at h1
rw [h] at h1
apply le_one at h1
cases h1 with hl hr
rw [hl, zero_mul] at h
tauto
exact hr

mul_ne_zero

apply eq_succ_of_ne_zero at ha
apply eq_succ_of_ne_zero at hb
cases ha with c hc
cases hb with d hd
rw [hc, hd, mul_succ, add_succ]
symm
apply zero_ne_succ

mul_eq_zero

contrapose! h
have h1 := mul_ne_zero a b
tauto

mul_left_cancel

induction b with d hd generalizing c
rw [mul_zero] at h
symm at h
apply mul_eq_zero at h
tauto
rw [mul_succ] at h
cases c with e
rw [mul_zero] at h
apply add_left_eq_zero at h
tauto
rw [mul_succ] at h
apply add_right_cancel at h
apply hd at h
rw [h]
rfl

mul_right_eq_self

nth_rewrite 2 [← mul_one a] at h
apply mul_left_cancel at h
exact h
exact ha