Leanのtheorem

定理の導入

内部の扱いとしてはLeanのdefと同じ

code:lean

variable {p : Prop}

variable {q : Prop}

theorem t1 : p → q → p := fun hp : p => fun hq : q => hp

https://aconite-ac.github.io/theorem_proving_in_lean4_ja/propositions_and_proofs.html#working-with-propositions-as-types-型としての命題を実践する

code:lean

theorem t1 {p q : Prop} (hp : p) (hq : q) : p := hp

#print t1 -- ∀ {p q : Prop}, p → q → p := fun {p q} hp hq => hp

これの解釈をする

{p q : Prop}はgenericsみたいなもん

任意の命題p, qに対して、と言っている

theorem t1 (hp : p) (hq : q) : pは、

hsっぽく読み解けば、p -> q -> pというシグネチャだとわかる

単純に、$ (p \to q) \to pという論理式と同じ

:=の右側が証明

hpが証明ということ

hpとhqという前提を使っていいよということで、hpを使っている

hpを返せば型が合うのでqedということになる

Leanの#printした結果が普通の論理式に近くて読みやすいmrsekut.icon

code:lean

theorem t1 (p q : Prop) (hp : p) (hq : q) : p := hp

variable (p q r s : Prop)

#check t1 p q -- p → q → p

#check t1 r s -- r → s → r

#check t1 (r → s) (s → r) -- (r → s) → (s → r) → r → s

variable (h : r → s)

#check t1 (r → s) (s → r) h -- (s → r) → r → s

かなり意味がわからない

t1は2つの引数を取る関数(?)なのに、なぜ最終行では3つを適用しているのか

そもそもt1 p qというのは関数適用ではないのか

p, qは型だし

「t1 p q」自体が「p -> q -> p」という関数になっている

依存型のわけわかんなさを感じているmrsekut.icon

theorem t2 (h₁ : q → r) (h₂ : p → q) : p → r :=を証明してみる

わかりやすく書くと、

∀ (p q r : Prop), (q → r) → (p → q) → p → rという論理式を証明したい

(q → r) → (p → q)という前提は既に得ているので、あとは

p -> から始まって、rを返すことを示せれば良い

p ->を作るために、funを使う

code:lean

theorem t2 (h₁ : q → r) (h₂ : p → q) : p → r :=

fun h₃ : p => ???

あとは、良い感じ???の部分の型がrになるように、h1,h2,h3を組み合わせれば良い

h2 : p -> qで、h3 : pなので、h2 h3 : qが得られる

これをh1 : q -> rに適用すればrが得られる

従って、こうする

code:lean

theorem t2 (h₁ : q → r) (h₂ : p → q) : p → r :=

fun h₃ : p => h₁ (h₂ h₃)