Stream: MetaCoq

Topic: Set Suggest Proof Using


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Nov 24 2022 at 19:20):

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

view this post on Zulip Paolo Giarrusso (Nov 24 2022 at 19:21):

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

view this post on Zulip Paolo Giarrusso (Nov 24 2022 at 19:23):

got an example of missing Proof using annotation?

view this post on Zulip 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

view this post on Zulip 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.)

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Nov 24 2022 at 20:09):

other false positives I'd suspect:

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Jason Gross (Nov 24 2022 at 20:21):

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

view this post on Zulip 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).

view this post on Zulip Paolo Giarrusso (Nov 24 2022 at 20:33):

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


Last updated: Mar 29 2024 at 07:01 UTC