C.C. Lemma is a tool for automating equational proofs. It is implemented as a command-line tool that takes as input a file specifying inductive datatype definitions, function definitions, and equalities over these datatypes and functions. It attempts to prove each equality, optionally outputting a proof in Liquid Haskell*.

We include with our tool all of the datasets necessary to run the evaluation from our paper as well as scripts and instructions on how to reproduce our results. We also include two of the three tools we evaluate against, which the scripts will also run.

Our code can be found at https://github.com/cole-k/cc-lemma.

C.C. Lemma is implemented in Rust. At this time we do not expect there to be any special requirements for machines: modern laptops are sufficient, although even older machines ought to work fine. Some benchmarks, especially many in the optimization dataset, will run to timeout. We estimate running all benchmarks to take around 120 minutes in the worst-case; however, by default we set a much lower timeout so that testing the tool will only take a few minutes.

*Proof emission is experimental and not guaranteed to generate proofs that Liquid Haskell accepts, although reviewers may find it useful to inspect the proofs to see how C.C. Lemma proved an equality.