Proof Refactoring Assistant

Overview

Improve proof quality by restructuring Isabelle and Coq proofs for better readability, modularity, and maintainability while preserving semantics. This skill applies proven refactoring patterns to make proofs easier to understand and maintain.

Refactoring Workflow

Step 1: Analyze Current Proof

Identify code smells and improvement opportunities:

1. Structure issues:

   • Long, monolithic proofs (>20 lines)
   • Deep nesting of proof steps
   • Repeated proof patterns
   • Complex case analysis

2. Naming issues:

   • Generic names (lemma1, helper, aux)
   • Inconsistent naming conventions
   • Names don't describe what lemma proves

3. Documentation issues:

   • Missing comments
   • No explanation of complex steps
   • Unclear proof strategy

4. Modularity issues:

   • No helper lemmas
   • Duplicated reasoning
   • Overly specific lemmas

5. Complexity issues:

   • Manual proofs when automation available
   • Weak induction hypotheses
   • Unnecessarily complex tactics

Step 2: Identify Refactoring Opportunities

Choose appropriate refactoring patterns:

Extract Helper Lemma:

• Long proof with complex subgoals
• Repeated reasoning
• Reusable intermediate results

Inline Trivial Lemma:

• Helper used only once
• Proof is trivial
• Adds unnecessary indirection

Break Down Long Proof:

• Many cases to handle
• Complex nested structure
• Hard to follow logic

Extract Common Pattern:

• Same proof repeated
• Similar lemmas with minor variations
• Opportunity for generalization

Simplify Proof Structure:

• Complex tactics when simpler ones work
• Manual steps that automation handles
• Unnecessary proof verbosity

Improve Naming:

• Unclear or generic names
• Inconsistent conventions
• Names don't match content

Add Documentation:

• Complex lemmas without explanation
• Non-obvious proof strategies
• Important invariants not stated

Strengthen Induction Hypothesis:

• Induction gets stuck
• Need more general statement
• Weak hypothesis insufficient

Generalize Lemma:

• Overly specific statement
• Could be more reusable
• Hardcoded constants

Replace Manual Proof with Automation:

• Tedious manual steps
• Arithmetic or logic reasoning
• Standard library tactics available

Step 3: Apply Refactoring

Execute the refactoring safely:

1. Preserve semantics:

   • Don't change what is proved
   • Keep same logical content
   • Maintain correctness

2. Make incremental changes:

   • One refactoring at a time
   • Verify after each change
   • Easy to revert if needed

3. Test continuously:

   • Recompile after each change
   • Check dependent proofs
   • Verify no breakage

4. Document changes:

   • Add comments explaining complex parts
   • Note proof strategy
   • Explain design decisions

Step 4: Verify Improvements

Ensure refactoring achieved goals:

1. Readability:

   • Easier to understand?
   • Clear structure?
   • Good naming?

2. Modularity:

   • Reusable components?
   • Appropriate abstraction level?
   • Clear dependencies?

3. Maintainability:

   • Easier to modify?
   • Well documented?
   • Follows conventions?

4. Performance:

   • Compilation time acceptable?
   • No significant slowdown?
   • Automation effective?

Common Refactoring Patterns

For detailed patterns and examples, see refactoring_patterns.md.

Quick Reference

Examples

Example 1: Extract Helper Lemma

Before (Coq):

Lemma complex_theorem : forall n m : nat,
  n > 0 -> m > 0 -> n + m > 0 /\ n * m > 0.
Proof.
  intros n m Hn Hm.
  split.
  - destruct n. inversion Hn.
    destruct m. inversion Hm.
    simpl. lia.
  - destruct n. inversion Hn.
    destruct m. inversion Hm.
    simpl. apply Nat.mul_pos_pos; lia.
Qed.

After (Coq):

Lemma add_pos : forall n m : nat,
  n > 0 -> m > 0 -> n + m > 0.
Proof. intros. lia. Qed.

Lemma mul_pos : forall n m : nat,
  n > 0 -> m > 0 -> n * m > 0.
Proof. intros. apply Nat.mul_pos_pos; lia. Qed.

Lemma complex_theorem : forall n m : nat,
  n > 0 -> m > 0 -> n + m > 0 /\ n * m > 0.
Proof.
  intros. split.
  - apply add_pos; assumption.
  - apply mul_pos; assumption.
Qed.

Improvements:

• Extracted reusable helper lemmas
• Main proof now clear and concise
• Helpers can be used elsewhere

Example 2: Simplify Proof Structure

Before (Coq):

Lemma add_comm : forall n m : nat, n + m = m + n.
Proof.
  intros n m.
  induction n.
  - simpl. rewrite <- plus_n_O. reflexivity.
  - simpl. rewrite IHn. rewrite <- plus_n_Sm. reflexivity.
Qed.

After (Coq):

Lemma add_comm : forall n m : nat, n + m = m + n.
Proof.
  intros. lia.
Qed.

Improvements:

• Replaced manual proof with automation
• Much shorter and clearer
• Less maintenance burden

Example 3: Improve Naming

Before (Isabelle):

lemma l1: "length (xs @ ys) = length xs + length ys"
  by (induction xs) auto

lemma l2: "length (rev xs) = length xs"
  by (induction xs) auto

lemma thm: "length (xs @ ys) = length xs + length ys ∧
            length (rev xs) = length xs"
  using l1 l2 by simp

After (Isabelle):

lemma append_length: "length (xs @ ys) = length xs + length ys"
  by (induction xs) auto

lemma rev_length: "length (rev xs) = length xs"
  by (induction xs) auto

lemma list_length_properties:
  "length (xs @ ys) = length xs + length ys ∧
   length (rev xs) = length xs"
  using append_length rev_length by simp

Improvements:

• Descriptive names indicate what each lemma proves
• Follows naming conventions
• Easier to find and understand

Example 4: Add Documentation

Before (Coq):

Lemma partition_spec : forall (A : Type) (f : A -> bool) (l : list A),
  let (l1, l2) := partition f l in
  filter f l = l1 /\ filter (fun x => negb (f x)) l = l2.
Proof.
  (* Complex 20-line proof *)
Admitted.

After (Coq):

(** Specification of list partition function.

    Given a predicate f and a list l, partition splits l into two lists:
    - l1 contains all elements satisfying f
    - l2 contains all elements not satisfying f

    This lemma proves that partition is equivalent to filtering twice.

    Proof strategy: Induction on l, with case analysis on f(head).
*)
Lemma partition_spec : forall (A : Type) (f : A -> bool) (l : list A),
  let (l1, l2) := partition f l in
  filter f l = l1 /\ filter (fun x => negb (f x)) l = l2.
Proof.
  (* Complex 20-line proof *)
Admitted.

Improvements:

• Clear explanation of what lemma proves
• Documents proof strategy
• Easier for others to understand

Example 5: Break Down Long Proof

Before (Isabelle):

lemma complex_cases: "P x"
proof (cases x)
  case (C1 a b c)
  (* 15 lines of proof *)
  then show ?thesis by auto
next
  case (C2 d e)
  (* 12 lines of proof *)
  then show ?thesis by auto
next
  case (C3 f)
  (* 10 lines of proof *)
  then show ?thesis by auto
qed

After (Isabelle):

lemma case_C1: "⋀a b c. x = C1 a b c ⟹ P x"
  (* 15 lines of proof *)
  by auto

lemma case_C2: "⋀d e. x = C2 d e ⟹ P x