0
$\begingroup$

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?

$\endgroup$

1 Answer 1

1
$\begingroup$

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
  ...
$\endgroup$
1
  • $\begingroup$ Thank you. Completely splitting the triplet is what I chose to have a function that resembles the declarative specification as much as possible. $\endgroup$ Feb 2, 2023 at 15:02

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.