What is the idiomatic way in Coq to write recursive functions over product types?

Question

I need to write a recursive function in Coq that takes an argument with type T and produces a result with type option T. The problem is, the recursive invocation is not properly on a subterm of its argument, but it surely is decreasing - the problem is how to make Coq aware of this, without disrupting too much my type or function definitions. I exemplify the situation below.

Inductive expression : Type :=
| expr_ref : reference -> expression
| expr_val : value -> expression
| expr_get : expression -> string -> expression
| ...
end.

...

Definition config : type := program * memory * expression.

Fixpoint step (J : config) : option config :=
  match J with
  | (P, M, expr_get (expr_ref r) name) => (P, M, expr_val (M r name))
  | (P, M, expr_get e name) => match step (P, M, e) with
    | Some (P', M', e') => Some (P', M', expr_get e' name)
    | None => None
    end
  ...

Here the recursive call (P, M, e) should be OK because the third component of the configuration (the expression) is decreasing. I would like to express the thing without messing too much with the code of the function or with the definition of the types (the reason is, the function should be a computable version of a relation that I specified in a declarative style, and I want to keep the similarities in their definitions as much as possible). I have seen that Program Fixpoint allows to specify measures, but I was not able to understand how to specify the measure I need. What would be an idiomatic way to express in Coq the step function? Should I define the config type differently?

Answer 1

If your step functiom is really a structural recursion on the expression, a way to go is to split your triplet :

Fixpoint step_rec (J : program * memory) (e : expression) : option config :=
  match e with
  |  expr_get (expr_ref r) name) => (J, expr_val (M r name))
  |  expr_get e name => match step_rec J e with
    | Some (J', e') => Some (J', expr_get e' name)
    | None => None
    end
  ...
 Definition step (c : config) := let (J,e) := c in step_rec J e.

Then if you need it, you can always derive the theorem

forall c, step c =
  match c with
  | (P, M, expr_get (expr_ref r) name) => (P, M, expr_val (M r name))
  | (P, M, expr_get e name) => match step (P, M, e) with
    | Some (P', M', e') => Some (P', M', expr_get e' name)
    | None => None
    end
  ...