# Zulip Chat Archive

## Stream: new members

### Topic: Advent of code in Lean

#### 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?

#### 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.

#### Frank Dai (Dec 01 2019 at 23:33):

Thanks for the information, I got it!

#### 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

#### Patrick Massot (Dec 02 2019 at 21:21):

Isn't this sorry a new test for `omega`

?

#### 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 ~~ I think I can take it from there`fuel m = m/3 - 2`

:sweat: I just recently finished the natural number game ...

#### 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`

#### 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:

#### 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.

#### Patrick Massot (Dec 02 2019 at 22:36):

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

#### 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).

#### 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

#### 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...

#### 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.

#### 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.

#### 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