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

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

演習02-01

-- 目標１．example
-- 目標２．show, from
variable (A B : Prop) 
variable (h : A ∧ B)

-- example : 証明を与えられる命題 := 証明の具体例
example : A := And.left h -- A の証明を与えているイメージ
example : B := h.right -- B の証明を与えているイメージ

example : B ∧ A := And.intro (h.right) (h.left)

example : B ∧ A :=
  And.intro 
    (h.right) -- B の証明を与えているイメージ
    (h.left) -- A の証明を与えているイメージ

example : B ∧ A :=
  And.intro 
    (show B from h.right) -- show B により，Bの証明を与えていることが明示される
    (show A from h.left)  -- show A により，Aの証明が見やすくなる．

演習02-02

-- 目標１．assume
-- Lean4 では、`assume` は使えないので，`fun` で代用する．
variable (A B : Prop)

example : A → A :=
  fun h : A => h

example : A → A ∧ A :=
  fun h : A => And.intro h h

example : A → (A → B) → B :=
  fun h1 : A => fun h2 : A → B => h2 (h1)

example : A ∧ ¬ B → ¬ B ∧ A :=
  fun h : A ∧ ¬ B => And.intro 
    (show ¬ B from h.right)
    (show A from h.left) 

演習02-03

-- 目標１．example (...) :
-- example とコロンの間に変数の宣言を書く書き方
variable (A : Prop)

example (B : Prop) : A ∧ B → A :=
  fun (h : A ∧ B) => h.left

example (B : Prop) (h : A ∧ B) : A :=
  -- (h : A ∧ B) が仮定として定義されているので直接証明できる．
  h.left

example (B C : Prop) : B → (B → C) → C :=
  fun (b : B) (f : B → C) => f b

-- この書き方に準じることで example で閉じて証明を書くことができる

演習02-04

-- 目標１．assume
  -- Lean4 には `assume` がないので，`fun` で代用する．
-- 目標２．sorry
-- 目標３．_
variable (A B : Prop)

example : A ∧ B → A :=
  fun h : A ∧ B => And.left h

example : A ∧ B → A :=
  fun h => And.left h
  -- h が A ∧ B の証明であることを自動で認識する．

example : A ∧ B → A :=
  fun h : A ∧ B => sorry
  -- sorry は証明を保留する．

example : A ∧ B → B ∧ A :=
  fun h : A ∧ B => _
  -- placeholder`_`を書くと，今書くべき証明の型が表示される．

example : A ∧ B → B ∧ A :=
  fun h : A ∧ B => And.intro (_) (_)
  -- 今書くべき証明の型が表示されるので，それに合わせて証明を書く．