click on symbol, get all valid apply/rws ?

Stream: general

[TongKe Xue]

Is there some plugin/way to enable the following:
we click on a symbol, and get all valid apply/rws

For example, suppose we have (either hypothesis or goal) the expr

0 * (a + b)

if we click on the *, I'd like to get the option to

zero_mul => 0
mul_add => 0 * a + 0 * b

basically I'm looking for something where except for

1. filling in an exists
2. introducing a new lemma/expr/have
   to have the Lean4 system tell me all 'valid moves' involving a given expr

[Aaron Liu]

Well there's rw??

[TongKe Xue]

rw? is useful; thanks!

[Aaron Liu]

oh I meant rw?? not rw? (unless they changed the name?)

[Aaron Liu]

I think rw?? is better than rw?

[Kevin Buzzard]

"all valid moves" will leave you swamped. Any theorem of the form "F a = F b => a = b" would apply, for example, and leave you with a typically far more complicated goal.

[TongKe Xue]

I see. I guess transitivity lemmas also have infinite options:

a  = b -> b = c -> a = c
a \leq b -> b \leq c -> a \leq c

so basically unless we heavily limit the applicable lemmas (which makes this pointless), it's not really possible to build an UI of the form
"instead of people coming up with the tactic to apply, we list all applicable ones, and they pick one"

[Bhavik Mehta]

This is not far from what @Jovan Gerbscheid and the team in Cambridge are working on

[Jovan Gerbscheid]

Yes, the rw?? that I made will give you all the valid rewrite moves when clicking on a given expression. I'm currently working on an improved version that also gives apply suggestions. Hopefully I'll manage to PR this to mathlib soon!

[TongKe Xue]

@Aaron Liu @Jovan Gerbscheid

I'm confused. There is a rw?? ? When @Aaron Liu liu asked rw??, I thought it was a typo and inferred it as rw? ?

My vscode4/lean has a rw? but no rw??

[Michael Rothgang]

What version of mathlib are you on? Current mathlib definitely has rw??.

[Michael Rothgang]

It is unfortunate that there are two tactics with very similar names, that work differently. I hope rw? can be removed at some future point, so there will be only one tactic left (which we might rename to rw?).

[Mirek Olšák]

Do you import Mathlib? rw?? is in Mathlib, rw? is core.

[TongKe Xue]

screencast: https://www.youtube.com/watch?v=ACf69ZCC0Hk

[Aaron Liu]

You need to import mathlib

[Aaron Liu]

it's in the lakefile means your project depends on it

[TongKe Xue]

import Mathlib.Tactic


theorem easy : 2 + 2 = 4 := by
  rw??

^-- should this in theory work ?

[Aaron Liu]

but you still need to import the files in mathlib in the files in your project that depend on them

[TongKe Xue]

shift click is not working for me; hang on, recording part 2

[TongKe Xue]

https://www.youtube.com/watch?v=PYjVzr6917U everything works now

mathlib.tactic, rw??, and shift clicking (in the infoview, not editor)

this is very cool; glad we had this conversation & followup

Something else I was thinking: anyone trying to build a basic RPG game out of this? when you go around solving "puzzles", but the "puzzles" are levels of undergrad math; and part of this is to have a UI where it presents a finite set of options you use to solve the problem

[Kevin Buzzard]

You know about #nng right?

[TongKe Xue]

I've worked through all Natural Number Game ( https://www.youtube.com/watch?v=IQ-PUxz1u-Y ).

NNG is awesome, but I think it could also feel more "game like" (using rw?? for example). I have this crazy theory that the way to combat academic cheating in the ChatGPT age ... is to make STEM education as entertaining as video games.

So imagine something like a Pokemon style RPG, but instead of the monster battle screen, we replace it with NNG + rw?? + massively gamified UI, and it becomes a source of high-repetition lean4 tactics on undergrad math content.

[Kevin Buzzard]

I agree that the UI could do with a lot more love, e.g. drag and drop or whatever. But AFAIK nobody has funding for anything like this right now.

[Alex Kontorovich]

Coming soon(ish)...
image.png
(Very preliminary prototype, thanks to @Jason Reed )

[Kevin Buzzard]

Every development like this means younger people can get involved.

[Jason Reed]

Happy to talk to anyone who wants to hear more about what we're up to and to hear opinions/thoughts on what you think is important or what's stumbled in the past

[Jason Reed]

My team at the FRO is actively thinking about possibilities for lean games

[Matthew Ballard]

Vision Pro games? (this is not serious or maybe only slightly so)

[Snir Broshi]

Jason Reed said:

Happy to talk to anyone who wants to hear more about what we're up to and to hear opinions/thoughts on what you think is important or what's stumbled in the past

The prototype looks very promising! Thought: Paperproof places multiple goals side-by-side, is it possible to do with the blocks?
image.png

(btw, is the prototype using Google's Blockly?)

[Jason Reed]

I have been looking at paperproof, and yes, that's blockly.

[Mirek Olšák]

Speaking of edutainment games, who have played my Cookie clicker? :slight_smile: :cookie:
Formalizing that one in Lean is a bit hard though... as always with approximate values. At some point I was thinking if Lean could help me guarantee at least Ordinaly but even there I didn't get too far... (but happy to pick it up if anyone is interested)

[TongKe Xue]

https://www.youtube.com/watch?v=sjz1MU7mLhQ

I would like to see a Beat Sabre style game:
buttons on the light sabres = tactics
gestures on light sabres = tactics
sabres can also used to point at stuff, i.e. thenth_rewrite #N [ ... ] at #H

and you have to "chop up" proof-states as quickly as possible

[Jon Eugster]

Kevin Buzzard said:

I agree that the UI could do with a lot more love, e.g. drag and drop or whatever. But AFAIK nobody has funding for anything like this right now.

There's a little bit of funding going into lean4game again, and responsiveness (incl. drag&drop) is on the roadmap. But time and therefore progress is limited... Agree that there's more that coule be done!

[Snir Broshi]

I found this cool "logic proof visualizer game" thingy https://incredible.pm/, I wonder if it can be generalized to do any term-mode proof

[Yaël Dillies]

Snir, if you hadn't realised, this Zulip is blessed with the presence of the creator of incredible.pm :slight_smile:

[Joachim Breitner]

I consider myself being the one that's blessed by being present in this community. But happy to hear that you liked the IPM, Snir!

[Johan Commelin]

So many blessings!

[Jörg Hanisch]

:octopus: