Coq

2022年10月19日 (三) 06:53的版本

您可以在Wikipedia上了解到此条目的英文信息 Coq Thanks, Wikipedia.

Coq

简介

The Coq Proof Assistant 证明助手，使用 OCaml 编写，采用 LGPL 许可证。

功能

Coq 是一个定理证明辅助工具，不仅可以用来开发安全应用这类需要绝对可信的程序，还可以被数学家用来开发证明。将 Coq 系统被用作一个逻辑框架，在此框架下为新的逻辑提供公理，并基于这些逻辑来开发证明。

Coq Enhancement Proposals (CEP)

Coq 已成为跨计算机科学和数学研究的关键推动者

• 作为一个编程语言的建模平台，Coq 成为了研究员对复杂的语言定义进行描述和论证的标准工具。例如，它被用来检查 JavaCard 平台的安全性，得到了最高等级的通用准则验证，它还被用在 x86 和 LLVM 指令集以及 C 等编程语言的形式化规范中。
• 作为一个形式化软件验证的开发环境，Coq 被用来构建：CompCert 一个完全验证的 C 优化编译器；CertiKos 一个完全验证的工具，用于证明涉及浮点数的精妙算法的正确性；Coq 也是 CertiCrypt 的基础，一个用于论证密码学算法安全性的环境。Coq 还被用来构建开源 RISC-V 处理器架构的验证实现。
• 作为一个依赖类型函数式编程的现实环境，Coq 激发了大量的创新。例如 Ynot 系统嵌入了“关系式霍尔推理”（一个 '霍尔逻辑' 的扩展， 我们之后会看到它）。
• 作为一个高阶逻辑的证明助理，Coq 被用来验证数学中一些重要的结果。例如 Coq 可在证明中包含复杂计算的能力，使其开发出了第一个形式化验证的四色定理证明。此前数学家们对该证明颇有争议，因为它需要用程序对大量组态进行检验。在 Coq 的形式化中，所有东西都被检验过，自然也包括计算的正确性。近年来，Feit-Thompson 定理经过了更大的努力用 Coq 形式化了，它是对有限单群进行分类的十分重要的第一步。

指南

• Coq Wiki
• Coq Tutorials and books
• Coq Reference Manual
• The Coq Standard Library
• Install Coq with opam 推荐
• Install Coq Interactive Theorem Prover on Debian

sudo systemctl start snapd.service // 安装 sanpd 后要启动它

$ coqtop

Welcome to Coq 8.14.0
Coq < Print Scope nat_scope.
Coq 的 ZArith 库中使用的 positive 类型标识严格正整数。
Coq < Require Import ZArith.
Coq < Print positive.
Coq < Print Z.	
Coq < Quit. 

OPAM 安装

$ opam repository add coq-released --all-switches
$ opam install coqide
$ opam install coq-chick-blog
$ eval $(opam env)
$ coq-chick-blog
http://localhost:8008/ 

CoqIDE based on GTK

$ opam search coqide
# Packages matching: match(*coqide*)
# Name        # Installed # Synopsis
coqide        dev         The Coq Proof Assistant --- GTK3 IDE
coqide-server dev         The Coq Proof Assistant, XML protocol server
$ coqide

Emacs Mode

Proof General A generic Emacs interface for proof assistants, You can now open Coq file (.v), an EasyCrypt file (.ec), a qrhl-tool file (.qrhl), or a PhoX file (.phx).

项目

Awesome Coq awesome-coq

• Coq @ GitHub
• coq-community
• coq-contribs
• Mathematical Components The Four Color Theorem 四色理论
• Programming Languages and Verification Group at MIT CSAIL
• Fiat-Crypto Cryptographic Primitive Code Generation by Fiat Cryptography
• Kôika A Core Language for Rule-Based Hardware Design
• Formal Reasoning About Programs 关于程序的形式化推理
• Programs and Proofs Mechanizing Mathematics with Dependent Types] 程序和证明，使用依赖类型的数学机械化
• Coq 被用于 CompCert verified C compiler CompCert验证的C编译器
• Iris 一个高阶并发分离逻辑框架，在 Coq 证明助手中实现和验证。
• 相似项目：Agda, Idris
• CertiCoq A verified compiler for Coq
• MetaCoq Metaprogramming in Coq
• QuickChick
• Kami
• coq-haskell 一个在 Coq 中形式化 Haskell 类型和函数的库
• Foundational Cryptography Framework (FCF) Cryptography
• Mtac2 A typed tactic language for Coq.
• FSCQ is a file system written and verified in the Coq proof assistant.
• ChickBlog A blog engine written and proven in Coq
• Vellvm Verifying the LLVM
• Coq Tezos of OCaml 用 Coq 翻译和验证 Tezos 经济协议的代码
• coq-of-ocaml 可使用它做两件事：1、do formal proofs on OCaml programs; 2、port OCaml projects to Coq.
• hs-to-coq import Haskell to Coq
• Goose import Go to Coq
• SMTCoq Communication between Coq and SAT/SMT solvers
• An Open Framework for Certified System Software
• SMTCoq Communication between Coq and SAT/SMT solvers
• Homotopy Type Theory (HoTT) 同伦类型论
• Univalent Mathematics

语言

• Gallina Coq 原生的函数式编程语言
• tactic language
• SSReflect proof language
• Extraction of programs in OCaml and Haskell

包管理

• opam OCaml Package Manager
• Packaging Coq

STEM

• Coq In The Classroom
• Modelling and verifying algorithms in Coq
• Interactive Computer Theorem Proving
• Formalization of Mathematics
• Semantic of Proofs and Certified Mathematics
• Iris: Higher-Order Concurrent Separation Logic Lecture Notes
• Formal Reasoning About Programs Adam Chlipala
• Coq Preparation and Boot Camp Types, Logic, and Verification

文档

• Comparison of Two Theorem Provers: Isabelle/HOL and Coq
• Coq documentation

图书

• 《Software Foundations》 软件基础系列是对可靠软件的数学基础的广泛介绍。该系列的主要创新之处在于，每一个细节都是百分之百的形式化和机器检查：每一卷的整个文本，包括练习，实际上是Coq证明助手的 "证明脚本"。
• 《软件基础》系列广泛地介绍了可靠软件的数学基础，这是《Software Foundations》中文版。
• 《Certified Programming with Dependent Types》
• 《交互式定理证明与程序开发 Coq 归纳构造演算的艺术》
• Mathematical Components
• Modeling and Proving in Computational Type Theory
• Hydras & Co.
• 《Homotopy Type Theory: Univalent Foundations of Mathematics》 The Univalent Foundations Program

案例

• Trusted Logic 经过三年努力，成功地完成 JavaCard 语言的整个执行环境的形式化模拟。这项安全方面的工作获得 EAL7 证书奖（公共标准下最高级别的奖励）。这一形式开发工作使用了 121000 行 Coq 代码，总共 278 个模块。

图集

• 

  Coq

• 

  CompCert

• 

  ChickBlog

• 

  对不等式36<=38的证明

• 

  命题逻辑的符号

• 

  coq-of-ocaml

• 

  RISC-V形式化验证

链接

• Coq 官网
• Bluespec Open Source RISC-V Cores and Tools