The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Keiko Nakata wrote:
> Thank you for the prompt and instructive answer. 
> But my understanding is still partial :(
>
> The following code works fine: 
>
> Inductive list: Prop :=
> | nil: nat -> list.
>
> Inductive list_eq: list -> list -> Prop :=
> | nil_eq: forall n, list_eq (nil n) (nil n).
>
> Lemma invert_again: forall l0 l1, list_eq l0 l1 -> l1 = l0.
> Proof.
> inversion 1; reflexivity.
> Qed.
>
> I do not know where is the crucial difference in proof terms of your "invert"
> and my "invert_again".
>   

Well, the error message from my last posting indicated a problem with 
writing function to extract the argument to [nil].  Your [invert_again] 
doesn't need to look inside lists in this way, because it only talks 
about lists, not numbers.

It's hard to give a precise and intuitive answer.  The best I can 
suggest is printing the proof term for [invert_again], too, and 
comparing with the proof term I [Print]ed in my last message.  You 
should at least see the presence of a [nat]-grabbing function in the old 
version and the absence of such a function in your new version.