Game Of Life

Stream: general

[Mehul]

I'm trying to define a board which has either of two states and I am not sure how to do it
This is what I have written so far:
Is there a nicer way to do so? Because the Board structure asks me to pass in a state

inductive State
| Alive
| Dead

structure Point (α : State) :=
mk :: (x : State) (y : State)

structure Board (β : Point) where
  x : [β]

and this is what I get

type expected at
  Point
term has type
  State → Type

Something I would do in haskell would be type Point = (int, int) and type Board = [Point].
My end goal is John Conway's Game Of Life!

[Johan Commelin]

So do something similar here: Point := Int \times Int and Board := list Point.

[Johan Commelin]

[x] in Lean means the list with 1 element x. Not the type of lists.

[Patrick Massot]

Is this meant to be Lean 3 code or Lean 4 code?

[Mehul]

Patrick Massot said:

Is this meant to be Lean 3 code or Lean 4 code?

I installed lean using brew and I have Lean (version 3.23.0, Release)

[Patrick Massot]

So where will also not do what you expect.

[Mehul]

Johan Commelin said:

So do something similar here: Point := Int \times Int and Board := list Point.

That doesn't quite work, maybe I have an older version?

[Patrick Massot]

Mehul, you can't simply type Haskell code and hope this will work.

[Patrick Massot]

There certainly things in Lean that are very much inspired by Haskell, but the situation is not so simple.

[Mehul]

I mean, I get don't know how to synthesize placeholder context: when I type what Johan just wrote

[Johan Commelin]

inductive State
| Alive
| Dead

def Point := ℤ × ℤ

def Board := list Point

[Johan Commelin]

This compiles, although it migh not do exactly what you want.

[Mehul]

Oh!

[Mehul]

I'll try to figure out the rest and try to go through docs again

[Mehul]

Thanks!

[Marc Huisinga]

Which docs are you using, by the way?

[Mehul]

https://leanprover.github.io/reference/
https://leanprover.github.io/lean4/doc/whatIsLean.html
I am just trying to understand how everything works, not sure if this is the best resource lol

[Patrick Massot]

So I was right to ask whether your code was meant to be Lean 3 or Lean 4. You're mixing documentation from both versions, and they are very incompatible.

[Patrick Massot]

I particular Haskell's where does exist in Lean 4.

[Marc Huisinga]

Lean 4 is very different from Lean 3 and still in development. As of now, if you want to prove things, you should stick to Lean 3. Meanwhile, Lean 4 is more suitable as a general purpose programming language.

[Patrick Massot]

Lean 4 is not yet ready so the advice is stick to Lean 3 unless you know you specifically want to try Lean 4. If you do stick to Lean 3 then the entry point is https://leanprover-community.github.io/

[Marc Huisinga]

So if you want to code game of life and try out the experimental Lean 4, you should probably make sure that you actually have a Lean 4 installation, not a Lean 3 one :) (https://leanprover.github.io/lean4/doc/setup.html)

[Mehul]

Patrick Massot said:

Lean 4 is not yet ready so the advice is stick to Lean 3 unless you know you specifically want to try Lean 4. If you do stick to Lean 3 then the entry point is https://leanprover-community.github.io/

Yeah I totally understand, but reading that Lean 4 page helped me understand a lot of stuff!

[Mehul]

Marc Huisinga said:

So if you want to code game of life and try out the experimental Lean 4, you should probably make sure that you actually have a Lean 4 installation, not a Lean 3 one :) (https://leanprover.github.io/lean4/doc/setup.html)

Gotchu!