Domain specific Tactics

Stream: general

[Suryansh Shrivastava]

Are there any domain specific tactics in mathlib? Like there are some very ubiquitous tricks that we use all the time in specific domains of mathematics, and thus making it into a tactic might seem a good idea

[Notification Bot]

This topic was moved here from #Machine Learning for Theorem Proving > Domain specific Tactics by Heather Macbeth.

[Heather Macbeth]

@Suryansh Shrivastava Sure, do you mean like docs#tactic.interactive.measurability ?

[Eric Wieser]

tactic#filter_upwards comes to mind too

[Suryansh Shrivastava]

Heather Macbeth said:

Suryansh Shrivastava Sure, do you mean like docs#tactic.interactive.measurability ?

Yup

[Suryansh Shrivastava]

These seem extremely interesting.... are there any other domain-specific tactics in development right now?

[Suryansh Shrivastava]

Also, how much measure theory has been formalized? It would be really joyful to play with this tactic

[Scott Morrison]

I'm not sure how much you've looked at mathlib3. There is a lot of measure theory there.

[Scott Morrison]

There are many other domain specific tactics, e.g. coherence and slice in category theory, polyrith in algebra ...