maze game

Stream: lean4

[David Renshaw]

To help myself learn about Lean 4's syntax manipulation facilities,
I coded up a little maze game: https://github.com/dwrensha/lean4-maze

[David Renshaw]

It think it's kind of mind-blowing that Lean lets you do stuff like this:

def maze3 := ╔════════════════════════════╗
             ║▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓║
             ║▓░░░░░░░░░░░░░░░░░░░░▓░░░@░▓║
             ║▓░▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓░▓░▓▓▓▓▓║
             ║▓░▓░░░▓░░░░▓░░░░░░░░░▓░▓░░░▓║
             ║▓░▓░▓░▓░▓▓▓▓░▓▓▓▓▓▓▓▓▓░▓░▓░▓║
             ║▓░▓░▓░▓░▓░░░░▓░░░░░░░░░░░▓░▓║
             ║▓░▓░▓░▓░▓░▓▓▓▓▓▓▓▓▓▓▓▓░▓▓▓░▓║
             ║▓░▓░▓░▓░░░▓░░░░░░░░░░▓░░░▓░▓║
             ║▓░▓░▓░▓▓▓░▓░▓▓▓▓▓▓▓▓▓▓░▓░▓░▓║
             ║▓░▓░▓░░░░░▓░░░░░░░░░░░░▓░▓░▓║
             ║▓░▓░▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓░▓║
             ║░░▓░░░░░░░░░░░░░░░░░░░░░░░░▓║
             ║▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓▓║
             ╚════════════════════════════╝

[Scott Morrison]

Can you solve the maze by dec_trivial? :-)

[David Renshaw]

I don't know what the Lean 4 equivalent of dec_trivial is.

[David Renshaw]

I'm sure there's a way to write a tactic that solves these things.

[David Renshaw]

can_escape is defined as:

def can_escape (state : GameState) : Prop :=
  ∃ (gs : List Move), is_win (List.foldl make_move state gs)

[David Renshaw]

I would be delighted to receive a pull request that adds some maze-solving automation to the repo. :)

[Johan Commelin]

It's really sad that there is no :amazed: emoji on Zulip :joy:

[Max]

a-maze-ing!

[Damiano Testa]

This is really awesome!

A minor typo in the Readme:
"You are free to move within lightdark-colored cells. The darklight-colored cells are walls.", correct?

[Gabriel Ebner]

I think this depends on your color scheme.

[Marc Huisinga]

Damiano Testa said:

This is really awesome!

A minor typo in the Readme:
"You are free to move within lightdark-colored cells. The darklight-colored cells are walls.", correct?

Depends on your background color theme, I suppose? :grinning_face_with_smiling_eyes:

[Damiano Testa]

Ahaha I tried to change my theme to a light one, without success, though! Anyway, I agree that this is a color scheme issue!