Rewriting casts appears to have hidden casts

Stream: new members

[Snir Broshi]

import Mathlib
theorem foo : 2 + 3 + 4 + 5 = (9 : ℝ) := by
  nth_rw 2 [← Nat.cast_ofNat]
  sorry

This gives the following error:

Tactic `rewrite` failed: motive is not type correct:
  fun _a ↦ 2 + 3 + 4 + 5 = 9
Error: Application type mismatch: The argument
  Nat.instNeZeroSucc
has type
  NeZero (0 + 1)
but is expected to have type
  NeZero _a
in the application
  @Nat.instAtLeastTwoHAddOfNat _a Nat.instNeZeroSucc

To rewrite the nth number in the theorem I have to use 3n+1 in the nth_rw. Why is that?
It looks like there are some hidden numbers inside, can I reveal them somehow?
This doesn't happen for ℚ, so I thought maybe something in ofNat for reals contains more numbers, but Real.ofCauchy doesn't seem to have any extra numbers in its definition.

[Aaron Liu]

we have file#Tactic/DepRewrite now

[Aaron Liu]

though rw! is a bit broken so I would stick to rewrite!

[Aaron Liu]

other options include simp_rw, simp only, and conv

[Snir Broshi]

Wait what, rw isn't an alias of rewrite?

[Aaron Liu]

Snir said:

To rewrite the nth number in the theorem I have to use 3n+1 in the nth_rw. Why is that?
It looks like there are some hidden numbers inside, can I reveal them somehow?

It's the implicit arguments, try set_option pp.explicit true

[Robin Arnez]

rw is rewrite + try with_reducible rfl

[Robin Arnez]

Yeah, compare:

import Mathlib

set_option pp.all true

/--
info: @OfNat.ofNat.{0} Real (nat_lit 2)
  (@instOfNatAtLeastTwo.{0} Real (nat_lit 2) Real.instNatCast
    (@Nat.instAtLeastTwoHAddOfNat (@OfNat.ofNat.{0} Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))
      (@Nat.instNeZeroSucc (@OfNat.ofNat.{0} Nat (nat_lit 0) (instOfNatNat (nat_lit 0)))))) : Real
-/
#guard_msgs in
#check (2 : ℝ)

/-- info: @OfNat.ofNat.{0} Rat (nat_lit 2) (@Rat.instOfNat (nat_lit 2)) : Rat -/
#guard_msgs in
#check (2 : ℚ)

[Robin Arnez]

Rat has an explicit OfNat instance, Real doesn't

[Robin Arnez]

So it derives it through AtLeastTwo and NeZero

[Robin Arnez]

That's also where the additional ofNats are hidden

[Snir Broshi]

So every real n contains n-1 and n-2? Weird

[Robin Arnez]

Yeah... I would've hoped it would at least only be n - 2, but it seems like the priorities are messed up here

[Aaron Liu]

Snir said:

So every real n contains n-1 and n-2? Weird

yeah but there are reasons, there have also been discussions of changing it to something not so weird

[Robin Arnez]

docs#Nat.instAtLeastTwoHAddOfNat should at least have lower instance priority than docs#Nat.instAtLeastTwo

[Snir Broshi]

pp.all clears things up, thank you!