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

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

演習05-01

-- 目標１． def
def mpPropDef (A B : Prop) : Prop :=
  A → (A → B) → B 
-- 命題が定義されている

def mpProofDef (A B : Prop) : A → (A → B) → B := by
  intro (a : A)
  intro (f : A → B)
  exact f a
-- 命題の証明が定義されている

-- example と異なり，名前をつけることができる．

#check mpPropDef
#check mpProofDef

variable (X Y : Prop)
#check mpPropDef (X → ¬ Y) Y

variable (h₁ : X → ¬ Y)
variable (h₂ : (X → ¬ Y) → Y)

#check mpProofDef (X → ¬ Y) Y
-- h₁, h₂ の証明がほしい状態

#check mpProofDef (X → ¬ Y) Y h₁ h₂
-- Y の証明であることを示している．

-- 汎用的な証明の方法を関数として定義しておくことで，証明の再利用ができる．

演習05-02

-- 目標１．{}
def mpProofDef (A B : Prop) : A → (A → B) → B :=
  fun (a : A) (f : A → B) => f a

def mpProofDef2 {A B : Prop} : A → (A → B) → B :=
  fun (a : A) (f : A → B) => f a
-- 引数が{}で囲まれているときは，型推論が効く

variable (X Y : Prop)
variable (h₁ : X → ¬ Y)
variable (h₂ : (X  → ¬ Y) → Y)

#check mpProofDef (X → ¬ Y) Y h₁ h₂
#check mpProofDef2 h₁ h₂
-- A, B にあたる引数を入れなくてもよい
-- 証明だけ，証明の型も省略できる

演習05-03

-- 目標１．theorem, lemma
def mpProofDef (A B : Prop) : A → (A → B) → B := 
  fun (a : A) (f : A → B) => f a

theorem mpProofThm (A B : Prop) : A → (A → B) → B := 
  fun (a : A) (f : A → B) => f a

variable (X Y : Prop)
variable (h₁ : X → ¬ Y)
variable (h₂ : (X → ¬ Y) → Y)

#check mpProofThm (X → ¬ Y) Y h₁ h₂
-- Def と Thm は同じ扱い

-- 下記はエラーになる．Lean4では lemma は使えない？
-- lemma mpProofLem (A B : Prop) : A → (A → B) → B := 
--   fun (a : A) (f : A → B) => f a

演習05-04

-- 目標１．theoremの応用
theorem syllog {A B C : Prop} : (A → B) → (B → C) → (A → C) :=
  fun (f : A → B) (g : B → C) (a : A) => g (f a)

variable (Human Animal Dog : Prop)

example (ha : Human → Animal) (ad : Animal → Dog) : 
  Human → Dog :=
  syllog ha ad
-- 一度作ったtheoremは使い回せる

example (ha : Human → Animal → Human ∨ Animal) 
        (had : (Animal → Human ∨ Animal) → Dog ∧ Human) : 
  Human → Dog ∧ Human :=
  syllog ha had