演習問題¶

この章の演習では，まず証明図や自然言語の証明を考えてから Lean の tactic に翻訳してください． constructor，cases，intro，exact，False.elim，rw を意識して使います．

連言の可換性を証明してください．

example (P Q : Prop) : P ∧ Q → Q ∧ P := by
  -- `intro h` のあと，`constructor` と `h.left`, `h.right` を使う．
  sorry

選言の可換性を証明してください．

example (P Q : Prop) : P ∨ Q → Q ∨ P := by
  -- `cases` で場合分けする．
  sorry

modus ponens を Lean で書いてください．

example (P Q : Prop) (hPQ : P → Q) (hP : P) : Q := by
  -- 関数適用として読む．
  sorry

False から任意の命題が従うことを証明してください．

example (P : Prop) (h : False) : P := by
  -- `False.elim h`
  sorry

全称命題を使って具体的な元に関する結論を得てください．

example (α : Type) (P Q : α → Prop)
    (h : ∀ x : α, P x → Q x) (a : α) (ha : P a) : Q a := by
  -- `h a ha`
  sorry

存在命題から証拠を取り出し，同じ証拠で別の存在命題を作ってください．

example (α : Type) (P Q : α → Prop)
    (h : ∃ x : α, P x) (hpq : ∀ x, P x → Q x) :
    ∃ x : α, Q x := by
  -- `cases h with | intro x hx => ...`
  sorry

等式を使って命題を書き換えてください．

example (α : Type) (P : α → Prop) (a b : α)
    (hab : a = b) (ha : P a) : P b := by
  -- `hab ▸ ha`
  sorry

証明図を自分で書いてから，次の Lean 証明を完成させてください．

example (P Q R : Prop) (h₁ : P → Q) (h₂ : Q → R) : P → R := by
  -- `intro hP`
  sorry