Consider the following definition:

```
Program Fixpoint pf (n:nat) {measure n} : Prop :=
forall n' (H:n' < n), pf n'.
Next Obligation. apply lt_wf. Defined.
```

This works. However, it a bit ugly. Note that `H : n' < n`

is not used in the "source code"[^1] of the fixpoint, only when proving that the call is well-founded. Thus, one might want to replace the body by `forall n' (_:n' < n), pf n'`

, which is just the desugared version of `forall n', n' < n -> pf n'`

. However, these do not work, since either ends up with an obligation without the assumption `n' < n`

.

The question is: Why? Surely generating fresh names for these assumptions can't be too hard? Why drop them instead of allowing them to be used to prove an obligation?

This behavior is also inconsistent, since this works "properly" for this definition, where the anonymous binder belongs to a lambda instead of a forall:

```
Program Fixpoint pf (n:nat) {measure n} : Prop :=
let baz := fun n' (_:n' < n) => pf n' in (* in the generated obligation, the anonymous argument is present and has a name *)
forall n' (H:n' < n), baz n' H.
```

[^1]: Of course, it will later show up somewhere as an argument to something. Hence the scare quotes.

You can maybe try something like `Obligation Tactic := idtac.`

before using `Program`

.

oblgation tactic isn't the issue here

we do handle Anonymous differently for Prod https://github.com/coq/coq/blob/b06166b2b80899292e0309556b23ff8cc0f0975a/pretyping/pretyping.ml#L1048

see also coq#ec26ef7bdee30f93b53d53171fc881f8413cb7c1

Last updated: Jun 22 2024 at 15:01 UTC