The Coq mailing list

[Frederic Blanqui <frederic.blanqui AT inria.fr>]

Thank you Yves for your remark about termination. But my question was 
not exactly about that. It was about the theoretical justification of 
what is described in coq-8.2-refman/Reference-Manual006.html. I cannot 
remember in which paper this is explained :-(

------------------coq-8.2-refman/Reference-Manual006.html:

The case of Inductive definitions of sort Prop is a bit more 
complicated, because of our interpretation of this sort. The only 
harmless allowed elimination, is the one when predicate P is also of 
sort Prop.

Prop
    [I:Prop|I→Prop]

Prop is the type of logical propositions, the proofs of properties P in 
Prop could not be used for computation and are consequently ignored by 
the extraction mechanism. Assume A and B are two propositions, and the 
logical disjunction A∨ B is defined inductively by :
Coq < Inductive or (A B:Prop) : Prop :=
Coq <   lintro : A -> or A B | rintro : B -> or A B.

The following definition which computes a boolean value by case over the 
proof of or A B is not accepted :
Coq < Definition choice (A B: Prop) (x:or A B) :=
Coq <    match x with lintro a => true | rintro b => false end.
Coq < Coq < Error:
Incorrect elimination of "x" in the inductive type "or":
the return type has sort "Set" while it should be "Prop".
Elimination of an inductive object of sort Prop
is not allowed on a predicate in sort Set
because proofs can be eliminated only to build proofs.

From the computational point of view, the structure of the proof of (or 
A B) in this term is needed for computing the boolean value.

In general, if I has type Prop then P cannot have type I→ Set, because 
it will mean to build an informative proof of type (P m) doing a case 
analysis over a non-computational object that will disappear in the 
extracted program. But the other way is safe with respect to our 
interpretation we can have I a computational object and P a 
non-computational one, it just corresponds to proving a logical property 
of a computational object.

In the same spirit, elimination on P of type I→ Type cannot be allowed 
because it trivially implies the elimination on P of type I→ Set by 
cumulativity. It also implies that there is two proofs of the same 
property which are provably different, contradicting the 
proof-irrelevance property which is sometimes a useful axiom :
Coq < Axiom proof_irrelevance : forall (P : Prop) (x y : P), x=y.
proof_irrelevance is assumed

The elimination of an inductive definition of type Prop on a predicate P 
of type I→ Type leads to a paradox when applied to impredicative 
inductive definition like the second-order existential quantifier exProp 
defined above, because it give access to the two projections on this type.
Empty and singleton elimination

There are special inductive definitions in Prop for which more 
eliminations are allowed.

Prop-extended
        
    I  is an empty or singleton definition   s ∈  S
    [I:Prop|I→ s]

A singleton definition has only one constructor and all the arguments of 
this constructor have type Prop. In that case, there is a canonical way 
to interpret the informative extraction on an object in that type, such 
that the elimination on any sort s is legal. Typical examples are the 
conjunction of non-informative propositions and the equality. If there 
is an hypothesis h:a=b in the context, it can be used for rewriting not 
only in logical propositions but also in any type.
Coq < Print eq_rec.
eq_rec =
fun (A : Type) (x : A) (P : A -> Set) => eq_rect x P
     : forall (A : Type) (x : A) (P : A -> Set),
       P x -> forall y : A, x = y -> P y
Argument A is implicit
Argument scopes are [type_scope _ _ _ _ _]

Coq < Extraction eq_rec.
(** val eq_rec : ’a1 -> ’a2 -> ’a1 -> ’a2 **)
let eq_rec x f y =
  f

An empty definition has no constructors, in that case also, elimination 
on any sort is allowed.