proof-refactoring-assistant

Restructure and improve Isabelle or Coq proofs to enhance readability, modularity, and maintainability without changing semantics. Use when proofs are long and monolithic, have repeated patterns, use unclear naming, lack documentation, or when the user asks to refactor, clean up, improve, or reorganize their formal proofs.

Ir para a instalação

Repositório: ArabelaTso/Skills-4-SE
Última atividade na origem: 20 de fevereiro de 2026 às 09:49
Idioma detectado do SKILL.md: inglês
Estrelas: 240
Forks: 22

Opções de instalação

Por padrão, está selecionado o prompt que primeiro revisa a origem. Você pode mudar para um comando direto ou baixar uma cópia local.

Revise os arquivos de origem

Leia o SKILL.md e os arquivos complementares exibidos pelo SkillsMP antes de decidir se vai instalar.

Voltar à pesquisa Voltar à instalação

Code Smell	Refactoring	When to Apply
Long proof (>20 lines)	Extract Helper Lemma	Complex subgoals, repeated reasoning
One-use trivial lemma	Inline Trivial Lemma	Proof is simple, used once
Many cases	Break Down Long Proof	Complex case analysis
Repeated pattern	Extract Common Pattern	Same proof multiple times
Complex tactics	Simplify Proof Structure	Simpler tactics available
Generic names	Improve Naming	Unclear what lemma proves
No comments	Add Documentation	Complex or non-obvious proof
Stuck induction	Strengthen Hypothesis	Need more general statement
Too specific	Generalize Lemma	Could be more reusable
Tedious manual proof	Use Automation	Standard tactics available

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.

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.

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.

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

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

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

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.

(** 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.

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

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"
  (* 12 lines of proof *)
  by auto

lemma case_C3: "⋀f. x = C3 f ⟹ P x"
  (* 10 lines of proof *)
  by auto

lemma complex_cases: "P x"
  by (cases x) (auto simp: case_C1 case_C2 case_C3)

Fixpoint sum (n : nat) : nat :=
  match n with
  | 0 => 0
  | S n' => n + sum n'
  end.

Lemma sum_formula : forall n : nat, 2 * sum n = n * (n + 1).
Proof.
  induction n.
  - reflexivity.
  - simpl. (* Gets stuck - IH not strong enough *)
Admitted.

(* Strengthen by generalizing with accumulator *)
Lemma sum_formula_gen : forall n acc : nat,
  2 * (sum n + acc) = n * (n + 1) + 2 * acc.
Proof.
  induction n; intros.
  - simpl. lia.
  - simpl. rewrite IHn. lia.
Qed.

Lemma sum_formula : forall n : nat, 2 * sum n = n * (n + 1).
Proof.
  intros. pose proof (sum_formula_gen n 0). lia.
Qed.