Lean写経　応用情報数理学特論　第０１回

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

演習01-01

割愛 m(_ _)m

演習01-02

variable (A : Type)
variable (B C D: Type)
variable (a : A)
variable (b₁ b₂ : B)
variable (c : C)
variable (f : A → B)
variable (g : B → C)
variable (h : A → B → C → D)
variable (i : (A → B) → C → D)

#check A
#check B
#check a
#check b₁
#check f (a)
#check f a
#check g b₁ 
#check g (f a)
#check h a 
#check h a b₂ 
#check h a (f a) c
#check i a
#check i f

Lean4 だと variable 宣言時にカッコが必要．

演習01-03

-- Prop型
-- LEANの関数 And.intro, And.right, And.left
variable (A B : Prop)

#check A
#check A ∧ B
#check A ∨ B
#check (A ∧ B) ∨ A
#check ¬ A
#check A → B

variable (h₁ : A) -- 命題Aの証明の一つとしてh₁ を持っているとみなす．
variable (h₂ : A → B) -- 命題A → Bの証明の一つとしてh₂ を持っているとみなす．
variable (h₃ : A ∧ B) -- 命題A ∧ Bの証明の一つとしてh₃ を持っているとみなす．
#check h₁ 
#check h₂ h₁ -- h₂ はA → Bの証明であるから，Aの証明であるh₁ を代入することで h₂ の証明がなされた．
variable (g : A → (A → B) → B) 
#check g h₁ h₂ 

#check And.intro
#print And.intro
#check And.intro h₁
#check And.intro h₁ h₂ -- A ∧ (A → B) の証明を手に入れた
#check And.intro h₁ (h₂ h₁) -- A ∧ B の証明を手に入れた
#print And.right
#check And.right h₃ -- B の証明を手に入れた
#check h₃.right
#print And.left

Lean4 だと And の先頭は大文字．