Leanタクティク 2

順不同・断片的な記述となる。ネタ元は：

• https://leanprover.github.io/theorem_proving_in_lean4/tactics.html

https://leanprover.github.io/theorem_proving_in_lean4/tactics.html#basic-tactics で出てくるタクティクを列挙。

1. apply Iff.itro ： 論理同値を分解する。Iff.introの逆行。
2. intro h ： ターゲット含意の前件を、証拠名 h でコンテキストに移す。含意導入の逆行。
3. apply Or.elim (And.right h) ： 式 Or.elim (And.right h) - - の適用の逆行。
4. apply Or.elim h ： 式 Or.elim h - - の逆行。順行のOr.elimをよーく理解してないと逆行は難しい。

theorem Or.elim {c : Prop} (h : Or a b) (left : a → c) (right : b → c) : c :=
  match h with
  | Or.inl h => left h
  | Or.inr h => right h

説明：

• 第一明示引数 (h : Or a b) ： Or命題に至る証明、inl, inrという証明値コフィールド〈選択肢〉を持つコタプル構造〈コレコード〉h : a または h: b のどちらかとなる。
• 第二明示引数 (left : a → c) ： aからcへの証明
• 第三明示引数 (right : b → c) ： bからcへの証明
• ターゲット〈戻り型〉 c ： 共通の結論型

    /-
    case mp
    p q r : Prop
    h : p ∧ (q ∨ r)
    ⊢ p ∧ q ∨ p ∧ r
    -/
    apply Or.elim (And.right h) -- p → p∨r
    /-
    case mp.left
    p q r : Prop
    h : p ∧ (q ∨ r)
    ⊢ q → p ∧ q ∨ p ∧ r
    
    case mp.right
    p q r : Prop
    h : p ∧ (q ∨ r)
    ⊢ r → p ∧ q ∨ p ∧ r
    -/