The Coq mailing list

[scott constable <sdconsta AT syr.edu>]

Thank you all so much for the responses. Roux Cody was indeed correct that what I was trying to prove was false; I revised my eval function accordingly. It turned out that the right approach to begin the proof was to generalize tm, then induct over i, and then proceed by (non-inductive) cases over tm.

~Scott

On Wed, Mar 9, 2016 at 4:05 AM, Guillaume Melquiond <guillaume.melquiond AT inria.fr> wrote:

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