norm_cast and inverses

Stream: mathlib4

[Kevin Buzzard]

I was surprised to see this behaviour:

import Mathlib

example (x : ℝ) : Complex.cos ((3 : ℝ) * x) = 37 := by
  norm_cast
  -- ⊢ Real.cos (3 * x) = 37
  sorry

example (x : ℝ) : Complex.cos ((3 : ℂ) * (x : ℂ)) = 37 := by
  norm_cast
  -- ⊢ Real.cos (3 * x) = 37
  sorry

example (x : ℝ) : Complex.cos ((3⁻¹ : ℝ) * x) = 37 := by
  norm_cast
  -- ⊢ Real.cos (3⁻¹ * x) = 37
  sorry

example (x : ℝ) : Complex.cos ((3 : ℂ)⁻¹ * (x : ℂ)) = 37 := by
  norm_cast
  -- ⊢ Complex.cos (3⁻¹ * ↑x) = 37
  sorry

In the last example, which is somehow the pushout of the two previous examples, norm_cast fails to simplify it to Real.cos despite this clearly being possible. Is there some trick which will make norm_cast behave?

(I'm asking because I'm trying to understand some of the troubles I had in this proof .)

[Eric Wieser]

Starting with rw [←  Complex.ofReal_ofNat] fixes it

[Eric Wieser]

Also in #mathlib4 > norm_cast and ofNat , #mathlib4 > `norm_cast` requires manual `rw [← WithBot.coe_ofNat]` @ 💬, #mathlib4 > exact_mod_cast and rationals @ 💬

[Eric Wieser]

So I think the answer is that norm_cast hasn't be taught how to move numerals between types

[Eric Wieser]

And it's in core not mathlib, so I guess we need a mathlib-free repro

[Aaron Liu]

norm_cast can move numerals between types, it just doesn't know that the 3 want to be a ℝ because the ⁻¹ is in the way.

[Kevin Buzzard]

Cargo-culting from the last of those threads:

import Mathlib

-- we used to have this
example (x : ℝ) : Complex.cos ((3⁻¹ : ℝ) * x) = 37 := by
  norm_cast
  -- ⊢ Real.cos (3⁻¹ * x) = 37
  sorry

-- I don't understand parts of this gobble-de-gook
@[norm_cast]
theorem Rat.cast_ofNat_inv (K : Type*) [DivisionRing K] [CharZero K] (d : ℕ)
    [d.AtLeastTwo] :
    ((no_index (OfNat.ofNat d))⁻¹ : ℚ) =
      ((no_index (OfNat.ofNat d) : ℕ)⁻¹ : K)
       := by simp

-- this has now got a bit worse
example (x : ℝ) : Complex.cos ((3⁻¹ : ℝ) * x) = 37 := by
  norm_cast
  -- ⊢ Real.cos (↑3⁻¹ * x) = 37
  sorry

-- but this has now got a bit better
example (x : ℝ) : Complex.cos ((3 : ℂ)⁻¹ * (x : ℂ)) = 37 := by
  norm_cast
  -- ⊢ Complex.cos (↑3⁻¹ * ↑x) = 37
  sorry

[Kevin Buzzard]

The 3 that was a real is now a rational.

[Kevin Buzzard]

Oh wow:

example : (((37 : ℚ)⁻¹ : ℚ) : ℝ) = (37 : ℝ)⁻¹ := by
  norm_cast -- fails?!
  sorry

[Aaron Liu]

Kevin Buzzard said:

Oh wow:

example : (((37 : ℚ)⁻¹ : ℚ) : ℝ) = (37 : ℝ)⁻¹ := by
  norm_cast -- fails?!
  sorry

norm_cast doesn't work very well on numerals.

import Mathlib

example : (((37 : ℚ)⁻¹ : ℚ) : ℝ) = (37 : ℝ)⁻¹ := by
  /-
  simplifying ↑37⁻¹ = 37⁻¹
  · simplifying ↑37⁻¹
    · simplifying 37⁻¹
      · simplifying 37
        no simps
      result -> 37⁻¹
      no simps
    result -> ↑37⁻¹
    no simps
  · simplifying 37⁻¹
    · simplifying 37
      no simps
    result -> 37⁻¹
    no simps
  result -> ↑37⁻¹ = 37⁻¹
  no simps
  -/
  fail_if_success fail_if_no_progress norm_cast
  sorry

[Kevin Buzzard]

yeah but maybe we can fix that?

[Kevin Buzzard]

e.g.

@[norm_cast]
lemma foo (n : ℕ) : (((n : ℚ)⁻¹ : ℚ) : ℝ) = (n : ℝ)⁻¹ := by
  simp

example : (((37 : ℚ)⁻¹ : ℚ) : ℝ) = (37 : ℝ)⁻¹ := by
  norm_cast -- now works

[Aaron Liu]

You could turn off Nat.cast_ofNat while running norm_cast, and then do a second pass to refold it. This would also solve the Complex.cos one.

[Kevin Buzzard]

import Mathlib

@[norm_cast]
theorem Rat.cast_ofNat_inv (K : Type*) [DivisionRing K] [CharZero K] (d : ℕ) [d.AtLeastTwo] :
    ((ofNat(d))⁻¹ : ℚ) = ((ofNat(d) : ℕ)⁻¹ : K) := by simp

example (x : ℝ) : Complex.cos ((3⁻¹ : ℝ) * x) = 37 := by
  norm_cast
  -- ⊢ Real.cos (↑3⁻¹ * x) = 37
  push_cast
  -- ⊢ Real.cos (3⁻¹ * x) = 37 :tada:
  sorry

[Aaron Liu]

Unfortunately there is not way to remove the norm_cast attribute, so I can't show the the benefits of taking outNat.cast_ofNat.

The code for the attribute is here (notice there is no erase field).

[Kim Morrison]

You can make a PR to lean, and get a toolchain without the attribute! :-)

[Aaron Liu]

Kim Morrison said:

You can make a PR to lean, and get a toolchain without the attribute! :-)

Finally figured out how to build Lean, will try this tomorrow.