Posted on 2023-03-21

LEAN『Natural Number Game』やった

LEAN4を学ぶために Natural Number Game を友人とやった.

Tutorial World

Level 1: `refl` tactic

refl: 反射律 X = X を証明できる

lemma

lemma example1 (x y z : mynat) : x * y + z = x * y + z :=

proof

begin
  refl,
end

, はセミコロンみたいなものでproverが動く

Level2: `rw` tactic

rw h: h : A = B の時, A を B に出来る

x y : mynat,
h : y = x + 7
⊢ 2 * y = 2 * (x + 7)

h が仮定で ⊢ が証明したいgoal

lemma

lemma example2 (x y : mynat) (h : y = x + 7) : 2 * y = 2 * (x + 7) :=

proof

rw h
- ⊢ 2 * y = 2 * (x + 7) に
refl
- proof complete

Level 3: Peano's axioms

lemma

lemma example3 (a b : mynat) (h : succ a = b) : succ(succ(a)) = succ(b) :=

proof

rw h, -- succ(succ(a)) -(h)-> succ(b)
refl,

Level 4: Addition

lemma

lemma add_succ_zero (a : mynat) : a + succ(0) = succ(a) :=

proof

rw add_succ, -- succ (a + 0) = succ a
rw add_zero, -- succ a = succ a
refl,

Addition World

Level 1: `induction` tactic

zero_add(n : mynat) : 0 + n = n を証明したい
- 可換性 x + y = y + x は未証明(ボス) なので使えない
- だが, add_zero(n : mynat) : n + 0 = n はペアノの公理なので使える
induction n with d hd, で2つのgoalが出来る

⊢ 0 + 0 = 0

case mynat.succ
d : mynat,
hd : 0 + d = d
⊢ 0 + succ d = succ d

tacticは最初のgoalに作用する

proof

induction n with d hd,
-- h0
rw add_zero, -- 0 + 0 = 0 => 0 = 0
refl,
-- h1
rw add_succ, -- 0 + succ d = succ d => succ (0 + d) = succ d
rw hd, -- succ d = succ d
refl,

Level 2: `add_assoc`

lemma

lemma add_assoc (a b c : mynat) : (a + b) + c = a + (b + c) :=

proof

hint: 足し算は一番右の変数の再帰によって定義されたので、一番右の変数で帰納法を使いましょう

induction c with d hd,
-- h: a + b + 0 = a + (b + 0)
rw add_zero, -- a + b = a + (b + 0)
rw add_zero, -- a + b = a + b
refl,
-- hd : a + b + d = a + (b + d)
rw add_succ, -- succ (a + b + d) = a + (b + succ d)
rw add_succ, -- succ (a + b + d) = a + succ (b + d)
rw add_succ, -- succ (a + b + d) = succ (a + (b + d))
rw hd,
refl,

Level 3: `succ_add`

lemma

emma succ_add (a b : mynat) : succ a + b = succ (a + b) :=

proof

induction b with d hd,
rw add_zero,
rw add_zero,
refl,

rw add_succ,
rw add_succ,
rw hd,
refl,

Level 4: `add_comm` (boss)

boss battle music
- ノリが好き

|300

lemma

lemma add_comm (a b : mynat) : a + b = b + a :=

induction a with d hd,
rw zero_add,
rw add_zero,
refl,

rw succ_add,
rw add_succ,
rw hd,
refl,

帰納法慣れてきた

Level 5: `succ_eq_add_one`

theorem

theorem succ_eq_add_one (n : mynat) : succ n = n + 1 :=

proof

rw add_comm,
induction n with d hd,

rw add_zero,
rw one_eq_succ_zero,
refl,

rw add_succ,
rw hd,
refl,

Level 6: `add_right_comm`

lemma

lemma add_right_comm (a b c : mynat) : a + b + c = a + c + b :=

proof

rw add_assoc,
rw add_comm b c, -- 左辺の (b + c) に適用する
rw add_assoc,
refl,

Multiplication World

[[2023-03-16]]

Level 1 `zero_mul`

lemma: 0 * m = 0

induction m with k hk,
-- 0 * 0 = 0
rw mul_zero,
refl,
-- 0 * succ k = 0
rw mul_succ,
rw hk,
rw add_zero,
refl,

Level 2 `mul_one`

lemma: m * 1 = m

rw one_eq_succ_zero,
rw mul_succ,
rw mul_zero,
rw zero_add,
refl,

Level 3 `one_mul`

lemma: 1 * m = m

induction m with k hk,
-- 1 * 0 = 0
rw mul_zero,
refl,
-- hk: 1 * k = k
-- 1 * succ k = succ k
rw mul_succ,
rw hk,
rw succ_eq_add_one,
refl,

Level 4 `mul_add`

lemma: t * (a + b) = t * a + t * b

induction b with k hk,
-- t * (a + 0) = t * a + t * 0
rw add_zero,
rw mul_zero,
rw add_zero,
refl,
-- t * (a + succ k) = t * a + t * succ k
rw add_succ,
rw mul_succ,
rw mul_succ,
rw hk,
rw add_assoc,
refl,

Level 5 `mul_assoc`

lemma: (ab)c = a(bc)

induction c with k hk,
-- a * b * 0 = a * (b * 0)
repeat {rw mul_zero},
-- a * b * succ k = a * (b * succ k)
repeat {rw mul_succ},
rw hk,
rwa ← mul_add,

Level 6 `succ_mul`

lemma: succ a * b = a * b + b

induction b with k hk,
-- succ a * 0 = a * 0 + 0
repeat {rw mul_zero},
rwa add_zero,
-- succ a * succ k = a * succ k + succ k
repeat {rw mul_succ},
rw hk,
repeat {rw add_succ},
rw add_assoc,
rw add_right_comm,
rwa add_assoc,

Level 7 `add_mul`

lemma: (a + b) * t = a * t + b * t

induction b with k hk,
rw add_zero,
rw zero_mul,
rwa add_zero,
  
rw add_succ,
rw succ_mul,
rw succ_mul,
rw hk,
simp,

Level 8 `mul_comm`

lemma: a * b = b * a

induction b with k hk,
-- a * 0 = 0 * a
simp,
-- a * succ k = succ k * a
rw mul_succ,
rw succ_mul,
rwa hk,

Level 9 `mul_left_comm`

lemma: a * (b * c) = b * (a * c)

induction a with k hk,
-- 0(bc) = b(0c)
simp,
-- succ k * (bc) = b(succ k * c)
repeat {rw succ_mul},
-- k(bc) + bc = b(kc + c)
rw mul_add,
-- k(bc) + bc = b(kc) + bc
rw hk,
-- b * (k * c) + b * c = b * (k * c) + b * c
simp,

Power World

Level 1 `zero_pow_zero`

lemma: 0 ^ 0 = 1

rwa pow_zero,

Level 2 `zero_pow_succ`

lemma: 0 ^ succ m = 0

rw pow_succ,
rwa mul_zero,

Level 3 `pow_one`

lemma: a ^ 1 = a

rw one_eq_succ_zero,
rw pow_succ,
rw pow_zero,
rwa one_mul,

Level 4 `one_pow`

lemma: 1 ^ m = 1

induction m with k hk,
rwa pow_zero,

rw pow_succ,
rw mul_one,
rwa hk,

Level 5 `pow_add`

lemma: a ^ (m + n) = a ^ m + a ^ n

induction n with k hk,
rw add_zero,
rw pow_zero,
rwa mul_one,

rw add_succ,
rw pow_succ,
rw pow_succ,
rw hk,
rwa mul_assoc,

Level 6 `mul_pow`

lemma: (ab)^n = a^n b^n

induction n with k hk,
repeat {rw pow_zero},
simp,

repeat {rw pow_succ},
rw hk,
simp,

Level 7 `pow_pow`

lemma: (a ^ m) ^ n = a ^ (mn)

induction n with k hk,
-- (a ^ m) ^ 0 = a ^ (m * 0)
rw pow_zero,
rw mul_zero,
rwa pow_zero,
-- (a ^ m) ^ succ k = a ^ (m * succ k)
rw pow_succ,
rw mul_succ,
rw hk,
-- a ^ mk * a ^ m = a ^ (mk + m)
rwa pow_add,

Level 8 `add_squared`

lemma: (a + b) ^ 2 = a ^ 2 + b ^ 2 + 2ab

rw two_eq_succ_one,
repeat {rw pow_succ},
simp,
repeat {rw pow_one},
rw mul_succ,
simp,
repeat {rw mul_add},
repeat {rw add_mul},
simp,

Function World

新しいtactics

exact
intro
have
apply

$P, Q, R$ 集合, $h, j, k$ それ上の関数 $p \in P$

Level 1 `exact` tactic

構成方法を書く位の感じ?

example (P Q: Type) (p: P) (h: P -> Q): Q := begin
  exact h(p),
end

Level 2 `intro` tactic

n -> 3n + 2 関数を作ろう

数学者は $\mathrm{Hom}(\mathbb{N}, \mathbb{N})$ (線形写像の全体)と書くが, コンピュータサイエンティストは f: X -> Y と書く
intro x : 任意の $x \in X$

example: mynat -> mynat :=
begin
  intro n,
  exact 3 * n + 2,
end

Level 3 `have` tactic

$P$ から $U$ を構成したいときに exact l(j(h(p))) と書けるが,

-- exact l(j(h(p))),
have q := h(p),
have t: T := j(q),
have u: U := l(t),
exact u,

Level 4 `apply` tactic

apply: goalを動かすtactics
- l: T -> U で apply l すると $\vdash T$ が $\vdash U$ に変わる

apply l,
apply j,
apply h,
exact p,

Level 5 `P -> (Q -> P)`

$\to$ は右結合

example (P Q: Type): P -> (Q -> P) :=
begin
  -- intros p q,
  intro p,
  intro q,
  exact p,
end

Level 6 `(P -> (Q -> R)) -> ((P -> Q) -> (P -> R))`

矢印の左がintroで貰える

-- (P -> Q -> R) -> ((P -> Q) -> (P -> R))
intro f, -- P -> Q -> R
intro h, -- P -> Q
intro p, -- P
exact f(p)(h(p)),

Level 7 `(P -> Q) -> ((Q -> F) -> (P -> F))`

-- (P -> Q) -> ((Q -> F) -> (P -> F))
intro f, -- P -> Q
intro g, -- Q -> F
intro p, -- P
exact g(f(p)),

Level 8 `(P -> Q) -> ((Q -> empty) -> (P -> empty))`

-- (P -> Q) -> ((Q -> empty) -> (P -> empty))
intro f, -- P -> Q
intro g, -- Q -> empty
intro p, -- P
exact g(f(p)),

Level 9 Big Maze

-- A -> L
intro a, -- A
apply f15, -- I -> L
apply f11, -- J -> I
apply f9, -- G -> J
apply f8, -- F -> G
apply f5, -- E -> F
apply f2, -- B -> E
apply f1, -- A -> B
exact a,

Proposition World

Level 1

apply (l∘j∘h)
exact p,

Level 8

repeat {rw not_iff_imp_false}, -- ¬Q = Q => false
intro a,
intro b,
intro p,
apply b,
apply a,
exact p,

Advanced Proposition World

split
cases
left
right
exfalso

Level 1

split: $\land$ か <-> の時に2つのgoalに分ける

example  (P Q: Prop) (p: P) (q: Q): P \land Q :=
begin
  split,
  exact p,
  exact q,
end

Level 2

lemma and_symm (P Q: Prop): P \land Q -> Q \land P :=
begin
  intro h,
  cases h with p q,
  split,
  exact q,
  exact p,
end

Level 3 `and_trans`

intro a,
intro b,
split,
  
cases a with a1 a2,
exact a1,
  
cases b with b1 b2,
exact b2,

Level 4 `iff_trans`

intro a,
intro b,
split,
intro p,
cases a with a1 a2,
cases b with b1 b2,
exact b1(a1(p)),
  
intro r,
cases a with a1 a2,
cases b with b1 b2,
exact a2(b2(r)),

Level 5 `iff_trans`

(P <-> Q) -> (Q <-> R) -> (P <-> R)
intro a, -- P <-> Q
intro b, -- Q <-> R
split,
-- P -> R
intro p, -- P
exact (b.1 ∘ a.1) p,
-- R -> P
intro r, -- R
exact (a.2 ∘ b.2) r,

cases a with a1 a2 は a.1, a.2 とかける

Level 6 `left`, `right`

-- Q -> (P or Q)
intro q, -- Q
right, -- Q
exact q,

Level 7 `or_symm`

intro a,
cases a with p q,
right, exact p,
left, exact q,

Level 8 `and_or_distib_left`

split,
intro a,
cases a with p qr,
cases qr with q r,
left,
split,
exact p,
exact q,

right,
split,
exact p,
exact r,
  
intro pqpr,
split,
cases pqpr with pq pr,
cases pq with p q,
exact p,
cases pr with p r,
exact p,
  
cases pqpr with pq pr,
cases pq with p q,
left,
exact q,
  
cases pr with p r,
right,
exact r,

Level 9 `exfalso`

goal を false

rw not_iff_imp_false, P ^ (P -> false) -> Q
intro h,
cases h with h1 h2, -- P, P -> false
exfalso,-- vdash false
exact h2 h1,

Level 10 排中律

Note the semicolon! It means "do the next tactic to all the goals, not just the top one". After it, there are four goals, one for each of the four possibilities PQ=TT, TF, FT, FF. You can see that p is a proof of P in some of the goals, and a proof of ¬ P in others. Similar comments apply to q.

by_cases: P を総列挙したゴールを作る

by_cases p : P; by_cases q : Q,
-- P, Q |- (!Q -> !P) -> P -> Q
intro h1,
intro h2,
exact q,
-- P, !Q |- (!Q -> !P) -> P -> Q
intro h1,
intro h2,
have h3 := h1(q),
exfalso,
rw not_iff_imp_false at h3,
exact h3(h2),
-- !P, Q |- ...
cc,
-- !P, !Q |- ...
cc,

Advanced Addition World

Level 1 `succ_inj`

ペアノの公理では
- succ_inj
- zero_ne_succ がある. X != Y は X = Y => false

exact succ_inj(hs),

Level 2 `succ_succ_inj`

succ_inj(a b: mynat) : succ(a) = succ(b) -> a = b

exact succ_inj(succ_inj(h)),

Level 3 `succ_eq_succ_of_eq`

a = b => succ a = succ b

intro h,
rwa h,

Level 4 `eq_iff_succ_eq_succ`

-- ->
split,
apply succ_inj,
-- <-
intro h,
rwa h,

Level 5 `add_right_cancel`

a + t = b + t => a = b

intro h,
induction t with k hk,
-- h: a + 0 = b + 0 |- a + b
repeat {rw add_zero at h},
exact h,
-- hk: a + k = b + k -> a = b
-- h: a + succ k = b + succ k
repeat {rw add_succ at h},
-- h: succ (a + k) = succ (b + k)
rw succ_eq_succ_iff at h,
-- h: a + k = b + k
rwa hk,

Level 6 `add_left_cancel`

intro h,
induction t with k hk,
repeat {rw zero_add at h},
exact h,

repeat {rw succ_add at h},
rw succ_eq_succ_iff at h,
apply hk,
exact h,

Level 7 `add_right_cancel_iff`

a + t = b + t <=> a = b

split,
apply add_right_cancel,

intro h,
rwa h,

Level 8 `eq_zero_of_add_right_eq_self`

intro h,
induction a with k hk,

rw zero_add at h,
apply h,

rw succ_add at h,
apply hk,
apply succ_inj,
apply h,

Level 9 `succ_ne_zero`

= とかを入れ替える

symmetry,
apply zero_ne_succ,

Level 10 `add_left_eq_zero`

cases b with d,
refl,

rw add_succ at H,
exfalso,
-- false <- a + d
apply succ_ne_zero(a + d),
rwa H,

Level 11 `add_right_eq_zero`

a + b = 0 -> a = 0

intro h,
rw add_comm at h,
apply add_left_eq_zero(h),

Level 12 `add_one_eq_succ`

symmetry,
apply succ_eq_add_one,

Level 13 `ne_succ_self`

intro h,
induction n with k hk,
-- h: 0 = succ 0 |- false
apply succ_ne_zero(0),
symmetry,
apply h,
-- hk: k = succ k -> false
-- h: succ k = succ (succ k)
-- |- false
apply hk,
-- |- k = succ k
apply succ_inj,
-- |- succ k = succ (succ k)
apply h,

Advanced Multiplication World

Level 1 `mul_pos`

cases b with n と書くと b = 0, b = succ(n) にgoalが分かれる

⊢ X≠Y がゴールなら intro h で h : X = Y となり、⊢ false がゴールとなる。これは、X ≠ Y は (X = Y) → false を意味するからです。逆に、ゴールが偽で、h : X ≠ Y を仮説として持っている場合、apply h でゴールが X = Y になる。

hab : succ (3 x + 2 y + 1) = 0 が仮説で、あなたのゴールが⊢偽の場合、正確な succ_ne_zero hab はゴールを解決します。なぜなら Lean は が 3 x + 2 y + 1 であるべきだと理解するためです。

false -> h: 0 != 0 -> |- 0 = 0 -> refl

intros h1 h2 h3,
cases a with k,
apply h1,
refl,

cases b with l,
apply h2,
refl,
  
rw succ_mul at h3,
rw mul_succ at h3,
rw add_succ at h3,
exact succ_ne_zero _ h3,

Level 2

ab = 0 -> a = 0 v b = 0

cases a with k,
simp,

cases b with l,
simp,

rw succ_mul at h,
rw mul_succ at h,
rw add_succ at h,
exfalso,
exact succ_ne_zero _ h,

Level 3

ab = 0 iff a = 0 v b = 0

split,
apply eq_zero_or_eq_zero_of_mul_eq_zero,
intro h,
cases h with h1 h2,
rw h1, simp,
rw h2, simp,

Level 4 `mul_left_cancel`

a != 0, ab = ac => b = c
a, b 固定, 仮定 P(c): ab = ac -> b = c
- ab = ad => b = d
- goal: ab = a(d + 1) => b = d + 1
  - だが, ab = ad is not true
より強い仮定, a != 0 を固定した上で, 任意の b に対して ab = ac => b = c を c の帰納法で証明
- induction c with d hd generalizing b
16. Functions in Lean — Logic and Proof 3.18.4 documentation

induction c with k hk generalizing b,
rw mul_zero,
intro h,
rw mul_eq_zero_iff at h,
cases h with h1 h2,
exfalso,
apply ha,
apply h1,
apply h2,
  
intro h,

cases b with p,

exfalso,

rw mul_zero at h,

symmetry at h,

rw mul_eq_zero_iff at h,

cases h with h1 h2,

apply ha,

assumption,

  

apply succ_ne_zero(k),

assumption,

  

apply succ_eq_succ_of_eq,

have hkp := hk(p),

apply hkp,

rw mul_succ at h,

rw mul_succ at h,

  

apply add_right_cancel (a * p) a (a * k),

exact h,

仮定 hk が forall b である理由
- -> cases b with p として succ p したいから

Inequality World

[[2023-03-21]]

le_iff_exists_add(a b: mynat): a <= b <-> exists c, b = a + c

Level 1 `use` tactics

goal x <= 1 + x
use はexists cに具体的な値を与える

rw le_iff_exists_add, -- exist c
use 1, -- 1 + x = x + 1
exact add_comm 1 x,

Level 2 `le_refl`

rw le_iff_exists_add,
use 0,
simp,

attribute [refl] mynat.le_refl これ以降 refl で小なりイコールも対処できる

incatation: 呪文

Level 3 `le_succ_of_le`

仮定に $h:{}^{\exists} c,$ がある時はどうする?

intro h,
rw le_iff_exists_add at h ⊢,
cases h with c hc,
rw succ_eq_add_one,
rw hc,
use c + 1,
simp,

Level 4 `zero_le`

rw le_iff_exists_add,
use a,
simp,

Level 5 `le_trans`

rw le_iff_exists_add at hbc ⊢,
cases hab with p1 hp1, -- p1: mynat, hp1: b = a + p1
rw hp1 at hbc,
cases hbc with p2 hp2, -- p2: mynat, hp2: c = a + p1 + p2
rw hp2,
use p1 + p2,
simp,

不等式の推移律の証明：定義に戻って考える、存在命題の練習 | 趣味の大学数学

Level 6 `le_antisymm`

eq_zero_of_add_right_eq_self: a + b = a -> b = 0
have h := eq_zero_of_add_right_eq_self hd, と書くと
- hd: a + (c + d) = a
- h: c + d = 0

rw le_iff_exists_add at hab,
cases hab with p1 hp1,
rw le_iff_exists_add at hba,
cases hba with p2 hp2,
rw hp1 at hp2,
rw hp1,
symmetry at hp2,
rw add_assoc at hp2,
have h := eq_zero_of_add_right_eq_self hp2,
rw ← hp1,
rw hp1,
have p1_0 := add_right_eq_zero h,
rw p1_0,
simp,

Level 7 `le_zero`

rw le_iff_exists_add at h,
cases h with p hp,
symmetry at hp,
have p_zero := add_right_eq_zero hp,
exact p_zero,

Level 8 `succ_le_succ`

cases h with p hp,
rw hp,
rw le_iff_exists_add,
rw ← succ_add,use p,
refl,

Level 9 `le_total`

revert b,
induction a with k hk,
intro b, left, exact zero_le b,

intro b,
cases b,

right,
exact zero_le(succ k),
cases hk b with hkl hkr,
left,
exact succ_le_succ k b hkl,

right,
exact succ_le_succ b k hkr,

b を固定して a の帰納法

Level 10 `le_succ_self`

rw le_iff_exists_add,
use 1,
rwa succ_eq_add_one,

Level 11 `add_le_add_right`

[[2023-03-22]]

intro h,
rw le_iff_exists_add at h,
intro t,
rw le_iff_exists_add,
simp,
cases h with c hc,
rw hc,
use c,
simp,

Level 12 `le_of_succ_le_succ`

intro h,
rw le_iff_exists_add at h,
cases h with p hp,
rw le_iff_exists_add,
rw succ_add at hp,
use p,
have hp2 := succ_inj hp,
exact hp2,

Level 13 `not_succ_le_self`

左辺だけ rw するには conv が使える

intro saa,
apply ne_succ_self a,
apply le_antisymm a (succ a),
exact le_succ_self a,
exact saa,

Level 14 `add_le_add_left`

simp,
apply add_le_add_right h,

Level 15 introducing `<`

a <= b && !(b <= a) => succ a <= b

a <= b は ex k, a + k = b なので, use できる

intro h,
cases h with ab ba,
cases ab with k hk,
cases k with z sk,
exfalso,
rw add_zero at hk,
apply ba,
use 0,
symmetry at hk,
simp,
exact hk,

use z,
rw succ_add,
rw hk,
rwa add_succ,

Level 16 equivalence of two definitions of `<`

succ a <= b => a <= b && !(b <= a)

intro sab,
split,

rw le_iff_exists_add,
cases sab with k hk,
use succ k,
rw add_succ,
rw succ_add at hk,
exact hk,

intro ba,
apply not_succ_le_self a,
exact le_trans _ _ _ sab ba,

Level 17 definition of `<`

a < b <=> succ(a) <= b

split,
apply lt_aux_one,
apply lt_aux_two,

What's next?

xena/README.md at master · kbuzzard/xena · GitHub
Q: 統計は扱えるのか?
- mathlib/src/probability at master · leanprover-community/mathlib · GitHub
- probability.martingale.convergence - mathlib docs