sokoban simplification

Stream: new members

[Miroslav Olšák]

I was playing with a sokoban formalization, https://github.com/mirefek/my-lean-experiments/blob/master/sokoban.lean
so far just a solvability definition, and a proof that a level is solvable by providing a solution. However, I would like to see the current state of the game in a natural way, that is

#######
#. * .#
#$   $#
#.$ $.#
#$  @$#
#. * .#
#######

rather than

(sokoban.move direction.right
     (sokoban.move direction.right
        (sokoban.move direction.left
           (sokoban.move direction.down
              (sokoban.move direction.down
                 (sokoban.move direction.left
                    (sokoban.move direction.right
                       (sokoban.move direction.right
                          (sokoban.move direction.left (sokoban.move direction.up soko_level))))))))))

Would it be possible to tell lean to perform all the beta reductions, and show me the current state, ideally in the way I defined in has_repr? When I add simp tactic anywhere inside, I receive an error message:

deep recursion was detected at 'infer_type' (potential solution: increase stack space in your system)

On the other hand, the reflexivity tactic is able to finish the proof relatively fast.

[Yakov Pechersky]

Check out https://github.com/Julian/lean-across-the-board/blob/main/src/guarini.lean

[Yakov Pechersky]

We got displaying of chess boards working.

[Yakov Pechersky]

with moves, I mean

[Yakov Pechersky]

I think dec_trivial might help you here.

[Yakov Pechersky]

Show in https://github.com/Julian/lean-across-the-board/blob/main/src/guarini.lean

[Miroslav Olšák]

I also got displaying working to some extent (I can run #eval), just not in the tactic mode.

[Miroslav Olšák]

As far as I understand, dec_trivial is only for finishing the goal using decidability. So I can use it as well instead of reflexivity, maybe it will work better on bigger levels.

[Miroslav Olšák]

I imagined that I could see the current level, as I am applying the particular steps. How does the visualisation work in the chess problem? I don't see visualisation in the guarini file (except for in the comments).

[Miroslav Olšák]

What I was now thinking was that I could maybe write a tactic which finds an instance of sokoban, evaluates it, converts it into a string, tries to prove that the new and the old versions are equal using dec_trivial or reflexivity, and if it succeeds, it performs rewriting. Just that

• it feels a bit overcomplicated
• the string as shown in the current goal displays newlines as \n rather than actual newlines. So maybe, the tactic should also print the sokoban state on its own...

Any better idea?

[Yakov Pechersky]

I think this is in the style of a norm_* normalization tactic/plugin for norm_num. It is normalizing the expression for some term, given some proof or proof context

[Yakov Pechersky]

The other option is to look at examples of a styling widget, like what was done for the Rubik's cube or sudoku examples: https://github.com/kendfrey/rubiks-cube-group https://github.com/TwoFx/sudoku

[Miroslav Olšák]

wow, that looks really fancy, I am not sure if I can do that

[Miroslav Olšák]

So, in the end, I wrote the tactic that I mentioned before (I updated https://github.com/mirefek/my-lean-experiments/blob/master/sokoban.lean). I would be however still interested if there is a better way to convince lean to do the gradual move simplifications as the solution proceeds.

[Yakov Pechersky]

You wrote the normalizer, nice =)

[Miroslav Olšák]

I looked at the html widget examples, and they are not working for me. Maybe, I am just doing something wrong with the VSCode (usually, I am using emacs). In sudoku, I just see the standard lean state, and in rubik's cube, I only get a message successfully rendered widget. Is there some necessary addon, or the right version of VSCode, or something like that?

[Miroslav Olšák]

Or I just don't know how to open it...

[Mario Carneiro]

The key to making it show up in the goal view is this stuff

[Mario Carneiro]

that creates the begin [show_sudoku] environment, which will call save_info to store the data needed for goal data to show up when you put your cursor inside the tactic block

[Miroslav Olšák]

ss_sudoku.png ss_rubik.png

[Mario Carneiro]

do you have a #mwe? It's hard to work with screenshots

[Mario Carneiro]

Oh, you cut off the tactic state view but it doesn't look like mine

[Mario Carneiro]

is there a dropdown in the corner that says "plain text" / "widget"?

[Mario Carneiro]

I have version 0.16.25 of the vscode-lean extension

[Miroslav Olšák]

I have 0.15.8, maybe, I should upgrade.

[Mario Carneiro]

vscode makes it a one-click fix

[Miroslav Olšák]

Click where? I am sorry, I am not used to VSCode.

[Miroslav Olšák]

Maybe, I have to upgrade the VScode itself.

[Mario Carneiro]

click on the extension button (looks like four squares on the left sidebar), then find "lean" in the list

[Mario Carneiro]

it probably says "update available" or something like that

[Miroslav Olšák]

I upgraded VScode, and it somehow automatically upgraded the lean extension.

[Miroslav Olšák]

However, it is still not working.

[Miroslav Olšák]

It looks the same, there is a dropdown in the corner with options no_filter hide /^_/ goals_only

[Bryan Gin-ge Chen]

There should be a dropdown that lets you switch between "widget mode" and "text mode".

[Bryan Gin-ge Chen]

If you click inside a proof does the infoview window look like this? https://github.com/leanprover/vscode-lean/blob/master/media/infoview-overview.png

[Miroslav Olšák]

Ha, now it is working, there was some reload required button that I had to click on.

[Miroslav Olšák]

Probably to finish all the upgrades.

[Miroslav Olšák]

So now, I can go back about how this magic work. Is it somewhere documented? I mean what is the meaning of [show_sudoku]? As far as I can see, show_sudoku is a namespace, and an alias for a tactic. Is the alias necessary? And which functions are important in the namespace?

[Mario Carneiro]

begin [custom] end is a custom tactic block, where all the tactics inside live in the custom.interactive.* namespace instead of the usual tactic.interactive.*

[Mario Carneiro]

In order to make it work you need the specific definitions custom, custom.step, custom.istep, custom.save_info like in the sudoku example. These names are hardcoded in the way custom tactic blocks are desugared

[Mario Carneiro]

so yes, the namespace is required and the alias is required (although it doesn't have to be an alias of tactic, it can be any monad, although it's usually tactic or an extension of tactic to add state or something)

[Mario Carneiro]

The copy_decls function in the sudoku example is not required, but it will import all interactive tactics from tactic into your custom tactic environment, so that things like intro and apply work in addition to your game solving tactics, which may or may not be what you want

[Miroslav Olšák]

Ah, thanks for explanation of copy_decls. What about the role of solve1? And what is the meaning of step and istep? As far as I understand, save_info produces the widget / text in the tactic state window.

[Mario Carneiro]

I believe solve1 implements the braces operation { tacs }, while step and istep are the equivalent of bind in the monad (they attach some position information to the tactics so that they can later be located by the goal view tracker), and save_info adds data to the position info which determines how goals are printed

[Mario Carneiro]

for the most part you can just delegate to the tactic functions unless you want to do something special at the end of a tactic block, after every tactic, or if you want to print the goal in a special way