Tactic Suggestion Assistant

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