🚧 Here be dragons: research code ahead! 🚧

Today is April 07, 2024. The state of this repo is presently chaotic. The last commit was a91eb7b on Feburary 28, 2024. Especially during Feburary we made changes with little regard for the cleanliness or organization of code or repository. You may discover -- for example -- that there are feature flags which do nothing, code that is completely dead, or that this repository's name does not match the name we use in places that are not this repository. Please accept my apologies.

Instead of cleaning up this repository, our plan is to do a rewrite of the messiest parts in a fresh repository. If you see this message and the rewrite is not clearly linked here, I advise that you look for it first before continuing!

Best of luck, Cole

cyclegg is a fast theorem prover for equational reasoning powered by e-graphs. It has two main contributions.

1. Efficient, exhaustive search of induction hypothesis and lemma applications.

2. Lemma discovery based on subterms which appear in the goal.

cyclegg is fast: both of these examples run in under 50ms.

A sketch of its general algorithm can be found here.

To run cyclegg on the IsaPlanner benchmarks, run the below command.

$ cargo run -r -- examples/isaplanner.ceg --timeout 5

Run with --help to see an overview of the different command-line flags.

$ cargo run -- --help

As of 2a6aa34, when run with a timeout of 5s.

• IsaPlanner benchmarks: 78/86
• CLAM benchmarks: 30/50

cyclegg was originally based on CycleQ and its idea was to improve cyclic proof search using an e-graph (specifically, the egg e-graph library). We have since focused on the improvements e-graphs give to proof search as opposed to e-graphs plus cyclic proofs. So the "cycl-" part of the name is now a misnomer. We'll probably change the name soon.

• Create goals inside parser, do not expose RawGoal
• Decouple proof generation from proof search (e.g. put Defs, Proof term somewhere else)
• Make partial applications without $ work
• Move from SymbolLang to a proper language.
  • See babble for inspiration (https://github.com/dcao/babble/blob/main/src/ast_node.rs)
• Emit a proof data structure
  • Right now we just emit strings that are (mostly) valid LiquidHaskell.
  • Creating a proper equational proof data structure would allow us to emit to other backends.
  • It would also be cleaner.

• In cyclic mode: use multi-patterns instead of requiring that the premise has no extra vars?

• Conditional props proof generation
  • Add explanation for conditional unions (cannot just union_trusted).
  • Include the premise into the LH precondition
    • This can be accomplished by taking a witness of the precondition as an argument.
  • How to include the proof of the condition holding?

    • To use a conditional lemma you need a witness of the condition. We can take the e-graph from which we are getting the explanation and ask it to explain why the e-classes of the condition are equal and use those to build a proof. In LH this would look something like

      let conditionWitness =   condLHS 
                           ==. condLHS'
                           ? lemma lemmaArgs
                           ==. condRHS
                           *** QED
       in conditionalLemma conditionWitness args