The Coq mailing list

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

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.

Putting the definition in [Type] instead, everything goes through quite 
naturally.  I don't know why you're proceeding by case analysis on [x] 
instead of [xS], which is much more direct.

(**)
Inductive IsSome {T : Type} : option T -> Type :=
| isSome : forall (r : T), IsSome (Some r).

Definition IsSome_extract {A : Type} {x : option A} (xS : IsSome x) : A :=
  let (v) := xS in v.
(**)