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

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

演習04-01

-- 目標1. Or.elim
#print Or.elim

variable (A B C: Prop)

example (f : A → C) (g : B → C) : A ∨ B → C :=
  fun (h : A ∨ B) =>
    Or.elim h
      (fun (ha : A) => f ha)
      (fun (hb : B) => g hb)
-- 1行で書くなら
example (f : A → C) (g : B → C) : A ∨ B → C :=
  fun (h : A ∨ B) => Or.elim h f g

example : A ∨ (B ∧ C) → (A ∨ B) ∧ (A ∨ C) := -- 分配法則
  fun (h : A ∨ (B ∧ C)) =>
    And.intro
      (show (A ∨ B) from Or.elim h 
        (fun (ha : A) => (Or.inl ha))
        (fun (hbc : B ∧ C) => (Or.inr hbc.left)))
      (show (A ∨ C) from Or.elim h 
        (fun (ha : A) => (Or.inl ha))
        (fun (hbc : B ∧ C) => (Or.inr hbc.right)))
-- 別解: Aが成り立つ時の証明，Bが成り立つときの証明をそれぞれ書く
example : A ∨ (B ∧ C) → (A ∨ B) ∧ (A ∨ C) :=
  fun (h : A ∨ (B ∧ C)) =>
    Or.elim h
      (fun (ha : A) => And.intro (Or.inl ha) (Or.inl ha)) -- (A ∨ B) は A が真なので真，(A ∨ C) も A が真なので真，
      (fun (hbc : B ∧ C) => And.intro (Or.inr hbc.left) (Or.inr hbc.right))

演習04-02

-- 目標1. λ
variable (A B C: Prop)

variable (h1 : A → B)
variable (h2 : B → C)

example : A → C :=
  fun h : A => show C from h2 (h1 h)

example : A → C :=
  λ h : A => show C from h2 (h1 h) -- fun と λ は同じ．Lean4 では `assume` が使えないので，見た目一緒

example : A → C :=
  λ h : A ↦ h2 (h1 h) -- Lean4 ではカンマではなく `=>` か `↦` でつなぐ

example : A → C :=
  λ h ↦ h2 (h1 h) -- ここまで簡略化するとあとから見てわかりにくい．．．

演習04-03

-- 目標1. have
variable (A B C: Prop)

-- have は新たに証明を作る syntax
-- Lean4 では have name := proof という形式で書く
example : A ∧ B → (B ∧ A) :=
  fun h : A ∧ B => 
    have hA : A := h.left
    have hB : B := h.right
    show B ∧ A from And.intro hB hA

example : (A → B) → (B → C) → (A → C) :=
  fun hAB : A → B => 
    fun hBC : B → C =>
      fun hA : A =>
        have hB : B := hAB hA
        show C from hBC hB
-- have は示したい証明の中で補題を作るイメージで使う

レポート課題

-- 問 sorryを書き換えて，証明を完成せよ．
-- ただし、λ をつかわず，
-- また，have や show，from などを利用して
-- 証明を読みやすく工夫すること．

-- 問１
example (P Q: Prop) : P ∨ Q → Q ∨ P :=
  fun h: P ∨ Q => 
    Or.elim h
      (fun hp: P => Or.inr hp )
      (fun hq: Q => Or.inl hq)

-- 問２
example (P Q: Prop) : (P → Q) → (¬ Q → ¬ P) :=
  fun hPQ : P → Q =>
    fun hnQ : ¬ Q =>
      fun hP : P => 
        hnQ (hPQ hP)
-- 個人的にはまだ慣れていないので tactic モードを使ったほうが証明しやすい
example (P Q: Prop) : (P → Q) → (¬ Q → ¬ P) := by
  intro hPQ hnQ hP
  exact hnQ (hPQ hP)

-- 問3
example (P: Prop) : P ∨ False ↔ P := 
  Iff.intro
    (fun h : P ∨ False => 
      Or.elim h
        (fun hP : P => hP)
        (fun hF : False => False.elim hF))
    (fun h : P => Or.inl h)
-- tactic モードの別解
example (P: Prop) : P ∨ False ↔ P := by
  constructor
  · intro h 
    cases h
    case inl hP => exact hP
    case inr hF => contradiction
  · intro hP
    exact Or.inl hP
-- 問4
example (P Q R: Prop) : (P ∨ Q) ∨ R ↔ P ∨ (Q ∨ R) :=
  Iff.intro
    (fun h : (P ∨ Q) ∨ R =>
      Or.elim h
        (fun hPQ : P ∨ Q =>
          Or.elim hPQ
            (fun hP : P => Or.inl hP)
            (fun hQ : Q => Or.inr (Or.inl hQ)))
        (fun hR : R => Or.inr (Or.inr hR)))
    (fun h : P ∨ (Q ∨ R) =>
      Or.elim h
        (fun hP : P => Or.inl (Or.inl hP))
        (fun hQR : Q ∨ R =>
          Or.elim hQR
            (fun hQ : Q => Or.inl (Or.inr hQ))
            (fun hR : R => Or.inr hR)))

-- 問5
example (P Q: Prop) : ¬ (P ∨ Q) ↔ ¬ P ∧ ¬ Q :=
  Iff.intro
    (fun hNPQ : ¬ (P ∨ Q) =>
      And.intro
        (fun hP : P => show False from hNPQ (Or.inl hP))
        (fun hQ : Q => show False from hNPQ (Or.inr hQ)))
    (fun hNPNQ : ¬ P ∧ ¬ Q =>
      fun hPQ : P ∨ Q =>
        Or.elim hPQ
          (fun hP : P => show False from hNPNQ.left hP)
          (fun hQ : Q => show False from hNPNQ.right hQ))
-- tactic モードの別解
example (P Q: Prop) : ¬ (P ∨ Q) ↔ ¬ P ∧ ¬ Q := by
  constructor
  · intro hNPQ
    constructor
    · intro hP
      exact hNPQ (Or.inl hP)
    · intro hQ
      exact hNPQ (Or.inr hQ)
  · intro hNPNQ hPQ
    cases hPQ
    case inl hP => exact hNPNQ.left hP
    case inr hQ => exact hNPNQ.right hQ