Autogenerating parts of `calc`s

Stream: maths

[Eric Wieser]

Perhaps we could have calc? which outputs

calc A = A : _
     _ ≤ B : _

For the goal A ≤ B

[Heather Macbeth]

My dream here is actually a full calc widget, where you click on a subterm and it adds a new line with a hole replacing the subterm and a rel_congr partial proof focusing on the hole, as well as other UI features (drag and drop a hypothesis, click to combine two rel_congr lines into one, etc).

[Kevin Buzzard]

Eric Wieser said:

Perhaps we could have calc? which outputs

calc A = A : _
     _ ≤ B : _

For the goal A ≤ B

ha ha I remember asking for this with Lean 3 calc in about 2018 :-) I had an essentially isomorphic moan that it was hard to remember the syntax. I think the Lean 4 syntax is easier though (although IIRC someone was complaining that spacing issues can give counterintuitive errors)

[Yaël Dillies]

I think it would be even easier if the underscore could be replaced by something more visible when underlined, eg a dot

[Patrick Massot]

Eric Wieser said:

Perhaps we could have calc? which outputs

calc A = A : _
     _ ≤ B : _

For the goal A ≤ B

Nice proof by example: the Lean 4 syntax is really hard to remember. Your : should be := (I don't know why).

[Mario Carneiro]

Patrick Massot said:

Your : should be := (I don't know why).

Because the thing on the right is a proof of the thing on the left. If you use statement : proof it's backwards from every other use of : in lean

[Kevin Buzzard]

(sorry, just accidentally renamed this entire thread in an attempt to move a post (I didn't know I could do that with other people's threads) and couldn't remember what it had been called before so have guessed)

[Mario Carneiro]

you can see it in the edit history

[Yaël Dillies]

Restored

[Joachim Breitner]

Yaël Dillies said:

I think it would be even easier if the underscore could be replaced by something more visible when underlined, eg a dot

Coming from Isabelle, the natural and pretty symbol here would be …
Quite similar to pen and paper proofs that way.

[Notification Bot]

10 messages were moved here from #maths > New tactic for "relational congruence" by Heather Macbeth.

[Yaël Dillies]

That's what we have in Lean 3 (well, ...). Not sure why we changed. Maybe to have a single character?

[Eric Wieser]

Doesn't ... mean "as many _s as required" in Lean4?

[Thomas Murrills]

That’s ..—... might be unused?

[Eric Wieser]

Yaël Dillies said:

That's what we have in Lean 3 (well, ...). Not sure why we changed. Maybe to have a single character?

Having a single character is pretty handy for aligning

calc
  A = B := _
  _ = C := _

vs

calc
    A = B := _
  ... = C := _

(is this the right syntax for Lean 4 now?)

[Heather Macbeth]

True, but most goals proved by calcs don't have single-character LHS!

[Eric Wieser]

In lean 3 I would often have a single character there; a single underscore!

def foo : some_long_type ≃ some_other_long_type :=
calc _ ≃ some_intermediate_type : sorry
   ... ≃ some_other_intermediate_type : sorry
   ... ≃ _ : sorry

though I don't know if that's still legal in Lean 4.

[Ruben Van de Velde]

It is, yeah

[Pedro Sánchez Terraf]

Eric Wieser said:

Yaël Dillies said:

That's what we have in Lean 3 (well, ...). Not sure why we changed. Maybe to have a single character?

Having a single character is pretty handy for aligning

calc
  A = B := _
  _ = C := _

It could even be just one (Unicode) character: “…” (U+2026):

calc
  A = B := _
  … = C := _

[Mario Carneiro]

Yaël Dillies said:

That's what we have in Lean 3 (well, ...). Not sure why we changed. Maybe to have a single character?

The reason it's a _ is because it's a term. There is nothing keywordish going on here. You can perfectly well not put _ there and write out the term

[Mario Carneiro]

Eric Wieser said:

In lean 3 I would often have a single character there; a single underscore!

def foo : some_long_type ≃ some_other_long_type :=
calc _ ≃ some_intermediate_type : sorry
   ... ≃ some_other_intermediate_type : sorry
   ... ≃ _ : sorry

though I don't know if that's still legal in Lean 4.

in other words, yes this is legal, you could put all the underscores on the RHS instead if you wanted, or even put underscores everywhere and use the proof term to determine the type

[Heather Macbeth]

In the porting meeting today, we discussed code actions which would be useful for calcs. Here's a general framework for the discussion: consider a proof with a goal A < Z, and a partially-complete calc block, together with some cursor positions I have labelled by number:

calc
  A < B := by (1) possibly_existing_proof_about_A_B
  _ < C := by (2) possibly_existing_proof_about_B_C
(3)

At (1) the goal is A < B, at (2) the goal is B < C, and at (3) the goal is C < Z.

Wishlist item 1: a code action which is triggered by having a cursor in one of the numbered positions, then clicking on a subterm of either the LHS or the RHS of the goal displayed at that numbered position. It would generate a row which is a duplicate of the LHS/RHS (whichever side was clicked on), which has a _ replacing the subterm that was clicked on, and which has a partial proof by rel_congr focusing on that subterm, and which is either above or below the existing row, as appropriate.

So, for example, if B has the form 3 * (x + y) + 5, clicking x + y as shown on the RHS of the goal at position (1) generates

calc
  A < 3 * _ + 5 := _
  _ < 3 * (x + y) + 5 := by rel_congr 3 * ?_ + 5; _
  _ < C := by possibly_existing_proof_about_B_C

and clicking x + y as shown on the LHS of the goal at position (2) generates

calc
  A < 3 * (x + y) + 5 := by (1) possibly_existing_proof_about_A_B
  _ < 3 * _ + 5 := by rel_congr 3 * ?_ + 5; _
  _ < C := by possibly_existing_proof_about_B_C

If C has the form 3 * (x + y) + 5, clicking x + y as shown on the LHS of the goal at position (3) generates

calc
  A < B := by possibly_existing_proof_about_A_B
  _ < 3 * (x + y) + 5 := by possibly_existing_proof_about_B_C
  _ < 3 * _ + 5 := by rel_congr 3 * ?_ + 5; _

If Z has the form 3 * (x + y) + 5, clicking x + y as shown on the RHS of the goal at position (3) generates

calc
  A < B := by possibly_existing_proof_about_A_B
  _ < C := by possibly_existing_proof_about_B_C
  _ < 3 * _ + 5 := _
  _ < 3 * (x + y) + 5 := by rel_congr 3 * ?_ + 5; _

[Heather Macbeth]

Wishlist item 2: a code action which is triggered when we have a proof with consecutive "disjoint" rel_congrs,

calc
  stuff < stuff := _
  [etc]
  _ < x ^ 2 + 4 * (y + z) := _
  _ < x ^ 2 + 4 * x := by rel_congr x ^ 2 + 4 * ?_; possibly_existing_proof_1
  _ < t ^ 2 + 4 * x := by rel_congr ?_ ^ 2 + _; possibly_existing_proof_2
  [etc]

and which cleans it up by combining the two lines to

calc
  stuff < stuff := _
  [etc]
  _ < x ^ 2 + 4 * (y + z) := _
  _ < t ^ 2 + 4 * x := by rel_congr ?_ ^ 2 + ?_; possibly_existing_proof_1; possibly_existing_proof_2; [sorries here, if more side goals are generated than before]
  [etc]

[Heather Macbeth]

I have bigger dreams, but I think said dreams would require rendering a clickable interactive version of the calc as a picture in the infoview. So these are intended as more modest proposals which might be doable with the current framework.

[Heather Macbeth]

I should say, also, that this is partly a record of a conversation with @Wojciech Nawrocki a few months ago. But maybe now that both widgets and rel_congr are more advanced, it is easier to state a proper specification.

[Mario Carneiro]

Are there any variations on these code actions (it sounds like you are describing not code actions but widgets) which would be applicable without rel_congr?

[Mario Carneiro]

Code actions in std have calc available but not rel_congr

[Mario Carneiro]

and even without that, not all calc proofs use rel_congr for the proof

[Mario Carneiro]

I suppose Eric's original suggestion could be done as a tactic code action

[Heather Macbeth]

For equality calcs, you'd want congrm (once it's ported) instead of rel_congr. But I think the pattern feature (common to both those tactics) will often be important in writing a partial proof which focused correctly.

[Heather Macbeth]

Honestly, rel_congr probably could move to Std; it imports

import Mathlib.Init.Algebra.Order
import Mathlib.Tactic.Relation.Rfl
import Mathlib.Tactic.Relation.Symm

and even those three imports are only for the limited amount of forward-reasoning on hypotheses.

[Mario Carneiro]

that should be an extensible tactic anyway, like we did for rel_congr_discharger

[Mario Carneiro]

I think we could also move rfl and symm

[Heather Macbeth]

I guess my point is that the situation when writing a new line of the calc is (most) annoying is precisely when it's largely the same as an existing line, with a difference in a subterm. And that's precisely the use case of rel_congr/congrm. For a new calc line which differs "in the large" from existing lines, there's no code action which could help -- you just need to write it out.

[Mario Carneiro]

I think some code actions (which, mind you, take no input other than the cursor/selection position) could be used to do structural editing of calc blocks, like the thing you mentioned about selecting a subterm and producing a new intermediate goal replacing this with _

[Heather Macbeth]

You mean, as opposed to letting the user select the subterm by clicking in the goal view? I do think that clicking in the goal view will be much more user-friendly (and less liable to user error).

[Mario Carneiro]

No "as opposed"

[Mario Carneiro]

this is just general support for calc block syntax trickiness

[Mario Carneiro]

clicking in the goal view isn't going to work in the near term because the goal view is not configurable/extensible like code actions are

[Heather Macbeth]

Perhaps what I don't understand is how you could reliably let the user select a subterm based just on the code. Would the action make a guess based on the fewest-characters-away head symbol?

[Mario Carneiro]

You can make a brand new widget and put whatever functionality you like in there

[Heather Macbeth]

Mario Carneiro said:

clicking in the goal view isn't going to work in the near term because the goal view is not configurable/extensible like code actions are

What about a widget which just displayed the existing goal, and let you click and do the things I was suggesting?

[Mario Carneiro]

but it won't actually be the goal view, and more likely than not the goal view will still be there

[Heather Macbeth]

That seems fine.

[Mario Carneiro]

sure, you can do that (or induce others to do so :) )

[Heather Macbeth]

Hoping for the latter .... I hadn't necessarily hoped for it immediately, but I got excited when Scott was asking about it in the porting meeting!

[Mario Carneiro]

but it's a rather heavyweight solution and probably not suitable for std (at least not on all calc blocks)

[Mario Carneiro]

so I'm thinking more in the direction of smaller "quick fix" style code actions that are more universally useful

[Mario Carneiro]

like eric's autocomplete suggestion

[Heather Macbeth]

Heather Macbeth said:

Perhaps what I don't understand is how you could reliably let the user select a subterm based just on the code. Would the action make a guess based on the fewest-characters-away head symbol?

Can you explain the answer to this? It's perhaps what I'm missing from your idea.

[Mario Carneiro]

code actions actually get a selection, not just a cursor position

[Mario Carneiro]

(the cursor is a Range)

[Heather Macbeth]

Do you mean, the user would highlight the subterm?

[Mario Carneiro]

so selecting subterms is a thing you can do, and we can also do something reasonable for point selections

[Heather Macbeth]

I think that could work if it was rather forgiving of the range selected. It would be frustrating to have to highlight exactly the right number of parentheses.

[Mario Carneiro]

when you hover any position you already see a highlight for the nearest enclosing subterm

[Mario Carneiro]

yeah, I would do something very forgiving, basically trying to give an answer to any possible cursor position / selection

[Mario Carneiro]

This is actually one of the issues with "term code actions" along the same lines as hole code actions: terms can be nested, so it's not always obvious whether you want a code action for foo to fire when your cursor is in the x of foo x y

[Heather Macbeth]

Right, and in this task it will do something different for every term and subterm, so you have to get it right.

[Mario Carneiro]

and I don't want to generate tens of code actions for every super-term of your cursor position, it needs to be just one for the user to be able to make sense of it

[Heather Macbeth]

Mario Carneiro said:

when you hover any position you already see a highlight for the nearest enclosing subterm

Can you clarify what you mean by this? I just fired up a mathlib4 to investigate, but can't see it.

[Mario Carneiro]

the other thing is that if possible I would like it to be implementable as one pass for all (or at least most) term code actions, because you basically have to scan the whole info tree to do anything with it, so if every code action does its own pass that's a lot of work per cursor move

[Mario Carneiro]

def foo := 1 + 2 + 3

If you put your mouse cursor over the first + you should see a highlight over the span 1 + 2

[Heather Macbeth]

Oh wait, I do see it .. it's a very faint highlight and half-covered by the pop-up.

[Heather Macbeth]

(I'll fix my VSCode settings.)

[Heather Macbeth]

OK, I can see how a code action (no widget) would work then.

[Heather Macbeth]

What about my other wishlist item? That seems like it doesn't need a widget either?

[Mario Carneiro]

that's certainly possible to do, it would be quite specific to rel_congr but should be implementable as a tactic code action

[Mario Carneiro]

actually I'm not sure about the sorries part, current code actions don't actually try to run the tactic in the new state to see what they would do, although I suppose they could

[Heather Macbeth]

I guess you could stick <;> sorry at the end so it doesn't need to know.

[Mario Carneiro]

or just nothing and let the user deal with the errors?

[Mario Carneiro]

we try to discourage proofs with subgoals not using . for focusing, not sure I like that this tactic is producing such proofs

[Heather Macbeth]

The important part for me would that in combining

rel_congr x ^ 2 + 4 * ?_; possibly_existing_proof_1
rel_congr ?_ ^ 2 + _; possibly_existing_proof_2

to

rel_congr ?_ ^ 2 + ?_; possibly_existing_proof_1; possibly_existing_proof_2; [sorries here, if more side goals are generated than before]

it put the proofs for the main goals, possibly_existing_proof_1 and possibly_existing_proof_2, in the right positions to deal with the new main goals. I think, as you say, that how or whether it deals with the side goals is secondary.

[Mario Carneiro]

well, this is made more awkward given that we decided to put the side goals in the same place as the main goals

[Heather Macbeth]

(FWIW, in my experiments with the tactic so far, I'd guess the side goals are being auto-resolved 90% of the time. But it is still very useful to have the tactic work sensibly when they're not.)

[Mario Carneiro]

you also have the reverse problem: the possibly_existing_proof_1 might actually be a side goal or start with a proof of one, which is gone or reordered in the new proof

[Heather Macbeth]

Yup!

[Mario Carneiro]

I'm not sure what we can do for those, since there is no guarantee of a correspondence between the old and new side goals

[Heather Macbeth]

Can the code action be a tactic itself?

[Mario Carneiro]

it isn't a tactic, but it can run elaborator functions and tactics on the original goal state, or make up a new goal state and run a tactic on that

[Mario Carneiro]

It's a plain IO action, but it has a bird's eye view of the original elaboration and can pick and choose states to work in

[Heather Macbeth]

Does it know which parts of the proof terms in the original 2-line proof were generated by rel_congr and which parts by possibly_existing_proof_n?

[Mario Carneiro]

you have the goals before and after each tactic, and by looking at the instantiations of before mvars in the after state you can also determine what partial proof term was generated by that tactic

[Mario Carneiro]

why would you care about proof terms here though?

[Heather Macbeth]

I figured you could reverse-engineer what main goals were generated purely by looking at the rel_congr lemmas used (and what is stored for them in the rel_congr attribute).

[Mario Carneiro]

the easiest way to keep track of the main goals would be to have rel_congr push a "the first 5 goals are side goals" log to the info tree

[Heather Macbeth]

I don't know what an infotree is, I guess it's one of the pieces of information about the original elaboration which you were saying was available to the code action?

[Mario Carneiro]

the info tree stores basically everything about lean's elaboration: the tactic states, the syntax and the terms they elaborate to, how many goals and the metavariable context to interpret them in, etc. All of the information I have been talking about is pulled out of the info tree

[Mario Carneiro]

and you can also put whatever custom information you want in there and pull it back out in code actions or what have you

[Heather Macbeth]

When rel_congr applies a congruence lemma, say for a pattern f x1 y z1 < f x2 y z2, it knows which hypothesis (or -es?) of the congruence lemma are associated to which of the pairs (x1, x2) and (z1, z2). So it should be able to store not just the pattern-tree of the match which rel_congr identifies between the LHS and the RHS, but also the "trace through the pattern-tree" which is the history of any main goal that results.

[Heather Macbeth]

(By "store" I mean "store in the infotree", if I'm understanding its capabilities correctly.)

[Mario Carneiro]

yes to the storage question, although I'm not sure I quite understand the data structure you are proposing

[Mario Carneiro]

If there is a template provided, you can pretty directly say which syntax corresponds to which main goal, but when there is no template you need to describe that same structure without the syntax

[Heather Macbeth]

To make a concrete claim: It seems to me that when rel_congr does this, even without a template:

example {a b x c d : ℝ} (h1 : a + 1 ≤ b + 1) (h2 : c + 2 ≤ d + 2) :
    x ^ 4 * a + c ≤ x ^ 4 * b + d := by
  rel_congr
  · linarith
  · linarith

you can keep track, from rel_congr's operation, of what the pattern _ * ?m1 + ?m2 must be, and also of the fact that the first goal is a relation between the two inputs in ?m1 and the second goal is a relation between the two inputs in ?m2.

[Mario Carneiro]

sure, it could generate a template expression (with deliberately unassigned ?m1 mvars), and then make a list of (?m1, ?g1) pairs for each main subgoal ?g1 produced

[Heather Macbeth]

So then the task is to take two rel_congr runs, like in my other example x^2 + 4 * ?m1 and ?m2 ^ 2 + _, which are both partial trips down the parse tree of the middle expression in the A < B < C they are proving, formally combine the trees to ?m2 ^ 2 + 4 * ?m1 with a p1/p2 possibly recorded as a proof for ?m1/?m2, run rel_congr again now on A < Cwith the pattern ?m2 ^ 2 + 4 * ?m1, and optimistically fill in pifor any main goals associated to ?mi in that last rel_congr run.

[Eric Wieser]

Heather Macbeth said:

calc
  A < 3 * (x + y) + 5 := by (1) possibly_existing_proof_about_A_B
  _ < 3 * _ + 5 := by rel_congr 3 * ?_ + 5; _
  _ < C := by possibly_existing_proof_about_B_C

It seems pretty unpleasant (at least, for long expressions) that we have to write 3 * _ + 5 twice here

[Eric Wieser]

A possible idea might be

calc_congr
  A < 3 * from%(x + y) + 5 := by (1) possibly_existing_proof_about_A_B
  _ < 3 * to%(y + x) + 5 := _ -- goal is add_comm
  _ < C := by possibly_existing_proof_about_B_C

[Eric Wieser]

Where the semantics are "use rel_congr to focus such that the goal is between the from in the previous step and the to in the current one"

[Eric Wieser]

That could extend to multiple (named) goals with from[name]% etc

[Eric Wieser]

Maybe you don't need from, and to alone is enough with heuristics

[Yaël Dillies]

Heather Macbeth said:

So, for example, if B has the form 3 * (x + y) + 5, clicking x + y as shown on the RHS of the goal at position (1) generates

calc
  A < 3 * _ + 5 := _
  _ < 3 * (x + 5) + 5 := by rel_congr 3 * ?_ + 5; _
  _ < C := by possibly_existing_proof_about_B_C

I assume this is a typo and the middle line should be 3 * (x + y) + 5?

[Mario Carneiro]

Eric Wieser said:

It seems pretty unpleasant (at least, for long expressions) that we have to write 3 * _ + 5 twice here

You don't. The template argument of rel_congr is optional

[Eric Wieser]

Presumably there are situations where the heuristic fails, like it does with congr on f (a + b) = f (b + a). In those cases, it would be nice to have a way to be precise about the target without having to repeat yourself

[Scott Morrison]

I mean, what we want is a bunch of coloured pencils, and you underline in one colour the corresponding changing pieces between lines n and n+1, and in another colour the corresponding pieces between lines n+1 and n+2, and so on.

[Scott Morrison]

Or at least, that's what I do in complicated calc blocks.

[Eric Wieser]

Semantic highlighting could in theory do that if we had the source code markers

[Joachim Breitner]

Eric Wieser said:

Heather Macbeth said:

calc
  A < 3 * (x + y) + 5 := by (1) possibly_existing_proof_about_A_B
  _ < 3 * _ + 5 := by rel_congr 3 * ?_ + 5; _
  _ < C := by possibly_existing_proof_about_B_C

It seems pretty unpleasant (at least, for long expressions) that we have to write 3 * _ + 5 twice here

Would this work (maybe a naive question):

calc
  A < 3 * (x + y) + 5 := by (1) possibly_existing_proof_about_A_B
  _ < _ := by rel_congr 3 * ?_ + 5; _
  _ < C := by possibly_existing_proof_about_B_C

I.e., if rel_congr is given a pattern, and the LHS is known, as it is here, will lean see that the RHS must be of shape 3 * _ + 5?

[Eric Wieser]

I don't think so; the problem is that the _ was a placeholder from Heather, the actual value is (say) 3 * foo x + 5, while the ?_ is literally ?_ to be populated by the tactic

[Heather Macbeth]

I'm imagining that the code action would generate the _, but then the user would fill it in to foo x

[Eric Wieser]

Perhaps generating a sorry would send a clearer message to the user that they have to fill it

[Heather Macbeth]

It doesn't seem to me that that would be a problem? The user clicked on that term because she wanted to replace it.

[Heather Macbeth]

Oh, maybe you mean the second _ rather than the first _ in

  _ < 3 * _ + 5 := by rel_congr 3 * ?_ + 5; _

[Heather Macbeth]

Sure, the second _ could be a sorry.

[Eric Wieser]

I meant the first _, but I guess I should have meant both (though I think Mario has argued that done is better for hole command-like things)

[Eric Wieser]

The user clicked on that term because she wanted to replace it.

Sure, but if the term contains _s already that they didn't click on (proof terms found by unification), then I think things are going to be confusing

[Heather Macbeth]

I think for a wide audience, having a sorry representing a mathematical expression (as opposed to a missing proof) is more confusing than that!

[Yaël Dillies]

Maybe we could have a hole tactic that's synonym to done (and maybe make it emit a custom warning).

[Eric Wieser]

That doesn't help with the LHS unless we also have a %hole term to use as 3 * %hole + 5

[Eric Wieser]

Maybe ?!_?

[Yaël Dillies]

Or a hole proof term that's synonym of `sorry|

[Heather Macbeth]

This really just doesn't seem like an issue to me. And I think multi-character solutions are awkward to interact with (more times hitting the backspace key) and lots of punctuation is forbidding. I'd suggest trying with _ before getting more baroque ... but of course, before we can even bikeshed properly, someone needs to implement it!