The Coq mailing list

[scott constable <sdconsta AT syr.edu>]

Hi All,

I have a simple recursive programming language implemented in coq with an evaluate function "eval". Since the language is non-normalizing, eval is recursively defined over a nat counter, "i" (I'm following the strategy given in the ImpCEvalFun chapter of SF). I'm currently trying to prove that whenever a term "tm" in the language is well-formed, no error can occur during a computation. So the theorem is as follows:

Theorem NoFail : forall i tm, well_formed tm -> eval i tm <> Error.

It seems that I need to induct over both i and tm, but doing something like

induction i as [|i'], tm.

always leads to unprovable subgoals, such as

  IHi' : eval i' (t_Plus t1 t2) <> Error

  ============================

   eval (S i') (t_Plus t1 t2) <> Error

when what I really want would be something like

  IH1 : eval i' t1 <> Error

  IH2 : eval i' t2 <> Error

  ============================

   eval (S i') (t_Plus t1 t2) <> Error

Any help would be much appreciated.

Thanks,

Scott Constable