"Proof using + with · Coq users · Zulip Chat Archive

Stream: Coq users

Topic: "Proof using + with

Pierre Courtieu (Oct 16 2020 at 12:26):

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

Théo Zimmermann (Oct 16 2020 at 12:28):

The documentation of Proof using is being fixed at https://github.com/coq/coq/pull/12936

Théo Zimmermann (Oct 16 2020 at 12:30):

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

Théo Zimmermann (Oct 16 2020 at 12:31):

You can always use Type instead of nothing if a proof depends on no variable.

Théo Zimmermann (Oct 16 2020 at 12:32):

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.

Théo Zimmermann (Oct 16 2020 at 12:33):

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

Pierre Courtieu (Oct 16 2020 at 12:35):

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.

Théo Zimmermann (Oct 16 2020 at 12:35):

We could also change coq's suggestion to suggest Type. Maybe worth another issue!

Karl Palmskog (Oct 16 2020 at 12:36):

wait, are Proof using. and Proof using Type. exactly the same semantically? Only under specific conditions, right?

Pierre Courtieu (Oct 16 2020 at 12:42):

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

Gaëtan Gilbert (Oct 16 2020 at 12:44):

Proof using expr. is really Proof using Type + expr.

Pierre Courtieu (Oct 16 2020 at 12:44):

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

Pierre Courtieu (Oct 16 2020 at 12:47):

is the order of the documentation to be preferred?

Théo Zimmermann (Oct 16 2020 at 12:52):

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.

Théo Zimmermann (Oct 16 2020 at 12:58):

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

Karl Palmskog (Oct 16 2020 at 13:00):

Proof with is a huge pain when updating old code.

Pierre Courtieu (Oct 16 2020 at 13:12):

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.

Karl Palmskog (Oct 16 2020 at 13:14):

I think there is a huge chasm between deprecating Proof with (rarely used, nearly always a problem) and deprecating ; (nearly universally used)

Paolo Giarrusso (Oct 16 2020 at 14:07):

We could also change coq's suggestion to suggest Type. Maybe worth another issue!

Paolo Giarrusso (Oct 16 2020 at 14:08):

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.

Enrico Tassi (Oct 16 2020 at 15:08):

@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

Pierre Courtieu (Oct 16 2020 at 16:49):

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.

Pierre Courtieu (Oct 16 2020 at 16:50):

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.

Paolo Giarrusso (Oct 16 2020 at 18:19):

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

Pierre Courtieu (Oct 16 2020 at 18:32):

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.

Pierre Courtieu (Oct 16 2020 at 18:33):

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.

Paolo Giarrusso (Oct 18 2020 at 20:29):

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 Σ σ

Paolo Giarrusso (Oct 18 2020 at 20:30):

Of course, this proof started with Proof. (and `Set Default Proof Using "Type".)

Paolo Giarrusso (Oct 18 2020 at 20:31):

and the correct command is Proof using interp_timeless Inh_dev Inh_T.

Pierre Courtieu (Oct 19 2020 at 12:53):

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?

Paolo Giarrusso (Oct 19 2020 at 13:05):

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

Paolo Giarrusso (Oct 19 2020 at 13:06):

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

Last updated: Apr 19 2024 at 22:01 UTC