norm_cast best practices

Stream: mathlib4

[Alex Meiburg]

Consider the following:

import Mathlib

example (x : ℝ) (hx : x = 3 / 5) : ((3 / 5 : ℚ) : ℂ) = x := by
  rw [hx]
  norm_cast
  sorry

The norm_cast fails to close this goal. Before that line, the goal is

↑(3 / 5) = ↑(3 / 5)   aka  ((3 / 5 : ℚ) : ℂ) = ((3 / 5 : ℝ) : ℂ)

and afterwards it's

↑(3 / 5) = 3 / 5   aka  ((3 / 5 : ℚ) : ℝ) = (3 / 5 : ℝ)

This seems a bit unfortunate, since a goal that "looks like" ↑(3 / 5) = ↑(3 / 5) should in general be the kind of thing that norm_cast can solve. This also means that exact_mod_cast rfl doesn't close the goal. (Not that that is really necessary, but it means that in other more complicated situations things wouldn't work.) Note that simp and push_cast; rfl both work, by essentially moving all the casts inwards instead.

I noticed this while trying to figure out the ideal norm_cast's for a different type, was having some issues, and I wanted to see how ℂ handles it, only to see it wasn't ideal either.

What's the theory here? Like, what's the best way to pick simp/norm_cast/push_cast lemmas to handle this robustly?

[Aaron Liu]

#mathlib4 > norm_cast and inverses

[Aaron Liu]

it looks like essentially the same problem

[Kenny Lau]

I wanted to say "we should change norm_cast to call norm_num to prove that the denom is not zero", but norm_cast is in core unfortunately and we can't change core

[Kenny Lau]

I see

[Alex Meiburg]

In particular it looks like #mathlib4 > exact_mod_cast and rationals @ 💬 . Thanks for pointer

[Alex Meiburg]

Well, sounds like not a very solved problem then I guess. Too bad

[Aaron Liu]

I would make an example without mathlib but I don't know of any scalar towers in core

[Kenny Lau]

N N Z?

[Aaron Liu]

N N doesn't give you a cast

[Alex Meiburg]

There's N -> Z -> Fin x

[Aaron Liu]

Z -> Fin also doesn't give you a cast

[Alex Meiburg]

What do you mean? docs#Fin.IntCast.instIntCast

[Aaron Liu]

is Z -> Fin something that norm_cast will know about?

[Aaron Liu]

oh this might work

[Yaël Dillies]

This instance to fin is deprecated as of recently

[Aaron Liu]

maybe I have misunderstood how norm_cast works

[Aaron Liu]

I feel like all my examples are reflecting a poor support for Fin rather than a problem with norm_cast

[Jovan Gerbscheid]

Here's a solution:

import Mathlib

variable {α} [DivisionRing α] [CharZero α] {p q : ℚ}

@[norm_cast]
theorem Nat.cast_div' (n m : Nat) : (n / m : α) = (Rat.divInt n m : α) := by
  simp [Rat.divInt_eq_div]

@[norm_cast] -- not needed for the below example
theorem Int.cast_div' (n m : Int) : (n / m : α) = (Rat.divInt n m : α) := by
  simp [Rat.divInt_eq_div]

example (x : ℝ) (hx : x = 3 / 5) : ((3 / 5 : ℚ) : ℂ) = x := by
  rw [hx]
  norm_cast

[Kim Morrison]

Kenny Lau said:

but norm_cast is in core unfortunately and we can't change core

A PR, making sure to branch off nightly-with-mathlib and to verify that Mathlib still builds with whatever changes you make (adjusting the Mathlib lean-pr-testing-NNNN branch as needed), is very welcome.

[Kim Morrison]

It would have to be a change that allows a customisable discharger, of course, because norm_num is in Mathlib.

[Jovan Gerbscheid]

I've made an attempt in #28355 to fix this, but unfortunately the new @[norm_cast] lemma overshadows cast_div_charZero. And I can't solve this non-confluency by adding the extra lemma, because that lemma doesn't work as a @[norm_cast] lemma in the norm_cast direction.

I don't think a fix here should involve norm_num, because we want it to also work for arbitrary natural numbers, e.g.

import Mathlib

example (x : ℝ) (a b : Nat) (hx : x = a / b) : ((a / b : ℚ) : ℂ) = x := by
  rw [hx]
  norm_cast
  sorry

[Alex Meiburg]

It might sound crazy, but I think the answer might be to do some un-squashing before the elim. You can unsquash it into Complex.ofReal on both sides, then strip that in the elim phase, and things look better.

[Eric Wieser]

As an aside, I think you're generally in trouble as soon as you step outside of the $\mathbb{N} < \mathbb{Z} < \mathbb{Q} < \mathbb{R} < \mathbb{C}$ chain (eg to NNReal or NNRat)

[Eric Wieser]

From what I remember, the norm_cast algorithm only makes sense when the type involved in any given expression are totally ordered

[Alex Meiburg]

I was working with real interval arithmetic (and don't really care about ordering, just calculation)

[Jovan Gerbscheid]

Alex Meiburg said:

You can unsquash it into Complex.ofReal on both sides, then strip that in the elim phase, and things look better.

Isn't that exactly what norm_cast is doing?

[Jovan Gerbscheid]

Eric Wieser said:

As an aside, I think you're generally in trouble as soon as you step outside of the $\mathbb{N} < \mathbb{Z} < \mathbb{Q} < \mathbb{R} < \mathbb{C}$ chain (eg to NNReal or NNRat)

Indeed, I would have expected the following to work:

import Mathlib
open NNReal NNRat
example (x : ℝ≥0) (a : ℚ≥0) (h : (x : ℝ) = a) : x = a := by
  exact_mod_cast h

[Jovan Gerbscheid]

The same problem appears for ⁻¹, so I think that makes it easier to understand:

import Mathlib

example (a b : ℤ) (h : (a : ℚ)⁻¹ = b) : ((a : ℚ) : ℝ)⁻¹ = b := by
  exact_mod_cast h -- succeeds

example (a b : ℤ) (h : (a : ℚ)⁻¹ = b) : (a : ℝ)⁻¹ = b := by
  exact_mod_cast h -- fails

The underlying problem is that ((a : ℤ) : ℝ)⁻¹ should be un-squashed to (((a : ℤ) : ℚ) : ℝ)⁻¹. This could be done with a simproc.

[Alex Meiburg]

Jovan Gerbscheid said:

Isn't that exactly what norm_cast is doing?

Oh, this is the "heuristic splitting procedure" I guess? It's described in the paper but not anywhere in the Lean docs, afaict. (This is also the only place I've seen that states that move lemmas are applied right-to-left!)

[Alex Meiburg]

In that case I don't understand why the original above didn't work.

[Jovan Gerbscheid]

The splitting heuristic is used when an operator has 2 arguments, and if it can un-squash one of the arguments to match the other one. In this case, = has two arguments, and it can un-squash one of them so that both sides have the same cast as the head.

But in the problematic case, the casts are hidden inside a ⁻¹, so it doesn't know that it should un-squash them...