The Coq mailing list

[Per Lindgren <Per.Lindgren AT ltu.se>]

Hi

Without knowing details of your problem, it seems similar to a problem we 
faced. Is it possible to define a “measure" (well founded relation) for i?

Best,
  Per 

> On 08 Mar 2016, at 21:41, scott constable 
> <sdconsta AT syr.edu>
>  wrote:
> 
> 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
>