Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] case & inversion, Set & Prop

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] case & inversion, Set & Prop


chronological Thread 
  • 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].





Archive powered by MhonArc 2.6.16.

Top of Page