ne.def

Stream: general

[Johan Commelin]

Would it be evil to teach rw about ne.def? I find it quite frustrating that rw fails because I have \ne instead of a \not _ = _ or vice versa.

[Jalex Stark]

I guess to combat the evilness we want a story for how to avoid scope creep that turns rw into simp_rw or something else it's not supposed to be. Maybe something like "we teach it only about 'basic logic synonyms'"?

[Reid Barton]

What's an example where this is an issue? As far as I can tell ne is reducible and rw should already look through reducible things.

[Johan Commelin]

If you have \not n = 0, and you want to rw \l nat.pos_iff_ne_zero, that seems to fail. Let me build a mwe

[Reid Barton]

I guess there are two possible cases: the goal contains a \ne b but you want to rewrite using a lemma that says a = b \iff ...; or the goal contains \not (a = b) but you want to rewrite using a lemma that says a \ne b \iff

[Johan Commelin]

https://leanprover-community.github.io/lean-web-editor/#code=import%20data.nat.basic%0A%0Aexample%20%28n%20%3A%20%E2%84%95%29%20%28h%20%3A%20%C2%AC%20n%20%3D%200%29%20%3A%20n%20%3E%200%20%3A%3D%0Abegin%0A%20%20rw%20%E2%86%90%20nat.pos_iff_ne_zero%20at%20h%2C%0Aend

[Kevin Buzzard]

lemma ne1 (n : ℕ) : n ≠ 0 ↔ true := sorry
lemma ne2 (n : ℕ) : ¬(n = 0) ↔ true := sorry

example (n : ℕ) : n ≠ 0 ↔ false :=
begin
  rw ne2, -- fails
end

example (n : ℕ) : ¬ (n = 0) ↔ false :=
begin
  rw ne1, -- fails
end

They're both failing for me.

[Reid Barton]

I wonder what md := reducible in rewrite_cfg does then

[Reid Barton]

actually even erw fails, and even if you tell it n

[Kevin Buzzard]

Has this always been the case?