The Coq mailing list

[Charles D <coqletsgo AT yahoo.com>]

So if I understand it correctly, the "Local Unset Elimination Schemes" is 
there mainly to prevent careless users from assuming both equalities 
(extensional and Leibniz) coincide? Or is there a deeper reason for that?




----- Original Message -----
From: Damien Pous 
<Damien.Pous AT inria.fr>
To: coq-club 
<coq-club AT inria.fr>
Cc: 
Sent: Thursday, December 22, 2011 12:25 PM
Subject: Re: [Coq-Club] Decidable equality on PositiveSets

Hi,

Yes and no :
- the remove function normalizes trees, so that in practice, the only
empty tree should be "Leaf" ;
- we did not need extensional equality to coincide with Leibniz
equality, so that we did not enforce this constraint.

This means that :
- you won't be able to prove that the two equalities coincide (they
don't, although they do on all objects you create through the
FSetInterface) ;
- the [equal] and [is_empty] functions have to handle the case where
they are given ill-formed trees (although the corresponding code will
never be executed in practice).

Enforcing the invariant and staying within the FSetInterface bounds
would require sig-types (like for, e.g., FSetList, FSetAVL...), which
introduce an overhead when using the data-structure for reflection
(vm_compute).

Damien



When we wrote this code

2011/12/21 AUGER Cédric 
<Cedric.Auger AT lri.fr>:
> Le Wed, 21 Dec 2011 09:43:15 +0000 (GMT),
> Coq Dev 
>Â <coqletsgo AT yahoo.com>
>  a écrit :
>
>> Could someone please indicate me some texts (perhaps some basic ones)
>> that could help explain the following behavior?
>>
>> Import MSetPositive.
>> Lemma l: forall (p p' : PositiveSet.t), {p = p'} + {p <> p'}.
>> Proof.
>>   induction p.
>>
>> Error: Cannot find the elimination combinator tree_rec, the
>> elimination of the inductive definition PositiveSet.tree on sort Set
>> is probably not allowed.
>>
>>
>
> By the way, I haven't read what the PositiveSet.t implementation is,
> but know that it may not be what you expect, that is you may have two
> sets wich are extensionnaly equal, but not intensionnaly.
>
> It is the case for the implementation of PositiveMap AFAIK:
> it is implemented with PATRICIA trees; but the implementation doesn't
> give unique representations; for example:
>
> empty:= (Node None None None)
> add 1 tt empty := (Node None (Node None None (Some tt)) None)
> remove (add 1 tt empty) 1 := (Node None (Node None None None) None),
>
> that is the result is not necessarily normalized, and even if it were,
> you have no information in general when you have a set if it is or not
> normalized.
>
> I already wrote a version with some tricks to have unicity of
> representations using a variation of the same structure;
> so I had a theorem, that if equality is decidable for elements, then
> equality is decidable for maps.
>