lean4-maze

KO | EN

gitlite — search

#python #javascript #react #typescript #reactjs #html #css #docker #linux #rust #android #java

★ 72 Open GitHub ↗

maze game encoded in Lean 4 syntax

// repository documentation

Was this content helpful?

★ 0 (0 ratings)

# lean4-maze

This repo shows how maze solving
can be encoded as theorem proving
using the Lean 4 programming language.

It draws inspiration from https://github.com/kbuzzard/maze-game.

## Setup

### On The Web

[Try it in your browser on the Lean 4 Playground.](https://live.lean-lang.org/#url=https%3A%2F%2Fraw.githubusercontent.com%2Fdwrensha%2Flean4-maze%2Fmain%2FMaze.lean)

### Locally

First, install Lean 4 on your computer: https://leanprover.github.io/lean4/doc/setup.html

Then open `Maze.lean` in emacs or VSCode.

## Playing

You can define a maze like this:

```lean
def maze := ┌────────┐
            │▓▓▓▓▓▓▓▓│
            │▓░▓@▓░▓▓│
            │▓░▓░░░▓▓│
            │▓░░▓░▓▓▓│
            │▓▓░▓░▓░░│
            │▓░░░░▓░▓│
            │▓░▓▓▓▓░▓│
            │▓░░░░░░▓│
            │▓▓▓▓▓▓▓▓│
            └────────┘
```

The `@` symbol denotes your current location.
You are free to move within the `░` cells.
The `▓` cells are walls.

Your goal is to escape the maze at any of its borders.

You can interactively solve a maze like this:

```lean
example : Escapable maze :=
 by south
    east
    south
    south
```

As you make progress, Lean's goal view will display your current state.
For example, after the moves made above, the state is shown as:

```lean
⊢ Escapable
    (
        ┌────────┐
        │▓▓▓▓▓▓▓▓│
        │▓░▓░▓░▓▓│
        │▓░▓░░░▓▓│
        │▓░░▓░▓▓▓│
        │▓▓░▓@▓░░│
        │▓░░░░▓░▓│
        │▓░▓▓▓▓░▓│
        │▓░░░░░░▓│
        │▓▓▓▓▓▓▓▓│
        └────────┘
        )
```

The main moves available to you at any point are `north`, `south`, `east`, and `west`.

When you reach the boundary, you can finish your proof with `out`.

## how does it work?

As you traverse a maze, you are constructing a proof
that the maze satisfies an `Escapable` predicate, defined as

```lean
inductive Escapable : GameState → Prop where
| Done (s : GameState) : IsWin s → Escapable s
| Step (s : GameState) (m : Move) : Escapable (make_move s m) → Escapable s
```

The mazes as drawn above are actual valid Lean 4 syntax!

We define new syntax categories and some `macro_rules` for elaborating
them into valid values.

To get Lean to render the values back in the above format,
we define a delaboration function and register it with the pretty printer.

Lean 4 lets us do all of this in-line, in ordinary Lean 4 code.

lean4-maze

Explore Similar Repositories

Was this content helpful?

Recent Feedback

Download README