coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Adam Chlipala <adamc AT hcoop.net>
- To: Keiko Nakata <keiko AT kurims.kyoto-u.ac.jp>
- Cc: coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club] case & inversion, Set & Prop
- Date: Thu, 06 Aug 2009 08:53:39 -0400
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Keiko Nakata wrote:
I have been confused by different behaviour of case and inversion tactics,
when I moved from Set to Prop. Will someone please explain?
In the following code, the last "inversion h1" is not helpful at all.
Inductive list: Prop :=
| nil: nat -> list.
Inductive list_eq: list -> list -> Prop :=
| nil_eq: forall n, list_eq (nil n) (nil n).
Lemma inversion_list: forall l0 l1, list_eq l0 l1 -> list_eq l1 l0.
Proof.
intro l0. case l0. intro n0. intro l1. case l1. intro n1. intro h1. inversion h1. (* This changes nothing, so I've got stuck.)
There's a generic way of answering this kind of question. For this case, you can run the following with [list] in [Set]:
====
Lemma invert : forall n1 n2, list_eq (nil n1) (nil n2) -> n1 = n2.
inversion 1; reflexivity.
Qed.
Print invert.
====
Now you know how [invert] wants to prove this goal. You can try to type-check this exact proof term after moving [list] to [Prop]. I get this error message:
====
Incorrect elimination of "e" in the inductive type "list":
the return type has sort "Set" while it should be "Prop".
Elimination of an inductive object of sort Prop
is not allowed on a predicate in sort Set
because proofs can be eliminated only to build proofs.
====
Inspecting the proof term, we see that this error message is essentially complaining about the inability to write a function that extracts a [nat] from a [list], by picking out the argument to [nil].
- [Coq-Club] case & inversion, Set & Prop, Keiko Nakata
- Re: [Coq-Club] case & inversion, Set & Prop, Adam Chlipala
- Re: [Coq-Club] case & inversion, Set & Prop,
Keiko Nakata
- Re: [Coq-Club] case & inversion, Set & Prop, Adam Chlipala
- Re: [Coq-Club] case & inversion, Set & Prop,
Keiko Nakata
- Re: [Coq-Club] case & inversion, Set & Prop,
Taral
- Re: [Coq-Club] case & inversion, Set & Prop,
Keiko Nakata
- Re: [Coq-Club] case & inversion, Set & Prop,
Adam Chlipala
- Re: [Coq-Club] case & inversion, Set & Prop,
Keiko Nakata
- Re: [Coq-Club] case & inversion, Set & Prop,
Adam Chlipala
- Re: [Coq-Club] case & inversion, Set & Prop,
Keiko Nakata
- Re: [Coq-Club] case & inversion, Set & Prop, Adam Chlipala
- Re: [Coq-Club] case & inversion, Set & Prop,
Keiko Nakata
- Re: [Coq-Club] case & inversion, Set & Prop,
Adam Chlipala
- Re: [Coq-Club] case & inversion, Set & Prop, Keiko Nakata
- Re: [Coq-Club] case & inversion, Set & Prop,
Keiko Nakata
- Re: [Coq-Club] case & inversion, Set & Prop,
Adam Chlipala
- Re: [Coq-Club] case & inversion, Set & Prop,
Keiko Nakata
- Re: [Coq-Club] case & inversion, Set & Prop, Adam Chlipala
Archive powered by MhonArc 2.6.16.