在Coq中計算列表中不同元素的數量

我正在嘗試編寫一個函數，該函數將自然數列表作爲輸出並返回其中不同元素的數量。例如，如果我有列表[1,2,2,4,1]，我的函數DifElem應輸出「3」。我試過很多東西，我已經得到最接近的是這樣的：在Coq中計算列表中不同元素的數量

Fixpoint DifElem (l : list nat) : nat := 
    match l with 
    | [] => 0 
    | m::tm => 
    let n := listWidth tm in 
    if (~ In m tm) then S n else n 
end.

我的邏輯是這樣的：如果m不在列表中的尾部，然後添加一個櫃檯。如果是這樣，不要添加到櫃檯，所以我只會計算一次：當它是最後一次出現時。我得到的錯誤：

Error: The term "~ In m tm" has type "Prop" 
which is not a (co-)inductive type.

在爲它定義那裏勒柯克的名單標準庫Coq.Lists.List.的一部分：

Fixpoint In (a:A) (l:list A) : Prop := 
    match l with 
    | [] => False 
    | b :: m => b = a \/ In a m 
end.

我想我不明白不夠好怎麼用。如果再聲明定義，Coq的文檔沒有足夠的幫助。

我也試過這個定義與nodup來自同一庫：

Definition Width (A : list nat) := length (nodup (A)).

在這種情況下，我所得到的錯誤是：

The term "A" has type "list nat" while it is expected to have 
type "forall x y : ?A0, {x = y} + {x <> y}".

而且我安靜困惑，這是怎麼回事在這。我希望你能幫助解決這個問題。

來源

2016-04-21 Sara

你似乎混淆命題（Prop）和布爾（bool）。我試圖用簡單的術語來解釋：命題是你證明的東西（根據Martin-Lof的解釋它是一組證明），而布爾型是一個只能保存2個值的數據類型（true/false）。當只有兩種可能的結果，並且不需要附加信息時，布爾可以用於計算。您可以通過@Ptival在this answer中找到關於此主題的更多信息，或者在B.C.的「軟件基礎」一書中關於此主題的全面部分。 Pierce等人（見Propositions and Booleans部分）。

實際上，nodup是這裏的方法，但Coq希望您提供一種決定輸入列表元素相等的方式。如果你看一看的nodup定義：

Hypothesis decA: forall x y : A, {x = y} + {x <> y}. 

Fixpoint nodup (l : list A) : list A := 
    match l with 
    | [] => [] 
    | x::xs => if in_dec decA x xs then nodup xs else x::(nodup xs) 
    end.

，你會發現一個假設decA，成爲一個額外的參數給nodup功能，所以你需要通過eq_nat_dec（FOT nats可判定的平等），用於例如，像這樣：nodup eq_nat_dec l。

所以，這裏是一個可能的解決方案：

Require Import Coq.Arith.Arith. 
Require Import Coq.Lists.List. 
Import ListNotations. 

Definition count_uniques (l : list nat) : nat := 
    length (nodup eq_nat_dec l). 

Eval compute in count_uniques [1; 2; 2; 4; 1]. 
(* = 3 : nat *)

注：因爲勒柯克V8.5的nodup功能工作。

來源

2016-04-21 17:02:25

謝謝你，我其實無所適從勒柯克可採取的「如果......那麼......」的語句。它可以採取布爾人。只有2個構造函數可以使用任何歸納定義嗎？或者有什麼限制？非常感謝您的建議。源代碼和如何修復我的代碼都非常有幫助！ – Sara

是的，'if'語句將任何兩個構造函數類型視爲布爾值。第一個構造函數被視爲true。更多關於這方面的內容，你可以在Adam Chlipala的[CPDT]（http://adam.chlipala.net/cpdt/）書中找到（[here]（http://adam.chlipala.net/cpdt/html/MoreDep.html））。 –

僅供參考，SF的'MoreLogic'章節已經從更新版本的SF中刪除:(我不確定在哪裏可以找到不包含解決方案的鏡像 –

除了使用標準庫的Anton解決方案之外，我想說的是，mathcomp提供了對此用例的特別好的支持以及關於count和uniq的完整理論。你的函數變爲：

From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. 

Definition count_uniques (T : eqType) (s : seq T) := size (undup s).

其實，我覺得count_uniques名字是多餘的，我寧願直接使用size (undup s)需要的地方。

來源

2016-04-22 08:29:18 ejgallego

[math-comp]的當前主頁（http：// math-comp .github.io /數學-COMP /） –

使用套：

Require Import MSets. 
Require List. Import ListNotations. 

Module NatSet := Make Nat_as_OT. 

Definition no_dup l := List.fold_left (fun s x => NatSet.add x s) l NatSet.empty. 
Definition count_uniques l := NatSet.cardinal (no_dup l). 

Eval compute in count_uniques [1; 2; 2; 4; 1].

來源

2016-04-22 13:00:08 eponier

在Coq中計算列表中不同元素的數量

回答

相關問題