## Stream: general

### Topic: rw feature

#### 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?)

#### 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


#### 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]

#### 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.

#### 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?

#### 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 :-)

#### 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

#### 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.

#### 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