rw under binders

Stream: general

[Kevin Buzzard]

I was really surprised today in class when I couldn't get this working:

import tactic
import data.real.basic

example (a : ℕ → ℝ) (t : ℝ) :
  ∀ (ε : ℝ), 0 < ε → (∃ (B : ℕ), ∀ (n : ℕ), B ≤ n → |t - a n| < ε) :=
begin
  -- want to change |t - a n| to |a n - t| in the goal
  -- rw abs_sub_comm, -- fails
  -- simp_rw [abs_sub_comm] -- fails
  -- simp only [abs_sub_comm], -- fails
  intros ε hε,
  use 37,
  intros n hn,
  rw abs_sub_comm, -- works now
  sorry,
end

I even tried using conv mode but then I couldn't enter the forall binder (I thought funext would work but it didn't; perhaps that only enters lambdas rather than pi types?). What am I missing? I specifically didn't want to do the intros.

[Yaël Dillies]

example (a : ℕ → ℝ) (t : ℝ) :
  ∀ (ε : ℝ), 0 < ε → (∃ (B : ℕ), ∀ (n : ℕ), B ≤ n → |t - a n| < ε) :=
begin
  simp_rw [abs_sub_comm _ (a _)],
  sorry
end

[Yaël Dillies]

The trick when simp_rw doesn't want to rewrite with a commutativity lemma is to specify its arguments enough for it to not be a commutativity lemma anymore!

[Yaël Dillies]

Placeholders here are crucial, given that they are getting filled with variables local to the lambda we're rewriting in.

[Kevin Buzzard]

Thanks!

[Patrick Johnson]

That wouldn't work if a and t are quantified, but this would:

simp only [abs_sub_comm _] {single_pass := tt}

[Kevin Buzzard]

I see! simp only [abs_sub_comm] doesn't work but simp only [abs_sub_comm _] doesn't end well at all.