The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 08/03/2014 12:02 PM, Cédric wrote:
> 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.


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

!
?

-- Jonathan