The Coq mailing list

[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.