simp_rw weirdness

Stream: general

[Kevin Buzzard]

A student just came to me with the following question, which I'm completely bamboozled by:

import tactic
import data.real.basic

example {a : ℕ → ℝ} {t : ℝ} (ha : ∀ (ε : ℝ), 0 < ε →
  (∃ (B : ℕ), ∀ (n : ℕ), B ≤ n → |a n - t| < ε)) :
  ∀ (ε : ℝ), 0 < ε → (∃ (B : ℕ), ∀ (n : ℕ), B ≤ n → |t - a n| < ε) :=
begin
  -- simp_rw [abs_sub_comm], -- ??
  -- convert ha,
  simp_rw abs_sub_comm at ha, -- ??
  exact ha,
end

They can't use rw abs_sub_comm on either the goal or ha, presumably because it's under a binder. But why does simp_rw only work on ha and not on the goal? When applied to the goal you get the error simplify tactic failed to simplify despite everything looking completely formally the same to me.

Probably unrelated: it would be nice if convert ha using 37 turned the goal into |a n - t| = |t - a n| but in practice it makes essentially no progress. I'm also slightly surprised by this...

[Damiano Testa]

This does not answer much, but the very verbose congrm (∀ ε : ℝ, 0 < ε → ∃ B : ℕ, ∀ n : ℕ, B ≤ n → (_ < ε)) does what convert ha alone should have done:

example {a : ℕ → ℝ} {t : ℝ} (ha : ∀ (ε : ℝ), 0 < ε →
  (∃ (B : ℕ), ∀ (n : ℕ), B ≤ n → |a n - t| < ε)) :
  ∀ (ε : ℝ), 0 < ε → (∃ (B : ℕ), ∀ (n : ℕ), B ≤ n → |t - a n| < ε) :=
begin
  convert ha,
  congrm (∀ ε : ℝ, 0 < ε → ∃ B : ℕ, ∀ n : ℕ, B ≤ n → (_ < ε)),
  exact abs_sub_comm _ _,
end

[Damiano Testa]

Maybe this is a cunning plot by Patrick to get everyone to use filters.

[Damiano Testa]

Actually, this is some further weirdness: change the order of the subtraction and simp_rw works on the target!

example {a : ℕ → ℝ} {t : ℝ} (ha : ∀ (ε : ℝ), 0 < ε →
  (∃ (B : ℕ), ∀ (n : ℕ), B ≤ n → |a n - t| < ε)) :
  ∀ (ε : ℝ), 0 < ε → (∃ (B : ℕ), ∀ (n : ℕ), B ≤ n → |a n - t| < ε) :=  -- note that this is the same as the hypothesis `ha`
begin
  simp_rw [abs_sub_comm], -- works!
  simp_rw [abs_sub_comm], -- but doing it twice does not!
end

Maybe it is because a is a function and some unification does not work on it, but it does on t?

[Damiano Testa]

here is a shorter failuer:

example {a : ℕ → ℝ} {t : ℝ} (n : ℕ) :
  ∀ (ε : ℝ), |a n - t| < ε :=
begin
  simp_rw [abs_sub_comm], -- works
  simp_rw [abs_sub_comm], -- fails
end

[Kevin Buzzard]

Actually, this is some further weirdness: change the order of the subtraction and simp_rw works on the target!

Yes, in my original post I noted that simp_rw works on ha but not the goal. It's order-dependent. Your example is a clearer version of this.

[Damiano Testa]

Ah, I had read your comment as saying that goals and hypotheses are dealt with differently. They might, but not in this case! :smile:

[Damiano Testa]

I may stop after this, it seems that the order in which the variables are declared (and not their type) matters:

example {a b : ℕ → ℝ} :
  ∀ n : ℕ, |a n + b n| = 0 :=
begin
  simp only [add_comm], --fails
end

example {b a : ℕ → ℝ} :  --  note that `b` is declared first here
  ∀ n : ℕ, |a n + b n| = 0 :=
begin
  simp only [add_comm], -- works
  simp only [add_comm], -- fails
end

[Kevin Buzzard]

Oh nice! What the heck is going on?

[Damiano Testa]

It is really puzzling: whenever I think that it might be something, it turns out that it isn't! Very cool example!

[Damiano Testa]

Btw, it is really simp that has this behaviour: simp_rw works until it calls simp and then simp fails. I updated the last example to use simp only and still displaying the same failure pattern.

Also,

  conv in |_| { rw [add_comm, add_comm, add_comm, add_comm, add_comm, add_comm] },

works, but, depending on the parity of the add_comms, the simp may or may not work! :upside_down:

[Johan Commelin]

Isn't this some sort of loop detection built in to simp?

[Johan Commelin]

Because simp [add_comm] would loop like crazy. But (iirc) it decides to only rewrite when it ends up sorting subexpressions, for some random ordering of subexpressions. And this ordering is probably influenced by de Bruijn indices, which are influenced by the order in which vars are declared.

[Damiano Testa]

Johan, your explanation fits with all that I have been observing!

[Johan Commelin]

And this is a sensible default for simp. But since simp_rw only does a single simp-pass, it would make sense if that loop-detection were disabled.

[Eric Wieser]

simp_rw does not make a single pass through

[Eric Wieser]

simp only [add_comm] { single_pass := tt } does though

[Johan Commelin]

Ooh :bulb: So what does simp_rw do? I guess I don't have an accurate model for how simp_rw is different from simp.

[Eric Wieser]

src#tactic.interactive.simp_rw

[Eric Wieser]

It just calls simp only [lemma] in sequence.

[Johan Commelin]

Yep, I get it now.