coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Can FSets be of 'Set'?

From: Jianzhou Zhao <jianzhou AT seas.upenn.edu>
To: coq-club AT inria.fr
Subject: [Coq-Club] Can FSets be of 'Set'?
Date: Tue, 9 Mar 2010 10:48:32 -0500
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:date:x-google-sender-auth:message-id:subject :from:to:content-type; b=YcPn/VGHmkOBS+tvLGkSfGxdfMLjaxTYkY0ayRKHn8/cZbsnZUi8wGGwilvxQUrXr+ rjDEFK4ooyKhn43PCCCjlCA2ofIZv+pjTlRs1tRwfW3b6Ylin49qID4UhqSl6ls3r+Vm EghypbD9EF2gLL8H86zE9aENPb7bVS4t5nih0=

Hi,

I wanted to have a set of natural numbers with the following code.

(* **************** begin ********** *)
Require Import Arith.
Require Import Bool.
Require Import List.

Require Import Coq.Logic.DecidableTypeEx.

Module NatDT <: UsualDecidableType.  (*with Definition t := nat.*)

  Definition t := nat.

  Definition eq := @eq nat.
  Definition eq_refl := @refl_equal nat.
  Definition eq_sym := @sym_eq nat.
  Definition eq_trans := @trans_eq nat.

  Definition eq_dec := eq_nat_dec.

End NatDT.

Require Import FSets FSetWeakList.

Module NSet := FSetWeakList.Make(NatDT).
Module NSetP := FSetProperties.Properties NSet.
Export NSetP.

Notation nset := NSet.t.

(*********************** end *************)

The type of 'nset' is of 'Type'. This is because
  NSet.t is 'list NSet.elt'
where NSet.elt is of 'Type', although NatDT.t, which
is assigned to NSet.elt, is of 'Set'.
'list' is of 'Type -> Type'. If a Set is given, 'list nat' is of Set.
But the module system does not seem to allow this.

Is there a way to let 'nset' be of type 'Set'?

Thanks.
--
Jianzhou

[Coq-Club] Can FSets be of 'Set'?, Jianzhou Zhao