千葉大学 萩原先生の 応用情報数理学特論 第１０回 の演習をLean4で写経してみる．
演習10-01
/- 目標１． ℕ
inductive
zero : ℕ
succ : ℕ → ℕ
-/
import Mathlib.Tactic -- Lean4だとだいたいこれで色々使えるようになる（適当．．．）
#print Nat -- これでNatの定義が見れる．
#check Nat.zero -- Lean では 0 も自然数
#check Nat.succ -- これでNat.succの型が見れる．
open Nat
#eval zero -- 0
#eval succ zero -- 1 ... 0の次の数
#eval succ (succ zero) -- 2 ... 1の次の数
-- #print + -- unexpected token '+'
#check Nat.add
#print Nat.add -- Lean4 では add._main で定義されていない．
/- add m 0 := m ... m + 0 :=m
add m succ n := succ (add m n) ... m + succ n := succ(m + n) -/
example (m : Nat) : m + 1 = succ m := rfl -- 定義のみの場合は rfl で証明できる．
example (m : Nat) : 1 + m = succ m := rfl -- 型が違うので証明出来ない
example (m : Nat) : 1 + m = succ m := by
rw [Nat.add_comm] -- 1 + m = m + 1
演習10-02
/- 目標１． add_succ ... ∀ (n m : ℕ), n + succ m = succ (n + m)
succ_add ... ∀ (n m : ℕ), succ n + m = succ (n + m)
-/
-- 目標２． Nat.rec_on
-- 目標３． rewrite, rw
import Mathlib.Tactic -- Lean4だとだいたいこれで色々使えるようになる（適当．．．）
open Nat
#check @add_succ
#print add_succ
#check @succ_add
#print succ_add
#print add_one
#print one_add
example (m : Nat) : 1 + m = succ m := one_add m
-- 数学的帰納法による証明
example (m : Nat) : 1 + m = succ m :=
Nat.recOn (motive := fun x => 1 + x = succ x)
m
(show 1 + 0 = succ 0 from rfl)
(fun (m : Nat) (h : 1 + m = succ m) =>
show 1 + succ m = succ (succ m) from
calc 1 + succ m
_ = succ (1 + m) := by rw [add_succ]
_ = succ (succ m) := by rw [h])
-- simp を使った省略版
example (m : Nat) : 1 + m = succ m :=
Nat.recOn (motive := fun x => 1 + x = succ x)
m
rfl -- base case
(fun m h => by simp [add_succ, h]) -- add_succ と仮定 h を使って簡約（よろしくやってもらう）
演習10-03
-- 目標１． Nat上の関数を定義する．≤ , < ... Nat上の大小関係
import Mathlib.Tactic -- Lean4だとだいたいこれで色々使えるようになる（適当．．．）
open Nat
def two_pow : ℕ → ℕ
| zero => 1 -- 2^0 = 1
| (succ n) => 2 * two_pow n -- 2^(succ n) = 2 * 2^n
#eval two_pow 10
example (n : Nat) : two_pow (succ n) = (two_pow n) + (two_pow n) := by
calc two_pow (succ n)
_ = 2 * two_pow n := by rfl
_ = (1 + 1) * two_pow n := by rfl
_ = (1 * two_pow n) + (1 * two_pow n) := by rw [right_distrib]
_ = (two_pow n) + (two_pow n) := by rw [one_mul]
def fib_ : ℕ → ℕ -- Nat.fib と被るため，fib_ とした．
| zero => 1
| 1 => 1
| (n+2) => fib_ (n+1) + fib_ n
#eval fib_ 0 -- 1
#eval fib 0 -- 0 Nat.fibだと0になる．
#eval fib_ 1 -- 1
#eval fib_ 2 -- 2
演習10-04
-- 目標１． ≤ , < ... Nat上の大小関係
-- 目標２． 定理を眺める
import Mathlib.Tactic -- Lean4だとだいたいこれで色々使えるようになる（適当．．．）
open Nat
#check zero_le -- 0 ≤ n
#check le_zero -- n ≤ 0 → n = 0
#check lt_succ_self -- n < succ n
#check le_succ -- n ≤ succ n
#check lt_of_lt_of_le -- n < m → m ≤ k → n < k
#check lt_of_le_of_lt -- n ≤ m → m < k → n < k
#check le_of_lt -- n < m → n ≤ m
#check lt_trans -- n < m → m < k → n < k
#check le_trans -- n ≤ m → m ≤ k → n ≤ k
#check le_refl -- n ≤ n
#check le_antisymm -- a = b
#check le_antisymm_iff -- a = b ↔ a ≤ b ∧ b ≤ a
#check le_total -- a ≤ b ∨ b ≤ a
#check succ_le_succ -- m ≤ n → succ m ≤ succ n
レポート課題
/-
課題：
参考文献の次のExerciseを解きなさい
・１２．５節のExercie２番
・１４．４節のExercise４番、
・１８．３節のExercise 1.a、1.b、2.b、2.d
-/
import Mathlib.Tactic -- Lean4だとだいたいこれで色々使えるようになる（適当．．．）
-- 12.5 Exercise 2
section
open Set
variable {U : Type}
/- defining "disjoint" -/
def disj (A B : Set U) : Prop := ∀ ⦃x⦄, x ∈ A → x ∈ B → False
example (A B : Set U) (h : ∀ x, ¬ (x ∈ A ∧ x ∈ B)) : disj A B := by
intro x
intro (h1 : x ∈ A)
intro (h2 : x ∈ B)
obtain (h3 : x ∈ A ∧ x ∈ B) := And.intro h1 h2
exact h x h3
-- notice that we do not have to mention x when applying
-- h : disj A B
example (A B : Set U) (h1 : disj A B) (x : U)
(h2 : x ∈ A) (h3 : x ∈ B) :
False := h1 h2 h3
-- the same is true of ⊆
example (A B : Set U) (x : U) (h : A ⊆ B) (h1 : x ∈ A) :
x ∈ B := h h1
example (A B C D : Set U) (h1 : disj A B) (h2 : C ⊆ A)
(h3 : D ⊆ B) : disj C D := by
intro x hC hD
have hA : x ∈ A := h2 hC
have hB : x ∈ B := h3 hD
exact h1 hA hB
end
-- 14.4 Exercise 4
section
open Nat
example : 1 ≤ 4 := by
calc
1 ≤ 2 := le_succ 1
_ ≤ 3 := le_succ 2
_ ≤ 4 := le_succ 3
end
-- 18.3 Exercise 1.a 1.b 2.b 2.d
section
open Nat
--1.a.
example : ∀ m n k : Nat, m * (n + k) = m * n + m * k := left_distrib
--1.b.
example : ∀ n : Nat, 0 * n = 0 := zero_mul
--2.b.
#check Nat.sub_le_sub_right
example : ∀ m n k : Nat, n + k ≤ m + k → n ≤ m := by
intro m n k
intro h
have h1 : n + k - k ≤ m + k - k := by
apply Nat.sub_le_sub_right h k
simp at h1 -- n ≤ m にする．
exact h1
--2.d.
example : ∀ m n : Nat, m ≥ n → (m = n) ∨ (m ≥ n+1) := by
intro m n h
cases Nat.eq_or_lt_of_le h with
| inl heq => -- 仮定の等式を使って goal の等式（左側）を証明する．
replace heq : m = n := Eq.symm heq
left
exact heq
| inr hlt => -- 仮定の不等式 < を使って goal の不等式（右側）を証明する．
right
exact hlt
#check Nat.eq_or_lt_of_le -- ≤ を = ∨ < に分解する．
end
Leave a Reply