The Coq mailing list

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

Le Thu, 22 Dec 2011 13:07:27 +0000 (GMT),
Charles D 
<coqletsgo AT yahoo.com>
 a écrit :

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

I wasn't aware of this option, I think I will use it from now on for
non recursive inductives!

I don't think this option is here "mainly" to prevent careless users
from assuming that.
The point of having such an option is mainly:
* sometimes, the induction predicate generated is not the one you wish,
  especially in the case of mutually recursive types, where some of the
  coq users (I am not one of them, so I won't tell more on it as I am
  not an expert) prefer to use "Induction Scheme", so we may wish to
  tell Coq, not to generate such a principle, and use the one we prefer
  instead. (Although I am not a user of "Induction Scheme", I could
  also deactivate it for mutually recursive types, as often, the coq
  generated principle is just useless)
But you have also:
* Your point
* The point of people doing extraction:

Module Bool.
 Inductive bool := True | False.
End Bool.

Extraction Bool.
(*
If Elimination Schemes is set:
module Bool = 
 struct 
  type bool =
  | True
  | False
  
  (** val bool_rect : 'a1 -> 'a1 -> bool -> 'a1 **)
  
  let bool_rect f f0 = function
  | True -> f
  | False -> f0
  
  (** val bool_rec : 'a1 -> 'a1 -> bool -> 'a1 **)
  
  let bool_rec f f0 = function
  | True -> f
  | False -> f0
 end
else:
module Bool = 
 struct 
  type bool =
  | True
  | False
 end
*)

I guess that no one would want "bool_rec" and "bool_rect" to "polute"
their code, since it will never be used (unless you use them
explicitly in your definitions, or if you build a term using tactics
[hardly ever wise] using induction [I never do so when my type is not
a recursive one]).

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