The Coq mailing list

[AUGER Cédric <Cedric.Auger AT lri.fr>]

Le Thu, 22 Dec 2011 12:25:02 +0100,
Damien Pous 
<Damien.Pous AT inria.fr>
 a écrit :

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

unless you use a set not built from the interface.

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

Not at all, you can have clever implementations avoiding that (but
maybe not always easy to use).

For instance, using my version of PositiveMap, I could define
PositiveSet as:

Inductive tree :=
| FilledBucket : option tree -> option tree -> tree
  (*meaning that there is the "xH" positive in this node*)
| EmptyBucketL : tree -> tree
  (*meaning that there is no even positive from this node,
    and that there is some odd positive*)
| EmptyBucketR : tree -> tree
  (*meaning that there is no odd positive from this node,
    and that there is some even positive*)
| EmptyBucketLR : tree -> tree -> tree
  (*meaning that you have even and odd positives from this node*)
.

Inductive postiveset := option tree.

Such a type ensures unicity of representations, and furthermore, it
doesn't need any dependant type, and is extracted as identity both in
Ocaml and Haskell

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