Stream: Coq users

Topic: Unfolding `Opaque`

Paolo Giarrusso (Oct 15 2021 at 16:43):

Can one implement an Opaque-piercing unfold tactic that does _not_ conflict with async proofs? As @Abhishek Anand pointed out to me recently, that'd let you use Opaque as a less-broken simpl never flag (e.g. one that actually deserves that name).

Today one can write the code below, but those commands break async proofs since they access mutable state. I'm aware of stdpp sealing but it requires rewrite, which is sometimes too slow (and I suspect ssreflect does too).

Opaque foo. (* Coq's actual command for the `simpl never` functionality. *)
Lemma ...
Proof.
  ...
  (* The `simpl never` usecase requires an unfolding option. *)
  Local Transparent foo. unfold foo. Local Opaque foo.
...
Qed.

Janno (Oct 15 2021 at 17:29):

It just occurred to me that with_strategy might be useful here: https://coq.github.io/doc/V8.13.2/refman/proofs/writing-proofs/rewriting.html#coq:tacn.with_strategy

Gaëtan Gilbert (Oct 15 2021 at 17:36):

Opaque doesn't have anything to do with async proofs afaik

Paolo Giarrusso (Oct 15 2021 at 19:12):

@Gaëtan Gilbert global ^W non-proof local commands in proofs block async

Paolo Giarrusso (Oct 15 2021 at 19:14):

since those affect later proofs, the async proof mechanism can't just "skip what's between Proof. and Qed.".
I'm not sure why the async engine can't "pull them out" and pretend it's dealing with

Transparent foo. Opaque foo.
Lemma ...

but then again, that sounds as hard as inferring a Proof. command when missing (also an open challenge); maybe that's what the document manager is about (no clue?)

Gaëtan Gilbert (Oct 15 2021 at 19:16):

non-proof local commands in proofs block async

are you sure? when I do -vos on the following I get no error, which implies async worked

Lemma foo : False.
Proof.
  Opaque id.
  fail.
Qed.

Gaëtan Gilbert (Oct 15 2021 at 19:16):

the stm has a "replay" mechanism so side-effect commands are done twice (once in the proof, and once out of the proof before sending the term to the kernel IIRC)

Gaëtan Gilbert (Oct 15 2021 at 19:19):

so for instance if you do

Class XX := xx {}.

Lemma foo : True.
Proof.
  Existing Instance xx.
  exact I.
Qed.

you get the missing locality warning once at Existing Instance and again at Qed

Paolo Giarrusso (Oct 15 2021 at 19:22):

uuh, thanks. I thought I had minimized this a while ago, but I can't reproduce it... and I do have a proof taking too long in vos, but something else might be the cause.

Paolo Giarrusso (Oct 15 2021 at 19:28):

and coqc -time -vos confirms — maybe I should use that to debug _where_ the problem starts:

$ coqc -time -vos test.v
Chars 0 - 26 [Set~Nested~Proofs~Allowed.] 0. secs (0.u,0.s)
Chars 0 - 21 [Lemma~foofoo~:~False.] 0.004 secs (0.u,0.002s)
Chars 22 - 28 [Proof.] 0. secs (0.u,0.s)
Chars 31 - 41 [Opaque~id.] 0. secs (0.u,0.s)
Chars 50 - 54 [Qed.] 0. secs (0.u,0.s)

Last updated: Oct 01 2023 at 19:01 UTC