tactic-suggestion-assistant

name

tactic-suggestion-assistant

description

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.

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:

1. System: Isabelle or Coq
2. Goal: The current goal to prove
3. Context: Available hypotheses/assumptions (if any)
4. 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:

1. Structural match with goal
2. Simplicity and directness
3. Automation potential
4. Common proof patterns
5. Context support

Suggestion Format

For each suggested tactic, provide:

1. Tactic: The exact tactic syntax
2. Rationale: Why this tactic applies
3. Effect: What happens after applying it
4. 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:

1. 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

2. 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

3. 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:

1. 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

2. 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

3. 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

4. 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

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