successor to rsimp?

Stream: lean4

[Jonathan Protzenko]

@Son Ho and I were reading the 2017 ICFP paper ("A Metaprogramming Framework for Formal Verification") and it mentions rsimp, which (insofar as we understand) would be quite helpful for the kinds of proofs we're trying to do with the Aeneas/Lean backend. Now rsimp is probably an artifact from Lean 3, and we're wondering what would be a modern equivalent in Lean4.

It might be helpful to have a bit more context. When trying to prove properties about programs (and here I'm perhaps biased because of my experience verifying crypto code), there are oftentimes supremely boring lemmas and administrative things that we want to make progress on, automatically. Example: a > 0 /\ b > 0 => a *b > 0 is always a good idea to apply, before "getting to work". Or, List.length (l1 ++ l2) = List.length l1 + List.length l2, etc. In SMT-based proof, we typically rely on the SMT solver to saturate the context with those mundane facts, except it doesn't scale up, especially in the presence of non-linear arithmetic. But it would be helpful (in our opinion) to have a similar facility that can eagerly apply a set of known useful lemmas in the context of interactive proof, in Lean4.

Now I realize that what I'm describing is very similar to auto (in other theorem provers), crush, or perhaps Aesop, in Lean. Except Aesop (correct me if I'm wrong) aims to find a proof, and fails otherwise, whereas here, we are trying to get a bunch of repetitive work out of the way before we roll up our sleeves and focus on the core of the proof which requires careful explaining to the proof assistant.

What would be the idiomatic, "classic" way of implementing that approach in Lean4? Is there a successor to rsimp? An equivalent to crush? A mode of Aesop that can be used to make progress on, but not necessarily clear the proof obligation? Any thoughts welcome. Thanks!

[Jannis Limperg]

By default, Aesop, when it can't solve a goal, returns the goals obtained by exhaustively applying rules tagged as 'safe'. Sounds like this should do what you want. Aesop usually prints a warning in this situation, but you can suppress this with aesop (options := { warnOnNonterminal := false }).

[Mario Carneiro]

When I started working on lean in 2016-2017, rsimp was already of unclear usability and there were no good examples of its use. This has obviously not changed since mathlib was founded and developed, so we are left with nothing to work with. I would expect that any rsimp successor needs to be redesigned from scratch, as IIRC the original one was tied in to the SMT framework (that was buggy / unmaintained and not ported to lean 4)

[Mario Carneiro]

(this is meant as historical context for those who don't know about rsimp)

[Mario Carneiro]

I would guess that aesop is the best way to do this in lean 4. It hits on some tensions regarding non-terminal use, which I'm not sure are solvable if you are tagging an open ended collection of lemmas as intro rules or forward reasoning steps

[Jonathan Protzenko]

ok, thanks @Jannis Limperg for the customization option for aesop... we'll start with that and see how far that gets us, then we'll report back!

[Jonathan Protzenko]

@Mario Carneiro thanks for the historical context. Out of curiosity, is there any summary or debrief on what happened with the SMT framework and why it ended up not being ported to Lean4?

[Mario Carneiro]

Like I said, it was unmaintained for a long time, it accrued bugs and we just started avoiding it

[Jonathan Protzenko]

I guess this means that the need for it was never big enough, otherwise surely some maintainers would've kept it alive... interesting

[Mario Carneiro]

It's a very technical bit of infrastructure, I'm not sure it could be maintained by anyone except Leo, and he was not involved in lean 3 for most of the history of mathlib

[Henrik Böving]

There is some work on getting CVC5 into Lean right now.

[Mario Carneiro]

I think there is a fair amount of expressed desire, but no one knowledgeable enough to write something with all the bells and whistles of a SMT solver and get it into mathlib

[Mario Carneiro]

Something that interfaces with an external solver is in some ways simpler, although there is a significant impedance mismatch between SMT-LIB and DTT

[Mario Carneiro]

but the original smt_tactic framework was written by someone who was involved in Z3 for a long time, and we don't have anyone else with that kind of experience AFAIK

[Mario Carneiro]

once upon a time lean was going to be a more configurable kind of ATP and the vision changed pretty drastically over time to the ITP it is today

[Mario Carneiro]

Jonathan Protzenko said:

I guess this means that the need for it was never big enough, otherwise surely some maintainers would've kept it alive... interesting

It's certainly not something you can't work around, I mean what you are talking about boils down to calling intro and apply with appropriately chosen lemmas

[Jonathan Protzenko]

oh definitely -- I'm just interesting in what is seen as a desirable/popular style of going about proofs

[Mario Carneiro]

it's annoying for sure but it takes off a lot of the pressure to do something better, especially when it's up against a project the size of a masters thesis (+ continuing maintenance)

[Mario Carneiro]

luckily @Jannis Limperg has graciously donated his PhD to solving this problem, and aesop is in mathlib so the continuing maintenance part is also handled