Hi there,

I noticed a small peculiarity in the implementation and documentation of `Proof using X with Y.`

. Should I file a bug report/pull request?

When a proof depends on no Variable of the section, the `using`

annotation is mandatory (which I think is the intended behavior).

But

1) small error in the documentation says

Proof using ident+.

Should it be

Proof using ident*.

2) Empty list of hyps is indeed alone except in the presence of the "with" annotation:

```
Proof using. (* OK *)
Proof using with auto. (* Syntax error: [vernac:section_subset_expr] expected after 'using' (in [vernac:command]). *)
```

The documentation of `Proof using`

is being fixed at https://github.com/coq/coq/pull/12936

The updated documentation is here: https://coq.gitlab.io/-/coq/-/jobs/791990318/artifacts/_install_ci/share/doc/coq/sphinx/html/proof-engine/proof-handling.html#coq:cmd.proof-using

You can always use `Type`

instead of nothing if a proof depends on no variable.

This limitation when using the combination of `with`

and `using`

is too bad, but I'd call it a parser limitation. I don't know if there is anything we can do about it, although you should feel free to open an issue to ask about it.

In any case, we should probably add some words about it in the doc as part of the above mentioned PR.

Thanks for your answers.

I am currently fixing the automatic filling of these annotations in PG, I will put "Type" then when coq's suggestion is empty.

We could also change coq's suggestion to suggest `Type`

. Maybe worth another issue!

wait, are `Proof using.`

and `Proof using Type.`

exactly the same semantically? Only under specific conditions, right?

Type means "vars that occur in the statement". I can't see any circumstance where this would not have the same effect.

`Proof using expr.`

is really `Proof using Type + expr.`

Another question:

It seems that coq supports

```
Proof using Y with X.
Proof with X using Y.
```

but documentation cites only the former. The former has one glitch when the tactic itself accepts "using" in its syntax

```
Proof with auto using Foo.
```

is understood as

```
Proof with (auto using Foo).
```

is the order of the documentation to be preferred?

I just discovered this thanks to you. Actually, the two forms are documented at https://coq.gitlab.io/-/coq/-/jobs/791990318/artifacts/_install_ci/share/doc/coq/sphinx/html/proof-engine/tactics.html#coq:cmd.proof-with.

BTW, there has been some recent discussion about removing `Proof with`

(see https://github.com/coq/coq/issues/12059 but actually the most interesting discussion is the one that happened in https://github.com/coq/coq/pull/12065 after we discovered that SF uses it).

`Proof with`

is a huge pain when updating old code.

As are all tactic combinators `;`

itself is a pain when updating code but wa don't want (well, I want) to get rid of it.

I think there is a huge chasm between deprecating `Proof with`

(rarely used, nearly always a problem) and deprecating `;`

(nearly universally used)

We could also change coq's suggestion to suggest

`Type`

. Maybe worth another issue!

relevantly, suggestions from “Set Suggest Proof Using” list _all_ used variables, but that’s not what you want to write after `Proof using ...`

— many/most of those are implied.

@Pierre Courtieu FYI this PR https://github.com/coq/coq/pull/13183 makes `Proof using`

available as an attribute, so you will eventually be able to write `#[using="...."] Lemma ... Proof with tac. `

as an alternative syntax for `Lemma ... Proof using ... with tac`

Paolo Giarrusso said:

relevantly, suggestions from “Set Suggest Proof Using” list _all_ used variables, but that’s not what you want to write after

`Proof using ...`

— many/most of those are implied.

Not entirely true, several suggestions are proposed and the first one tries to minimize the list. (xx is not suggested here):

```
Section Foo.
Variables xx: Prop.
Variable pp : forall x:xx, True.
Variable a:xx.
Theorem lt_n_S :True-> True.
Proof.
intro. apply (pp a).
Qed. (*The proof of lt_n_S should start with one of the following commands: Proof using a pp.
Proof using All.*)
End Foo.
```

Moreover I am not entirely convinced that having implicit there is a good idea: the more it fails when something changes the best imho.

Enrico Tassi said:

Pierre Courtieu FYI this PR https://github.com/coq/coq/pull/13183 makes

`Proof using`

available as an attribute, so you will eventually be able to write`#[using="...."] Lemma ... Proof with tac.`

as an alternative syntax for`Lemma ... Proof using ... with tac`

Yes this may be anothersolution, but PG has to be compatible with a few older versions of coq, so I will wait.

@Pierre Courtieu the suggestions can mention variables that are mentioned in the statement and would be implied by `using.`

I guess this should be reported. Since the mechanics knows how to ignore variables implied by the term, it should be rather trivial to do the same with its type.

Something smart could also maybe be done with declared `Collection`

too but I am not sure what.

And PG could propose all suggested solutions instead of the first one currently.

Just FTR:

```
The following section variables are used but not declared:
interp_timeless Inh_dev Inh_T.
You can either update your proof to not depend on interp_timeless Inh_dev
Inh_T, or you can update your Proof line from
Proof using HAS_Proto T _protoM d interp io thread_info Σ σ
to
Proof using HAS_Proto Inh_T Inh_dev T _protoM d interp interp_timeless io thread_info Σ σ
```

Of course, this proof started with `Proof.`

(and `Set Default Proof Using "Type".)

and the correct command is `Proof using interp_timeless Inh_dev Inh_T.`

Paolo Giarrusso said:

and the correct command is

`Proof using interp_timeless Inh_dev Inh_T.`

I think this should be the subject of feature wish. Can you point to the complete code please?

No; I might be able to minimize it... However, I've never seen code where this bug doesn't trigger.

(which mostly affects the priority; I prioritize minimizing bugs that are hard to reproduce, over other ones)

Last updated: Jun 16 2024 at 01:42 UTC