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

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

演習03-01

-- 目標1. section
-- section は変数のスコープをつけるもの．
variable (A B : Prop)

section
  variable (a : A)

  example : A := 
    a

  example : (A → B) → B :=
    fun (f : A → B) => f a
end 

section
  variable (h : A ∧ B)
  -- ここからは A ∧ B が仮定される
  example : A :=
    -- a は unknown identifier になる
    h.left
end

演習03-02

-- 目標．証明の定石
-- 目標１．implication (→)
-- 目標２．conjunction (∧)
variable (A B : Prop)
-- implicationの証明の方法
-- example : 仮定 → 帰結 := 
-- fun 仮定 => 帰結の証明
section 
  example : B → B ∧ B :=
    fun h : B => show B ∧ B from And.intro h h
end
-- conjunctionの証明の方法
-- example : 左 ∧ 右 := And.intro 左の証明 右の証明
section
  variable (h : A ∧ B)
  example : B ∧ A :=
    And.intro
      (show B from h.right)
      (show A from h.left)
end 

演習03-03

-- 目標．証明の定石
-- 目標１．disjunction (∨)
-- 目標２．negation (¬)
variable (A B : Prop)

-- disjunction (∨) の証明
-- example : 左 ∨ 右 := Or.inl 左の証明 
-- example : 左 ∨ 右 := Or.inr 右の証明 
section
  example (h : A) : A ∨ B := Or.inl h
  example (h : B) : A ∨ B := Or.inr h
end

-- negation (¬) の証明
-- example : ¬ 命題 := 
-- fun h : 命題 => 矛盾の証明
-- 矛盾の証明は show false from false の証明
section
  variable (h : ¬ A) -- A → false の略記
  example : ¬ (A ∧ B) :=
    fun g : A ∧ B => h g.left
end

-- tactics modeでの ¬ (A ∧ B)の証明
section
  variable (h : ¬ A) -- A → false の略記
  example : ¬ (A ∧ B) := by
  -- A ∧ Bを仮定として導入します。
  intro (g : A ∧ B) -- これは A ∧ Bの仮定を持ってきます
  -- gからAの部分を取り出します
  have ha : A := g.left
  -- しかし、hはAが真であればfalseを導出するという意味なので、これを使ってfalseを導出します
  exact h ha
end
-- 上記の証明では，A ∧ Bを仮定として導入し，この仮定からAを導出します．しかし，変数hはAが真であればfalseを導出する能力を持っているので、それを使ってfalseを導出し、¬ (A ∧ B)を証明します．

演習03-04

-- 目標．証明の定石
-- 目標１．ex false (false → 任意の命題)
-- 目標２．bi-implication (↔)
variable (A : Prop)
-- ex falso quodlibet（矛盾からは何でも導出される）
-- example : 命題 := False.elim falseの証明
section
  variable (h : A ∧ ¬ A)
  example (X : Prop) : X := 
    False.elim (show False from h.right h.left)
    -- ¬ A は A → false なので，h.right に h.left (A)を代入してFalseを得る
end

-- example : 命題 := 命題1 ↔ 命題2
-- iff.intro
-- (show 命題1 → 命題2, from 命題1 → 命題2の証明)
-- (show 命題2 → 命題1, from 命題2 → 命題1の証明)
#print Iff.intro -- Iff.intro の説明をinfoviewで見る

section
  variable (B : Prop)
  example : (A ∧ B) ↔ (B ∧ A) :=
    Iff.intro
      (fun h : A ∧ B =>
        show B ∧ A from And.intro h.right h.left)
      (fun h : B ∧ A =>
        show A ∧ B from And.intro h.right h.left)
end