The Coq mailing list

[scott constable <sdconsta AT syr.edu>]

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
>