not_nonempty_iff can be annoying as a simp lemma

Stream: mathlib4

[Sam]

I'm a relative newb but I've been playing around with some types/theorems involving Nonempty and have been finding that the simplifier chokes on them a lot because of not_nonempty_iff. It turns Not Nonempty into IsEmpty, then all of the automation that would normally handle inverted props stops working when I have expressions which involve both Nonempty α and ¬ Nonempty α.

My life improved a lot when I worked out that I could do attribute [-simp] not_nonempty_iff. (By the way, https://leanprover.github.io/theorem_proving_in_lean4/tactics.html doesn't mention this and in fact implies that it's impossible. It might be a good idea to change that?)

Perhaps my trick of removing the attribute is the "correct" way to handle this, but I was wondering whether it was worth reconsidering whether not_nonempty_iff should be marked as @[simp]?

I expect it adds value in other situations which outweigh this issue, but I thought I'd raise it just in case.

[Riccardo Brasca]

You can try to remove the simp attribute and see what happens. (You don't need to recompile everything by yourself, just open a PR and CI will do it).

[Yaël Dillies]

What kind of theorems are you proving though? In practice you don't really get \not Nonempty alpha.

[Yaël Dillies]

Also, are you aware that you can make a specific simp call not use a specific lemma? The syntax is simp [-not_nonempty_iff]

[Sam]

Yeah it's quite possible that I'm doing something atypical or silly. I'm playing around with some quite trivial things for learning purposes. One of them is this, i.e. a bundling of types where either they're all nonempty or none of them are.

-- Badly named
structure EquivTypeSet where
  types: Finset (Sort u)
  -- We use Not Nonempty instead of IsEmpty,
  -- because tactics have a hard type jumping between the two.
  pred: (∀ α ∈ types, Nonempty α) ∨ (∀ α ∈ types, Not (Nonempty α))

A lot of my basic theorems on this then involve handling the empty and nonempty cases. Perhaps I should instead just look for a different way of defining it.

[Sam]

I'm aware of simp [-not_nonempty_iff], but it's a little annoying to have to do that every time I want to quickly try simp and see where it gets me, and when using hint. Obviously nothing about this is a showstopper - it's just a small usability thing.

[Sam]

Riccardo Brasca said:

You can try to remove the simp attribute and see what happens. (You don't need to recompile everything by yourself, just open a PR and CI will do it).

Yeah - I just thought it best to ask less formally here before bothering the repo with my potentially silly ideas!

[Josha Dekker]

Wouldn’t it be easier to use IsEmpty in your definition? There should be a result linking that directly to the negation of Nonempty, and I think we have much more API for IsEmpty

[Sam]

Oh - like have them both use IsEmpty, i.e. switch the Nonempty to Not Nonempty? I haven't tried that - it could be an option!

But having them both be the same is nice. For example the tauto here breaks if one is Nonempty and the other is IsEmpty. When they were opposites I was finding that I was rewriting them to be the same again and again.

  theorem exists_nonempty {ets: EquivTypeSet} (h: ∃ α ∈ ets, Nonempty α) : ∀ β ∈ ets, Nonempty β := by
    cases ets.pred
    assumption
    tauto

[Sam]

Oops - that example relies on this instance to work

  instance : Membership (Sort u) EquivTypeSet where
    mem (x) (ets) := x ∈ ets.types

[Josha Dekker]

Yeah, it is a trade-off. We added Uncountable recently because carrying Not Countable was not convenient for some use-cases, I think it came at the cost of having to unfold the definition sometimes.

[Eric Wieser]

Can you elaborate on why pred : (∀ α ∈ types, Nonempty α) ∨ (∀ α ∈ types, IsEmpty α) doesn't work for you?

[Sam]

@Eric Wieser Sure - here's a self contained repro of the exists_nonempty issue mentioned above.

-- This is needed to make aesop work on the easier Not Nonempty version
-- - Without it, aesop starts by simping into the harder version, then gets stuck
attribute [-simp] not_nonempty_iff

example
  (types: Finset (Sort u))
  (pred: (∀ α ∈ types, Nonempty α) ∨ (∀ α ∈ types, Not (Nonempty α)))
  -- (pred: (∀ α ∈ types, Nonempty α) ∨ (∀ α ∈ types, IsEmpty α))
  (h: ∃ α ∈ types, Nonempty α)
  : ∀ β ∈ types, Nonempty β := by
  cases pred
  assumption
  tauto -- or aesop

We cases the Or, show the first case by assumption, and show the second case is a contradiction by h.

This latter step can be tackled by tactics like tauto and aesop in this form, but if we change it to IsEmpty they don't get it because they're not spotting the identities involving negated predicates.

Of course I could use IsEmpty in the definition and just add a rw step into the proof, but it felt messy to keep doing that and this felt cleaner to my inexperienced eye.

The issue with the simp lemma is that it aggressively tries to put things into the form which blocks tauto. Which again is perfectly workaroundable, but feels annoying/unclean.

[Sam]

Actually it's worse than that! I just realised. Without doing attribute [-simp] not_nonempty_iff, aesop actually fails on both versions - including the Not Nonempty one!

I assume it's aggressively applying simp internally and tripping itself up. tauto still works.

[Josha Dekker]

Doing it with IsEmpty gives the following proof, which is slightly longer:

 example
    (types: Finset (Sort u))
    (pred: (∀ α ∈ types, Nonempty α) ∨ (∀ α ∈ types, IsEmpty α))
    (h: ∃ α ∈ types, Nonempty α)
    : ∀ β ∈ types, Nonempty β := by
  rcases pred
  · assumption
  · rcases h with ⟨_,_,hc⟩
    rw [← not_isEmpty_iff] at hc
    tauto

[Sam]

Yeah that's what I did first, then I changed the definition to avoid the rw because it felt messy to have to repeat that step in multiple theorems. I'm very open to the fact that may have been a silly deviation from best practice!? As a relatively inexperienced user I currently have a strong bias towards putting things in forms that make it as easy as possible for automation to do all the work for me so I don't have to mess about with finding/remembering the right theorems in the library.

I'm definitely bikeshedding between two perfectly good ways of doing it here.

[Josha Dekker]

So here is my motivation for using IsEmpty; which is the same reason why we introduced Uncountable for Not Countable a while back:
in the following, the thing to be proven is not material, it is about the instance implicit terms. For the former, we get an error, for the latter, we don't:

import Mathlib
example (α : Set X) [Not (Countable α)] : Prop := X = X
example (α : Set X) [Uncountable α] : Prop := X = X

[Josha Dekker]

same for your Not Nonempty:

import Mathlib
example (α : Set X) [Not (Nonempty α)] : Prop := X = X
example (α : Set X) [IsEmpty α] : Prop := X = X

[Josha Dekker]

I agree that you have to use rw a bit more, but the fact that you get access to this way of using instance implicit terms seems worthwhile to me.

[Sam]

That makes total sense!

However the thing that felt weird to me is that simp thinks the simplest form of the expression (Nonempty α) ∨ ¬(Nonempty α) is (Nonempty α) ∨ (IsEmpty α). That hides the simple fact that one is a clear opposite of the other, and blocks reasoning by other tactics. The fact that it fully blocks aesop from working in this case seems quite bad?

I see the clear value of IsEmpty existing - it's just not (yet) obvious to me why not_nonempty_iff should be a default simp lemma. But perhaps it's useful more often than it hinders!

[Josha Dekker]

That is a very good question, I don't know what the answer is to that

[Sam]

I wonder if adding coes between them might occasionally be helpful? But I don't think that addresses the issue with things like aesop, so it's probably a sidetrack. (Edit: Tried it, can confirm it doesn't help.)

I sort of wish there were a way to modify the "matcher" (whatever Lean calls that) to treat them as truly identical for the purposes of tactic automation - but I don't think that exists!?

[Sam]

My (humble newbie) assertion would be that any time you have a theorem involving both Nonempty and IsEmpty, the simplest form is to pick one or the other and stick with it. Having both side by side obscures the logic and blocks automation.

The current behaviour of having not_nonempty_iff and not_isEmpty_iff be simp lemmas means the simplifier actively works against this. If you put them in the same form, it splits them back up again and kills aesop.

It looks like there are two ways this could be addressed:

1. Remove @[simp] from both lemmas and let the user choose how they want to handle this. The simplifier will no longer work against you when you put them both in the same form, but it won't help you when you only have one, either.
2. Pick one form to be canonical, and have the simplifier move everything in that direction. The other form would be reserved mainly for use in type class inference. I think this would have the best automation results, but would occasionally be slightly ugly when dealing with Not everywhere. (This is what I've done locally in my tiny project and it feels nice so far.)

I assume the same would go for Countable and Uncountable.

Thoughts? I really don't know the bigger picture here.

[Sébastien Gouëzel]

We have learnt after a lot of experiments that it's better to have Countable and Uncountable instead of Countable and ¬ Countable, and a simp lemma converting ¬ Countable to Uncountable. In most cases, you have one assumption or the other one, but not the two of them together, and having one definite name to speak about it enables dot notation and typeclass resolution. The situation you're considering in your application is quite specific and a little bit artificial, and therefore probably a little bit misleading as to what works best most of the time. Of course, no design choice is perfect in all situations!

[Sébastien Gouëzel]

Note that, in concrete situations, lemmas like docs#isEmpty_or_nonempty make it possible to discuss separately the case where a type is empty or nonempty without encountering a single negation.

[Sam]

Right - that makes total sense @Sébastien Gouëzel! I'm very happy to believe that the inconvenience in this case is outweighed by good reasons in others, and that the situation I'm in is simply the low priority outlier!