如何在Coq語句中對給定集合進行證明

COQ中的一個證明語句如下所示。如何在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.

或者，假設你有一個數字給定的名單，你想證明，沒有數量在列表中出現兩次。

也許人們必須編寫一個引理類型的算法。但我不知道如何做到這一點。

順便說一句，它不是一個功課練習。

來源

2015-12-19 Cryptostasis

這很容易證明（在Coq或手中），因爲它只是一個特定的列表。你的最終目標是證明由別的東西產生的列表嗎？在這種情況下，您需要證明有關生成列表的代碼/函數/過程的內容。這就是它變得有趣的地方。 –

如果列表變得複雜，證明「手工」是不可能的。例如，考慮使用需要大型1000x1000矩陣作爲參數的COQ模型。必須確保矩陣具有完整的等級。假設您需要完整的排名屬性來驗證模型的屬性。當然可以用計算機代數系統檢查模型的每個單獨實例，並將「滿秩」屬性作爲模型的公理。但是，這有點奇怪... – Cryptostasis

我認爲問題在於COQ對依賴類型的歸納有一些限制。該網站http://homes.cs.washington.edu/~jrw12/dep-destruct.html試圖解釋它，但我有一些難以遵循他們的論點。 – Cryptostasis

這裏是一個快速和骯髒的證明：

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公理，但這不應該是一個問題。

來源

2015-12-21 13:08:15

您可以使用'repeat'將其縮小到'repeat dependent destruction x;計算;自動10.'。 – gallais

讓我用數學壓縮庫提出一個解決方案：

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引理將通過其可計算的版本，這反過來又會使勒柯克檢查的元組的所有元素都更換您的謂詞大於0，結論證明。

來源

2016-02-26 00:42:52 ejgallego

如何在Coq語句中對給定集合進行證明

回答

相關問題