How do I express a fixpoint of a decreasing argument that is not a subterm of the function's argument?

Question

I have a recursively defined function in Coq whose arguments in the recursive invocations are surely decreasing, but Coq cannot understand this fact since they are not subterms of the function's argument. This is a snippet exemplifying the situation:

Inductive expression : Type :=
| Get : expression -> identifier -> expression
| IfThenElse : expression -> expression -> expression -> expression
...
end.

Fixpoint eval (M : memory) (e : expression) : value :=
  match e with
  | Get (IfThenElse cond e1 e2) var_name => ... eval M (Get e1 var_name) ... eval M (Get e2 var_name) ...
  ...
  end.

While the recursive invocations of eval have not a subterm of e as their argument, it is easy to find a decreasing measure for the e argument of eval, e.g., the maximum nesting level of subterms in it. I read that Program Fixpoint allows to specify a measure, but I found the section on Program in the reference manual too obscure, nor I was able to find a tutorial or examples that may suit a beginner as I am. Can anyone provide me some references, or a quick explanation, or perhaps suggest an alternative approach that does not imply restructuring the inductive type definitions?

Answer 1

It turns out that using Program Fixpoint is much easier than I thought:

From Coq Require Import Program.Wf.

...

Inductive height (e : expression) : nat
  match e with
  | Get e1 => height e1 + 1
  | IfThenElse e1 e2 e3 => (Nat.max (height e1) (Nat.max (height e2) (height e3))) + 1
  ...
  end.

Program Fixpoint eval (M : memory) (e : expression) {measure (height e)} : value := ...

A more worked-out example, similar in spirit to a subset of the specification I am working on, is available at https://gist.github.com/pietrobraione/22cad84ed2d84da57e2fd500ee14fe02. The next point would be, as far as I could understand, proving the obligations that are generated.

Answer 2

Maybe you could have a fixpoint dedicated to Get to avoid rebuilding terms.

Fixpoint eval_get (M : memory) (e : expression)  (var_name : identifier) : value :=
  match e with
  | IfThenElse cond e1 e2 var => ... eval_get M e1 var_name ... eval_get M e2 var_name ...
  ...
  end.

and then

Fixpoint eval (M : memory) (e : expression) : value :=
  match e with
  | Get e var_name => eval_get e1 var_name
  end.

Answer 3

I find your definition of eval a bit odd. You are implementing something like large-step evaluation, which should be defined by structural recursion on the expression being evaluated.

I would expect your pseudo-code to look like this:

Inductive expression : Type :=
| Get : expression -> identifier -> expression
| IfThenElse : expression -> expression -> expression -> expression
...
end.

Fixpoint eval (M : memory) (e : expression) : value :=
  match e with
  | IfThenElse cond e1 e2 =>
      match eval M cond with
      | ValueFalse => eval M e2
      | ValueTrue => eval M e1
      | _ => ValueRuntimeError
     end

  | Get e var_name => 
      match eval M e with
      | ValueObject obj => get_field obj var_name
      | _ => ValueRuntimeError

  ...

  end.

Above get_field is a primitive function (not part of your source language) that extracts a field from an object, represented as a value.