inconsistency in matching

Stream: mathlib4

[Ralf Stephan]

Can someone explain please why the first example works but the second does not?

import Mathlib
open ZMod Nat

example (a p : ℕ) (h : p ∣ a) : a = (0 : ZMod p) := by
  apply (natCast_zmod_eq_zero_iff_dvd a p).mpr h

example  (a p : ℕ) (h : p ∣ a + 1) : a + 1 = (0 : ZMod p) := by
  apply (natCast_zmod_eq_zero_iff_dvd (a + 1) p).mpr h

[Ralf Stephan]

I needed norm_cast. Thanks.

[Ruben Van de Velde]

Probably one happens to be true by definition and the other doesn't

[Eric Wieser]

The second one is fine if you write

example  (a p : ℕ) (h : p ∣ a + 1) : ↑(a + 1) = (0 : ZMod p) := by
  apply (natCast_zmod_eq_zero_iff_dvd (a + 1) p).mpr h

[Ralf Stephan]

The original does also not work with exact. I would have expected exact to apply norm_cast.

[Damiano Testa]

There is exact_mod_cast for that.

[Mario Carneiro]

I wonder if we should deprecate exact_mod_cast since it's just exact mod_cast

[Kevin Buzzard]

By the same argument we should deprecate simpa because "it's just exact simp" right?

[Kevin Buzzard]

@Ralf Stephan exact h succeeds when h is definitionally equal to the goal, exact isn't applying any cast tactics or anything, it's just applying the algorithm for rfl.

[Eric Wieser]

Kevin Buzzard said:

By the same argument we should deprecate simpa because "it's just exact simp" right?

Surely simp isn't legal in term mode?

[Mario Carneiro]

it's also the same number of characters and even the same words in the same order

[Mario Carneiro]

also simpa isn't just exact simp, it's simp at h; simp; exact h

[Mario Carneiro]

give or take some edge cases

[Mario Carneiro]

when I say it is just exact mod_cast I mean it literally; compare with simpa

[Eric Wieser]

They're not literally the same, right? Thanks to the extra parens, exact_mod_cast . is legal, but exact mod_cast . isn't.

[Ralf Stephan]

It would be helpful if hint would find it.

[Mario Carneiro]

Eric Wieser said:

They're not literally the same, right? Thanks to the extra parens, exact_mod_cast . is legal, but exact mod_cast . isn't.

no, . is extra magic, it applies before macro expansion so it doesn't work like that

[Mario Carneiro]

the extra parens presumably do something but as far as I know (e : _) is a no-op

[Eric Wieser]

Mario Carneiro said:

no, . is extra magic, it applies before macro expansion so it doesn't work like that

I agree it shouldn't work like that, but it does:

import Mathlib

example : ℕ → ℕ := by exact mod_cast · -- fails
example : ℕ → ℕ := by exact_mod_cast · -- ok

[Eric Wieser]

by use · is legal for the same reason, even though by exact · isn't