intro
#Fleeting_Notes
intro
含意(→)を除去するやつ
→除去規則
モーダスポネンス
Leanのintroの使い方の例
code:lean.hs
example : (P → Q) → ¬Q → ¬P := by
-- (P → Q)を仮定hPQとして切り出す
-- ゴールは⊢ ¬Q → ¬P
intro hPQ
-- ¬Qを仮定hNQとして切り出す
-- ゴールは⊢ ¬P
intro hNQ
-- Pを仮定に切り出す。¬はゴールに⊢ Falseとして残る
-- 否定命題¬PはP → Falseと定義されているのでそうなる。
intro hP
-- h2: ¬Qを⊢Falseにapplyするとゴールは⊢ Qになる
apply hNQ
-- h1: P → Qを⊢ Qにapplyするとゴールはなぜか⊢ Pになる
-- → h: P → Qのような仮定をゴールに適用すると→の左部分がゴールに置き換わる
apply hPQ
exact hP
確認用
Q. intro
メモ
intro: 含意→や全称∀を示す - Lean by Example
調査用
Google.icon intro(日)
Google.icon intro lean(日)
Google.icon intro coq(日)
Google.icon intro(英)
Google.icon intro lean(英)
Google.icon intro coq(英)