MagmaEgg egg-based Rust prover

Stream: Equational

[lyphyser]

I wrote an egg-based Rust prover and submitted it at https://github.com/teorth/equational_theories/pull/216

It seems to have proven 5574 of the 24283 implications in the "only_strongest.txt" file (of which around 3000 with reasonable length proofs), though right now I can't tell whether it is significant or not since I have mostly focused on getting the code to work.

[lyphyser]

After reverting Vampire, these are the changes from adding the small theorems.

Vampire reverted:
{"explicit_proof_true": 27803,
"implicit_proof_true": 5294943,
"unknown": 2886650,
"implicit_proof_false": 12994633,
"explicit_proof_false": 829607
}

With MagmaEgg small:
{"explicit_proof_true": 30981,
"implicit_proof_true": 7042768,
"unknown": 1135647,
"implicit_proof_false": 12994633,
"explicit_proof_false": 829607
}

[Andrés Goens]

cool! I'm curious, what does this do exactly? asking to understand the difference between this and the egg tactic that uses the same underlying library

[Marcus Rossel]

Aside from using a custom language for magmas, one difference (which we could actually address in lean-egg) is that it already does the better version of explosion:

"Currently search just uses the egg library in a basic fashion, except that in case there are extra variables not present in the LHS, it has code to instantiate them with all subexpressions of the original goal."

For this they use an approach I'd hoped would be feasible for lean-egg in the past, but doesn't work when you have terms of different (possibly dependent) types. Namely, by using a custom applier (PartiallyBoundApplier) they instantiate the missing pattern variables at runtime, instead of generating additional rewrite rules. The possible values for instantiation are simply all e-classes present in the e-graph before eqsat starts (cf. add_rules and its call site) - which yields all subexpressions of the lhs and rhs (very cool idea).

[Marcus Rossel]

@lyphyser If it's at any point desirable, I could try tearing out parts of lean-egg and hook up your backend to it. Then one could simply use your approach as a tactic from Lean.

[Marcus Rossel]

@Andrés Goens I guess this is a very nice and small example to work towards, if we ever decide to build a more general egg API for Lean.

[Vlad Tsyrklevich]

@lyphyser JFYI I noticed that the dashboard numbers hadn't updated after your PR and realized it was because MagmaEgg wasn't included in Generated.lean. PR for it here https://github.com/teorth/equational_theories/pull/272

[Vlad Tsyrklevich]

94.891% :partying_face:

[David Renshaw]

getting close to the "only a million left" milestone!