The Coq mailing list

[Cody Roux <Cody.Roux AT loria.fr>]

Hello Matej


   There are many trivial functions you can define from types of kind
Prop to types of kind Set, for example

fun x:True => 3 : True -> nat

Unfortunately, for more interesting functions you run into a famous
problem: the "elimination of Prop into Set problem" discussed a certain
number of times on this mailing list. For reasons related to proof
irrelevance, it is illegal to de-construct an inductive term of type
P:Prop in order to contruct a term of type S:Set. This, as well as a
certain number of possible solutions, is discussed in the Coq'Art book
in section 14.2 (p394).

  As an example, take the sample coq code:

Require Import List.

Variable A:Set.


Inductive not_empty:list A -> Prop:=
|ne_cons: forall a l, not_empty (a::l).


Variable l:list A.

Definition safe_head: not_empty l -> A.
intros.
destruct H.
exact a.
Defined.

This fails at "destruct H" for exactly this reason. This is why it is
difficult to define functions of type A->B, with A:Prop and B:Set.

Cheers,

Cody


On Wed, 2009-04-15 at 12:35 +0200, Matej Kosik wrote:
> Hello,
> 
> I have started to read the Coq-book
> (Interactive Theorem Proving and Program Development)
> 
> The general shape of the Prod(s,s',s'') rule is stated
> on page 91 as:
> 
>         E,Γ |- A:s      E,Γ::(a:A) |- B:s'
>         ----------------------------------
>             E,Γ ⊦ ∀a:A,B:s''
> 
> One of the trivial cases whose description was left out from the book is
> this:
> s = Prop
> s' = s'' = Set
> 
>         E,Γ |- A:Prop      E,Γ::(a:A) |- B:Set
>         ----------------------------------
>             E,Γ |- ∀a:A,B:Set
> 
> or perhaps the special case were
> `a' does not occur free in `B':
> 
>         E,Γ |- A:Prop      E,Γ |- B:Set
>         ----------------------------------
>             E,Γ |- A->B:Set
> 
> Is it possible to give some meaningful examples of terms that can be
> constructed this way?
> 
> Thanks in advance for advice.
> 
> --------------------------------------------------------
> Bug reports: http://logical.saclay.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club