(In)completeness of ring_exp

Stream: new members

[Kazuhiko Sakaguchi]

Hello. It seems to me that mathlib's ring_exp is incomplete. For example, it does not solve the following goal.

example (a b c : int) (n : nat) : (a * (b + c)) ^ n = a ^ n * (b + c) ^ n :=
begin
ring_exp,
end

Is there any idea on how to fix this issue and guarantee completeness? I'm actually interested in reimplementing ring_exp in Coq (for MathComp) using computational reflection rather than fixing this issue in mathlib. Since I have to prove the correctness of the procedure in that scenario, it would be nice to have a complete procedure first (so that I don't have to fix the procedure and the proof again and again).

[Reid Barton]

I think this kind of question is quite subtle, e.g. https://en.wikipedia.org/wiki/Tarski%27s_high_school_algebra_problem

[Rob Lewis]

cc @Anne Baanen

[Anne Baanen]

Good catch! There's no real support for addition under an exponent, so it doesn't really surprise me something goes wrong here, but it should do better than this so let me see if I can fix it...

[Anne Baanen]

Aha, so it rewrites a * (b + c) to a * b + a * c and then gives up because there is no rule for (_ + _) ^ _.

[Anne Baanen]

I don't see an easy way to modify the current ring_exp procedure so it solves this goal. :frown:

[Mario Carneiro]

Is ring_exp intended to be a decision procedure? Is its range of applicability known?

[Mario Carneiro]

Like Reid says, an actual decision procedure for this grammar seems technically challenging at best and provably impossible at worst

[Anne Baanen]

It's a simplification procedure extending the language of rings to allow polynomial expressions in the exponents of (products of) variables.

[Anne Baanen]

So any additions appearing under an exponentiation will be handled best-effort (which is not very good as you just showed)

[Kazuhiko Sakaguchi]

In the case of Tarski's high school algebra problem, the Wikipedia article says that the source of incompleteness is the lack of the opposite operator. So it does not seem to directly apply to ring_exp. But indeed, "this problem is actually undecidable" is one of the answers I expected.
Anyway, thanks for the feedback. The way I see this problem is the rewriting rules are not confluent (modulo AC). So known facts or techniques in term rewriting may answer this question.

[Reid Barton]

That's true but if you allow - in the syntax then it becomes a bit unclear what the domain of the decision procedure should even be--after all you can't raise an element of a ring to a negative power.

[Kazuhiko Sakaguchi]

My understanding is that the syntax is multi sorted and an exponent must be a natural number. But then, what ring_exp accepts as an exponent is a semiring expression with exponents. Now I see the problem you pointed out.