The Coq mailing list

[Maxime Dénès <mail AT maximedenes.fr>]

I take it back. Singleton elimination does not apply here because A is 
unknown.

So it is probably indeed sort polymorphism, but the type annotation 
doesn't seem to have any effect.

Maxime.

On 08/03/2014 12:17 PM, Maxime Dénès wrote:
> I think this is actually a bug of destruct. The following works:
>
> Goal forall (A : Prop) (P : A -> Prop),
>      (exists x, P x) -> ({x : A | P x } : Type).
> intros A P H.
> refine (match H with ex_intro _ a p => _ end).
> exists a. exact p.
> Qed.
>
> I don't think this example is directly connected to sort polymorphism.
> The reason why this is allowed is the so-called singleton elimination 
> rule. Of course, it relies critically on the fact that A is in Prop.
>
> Maxime.
>
> 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.
> >
> >
> > =====================
> > Coq has a non obvious system to tell what is in Prop and what is in 
> > Type.
> >
> > > -- Jonathan