The Coq mailing list

[Valentin Robert <valentin.robert.42 AT gmail.com>]

Hello,

In trying to define a non-structurally recursive monadic function, I came upon the realization that [Program Fixpoint] is unable to propagate values through immediately-applied lambdas.

Here is a small example that illustrates the issue:

Program Fixpoint recurse (n : nat) { measure n } : unit :=

  match n with

  | S n' => (fun i => recurse i) n'

  | O => tt

  end.

Next Obligation.

  (* Problem: Coq did not realize that i was n' *)

It seems that in this case, [Fixpoint] is actually smarter, as the following is accepted;

Fixpoint recurse' (n : nat) { struct n } : unit :=

  match n with

  | S n' => (fun i => recurse' i) n'

  | O => tt

  end.

Is there a way to have the same power in [Program Fixpoint]? Since monadic code unfolds to (foo >>= (fun x => bar)), it's impossible to prove that recursive calls are safe because the provenance of values is lost in the function application.

- Valentin