Zulip Chat Archive

Stream: new members

Topic: Effectiveness as a computer algebra system?


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Jake (May 17 2020 at 02:48):

awesome ill check that out

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Scott Morrison (May 17 2020 at 03:45):

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

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (May 17 2020 at 03:46):

Except maybe for human*hours.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Scott Morrison (May 17 2020 at 03:48):

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

view this post on Zulip Mario Carneiro (May 17 2020 at 03:54):

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

view this post on Zulip 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

view this post on Zulip Scott Morrison (May 17 2020 at 04:04):

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

view this post on Zulip Bryan Gin-ge Chen (May 17 2020 at 04:11):

Good idea. I just opened #2706.

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (May 17 2020 at 04:12):

I think it's called simp

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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