paperproof discussion

Stream: general

[Johan Commelin]

Paperproof was announced here: https://leanprover.zulipchat.com/#narrow/stream/113486-announce/topic/Announcing.20Paperproof

This is a thread for questions and discussions related to the announcement.

[Johan Commelin]

@Evgenia Karunus Thanks for creating paperproof! This looks like a nice mode for beginners. I have some UI/UX questions:

• Looking at the screencasts, it feels to me like the boxes take up quite a bit of space. Have you considered a "compact mode" with smaller padding for the boxes?
• Are you considering input options for paperproof? Or is it meant as an output/display mode only? I'm thinking of point-and-click / drag-n-drop UIs for certain tactics.

Maybe this should be orthogonal to paperproof, so that the regular infoview can also benefit from it... I have no idea if that would be possible from a design point of view.

[Evgenia Karunus]

@Johan Commelin, re:more compact version - highly desired, but we first plan to switch from tldraw.js to vanilla react - making these changes within the confines of tldraw is surprisingly hard. Another trick for making the proof look compact is subgoal collapsing - also would be straightforward with vanilla react.

Same goes for point&clicking/drag&dropping - also will be straightforward with vanilla react, and is also a desired functionality - this one we need because we want intergration with ReProver where the user creates a node with a new hypothesis/goal type, and ReProver suggests a tactic. In fact @Kaiyu Yang & @Anton Kovsharov already trained a custom ReProver model for us that returns a tactic based on [current tactic state, desired after state with the nodes we added], works pretty great locally.

[Ruben Van de Velde]

I was curious to try it in mathlib, but it seems like it needs a bunch of code changes to the project to work. Are there ideas on avoiding that?

[Evgenia Karunus]

@Ruben Van de Velde, nope, you don't need any code changes to make it work (only require Paperproof ... in lakefile.lean and import Paperproof in a file you're working on), it should work as is. Are you stumbling upon some issue during the installation?

[Heather Macbeth]

@Evgenia Karunus Thank you for this interesting development! Some first impressions from the
following (artificial) example:

import Mathlib.Tactic.Linarith
import Mathlib.Tactic.GCongr
import Paperproof

example {m n : ℤ} (h1 : m + 3 ≤ 2 * n - 1) (h2 : n ≤ 5) : m ≤ 6 := by
  have h3 :=
  calc
    m + 3 ≤ 2 * n - 1 := by gcongr
    _ ≤ 2 * 5 - 1 := by gcongr
    _ = 9 := by norm_num
  clear h1 h2
  linarith

1. Would it be possible to notice when a tactic invokes a hypothesis without naming it. E.g. in this example the first gcongr uses h1, the second uses h2, and the linarith uses h3, but there is no little arrow to the box like there is if I change to respectively rel [h1], rel [h2], linarith only [h3]
2. The calc is presented out of order in the above example, how hard would it be to enforce that the calc appears in the same (transitive) order as in the code?

[Anton Kovsharov]

Heather Macbeth said:

Evgenia Karunus Thank you for this interesting development! Some first impressions from the
following (artificial) example:

import Mathlib.Tactic.Linarith
import Mathlib.Tactic.GCongr
import Paperproof

example {m n : ℤ} (h1 : m + 3 ≤ 2 * n - 1) (h2 : n ≤ 5) : m ≤ 6 := by
  have h3 :=
  calc
    m + 3 ≤ 2 * n - 1 := by gcongr
    _ ≤ 2 * 5 - 1 := by gcongr
    _ = 9 := by norm_num
  clear h1 h2
  linarith

1. Would it be possible to notice when a tactic invokes a hypothesis without naming it. E.g. in this example the first gcongr uses h1, the second uses h2, and the linarith uses h3, but there is no little arrow to the box like there is if I change to respectively rel [h1], rel [h2], linarith only [h3]
2. The calc is presented out of order in the above example, how hard would it be to enforce that the calc appears in the same (transitive) order as in the code?

Hi Heather,
thanks for the great example

Regarding #2, unfortunately our Lean InfoTree parser doesn't support it yet, you'll need to annotate have h3 with the type and also use by calc for now
Screenshot-2023-10-22-at-22.48.49.png

To fix it we'll need to close a couple of TODO's in our parser:
1) Support multi-subproof tactics https://github.com/Paper-Proof/paperproof/blob/dff701770efeb9c9225095c3499acc4a4369ae46/lean/BetterParser.lean#L147
2) Support have's without type annotation
3) Support term based have definition

hopefully we will be able to resolve all of it soon
--
Regarding #1 ideally we would like to show the hypothesis used in the term assigned to the metavariable constructed by tactic (e.g. like show_term command from Lean 3). So that linarith,simp, etc show the hypothesis actually used. I was looking into that however struggled to connect dots with my mental model and used simple command syntax parsing for the first version.
I'm going to revisit it too, as the behaviour you mentioned is the desirable one.

I'm going to track work on this issue here https://github.com/Paper-Proof/paperproof/issues/27

[Heather Macbeth]

@Anton Kovsharov Thanks, I'm glad this is a useful example!

By the way, do you know why the calc is still presented out of order in the screenshot you just posted with the type-annotated, tactic-mode have ... calc ...?

[Heather Macbeth]

(that is, I'd expect the three steps to appear left-to-right as
$m+3\le 2n-1\le 2\cdot 5-1=9$,
i.e. $m+3\le 2n-1$ then $2n-1\le 2\cdot 5-1$ then $2\cdot 5 - 1=9$)

[Anton Kovsharov]

Screenshot-2023-10-22-at-23.24.53.png
that's because we didn't sort goals :D Fixed and pushed, please reload vscode

[Anton Kovsharov]

Heather Macbeth said:

(that is, I'd expect the three steps to appear left-to-right as
$m+3\le 2n-1\le 2\cdot 5-1=9$,
i.e. $m+3\le 2n-1$ then $2n-1\le 2\cdot 5-1$ then $2\cdot 5 - 1=9$)

I fixed all the problems mentioned above, now the example looks like:
Screenshot-2023-10-28-at-15.42.44.png

also removing/adding clear h1 h2 changes what linarith uses to prove final goal (h1 + h2 or h3) and you can see paperproof changing accordingly
Screen-Recording-2023-10-27-at-18.22.59.mov

Now as the hypothesis used by tactic are parsed from actual term assignment instead of syntax parsing, some other interesting examples are:

• what assumption used
  Screenshot-2023-10-28-at-15.40.45.png

  

• or what simp [...] used
  Screenshot-2023-10-28-at-15.46.10.png

  

[Anton Kovsharov]

You'll need to reload VS code to get a new version and call lake update Paperproof this time since parser also updated. We will add some reminder from extension when there is a new version of lean library and lake update Paperproof should be called.

[Shreyas Srinivas]

I tried paper proof on some semantics stuff. Paper proof tried to fit to screenwidth which resulted in very small font output. Is there a setting I need to change so that it appears in normal size with scroll bars?
image.png

[Kevin Buzzard]

One suggestion is to change your VS code set up so that the paperproof window is on the bottom half of the screen, not the right half

[Shreyas Srinivas]

Kevin Buzzard said:

One suggestion is to change your VS code set up so that the paperproof window is on the bottom half of the screen, not the right half

It doesn't help much.
paperproof_vertical_no_improvement.png

[Shreyas Srinivas]

is there an option to split the paper proof by only showing the tree upto a certain depth and linking to other "pages" for each subtree?

[Anton Kovsharov]

Screen Recording 2023-11-07 at 22.04.25.mov you should be able to zoom in/out by clicking on the subproof rectangle and out of it

[Shreyas Srinivas]

Ah yes, zoom and scroll works with my trackpad as soon as I click on a box (although this also shows me a blue box around the selected box which is bigger in size than the other box and cuts into neighbouring boxes)

[Shreyas Srinivas]

At the moment the overlap is not a big deal. Thanks :)

[Evgenia Karunus]

although this also shows me a blue box around the selected box

I haven't stumbled upon this, but this sounds like a focus ring - try pressing ESC.

[Shreyas Srinivas]

Hitting esc makes the ring disappear while still permitting zooming and out. This does mean two steps before zooming+scrolling becomes possible, but I don't mind it. I like this way of reading proofs, especially for this topic.

[Evgenia Karunus]

I'm surprised you're stumbling upon the focus-ring issue, vscode is supposed to come with the same browser version for everyone. I suspect you somehow went into non-read-only mode, try CMD+SHIFT+P Developer: Reload Webviews, it's possible you won't need to ESC after that refresh.

[Shreyas Srinivas]

Still get it

[Anton Kovsharov]

I also see blue ring (using cursor.so) - there is also vscode-insiders