Simplifying real/complex expressions

Stream: new members

[Simon Jacobsson]

Hello,
Sometimes I get real/complex algebraic expressions like

z * (p / 2) + (z * (p / 2) + p / 2 * (p / 2)) = z * p + p / 2 * (p / 2)

that are obviously equal and that I know I would be able to show are equal if I could rewrite them to some canonical form. For example, if I could automatically

1. distribute multiplication over addition
2. sort the factors of each term (and collect the numerical coefficients)
3. sort the terms (and collect terms that only have different coefficients).
   Is it possible to write something like this in Lean? If so, is such a thing maybe already implemented?

I have written something like this in Mathematica once, but there I was able to get the names of variables as strings which I don't know if you can in Lean. Also, in Mathematica, addition is implemented like Plus : [expr] -> expr and automatically unpacks nested additions, while in Lean I guess you're stuck with the binary operator and have to use the associativity property explicitly each time?

[Anne Baanen]

You could try tactic#ring_nf, this does basically the three things you listed.

[Anne Baanen]

If your expression contains more complicated divisions, you might want to use tactic#field_simp first, because ring / ring_nf don't know how to deal with those.

[Anne Baanen]

Anne Baanen said:

You could try tactic#ring_nf, this does basically the three things you listed.

Sorry, ring_nf is documented as part of tactic#ring.

[Rémy Degenne]

To illustrate what Anne is explaining, here is a proof of your equality:

import analysis.complex.basic

example (z p : ℂ) :
  z * (p / 2) + (z * (p / 2) + p / 2 * (p / 2)) = z * p + p / 2 * (p / 2) :=
by ring

[Simon Jacobsson]

Okay thank you, I guess ring_nf is exactly what I was looking for.

[Simon Jacobsson]

I'm guessing that, since you only have binary addition in Lean, ring and ring_nf must be more advanced than a tactic simp [lemma1, lemma2, ...]

[Anne Baanen]

Simon Jacobsson said:

I'm guessing that, since you only have binary addition in Lean, ring and ring_nf must be more advanced than a tactic simp [lemma1, lemma2, ...]

Indeed! They represent expressions as multivariate polynomials in Horner normal form.

[Mario Carneiro]

What do you mean by "you only have binary addition in lean"? ring is what you want in this example, not ring_nf, but it works roughly as you have described (except it works on multivariate polynomials so it also has to sort monomials)

[Anne Baanen]

If you want the gory details, see Proving Equalities in a Commutative Ring Done Right in Coq :)

[Mario Carneiro]

and then cross out the word Coq and write Lean :)

[Anne Baanen]

Although you can get pretty far if you don't care about coefficients, with simp [add_assoc, mul_assoc, add_comm, add_left_comm, mul_comm, mul_left_comm] (or is that add_right_comm? I always forget)

[Anne Baanen]

Mario Carneiro said:

and then cross out the word Coq and write Lean :)

Well, Lean doesn't even do the proof by reflection part :grinning:

[Mario Carneiro]

true, it's actually quite a bit different such that you might only call the original coq implementation an inspiration rather than an actual port

[Mario Carneiro]

(it is add_left_comm btw)

[Simon Jacobsson]

Mario Carneiro said:

What do you mean by "you only have binary addition in lean"?

I just meant that, in e.g. Mathematica, the + takes a list as an argument and a + b is shorthand for Plus [a, b].

[Mario Carneiro]

If you simp [add_assoc, add_left_comm, add_comm] like anne suggests, you will get an effect equivalent to mathematica's Plus [a, b, c, ...]: the entire addition chain will get sorted by the term order

[Simon Jacobsson]

Anne Baanen said:

If you want the gory details, see Proving Equalities in a Commutative Ring Done Right in Coq :)

I had already opened it in a different tab :)

[Mario Carneiro]

the reason this doesn't really work and why ring is a separate mechanism is that it might not sort -a next to a in order to cancel them

[Mario Carneiro]

or more generally, 2 * a and 4 * a and so on

[Patrick Johnson]

Simon Jacobsson said:

I just meant that, in e.g. Mathematica, the + takes a list as an argument and a + b is shorthand for Plus [a, b].

We also have docs#list.sum. For example, list.sum [a, b, c] is definitionally equal to 0 + a + b + c, although list.sum doesn't go well with ring

[Eric Wieser]

I don't think that's what it's definitionally equal to, I think it's more like a + (b + (c + 0))) (xref #161)