https://github.com/leanprover/lean4/blob/master/tests/lean/r

Stream: computer science

[TongKe Xue]

I'm currently trying to work through https://github.com/leanprover/lean4/blob/master/tests/lean/run/doLogicTests.lean (linked from a zulip discussion on proving runtime.) -- but I'm a bit lost, not sure what is going on. I.e. I see we have a imperative Fib impl, and a functional Fib spec, but it's not obvious to me what "technique" (besides induction) is used to prove they match up.

Questions:

1. Is this std.do the so called Boole language? Or is Boole something else ? If something else, what is Boole? (The only terms more difficult to Google would be True/False).

2. Is there any documentation for this, or is: "replicate the examples in vscode/lean4, look at compiler errors along the way" the best way to learn this ?

Thanks!

[Chris Henson]

Std.Do and Boole are separate frameworks with overlapping applications. Boole is a dialect made using Strata, a library for defining languages embedded in Lean. This will in the near future be used in CSLib for verification of imperative programs.

[TongKe Xue]

Not trolling -- I'm genuinely this clueless -- is Boole publicly available ? Can I install it from a public github repo (compiling from source is fine) ? Are there sample programs (Fibonacci? MergeSort?) written in Boole with proofs ?

I've heard Boole mentioned a few time in discussions, but I can't find a install link or sample code.

Thanks!

[Chris Henson]

I think finding examples this early will be difficult, but it is possible already to use Strata as a dependency. There is a "getting started" guide there, but I have not tried this out myself.

[Chris Henson]

At this point you will probably find it easier to get started with Std.Do, maybe starting from examples posted here on Zulip.