The Coq mailing list

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

"move into Prop" refers to moving away from a goal [A]
(or [{ r | Some x = r}] in my example) which is in Type to
a goal in Prop ([False]).

There are a few cases where elimination of something
in Prop when trying to build something in Type is allowed:
http://coq.inria.fr/doc/Reference-Manual006.html#singleton

Basically when what you get from this elimination is:
- still in Prop and there's only one case (e.g. accessibility
predicates to define something by well-founded induction)
- nothing (because there are no constructors at all for this
proposition)

--
gallais


On 23 July 2012 17:06, Wolfram Kahl 
<kahl AT cas.mcmaster.ca>
 wrote:
> 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
>
>
>
>