2

COQ 中的一个证明陈述如何类似于以下一个。

Require Import Vector.
Import VectorNotations.
Require Import Fin.

Definition v:=[1;2;3;4;5;6;7;8].
Lemma L: forall (x: Fin.t 8), (nth v x) > 0.

或者，假设您有一个给定的数字列表，并且您想证明没有数字在该列表中出现两次。

也许必须编写一个以引理为类型的算法。但我不知道如何做到这一点。

顺便说一句，这不是家庭作业。

4

2 回答 2

2

这是一个快速而肮脏的证明：

Proof.
Require Import Program.
dependent destruction x.
auto.
dependent destruction x.
compute.
auto.
dependent destruction x.
compute.
auto.
dependent destruction x.
compute.
auto.
dependent destruction x.
compute.
auto.
dependent destruction x.
compute.
auto 10.
dependent destruction x.
compute.
auto 10.
dependent destruction x.
compute.
auto 10.
dependent destruction x.
Qed.

我们使用模块中的dependent destruction策略Program。这依赖于 JMeq 公理，但这应该不是问题。

于 2015-12-21T13:08:15.753 回答
1

让我建议使用 math-comp 库的解决方案：

From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
From mathcomp Require Import fintype tuple.

Definition v := [tuple of [:: 1;2;3;4;5;6;7;8]].

Lemma L : forall x, tnth v x > 0.
Proof. exact/all_tnthP. Qed.

引理将all_tnthP用它的可计算版本替换你的谓词，这反过来又会让 Coq 检查元组中的所有元素是否大于 0，从而得出证明。

于 2016-02-26T00:42:52.467 回答