## Stream: new members

### Topic: sokoban simplification

#### Miroslav Olšák (Mar 19 2021 at 16:31):

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 (Mar 19 2021 at 16:50):

We got displaying of chess boards working.

#### Yakov Pechersky (Mar 19 2021 at 16:51):

with moves, I mean

#### Yakov Pechersky (Mar 19 2021 at 16:51):

I think dec_trivial might help you here.

#### Miroslav Olšák (Mar 19 2021 at 17:35):

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

#### Miroslav Olšák (Mar 19 2021 at 17:38):

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 (Mar 19 2021 at 17:43):

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 (Mar 19 2021 at 18:31):

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 (Mar 19 2021 at 18:57):

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 (Mar 19 2021 at 18:59):

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 (Mar 19 2021 at 21:16):

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

#### Miroslav Olšák (Mar 19 2021 at 21:59):

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 (Mar 19 2021 at 22:14):

You wrote the normalizer, nice =)

#### Miroslav Olšák (Mar 19 2021 at 22:47):

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 (Mar 19 2021 at 22:48):

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

#### Mario Carneiro (Mar 19 2021 at 22:55):

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

#### Mario Carneiro (Mar 19 2021 at 22:56):

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

#### Mario Carneiro (Mar 19 2021 at 23:19):

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

#### Mario Carneiro (Mar 19 2021 at 23:22):

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

#### Mario Carneiro (Mar 19 2021 at 23:23):

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

#### Mario Carneiro (Mar 19 2021 at 23:23):

I have version 0.16.25 of the vscode-lean extension

#### Miroslav Olšák (Mar 19 2021 at 23:25):

I have 0.15.8, maybe, I should upgrade.

#### Mario Carneiro (Mar 19 2021 at 23:25):

vscode makes it a one-click fix

#### Miroslav Olšák (Mar 19 2021 at 23:26):

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

#### Miroslav Olšák (Mar 19 2021 at 23:28):

Maybe, I have to upgrade the VScode itself.

#### Mario Carneiro (Mar 19 2021 at 23:30):

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

#### Mario Carneiro (Mar 19 2021 at 23:30):

it probably says "update available" or something like that

#### Miroslav Olšák (Mar 19 2021 at 23:33):

However, it is still not working.

#### Miroslav Olšák (Mar 19 2021 at 23:34):

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

#### Bryan Gin-ge Chen (Mar 19 2021 at 23:34):

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

#### Bryan Gin-ge Chen (Mar 19 2021 at 23:35):

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 (Mar 19 2021 at 23:35):

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

#### Miroslav Olšák (Mar 19 2021 at 23:35):

Probably to finish all the upgrades.

#### Miroslav Olšák (Mar 19 2021 at 23:50):

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 (Mar 20 2021 at 00:07):

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 (Mar 20 2021 at 00:09):

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 (Mar 20 2021 at 00:10):

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 (Mar 20 2021 at 00:16):

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 (Mar 20 2021 at 00:21):

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 (Mar 20 2021 at 00:43):

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 (Mar 20 2021 at 00:44):

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

Last updated: May 08 2021 at 18:17 UTC