Coq MSet de naturels bornés

Question

J'essaye de définir un type pour l'ensemble des nombres naturels avec la limite supérieure donnée. MSet de la bibliothèque standard semble être une voie à suivre. J'ai trouvé this discussion qui donne un bel exemple de la façon de définir un ensemble de nat. Cependant je ne peux pas comprendre comment l'étendre aux types de sous-ensembles. J'ai essayé quelque chose comme ceci:

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

Je vais travailler avec des ensembles avec différentes limites supérieures. Mais je ne vois pas comment instancier ce module avec un 'n' donné. Idéalement, j'aimerais pouvoir écrire quelque chose comme ceci:

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

P.S. Cette question est probablement ancrée dans ma compréhension insuffisante du système de modules Coq, et non spécifique aux Sets.

Answer 1

Vous devez utiliser un foncteur. Quelque chose comme:

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. 

Vous pouvez ensuite appliquer OWL aux modules de signature FIXED_NAT.

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

Module OWL1 := OWL N1. 

Require Import MSets. 

Module M1 := Make OWL1. 

EDIT: Qu'en est-:

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