Add Lean bf

[philnguyen]

Add bf benchmark in Lean. Compared to other languages, these are unique features in the Lean program:

• The source program appears to "functionally update" an array, which sounds inefficient. But at run time, Lean destructively updates the array, because it is used linearly. This makes it comparable to using an ArrayList in Java.
• The standard test case is checked at compile time. If the program breaks the test, it won't build.
• The Tape requires that pos is statically proven to be in bound. This program is relatively simple, so the proofs are taken care of by Lean's built-in tactics (by simp, by omega, by grind).

There are instructions for installing Lean either for a standard desktop use, or for a more minimal command-line environment.

After making sure that lake is in path:

cd brainfuck/lean
lake build
lake exe bf path/to/bench.b