Agent-Skills.md

Agent Skills: Coq Proof Assistant

Interface with Coq proof assistant for formal verification

theorem-provingID: a5c-ai/babysitter/coq-proof-assistant

Repository

a5c-ai/babysitter
a5c-aiLicense: MIT
244

Install this agent skill to your local

pnpm dlx add-skill https://github.com/a5c-ai/babysitter/tree/HEAD/plugins/babysitter/skills/babysit/process/specializations/domains/science/mathematics/skills/coq-proof-assistant

Skill Files

Browse the full folder contents for coq-proof-assistant.

Download Skill

Loading file tree…

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

Skill Metadata

Name
coq-proof-assistant
Description
Interface with Coq proof assistant for formal verification

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