Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] How to make Coq ``see'' emptyness of inductively defined Props?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] How to make Coq ``see'' emptyness of inductively defined Props?


Chronological Thread 
  • From: Wolfram Kahl <kahl AT cas.mcmaster.ca>
  • To: Adam Chlipala <adamc AT csail.mit.edu>
  • Cc: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] How to make Coq ``see'' emptyness of inductively defined Props?
  • Date: Mon, 23 Jul 2012 12:06:42 -0400

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







Archive powered by MHonArc 2.6.18.

Top of Page