Mathlib `have` tactic support

[hrmacbeth]

The Mathlib have tactic does not seem to be supported yet, is that right?

The following two code snippets are mathematically equivalent, as far as I'm concerned, and it would be nice if they produced the same display:

import Mathlib.Tactic.Positivity
import Mathlib.Tactic.Linarith
import Paperproof

example {x y : ℚ} : 2 * x * y ≤ x ^ 2 + y ^ 2 := by
  have H : 0 ≤ (x - y) ^ 2 := by
    positivity
  linarith

example {x y : ℚ} : 2 * x * y ≤ x ^ 2 + y ^ 2 := by
  have H : 0 ≤ (x - y) ^ 2 
  · positivity
  linarith

But they generate different Paperproof output -- I think the one above (for core have) is much better than the one below (for Mathlib have). I'm not sure if there is a principled reason for the difference or if it's just that Mathlib have is not yet explicitly supported.

[antonkov]

Hi Heather, that's indeed an interesting example.

tldr; Paperproof doesn't explicitly check tactic names and tries to be as generic as possible. However the heuristic we apply to prettify have-like tactics isn't generic enough yet to capture the second case. I agree that the Paperproof output for the two proofs should be the same and will think how we can generalise the heuristic further.

details The reason regular have produces the better output is because we have the following heuristic: https://antonkov.github.io/posts/How-to-build-a-proof-tree/#how-tactics-like-have-fit-into-the-model

• have H : 0 ≤ (x - y) ^ 2 := by positivity was treated as a single step which

  1. didn't bifurcate the goal
  2. goal type stayed unchanged.

• whether have H : 0 ≤ (x - y) ^ 2 · positivity was treated as a sequence of 2 steps. have without := bifurcated the goal into 0 ≤ (x - y) ^ 2 and the one with H in the context. But because of bifurcation the heuristic didn't apply.

[lakesare]

Modern Lean errors out with the second-example code unfortunately: https://live.lean-lang.org (unexpected token '·'; expected '|').

I will close this issue for now - if you have a way to recreate a similar issue in modern Lean, please reopen.

[hrmacbeth]

I believe it's just that in current mathlib one needs another import:

import Mathlib.Tactic.Have

[lakesare]

From what I see, Paperproof renders this appropriately. These are mathematically similar statements, but they are structurally different - and Paperproof accurately reflects that.

When we go through this proof:

example {x y : ℚ} : 2 * x * y ≤ x ^ 2 + y ^ 2 := by
  have H : 0 ≤ (x - y) ^ 2
  · positivity
  linarith

letter by letter, we do have two goals at some point:

And this is reflected in Paperproof:

The second proof is rendered differently from the first one because it offers different functionality. For example, in the second case, the user can type pick_goal 2 (and that's obvious from the way paperproof renders it), while in the first case they cannot do that. Also, our visualisation of the second proof makes it obvious what the role of · is, and what will happen if we leave it out. I think it makes sense for Paperproof to follow exactly what's going on in the proof internally. I think rather than aiming for the prettiest possible visualisation of a proof, we want to aim for high trust that "paperproof will display the proof as it really is internally".

Open to objections though.

[hrmacbeth]

That seems reasonable. Thanks for thinking about it.