The Coq mailing list

[Andrew Kennedy <akenn AT microsoft.com>]

Hi all

I'm trying to prove some seemingly trivial inversion lemmas for a typed 
evaluation relation. I've managed to prove the lemmas using Eqdep.inj_pair2 
(which captures injectivity of dependent pairs) but wonder why the tactics 
inversion/injection don't build this in, and why "dependent rewrite" doesn't 
work either. Boiling down my example to something really simple, I define a 
grammar of types and expressions over those types:

Set Implicit Arguments.

Inductive Ty :=
  | Nat : Ty
  | Prod : Ty -> Ty -> Ty.

Inductive Exp : Ty -> Type :=
| Const : nat -> Exp Nat
| Pair : forall t1 t2, Exp t1 -> Exp t2 -> Exp (Prod t1 t2)
| Fst : forall t1 t2, Exp (Prod t1 t2) -> Exp t1.

Now I define an evaluation relation:

Inductive Ev : forall t, Exp t -> Exp t -> Prop :=
| EvConst   : forall n, Ev (Const n) (Const n)
| EvPair    : forall t1 t2 (e1:Exp t1) (e2:Exp t2) e1' e2',
                Ev e1 e1' -> Ev e2 e2' -> Ev (Pair e1 e2) (Pair e1' e2')
| EvFst     : forall t1 t2 (e:Exp (Prod t1 t2)) e1 e2,
                Ev e (Pair e1 e2) ->
                Ev (Fst e) e1.

Now I want to prove a simple inversion lemma for the "Fst" constructor:

Lemma EvFst_inversion : forall t1 t2 (e:Exp (Prod t1 t2)) e1, Ev (Fst e) e1 
-> exists e2, Ev e (Pair e1 e2).
intros t1 t2 e e1 ev.
inversion ev. subst.

This gives me a goal

t1 : Ty
  t2 : Ty
  e : Exp (Prod t1 t2)
  e1 : Exp t1
  ev : Ev (Fst e) e1
  e2 : Exp t1
  e3 : Exp t2
  e4 : Exp (Prod t1 t2)
  H1 : Ev e4 (Pair e2 e3)
  H2 : existT (fun t1 : Ty => {t2 : Ty &  Exp (Prod t1 t2)}) t1
         (existT (fun t2 : Ty => Exp (Prod t1 t2)) t2 e4) =
       existT (fun t1 : Ty => {t2 : Ty &  Exp (Prod t1 t2)}) t1
         (existT (fun t2 : Ty => Exp (Prod t1 t2)) t2 e)
  H3 : existT (fun x : Ty => Exp x) t1 e2 =
       existT (fun x : Ty => Exp x) t1 e1
  ============================
   exists e5 : Exp t2, Ev e (Pair e1 e5)

Now the docs for inversion/injection do warn that

"Beware that injection yields always an equality in a sigma type whenever the 
injected object has a dependent type."

So my first question is: why? Why can't H2 and H3 be decomposed further by 
the injection tactic?

My second question is: why cannot "dependent rewrite" do anything with H2 and 
H3? The documentation presents dependent rewrite as the recommended tactic 
for this kind of thing.

In the end, I manage to prove the lemma with repeated invocation of 
Eqdep.inj_pair2:

Require Import Eqdep.
(* Unfortunately inversion doesn't know how to take apart dependent pairs,
   so we must invoke inj_pair2 repeatedly to get the equalities that we need.
   dependent rewrite is supposed to be able to do this but I can't get it to 
work *)
assert (H3c := inj_pair2 _ _ _ _ _ H3). clear H3. subst.
assert (H2a := inj_pair2 _ _ _ _ _ H2). clear H2.
assert (H2b := inj_pair2 _ _ _ _ _ H2a). clear H2a. subst.
exists e3; trivial.
Qed.

So my third question is: why is this not built into tactics such as 
inversion, injection, and congruence?

Thanks!
Andrew.