rw feature

Stream: general

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

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]

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]

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]

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

[Kevin Buzzard]

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]

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