adaptations for lean#2793

Stream: nightly-testing

[Kim Morrison]

We're reviving the long dormant lean#2793. This will have the effect (by design) that auto_params will not be used when rewriting by lemmas. This does not have much effect on mathlib outside of the Matroid development, which seems to use it heavily.

@Peter Nelson, as I think you're the primary author of the Matroid material, could I ask you to take a look at this and see if you can come up with a redesign that relies on auto_param in rewrite lemmas less?

For now I've just inserted by aesop_mat as an argument to all the rewrite lemmas that are failing. Please have a look at branch#lean-pr-testing-2793 to see how it looks.

[Kim Morrison]

(While on the subject, these Matroid files do seem to have a lot of ; where a newline would do just fine. :-)

[Kim Morrison]

Ah, false alarm, actually. Still rw [my_lemma ..] results in the auto-param firing, so I'll just switch to this and I think we can be happy.

[Yaël Dillies]

Ah great. I was scared that change was killing in the egg the idea of @David Loeffler and I to use auto-params for measurability and integrability conditions

[Peter Nelson]

Kim Morrison said:

Ah, false alarm, actually. Still rw [my_lemma ..] results in the auto-param firing, so I'll just switch to this and I think we can be happy.

I’m actually strictly happier now! It will be convenient to have the option of telling the autoparam whether to fire or not when rewriting.

Is there a way to do this with autoparams more generally?

[Peter Nelson]

Kim Morrison said:

(While on the subject, these Matroid files do seem to have a lot of ; where a newline would do just fine. :-)

This is one of these points where I’d like to see a more prominent and detailed style guide for mathlib. I’m very happy to change my style, but I often feel like my impression of what is preferred comes from an ad hoc combination of zulip comments and PR reviews, and they aren’t always internally consistent.

[Peter Nelson]

(Looking at the style guide again, I see that it’s probably clear enough on this particular point)

[Eric Wieser]

Should this be merged with the other thread?

[Bhavik Mehta]

I don't think so - I suspect Kim made two separate threads on purpose, this one for the way the change affects auto-params, and the other one for the way the change affects implicit arguments. They are similar in nature, but I think the focus is sufficiently different to warrant separate threads.