intro
intro
は数学で慣習的に行われる
P → Q
を示すときに最初にP
を仮定する∀ x ∈ A, P(x)
を示すときに最初にx ∈ A
が与えられたと仮定する
といった導入(introduction)を行います。
具体的には、intro
は
- ゴールが
⊢ P → Q
という形であるときにP
をローカルコンテキストに追加して、ゴールを⊢ Q
に変える - ゴールが
⊢ ∀ x, P x
という形であるときにx
をローカルコンテキストに追加してゴールを⊢ P x
に変える
といった挙動をします。
variable (P Q R : Prop)
example (hPQ: P → Q) (hQR: Q → R) : P → R := by
-- 示したいことが `P → R` なので、`P` だと仮定する
intro hP
-- 仮定 `hPQ : P → Q` と `hP : P` から `Q` が導かれる
have hQ : Q := hPQ hP
-- 仮定 `hQR : Q → R` と `hQ : Q` から `R` が導かれる
exact hQR hQ
特定の形の命題に対しての使用法
A ∧ B → C
前提が論理積の形をしていた場合、無名コンストラクタで仮定を分解することができます。
example {S : Prop} (hPR : P → R) (hQR : Q → S) : P ∧ Q → R ∧ S := by
-- `P ∧ Q` だと仮定する
intro ⟨hP, hQ⟩
constructor
. exact hPR hP
. exact hQR hQ
A ∨ B → C
前提が論理和の形をしていた場合、次のように分解することができます。
example (hPR : P → R) (hQR : Q → R) : P ∨ Q → R := by
intro
-- `P` が成り立つとする
| Or.inl hP =>
exact hPR hP
-- `Q` が成り立つとする
| Or.inr hQ =>
exact hQR hQ
rcases
を使って分解することも一般的です。
example (hPR : P → R) (hQR : Q → R) : P ∨ Q → R := by
intro h
rcases h with hP | hQ
-- `P` が成り立つとする
case inl =>
exact hPR hP
-- `Q` が成り立つとする
case inr =>
exact hQR hQ
また、rintro
を使うと上記の intro
と rcases
の組み合わせを同時に行うことができます。
example (hPR : P → R) (hQR : Q → R) : P ∨ Q → R := by
rintro (hP | hQ)
-- `P` が成り立つとする
case inl =>
exact hPR hP
-- `Q` が成り立つとする
case inr =>
exact hQR hQ
∀ x, P x
intro
は ∀ x, P x
という形のゴールにも使用できます。
example (P Q : Nat → Prop) (h : ∀ n, P n ↔ Q n) : ∀ y, P (y + 1) → Q (y + 1) := by
-- 任意の `y` について示すので、`intro` で `y` を導入する
-- そして `P (y + 1) → Q(y + 1)` を示したいので、`P (y + 1)` を仮定する
intro y hyP
-- `Q (y + 1)` を示せば良い
show Q (y + 1)
-- 同値を使ってゴールを書き換える
rw [← h]
-- 仮定 `P (y + 1)` より従う
assumption
否定 ¬ について
Lean では否定 ¬ P
は P → False
として定義されているので、ゴールが ¬ P
のときに intro
すると P
が仮定に追加されて、ゴールが False
に変わります。
False
は矛盾を導けば証明できます。
example (h: P → Q) : ¬Q → ¬P := by
-- 示したいことが `¬Q → ¬P` なので、`¬Q` だと仮定する
-- そうするとゴールが `¬P` になるので、
-- さらに `intro` を行って仮定 `hP : P` を導入する
intro hnQ hP
-- 矛盾を示したい
show False
-- `hP : P` と `h : P → Q` から `Q` が導かれる
have hQ : Q := h hP
-- `hQ : Q` と `hnQ : ¬Q` から矛盾が導かれる
contradiction
関数の構成
より一般的には、intro
は関数の構成に使うことができます。
intro
が全称命題 ∀ x, P x
や含意 P → Q
を統一的に扱うことができるのも、これらが Lean 内部で関数として扱われているからです。
variable {α : Type}
/-- `intro` による恒等写像の構成 -/
def f : α → α := by
intro x
exact x
example (x : α) : f x = id x := by dsimp [f]