2487 Proof Patterns 877a5e99

# Proof State Analysis Patterns

Guide for analyzing proof states and suggesting appropriate tactics.

## Analysis Framework

When analyzing a proof state, examine:

1. **Goal structure**: What logical form does the goal have?
2. **Available hypotheses**: What facts are in the context?
3. **Variable types**: What are we working with (nat, list, custom types)?
4. **Recursion opportunities**: Can we apply induction or case analysis?
5. **Simplification potential**: Can computation or rewriting help?

## Pattern Matching by Goal Structure

### Goal: Conjunction `P ∧ Q` (Isabelle) / `P /\ Q` (Coq)

**Analysis**: Need to prove both parts separately.

**Isabelle suggestions**:
1. `apply (rule conjI)` - Split into two subgoals
2. `by auto` - If both parts are trivial
3. `by simp` - If simplification proves both

**Coq suggestions**:
1. `split.` - Split into two subgoals
2. `auto.` - If both parts are trivial
3. `intuition.` - Propositional reasoning

### Goal: Implication `P ⟹ Q` (Isabelle) / `P -> Q` (Coq)

**Analysis**: Assume P and prove Q.

**Isabelle suggestions**:
1. `apply (rule impI)` - Move P to assumptions
2. `proof -` then `assume "P"` - Structured proof
3. `by auto` - If Q follows from P automatically

**Coq suggestions**:
1. `intro H.` - Introduce hypothesis H: P
2. `intros.` - Introduce all implications
3. `auto.` - If Q follows automatically

### Goal: Universal Quantification `∀x. P x` (Isabelle) / `forall x, P x` (Coq)

**Analysis**: Prove for arbitrary x.

**Isabelle suggestions**:
1. `apply (rule allI)` - Introduce arbitrary x
2. `proof -` then `fix x` - Structured proof
3. `by auto` - If automation handles it

**Coq suggestions**:
1. `intro x.` - Introduce arbitrary x
2. `intros.` - Introduce all quantifiers
3. `auto.` - If automation handles it

### Goal: Existential Quantification `∃x. P x` (Isabelle) / `exists x, P x` (Coq)

**Analysis**: Need to provide a witness.

**Isabelle suggestions**:
1. `apply (rule exI[where x="witness"])` - Provide witness
2. `by auto` - If witness can be found automatically
3. `by force` - Aggressive search for witness

**Coq suggestions**:
1. `exists witness.` - Provide witness
2. `eauto.` - Search for witness automatically
3. `firstorder.` - First-order reasoning

### Goal: Disjunction `P ∨ Q` (Isabelle) / `P \/ Q` (Coq)

**Analysis**: Choose which side to prove.

**Isabelle suggestions**:
1. `apply (rule disjI1)` - Prove left side (P)
2. `apply (rule disjI2)` - Prove right side (Q)
3. `by auto` - If automation can choose

**Coq suggestions**:
1. `left.` - Prove left side (P)
2. `right.` - Prove right side (Q)
3. `auto.` - If automation can choose

### Goal: Equality `t1 = t2`

**Analysis**: Can we compute, rewrite, or simplify?

**Isabelle suggestions**:
1. `by simp` - Simplification
2. `by (simp add: defs)` - Unfold definitions
3. `apply (subst rule)` - Rewrite with equation
4. `by auto` - Automatic reasoning

**Coq suggestions**:
1. `reflexivity.` - If equal by computation
2. `simpl. reflexivity.` - Simplify then check
3. `rewrite H. reflexivity.` - Rewrite with hypothesis
4. `auto.` - Automatic reasoning

### Goal: Negation `¬P` (Isabelle) / `~ P` (Coq)

**Analysis**: Assume P and derive contradiction.

**Isabelle suggestions**:
1. `apply (rule notI)` - Introduce P, prove False
2. `by contradiction` - Derive contradiction
3. `by auto` - If contradiction is obvious

**Coq suggestions**:
1. `intro H.` - Introduce hypothesis H: P
2. `contradiction.` - Derive contradiction
3. `auto.` - If contradiction is obvious

## Pattern Matching by Variable Types

### Working with Lists

**Indicators**: Variables of type `'a list` (Isabelle) or `list A` (Coq)

**Isabelle suggestions**:
1. `proof (induction xs)` - List induction
2. `proof (cases xs)` - Case analysis (empty vs cons)
3. `by (simp add: list_rules)` - Simplify with list lemmas

**Coq suggestions**:
1. `induction l as [|x l' IH].` - List induction
2. `destruct l as [|x l'].` - Case analysis
3. `simpl. auto.` - Simplify and auto

### Working with Natural Numbers

**Indicators**: Variables of type `nat`

**Isabelle suggestions**:
1. `proof (induction n)` - Natural number induction
2. `proof (cases n)` - Case analysis (0 vs Suc)
3. `by arith` - Arithmetic decision procedure

**Coq suggestions**:
1. `induction n as [|n' IH].` - Natural number induction
2. `destruct n as [|n'].` - Case analysis
3. `lia.` - Linear arithmetic solver

### Working with Options

**Indicators**: Variables of type `'a option` (Isabelle) or `option A` (Coq)

**Isabelle suggestions**:
1. `proof (cases opt)` - Case analysis (None vs Some)
2. `by (auto split: option.split)` - Auto with case split

**Coq suggestions**:
1. `destruct opt as [x|].` - Case analysis
2. `destruct opt eqn:E.` - Case analysis with equation

### Working with Custom Datatypes

**Indicators**: Variables of custom inductive types (trees, etc.)

**Isabelle suggestions**:
1. `proof (induction t)` - Structural induction
2. `proof (cases t)` - Case analysis on constructors
3. `by (auto split: datatype.split)` - Auto with splits

**Coq suggestions**:
1. `induction t.` - Structural induction
2. `destruct t.` - Case analysis on constructors
3. `auto.` - Automatic reasoning

## Pattern Matching by Hypotheses

### Hypothesis: Conjunction `H: P ∧ Q` (Isabelle) / `H: P /\ Q` (Coq)

**Analysis**: Can extract both parts.

**Isabelle suggestions**:
1. `from H have "P" and "Q" by simp_all` - Extract both
2. `using H by simp` - Use directly

**Coq suggestions**:
1. `destruct H as [HP HQ].` - Extract both parts
2. `apply H.` - Use directly if applicable

### Hypothesis: Disjunction `H: P ∨ Q` (Isabelle) / `H: P \/ Q` (Coq)

**Analysis**: Need case analysis.

**Isabelle suggestions**:
1. `proof (cases rule: H)` - Case analysis on H
2. `using H by auto` - Let automation handle

**Coq suggestions**:
1. `destruct H as [HP|HQ].` - Case analysis
2. `intuition.` - Let automation handle

### Hypothesis: Existential `H: ∃x. P x` (Isabelle) / `H: exists x, P x` (Coq)

**Analysis**: Extract witness.

**Isabelle suggestions**:
1. `from H obtain x where "P x" by auto` - Extract witness
2. `using H by auto` - Use directly

**Coq suggestions**:
1. `destruct H as [x HP].` - Extract witness
2. `apply H.` - Use directly if applicable

### Hypothesis: Equation `H: t1 = t2`

**Analysis**: Can rewrite with it.

**Isabelle suggestions**:
1. `using H by simp` - Simplify with equation
2. `apply (subst H)` - Substitute in goal
3. `from H show ?thesis` - Use directly

**Coq suggestions**:
1. `rewrite H.` - Rewrite in goal
2. `rewrite H in *.` - Rewrite everywhere
3. `subst.` - Substitute all equations

### Hypothesis: Inductive Predicate

**Analysis**: Can invert to get structure.

**Isabelle suggestions**:
1. `from H show ?thesis by (cases H)` - Case analysis
2. `using H by auto` - Use directly

**Coq suggestions**:
1. `inversion H.` - Invert the predicate
2. `inversion H; subst.` - Invert and substitute
3. `apply H.` - Use directly if applicable

## Situation-Based Suggestions

### Situation: Stuck on Complex Goal

**Indicators**: Goal has many connectives, nested structure

**Isabelle suggestions**:
1. `by auto` - Try full automation
2. `by fastforce` - Aggressive automation
3. `by (auto intro: rules)` - Auto with hints
4. `sledgehammer` - Invoke external provers

**Coq suggestions**:
1. `auto.` - Try automation
2. `intuition.` - Propositional reasoning
3. `firstorder.` - First-order reasoning
4. `tauto.` - Tautology solver

### Situation: Need Intermediate Lemma

**Indicators**: Direct proof seems difficult, need stepping stone

**Isabelle suggestions**:
1. `have "intermediate_fact" by method` - Prove intermediate
2. `from assms have "fact" by method` - Derive from assumptions

**Coq suggestions**:
1. `assert (H: intermediate_fact).` - State intermediate
2. `pose proof (lemma args) as H.` - Use existing lemma

### Situation: Induction Hypothesis Not Strong Enough

**Indicators**: IH doesn't apply, need generalization

**Isabelle suggestions**:
1. `proof (induction xs arbitrary: ys)` - Generalize variables
2. Restart with stronger statement

**Coq suggestions**:
1. `generalize dependent y.` - Generalize before induction
2. `revert y.` - Move variable back to goal
3. Restart with stronger statement

### Situation: Case Analysis Needed

**Indicators**: Goal or hypothesis has conditional, pattern match

**Isabelle suggestions**:
1. `proof (cases "condition")` - Case split on condition
2. `by (auto split: if_split)` - Auto with if-split
3. `proof (cases var)` - Case analysis on variable

**Coq suggestions**:
1. `destruct (condition).` - Case split
2. `destruct var.` - Case analysis on variable
3. `case_eq term.` - Case analysis with equation

### Situation: Arithmetic Goal

**Indicators**: Goal involves +, -, *, <, ≤, etc.

**Isabelle suggestions**:
1. `by arith` - Arithmetic decision procedure
2. `by linarith` - Linear arithmetic
3. `by simp` - Simplification may suffice

**Coq suggestions**:
1. `lia.` - Linear integer arithmetic
2. `nia.` - Non-linear arithmetic
3. `ring.` - Ring solver

### Situation: Equality with Constructors

**Indicators**: Hypothesis like `Cons x xs = Cons y ys` or `S n = S m`

**Isabelle suggestions**:
1. `by simp` - Simplification extracts equalities
2. `by auto` - Automatic reasoning

**Coq suggestions**:
1. `injection H.` - Extract equalities
2. `injection H as H1 H2.` - Extract and name
3. `inversion H; subst.` - Invert and substitute

### Situation: Impossible Equality

**Indicators**: Hypothesis like `[] = x :: xs` or `0 = S n`

**Isabelle suggestions**:
1. `by simp` - Simplification derives contradiction
2. `by auto` - Automatic reasoning

**Coq suggestions**:
1. `discriminate.` - Derive contradiction
2. `discriminate H.` - Use specific hypothesis
3. `inversion H.` - Invert (also finds contradiction)

## Ranking Tactics by Likelihood

When multiple tactics apply, rank by:

1. **Structural match**: Does the tactic directly match the goal form?
2. **Simplicity**: Simpler tactics before complex ones
3. **Automation potential**: Can automation solve it?
4. **Common patterns**: Is this a standard proof pattern?
5. **Context fit**: Do hypotheses support this approach?

**Example ranking for goal `P ∧ Q`**:
1. Split tactic (direct structural match)
2. Auto (if both parts are simple)
3. Manual proof of each part (fallback)