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?