rewriting an assumption using it

Stream: general

[Patrick Massot]

Nice little weirdness from #9934: you can't rewrite at an assumption using that assumption. Stupid example:

example (a b : ℕ) (h : a = b) : true :=
begin
  rw h at h, -- does nothing
  have h' := h,
  rw h' at h, -- works
  trivial
end

slightly more realistic example:

example (a b c : ℕ) (h : a = b) (h' : b = c): c = b :=
begin
  rw h.trans h' at h, -- does nothing
  have h'' := h.trans h',
  rw h'' at h, -- works
  exact h
end

[Patrick Massot]

The actual example where this is disappointing is https://github.com/leanprover-community/mathlib/pull/9934/files#diff-007a1719e43583bdb2859622b2bbb8c1077df80b48dd26e0bf52fdd4041f8b53R335-R339

[Patrick Massot]

@Anatole Dedecker You can replace this proof by show tendsto f (𝓝 a) (𝓝 $ f a), by rwa eq_of_tendsto_nhds h to make it less puzzling.

[Anatole Dedecker]

Yes I was a bit surprised it didn't work, I felt I had already done that lots of time without problem, but I guess not then. Anyway, thanks for the alternative.

[Yaël Dillies]

This is actually a failsafe security of rw. It checks whether the rewritten hypothesis appears in the term you rewrite by.

[Eric Rodriguez]

I just ran into this again, with, for example:

variables (a b c d : ℕ) (hab : a = b) (hbc : b = c) (hcd : c = d)
include hab hbc hcd

example : a = c :=
let this := hbc.trans hcd in
by rwa [←this, ←hab, eq_comm] at hcd

example : a = c :=
begin
  rwa [←hbc.trans hcd, ←hab, eq_comm] at hcd,
  sorry
end

This behaviour seems totally sensible, but that it silently errors (whilst fully breaking the infoview in the rw!) is baffling to me. if as Yaël says, this behaviour is an explicit failsafe, I think an error message should be emitted

[Mario Carneiro]

It is an explicit failsafe, but it is supposed to do nothing

[Mario Carneiro]

it can't just fail because I think that breaks rw at * which applies the rewrite to all the hypotheses

[Mario Carneiro]

and this behavior makes it automagically skip the expressions in the rewrite

[Mario Carneiro]

oh but there is a bug, it's skipping all the rest of the rules instead of just the one that is involved

[Yaël Dillies]

Can't we detect whether a rw did anything or not? If it didn't, then throw a warning.

[Mario Carneiro]

if it fails then it will break tactics that depend on this behavior to apply rw thm to several hypotheses at once

[Mario Carneiro]

there is literally a bit of code that says "if the thm uses the hypothesis then do nothing"

[Yaël Dillies]

"did anything"

[Mario Carneiro]

normally that would be where you put "fail", so this behavior is definitely intentional

[Mario Carneiro]

the part that looks unintentional is that "do nothing" is also skipping the remainder of the list of rules to apply

[Mario Carneiro]

lean#686

[Mario Carneiro]

Yaël Dillies said:

"did anything"

I'm talking about meta-tactics that apply rw in a loop, or to multiple hypotheses. rw itself is written that way

[Eric Rodriguez]

this is a nice bug-fix as on the consumer-end it will probably be very noticeable that it does nothing!