Stream: Coq users

Topic: Suggest Proof Using for Program

view this post on Zulip Alex Sanchez-Stern (Mar 01 2024 at 19:48):

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?

view this post on Zulip Gaëtan Gilbert (Mar 01 2024 at 21:47):

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

view this post on Zulip Paolo Giarrusso (Mar 02 2024 at 05:25):

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: Jun 23 2024 at 05:02 UTC