Hey all,
I've been using the Set Suggest Proof Using
flag in coq to get Proof using annotations for proofs, which I then insert into proof files to allow automation to skip proofs reliably. But I noticed this doesn't seem to work for the obligations resulting from a Program statement. So, if you set that flag, and then run a program statement with holes, you get a bunch of obligations that you navigate with the Next Obligation
vernac. Depending on the holes, some of these can be filled with opaque objects, so you can use Qed to close them, or you can use Admitted to skip them. But like a normal proof, if you close it with Admitted without a Proof using
annotation, it'll assume it depends on all available section variables. And, like a normal proof, you can insert a Proof using
annotation to restrict this to a subset of the section variables, and then run Admitted, and it'll have the right type. unlike a normal proof though, the Set Suggest Proof Using flag won't suggest annotations for obligations opened with Next Obligation.
Is this a coq bug? Or intended behavior for some weird reason?
Proof using doesn't work for obligations, for instance
Axiom foo : nat -> True.
Section S.
Variable x : nat.
Program Definition bla : True := _.
Next Obligation.
Proof using .
apply foo,x.
Qed. (* accepted *)
I guess this is a bug
The bug is larger... Proof using
exists to help async processing, but that is not supporred for obligations. And in many cases, you'd want the same using
annotation for all obligations in a Definition
Last updated: Oct 13 2024 at 01:02 UTC