Zulip Chat Archive

Stream: general

Topic: rw feature


view this post on Zulip Kevin Buzzard (Aug 23 2018 at 09:54):

example (a b c : ) (H : a = b) (H2 : (a = b)  (a = c)) : c = b :=
begin
  rw (H2 H) at H, -- does nothing
  exact H -- fails
end

example (a b c : ) (H : a = b) (H2 : (a = b)  (a = c)) : c = b :=
begin
  have H' := H,
  rw (H2 H') at H, -- works fine
  exact H
end

example (a b c : ) (H : a = b) (H2 : (a = b)  (a = c)) : c = b :=
begin
  have H' := H,
  rw (H2 H) at H', -- works fine
  exact H'
end

Is this a bug, or is it not a good idea to let rewrites affect hypotheses which are used to construct the term being rewritten? (or both?)

view this post on Zulip Kevin Buzzard (Aug 23 2018 at 09:56):

example (a b : ) (H : a = b) : false :=
begin
  rw H at H, -- I would expect H to become b = b...
  sorry
end

view this post on Zulip Kevin Buzzard (Aug 23 2018 at 09:57):

[PS this is not frivolous -- I just attempted to do a rewrite on a term which I had used to explicitly fill in something which type class inference couldn't infer, and it silently failed]

view this post on Zulip Simon Hudon (Aug 23 2018 at 14:11):

I think rw does not rewrite the assumptions themselves because if you have:

h0 : a = b,
h1 : a = c
...

rw h0 at * would transform h0 into b = b and then rw would not be able to rewrite h1.

view this post on Zulip Simon Hudon (Aug 23 2018 at 14:13):

I suspect the developers consciously decided to not let rw rewrite assumptions using themselves as a rule. If the assumptions eventually get reshuffled, the design of rw makes the re-execution of the same proof less surprising. Does simp or dsimp help in your situation?

view this post on Zulip Kevin Buzzard (Aug 23 2018 at 14:14):

I did exactly what I suggested in my original post -- I just introduced a new hypothesis which was by definition the old one :-)

view this post on Zulip Simon Hudon (Aug 23 2018 at 14:20):

Ah ok, I thought it might fit in a more complex situation. So it would rank as "annoying", I assume

view this post on Zulip Kevin Buzzard (Aug 23 2018 at 14:21):

Yeah, I'm helping undergraduates to write code and today has been quite an annoying day for some reason, I've had to introduce several workarounds for things.

view this post on Zulip Simon Hudon (Aug 23 2018 at 14:24):

I think that happens a lot in any programming language: with time, you start instinctively avoiding the pain points and then the newcomers run right into them


Last updated: May 11 2021 at 22:14 UTC