Coq有界自然數MSet

我想爲給定上限的自然數集合定義一個類型。標準圖書館的MSet似乎是一種方式。我找到了this discussion，它給出了一個很好的例子來說明如何定義一組nat。但是我不知道如何將它擴展到子集類型。我試過這樣的事情：Coq有界自然數MSet

Module OWL. 
    Parameter n : nat. 
    Definition t := {i:nat | i<n}. 
    Definition eq := @eq t. 
    Instance eq_equiv : @Equivalence t eq := eq_equivalence. 
    Definition lt (a b:t) := Peano.lt (proj1_sig a) (proj1_sig b). 
    Instance lt_strorder : @StrictOrder t lt. 
    ...

我將使用具有不同上限的集合。但我不明白如何用給定的'n'來實例化這個模塊。理想情況下，我希望能夠這樣寫：

Module BoundedMNatSets := MakeWithLeibniz OWL. 
Definition BoundedMNatSetN (n:nat) : Type := BoundedMNatSets n.

P.S.這個問題可能源於我對Coq模塊系統的不足理解，而不是針對集合。

來源

2017-03-29 krokodil

是否'模塊OWL <：OrderedType.'幫助嗎？ – ejgallego

我認爲我的問題不在於排序，而在於參數化。我想用'n'來設置參數。 – krokodil

您將需要使用仿函數。 – ejgallego

您需要使用仿函數。喜歡的東西：

Require Import Orders. 

Module Type FIXED_NAT. 
    Parameter n : nat. 
End FIXED_NAT. 

Module OWL (N : FIXED_NAT) <: OrderedType. 
    Definition t := {i:nat | i < N.n}. 
    ... 
End OWL.

您可以再申請OWL簽字FIXED_NAT的模塊。

Module N1 <: FIXED_NAT. 
    Definition n := 10. 
End N1. 

Module OWL1 := OWL N1. 

Require Import MSets. 

Module M1 := Make OWL1.

編輯：什麼：

Require Import Orders. 
Require Import OrdersEx. 
Require Import MSets. 
Require Import Arith. 

Module M := Make Nat_as_OT. 

Definition has_upper_bound s n := M.For_all (ge n) s. 

Definition t n := {s : M.t | has_upper_bound s n}.

來源

2017-03-29 12:45:32 eponier

謝謝！它有點幫助，但這不完全是我想要實現的。我想'n'是一個MNatSet類型的參數，所以我可以在不同情況下使用不同的大小，而不用每次都實例化一個模塊。例如使用'Ensembles'，我可以這樣做：需要導入Coq.Sets.Ensembles。定義EFinNatSet（n：nat）：類型：= Ensemble {x：nat | （X krokodil

我正在玩最新的解決方案，你在更新中建議。它看起來很有趣。我會在這裏更新一次，我會更好地理解它。謝謝！ – krokodil

它看起來像建議的方式可能適合我。我只是一個快速的後續問題：1）爲什麼你選擇'bool'而不是'prop'。 2）爲什麼'fold'不是'For_all' 3）如何獲得額外的引理，比如在這個集合的MSetFacts或MSetInterface中？謝謝！附：這是一個小例子，將您對Prop/Forall的建議重新加工，並嘗試使用它來證明一個簡單的引理。 http://ideone.com/gKcl6j任何評論都非常受歡迎。 – krokodil

Coq有界自然數MSet

回答

相關問題