The Coq mailing list

[Ralf Jung <jung AT mpi-sws.org>]

Hi all,

I just noticed that there are some weird differences between Program
Definition and Program Fixpoint, which force me to use Fixpoint even for
some non-recursive definition unless I want to spell out some "_"
explicitly:

---------- BEGIN --------------
Require Import Program Omega.

Definition foo (n : nat) {H : n > 5} := n.

Program Fixpoint foo1 x := foo (x + 6).
Next Obligation. omega. Qed.

(* I would expect this to work. *)
Fail Program Definition foo1 x := foo (x + 6).


(* I can work around it, but it's ugly. *)
Program Definition foo2 x := foo (x + 6) (H:=_).
Next Obligation. omega. Qed.
--------- END ------------

Is this somehow a feature I do not understand, or is it an outright bug
in "Program"?

In any case, this can be problematic if what you are defining is not a
function, i.e. does not have any arguments - in that case, you cannot
use Fixpoint, so you have to be explicit about the "_".

Kind regards,
Ralf