Simp turning `≠` into `¬ =`

Stream: mathlib4

[Kenny Lau]

I'm working on making the projective space ℙ(n; S) and it's taking longer than I thought. One intermediate object involved is MvPolynomial { k // k ≠ i } R, which occurs naturally as the correct thing to consider in the basic open defined by X i ≠ 0.

I haven't PR'ed anything yet, but I can already see that the simp linter will complain a lot about me not turning k ≠ i into ¬ k = i, so I wonder what yall think about this.

[Kenny Lau]

basically i see three pathways:

1. remove that simp lemma (basically impossible, i can see how ¬ a = b is in fact better for the whole context of simp.
2. make a separate type instead of just using { k // k ≠ i } all the time.
3. convert all occurrences of k ≠ i into ¬ k = i, which actually the only reason I haven't done this is artistic

[Kenny Lau]

@Andrew Yang I wonder what you think about this

[Markus Himmel]

(To give some context for this discussion: the FRO is very much aware that this is a pain point and we have decided that we want to make ≠ and ¬ = the same thing, for example by making the former a notation for the latter. It's unclear when we will get to this.)

[Kenny Lau]

Thanks a lot!

[Johan Commelin]

Does that mean we would need special elaborator support for the Ne namespace, so that h.symm still works?

[Markus Himmel]

This is why we haven't done it yet: it's unclear what the best approach is, and it's easy to break things, so careful testing and experiments will be needed before we can pull the trigger.

[Kenny Lau]

Johan Commelin said:

Does that mean we would need special elaborator support for the Ne namespace, so that h.symm still works?

would abbrev work for this?

[Andrew Yang]

It would be nice to consider decoupling namespaces and dot notation anyways, as currently dot notation is sometimes encouraging people to put lemmas in the wrong namespace. But this is probably a way harder design decision to get right.

[Jz Pan]

My 2 cents: make Ne an abbrev, remove @[simp] from ne_eq (this should not break things? since if Ne is an abbrev then rw can pass through it), but keep ne_eq in case that if one want to rewrite ¬ = to ≠ to use results in Ne namespace.

[Aaron Liu]

Jz Pan said:

(this should not break things? since if Ne is an abbrev then rw can pass through it)

I'm pretty sure this is actually not how rw works. In particular if you're rewriting with a statement _ ≠ _ ↔ _ then it will not find anything that not exactly ≠, even if Ne is an abbrev.

[Kenny Lau]

@Jz Pan Indeed, Aaron is correct here. I've made a way to experiment with ideas:

abbrev Ne' {α : Sort u} (x y : α) : Prop := ¬ (x = y)

theorem Ne'.symm {α : Sort u} (x y : α) (h : Ne' x y) : Ne' y x := Ne.symm h

example {α : Sort u} (x y : α) (h : Ne' x y) : Ne' y x := h.symm

set_option trace.Meta.Tactic.simp.rewrite true
example {α : Sort u} (x : α) : Ne' x x := by rw [eq_self] -- fails
example {α : Sort u} (x : α) : Ne' x x := by simp [-ne_eq, eq_self] -- fails
example {α : Sort u} (x : α) : Ne' x x := by simp -- succeeds
-- (these are all `False`, so by "succeed" I mean that it successfully simplifies to `False`)

[Kenny Lau]

(the reason why simp can use ne_eq at all is beyond me)

[Miyahara Kō]

How about this:

import Mathlib.Tactic.TypeStar

theorem Not.esymm {α : Type*} {a b : α} (h : ¬a = b) : ¬b = a :=
  Ne.symm h

example {α : Type*} {a b : α} (h : ¬a = b) : ¬b = a :=
  h.esymm

[Yaël Dillies]

Maybe we could already have today the more general Not.symm {α : Type*} {r : α → α → Prop} [IsSymm α r] {a b : α} (hab : ¬ r a b) : ¬ r b a

[Miyahara Kō]

@Yaël Dillies Thank you. Without realizing it, I was applying Cunningham's Law (the best way to get the right answer on the internet is to post something incorrect).:

import Mathlib.Tactic.TypeStar
import Mathlib.Order.Defs.Unbundled

theorem Not.symm {α : Type*} {r : α → α → Prop} [IsSymm α r] {a b : α} : ¬r a b → ¬r b a :=
  mt _root_.symm

example {α : Type*} {a b : α} (h : ¬a = b) : ¬b = a :=
  h.symm

[Robin Arnez]

The only problem is that @[symm] wouldn't work anymore. But maybe we can simply teach symm in core to treat Not specially.

[Robin Arnez]

And for other Ne lemmas we could perhaps just use a {r : α → α → Prop} [IsRefl α r] (h : ¬r a b) construction

[Edward van de Meent]

Kenny Lau said:

1. remove that simp lemma (basically impossible, i can see how ¬ a = b is in fact better for the whole context of simp.

what if we do this, and add simprocs instead?

[Edward van de Meent]

i.e. a simproc which, when simplifying a ≠ b tries to simplify ¬ a = b, then convert back to a ≠ b wherever possible?

[Edward van de Meent]

(because i suspect that that's basically the only reason why ne_eq is a simp lemma?)

[Johan Commelin]

It should be some sort of simp post-processor.

[Jz Pan]

What about add an instance {α : Type*} {r : α → α → Prop} [IsSymm α r] : IsSymm α fun a b => ¬r a b?

[Edward van de Meent]

Johan Commelin said:

It should be some sort of simp post-processor.

i wonder if it's as simple as adding attribute [-simp, simp↓, simp ←] ne_eq somewhere? spoiler: it's not

[Aaron Liu]

What about stuff like not_not not working on ≠?

[Edward van de Meent]

that's plainly not true, i think?

[Edward van de Meent]

since Ne is reducible

[Edward van de Meent]

i.e.:

example : ¬ a ≠ a := by
  simp only [Classical.not_not]

works

[Aaron Liu]

neat

[Aaron Liu]

TIL Ne is reducible

[Robin Arnez]

Jz Pan schrieb:

What about add an instance {α : Type*} {r : α → α → Prop} [IsSymm α r] : IsSymm α fun a b => ¬r a b?

Doesn't work, since for Not (Eq a b) it expects something of the form r _ _ but only finds one parameter.

[Robin Arnez]

Edward van de Meent schrieb:

what if we do this, and add simprocs instead?

I'd rather prefer if ≠ was just notation because otherwise we'd have some weird special casing for simp and putting things into the Not namespace seems like a reasonable solution.

[Robin Arnez]

Also I'm getting annoyed at the fact that once again, we have Std.Refl / IsRefl, Std.Irrefl / IsIrrefl, Std.Antisymm / IsAntisymm etc. (mathlib + core having the same things with different names!)

[Jz Pan]

Robin Arnez said:

Also I'm getting annoyed at the fact that once again, we have Std.Refl / IsRefl, Std.Irrefl / IsIrrefl, Std.Antisymm / IsAntisymm etc. (mathlib + core having the same things with different names!)

Also Nat.repeat / Nat.iterate

[Alex Meiburg]

Robin Arnez said:

The only problem is that @[symm] wouldn't work anymore. But maybe we can simply teach symm in core to treat Not specially.

I think it would be reasonable to have some behavior like, "if the top level expression has only a single explicit argument (and it doesn't have an applicable @symm itself), then recurse into that argument".

So "Not Iff a b" would become "Not Iff b a", but also e.g. "Set.Infinite (setOf (fun n -> x^n = y))" would become "Set.Infinite (setOf (fun n -> y = x^n))"

[Alex Meiburg]

Because in 99% of cases where symm is used it's some kind of binary connective, and so if that's wrapped in some number of unary operators it's pretty reasonable to call the first binary connective you find the canonical one

[Robin Arnez]

Hmm I'm not sure how I should feel about symm recursing into deep arguments; at that point it becomes more of a commutativity tactic than a symmetry tactic (since it then actually needs symmetry for all a, b instead of just two of the parameters that are provided)

[Robin Arnez]

I mean we certainly don't want Monotone (fun a => a + 1) to turn into Monotone (fun a => 1 + a), do we?

[Robin Arnez]

Just allowing Not would mean supporting "apply mt symm" instead of "apply symm" which is more reasonable I'd think

[Alex Meiburg]

I'm not sure I follow - maybe I've misunderstood the purpose of symm, then, but in my head it is precisely the "commutativity tactic" (that doesn't require me knowing name of the relevant commutativity theorem). Every @symm theorem I can find is of the form f x y -> f y x, and this is clearly enough to construct f x y <-> f y x and then do a simp_rw [the iff version].

[Alex Meiburg]

Robin Arnez said:

I mean we certainly don't want Monotone (fun a => a + 1) to turn into Monotone (fun a => 1 + a), do we?

I agree that would be be pretty surprising. But in my head, I don't think there's anything else I would reasonably expect symm to do on that goal, so if a user wants to do that, I don't _mind_ the behavioral possibility.

[Alex Meiburg]

My feelings on this would certainly change if there's an argument that allowing this will lead to e.g. less readable or less maintainable proofs

[Robin Arnez]

Well my point is mostly that symm is currently more of an apply-like tactic and making it rw or simp-like would require significant changes and I'm not sure that there is enough of a use case to justify such a shift.