The Coq mailing list

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

Is there any way that I can get Coq to derive automatically the 
dependent inversion principle 'tm_invert_true' below?

Inductive tm : bool -> Set :=
  | t : tm true
  | f : tm false.

Lemma tm_invert_true' : forall (P : tm true -> Prop),
  P t
  -> forall t e,
    (match t return (tm t -> Prop) with
       | true => P
       | _ => fun _ => True
     end) e.
  destruct e; trivial.
Qed.

Lemma tm_invert_true : forall (P : tm true -> Prop),
  P t
  -> forall e, P e.
  intros.
  generalize (tm_invert_true' P); intuition.
  generalize (H1 true); trivial.
Qed.

Goal (forall (e1 e2 : tm true),
  match e1 with
    | t => e2
    | _ => t
  end = e2).
  inversion e1 using tm_invert_true; trivial.