Simp not firing

Stream: general

[Bolton Bailey]

Refactoring padic_norm, I found this. Why does simp fail to fire here? My understanding was that if all the hypotheses for a simp lemma were present in the context, simp should fire.

import number_theory.padics.padic_norm

/-- For `p ≠ 0, p ≠ 1, `padic_val_nat p p` is 1. -/
@[simp] lemma padic_val_nat_self' {p : ℕ} (hp : 1 < p) : padic_val_nat p p = 1 :=
begin
  sorry,
end

@[simp] lemma padic_val_rat_of_nat' (p q : ℕ) : padic_val_rat p q = padic_val_nat p q :=
begin
  sorry,
end

/-- For `p ≠ 0, p ≠ 1, `padic_val_rat p p` is 1. -/
lemma padic_val_rat_self' {p : ℕ} (hp : 1 < p) : padic_val_rat p p = 1 :=
begin
  simp only [padic_val_rat_of_nat'],
  -- simp, --failed to simplify
  rw padic_val_nat_self' hp, -- Why does simp fail to fire this here?
  refl,
end

[Damiano Testa]

If I'm correct, the hypothesis should not simply be in context, but within the simp set. Does adding hp inside the square brackets of simp work?

[Kyle Miller]

Does simp [*, padic_val_rat_of_nat'] work? I think you need to explicitly include the context.

[Kyle Miller]

There seems to be a more serious problem, that padic_val_rat_of_nat' causes simp to seemingly run forever. Is there a loop in the simp set somewhere when you include this?

[Bolton Bailey]

Ok, I see, I didn't realize it was necessary to actually include the context in simp. (The loop is probably because I'm refactoring this now).

[Kyle Miller]

Other than *, another way to get simp to fill in additional hypotheses is to specify a discharger. In this case, tactic.assumption would work:

  simp [padic_val_rat_of_nat'] {discharger := tactic.assumption},

[Kevin Buzzard]

(deleted)