Consider a simple inductive data structure of binary trees, and a type of pairs of integers:
structure Edge : Type := edge:: fst : Nat snd : Nat inductive SimpleTree (α : Type) : Type | empty : SimpleTree α | leaf : α → SimpleTree α | node : α → SimpleTree α → SimpleTree α → SimpleTree α
I would like to build trees of edges with a couple of thousand nodes. A small example would look like this:
example : SimpleTree Edge := .node (.edge 5 0) .empty (.leaf (.edge 3 1))
I placed a larger example with around 1200 nodes in
example.lean at this gist repository.
You will find there comparable Coq, Agda, and OCaml implementations, as well as the variants shown below. Processing these files on my laptop (see
time.sh in the gist) gives the following timings:
ocamlc -c example.ml 0.07s user 0.01s system 95% cpu 0.087 total lean example.lean 5.16s user 0.05s system 99% cpu 5.229 total agda example.agda 3.63s user 0.22s system 100% cpu 3.847 total coqc example.v 2.55s user 0.19s system 99% cpu 2.737 total
Lean is the slowest, contrary to its fame. I experimented with
@[inline] but that doesn't seem to help with a one-time compilation. Am I doing something wrong?
Things get worse if we use dependent types. Suppose we define edges so that the first component is known to be in
Fin n, and the second must be smaller than the first:
structure Edge (n : Nat) : Type := edge:: fst : Fin n snd : Fin fst -- smart constructor for edges macro "E[" i:term "," j:term "]" : term => `(.edge $i (Fin.mk $j (by trivial)))
A small example would now look like this:
def test1 : Tree (Edge 100) := .node E[5,0] .empty (.leaf E[3,1])
When we run the same tree, but with the dependent type of edges, we get these timings:
lean exampleDependentNoTactic.lean 18.75s user 0.10s system 99% cpu 18.886 total lean exampleDependentTactic.lean 15.07s user 0.38s system 99% cpu 15.471 total agda exampleDependent.agda 5.39s user 0.24s system 100% cpu 5.625 total coqc exampleDependent.v 7.74s user 0.25s system 99% cpu 7.998 total
Once again, Lean is quite a bit slower than Agda and Coq.
(In above benchmarks there are two versions of Lean, one uses the
trivial tactic to constructs proof terms, while the other one avoids doing so by boolean reflection, see exampleDependentNoTactic.lean.)
Eventually I would like to process thousands of such trees, as well as other similar data structures. I would appreciate advice on how to speed things up in Lean. If you have advice on how to speed up Agda and Coq, it's welcome, too.
myInit : IO (SimpleTree Edge)and then declare
@[init myInit] def myTree : SimpleTree Edge := dummyValue. The initializer can even be
unsafeif you wish. $\endgroup$