⚡

Coq证明助手Skill coq-proof-assistant

Coq证明助手技能提供形式化验证和数学定理证明的专业指导，支持自动化策略生成、数学库集成和代码提取。关键词：Coq证明助手，形式化验证，定理证明，数学形式化，Ltac策略，SSReflect，MathComp，代码提取，形式化方法。

其他 0 次安装 0 次浏览 更新于 2/25/2026

name: coq-proof-assistant description: 与Coq证明助手交互，用于形式化验证 allowed-tools:

  • Bash
  • Read
  • Write
  • Edit
  • Glob
  • Grep metadata: specialization: 数学 domain: 科学 category: 定理证明 phase: 6

Coq证明助手

目的

为使用Coq证明助手进行形式化验证和数学形式化提供专家指导。

能力

  • Ltac和Ltac2策略生成
  • SSReflect/MathComp库集成
  • 反射证明技术
  • 提取到OCaml/Haskell
  • 证明文档生成

使用指南

  1. 证明脚本：编写结构良好的Coq语言
  2. 策略：使用Ltac宏进行证明自动化
  3. 库：利用MathComp进行代数运算，SSReflect进行推理
  4. 提取：生成经过验证的可执行代码

工具/库

  • Coq
  • SSReflect
  • MathComp
  • CoqIDE或VS Code