Johannes Hostert (Nov 29 2023 at 04:05): Johannes Hostert (Nov 29 2023 at 04:05):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.
Pierre Roux (Nov 29 2023 at 08:11):You can maybe try something like Obligation Tactic := idtac. before using Program.
Gaëtan Gilbert (Nov 29 2023 at 09:46):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
Gaëtan Gilbert (Nov 29 2023 at 09:47):see also coq#ec26ef7bdee30f93b53d53171fc881f8413cb7c1
Last updated: Oct 13 2024 at 01:02 UTC