The Coq mailing list

[Gert Smolka <smolka AT ps.uni-saarland.de>]

Thanks Adam, you made my day.

So the trick is to formulate the inversion
lemma with a match so that it type checks.

Inductive Fin : nat -> Type :=
| FinO : forall n, Fin (S n)
| FinS : forall n, Fin n -> Fin (S n).

Lemma Fin_inversion {n : nat} (k : Fin n) :
match n as z return Fin z -> Prop with
| 0 => fun k => False
| S n' => fun k =>  k = FinO n' \/ exists k', k = FinS n' k'
end k.
Proof. destruct k. tauto. right. exists k. reflexivity. Qed.

Lemma Fin1 (k : Fin 1) :
k = FinO 0.
Proof. destruct (Fin_inversion k) as [A|[k' A]]. exact A.
contradiction (Fin_inversion k'). Qed.


Am 28.06.2011 17:11, schrieb Adam Chlipala:
> Definition out n (k : Fin n) :=
>   match k in Fin n return match n return Fin n -> Type with
>                             | O => fun _ => Empty_set
>                             | S n' => fun k => {k' | k = FinS _ k'} + 
> {k = FinO _}
>                           end k with
>     | FinO _ => inright _ (refl_equal _)
>     | FinS _ _ => inleft _ (exist _ _ (refl_equal _))
>   end.
>
> Definition Fin1 (k : Fin 1) : k = FinO 0 :=
>   match out _ k with
>     | inleft (exist k' _) => match out _ k' with end
>     | inright pf => pf
>   end.