Lean どのタクティク使えばええねんメモ
ゴールが？を適用するか仮定が？を適用するかは、場合による
ゴールが？
含意 P → Q
intro タクティク
否定 ￢ P
intro タクティク
否定は P → False
同値性 ↔
constructor タクティク
mp と mpr に分解
論理積 ∧
constructor タクティク
left と right に分解
論理和 ∨
left タクティク
right タクティク
全称量化 ∀
intro タクティク
存在量化 ∃
exists タクティク
仮定が？
h : P
exact h
終わり
h : Q → P
apply h
ゴールが P のときゴールが Q になる
h : ￢Q
h' : Q もあれば contradiction
終わり
h : Q ↔ P
rw [h]
ゴールが Q になる
h : P ↔ Q
rw [←h]
ゴールが Q になる
h : Q ∧ R
仮定として h.left : Q が使える
仮定として h.right : R が使える
h : Q ∨ R
cases h
inl の場合では仮定として Q が使える
inr の場合では仮定として R が使える
h : ∀x, P x
h a : P a
h : ∃x, P x
obtain ⟨y, hy⟩ := h
適切なタイミングで使うやつ
exfalso
ゴールを False にする
なぜなら爆発律でなんでも言える
by_cases
P ∨ ￢P が仮定として得られる
古典論理になる