playbooks

home / skills / a5c-ai / babysitter / coq-proof-assistant

coq-proof-assistant skill

/plugins/babysitter/skills/babysit/process/specializations/domains/science/mathematics/skills/coq-proof-assistant

This skill guides formal verification with the Coq proof assistant, generating tactics, leveraging SSReflect/MathComp, and extracting verified code.

npx playbooks add skill a5c-ai/babysitter --skill coq-proof-assistant

Review the files below or copy the command above to add this skill to your agents.

Files (1)
SKILL.md
954 B
---
name: coq-proof-assistant
description: Interface with Coq proof assistant for formal verification
allowed-tools:
  - Bash
  - Read
  - Write
  - Edit
  - Glob
  - Grep
metadata:
  specialization: mathematics
  domain: science
  category: theorem-proving
  phase: 6
---

# Coq Proof Assistant

## Purpose

Provides expert guidance on using the Coq proof assistant for formal verification and mathematical formalization.

## Capabilities

- Ltac and Ltac2 tactic generation
- SSReflect/MathComp library integration
- Proof by reflection techniques
- Extraction to OCaml/Haskell
- Proof documentation generation

## Usage Guidelines

1. **Proof Scripts**: Write Coq vernacular with proper structuring
2. **Tactics**: Use Ltac macros for proof automation
3. **Libraries**: Leverage MathComp for algebra and SSReflect for reasoning
4. **Extraction**: Generate verified executable code

## Tools/Libraries

- Coq
- SSReflect
- MathComp
- CoqIDE or VS Code

Overview

This skill interfaces with the Coq proof assistant to support formal verification, proof development, and extraction of verified code. I provide targeted help generating Ltac/Ltac2 tactics, integrating SSReflect/MathComp patterns, and structuring proof scripts for maintainability. The skill also assists with proof-by-reflection techniques and producing extractable, documented code.

How this skill works

I inspect your Coq goals, context, and existing script fragments and propose compact vernacular steps or automated tactics. I generate Ltac and Ltac2 macros, suggest SSReflect-style rewrites, and recommend MathComp lemmas to reuse. For extraction I outline how to annotate and export verified functions to OCaml or Haskell and produce minimal documentation for each lemma and definition.

When to use it

  • When you need help converting a math argument into a Coq proof script.
  • When you want compact Ltac or Ltac2 tactics to automate repetitive proof patterns.
  • When integrating MathComp/SSReflect idioms into existing developments.
  • When applying proof-by-reflection to speed up decision procedures.
  • When preparing verified functions for extraction to OCaml or Haskell.

Best practices

  • Structure scripts with clear sections: imports, definitions, lemmas, proofs, and doc comments.
  • Prefer small, composable lemmas and name them consistently for MathComp lookup.
  • Use SSReflect tactics for concise rewrites and view-based reasoning where applicable.
  • Encapsulate automation in Ltac/Ltac2 macros and keep their effect localized.
  • Annotate extraction boundaries early and test extracted code for expected semantics.

Example use cases

  • Translate a pen-and-paper induction into a robust Coq proof using Ltac helpers.
  • Refactor long proofs into SSReflect style with MathComp lemmas for algebraic reasoning.
  • Implement a reflection-based decision procedure for arithmetic and generate automation.
  • Prepare verified sorting or parsing functions and extract them to OCaml with correct signatures.
  • Generate inline documentation for a Coq library to assist reviewers and downstream users.

FAQ

Can you generate complete proofs automatically?

I can produce tactic sequences and automation that solve many routine goals, but complex proofs often require human design, lemma selection, and iterative refinement.

Do you support both Ltac and Ltac2?

Yes. I provide suggestions and macro templates for both Ltac and Ltac2 and explain trade-offs for maintenance and performance.