The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi,

  this is more of a conceptual issue with monads, you'd have to give a dependent type to the bind construct to show how foo produces "smaller" values that you can use to recurse on in bar (I don't claim to know how to do this in general :). Similarly, you can annotate your lambda abstraction to carry the logical information about [i] that you need:

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

  match n with

  | S n' => (fun (i : nat | i <= n') => recurse i) n'

  | O => tt

  end.

Next Obligation.

  auto with arith.

Defined.

Hope this helps,

-- Matthieu

On Fri, Mar 17, 2017 at 10:54 AM Valentin Robert <valentin.robert.42 AT gmail.com> wrote:

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