Stream: general

Topic: interesting tactics?

Daniel Selsam (May 12 2021 at 01:44):

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 (May 12 2021 at 02:25):

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

Mario Carneiro (May 12 2021 at 02:26):

tidy to clean up side conditions in category theory

Mario Carneiro (May 12 2021 at 02:29):

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 (May 12 2021 at 02:31):

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

Daniel Selsam (May 12 2021 at 02:33):

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 (May 12 2021 at 02:34):

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 (May 12 2021 at 02:36):

Mario Carneiro said:

tidy to clean up side conditions in category theory

This is a great one.

Daniel Selsam (May 12 2021 at 02:37):

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 (May 12 2021 at 02:37):

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 (May 12 2021 at 02:40):

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

Mario Carneiro (May 12 2021 at 02:41):

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 (May 12 2021 at 02:42):

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 (May 12 2021 at 02:45):

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 (May 12 2021 at 02:50):

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 (May 12 2021 at 02:52):

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

Mario Carneiro (May 12 2021 at 02:53):

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 (May 12 2021 at 02:55):

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 (May 12 2021 at 02:57):

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 (May 12 2021 at 03:02):

Mario Carneiro said:

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

This is somewhat of a dark art.

Johan Commelin (May 12 2021 at 04:53):

@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 (May 12 2021 at 05:00):

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 (May 12 2021 at 05:02):

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

Johan Commelin (May 12 2021 at 05:41):

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 (May 12 2021 at 07:26):

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 (May 12 2021 at 07:37):

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| and $|b-c| and $|c-d| so clearly $|a-d|" 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 (May 12 2021 at 08:37):

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 (May 12 2021 at 14:32):

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 (May 12 2021 at 14:34):

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

Jannis Limperg (May 12 2021 at 14:39):

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 (May 12 2021 at 14:44):

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 (May 12 2021 at 14:45):

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

Jannis Limperg (May 12 2021 at 14:54):

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 (May 12 2021 at 15:13):

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 (May 12 2021 at 15:24):

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

Rob Lewis (May 12 2021 at 15:32):

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 (May 12 2021 at 22:58):

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

Last updated: Dec 20 2023 at 11:08 UTC