如何在 Coq 语句中证明给定集合答案

【问题标题】：How to proof in Coq statements about given sets如何在 Coq 语句中证明给定集合
【发布时间】：2015-12-19 19:39:01
【问题描述】：

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.

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

也许必须编写一个以引理为类型的算法。但我不知道该怎么做。

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

【问题讨论】：

这很容易证明（在 Coq 中或手动），因为它只是一个特定的列表。你的最终目标是证明由其他东西生成的列表吗？在这种情况下，您需要证明有关生成列表的代码/功能/过程的事情。这就是它变得有趣的地方。
如果列表变得复杂，则无法“手动”证明。例如，考虑一个 COQ 模型，它需要一个 1000x1000 的大矩阵作为参数。并且必须确保矩阵具有满秩。假设您需要全等级属性来证明模型的属性。当然，可以使用计算机代数系统检查模型的每个单独实例，并将“满秩”属性作为公理添加到模型中。但这有点奇怪......
我认为问题在于 COQ 对依赖类型的归纳有一些限制。网站homes.cs.washington.edu/~jrw12/dep-destruct.html 试图解释它，但我很难理解他们的论点。

标签： coq dependent-type induction

【解决方案1】：

这是一个简单明了的证明：

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.

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

【讨论】：

您可以使用repeat 将其缩小为repeat dependent destruction x; compute; auto 10.。

【解决方案2】：

让我建议使用 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，从而得出证明。

【讨论】：