The Coq mailing list

["St�phane Lescuyer" <lescuyer AT lri.fr>]

As far as I know, subst only deals with Leibniz equalities (Logic.eq),
Im using it to remove the equalities introduced by the inversion
tactic. I've never encountered the issue you describe before (I'm
using the trunk version, but I dont know if it makes any difference).
In particular, the reason I use an alternate name "eq_" instead of
"eq" directly is not to avoid any name clash with the standard "eq",
but because of a (harmless, yet annoying) limitation that prevents one
from instantiating a Parameter in a module by an Inductive (hence the
use of "eq_" and the redefinition of "eq" afterwards).

SL

On Wed, Nov 26, 2008 at 9:07 PM, M. Scott Doerrie 
<mdoerri AT cs.jhu.edu>
 wrote:
> 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.
>>
>>
>>
>
> --------------------------------------------------------
> Bug reports: http://logical.futurs.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>         http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>



-- 
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06