Algebraic simplification / CAS

Stream: new members

[Izan Beltran]

Hello! I have been learning Lean for a month already.

I am wondering whether there is any way of doing algebraic simplification (as in a CAS like Sympy, Mathematica, etc) to simplify expressions. I am finding that some problems involving vectors, norms, etc... require a lot of steps just for typical algebraic manipulations/simplification. Sometimes take the majority of the code, while the formalization and key steps are much simpler in terms of code length.
I am using mathlib and real numbers mostly.

Usually things like canceling inverse terms in long products or numerators with denominators is not straightforward, but functions like Sympy's simplify() usually solve them.

I didn't find anything similar yet, so maybe someone here can point me to an appropiate tactic or tool?
I think this would improve a lot my experience with Lean for verifying some textbook problems solutions.

Thanks!

[Kenny Lau]

import Mathlib

example : (1 + 1/3 + 1/5 + 1/7 : ℝ) = sorry := by
  norm_num
  -- ⊢ 176 / 105 = sorry
  sorry

[Kenny Lau]

is norm_num what you're looking for?

[Michael Rothgang]

Do you know about field_simp and ring?

[Kenny Lau]

giving examples would greatly help us help you

[Izan Beltran]

Sure! Sorry I should have started with an example.

Consider the following example:

c x y : ℝ
u v : EuclideanSpace ℝ (Fin 2)
hc : c ≠ 0
hx : x ≠ 0
hy : y ≠ 0
hu : u ≠ ![0, 0]
hv : v ≠ ![0, 0]
huv : ‖u‖ * ‖v‖ = ⟪u, v⟫ -- implies aligned
huv' : ‖v‖ > ‖u‖
h1 : ‖u‖ ≠ 0
h2 : ‖v‖ ≠ 0
⊢ ‖-(-(c * x * y * x⁻¹ * ‖v‖⁻¹ ^ 3) • v) + -(c * y * x * x⁻¹ * ‖u‖⁻¹ ^ 3) • u‖ = c * y * (‖u‖⁻¹ ^ 2 - ‖v‖⁻¹ ^ 2)

I would like for the x and x⁻¹ to cancel automatically, but x * y * x⁻¹ is not simplified with field_simp or ring_nf. Moreover, I would be happy for it to automatically factor c * y and get something like
‖(c * y) • ((‖v‖⁻¹ ^ 3) • v - (‖u‖⁻¹ ^ 3) • u)‖
or
|c * y| * ‖(‖v‖⁻¹ ^ 3) • v - (‖u‖⁻¹ ^ 3) • u‖
in the left hand side. Most computer algebra systems, like Sympy, can get to this point, so I was wondering if there is any algorithm implemented with similar capabilities.

[Ruben Van de Velde]

You did call it as field_simp [hx], right? The cancelling seems like it could be workable, but might not work yet

[Richard Copley]

The docstring for field_simp says

If you have objects with an IsUnit x instance like (x : R) (hx : IsUnit x), you should lift them with lift x to Rˣ using id hx; rw [IsUnit.unit_of_val_units] clear hx before using field_simp.

There appears to be a typo. I'm not sure what was meant. But if you can guess, you could start with rw [← isUnit_iff_ne_zero] at hx hy hc h1 h2, then try doing some lifts.

[Richard Copley]

(Please see #mwe; if you had formatted your example as below, it would be easier for people to jump in and try things out, and you might get more ideas.)

import Mathlib

open RealInnerProductSpace

example
  (c x y : ℝ)
  (u v : EuclideanSpace ℝ (Fin 2))
  (hc : c ≠ 0)
  (hx : x ≠ 0)
  (hy : y ≠ 0)
  (hu : u ≠ ![0, 0])
  (hv : v ≠ ![0, 0])
  (huv : ‖u‖ * ‖v‖ = ⟪u, v⟫) -- implies aligned
  (huv' : ‖v‖ > ‖u‖)
  (h1 : ‖u‖ ≠ 0)
  (h2 : ‖v‖ ≠ 0) :
    ‖-(-(c * x * y * x⁻¹ * ‖v‖⁻¹ ^ 3) • v) + -(c * y * x * x⁻¹ * ‖u‖⁻¹ ^ 3) • u‖ =
      c * y * (‖u‖⁻¹ ^ 2 - ‖v‖⁻¹ ^ 2) := by
  sorry

[Izan Beltran]

@Ruben Van de Velde Yes, I have tried that

[Izan Beltran]

@Richard Copley Just read #mwe and makes a lot of sense, thanks

[Ruben Van de Velde]

I suspect everything you're asking about is possible but nothing exists right now

[Nikolas Tapia]

Ruben Van de Velde said:

I suspect everything you're asking about is possible but nothing exists right now

For example, as far as I could see the theorem ‖u‖ * ‖v‖ = ⟪u, v⟫ → ‖u+v‖ = ‖u‖ + ‖v‖ (which I guess has to be used at some point) is not in Mathlib.Analysis.InnerProductSpace.Basic. Here's a proof

have : ‖u+v‖ = ‖u‖ + ‖v‖ := by
  apply norm_add_eq_iff_real.mpr
  apply inner_eq_norm_mul_iff_real.mp
  symm
  exact huv

[Izan Beltran]

@Nikolas Tapia Yes, thanks, I was using inner_eq_norm_mul_iff_real : ⟪x, y⟫ = ‖x‖ * ‖y‖ ↔ ‖y‖ • x = ‖x‖ • y for doing something similar. The problem is all the little algebraic manipulations required in between, which are not trivial to do in Lean (with my little experience).

[Izan Beltran]

Richard Copley said:

The docstring for field_simp says

If you have objects with an IsUnit x instance like (x : R) (hx : IsUnit x), you should lift them with lift x to Rˣ using id hx; rw [IsUnit.unit_of_val_units] clear hx before using field_simp.

There appears to be a typo. I'm not sure what was meant. But if you can guess, you could start with rw [← isUnit_iff_ne_zero] at hx hy hc h1 h2, then try doing some lifts.

I have been checking this, but I didn't manage to get any improvement. I don't understand at all what is the benefit of lifting to the units of ℝ. I was expecting field_simp [hx] to act similarly, as I provided that x ≠ 0.

[Ruben Van de Velde]

Yeah, I think the units are a red herring. This works:

import Mathlib

example {x y : ℝ} (hx : x ≠ 0) : x * x⁻¹ * y = y := by field_simp

[Ruben Van de Velde]

It's getting the x and x⁻¹ together that field_simp doesn't do

[Izan Beltran]

@Ruben Van de Velde Yes, in such simple situations it works, but consider the example above that Richard shared. If we have

‖-(-(c * x * y * x⁻¹ * ‖v‖⁻¹ ^ 3) • v) + -(c * y * x * x⁻¹ * ‖u‖⁻¹ ^ 3) • u‖ =
      c * y * (‖u‖⁻¹ ^ 2 - ‖v‖⁻¹ ^ 2)

then field_simp [hx] simplifies it to

‖-((-(c * x * y) / (x * ‖v‖ ^ 3)) • v) + (-(c * y) / ‖u‖ ^ 3) • u‖ *
      (‖u‖ ^ 2 * ‖v‖ ^ 2) =
      c * y * (‖v‖ ^ 2 - ‖u‖ ^ 2)

which is not super useful, since x could be cancelled, and some other simplifications could be devised.

[Nikolas Tapia]

I think it gets confused as soon as there are too many variables:

import Mathlib

example {x y c : ℝ} (h : x ≠ 0) : c * x * y * x⁻¹ = c * y := by field_simp

yields

unsolved goals
x y c : ℝ
h : x ≠ 0
⊢ c * x * y = c * y * x

[Yaël Dillies]

Note that @Heather Macbeth and co have a reimplementation of field_simp in the works, and I believe it solves this specific issue. I think therefore it's not particularly useful to spend time debugging field_simp this month :slight_smile:

[Izan Beltran]

Exactly @Nikolas Tapia, that's my point, that it stops working as desired if you have a more convoluted context. Nice to know that there will be an improved version of it, thanks @Yaël Dillies!

[Izan Beltran]

But therefore I guess there is no way of using an equivalent of a CAS inside Lean or a tactic that works like it, and the main options for simplifications are tactics like ring_nf, field_simp and simp?

[Yaël Dillies]

... and the shiny new grind tactic

[Izan Beltran]

@Yaël Dillies Unfortunately, grind is not powerful enough for this case :(

[Michael Rothgang]

I'm one of the people working on the field_simp rewrite: we hope to open the real PR this week (and then, reviewing will be very welcome :-))

[Ruben Van de Velde]

Is everyone who could plausibly review it working on it? :)

[Michael Rothgang]

I hope not... but indeed, that tends to be the issue with meta code.

[Notification Bot]

5 messages were moved from this topic to #mathlib4 > PR for new field_simp implementation by Heather Macbeth.