The Coq mailing list

[roux cody <cody.roux AT gmail.com>]

I'm now not sure that your theorem is true: what happens if you give "too little" fuel? Some subterm could evaluate to Overflow, which evaluates the overall term to Error.

You need to handle overflow of subterms differently, or to integrate i into your well_formed predicate.

I suspect that you want to be doing induction over well_formed tm (or well_formed tm i) at any rate.

Best,

Cody

On Tue, Mar 8, 2016 at 4:14 PM, scott constable <sdconsta AT syr.edu> wrote:

Per,

"i" is just a nat, so the well-founded relation would simply be the less-than operator. But even so, I'm not certain how this would help. My eval function is defined as follows (for brevity I'm omitting some rules):

(***********************************)

  Variable type : context.

  Inductive Result : Type :=

  | Value : t -> Result

  | Error : Result

  | Overflow : Result.

  Fixpoint eval (i : nat) (tm : t) {struct i} : Result :=

    match i with

    | 0 => Overflow

    | S i' => match tm with

              | (t_Var _) => Error

              | (t_Num n) => Value (t_Num n)

              | (t_Plus t1 t2) => match eval i' t1, eval i' t2 with

                                  | Value (t_Num n1), Value (t_Num n2) => Value (t_Num (Zplus n1 n2))

                                  | _, _ => Error

                                  end

              | (t_Cond b t1 t2) => match eval i' b with

                                    | Value b' => match b' with

                                                 | t_Num n => if Z.eq_dec n Z0

                                                              then eval i' t1

                                                              else eval i' t2

                                                 | _ => Error

                                                 end

                                    | _ => Error

                                    end

              | (t_Lam x t) => if bclosed (t_Lam x t)

                               then Value (t_Lam x t)

                               else Error

              | (t_App t1 t2) => match eval i' t1, eval i' t2 with

                                 | Value (t_Lam x t1'), Value c2 => eval i' (tsubst_t t2 x t1')

                                 | _, _ => Error

                                 end

              | (t_Bind x t1 t2) => match eval i' t1 with

                                    | Value c1 => eval i' (tsubst_t c1 x t2)

                                    | _ => Error

                                    end

              | (t_Rec y x t) => eval i' (t_Lam x (tsubst_t (t_Rec y x t) y t))

              end

    end.

(***********************************)

I also have a separate type checking function. The theorem that I am trying to proved is that whenever a term is well-formed (i.e. it type checks, and has no free variables) then eval will not emit an error. 

Thanks

Scott

On Tue, Mar 8, 2016 at 3:57 PM, Per Lindgren <Per.Lindgren AT ltu.se> wrote:

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
>