有界自然数的 Coq MSet

Question

我正在尝试为具有给定上限的自然数集定义一个类型。标准库的 MSet 似乎是一条路要走。我发现 this discussion 给出了一个很好的例子，说明如何定义一组 nat。但是我不知道如何将它扩展到子集类型。我试过这样的事情：

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模块系统的理解不够，而不是特定于Sets。

Answer 1

你需要使用仿函数。类似于：

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}.

有界自然数的 Coq MSet

Coq MSet of bounded naturals

module

set

coq