Stream: MetaCoq

Topic: Set Suggest Proof Using

Jason Gross (Nov 24 2022 at 18:53):

Set Suggest Proof Using does not work in MetaCoq (coqc emits no suggestions). Any ideas why? Does Equations change the meaning of Proof in a way that breaks Set Suggest Proof Using or something?

Yannick Forster (Nov 24 2022 at 19:00):

I used Set Suggest Proof using to annotate the whole code base with using. So it for sure used to work, but I think I did that on 8.15

Jason Gross (Nov 24 2022 at 19:04):

I think it works in some files and not in others. In particular, there are a bunch of proofs still missing Proof using annotations, and those are precisely the proofs where it does not work.

Paolo Giarrusso (Nov 24 2022 at 19:18):

Self-contained example: this will give a warning exactly at the second Qed, as expected.

Set Suggest Proof Using.

Lemma foo0 {A} (x : A) : x = x.
easy. Qed.

Class Decision (P : Prop) := {}.
Section foo.
  Context {P} `{Decision P}.
  Lemma foo {A} (x : A) : x = x.
  easy. Qed.

Yannick Forster (Nov 24 2022 at 19:20):

I used Set Suggest Proof using to annotate the whole code base with using. So it for sure used to work, but I think I did that on 8.15

Paolo Giarrusso (Nov 24 2022 at 19:20):

this test is on 8.16, but :bulb: this won't work on obligations

Paolo Giarrusso (Nov 24 2022 at 19:21):

is the goal to speed up make vos? Tough luck I fear: that cannot skip obligations

Paolo Giarrusso (Nov 24 2022 at 19:23):

got an example of missing Proof using annotation?

Jason Gross (Nov 24 2022 at 19:46):

$ for i in $(for d in template-coq pcuic safechecker erasure translations; do git ls-files "$d/*.v"; done); do foo="$(grep -o 'Section\|End\|Module\|Proof\.\|(\*\|\*)' $i | sed 's/^ *//g' | tr '\n' '~' | sed 's/(\*[^\*]*\*)//g; s/(\*[^\*]*\*)//g' | grep -o 'Section[^SME]*Proof[^SME]*End')"; if [ ! -z "$foo" ]; then echo "$i"; fi; done | wc -l
45

suggests there are 45 files with a missing proof using. In template-coq we have

template-coq/theories/EnvironmentTyping.v
template-coq/theories/Universes.v
template-coq/theories/WcbvEval.v
template-coq/theories/common/uGraph.v
template-coq/theories/utils/All_Forall.v
template-coq/theories/utils/wGraph.v

In template-coq/theories/EnvironmentTyping.v, All_local_env_fold in Section TypeLocal is missing Proof using and Set Suggest Proof Using does not seem to function on it

Jason Gross (Nov 24 2022 at 19:46):

(The goal for me is to make sure that proofs don't in the future pick up extra section arguments that they shouldn't.)

Paolo Giarrusso (Nov 24 2022 at 20:04):

https://github.com/MetaCoq/metacoq/blob/d70aa6e70be0f51e2f9747819570b16d429a123c/template-coq/theories/EnvironmentTyping.v#L291 is outside of the section, see End TypeLocal. on line 285

Paolo Giarrusso (Nov 24 2022 at 20:09):

other false positives I'd suspect:

• Section All_local_env_rel. has no assumptions, but that regexp won't know
• proofs ending with Defined. are _IIRC_ not reported, because Proof using isn't needed for make vos — here your goals don't align with the designs
• equation obligations might be a real problem

Paolo Giarrusso (Nov 24 2022 at 20:13):

uh, would obligations be affected by #[using="Hn"] Definition foo? https://coq.inria.fr/refman/proofs/writing-proofs/proof-mode.html#coq:attr.using

Jason Gross (Nov 24 2022 at 20:21):

Here is one that does not look like a false positive, though it's much further into the code base: https://github.com/MetaCoq/metacoq/blob/d70aa6e70be0f51e2f9747819570b16d429a123c/erasure/theories/ErasureFunction.v#L44-L52

Jason Gross (Nov 24 2022 at 20:21):

Maybe this is because of Set Default Proof Using "Type*".?

Paolo Giarrusso (Nov 24 2022 at 20:33):

yep, that Proof. will mean Proof Using Type*. if Set Default Proof Using "Type*". is active (docs: https://coq.inria.fr/refman/proofs/writing-proofs/proof-mode.html#coq:opt.Default-Proof-Using).

Paolo Giarrusso (Nov 24 2022 at 20:33):

(But you can't leave out Proof.!)

Last updated: May 31 2023 at 02:31 UTC