simp 1 <= x

Stream: mathlib4

[James Gallicchio]

Is there an intention behind both 0 < x and 1 <= x being simp-normal? It seems a bit awkward to duplicate defeq lemmas like

@[simp] theorem count_pos {a : α} {l : List α} : 0 < count a l ↔ a ∈ l := by
  simp only [count, countp_pos, beq_iff_eq, exists_eq_right]

@[simp] theorem one_le_count_iff_mem {a : α} {l : List α} : 1 ≤ count a l ↔ a ∈ l := count_pos

[James Gallicchio]

(I searched a tiny bit in history for discussion but didn't come across any -- if this is a duplicate thread let me know)

[James Gallicchio]

I guess I'm also curious about ¬x = 0, since I'd expect its simp normal form to also be 0 < x, but it might be an entirely different case since it's not defeq to the other two

[James Gallicchio]

Should I just try marking those lemmas simp and see what the fallout is? :joy:

[Reid Barton]

Certainly $x \ne 0$ vs $0 < x$ has been discussed at length before

[James Gallicchio]

The conclusion here seemed to be that we should prefer Ne 0 xin hypotheses and 0 < x in conclusions (since for arbitrary preorders this gives the strongest statement). But there was no discussion of adding a simp lemma in the general case (since it doesn't hold).

[Reid Barton]

I don't think a simp lemma is likely to be a good idea.

[Reid Barton]

I think adding one right now is definitely a very bad idea

[James Gallicchio]

Definitely. I'm currently figuring out whether to include both of these in Std or just one. Either way both will remain in mathlib for the foreseeable future.

But if we have a (long-term) plan to move to one or the other I'd rather Std just include the "preferred" one

[James Gallicchio]

(And it seems like 0 < x should be the preferred form? Since it's the "strongest" from the view of a preorder?)

[Mario Carneiro]

Given that there is no simp lemma in either direction (for the reasons Reid stated), I would expect to have both versions of that count lemma as simp lemmas.

[Mario Carneiro]

normally simp lemmas exist to get you "out" of the bad form and into the good form so it is not unusual to have simp lemmas from slightly weird representations into a more canonical one

[James Gallicchio]

Hm, okay. So having a simp lemma in any direction for any of these three forms in Std is a bad idea even if we set aside mathlib's conflicting usage?

[James Gallicchio]

I can see that in the case of Ne x 0 since there are many lemmas stated in that form generalized across all types, so if a hypothesis was simplified from Ne x 0 to 0 < x then simp would not find Ne x 0.