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.
91
86%
Does it follow best practices?
Impact
100%
1.00xAverage score across 3 eval scenarios
Passed
No known issues
Evaluation results
100%
Cleaning Up an Inherited Coq Proof Library
Naming conventions and documentation
No generic names
100%
100%
Descriptive lemma names
100%
100%
Convention suffixes used
100%
100%
Coq doc comments present
100%
100%
Doc comments explain content
100%
100%
Proof strategy documented
100%
100%
100%
Restructuring a Monolithic Tree Properties Proof
Extract helper lemmas and use automation
Helper lemmas extracted
100%
100%
Helper names are descriptive
100%
100%
Main proof uses helpers
100%
100%
Automation tactics used
100%
100%
Semantics preserved
100%
100%
No over-extraction
100%
100%
100%
Fixing and Deduplicating an Isabelle List Theory
Strengthen induction hypothesis and extract common patterns
General count_append lemma
100%
100%
Specialized lemmas use general one
100%
100%
list_sum_append helper introduced
100%
100%
list_sum_rev proved using helper
100%
100%
No sorry remains
100%
100%
- Repository
- ArabelaTso/Skills-4-SE
- Commit
0f00a4f
- Evaluated
- Agent
- Claude Code
- Model
- Claude Sonnet 4.6
Table of Contents
Is this your skill?
If you maintain this skill, you can claim it as your own. Once claimed, you can manage eval scenarios, bundle related skills, attach documentation or rules, and ensure cross-agent compatibility.