The Coq mailing list

["gallais @ ensl.org" <guillaume.allais AT ens-lyon.org>]

Hu?

Lemma IsSome_extract : forall A (x : option A), IsSome x -> { r | x = Some r 
}.
Proof.
intros A x Hx ; destruct x.
 exists a ; reflexivity.
 apply False_rect.
  inversion Hx.
Qed.

--
gallais


On 23 July 2012 15:35, Adam Chlipala 
<adamc AT csail.mit.edu>
 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.
>
> 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.
> (**)
>