Automation for Directed Rewrite Based Proof Search

Stream: Program verification

[Jesse Slater]

I have a deeply embedded DSL and a set of directed rewrite rules. The rewrites are directed because the semantics are nondeterministic and some rewrites are refinements which reduce non-determinism irreversibly.

Using sequences of rewrites, I can prove complex program equivalences, but the proofs become long and unwieldy quickly. I have monotonicity lemmas for each operation, so to apply a rewrite deep in an AST, I apply a sequence of monotonicity lemmas to get the spot I want to rewrite at the root and then apply the rule. This makes proofs long, and the process feels readily automatable.

Are there automation tools for Lean which would be appropriate for this task?

[Aaron Liu]

there's grw

[Malvin Gattinger]

Maybe the egg tactic by @Andrés Goens and @Marcus Rossel could help in your use case. (I've not actually used it myself much.) https://github.com/marcusrossel/lean-egg

[Marcus Rossel]

egg can only do =/↔, so this probably won't help