# Zulip Chat Archive

## 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

#### Mario Carneiro (May 12 2021 at 05:05):

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 (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 `fact`

s 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|<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 (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_chaining`

tactic 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