Advent of code in Lean

Stream: new members

[Frank Dai]

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]

@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]

Thanks for the information, I got it!

[Elvorfirilmathredia]

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]

Isn't this sorry a new test for omega?

[Elvorfirilmathredia]

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

[Mario Carneiro]

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]

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]

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]

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

[Patrick Massot]

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]

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

[Patrick Massot]

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]

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]

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

[Rob Lewis]

norm_num is more appropriate than linarith in the first have.

[Ocschwar]

Hello, all. I'm insane in doing this, but I'm hoping to try advent of code in Lean this year.

[Alex J. Best]

@Reid Barton tried this in lean 4 last year iirc. I think he called the project advent of lean 4. Maybe you can find some useful stuff there

[Reid Barton]

https://github.com/rwbarton/advent-of-lean-4

[Tim Hunter]

Hello all, I am completely new to Lean and I am planning to use advent of code as an opportunity to learn about it. Looking forward to trying it out! By the way, is it preferable to start new topics for asking questions, or to simply continue this thread?

[Johan Commelin]

topics are cheap. feel free to start new ones.

[Johan Commelin]

It keeps the discussion organized