The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 08/03/2014 12:02 PM, Pierre-Marie Pédrot wrote:
> On 03/08/2014 17:47, Jonathan wrote:
> > 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?
> This is due to a weak form of universe polymorphism of the old
> inductives. In your case, the sig that usually lives in Type collapse
> into Prop because all of its arguments are from Prop.
>
> Variable A : Prop.
> Variable P : A -> Prop.
>
> Check {x : A | P x}.
>
> {x : A | P x} : Prop
>
> I do not know if this is documented somewhere, but this phenomenon
> occurs with all inductives which do not provide a relevant content
> whenever their parameters are instantiated with Prop-living types. This
> is the case with one-constructor inductives, like sig, prod & eq.
> PMP

So, what exactly is not being able to destruct H in the nat goal 
preventing, when I can just do this:

Goal forall (A : Prop) (P : A -> Prop),
     (exists x, P x) -> nat.
intros A P H.
Fail destruct H.
assert ({x : A | P x}) as H' by (destruct H; eexists; exact H).
destruct H'.

I could even write a rewrite rule:

Lemma ex2sig: forall (A : Prop) (P : A -> Prop),
    (exists x, P x) <-> {x : A | P x}.
intros A P.
split.
intro H. destruct H. eexists. exact H.
intro H. destruct H. eexists. exact p.
Qed.

Require Setoid.

Goal forall (A : Prop) (P : A -> Prop),
     (exists x, P x) -> nat.
intros A P H.
Fail destruct H.
rewrite ex2sig in H.
destruct H.
Abort.

-- Jonathan