`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?

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

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.

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.
```

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

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

is the goal to speed up `make vos`

? Tough luck I fear: that cannot skip obligations

got an example of missing `Proof using`

annotation?

```
$ 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

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

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

on line 285

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

uh, would obligations be affected by `#[using="Hn"] Definition foo`

? https://coq.inria.fr/refman/proofs/writing-proofs/proof-mode.html#coq:attr.using

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

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

?

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).

(But you can't leave out `Proof.`

!)

Last updated: Jun 14 2024 at 17:02 UTC