# Zulip Chat Archive

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

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

Last updated: Dec 20 2023 at 11:08 UTC