The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi,

You basically exhausted the elementary bricks of types for which
singleton elimination is allowed:

recursivity: Acc
tuples: True, and
indices: eq
emptyness: False

Indeed, indices is where finer discriminating criteria can be thought of.

Hugo Herbelin

On Sun, Jan 22, 2012 at 02:33:48PM -0800, Michael Shulman wrote:
> Hi,
> 
> I am looking for examples of the use of Coq's "singleton elimination"
> feature for eliminating out of inductive Props into non-Prop types.
> The canonical examples seem to be equality 'eq' and the accessibility
> predicate 'Acc' used in defining wellfoundedness.  I guess there are
> also True, False ("singleton elimination" also applies to inductive
> Props with no constructors), and the conjunction of two propositions.
> I would be interested to hear of any other examples, from any source.
> 
> (Context: under a homotopical interpretation, if Prop were to be
> replaced by a universe of h-propositions, then singleton elimination
> would no longer be valid for 'eq' (except over domains that are
> h-sets), but it would still be valid for 'Acc' and for the more
> trivial examples.  It would be nice to have more examples against
> which to test a general principle of which singleton eliminations
> remain valid.)
> 
> Thanks!
> Mike