Simple computation with real numbers is painful

Stream: mathlib4

[Michael Rothgang]

Fixing a proof in the Carleson project, I'm left with the following computation: it's simple, right? The best I can do without putting excessive thought into it is five dense lines. Please show me what I'm doing wrong :-)

import Mathlib
lemma baz : (2 : ℝ) ^ (1 / (2 : ℝ)) * 2 = 8 ^ (1 / (2 : ℝ)) := sorry

Let me pre-empt this by noting that norm_num does nothing on the goal.

[Michael Rothgang]

My solution

import Mathlib
lemma baz : (2 : ℝ) ^ (1 / (2 : ℝ)) * 2 = 8 ^ (1 / (2 : ℝ)) := by
        rw [← Real.sqrt_eq_rpow, ← Real.sqrt_eq_rpow]
        have : Real.sqrt 4 = 2 := Real.sqrt_eq_cases.mpr <| Or.inl ⟨by norm_num, by positivity⟩
        nth_rw 2 [← this]
        rw [← Real.sqrt_mul (by positivity) 4]
        norm_num

[Michael Rothgang]

"Don't get to a stage where you have 2 ^ (1/2)" would be a reasonable answer, but not when I'm fixing somebody else's proof, in a file with lower standards than mathlib, which I need to maintain to bump Carleson.

[Michael Stoll]

import Mathlib

lemma baz : (2 : ℝ) ^ (1 / (2 : ℝ)) * 2 = 8 ^ (1 / (2 : ℝ)) := by
  rw [← sq_eq_sq₀ (by positivity) (by positivity), mul_pow, ← Real.rpow_natCast,
    ← Real.rpow_mul zero_le_two, ← Real.rpow_natCast (_ ^ (1 / 2 : ℝ)), ← Real.rpow_mul (by positivity)]
  norm_num

Not much shorter, but perhaps clearer...

[Sébastien Gouëzel]

With rpow_ring from PFR, it's

lemma baz : (2 : ℝ) ^ (1 / (2 : ℝ)) * 2 = 8 ^ (1 / (2 : ℝ)) := by
  rw [show (8: ℝ) = 2 ^ 3 by norm_num]
  rpow_simp
  norm_num

Not sure why we never upstreamed it...

[Michael Stoll]

rpow_simp looks like a nice addition. Could it be a simproc?

[Ruben Van de Velde]

import Mathlib
lemma baz : (2 : ℝ) ^ (1 / (2 : ℝ)) * 2 = 8 ^ (1 / (2 : ℝ)) := by
  have : (2 : ℝ) = (2 : ℝ) ^ (1 / (2 : ℝ)) * (2 : ℝ) ^ (1 / (2 : ℝ)) := by
    rw [← Real.mul_rpow, ← sq, ← Real.rpow_ofNat, ← Real.rpow_mul]
    simp
    all_goals positivity
  conv =>
    lhs
    right
    rw [this]
  simp [← Real.mul_rpow]
  norm_num

Meh.

[Ruben Van de Velde]

import Mathlib
lemma baz : (2 : ℝ) ^ (1 / (2 : ℝ)) * 2 = 8 ^ (1 / (2 : ℝ)) := by
  rw [mul_comm, ← eq_div_iff_mul_eq, ← Real.div_rpow]
  all_goals norm_num

[Michael Rothgang]

I'm not sure what rpow_simp is, but I'm sure I'll love it. What can I do I to make you upstream it? Promise to take a look at the PR? :sweat_smile:

[Michael Rothgang]

It's defined here: https://github.com/teorth/pfr/blob/master/PFR/Tactic/RPowSimp.lean

[Sébastien Gouëzel]

It's pure meta code, so I'm definitely not in a position to upstream it. If you want to have a look, it's the single file https://github.com/teorth/pfr/blob/master/PFR/Tactic/RPowSimp.lean. You can use it in Carleson if you like!

[Michael Rothgang]

So, this file defines

• a tactic rpow_ring (some kind of extension of ring to support real powers?)
• a macros rpow_simp which runs (1) simp with positivity as discharger and some custom simp set, then rpow_ring, field_simp and that simp version again

So, the hard part of reviewing is the ring part --- and then some documentation on that set of lemmas would be nice. I'll ask around for the first part.

[Yaël Dillies]

Note that I removed code from rpow_ring over a few mathlib bumps. I believe it did not make the tactic weaker, but you might want to check the earlier code as well

[Yaël Dillies]

I should add that it didn't make the tactic weaker within PFR

[Eric Wieser]

Didn't @Yury G. Kudryashov recently merge a PR that teaches norm_num to do this?

[Yury G. Kudryashov]

Not this, only roots that are rational.

[Aaron Liu]

I wonder if it would be easy to decide the theory of real-closed fields in a tactic

[Yury G. Kudryashov]

Here is a 2-line proof:

lemma baz : (2 : ℝ) ^ (1 / (2 : ℝ)) * 2 = 8 ^ (1 / (2 : ℝ)) := by
  rw [← sq_eq_sq₀] <;> try positivity
  norm_num [mul_pow, ← Real.rpow_mul_natCast]

[Johan Commelin]

Aaron Liu said:

I wonder if it would be easy to decide the theory of real-closed fields in a tactic

That doesn't give you rpow, right?

[Johan Commelin]

General comment about the golfs in this thread: they are really impressive! :octopus: :tada: :golf:

However, I believe that a goal like this deserves to be closed by a single tactic (without needing to feed it some extra lemmas). And reaching for this tactic should be a no-brainer.

Until we have that tactic, we're living in the real number stone age...

[Ruben Van de Velde]

Yeah, this seems like it should be in scope for norm_num

[Michael Rothgang]

Indeed! Recognising "this is a power 1/2, let me convert that to a square root" (and then the remaining algorithm of norm_num kick in) seems like a missing extension. Volunteers writing that appreciated :-)

[Ruben Van de Velde]

Mm,I think I'd like it to support other powers as well

[Yury G. Kudryashov]

Michael Rothgang said:

Indeed! Recognising "this is a power 1/2, let me convert that to a square root" (and then the remaining algorithm of norm_num kick in) seems like a missing extension. Volunteers writing that appreciated :-)

It's not in the scope of norm_num, because the answer is irrational.

[Ruben Van de Velde]

Normalize numerical expressions. Supports the operations + - * / ⁻¹ ^ and % over numerical types such as ℕ, ℤ, ℚ, ℝ, ℂ and some general algebraic types, and can prove goals of the form A = B, A ≠ B, A < B and A ≤ B, where A and B are numerical expressions. It also has a relatively simple primality prover.

[Ruben Van de Velde]

Sounds in scope to me :)

[Yury G. Kudryashov]

I mean, we can't easily write a norm_num extension that will handle this. We need to redesign norm_num itself (or write a bunch of simpprocs instead).

[Yury G. Kudryashov]

Before doing any redesign, we need to decide what should be in scope:

• $\sqrt{5+2\sqrt{6}} = \sqrt{2} + \sqrt{3}$?
• $\sqrt{5-2\sqrt{6}} = \sqrt{3} - \sqrt{2}$?
• $(1 + i) ^{50}$?
• $8 ^ (1 / 2) * 6 ^ (1 / 3) * 2 ^ (1 / 6)$?