The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 08/03/2014 07:28 PM, Cédric wrote:
> Le Sun, 03 Aug 2014 20:01:06 +0200, Jonathan <jonikelee AT gmail.com> a 
> écrit:
>
> > 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…

I was just wondering if someone could state the rules in some consistent 
way, by which I mean there are no rules that appear to prevent something 
(destruct an uninformative ex in a non-Prop context) when actually they 
don't (rewrite it to a sig, then destruct it) - which just creates 
confusion.  It would certainly be nice if the rule was simply that 
anything at all that contains no information can be case analyzed in any 
context.  I would even argue that things like "False \/ P" should be 
case analyzable in any context - because (and, of course) it can be 
turned into P by use of assert, applying a lemma or a rewrite.  
Although, perhaps in the general case whether or not such a thing 
contains information isn't computable.  What if there was some 
meta-predicate "uninformative" that one could first prove on a specific 
instance and then use later to case analyze that instance?  Or, separate 
Prop into IProp (informative props, like P \/ Q) and UProp 
(uninformative props, like False \/ P), where Prop is the 
undecidably-disjoint union of those?  But this is much ado about ... 
well ... nothing.  Other than linguistic consistency.

-- Jonathan