順不同・断片的な記述となる。ネタ元は:
https://leanprover.github.io/theorem_proving_in_lean4/tactics.html#basic-tactics で出てくるタクティクを列挙。
- apply Iff.itro : 論理同値を分解する。Iff.introの逆行。
- intro h : ターゲット含意の前件を、証拠名 h でコンテキストに移す。含意導入の逆行。
- apply Or.elim (And.right h) : 式 Or.elim (And.right h) - - の適用の逆行。
- 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 -/