coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] How to make Coq ``see'' emptyness of inductively defined Props?, Wolfram Kahl, 07/23/2012
- Re: [Coq-Club] How to make Coq ``see'' emptyness of inductively defined Props?, Adam Chlipala, 07/23/2012
- Re: [Coq-Club] How to make Coq ``see'' emptyness of inductively defined Props?, Adam Chlipala, 07/23/2012
- Re: [Coq-Club] How to make Coq ``see'' emptyness of inductively defined Props?, Adam Chlipala, 07/23/2012
- Re: [Coq-Club] How to make Coq ``see'' emptyness of inductively defined Props?, gallais @ ensl.org, 07/23/2012
- Re: [Coq-Club] How to make Coq ``see'' emptyness of inductively defined Props?, Wolfram Kahl, 07/23/2012
- Re: [Coq-Club] How to make Coq ``see'' emptyness of inductively defined Props?, Adam Chlipala, 07/23/2012
- Re: [Coq-Club] How to make Coq ``see'' emptyness of inductively defined Props?, Wolfram Kahl, 07/23/2012
- Re: [Coq-Club] How to make Coq ``see'' emptyness of inductively defined Props?, gallais @ ensl.org, 07/23/2012
- Re: [Coq-Club] How to make Coq ``see'' emptyness of inductively defined Props?, Wolfram Kahl, 07/23/2012
- Re: [Coq-Club] How to make Coq ``see'' emptyness of inductively defined Props?, gallais @ ensl.org, 07/23/2012
- Re: [Coq-Club] How to make Coq ``see'' emptyness of inductively defined Props?, Paolo Herms, 07/23/2012
- Re: [Coq-Club] How to make Coq ``see'' emptyness of inductively defined Props?, Adam Chlipala, 07/23/2012
- Re: [Coq-Club] How to make Coq ``see'' emptyness of inductively defined Props?, Wolfram Kahl, 07/23/2012
- Re: [Coq-Club] How to make Coq ``see'' emptyness of inductively defined Props?, Adam Chlipala, 07/23/2012
- Re: [Coq-Club] How to make Coq ``see'' emptyness of inductively defined Props?, Wolfram Kahl, 07/23/2012
- Re: [Coq-Club] How to make Coq ``see'' emptyness of inductively defined Props?, Adam Chlipala, 07/23/2012
Archive powered by MHonArc 2.6.18.