Skills-4-SE tactic-suggestion-assistant

Analyze proof states in Isabelle or Coq and suggest applicable tactics to make progress. Use when users need help with: (1) Choosing the next tactic in an interactive proof, (2) Understanding what tactics apply to their current goal, (3) Getting unstuck in a proof, (4) Learning which tactics work for specific goal structures (conjunctions, implications, induction, etc.). Provides 3-5 ranked tactic suggestions with explanations for intermediate-level proofs in both Isabelle/Isar and Coq.

install

source · Clone the upstream repo

git clone https://github.com/ArabelaTso/Skills-4-SE

Claude Code · Install into ~/.claude/skills/

T=$(mktemp -d) && git clone --depth=1 https://github.com/ArabelaTso/Skills-4-SE "$T" && mkdir -p ~/.claude/skills && cp -r "$T/skills/tactic-suggestion-assistant" ~/.claude/skills/arabelatso-skills-4-se-tactic-suggestion-assistant && rm -rf "$T"

manifest: skills/tactic-suggestion-assistant/SKILL.md

source content

Tactic Suggestion Assistant

Analyze proof states and suggest applicable tactics to make progress in Isabelle or Coq.

Overview

This skill helps you navigate interactive proofs by analyzing the current proof state and suggesting 3-5 ranked tactics that can make progress. It works with both Isabelle/Isar and Coq, providing system-specific suggestions with explanations.

How to Use

Provide the current proof state including:

System: Isabelle or Coq
Goal: The current goal to prove
Context: Available hypotheses/assumptions (if any)
Variables: Types of variables involved (optional but helpful)

The assistant will analyze the state and suggest tactics ranked by likelihood of success.

Analysis Process

Step 1: Identify the Proof System

Determine whether you're working in Isabelle or Coq based on syntax:

Isabelle: Uses
```
⟹
```
,
```
∧
```
,
```
∨
```
,
```
∀
```
,
```
∃
```
,
```
'a list
```
, etc.
Coq: Uses
```
->
```
,
```
/\
```
,
```
\/
```
,
```
forall
```
,
```
exists
```
,
```
list A
```
, etc.

Step 2: Analyze Goal Structure

Examine the goal's logical form:

Conjunction:
```
P ∧ Q
```
/
```
P /\ Q
```
→ Split tactics
Implication:
```
P ⟹ Q
```
/
```
P -> Q
```
→ Introduction tactics
Quantification:
```
∀x. P
```
/
```
forall x, P
```
→ Variable introduction
Equality:
```
t1 = t2
```
→ Simplification or rewriting
Inductive types: Lists, nat, trees → Induction or case analysis

Step 3: Examine Context

Look at available hypotheses:

Equations: Can be used for rewriting
Inductive predicates: Can be inverted or used directly
Conjunctions: Can be decomposed
Disjunctions: Require case analysis

Step 4: Consider Variable Types

Type information guides tactic choice:

Lists: Suggest induction or case analysis (empty vs cons)
Natural numbers: Suggest induction or case analysis (0 vs successor)
Options: Suggest case analysis (None vs Some)
Custom types: Suggest structural induction

Step 5: Rank Suggestions

Provide 3-5 tactics ranked by:

Structural match with goal
Simplicity and directness
Automation potential
Common proof patterns
Context support

Suggestion Format

For each suggested tactic, provide:

Tactic: The exact tactic syntax
Rationale: Why this tactic applies
Effect: What happens after applying it
Likelihood: High/Medium/Low

Example: Isabelle Proof State

Proof state:

goal (1 subgoal):
 1. ⋀xs ys. length xs = length ys ⟹ length (xs @ ys) = 2 * length xs

Analysis:

Goal: Implication with equality
Hypothesis:
```
length xs = length ys
```
Variables: Lists
```
xs
```
and
```
ys
```

Suggestions:

```
by simp
```
(High likelihood)
- Rationale: Goal is an arithmetic equality that simplification can handle
- Effect: Simplifies
```
length (xs @ ys)
```
  to
```
length xs + length ys
```
  , then uses hypothesis
- Try this first for simple arithmetic goals
```
apply (subst length_append)
```
(Medium likelihood)
- Rationale: Explicitly unfold the append length property
- Effect: Rewrites
```
length (xs @ ys)
```
  to
```
length xs + length ys
```
- More explicit than simp, useful if simp fails
```
using assms by auto
```
(Medium likelihood)
- Rationale: Use assumptions with automation
- Effect: Combines hypothesis with automatic reasoning
- Good fallback if simp doesn't work

Example: Coq Proof State

Proof state:

1 subgoal
n : nat
IHn : even n -> even (n + 2)
============================
even n -> even (S (S n))

Analysis:

Goal: Implication
Hypothesis: Induction hypothesis
```
IHn
```
Variables: Natural number
```
n
```
Context: In an induction proof

Suggestions:

```
intro H.
```
(High likelihood)
- Rationale: Goal is an implication, introduce the hypothesis
- Effect: Adds
```
H: even n
```
  to context, goal becomes
```
even (S (S n))
```
- Standard first step for implications
```
intros. simpl. apply IHn. assumption.
```
(High likelihood)
- Rationale: Complete proof chain using IH
- Effect: Introduces hypothesis, simplifies, applies IH, solves with assumption
- Direct solution if
```
S (S n)
```
  simplifies to
```
n + 2
```
```
intro H. rewrite <- plus_n_Sm. rewrite <- plus_n_O. apply IHn. exact H.
```
(Medium likelihood)
- Rationale: Rewrite to match IH form
- Effect: Converts
```
S (S n)
```
  to
```
n + 2
```
  form to use IH
- Needed if simplification doesn't automatically match
```
auto.
```
(Low likelihood)
- Rationale: Try automation
- Effect: May solve if proof is straightforward
- Worth trying but may not have enough hints

Common Situations

Situation: Conjunction Goal

Isabelle:

⊢ P ∧ Q

```
apply (rule conjI)
```
- Split into two goals
```
by auto
```
- If both parts are trivial
```
by simp
```
- If simplification proves both

Coq:

P /\ Q

```
split.
```
- Split into two goals
```
auto.
```
- If both parts are trivial
```
intuition.
```
- Propositional reasoning

Situation: Need Induction

Indicators: Goal about all elements of a list/nat, recursive structure

Isabelle:

```
proof (induction xs)
```
- List induction
```
proof (induction n)
```
- Nat induction
```
proof (induction t)
```
- Custom type induction

Coq:

```
induction l as [|x l' IH].
```
- List induction
```
induction n as [|n' IH].
```
- Nat induction
```
induction t.
```
- Custom type induction

Situation: Case Analysis Needed

Indicators: Goal or hypothesis with conditional, pattern match

Isabelle:

```
proof (cases xs)
```
- Case analysis on variable
```
proof (cases "condition")
```
- Case split on boolean
```
by (auto split: if_split)
```
- Auto with case split

Coq:

```
destruct l as [|x l'].
```
- Case analysis on variable
```
destruct (condition).
```
- Case split on boolean
```
case_eq term.
```
- Case analysis with equation

Situation: Arithmetic Goal

Indicators: Goal with +, -, *, <, ≤

Isabelle:

```
by arith
```
- Arithmetic decision procedure
```
by linarith
```
- Linear arithmetic
```
by simp
```
- Simplification

Coq:

```
lia.
```
- Linear integer arithmetic
```
nia.
```
- Non-linear arithmetic
```
ring.
```
- Ring solver

Situation: Stuck on Complex Goal

Indicators: Many connectives, nested structure

Isabelle:

```
by auto
```
- Full automation
```
by fastforce
```
- Aggressive automation
```
sledgehammer
```
- External provers

Coq:

```
auto.
```
- Automation
```
intuition.
```
- Propositional reasoning
```
firstorder.
```
- First-order reasoning
```
tauto.
```
- Tautology solver

References

Detailed tactic references and patterns:

isabelle_tactics.md: Complete Isabelle/Isar tactic reference
coq_tactics.md: Complete Coq tactic reference
proof_patterns.md: Detailed proof state analysis patterns

Load these references when you need:

Complete tactic syntax and options
Advanced tactic usage
Detailed pattern matching rules
Tactic combinators and composition

Tips for Effective Suggestions

Start simple: Suggest automation (
```
auto
```
,
```
simp
```
) before manual tactics
Match structure: Prioritize tactics that directly match the goal form
Consider context: Use available hypotheses in suggestions
Explain effects: Clearly state what happens after applying the tactic
Provide alternatives: Offer 3-5 options ranked by likelihood
Be specific: Give exact syntax, not just tactic names
Learn from failures: If a suggested tactic fails, analyze why and suggest alternatives