The Coq mailing list

[Cédric <sedrikov AT gmail.com>]

Le Sun, 03 Aug 2014 17:47:10 +0200, Jonathan 
<jonikelee AT gmail.com>
 a écrit:

> I thought that just the kind of goal (Prop vs, non-Prop), along with the  
> particulars of a specific Prop (single constructor/no info vs  
> otherwise), determine whether or not that Prop can be analyzed in a  
> context.  But then I stumbled on this (works in the trunk):
>
> Goal forall (A : Prop) (P : A -> Prop),
>      (exists x, P x) -> {x : A | P x }.
> intros A P H.
> destruct H. eexists. exact H.
> Qed.
>
>
> Goal forall (A : Prop) (P : A -> Prop),
>       (exists x, P x) -> nat.
> intros A P H.
> Fail destruct H.
> Abort.
>
> What is so different about a nat vs. a sig that allows the analysis of  
> the ex H in the sig goal but not the nat goal?
>
> More importantly, why prevent the destruct in the nat goal if it is  
> allowed in the sig goal?

Compare these variants, and you will probably have your answer.

Goal forall (A : Prop) (P : A -> Prop),
     (exists x, P x) -> ({x : A | P x } : Prop).
intros A P H.
destruct H. eexists. exact H.
Qed.

Goal forall (A : Prop) (P : A -> Prop),
     (exists x, P x) -> ({x : A | P x } : Type).
intros A P H.
destruct H. eexists. exact H.
Qed.


=====================
Coq has a non obvious system to tell what is in Prop and what is in Type.

> -- Jonathan


--
---
Cédric AUGER