メニュー
Decision trees for choosing tactics based on goal type and proof strategy. Use when unsure which tactic to apply or planning proof approach.
Codex または Claude でインストール この Prompt をコピーして Codex、Claude、または他のアシスタントに貼り付けると、Skill ページを確認してインストールできます。
SOC 職業分類に基づく
Lean 4 fundamentals including syntax, structures, inductive types, and polymorphism. Use when writing basic Lean code, defining custom data types, pattern matching, or learning core language patterns.
Dependent types for type-safe APIs and compile-time guarantees. Use for Vect, Fin, indexed families, universes, or making illegal states unrepresentable.
Functor, Applicative, Alternative, and the abstraction hierarchy. Use when transforming values in containers, combining independent computations, or choosing abstraction level.
Monadic effect handling in Lean including Option, Except, State, Reader, and do-notation. Use when chaining computations that may fail, need state, or require environment access.
Tail recursion, array mutation, Fin, and performance patterns. Use when optimizing recursive functions, avoiding stack overflow, or working with large data.
Combining multiple effects with monad transformers including StateT, ExceptT, ReaderT, and OptionT. Use when you need error handling AND state, or multiple effects together.
| name | lean-tp-tactic-selection |
| description | Decision trees for choosing tactics based on goal type and proof strategy. Use when unsure which tactic to apply or planning proof approach. |
| allowed-tools | Read, Grep, Glob |
Decision trees for choosing the right tactic based on goal type and proof strategy. Use when unsure which tactic to apply.
Trigger terms: "which tactic", "tactic choice", "proof strategy", "how to prove", "tactic decision"
Goal type?
├─ a = b (equality)
│ ├─ Definitional equality? → rfl
│ ├─ Have proof h : a = b? → exact h
│ ├─ Need rewriting? → rw [lemmas]
│ └─ Complex chain? → calc
│
├─ p ∧ q (conjunction)
│ ├─ Have both proofs? → exact ⟨hp, hq⟩
│ └─ Need to derive each? → constructor
│
├─ p ∨ q (disjunction)
│ ├─ Have p? → left; exact hp
│ ├─ Have q? → right; exact hq
│ └─ Case split on h : p ∨ q? → cases h
│
├─ p → q (implication)
│ └─ Introduce assumption → intro hp
│
├─ ∀ x, p x (universal)
│ └─ Introduce variable → intro x
│
├─ ∃ x, p x (existential)
│ └─ Provide witness → use w
│
├─ ¬p (negation = p → False)
│ └─ Introduce and derive False → intro hp
│
├─ Inductive type
│ ├─ Single constructor? → constructor
│ ├─ Multiple constructors? → cases h
│ └─ Recursive proof? → induction h
│
├─ Contradictory hypotheses?
│ └─ contradiction
│
├─ Goal is in context?
│ └─ assumption
│
└─ Complex expression?
└─ simp / simp_all
What's your approach?
├─ Direct construction
│ └─ exact <term> / apply <lemma>
│
├─ Case analysis
│ ├─ On hypothesis h : P ∨ Q → cases h
│ └─ On decidable prop → by_cases h : P
│
├─ Induction
│ └─ induction n with | base => ... | step ih => ...
│
├─ Rewriting
│ ├─ Simple substitution → rw [h]
│ ├─ Repeated/normalized → simp
│ └─ Precise location → conv
│
├─ Backward reasoning ("suffices to show X")
│ └─ suffices h : X by use_h; prove_X
│
├─ Forward reasoning ("we have X")
│ └─ have h : X := proof
│
├─ Contradiction
│ └─ exfalso / contradiction
│
└─ Classical (excluded middle)
└─ by_cases h : P
| Situation | Tactic |
|---|---|
| Goal exactly matches hypothesis | assumption or exact h |
Goal is a = a or computes to equality | rfl |
Goal is True | trivial |
Goal is conjunction P ∧ Q | constructor |
| Goal is disjunction, have left | left |
| Goal is disjunction, have right | right |
| Goal is implication/universal | intro |
| Goal is existential | use witness |
| Have equality, need to substitute | rw [h] |
| Complex arithmetic | omega |
| Decidable by computation | decide |
| Need to case split | cases h |
| Need induction | induction n |
| Hypotheses contradict | contradiction |
| Simplify with lemmas | simp [lemmas] |
| Use | When |
|---|---|
rw [h] | Single specific rewrite, leftmost match |
rw [← h] | Rewrite right-to-left |
simp | Apply all @[simp] lemmas to simplify |
simp [h] | Include h as additional simp lemma |
simp only [h] | Use ONLY specified lemmas |
conv => ... | Precise control over WHERE to rewrite |
"unknown identifier": Hypothesis name typo or not in scope "type mismatch": Term doesn't match goal type "tactic 'assumption' failed": No matching hypothesis "goals remain": Forgot to prove all cases
lean-tp-tactics - Detailed tactic referencelean-tp-propositions - Logical connectiveslean-tp-foundations - Type theorySource: Theorem Proving in Lean 4