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

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

演習09-01

/- 目標１．
 set    set
 ⊆      \subseteq
 ∈      \in
 ∪      \u
 ∩      \i
 \      \ 
 ∅      \empty
-/ 
import Mathlib.Tactic
-- 目標２． False.elim (h : x ∈ (∅ : set U))
variable {U : Type} -- このあと引数が柔軟にとれるように，中括弧にしておく
variable (A B : Set U) -- U を母集合とする部分集合 A, B
variable (x : U)
#check x ∈ A -- x が A に含まれるかという命題
#check x ∈ ∅ -- x が ∅ に含まれるかという命題
variable (h : x ∈ (∅ : Set U)) -- 母集合 U の部分集合としての空集合 ∅ に含まれるという仮定 Falseとなる命題
#check False.elim h
#print False.elim -- Falseになる命題からなんでも証明できる

演習09-02

/- 目標１．x ∈ A ∪ B
          ↔ x ∈ A ∨ x ∈ B -/
/- 目標２．x ∈ A ∩ B
          ↔ x ∈ A ∧ x ∈ B -/
import Mathlib.Tactic
variable {U : Type} -- このあと引数が柔軟にとれるように，中括弧にしておく
variable (A B : Set U) -- U を母集合とする部分集合 A, B

example (x : U) : x ∈ A → x ∈ A ∪ B := by
  intro (h : x ∈ A)
  apply Or.inl h
  -- left
  -- assumption でも証明可能

example (x : U) : x ∈ A → x ∈ B → x ∈ A ∩ B := by
  intro hA hB
  apply And.intro hA hB

example (x : U) : x ∈ A ∩ B → x ∈ B ∩ A := by
  intro h
  apply And.intro h.right h.left

演習09-03

/- 目標１．x ∈ A ⊆ B
          ↔ x : U → x ∈ A → x ∈ B -/
/- 目標２．∅ : Set U -/
/- 目標３．(x : U) ∈ (∅ : Set U) ...  False -/

import Mathlib.Tactic
variable {U : Type} -- このあと引数が柔軟にとれるように，中括弧にしておく
variable (A B : Set U) -- U を母集合とする部分集合 A, B

example : A ⊆ A ∪ B := by
  intro x h
  apply Or.inl h

example : ∅ ⊆ A := by
  intro x (h : x ∈ ∅) -- Lean4 だと (∅ : Set U) と書かなくてもよい
  apply False.elim h

演習09-04

-- 目標１．import Data.Set
-- 目標２．open set
-- 目標３．#check @
/- 目標４．
  mem_inter               : x ∈ a → x ∈ b → a ∩ b
  mem_of_mem_inter_left   : x ∈ a ∩ b → x ∈ a
  mem_of_mem_inter_right  : x ∈ a ∩ b → x ∈ b
  mem_union_left          : x ∈ a → x ∈ a ∪ b
  mem_union_right         : x ∈ b → x ∈ a ∪ b
  mem_or_mem_of_mem_union : x ∈ a ∪ b → x ∈ a ∨ x ∈ b
  not_mem_empty           : x ∉ ∅ ... x ∈ ∅ → False
  ∉                       : ∉
-/
import Mathlib.Tactic -- Lean4だとだいたいこれで色々使えるようになる（適当．．．）
#check Set.mem_inter
open Set -- メソッドを global scopeに持ちあげる
#check mem_inter
#check @mem_inter -- @をつけると見やすくなる．
variable {U : Type}
variable (x : U)
variable (h1 : x ∈ (∅ : Set U))
variable (h2 : x ∉ (∅ : Set U))
#check h2 h1 -- これは矛盾．False が返る．

演習09-05

/- 目標１．ext              : (∀ (x : α), x ∈ a ↔ x ∈ b) → a = b 外延性公理
  eq_of_subset_of_subset   : a ⊆ b → b ⊆ a → a = b
-/
-- 目標２．Classical.em    : ∀ (p : Prop), p ∨ ¬p  排中律
/- 目標３．univ
          subset_univ      : (a : Set α), a ⊆ univ どんな集合も全体集合(univ)の部分集合
-/
-- 目標４．x ∈ univ         : trivial
import Mathlib.Tactic -- Lean4だとだいたいこれで色々使えるようになる（適当．．．）
open Set -- メソッドを global scopeに持ちあげる
variable {U : Type}
variable (A B C : Set U)

example : univ = A ∪ (A.compl) := by -- -A でエラーが出たので A.compl に変更
  apply eq_of_subset_of_subset -- 他方が他方の部分集合であることを示す．
  ( intro x hu
    apply Classical.em (x ∈ A)
  )
  ( apply subset_univ )

#check @subset_univ

example : A ⊆ univ := by
  intro x h
  trivial
  -- apply subset_univ でも証明可能