The Coq mailing list

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

Le Sun, 03 Aug 2014 20:01:06 +0200, Jonathan 
<jonikelee AT gmail.com>
 a écrit:

> 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


Well, "sig" is declared to be of type "forall A, (A -> Prop) -> Type", so  
it is not very surprising that a ({x : A | P x} : Prop) can be cast into a  
({x : A | P x} : Type).

What could be surprising is that ({x : A | P x} : Prop) is accepted. I  
know that this is not a bug, as this is something known and intended, but  
that is so unnatural for me…

It is like promotion of the unit type to Prop. Although you declare it in  
Type, it lives in Prop:

Inductive unit : Type := tt.
Goal unit : Prop.
exact tt.
Qed.

Inductive bool : Type := true | false.
Goal bool : Prop.


I know that it is legit, as it contains no information, but still, that  
tends to make things non obvious…


--
---
Cédric AUGER