The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

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].