The Coq mailing list

[Edsko de Vries <devriese AT cs.tcd.ie>]

Hi,

First, I'm sorry for asking so many questions - I'm obviously still a
beginner at this stuff!

I need to do a proof over an inductively defined predicate:

Lemma preservation_under_subst : 
  forall (G:context) (x:Var) (S T:type) (t s:Term) 
    (pf: disjoint eq_var_dec (x::fv s) (bv t)),
  typeof (upd x S G) t T -> typeof G s S -> typeof G (subst x s t pf) T.

The details don't matter, except that I need to do induction over

 H : typeof (upd x S G) t T

Now I can't directly do elim H, since some of the arguments of typeof
aren't variables. Now this occurs quite frequently, and so far I've
always successfully applied the technique explained in section 8.4.3
(Proving Semantic Properties) of Coq'Art, which introduces a new
variable to be bound to the expression, i.e.

cut(forall (G':context), typeof G' t T -> G' = upd x S G ->
  forall pf : disjoint eq_var_dec (x :: fv s) (bv t),
  typeof G s S -> typeof G (subst x s t pf) T).

where G' is bound to "upd x S G". I can then call elim, and I get what I
need. Unfortunately, in this particular case, it turns out that this cut
has made the induction hypotheses unusable: they will have a premise of
the form ".. = .." (the additional premise added by the cut), and that
premise cannot be fulfilled.

Now, it may well be that I'm talking non-sense here, and that a cut of
this form cannot influence whether or not the induction hypotheses can
be used; if that is true, I'm clearly doing something silly somewhere.
However, if not, is there any other way I can do my induction, without
introducing the equality?

Thanks!

Edsko