Proof Skeleton Generator

Generate structured proof skeletons with tactics, proof strategies, and key lemmas for theorems in Isabelle/HOL or Coq.

Workflow

1. Analyze the Theorem Statement

Examine the theorem to understand:

Quantifiers: Universal (∀/forall) or existential (∃/exists)
Logical structure: Implications, conjunctions, disjunctions
Data types involved: Lists, natural numbers, custom types
Complexity: Simple equality vs. complex property

2. Choose Target System

Ask the user which proof assistant to target:

Isabelle/HOL: Uses Isar structured proofs, automatic tactics
Coq: Uses Ltac tactics, more explicit proof terms
Both: Generate skeletons for both systems

If not specified, default to generating both versions.

3. Determine Proof Strategy

Based on the theorem structure, identify the appropriate proof technique:

Induction - When theorem involves recursive types:

List induction for list properties
Natural number induction for arithmetic
Structural induction for custom datatypes
Strong induction when needed

Case Analysis - When theorem involves:

Boolean conditions
Option types (None/Some)
Sum types or custom constructors
Conditional expressions

Direct Proof - When theorem is:

Simple equality that simplifies
Follows directly from definitions
Provable by automatic tactics

Forward Reasoning - Build up facts:

Establish intermediate lemmas
Chain implications
Construct witnesses for existentials

Backward Reasoning - Work from goal:

Apply rules to reduce goal
Split conjunctions
Introduce implications

4. Identify Required Lemmas

Determine helper lemmas that may be needed:

Standard library lemmas: Check if already available
Custom lemmas: Properties that need separate proof
Induction hypotheses: How they'll be used
Intermediate facts: Steps in the main proof

5. Generate Proof Skeleton

Use the reference files for tactics and patterns:

Isabelle tactics: See isabelle_tactics.md
Coq tactics: See coq_tactics.md
Complete examples: See examples.md

Create a skeleton that includes:

Proof structure with appropriate method (induction, cases, etc.)
Case labels for each subgoal
Strategy comments explaining the approach
Tactic placeholders (sorry/admit) for incomplete steps
Intermediate assertions (have/assert) for key facts
Helper lemmas with their own skeletons

6. Structure the Output

Organize the proof skeleton clearly:

For Isabelle/HOL:

(* Helper lemmas if needed *)
lemma helper_name:
  "statement"
  sorry

(* Main theorem *)
theorem theorem_name:
  assumes "assumptions"
  shows "conclusion"
proof (method)
  case case_name
  (* Goal: ... *)
  (* Strategy: ... *)
  (* Key steps:
     1. ...
     2. ...
  *)
  show ?case sorry
next
  (* Additional cases *)
qed

For Coq:

(* Helper lemmas if needed *)
Lemma helper_name :
  statement.
Proof.
  (* proof *)
  admit.
Admitted.

(* Main theorem *)
Theorem theorem_name :
  statement.
Proof.
  intros.
  induction ... as [| ...].
  - (* Case: ... *)
    (* Strategy: ... *)
    admit.
  - (* Case: ... *)
    (* IH: ... *)
    (* Strategy: ... *)
    admit.
Admitted.

Key Principles

Clarity

Add comments explaining the proof strategy
Label each case clearly
Document what the induction hypothesis provides
Explain non-obvious steps

Completeness

Include all necessary cases
Identify all required helper lemmas
Show the structure of nested proofs
Indicate where automation might work

Practicality

Use sorry (Isabelle) or admit (Coq) for incomplete steps
Suggest automatic tactics where applicable
Note when sledgehammer (Isabelle) might help
Indicate which steps are trivial vs. challenging

Correctness

Ensure case analysis is exhaustive
Verify induction is on the right variable
Check that the proof structure matches the goal
Validate that lemmas are actually needed

Proof Strategy Selection Guide

When to Use Induction

List properties: forall xs, P xs

Induction on xs
Base case: empty list
Inductive case: x :: xs with IH P xs

Natural number properties: forall n, P n

Induction on n
Base case: 0 or Suc 0
Inductive case: Suc n with IH P n

Recursive function properties: When function is defined recursively

Induct on the recursive argument
IH mirrors the recursive call

When to Use Case Analysis

Conditional expressions: if b then ... else ...

Split on b (true/false cases)

Option types: match opt with None => ... | Some x => ...

Case on None and Some x

Sum types: match x with Left a => ... | Right b => ...

Case on each constructor

When to Use Direct Proof

Definitional equalities: f x = g x where definitions unfold

Unfold definitions and simplify

Trivial goals: Provable by auto, simp, reflexivity

Try automatic tactics first

When to Use Lemmas

Repeated subgoals: Same property needed multiple times

Extract as separate lemma

Complex intermediate facts: Multi-step derivations

Prove as helper lemma

Standard properties: Check standard library first

Import and use existing lemmas

Common Patterns

Induction with Simplification

proof (induction xs)
  case Nil
  show ?case by simp
next
  case (Cons x xs)
  show ?case using Cons.IH by simp
qed

Case Analysis with Subproofs

proof (cases x)
  case Constructor1
  show ?thesis
  proof -
    (* detailed steps *)
  qed
next
  case Constructor2
  (* ... *)
qed

Forward Reasoning Chain

proof -
  have step1: "fact1" by simp
  have step2: "fact2" using step1 by simp
  show ?thesis using step2 by simp
qed

Backward Reasoning with Rules

proof (rule some_rule)
  show "premise1" sorry
  show "premise2" sorry
qed

Tips

Start with structure: Get the proof skeleton right before filling details
Use comments liberally: Explain strategy and key steps
Identify IH usage: Note where induction hypothesis is applied
Check standard library: Many lemmas already exist
Suggest automation: Note where auto, simp, blast might work
Be realistic: Mark challenging steps as sorry/admit
Both systems: Ensure semantic equivalence when generating both
Nested induction: Handle carefully with clear variable names
Termination: Note when termination proofs are needed

proof-skeleton-generator