rw on sub expressions?

Stream: new members

[Martin C. Martin]

Why can't rw find an instance of P ∧ Q here?

example : ∃ (n : ℕ ), 10 < n ∧ n < 20 :=
begin
  rw and_comm,
  sorry
end

How can I swap the order of the conjuncts in the goal?

[Pedro Sánchez Terraf]

Might be related to the fact that rw finds it difficult to work under binders

[Martin C. Martin]

Interesting, thanks! The suggestion in that thread, using simp_rw, doesn't work for me. Is there a way to swap the order of the conjuncts?

[Pedro Sánchez Terraf]

(I'm also a new member). For fine tuning, you have the conv mode.

[Pedro Sánchez Terraf]

I also don't know why simp_rw won't work. Here's one solution (surely not an optimal one), using the approach above.

example : ∃ (n : ℕ ), 10 < n ∧ n < 20 :=
begin
  conv
  begin
    congr,
    funext,
    rw and_comm,
  end,
  sorry
end

[Riccardo Brasca]

You can also try simp_rw.

[Michael Stoll]

rwdoes not work on expressions that contain bound variables. simp_rw does, but applies lemmas repeatedly and so gets trapped in a loop when you give it and_comm. simp_rw [and_comm (10 < _)] does work, since the lemma applies only once with a left argument to and that matches 10 < _.

[Gareth Ma]

Or as Kevin Buzzard taught me, simp_rw uses simp only under the hood, and for the latter there is a context (ctx) optional parameter. So you can do this:

example : ∃ (n : ℕ), 10 < n ∧ n < 20 :=
begin
  -- rw and_comm,
  -- simp_rw [and_comm],
  simp only [and_comm _] { single_pass := tt },
end

[Gareth Ma]

You need this when specifying the arguments doesn't work, which happened to me a while ago