The Coq mailing list

[Wolfram Kahl <kahl AT cas.mcmaster.ca>]

Still in the context of:
 >>
 >>  Inductive IsSome {T : Type} : option T ->  Prop :=
 >>  |  isSome : forall (r : T), IsSome (Some r).
 >>
, on Mon, Jul 23, 2012 at 11:56:59AM -0400, Adam Chlipala wrote:
 > On 07/23/2012 11:43 AM, Wolfram Kahl wrote:
 > >``gallais'' wrote:
 > >
 > >  >  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.
 > >
 > >(That additional equation is indeed essential, and I also had produced
 > >  it for the other definition in the meantime.)
 > >I found it surprising that ``inversion Hx'' works here,
 > >while in my attempt (without the False_rect of gallais),
 > >it produces a sort error.
 > >   
 > 
 > The key is that he first applied [False_rect] to move into [Prop].  

Since [IsSome None : Prop] I am puzzled; what does ``move into [Prop]'' mean 
here?


> (This is exactly the Curry-Howard analogue of my advice.)

Does this mean that [False_rect] is the only proof term constructor
that eliminates empty [Prop]s?


> P.S.: I really advise _not_ using tactics to build dependently typed 
> definitions with computational content.

I know, and I didn't really want to do it either,
but I thought I stood a better chance there
since my ``obviously empty'' match was not accepted...


Thanks again,

Wolfram