The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Tue, Jun 28, 2011 at 9:28 AM, Gert Smolka <smolka AT ps.uni-saarland.de> wrote:

Thanks Adam, you made my day.

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

How about constructing an inversion function in a form which is easy to feed into the inversion tactic?

Definition Fin_inversion_aux (n:nat) (x:Fin n) :
  match n as n0 return (Fin n0 -> Type) with
  | 0 => fun _ => Empty_set
  | S m => fun x:Fin (S m) => forall (P:Fin (S m) -> Type)
      (P0:P (FinO m)) (PS: forall y:Fin m, P (FinS m y)),
      P x
  end x :=
match x with
| FinO n0 => fun P P0 PS => P0
| FinS n0 x0 => fun P P0 PS => PS x0
end.

Definition Fin_inversionS (n:nat) (P:Fin (S n) -> Type)
  (P0: P (FinO n)) (PS: forall x:Fin n, P (FinS n x))
  (x:Fin (S n)) : P x :=
Fin_inversion_aux (S n) x P P0 PS.

Definition Fin_inversion0 (P:Fin 0 -> Type) (x:Fin 0) : P x :=
match (Fin_inversion_aux 0 x) with
end.

Lemma Fin1: forall k:Fin 1, k = FinO 0.
Proof.
inversion k using Fin_inversionS.
trivial.
inversion x using Fin_inversion0.
Qed.

--
Daniel