Display goal as LaTeX in infoview

Stream: general

[Li Xuanji]

Hello,

I am working on a tactic to display goals (and hypotheses) as LaTeX in the infoview. It's at a pre-alpha stage, but here's some demos of what it can do.

image.png

image.png

You can see further demos in this file, and the source code including some documentation of missing features here. It's currently a pretty simple tree-walking traversal of Expr plus some heuristics. PR's welcome!

Motivation: with ASCII expressions, I found precedence mistakes in my proofs (e.g. writing a * b / c when I meant (a * b) / c, but with longer subexpressions) too hard to spot even with mouseover. These sometimes block tactics like rw and linarith from working.

[Johan Commelin]

Cool! But I have one question. In the second screenshot, where does the $\xi_0$ come from? Shouldn't that be $i$?

[Johan Commelin]

Aha, that's just how you are printing bvars at the moment.

[Johan Commelin]

I wonder whether it would be possible to make use of the delaboration framework. In particular, that might help with making this extendable.

[Kyle Miller]

Neat!

I happen to have a library for pretty printing to LaTeX (LeanTeX) that you might be interested in. I just updated it to the newest Lean version, and I incorporated your code for doing HTML display if you don't mind.

This library doesn't have many pretty printers for mathlib (and it doesn't even import mathlib itself), but in principle it's extensible.

Here's an example from test/widget_bigop.lean:

variable (s : Finset Nat) (t : Nat → Finset Nat) (x : Real)
#texify λ (c : Nat) => c * s.sum (λ x => (t x).sum (λ y => x * y))

image.png

Here's one from test/widget_basic.lean:

example (x y : Nat) (h : x < y) : 2 * x < 2 * y := by
  texify
  sorry

image.png

Feel free to make use of LeanTeX in your project! Writing the LaTeX pretty printers is currently a bit obscure unfortunately. The current rules are in LeanTeX/Builtins.lean. I think it would make sense to have another LeanTeX repo with additional mathlib-specific rules.

Edit: now https://github.com/kmill/LeanTeX-mathlib is the part that imports mathlib and adds mathlib-specific pretty printers.

[Kyle Miller]

The status of LeanTeX now is that https://github.com/kmill/LeanTeX-mathlib can be a place for mathlib pretty printers.

I looked through your system and LeanTeX-ified the printers you defined. Examples:

example (a b c : ℝ)
    (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) (h : a*b*c = 1) :
    3 ≤ Real.sqrt ((a + b) / (a + 1)) + Real.sqrt ((b + c) / (b + 1)) + Real.sqrt ((c + a) / (c + 1)) := by
  texify
  sorry

image.png

example (n : ℕ) : ∑ i ∈ Finset.range n, i = n * (n - 1) / 2 := by
  texify
  sorry

image.png

theorem imo1966_p4 (n : ℕ) (x : ℝ)
    (hx : ∀ t : ℕ, ∀ k : ℤ, x ≠ k * Real.pi / 2^t) :
    ∑ i ∈ Finset.range n, 1 / Real.sin (2^(i + 1) * x) =
    1 / Real.tan x - 1 / Real.tan (2^n * x) := by
  texify
  sorry

image.png

[Oliver Nash]

I've mentioned this before but a widget feature that I think would be easy to build and quite useful would be a rendering of all functions / morphisms.

The idea would be to inspect the context for any function term (e.g., any term carrying a docs#FunLike instance), render a node for any type that occurs as the domain / codomain of one of these function terms, and then add arrows for all the function terms.

[Oliver Nash]

(If this worked well, it could even be made interactive with features like: "click here to generate a have statement capturing the fact that this part of the diagram commutes" etc.)

[Li Xuanji]

LeanTex-mathlib looks great! It even handles the goal here properly, which I was pretty afraid of working on :sweat_smile:

image.png

I'll play with it more when I have time on the weekend

[Shreyas Srinivas]

I wish this were part of the lean4 extension

[Martin Dvořák]

Long shot but can you do block matrices?