Stream: Coq users

Topic: Force Proof using. (vos)

Andrej Dudenhefner (Dec 07 2020 at 09:03):

I'm trying to optimize a larger code base for interface file (vos) compilation. I use Set Default Proof Using "Type"..
Unfortunately, in section with many variables automation such as lia/auto is happy to use every assumption, which leads to large interfaces and slow compilation.
clearing not necessary assumptions before automation helps, but is quite verbose in a large context.
A nice solution could be a Proof using command that actually clears all not explicitly mentioned variables.
Here is a small example:

Set Default Proof Using "Type".

Require Import Lia.
Section Capsule.

Context (n: nat) (H1: n = 0) (H1': n = 0).
Context (H2: n < 1) (H3: n-1 = 0).

Lemma main : n = 0.
Proof using H1.
  clear H1' H2 H3.
  lia.
Qed.

End Capsule.

Check main.

The line clear H1' H2 H3. feels quite redundant but seems to be necessary for small interfaces.
Am I missing some helpful command?

Enrico Tassi (Dec 07 2020 at 09:48):

There is a long standing problem with clear and section variables

Enrico Tassi (Dec 07 2020 at 09:49):

Doing it is not very safe, so Proof using does not do it automatically by default (there should be an option to turn this on, but given the problems it is off).

Enrico Tassi (Dec 07 2020 at 09:49):

I guess lia fiddles with the other hyps even if they are not needed, strictly speaking.

Enrico Tassi (Dec 07 2020 at 09:50):

eg, converting them to Z

Gaëtan Gilbert (Dec 07 2020 at 10:29):

wasn't the option removed?

Andrej Dudenhefner (Dec 07 2020 at 10:39):

At least in the documentation of Proof using there is no mention of such an option. Also it would be good to know the caveats.

Gaëtan Gilbert (Dec 07 2020 at 10:42):

https://github.com/coq/coq/commit/2e78edb4b8212cc5ab394fde168fc5241ad01660

Enrico Tassi (Dec 07 2020 at 20:11):

Then I think this behavior of lia should be reported as a bug.

Paolo Giarrusso (Dec 08 2020 at 01:17):

I don't think lia is alone here, so much so that I don't think lia can be blamed.

Paolo Giarrusso (Dec 08 2020 at 01:23):

for instance, stdpp's set_solver, written in Ltac1, is defined to collect all assertions about finite sets, transform them into another form, then invoke a generic first-order theorem prover, which does not tell you which assumptions it used.

Paolo Giarrusso (Dec 08 2020 at 01:24):

at best it offers shortcuts to clear assertions before reification, but those are implemented using clear. The same applies to lia: it reifies numeric assumptions, then invokes a decision procedure.

Paolo Giarrusso (Dec 08 2020 at 01:32):

and any proof-by-reflection solver does need to fiddle with all hyps, AFAICT.

Paolo Giarrusso (Dec 08 2020 at 01:34):

and because it's a general problem, no offense to Enrico, but his comment ends up suggesting to work around a section bug in various of tactics. Might still be the right call, if we despair of a proper fix :-|.

Guillaume Melquiond (Dec 08 2020 at 06:55):

Let us clear some misconceptions. First, lia is not to blame. In fact, it is rather well behaved, since it only uses hypotheses that appear with non-zero coefficients in its Farkas witness. Here, it only needs H2 (assuming it was not cleared). Second, notice how user expectations are wrong. Andrej expects only H1 to be used for the proof, but lia would prefer to use only H2. So, at this point, the only bug in lia is that it fails to read the mind of the user. Third, the actual cause for using all the hypotheses is zify, which is a preprocessing step. The zify tactic cannot know beforehand which hypotheses lia will end up using. So, to make it clever, it should first create a dummy goal, run lia on it, look at the generated proof, perform the minimal preprocessing needed, transform the generated proof, and actually apply it (or run lia a second time). Coq is lacking the machinery to do this kind of trick efficiently. Fourth, and we get to Paolo's point, by definition of reflection-based decision procedures being just a massive preprocessing step, any proof by reflection suffers from the same issue.

Karl Palmskog (Dec 08 2020 at 07:05):

I agree with Guillaume that this is mostly about user expectations rather than vos/lia/sections... Ideally, there would be a plugin that minimizes section dependencies automatically by doing something like the steps he recommends. Until then, manual clear seems like the way to go.

Andrej Dudenhefner (Dec 08 2020 at 08:10):

So, at this point, the only bug in lia is that it fails to read the mind of the user.

The user (me) explicitly states their expectations by Proof using H1.. No mind reading required.
So, one could imagine that preprocessing such as zify respects Proof using (whenever declared).
Without Proof using somehow cleverly minimizing dependencies would not be what I want.

Emilio Jesús Gallego Arias (Dec 08 2020 at 13:07):

As mentioned in the CUDW I believe that this kind of information should be tracked by the incremental checking properly, it seems unreasonable to me to expect the users to keep track of all that dependency information. I didn't have a look at sections yet tho, but IMHO should be doable, that's a pretty neat example that I've added to a future "test-suite"

Christian Doczkal (Dec 08 2020 at 14:04):

Enrico Tassi said:

Doing it is not very safe, so Proof using does not do it automatically by default (there should be an option to turn this on, but given the problems it is off).

Is it documented somewhere why or under which conditions doing a clear on section variables is not safe? If I understand correctly, the clear tactic allows clearing section hypotheses at any given point and I find it hard to imagine that clearing section hypotheses in the middle of a proof is safer than right when entering proof mode. So if there ever was an option for Proof using to remove forbidden assumptions (those whose use will make Qed. fail) and it was removed because clearing section variables is not safe but without changing the behavior of the clear tactic too at least emit a warning, this is starting to scare me. :scared:

Pierre-Marie Pédrot (Dec 08 2020 at 14:07):

Is it documented somewhere why or under which conditions doing a clear on section variables is not safe?
I'd rather ask the converse, i.e. when it's safe...

Paolo Giarrusso (Dec 08 2020 at 14:38):

If clear stays broken, every piece of ltac iterating over hypotheses has to work around this problem.

Paolo Giarrusso (Dec 08 2020 at 14:39):

And ltac itself must provide support for it. Should we provide and use appropriate variants of match goal?

Paolo Giarrusso (Dec 08 2020 at 14:40):

For now, every use case I see would prefer a working clear.

Paolo Giarrusso (Dec 08 2020 at 14:44):

And it'd be fine if clear just "hid" hypotheses, as long as the hiding worked well... Or is that the current fragile mechanism?

Guillaume Melquiond (Dec 08 2020 at 14:53):

If I remember correctly, what is important is that no other variable can be named the same as a cleared variable, whichever way it was cleared.

Andrej Dudenhefner (Dec 08 2020 at 15:57):

Guillaume Melquiond said:

If I remember correctly, what is important is that no other variable can be named the same as a cleared variable, whichever way it was cleared.

Interestingly, the following example works fine although the introduced assumption is named the same as the cleared variable

Require Import Lia.
Set Default Proof Using "Type".
Section Capsule.

Context (n : nat) (H : n = 0).

Lemma main : 0 = n -> n = 0.
Proof.
  clear H. intro H. lia.
Qed.

End Capsule.
Print main.

Andrej Dudenhefner (Dec 08 2020 at 16:01):

Something more evar-happy like clear H. intro H'. evar (H : n = 0). lia. Unshelve. lia. also works fine.

Fabian Kunze (Dec 08 2020 at 16:09):

One example where reusing section variable names leads to problems is this: https://github.com/coq/coq/issues/6773

Emilio Jesús Gallego Arias (Dec 08 2020 at 16:09):

Indeed @Paolo Giarrusso there were some discussions year ago in a presential CUDW on how to hide variables, bracketing, etc... We had some ideas but that is far from straightforward, tho there is a first task to do here IMHO, which is to refine the env used in the tactic engine.

Emilio Jesús Gallego Arias (Dec 08 2020 at 16:10):

Guillaume's example is not problematics as the proof term is closed and the inner H never shows up

Andrej Dudenhefner (Dec 08 2020 at 16:19):

#6773 does not use clear though; so maybe that one is more about induction.

Fabian Kunze (Dec 08 2020 at 16:22):

The point is that it's not at all about clear, it's about reusing variable names that "shadow" section variables. induction 'clears' in the background/reuses the same name as the variable one performs induction on.

Andrej Dudenhefner (Dec 08 2020 at 17:53):

I've boiled https://github.com/coq/coq/issues/6773 down to a minimal example (https://github.com/coq/coq/issues/6773#issuecomment-740796752). Hopefully this can be resolved, because the original problem of this thread is quite unfortunate.

Hugo Herbelin (Dec 08 2020 at 21:13):

See also this comment at #6773, whose objective is to eventually reach a solution. (Thanks to @Andrej Dudenhefner and @Paolo Giarrusso for linking both discussions!)

If courageous, you can also read this very long discussion at #883, and in particular this short comment from @Guillaume Melquiond.

Enrico Tassi (Dec 09 2020 at 08:25):

One example to rule them all is when the variable is used in extra logical stuff, like notations, hints, CS... Clear does not see, hence fix, these data bases. Also, you can re introduce a new variable picking the same name, as a side effect changing the meaning of extra logical data about the cleared variable.

IMO nothing is safe by design in this model. Still, if a variable has no metadata and you, or the name generator, doesn't reuse the same name, then clear should be safe :grimacing:

Enrico Tassi (Dec 09 2020 at 08:27):

To be clear, we talk about clearing section variables, not proof variables. These are fine.

Gaëtan Gilbert (Dec 09 2020 at 08:50):

clearing proof variables is not always fine, you can give them "metadata" in the ltac state
typically let x := constr:(some_var) in clear some_var; reuse some_var; use x

Enrico Tassi (Dec 09 2020 at 10:26):

IMO we should sit around a table and extend CEP 11 to encompass not only "proof language state" but a substantial subset of the system state. Not easy to get right and efficient, but it's the only way I can make sense of | Var of string and clear

Pierre-Marie Pédrot (Dec 09 2020 at 10:31):

I agree with the sitting around a table part, but I don't think that the solution consists in enriching the goal state (which, as I will never get tired to repeat, only an approximation not preserved by some components).

Pierre-Marie Pédrot (Dec 09 2020 at 10:32):

We already have a notion of global state in the engine, but the problem is not so much that we cannot store section data (actually we do).

Pierre-Marie Pédrot (Dec 09 2020 at 10:32):

Rather, for most of the infrastructure the notion of section seems to have been an afterthought.

Pierre-Marie Pédrot (Dec 09 2020 at 10:34):

It's not as if this has not been discussed already, I've heard about revamping sections already almost 10 years ago...

Pierre-Marie Pédrot (Dec 09 2020 at 10:35):

The bleak reality is that we still don't have a good idea of the solution, although we know it's going to be painful, likely both for devs and users alike.

Enrico Tassi (Dec 09 2020 at 12:56):

I think the implementation of Section is orthogonal here. Or at least, the fact that they don't abstract immediately, hence the kernel backdoor...

The problem of clear is another one. We don't have a notion of Var "x" goes out of scope, and this is problematic for the metadata you can attach to it. When Var is used to implement section variable, we do know when it ends, and we can remove the associated metadata at section closing time.

At the same time, we have use cases about adding implicits, notations, ... on proof variables, which are represented with the same Var node of section variables, but we can't because their lifetime is not that simple (and commands explicitly check you pass to it a section variable and not a proof variable).

I don't know exactly how to implement it (efficiently), but I can imagine the map metadata : variable -> 'a to be part of the state of a goal.
The same Var "x" can mean different things in different goals, and hence have different metadata. If this map is part of the goal state, we can start by inheriting the global one (the one for section variables), but then update it following goals, and make clear sound with respect to all metadata (clear would create a new goal with a thinner metadata map, and introducing a new variable with the same name will not resurrect the metadata).

Yes, CEP 11 is not working well when you cross the V8.2 compat boundary, and we have APIs to fiddle with goals... but I still believe that is the right direction.

Enrico Tassi (Dec 09 2020 at 13:03):

(I know this is not the simplest solution, forbidding "clear" on section variables is trivial to implement, but fixing the problem of clear in the way I sketch paves the way to features that are want)

Paolo Giarrusso (Dec 09 2020 at 19:47):

If you forbid clear, then this example could become a wontfix and Lia (and my custom tactics) wouldn't need to be fixed. Except that (maybe) "red in *" (or such) would have an effect on some TC assumptions.

Last updated: Apr 20 2024 at 08:02 UTC