The Coq mailing list

[Keiko Nakata <keiko AT kurims.kyoto-u.ac.jp>]

Hello, 

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

The following two variations are fine: 

1) Avoid the use of case: 

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.
intros l0 l1 h1. inversion h1. apply nil_eq.
Qed.

2) Change the kind of list from Prop to Set:

Inductive list: Set :=
| 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.
subst. apply nil_eq.
Qed. 


==
Best,
Keiko