Ssreflect Users Discussion List

[Georges Gonthier <>]

   Hello,

    Ssreflect currently doesn't have exactly what you want, but then what you 
want isn't exactly possible. The current library does, however, supply 
several approximate solutions to your need.
    If you're interested in the computational contents, but don't require
mathematical sets (with logical equality), then you can simply use sequences 
(type seq). Most of the lemmas you're interested in are in seq.v. In 
particular, there's a theory of lists as multisets (based on the perm_eq 
predicate), a uniq predicate that identifies sets, and an undup function that 
projects multisets on sets.
   If you want true mathematical sets, then the library supplies sets based 
on a finType, i.e., expect you to bound the range of sets that are combined 
together. The rationale is that this is usually not a problem, and it makes 
the library much easier to use, because it supports naïve set theory. Havinge 
finite sets within an infinite domain means each set object must carry its 
own bound, which is not as convenient as putting the bound in the element 
type.
   Possible alternative would be to base sets on a choiceType and quotient
the list type above in order to regain Leibnitz equality (we're developping a 
generic way of doing that), or on an ordered eqType and sorted sequences (the 
theory for the latter can be found in paths.v). I believe Aleks Nanevski has 
something along the latter lines, and Sidi Ould Biha developped last summer a 
package for CountType-based finite and cofinte sets (more precisely, it 
provided some of the inspiration for choice.v).
   Note that the computational contents for choiceType-based sets is unlikely 
to be useful as its complexity is prohibitive. Also, none of the options 
above could reduce your expression unless t and u are concrete values. Doing 
this requires reflection (à la ring/quote); we're just in the middle of 
developping the technology for that.

Cheers,

   Georges

-----Original Message-----
From: Chantal KELLER [] 
Sent: 24 June 2009 14:42
To: ssreflect
Subject: Computational finite sets over an eqType

    Hello everybody,

  I am looking for a library of finite sets that would be such that:
    - the type of the elements of the sets is an eqType
    - it is computational : for instance, I want [is_empty (remove t
(remove u (union empty (add t (singleton u)))))] to reduce to true
    - it has a few usual lemmas (typically, like in the FSetInterface
library).

  Many thanks,
    Chantal.