Zulip Chat Archive

Stream: general

Topic: rw under lambda


view this post on Zulip Reid Barton (May 04 2018 at 18:33):

rw refuses to perform rewrites inside a lambda, as far as I can tell. Is there a convenient way to do so?
For example, frequently my goal is of the form ∃ x, P x ∧ Q x and I would like to rewrite it to ∃ x, P x ∧ Q' x (where I know Q x ↔ Q' x).

view this post on Zulip Simon Hudon (May 04 2018 at 18:35):

use simp instead of rw if you want to rewrite under lambda. If you don't want simp to use default simp rules, you can do simp only [my_rule]

view this post on Zulip Reid Barton (May 04 2018 at 18:39):

Oops, I tried simp only, but I mixed up .symm and .mpr so it didn't appear to work. Thanks!

view this post on Zulip Patrick Massot (May 04 2018 at 19:19):

See also https://github.com/leanprover/mathlib/blob/master/docs/extras/conv.md

view this post on Zulip Reid Barton (May 04 2018 at 19:59):

I couldn't work out how to do this with conv:

example (h :  a b, a + b = 0) :  a b, b + a = 0 :=
begin
  conv begin
    -- use rw add_comm somehow
  end,
  exact h
end

view this post on Zulip Reid Barton (May 04 2018 at 20:00):

I tried congr, funext, congr but I got an error that I didn't understand on the second congr

view this post on Zulip Simon Hudon (May 04 2018 at 20:05):

try:

example : (∃ a b, a + b = 0) ↔ ∃ a b, b + a = 0 :=
by conv in (_ + _) begin
  rw add_comm,
end

view this post on Zulip Reid Barton (May 04 2018 at 20:13):

ah, interesting

view this post on Zulip Simon Hudon (May 04 2018 at 20:31):

This would also work, btw:

example (h : ( a b, a + b = 0)) :  a b, b + a = 0 :=
begin
  conv in (_ + _)
  { rw add_comm },
  exact h
end

view this post on Zulip Patrick Massot (May 04 2018 at 21:48):

conv in ( _ = _) would also work, but I would be interested in seeing a solution without pattern matching. It seems we lack some navigation tactic (like to_lhs/to_rhs, congr). @Gabriel Ebner @Mario Carneiro any idea?


Last updated: May 11 2021 at 00:31 UTC