I'm trying to learn a little #leanlang theorem proving as well as use it as a programming language for Advent of Code. I would especially like to get to where I could start to prove some simple properties about programs!
Comments
Log in with your Bluesky account to leave a comment
I had the same thought, but I'm not sure exactly what I'd try to prove. Maybe for some of the later days, proving that some brute force method is the same as some optimization?
I stole and ported this "diagonals" function for today's puzzle. It might be interesting to prove some properties about it, e.g. that the elements of `join (diagonals grid)` are the same (ignoring order) as the elements of `join grid`.
This is interesting! For today's (Day 5), I just added a little trivial proof of an alternate way to write getting the middle of an array i.e. `xs[xs.size / 2]?` is the same as a version that conditions on the length with `if h : xs.size = 0 then ...`.
Comments
I stole and ported this "diagonals" function for today's puzzle. It might be interesting to prove some properties about it, e.g. that the elements of `join (diagonals grid)` are the same (ignoring order) as the elements of `join grid`.