haves with blanks

Stream: mathlib4

[Kim Morrison]

I just came across a have statement

  have : HasFDerivAt (inversion c R) (_ : F →L[ℝ] F) (c + x) := by

in Mathlib.Geometry.Euclidean.Inversion.Calculus where the _ is determined by the proof. When the proof inevitably breaks, e.g. on nightly-testing right now, there's no easy way to even sorry the proof, without changing back to master, working out what term goes there, and filling it in manually.

Request 1: would someone mind fixing this instance on master?

Request 2: could we be more skeptical about allowing such placeholders in proofs, and resisting them during review?

I know they are sometimes convenient, but they add up to a maintenance burden that I doubt we can afford.

[Mario Carneiro]

I am dubious of the feasibility of applying this principle in general, because far more common than partially specified have statements are completely unspecified have statements have := ..., which suffer from exactly the same issue

[Mario Carneiro]

I also want to remark that having a working mathlib open in a separate folder / vscode instance is indispensable for debugging nightly-testing breakage and you should absolutely be doing this if you aren't already

[Kim Morrison]

(Yes, I have this. It's still annoying to have to go find the file in the other instance.)

[Yaël Dillies]

Scott Morrison said:

Request 1: would someone mind fixing this instance on master?

Request 2: could we be more skeptical about allowing such placeholders in proofs, and resisting them during review?

I know they are sometimes convenient, but they add up to a maintenance burden that I doubt we can afford.

Actually I don't think we should do either of these. @Tomas Skrivan and I were talking about writing a tactic to automatically compute the derivative of a function using fun_prop. So to me the solution is to write that tactic (shouldn't be so hard but I haven't had time to tinker) and use it.

[Eric Wieser]

I think Scott's issue here is that the proof outside the have is more fragile and harder to fix, as it is now less clear what particular normal form was chosen for the derivative

[Tomas Skrivan]

I think we need some guidelines for tactics generating data. They share similarities to non terminal simp which is discouraged as the resulting goal is highly unstable and that has a very high chance of breaking the rest of the proof.

What about having have? := by <tactic> with code action replacing it with have : X := by <tactic>.

[Yaël Dillies]

I don't think they "have a very high chance of breaking the rest of the proof", eg in that case a compute_deriv tactic would produce data corresponding to the shape of the input, so its output is basically unique

[Tomas Skrivan]

The tactic I have can very easily compute the derivative of fun x=> c + x either as fun x dx=> dx or fun x dx => 0 + dx. And by adding a theorem theorem to the environment you can switch from one to another.

[Kim Morrison]

Please note that this particular case is an actual broken proof. :-)

[Tomas Skrivan]

Yes that is why I'm suggesting having have? that would put the fully elaborated type in the code allowing you to use sorry if the proof breaks.

[Kim Morrison]

(My response was mostly directed at Yaël. :-)

[Yaël Dillies]

Well, you don't know how robust the tactic I'm thinking of is, since it doesn't exist yet :wink:

[Mario Carneiro]

Scott Morrison said:

Please note that this particular case is an actual broken proof. :-)

Is it broken because the inferred type of the have is wrong though?

[Mario Carneiro]

My impression is that this is just a debugging technique and actually once all is said and done it will turn out that the original proof was fine and the actual breakage is unrelated to changes in this have

[Kim Morrison]

No, it's just more annoying to debug.

[Mario Carneiro]

Maybe what you would rather have is some kind of robustify code action or other syntax transformer which inserts lots of intermediate goals and re-asserts the result of every step so that errors are more localized. I realize that this is why we have rules against non-terminal simp, but I think it may be a "why not both?" situation, we definitely want better tools for fixing breakage regardless

[Kim Morrison]

Another great code action might be sorryify, which e.g. replaces have h : P := by expensive_tactic with have h : P := by sorry_wrapper expensive_tactic.

(The idea of using the wrapper is that there would be in inverse code action to restore the proof, of course.)

[Kim Morrison]

(Presumably there are other things that could be sorrifyied beyond just the RHS of have.)

[Kim Morrison]

The intent here is working with longer proofs. Although of course proof incrementality, hopefully landing in the next release or two, will make this much less important.

[Kyle Miller]

(Regarding sorry_wrapper, there was discussion about sorrying out tactics and tactic blocks that has moved to https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/sorry.20a.20tactic.20block/near/427193728)