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

千葉大学 萩原先生の 応用情報数理学特論　第０７回 の演習をLean4で写経してみる．

演習07-01

-- 目標１．Exists.elimに慣れる
-- 目標２．$ ← LEAN4では不要？
-- 目標３．assume に複数の引数を与える $ ← LEAN4では intro
variable (U : Type)
variable (A B : U → Prop)

-- Exists.elim は ∃ を除去する規則
-- 逆に Exists.intro は ∃ を導入する規則
example : (∃ x, A x ) → ∃ x, A x ∨ B x := by
  intro (h1 : ∃ x, A x)    -- goal は ∃ x, A x ∨ B x
  apply Exists.elim h1     -- goal は ∀ (a : U), A a → ∃ x, A x ∨ B x
  intro (x : U) (h2 : A x) -- goal は ∃ x, A x ∨ B x
  apply Exists.intro x     -- goal は A x ∨ B x, Exists.intro 変数 だと ∃ x を消す．
  apply Or.inl h2
  -- Exists.elim で証明したい命題の ∃ を除去し，全称記号の仮定を導入した上で
  -- x と Ax を再導入（仮定）し，命題を解いている．

-- haveを使った書き方の場合
example : (∃ x, A x ) → ∃ x, A x ∨ B x := by
  intro (h1 : ∃ x, A x)    
  apply Exists.elim h1     
  intro (x : U) (h2 : A x) 
  have hAB : A x ∨ B x := Or.inl h2
  apply Exists.intro x hAB

-- term mode で書くとこうなる
example : (∃ x, A x ) → ∃ x, A x ∨ B x := 
  fun (h1 : ∃ x, A x) => Exists.elim h1 (fun (x : U) (h2 : A x) => Exists.intro x (Or.inl h2))

-- $ はなくても改行できる．
example : (∃ x, A x ) → ∃ x, A x ∨ B x := 
  fun (h1 : ∃ x, A x) => Exists.elim h1 
  fun (x : U) (h2 : A x) => Exists.intro x (Or.inl h2)

-- 以下はもう一つの例
-- 紹介されているコードとはだいぶ違うけど証明の方針は同じ
example : (∀ x, A x ) → ¬ ∃ x, ¬ A x := by
  intro (h1 : ∀ (x : U), A x) (h2 : ∃ (x : U), ¬ A x) -- 背理法の匂い
  apply Exists.elim h2 -- h2の ∃ を除去
  intro (x : U) (h3 : ¬ A x) -- x と ¬ A x を仮定
  have h4 : A x := h1 x -- h1の ∀ を使って A x を導出
  contradiction -- ¬ A x と A x が矛盾するので矛盾

-- 紹介されたコードに近い書き方
example : (∀ x, A x ) → ¬ ∃ x, ¬ A x := by
  intro (h1 : ∀ (x : U), A x) (h2 : ∃ (x : U), ¬ A x) -- 背理法の匂い
  apply Exists.elim h2 -- h2の ∃ を除去
  intro (x : U) (h3 : ¬ A x) -- x と ¬ A x を仮定
  have h4 : A x := h1 x -- h1の ∀ を使って A x を導出
  apply show False from h3 h4 -- ¬ A x と A x が矛盾するので矛盾

-- 学んだこと
-- 証明したい命題が ∃ x, A x → P x のとき，
-- Exists.elim h1 は ∀ (a : U), A a → P a という形の命題を導入する．
-- その後，intro (a : U) (h2 : A a) で ∃ のない仮定を導入し，P a を証明する．

演習07-02

-- 目標１．calc
-- 目標２．Eq.symm ： 対称律
variable (A : Type)
variable (a b c d : A)

example : (a = b) → (b = c) → (d = a) → (d = c) := by
  intro (hab : a = b) (hbc : b = c) (hda : d = a)
  calc d = a := by apply hda
      _  = b := by apply hab
      _  = c := by apply hbc

-- rw でもよい．
example : (a = b) → (b = c) → (d = a) → (d = c) := by
  intro (hab : a = b) (hbc : b = c) (hda : d = a)
  calc d = a := by rw [hda]
      _  = b := by rw [hab]
      _  = c := by rw [hbc]

-- rw で一気に式変形しても良い．
example : (a = b) → (b = c) → (d = a) → (d = c) := by
  intro (hab : a = b) (hbc : b = c) (hda : d = a)
  calc d = c := by rw [hda, hab, hbc]

#print Eq.symm

example : (a = b) → (b = c) → (d = a) → (d = c) := by
  intro (hab : a = b) (hbc : b = c) (hda : d = a)
  have hdc : d = c := by rw [hda, hab, hbc]
  exact hdc

example : (a = b) → (b = c) → (d = a) → (c = d) := by
  intro (hab : a = b) (hbc : b = c) (hda : d = a)
  have hdc : d = c := by rw [hda, hab, hbc]
  apply show c = d from Eq.symm hdc -- Eq.symm で左右の交換

example : (a = b) → (b = c) → (c = a) := by 
  intro (hab : a = b) (hbc : b = c)
  calc c = b := Eq.symm hbc -- Eq.symm で hbc の左右の交換
      _  = a := Eq.symm hab -- Eq.symm で hab の左右の交換

-- 左右交換は Eq.symm でなくても，rwならば ← でできる． 
example : (a = b) → (b = c) → (c = a) := by 
  intro (hab : a = b) (hbc : b = c)
  have hca : c = a := by rw [←hbc, ←hab]
  exact hca

-- 学んだこと
-- calcの使い方
-- Eq.symm で左右の交換
-- rw での式変形の書き方

演習07-03

-- 目標１．Eq.refl ： 反射律
-- 目標２．Eq.trans： 推移律
variable (A : Type)
variable (a b c : A)

#check Eq.refl
example : a = a := Eq.refl a

example : a = a := by 
  apply Eq.refl -- tactic modeだと apply Eq.refl で証明完了

#check Eq.trans
example : (a = b) → (b = c) → (a = c) := 
  fun h1 h2 => Eq.trans h1 h2

-- tactic mode
example : (a = b) → (b = c) → (a = c) := by
  intro h1 h2
  apply Eq.trans h1 h2

example : (b = a) → (b = c) → (a = c) := 
  fun h1 h2 => Eq.trans (Eq.symm h1) h2

-- tactic mode
example : (b = a) → (b = c) → (a = c) := by
  intro h1 h2
  apply Eq.trans (Eq.symm h1) h2