exact_mod_cast and rationals

Stream: mathlib4

[Eric Wieser]

Is there a tactic that can solve these "trivial" goals, besides doing the sequence of manual rewrites?

import Mathlib

example {x : ℚ} (h : (x : ℝ) = 1 + 2) : x = 1 + 2 := by
  exact_mod_cast h -- ok

example {x : ℚ} (h : (x : ℝ) = 1 / 2) : x = 1 / 2 := by
  exact_mod_cast h -- fails

example {x : ℚ} (h : (x : ℝ) = 1 + 2 / 3 + 0.5) : x = 1 + 2 / 3 + 0.5 := by
  exact_mod_cast h -- fails

[Heather Macbeth]

In both cases you can do rify; exact h. But it seems like it would be better to teach norm_cast to handle fractions and decimals.

[Floris van Doorn]

I thought norm_cast could already do this, because it can deal with fractions:

import Mathlib.Tactic

example {p q x : ℚ} (h : (x : ℝ) = p / q) : x = p / q := by
  norm_cast at h

So it fails only on fractions with a number as both numerator and denominator.
And indeed:
src#Lean.Elab.Tactic.NormCast.derive
has a preprocessing step for dealing with natural number numerals, but not for rationals/decimals.
(and negative numbers are just negation applied to a natural number, so need no special preprocessing).

[Eric Wieser]

I think it is pretty tricky to teach it about rational numbers, since norm_cast is in core where Rat doesn't exist yet

[Heather Macbeth]

Maybe that's a reason to move norm_cast back to Batteries.

[Eric Wieser]

I was hoping that something like this might work, but it seems to just send norm_cast into an infinite loop:

import Mathlib

/-- Try to pull casts of numeric literals outside division -/
@[norm_cast move]
theorem Rat.cast_natCast_div_natCast [DivisionRing K] [CharZero K] (n d : ℕ) : (n / d : K) =  (n / d : ℚ) := by simp

example {x : ℚ} (h : (x : ℝ) = 2 / 3) : x = 1 + 2 / 3 := by
  norm_cast at h

[Eric Wieser]

Oh, I can make this work!

[Eric Wieser]

@[norm_cast]
theorem Rat.cast_ofNat_div_ofNat [DivisionRing K] [CharZero K] (n d : ℕ) [n.AtLeastTwo] [d.AtLeastTwo]:
    (no_index (OfNat.ofNat n) / no_index (OfNat.ofNat d) : ℚ) =
      ((no_index (OfNat.ofNat n) : ℕ) / (no_index (OfNat.ofNat d) : ℕ) : K)
       := by simp

fixes the example with rationals

[Heather Macbeth]

Can you get OfScientific working too?

[Eric Wieser]

No, because the mechanism to make OfNat work is to insert a Nat.cast

[Eric Wieser]

So to make OfScientific work, we need to insert a Rat.cast (or NNRat.cast if we have a taste for worms)

[Eric Wieser]

Which of course core can't do

[Eric Wieser]

What core could do is handle Rat.cast_ofScientific specially, when it sees it has been tagged norm_cast

[Eric Wieser]

Allowing simprocs to be registered with norm_cast would probably work too