The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 07/23/2012 10:35 AM, Adam Chlipala wrote:
> On 07/23/2012 10:26 AM, Wolfram Kahl wrote:
> > However, I am still puzzled why I wasn't able to define IsSome_extract
> > starting from the inductive definition:
> >
> >   Inductive IsSome {T : Type} : option T ->  Prop :=
> >   |  isSome : forall (r : T), IsSome (Some r).
> >
> > This definition is used throughout in the remainder of this message.
> > I want to have IsSome_extract, and try:
> >
> >   Definition IsSome_extract : forall {A : Type} {x : option A} (xS : 
> > IsSome x) , A :=
> >    fun {A : Type} {x : option A} (xS : IsSome x) =>  match x with
> >       | None =>  match xS return A with
> >                 end
> >       | Some a =>  a
> >     end.
>
> It's a good thing that Coq rejects this definition, since _any_ 
> definition of [IsSome_extract] would be breaking basic rules about 
> what [Prop] means, and could even lead to logical inconsistency! ;)
>
> A type in [Prop] is meant to have no computational content, and yet 
> here you are trying to extract a potentially computational value out 
> of one of these.

OK, so here's my second attempt at a full answer: The phenomenon above 
is indeed what's going wrong in your example, though it (I now see) does 
not rule out writing a nice computational definition of 
[IsSome_extract].  You just need to express your contradiction solely 
within [Prop], and then you can do case analysis on a proof of [False], 
which is allowed because the universe restriction on [match] is waived 
for inductive types with at most one constructor, satisfying certain 
constraints.  (This is how [False_rect] is defined, and I think that 
writing the [match] directly is clearer.)

(**)
Lemma IsSome_None : forall {T}, IsSome (T := T) None -> False.
  inversion 1.
Qed.

Definition IsSome_extract {A : Type} {x : option A} : IsSome x -> A :=
  match x with
    | Some x => fun _ => x
    | None => fun H => match IsSome_None H with end
  end.
(**)