LEAN写経　応用情報数理学特論　第１０回

千葉大学 萩原先生の 応用情報数理学特論　第１０回 の演習を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