The Coq mailing list

[Adam Chlipala <adamc AT cs.berkeley.edu>]

rcp AT Cs.Nott.AC.UK
 wrote:
> I will like to examine the cases of i, so should think "dependent 
> inversion i" should do the trick. However, this does not help. Can 
> anyone suggest a way to proceed?

I don't have a quick solution for your particular case, but the way that 
I handle such situations is to prove alternate inversion principles 
manually.  Here's an example for a significantly simpler inversion 
dilemma that I've encountered.  Advice from others on how to improve 
this implementation would be very interesting to me!

Require Import List.

Set Implicit Arguments.

Section Var.

 Variable dom : Set.

 Inductive Var : list dom -> dom -> Set :=
   | First : forall G t, Var (t :: G) t
   | Next : forall G t t', Var G t -> Var (t' :: G) t.

 Lemma Var_invert'
   : forall P : forall (t' : dom) l t, Var (t' :: l) t -> Prop,
     (forall G t, P t G t (First G t)) ->
     (forall G t t' v,
   P t' G t (Next t' v)) ->
     forall l t v,
   match l return (Var l t -> Prop) with
     | nil => fun _ => True
     | _ => fun v => P _ _ _ v
   end v.
   intros.
   destruct v; auto.
 Qed.

 Theorem Var_invert
   : forall P : forall (t' : dom) l t, Var (t' :: l) t -> Prop,
     (forall G t, P t G t (First G t)) ->
     (forall G t t' v,
   P t' G t (Next t' v)) ->
     forall t' l t v, P t' l t v.
   intros.
   generalize (Var_invert' P).
   intuition.
   generalize (H1 (t' :: l)).
   trivial.
 Qed.

End Var.