Zulip Chat Archive

Stream: new members

Topic: sokoban simplification


view this post on Zulip 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.

view this post on Zulip Yakov Pechersky (Mar 19 2021 at 16:50):

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

view this post on Zulip Yakov Pechersky (Mar 19 2021 at 16:50):

We got displaying of chess boards working.

view this post on Zulip Yakov Pechersky (Mar 19 2021 at 16:51):

with moves, I mean

view this post on Zulip Yakov Pechersky (Mar 19 2021 at 16:51):

I think dec_trivial might help you here.

view this post on Zulip Yakov Pechersky (Mar 19 2021 at 16:52):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Miroslav Olšák (Mar 19 2021 at 21:16):

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

view this post on Zulip 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.

view this post on Zulip Yakov Pechersky (Mar 19 2021 at 22:14):

You wrote the normalizer, nice =)

view this post on Zulip 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?

view this post on Zulip Miroslav Olšák (Mar 19 2021 at 22:48):

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

view this post on Zulip Mario Carneiro (Mar 19 2021 at 22:55):

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

view this post on Zulip 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

view this post on Zulip Miroslav Olšák (Mar 19 2021 at 23:07):

ss_sudoku.png ss_rubik.png

view this post on Zulip Mario Carneiro (Mar 19 2021 at 23:19):

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

view this post on Zulip Mario Carneiro (Mar 19 2021 at 23:22):

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

view this post on Zulip Mario Carneiro (Mar 19 2021 at 23:23):

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

view this post on Zulip Mario Carneiro (Mar 19 2021 at 23:23):

I have version 0.16.25 of the vscode-lean extension

view this post on Zulip Miroslav Olšák (Mar 19 2021 at 23:25):

I have 0.15.8, maybe, I should upgrade.

view this post on Zulip Mario Carneiro (Mar 19 2021 at 23:25):

vscode makes it a one-click fix

view this post on Zulip Miroslav Olšák (Mar 19 2021 at 23:26):

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

view this post on Zulip Miroslav Olšák (Mar 19 2021 at 23:28):

Maybe, I have to upgrade the VScode itself.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Mar 19 2021 at 23:30):

it probably says "update available" or something like that

view this post on Zulip Miroslav Olšák (Mar 19 2021 at 23:32):

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

view this post on Zulip Miroslav Olšák (Mar 19 2021 at 23:33):

However, it is still not working.

view this post on Zulip 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

view this post on Zulip 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".

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Miroslav Olšák (Mar 19 2021 at 23:35):

Probably to finish all the upgrades.

view this post on Zulip 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?

view this post on Zulip 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.*

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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