The Coq mailing list

[Peter Vanderbilt <acm AT petervanderbilt.com>]

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