long term mode proofs

Stream: general

[Johan Commelin]

My experience is that I find fixing/maintaining long term mode proofs harder than fixing/maintaining long tactic proofs.
What are the benefits of writing long term mode proofs?

[Patrick Massot]

I think it's mostly showing off.

[Sebastien Gouezel]

Also making sure no one can touch it ever, so it remains your proof.

[Mario Carneiro]

Doesn't isabelle style map to term mode proofs (using lots of have/show)?

[Mario Carneiro]

I guess that's the initial motivation for most of the keywords and such

[Patrick Massot]

If I understand correctly, Isabelle style map to using SledgeHammer in Lean, so it maps to nothing

[Scott Morrison]

For me, the difference between term and tactic mode proofs that require diagnosis all comes down to the fact that I find it so much more convenient to read the intermediate tactic state in a tactic mode proof than in a term mode proof.

[Scott Morrison]

Even if there are lots of "literate" have, show, and assumes.

[Sebastien Gouezel]

No, Isabelle style maps to structured tactic proof (you have a goal state that you can see all the time in your proof).

[Mario Carneiro]

It sounds like all complaints boil down to the same thing: you can't see the tactic state in a term proof

[Mario Carneiro]

this is literally a feature that existed in lean 2

[Mario Carneiro]

there is no innate reason why term proofs can't show the context and expected type

[Mario Carneiro]

so I don't see it as a failing of term mode so much as a missing feature in lean 3

[Patrick Massot]

You can open a PR to Lean3, but I'm not sure this will exist in Lean4

[Johan Commelin]

How hard is it to add this feature (to Lean 3.x.c)?

[Gabriel Ebner]

It depends on what you want. If you want to have it show up as the goal, then I think the hardest part is figuring out what types to show. That is, where do you want term-mode goals in f (by exact g (by simp) b)?

[Bryan Gin-ge Chen]

What was it like in Lean 2?

[Mario Carneiro]

You could place your cursor over a parenthesis and it would tell you the type of the expression

[Mario Carneiro]

I think the most useful thing would be, if you mouse over a constant it shows the goal that you would get if you replaced the entire application with that constant at the head with _

[Mario Carneiro]

so for f (by exact g (by simp) b) you could mouse over f and get the result type, g gives you the same as the exact, the open paren on by simp gives you the type that simp is solving, and b gives you the type of b

[Patrick Massot]

This would be useful even for tactic mode, since we still use a lot of short terms there.

[Sebastian Ullrich]

I don't think it ever displayed the context, did it?

[Sebastian Ullrich]

Parentheses always felt a bit arbitrary, Mario's suggestion sounds more sensible to me

[Mario Carneiro]

This was back in the days when it was emacs mode and the context display was this janky console printing thing

[Mario Carneiro]

I think it showed the type in the mini-bar

[Reid Barton]

It would be nice if have, let etc. also qualified as "constants" here.

[Chris Hughes]

I find that long tactics mode proofs can often be very hard to maintain, because they're not divided up, and you can't tell how to fix it, because you don't know what the tactic state was supposed to look like, and the thing that changed is not necessarily anywhere near the bit that breaks.

[Chris Hughes]

This is more of a issue with haves versus no haves rather than term mode or tactic mode.

[Mario Carneiro]

I think you should try to keep any proof below about 100 lines. Beyond that it should be broken up into lemmas, which are better in every way with respect to understandability, doc comments, having intermediate statements, and increasing build parallelism

[Mario Carneiro]

actually 100 is too generous. Even 50 is pretty big

[Mario Carneiro]

Looking at my most recent big proof in #2792 , the longest proofs are 38, 59, and 83 lines, and the 83 line proof has two really obvious sub-lemmas that it could be broken into. There is also a 50 line definition but that is written with deliberately short lines for formatting reasons

[Patrick Massot]

That's simply not how real maths work. Of course you can always use extract_goal to cut a proof into pieces, but you'll get meaningless lemmas.

[Mario Carneiro]

Of course, I'm talking about good lemmas here, not just chopping the proof in half

[Mario Carneiro]

Of course this is how real maths works, humans have to chunk things up in order to understand them, and this happens all the time in paper proofs

[Mario Carneiro]

But the inductive step of a tricky induction is also a reasonable place to make a lemma, even though it may not be the prettiest thing

[Mario Carneiro]

I want to fight the notion that every top level theorem/lemma should be "meaningful". This is actively harmful in formalization

[Gabriel Ebner]

lean#275

[Gabriel Ebner]

This is a quick&dirty implementation. If you really want this, you need to live with unexpected side effects.

[Patrick Massot]

What if you are in a term inside tactic mode?

[Patrick Massot]

For instance in the stupid example by exact some_term sub_term other_arg?

[Gabriel Ebner]

It's a bit quirky. Between by and exact it will show you the goal of the tactic block. On some_term, sub_term, other_arg it will show you the type of the subterm.
So far as expected. But it will also show the tactic block goal on the space between some_term and sub_term. :shrug:

[Johan Commelin]

Isn't the type of some_term going to be the same thing as the by exact?

[Johan Commelin]

Ooh... will it show the full goal state, or only types?

[Johan Commelin]

Screenshot suggests full goal state

[Gabriel Ebner]

Yep, full goal state!

[Johan Commelin]

I think it's time for a new lean release! It's been like 3 days already!

[Gabriel Ebner]

I'm kind of waiting for @Edward Ayers to finish dividing up the widget PR. But depending on how long that's going to take, we could also make a release now.

[Patrick Massot]

Oh yes, let's have that widget thing!

[Johan Commelin]

There are 12 new commits already...

[Johan Commelin]

Otoh... I guess there won't be much mathlib breakage... so that isn't a reason to release early

[Gabriel Ebner]

Mmh, there is also one change that might reduce linting time by up to 50%. So maybe it's better to test it soon.

[Jason Rute]

By the way, in IntelliJ (and other JetBrains projects like PyCharm) if one selects a term/expression and presses cntr-cmd-P (on a mac, don't know the windows keys off hand) it shows the type of the term. It is amazingly useful, especially in Scala (but even in Python). I wonder if vs-code has support for something like this.

[Jason Rute]

Maybe relevant: https://github.com/microsoft/vscode/issues/65890

[Reid Barton]

(Python? what kind of type information does it give?)

[Jason Rute]

Python has static types now! Well sort of. Also, IntelliJ is pretty smart about guessing the type. If your function only has one return and it returns a string, then it knows the type of the function output is a string, for example.

[Shing Tak Lam]

In VSCode if you hover over a variable it gives you the type (if it can figure it out/has type hints)

[Jason Rute]

That is the problem. In IntelliJ you can hover over a selection. That is a big difference than a single variable.

[Gabriel Ebner]

The vscode side is easy. The hard part is the Lean side, we don't really store enough information to interpret ranges as expressions. At the moment we only store one position per expression (typically the "start").

[Jason Rute]

Yeah, I'm thinking for the future, like Lean 4. But are you sure this exists in vs-code for any language? The issue I linked above suggested that it maybe doesn't.

[Gabriel Ebner]

Yeah, I don't think any language extension does that so far. But we're doing many things in Lean that other languages don't.