The Coq mailing list

["M. Scott Doerrie" <mdoerri AT cs.jhu.edu>]

Thanks.  I'd started with a similar approach, but have stopped as I can 
use FSets for now.  However, I noticed that you used a tactic that works 
for you but not me.  I can't use the "subst" tactic, as it claims 
unification is impossible.  However, I am reusing the "eq" name from the 
module instead of using "_eq" as you do.  I changed the name to 
something other than "eq" and the tactic works.  Why will "subst" fail 
to unify with a local "eq" but will unify with "_eq"?  Is this a naming 
bug between local and FQ names in the tactic, or is it more fundamental?

Scott Doerrie

Stéphane Lescuyer wrote:
> On Wed, Nov 26, 2008 at 5:38 PM, Pierre Letouzey
> <Pierre.Letouzey AT pps.jussieu.fr>
>  wrote:
>   
> > On Tue, Nov 25, 2008 at 02:56:21PM -0500, M. Scott Doerrie wrote:
> >     
> > > I've been searching the Coq standard library and have been unable to
> > > find a functor that creates an OrderedType given an FSet or even a List
> > > of OrderedTypes.  This seems relatively straightforward given the
> > > implementation of PairOrderedType, so I've probably missed it.  I'd
> > > rather not duplicate effort, so I thought I'd ask first.
> > >
> > > Scott Doerrie
> > >
> > >       
> > Concerning lists of OrderedType.t, FSetList.Make is building a
> > FSetInterface.S whose base type is a sorted list attached with its
> > sortedness proof. As before, this FSetInterface.S can be seen as an
> > OrderedType. If you want to deal with arbitrary lists and not only the
> > sorted ones, nothing exists yet in the standard library, but it should
> > not be too difficult to build something (indeed, PairOrderedType can
> > be a good source of inspiration). If you write this kind of functor,
> > let me know, it might be interesting to include it in the standard
> > library.
> >     
>
> I had actually written such a functor (see attached file) some time
> ago, it builds an ordered type for lists with pointwise equality and
> lexicographic order. [eq] and [lt] are defined as inductives rather
> than functions because I find inversion really convenient.
>
> Hope this helps,
>
> Stéphane L.
>
>
>