lean4#1743

Stream: lean4

[Scott Morrison]

@Mario Carneiro, could I ask your advice on how I might achieve what I was asking about in lean4#1743, without needing changes to Lean 4?

I have a collection of simp lemmas, each with side-conditions, and I would like to simplify by them, only applying each lemma if its side condition can be discharged (e.g. by decide), and I would like to proceed even if the Expr.acLt term order would usually reject the rewrite.

So far I am only thinking of dreadful hacks. (e.g. tweak the lemmas by adding superfluous extra parameters so that simp doesn't classify them as perm lemmas).

As reasonable answer is, of course: "Please don't try this, it sounds like a bad idea."

[Mario Carneiro]

I would just take that part into my own hands, by adding a pre := tactic which rewrites with your lemma to the Simp.Methods

[Gabriel Ebner]

Is this actually used in mathlib, or do we want this for exciting new stuff?

[Scott Morrison]

As I said briefly during the meeting, the idea is to try implementing something like abel in two phases:

• a tactic that abstract atoms, e.g. replacing a + 2 • b - a + b with let L := [a, b]; let f i := L.get! i; f 0 + 2 • f 1 - f 0 + f 1
• then do all the proofs with the simplifier, using side conditions on indices appearing in f i to get the term order correct.

[Scott Morrison]

So @Gabriel Ebner, this is for "exciting new stuff" (or rather, an alternative implementation of a tactic that needs porting).

When I look at tactics like abel (or ring for that matter), it makes me wish that we were doing less manual proof construction, and more letting tools like simp handle it for us.

This approach would only require constructing a proof for the "abstract atoms" step.

[Mario Carneiro]

I would rather have those tactics be as efficient as possible. They are used a lot, including as components of other tactics, so they should try not to do unnecessary things

[Scott Morrison]

Okay, so it seems like the possibilities would be:

• Be able to disable the term order checking in Simp (probably not acceptable for Lean 4)
• Be able to pass a custom term order into Simp (probably not acceptable)
• Manage Simp more manually, by doing the rewriting myself in pre := with a custom tactic.
• Obfuscate the lemmas so that simp doesn't treat them as perm lemmas.

[Scott Morrison]

Is it clearly less efficient to do it this way, though?

[Mario Carneiro]

the additional let bindings and list construction is clearly unnecessary

[Scott Morrison]

Okay, true.

[Mario Carneiro]

also simp likes to unfold those

[Scott Morrison]

but it seems like the abstraction step is pretty cheap, hopefully just linear in the expression, and so insignificant compared to the term reordering proof.

[Mario Carneiro]

I'm not even sure why you need to use indices here, why doesn't the regular term order work?

[Scott Morrison]

I guess I haven't tried explicitly, but as you pointed out in the meeting the signs are probably trouble.

[Mario Carneiro]

I would go for an encoding more like have x := a; have y := b; x + 2 • y - x + y here

[Scott Morrison]

Really what I had in mind was f 37 2, which means "37 times the 2nd atom"

[Scott Morrison]

so you can absorb any signs into an argument to f, where it can't interfere with the term order.

[Mario Carneiro]

well the + and - here can be a tactic-specific operator, I think abel uses some kind of additive version of horner IIRC

[Mario Carneiro]

but every time I think about the most optimal way to combine all these pluses and minuses I end up with a pretty specific solution that uses custom data structures like insertion into a RBMap ExprId Int with proofs