## Stream: new members

### Topic: Effectiveness as a computer algebra system?

#### Jake (May 17 2020 at 02:15):

If i have two algebraic expressions, how complicated do they have to be such that simp, ring, cc, etc.. can't tell they are equal? And since we can add proofs that simp can use to simplify things, can we in theory make a simplifier on algebraic expressions as good as something like wolfram alpha (or simplify or fullsimplify on mathematica); if not where's the line where lean would start having technical roadblocks? Thank you

#### ROCKY KAMEN-RUBIO (May 17 2020 at 02:40):

The intuition for this is something I'm still developing. I was confused for a while why simp wasn't able to do some obvious things, like flip an inequality around, or feed A into A implies B to prove B. My understanding is that hopefully new, more comprehensive tactics will get written as mathlib gets built out, so that everything outside of the scope of your current proof can be automated. If you're interested in writing tactics, I recently started trying to figure out how to do it. Here's a brief guide. https://leanprover-community.github.io/extras/tactic_writing.html

#### Jake (May 17 2020 at 02:48):

awesome ill check that out

#### Scott Morrison (May 17 2020 at 03:44):

It's important to remember that tactics aren't magic. :-) Usually each of them is try to do one specific thing well.

#### Scott Morrison (May 17 2020 at 03:45):

That said, if you can clearly specify what you think a new tactic should do, the sky is the limit writing new tactics.

#### Scott Morrison (May 17 2020 at 03:45):

There's no particular reason why simp couldn't become as powerful as Mathematica's Simplify.

#### Scott Morrison (May 17 2020 at 03:46):

FullSimplify in Mathematica is doing something more complicated (and not at all publicly specified), that involves backtracking, which simp doesn't do.

#### Yury G. Kudryashov (May 17 2020 at 03:46):

Except maybe for human*hours.

#### Scott Morrison (May 17 2020 at 03:47):

Yes --- the bottleneck for new awesome tactics is definitely availability of humans who know how to write them, not ideas for them, or their viability in the current meta-programming setup.

#### Scott Morrison (May 17 2020 at 03:47):

I think it would actually be a fun project to compare the effectiveness of simp and Mathematica's Simplify.

#### Scott Morrison (May 17 2020 at 03:48):

Analysing examples of things that Simplify can do that simp can't could be very helpful.

#### Mario Carneiro (May 17 2020 at 03:54):

Actually I think there is also a bottleneck on precise specifications of tactics

#### Mario Carneiro (May 17 2020 at 03:55):

I can't think of many examples of precisely specified tactics that don't exist yet except for groebner

#### Scott Morrison (May 17 2020 at 04:04):

We really should keep a list of tactic requests. I guess just the issues page.

#### Bryan Gin-ge Chen (May 17 2020 at 04:11):

Good idea. I just opened #2706.

#### Scott Morrison (May 17 2020 at 04:11):

A tactic that we still don't have is group, which removes any instances of 1, g * g⁻¹ or g⁻¹ * g in a group product, even in the presence of parentheses.

#### Mario Carneiro (May 17 2020 at 04:12):

I think it's called simp

#### Scott Morrison (May 17 2020 at 04:14):

We should still have group := [simp only [...]]  for whatever the collection of lemmas that achieves this is.

#### Yury G. Kudryashov (May 17 2020 at 04:14):

I can't think of many examples of precisely specified tactics

E.g., CAS-style operations on expressions:

• expand (=simp only [mul_add, add_mul, mul_sub, sub_mul, smul_*]?),
• factorize;
• group by powers of x;
• cancel a fraction;
• together (probably field_simp does this job);
• a version of field_simp that adds goals a ≠ 0 instead of failing to apply a lemma.

#### Scott Morrison (May 17 2020 at 04:15):

More generally, we should have word_problem, that tries to discharge a goal of the form g1 * g2 * g3 = g4 * g5 by looking in the hypotheses for other relations in the group, and then dispatching to an appropriately registered solution to the word problem in the relevant group.

#### Scott Morrison (May 17 2020 at 04:16):

e.g. implementing all the mathematics in https://www3.nd.edu/~andyp/notes/OneRelator.pdf, and then being able to answer any such question where there is a single hypothesis giving a relation.

#### Scott Morrison (May 17 2020 at 04:17):

We should have the multiplicative version of abel, which I think is not a special case of simp.

#### Scott Morrison (May 17 2020 at 04:19):

We should have tactics push_hom and pull_hom, which use lemmas like ring_hom.map_mul to either move algebraic homomorphisms inwards or outwards.

#### Scott Morrison (May 17 2020 at 04:24):

Another fun project that would require doing some maths first would be to implement the Schreier-Sims algorithm, and then have a tactic that can write a permutation as a product of permutations from a given set (if possible).

#### Kevin Buzzard (May 17 2020 at 08:36):

A basic grouptactic got written in another thread, didn't it? The other thread probably mentions the same pdf

Last updated: May 13 2021 at 05:21 UTC