The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

On 08/03/2016 21:41, scott constable 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.

I must admit that I didn't even know it was possible to pass two
arguments to induction. I am not quite sure what the semantics could be.
Anyway, in your case, I would simply have first done an induction on i,
and then an induction on 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

My suggestion above would give

IHi : forall tm : t, well_formed tm -> eval i tm <> Error
=========================================================
well_formed (t_Plus t1 t2) -> eval (S i) (t_Plus t1 t2) <> Error

which seems much closer to what you are expecting.

Best regards,

Guillaume