Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] How can eq be a Prop yet have a recurse?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] How can eq be a Prop yet have a recurse?


Chronological Thread 
  • From: Robbert Krebbers <mailinglists AT robbertkrebbers.nl>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] How can eq be a Prop yet have a recurse?
  • Date: Thu, 3 Mar 2016 10:17:53 +0100
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=mailinglists AT robbertkrebbers.nl; spf=None smtp.mailfrom=mailinglists AT robbertkrebbers.nl; spf=None smtp.helo=postmaster AT smtp1.science.ru.nl
  • Ironport-phdr: 9a23:AczSeRAtht+OGwBjSnm6UyQJP3N1i/DPJgcQr6AfoPdwSP7+pMbcNUDSrc9gkEXOFd2CrakU1KyJ6Ou5AzNIyK3CmU5BWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYsExnyfTB4Ov7yUtaLyZ/niKbtoNaKOVoArQH+SI0xBS3+lR/WuMgSjNkqAYcK4TyNnEF1ff9Lz3hjP1OZkkW0zM6x+Jl+73YY4Kp5pIYTGZn9Kq8/VPlTCCksG2Ez/szi8xfZHiWV4X5JaGIcmBdSH0Dm9hzwVJrrqWOus+N83CicMsn3VqwvcS6l5a1mUgPrkioNPTMj6yfRjpoj3+pgvBu9qkknkMbva4aPOa8mcw==

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





Archive powered by MHonArc 2.6.18.

Top of Page