intro

intro

例:

ゴールが A → B のとき、Aを仮定に加えて Bを示すゴールに変換

例: ⊢ A → B ==> h : A ⊢ B

∀導入

ゴールが ∀ x, P x のとき、任意のxをローカルコンテキストに導入して P x を示すゴールに変換

例:

code:lean

example : ∀ n : Nat, n + 0 = n := by

intro n

-- 変換前: ⊢ ∀ n : Nat, n + 0 = n

-- 変換後: n : Nat ⊢ n + 0 = n

rfl

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として残る

intro hP

-- h2: ¬Qを⊢Falseにapplyするとゴールは⊢ Qになる

apply hNQ

-- h1: P → Qを⊢ Qにapplyするとゴールはなぜか⊢ Pになる

apply hPQ

exact hP

確認用

Q. intro

メモ

調査用