Effectiveness as a computer algebra system?

Stream: new members

[Jake]

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]

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]

awesome ill check that out

[Scott Morrison]

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

[Scott Morrison]

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]

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

[Scott Morrison]

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]

Except maybe for human*hours.

[Scott Morrison]

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]

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

[Scott Morrison]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Scott Morrison]

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

[Bryan Gin-ge Chen]

Good idea. I just opened #2706.

[Scott Morrison]

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]

I think it's called simp

[Scott Morrison]

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

[Yury G. Kudryashov]

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]

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]

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]

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

[Scott Morrison]

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]

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]

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