The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

Hi Peter,

"eq1" is a so called singleton definition, see:


https://coq.inria.fr/distrib/current/refman/Reference-Manual006.html#singleton

A singleton definition is inductive type that only has one constructor, 
and all arguments of that constructor are of type Prop. The elimination 
rules for singleton definitions are more liberal, they allow you to 
eliminate into Type. Note that your eq2 is not a singleton definition, 
but eq1 is.

Note that this does not endanger program extraction since inhabitants of 
a singleton definition do not carry informative information.

Robbert

On 03/02/2016 08:06 PM, Peter Vanderbilt wrote:
> Consider the following definitions (where type eq1 is the same as the
> built-in equality, eq):
>
> Inductive eq1 {A:Type} (a:A) : A -> Prop := refl1 : eq1 a a.
>
> Inductive eq2 {A: Type} : A -> A -> Prop := refl2 a : eq2 a a.
>
> Inductive eq3 {A: Type} : A -> A -> Type := refl3 a : eq3 a a.
>
> I’m surprised that Coq generates recursion principles (eq1_rect and
> eq1_rec) for eq1 even though it’s a Prop.
>
> As expected, there are recursion principles for eq3, but, not being a
> Prop, it can’t play with other Props (like it can’t be in a
> conjunction).
>
> As expected, eq2 can play with other Props, but there’s only an
> induction principle, eq2_ind, so it can’t be used in
> non-Prop-returning expressions.
>
> But eq1 can play with other Props and can be used in
> non-Prop-returning expressions.  For instance:
>
> Definition tr1 {A : Type} (B : A->Type) {x y : A} (p : eq1 x y) : B x
> -> B y := eq1_rect _ x (fun y => B x -> B y) (fun b => b) y p.
>
> Isn’t this a problem for program extraction?  Doesn’t extraction
> erase Prop-valued terms?
>
> What is it about the definition of eq1 that signals Coq to generate a
> recursion principle? Is it that eq1 has one constructor with no
> arguments and, so, it carries no information?
>
> Is there a way to make a definition of the form of eq2 & eq3 be a
> Prop with recursion principles?
>
> I’m using “Coq 8.5 (January 2016)”.
>
> Pete