Zulip Chat Archive

Stream: new members

Topic: Advent of code in Lean


view this post on Zulip Frank Dai (Dec 01 2019 at 23:18):

Hello Lean Zulip chat,

I am trying to do the advent of code (https://adventofcode.com/) in Lean. I've gotten the code for part 1 written, I'm just trying to figure out how to do IO. There seems to be some functions for doing file IO (https://github.com/leanprover/lean/blob/master/library/system/io.lean), but then I realized I have no idea how to parse a char_buffer into a \N. Is there some sort of standard library function for parsing numbers, or will I need to roll my own?

view this post on Zulip Bryan Gin-ge Chen (Dec 01 2019 at 23:28):

@Mario Carneiro did a few of last year's problems in Lean (repo here). It looks like he used core Lean's data.buffer.parser functions in his code here.

view this post on Zulip Frank Dai (Dec 01 2019 at 23:33):

Thanks for the information, I got it!

view this post on Zulip Elvorfirilmathredia (Dec 02 2019 at 21:06):

This is what I have for the first day. It's not pretty and there is one 'sorry' ... so suggestions on how to improve this are quite welcome :slight_smile:

import system.io
import data.list.basic

open list io nat

def append_line : io (list string)    io (list string) :=
  λ ml i, do l <- ml,
             x <- get_line,
             return (append l [x])

def fuel (m : ) := m / 3 - 2

lemma fuel_wf (m : ) (h : m > 0) : fuel m < m := sorry

def additional_fuel :   
  | m :=
    if h : m > 0 then
      have fuel m < m,
        from fuel_wf m h,
        fuel m + additional_fuel (fuel m)
    else
      0

def total_fuel (m : ):= let fm := fuel m in fm + additional_fuel fm

#eval do lines <- (foldl append_line) (return []) (range 100),
         fuel <- return $ sum $ map (total_fuel  string.to_nat) lines,
         put_str_ln  to_string $ fuel

view this post on Zulip Patrick Massot (Dec 02 2019 at 21:21):

Isn't this sorry a new test for omega?

view this post on Zulip Elvorfirilmathredia (Dec 02 2019 at 22:11):

Isn't this sorry a new test for omega?

Hm, I can indeed solve m < 3 * (m+2) with omega, which leaves me with

lemma fuel_wf (m : ) (h : m > 0) : fuel m < m :=
begin
  suffices : m < 3 * (m + 2),
    sorry,

  omega
end

Sadly I don't even know how to use the definitional equality fuel m = m/3 - 2 :sweat: I just recently finished the natural number game ... I think I can take it from there

view this post on Zulip Mario Carneiro (Dec 02 2019 at 22:16):

If you are doing advent of code, you don't need to worry about termination, so you can mark additional_fuel as meta and delete the have

view this post on Zulip Elvorfirilmathredia (Dec 02 2019 at 22:18):

If you are doing advent of code, you don't need to worry about termination, so you can mark additional_fuel as meta and delete the have

I know, but where's the fun in that? :stuck_out_tongue_wink:

view this post on Zulip Patrick Massot (Dec 02 2019 at 22:35):

Sadly m < 3 * (m + 2) is much easier to prove than your goal (and linarith probably does it as well). What you found is the worst part of Lean: nat subtraction hell.

view this post on Zulip Patrick Massot (Dec 02 2019 at 22:36):

Unfortunately we still don't have a tactic handling that.

view this post on Zulip Patrick Massot (Dec 02 2019 at 22:41):

Actually it may start even before that. Are you sure you actually understand what is m/3 in your code? (hint: it's a natural number, not a rational number).

view this post on Zulip Bryan Gin-ge Chen (Dec 02 2019 at 22:43):

This is a rare instance where getting a nat from division is actually desired: https://adventofcode.com/2019/day/1

view this post on Zulip Patrick Massot (Dec 02 2019 at 22:49):

import data.nat.basic

def fuel (m : ) := m / 3 - 2

lemma fuel_wf (m : ) (h : 9  m) : fuel m < m :=
begin
  have : 3  m/3, by { rw nat.le_div_iff_mul_le ; linarith },
  erw nat.sub_lt_left_iff_lt_add,
  conv_rhs { rw  nat.mod_add_div m 3 },
  all_goals { linarith  },
end

I really don't know why I did this, probably fear of not finding sleep if I go to bed...

view this post on Zulip Elvorfirilmathredia (Dec 05 2019 at 12:02):

Nice, thanks a lot! I tried to do it myself and ended up with the following:

lemma fuel_wf (m : ) (h : m > 0) : fuel m < m :=
begin
  have : m/3 < m, by {apply div_lt_self h _; linarith },
  have : m/3 - 2  m/3, by {exact nat.sub_le_self (m/3) 2},
  rw fuel,
  linarith,
end

Somehow I had a hard time finding sub_le_self ... I also had to prefix it with nat. because otherwise lean tried to use the one for ordered commutative groups, which obviously does not work for nat.

view this post on Zulip Rob Lewis (Dec 05 2019 at 12:06):

It's a bug that m/3 - 2 ≤ m/3 isn't by omega. Hopefully we get this fixed soon.

view this post on Zulip Rob Lewis (Dec 05 2019 at 12:06):

norm_num is more appropriate than linarith in the first have.


Last updated: May 18 2021 at 17:44 UTC