Zulip Chat Archive

Stream: general

Topic: Game Of Life


view this post on Zulip Mehul (Feb 01 2021 at 15:03):

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!

view this post on Zulip Johan Commelin (Feb 01 2021 at 15:07):

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

view this post on Zulip Johan Commelin (Feb 01 2021 at 15:08):

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

view this post on Zulip Patrick Massot (Feb 01 2021 at 15:09):

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

view this post on Zulip Mehul (Feb 01 2021 at 15:10):

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)

view this post on Zulip Patrick Massot (Feb 01 2021 at 15:11):

So where will also not do what you expect.

view this post on Zulip Mehul (Feb 01 2021 at 15:11):

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?

view this post on Zulip Patrick Massot (Feb 01 2021 at 15:11):

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

view this post on Zulip Patrick Massot (Feb 01 2021 at 15:12):

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

view this post on Zulip Mehul (Feb 01 2021 at 15:13):

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

view this post on Zulip Johan Commelin (Feb 01 2021 at 15:13):

inductive State
| Alive
| Dead

def Point :=  × 

def Board := list Point

view this post on Zulip Johan Commelin (Feb 01 2021 at 15:13):

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

view this post on Zulip Mehul (Feb 01 2021 at 15:13):

Oh!

view this post on Zulip Mehul (Feb 01 2021 at 15:14):

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

view this post on Zulip Mehul (Feb 01 2021 at 15:14):

Thanks!

view this post on Zulip Marc Huisinga (Feb 01 2021 at 15:14):

Which docs are you using, by the way?

view this post on Zulip Mehul (Feb 01 2021 at 15:41):

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

view this post on Zulip Patrick Massot (Feb 01 2021 at 15:42):

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.

view this post on Zulip Patrick Massot (Feb 01 2021 at 15:42):

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

view this post on Zulip Marc Huisinga (Feb 01 2021 at 15:43):

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.

view this post on Zulip Patrick Massot (Feb 01 2021 at 15:43):

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/

view this post on Zulip Marc Huisinga (Feb 01 2021 at 15:45):

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)

view this post on Zulip Mehul (Feb 01 2021 at 16:11):

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!

view this post on Zulip Mehul (Feb 01 2021 at 16:12):

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!


Last updated: May 17 2021 at 22:15 UTC