clarus/falso

语言: Coq

git: https://github.com/clarus/falso

虚假证明。
A proof of false.
README.md (中文)

虚假证明。

这是Falso证明系统的Coq证明助手中的一个实现。当存在超过255个构造函数的类型时,它会利用vm_compute命令的错误。 vm_compute命令通过编译为字节代码来有效地计算术语。这个bug涉及Coq的所有最新稳定版本,包括Coq 8.4pl5。

[编辑]使用Coq 8.4.6更正此错误。

使用

使用OPAM for Coq安装:

opam repo add coq-released https://coq.inria.fr/opam/released
opam install -j4 coq:falso

在一个乏味的发展:

Require Import Falso.All.

Lemma hard : forall (A : Prop), A.
  destruct falso.
Qed.

(** Print the list of axioms used by [hard]. This list is empty. *)
Print Assumptions hard.

积分

这种证明技术是由MaximeDénès和Pierre-MariePédrot发现的。该套餐由Guillaume Claret根据麻省理工学院许可证制作。

本文使用googletrans自动翻译,仅供参考, 原文来自github.com

en_README.md

Falso

A proof of false.

This is an implementation in the Coq proof assistant of the Falso proof system. It exploits a bug of the vm_compute command when there is a type with more than 255 constructors. The vm_compute command evaluates a term efficiently by compilation to a byte-code. This bug concerns all recent stable versions of Coq, including Coq 8.4pl5.

[Edit] This bug was corrected with Coq 8.4.6.

Use

Install with OPAM for Coq:

opam repo add coq-released https://coq.inria.fr/opam/released
opam install -j4 coq:falso

In a tedious development:

Require Import Falso.All.

Lemma hard : forall (A : Prop), A.
  destruct falso.
Qed.

(** Print the list of axioms used by [hard]. This list is empty. *)
Print Assumptions hard.

Credits

This proof technique was discovered by Maxime Dénès and Pierre-Marie Pédrot. This package is made by Guillaume Claret, under MIT license.