interesting tactics?

Stream: general

[Daniel Selsam]

Hello general. I am giving a talk next week about algorithmic problem solving to an audience of mathematicians. I would like to highlight some of the interesting uses of tactics within mathlib. Suggestions?

[Mario Carneiro]

The continuity tactic might be worth a mention, as well as the use of simp to prove integrals

[Mario Carneiro]

tidy to clean up side conditions in category theory

[Mario Carneiro]

A grobner tactic doesn't exist, but it is mathematically interesting and could exist. ring, of course, although I don't know how impressive it is

[Mario Carneiro]

The Risch algorithm is a good talking point, although to my knowledge it's never been implemented in full anywhere

[Daniel Selsam]

Mario Carneiro said:

The continuity tactic might be worth a mention, as well as the use of simp to prove integrals

Thanks, great suggestion. There are over 80 @[continuity] tags.

[Mario Carneiro]

Oh, norm_num looks like a boring tactic but I think it is more interesting when used to prove e to ten decimals

[Daniel Selsam]

Mario Carneiro said:

tidy to clean up side conditions in category theory

This is a great one.

[Daniel Selsam]

Mario Carneiro said:

Oh, norm_num looks like a boring tactic but I think it is more interesting when used to prove e to ten decimals

Indeed :)

[Mario Carneiro]

linarith is great for just not having to worry about an entire class of problems that mathematicians are ill suited to solve directly

[Daniel Selsam]

Is there a diagram chaser? Or does tidy handle this?

[Mario Carneiro]

There is rewrite_search, although it got stuck in PR limbo for a while and I'm not sure if it landed

[Alex J. Best]

I know its a bit silly but I always liked tactic#dec_trivial, the fact that lean automatically determines that certain propositions are decidable based on some simple rules via typeclass search, and then executes the code to decide the proposition always seemed quite magic to me. I'm thinking of proofs like https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/quickest.20way.20to.20kill.20.22trivial.20mod.20N.22.3F/near/194219197 or more complex variations on the same idea (i.e. which numbers are sums of 3 cubes mod 9, where writing an actual argument takes longer than just instructing lean to case-bash) where this is a very transparent way of saying just check all the cases.

[Bryan Gin-ge Chen]

Mario Carneiro said:

There is rewrite_search, although it got stuck in PR limbo for a while and I'm not sure if it landed

A version of rewrite_search was merged in #4841.

[Daniel Selsam]

Based on a quick skim, rewrite_search seems similar to SMT-style E-graph + heuristic instantiation, but without the E-graph and with more focus on the heuristic.

[Daniel Selsam]

I guess it is literally heuristic bidirectional search in rewrite space.

[Mario Carneiro]

It would be nice if we had a tactic for that that was written by someone who is familar with the theory. I think we've been bumbling about in the space

[Daniel Selsam]

At some point lean3 had a reasonable E-matching tactic, written by Leo on top of the SMT infrastructure. But E-matching might not be a good heuristic for most mathlib domains.

[Mario Carneiro]

That does ring a bell. I never really learned how to use the @[ematch] attributes correctly. I think we dropped it because there was a bug and no one knew the code well enough to fix it

[Daniel Selsam]

Mario Carneiro said:

I never really learned how to use the @[ematch] attributes correctly.

This is somewhat of a dark art.

[Johan Commelin]

@Daniel Selsam If the audience is mathematicians, I think even simp and rw deserve quite some attention. They are certainly the most used "real" tactics. (In some sense apply and exact or not "real" tactics.)
But especially simp breaks the A = B symmetry that mathematicians have fundamentally ingrained. So explaining what makes a good simp-lemma might be useful/interesting.

[Mario Carneiro]

simp is an especially interesting example because it has almost unbounded scope, it is as powerful as the simp lemmas that go into it

[Mario Carneiro]

like the example with solving integrals, it does things people would not have originally expected - the user basically gets to "program" it using simp lemmas

[Mario Carneiro]

I'm thinking of this: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/What's.20new.20in.20Lean.20maths.3F/near/228351477

[Johan Commelin]

Another, which isn't a tactic: typeclass inference. The fact that Lean automatically figures out that polynomial B is a commutative ring, and a module and an algebra over B is just very very nice.
In LTE we also (ab)use it with facts to prove all sorts of annoying trivial inequalities about real numbers.

[Scott Morrison]

The ematch bug was pretty simple: any lemma that required two different copies of the same typeclass (but for different types) killed it. This made it useless in category theory as soon any functor was involved, because there would be both the source and target category instance.

[Kevin Buzzard]

Did nobody mention nlinarith yet? A potted and probably slightly inaccurate version of its history: linarith is a powerful tool for 1st year undergraduate analysis, because it turns out that many times in analysis you say stuff like "well $|a-b|<x$ and $|b-c|<y$ and $|c-d|<z$ so clearly $|a-d|<x+y+z$" and doing this manually is a real drag, but if you invoke abs_lt then linarith does it all for you. However it didn't know $x^2\geq0$ because this wasn't linear, so @Rob Lewis added what seemed to me at least to be a "minor" extension to linarith which knew this and a couple of other nonlinear facts like $a,b\geq0\implies ab\geq0$ and called it nlinarith, and the result was a tool which, for me, was surprisingly powerful. Here's Heather using it with manifolds, and if you define the integers as a mathematician would, as a quotient of $\mathbb{N}^2$, then there's a really annoying goal to prove when checking that multiplication is well-defined, and nlinarith solves it immediately (the argument is circular but this doesn't matter for pedagogical purposes).

[David Wärn]

Kind of off-topic, but I think the quotient of $\mathbb N^2$ becomes easier to deal with if you make it a quot instead of a quotient. Namely it's the quot by the inductive family of props relating (a, b) and (a + k, b + k). Then defining multiplication using docs#quot.lift₂ should leave you with a simpler goal.

[Daniel Selsam]

Mario Carneiro said:

the user basically gets to "program" it using simp lemmas

Similar with tidy. Is there an analogue of Coq's auto in lean3? i.e. a programmable tree search?

[Daniel Selsam]

I see the extensible back_chainingtactic is still there, but I can't find a single use in mathlib

[Jannis Limperg]

We don't currently have a reasonably fully-featured proof search procedure except possibly gptf. I'm working on an auto-like tactic, but it'll be a while until that's ready for use.

[Daniel Selsam]

Interesting. FYI auto gets a lot of mileage in Coq. A few months back I cloned a dozen top Coq libraries and grepped for tactic occurrences, and auto was used 40,000 times. In contrast, ring appeared 4,000 times and field 400 times.

[Daniel Selsam]

@Jannis Limperg programmable tree-search (in lean4) is on my critical path as well

[Jannis Limperg]

Yeah, these tactics tend to be big workhorses (in Isabelle and ACL2 as well, even compared to Sledgehammer). It'll be interesting to see to what extent they apply to mathlib since the proofs here are less computer sciency. I'm planning to port to Lean 4 as well; I just started in Lean 3 so that I would have a staple API and a big library on which to test the thing.

[Daniel Selsam]

FWIW I wouldn't recommend porting this kind of tactic. There are many new opportunities that could be exploited by a clean-slate design in lean4, thanks to e.g. built-in discrimination trees, better support for environment caching, etc.

[Jannis Limperg]

Interesting. I'll message you privately to avoid derailing the thread further.

[Rob Lewis]

Kevin Buzzard said:

nlinarith

The original nlinarith was from @Mario Carneiro , a light wrapper around linarith that did what the Coq nlinarith docs claimed to do. I updated it a bit to do what (I think) Coq's nlinarith actually does. Then had to speed up linarith because some reasonable goals were too slow.

[Scott Morrison]

Anothern interesting tactic that I think hasn't been mentioned (and is perhaps underused) is tactic#solve_by_elim