RFC: add simp lemmas for quantification over `Fin 0`

[fgdorais]

Proposal

I propose to add the following two theorems to Init.Data.Fin.Lemmas:

@[simp] theorem forall_fin_zero {p : Fin 0 → Prop} : (∀ i, p i) ↔ True := ...

@[simp] theorem exists_fin_zero {p : Fin 0 → Prop} : (∃ i, p i) ↔ False := ...

This file already contains similar theorems forall_fin_one, forall_fin_two, exists_fin_one, exists_fin_two. These four theorems should probably have attribute simp but this is not formally part of this RFC.

It is clear that these two theorems are handy to quickly deal with trivial situations. The necessity for these two theorems hasn't been apparent since Mathlib has IsEmpty.forall_iff and IsEmpty.exists_iff as simp lemmas. Unfortunately, the former triggers on every ∀ _, _ statement, which is a bad idea for simp. This needs to be corrected. The two theorems proposed here will help with that effort by reducing the amount of breakage when the simp attribute is removed from IsEmpty.forall_iff and IsEmpty.exists_iff.

The tentative PR #10627 which implements this has no consequences in Lean. The tentative port in Batteries PR batteries#1433 causes no downstream issues in Batteries nor Mathlib. There seems to be no negative consequences to adding the two proposed theorems.

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

[nomeata]

Out of curiosity, why does exists_fin_zero not need a simp lemma?

[fgdorais]

The proof is simp, so it would be redundant. (In detail, the simp proof boils down to rw [iff_false, not_exists, forall_fin_zero].)

[nomeata]

If it's using iff_false, then that probably means that this only works if the goal is an iff, but not if the existential is somewhere else. Did you test that the changes work as desired?

[fgdorais]

Ah, I see. You think it's better if it triggers on ∃ _ : Fin 0, _ since the current chain triggers on ¬ ∃ _ : Fin 0, _. That makes sense. I doodled a few examples where I can see the difference. I will add that simp. Thanks!

[fgdorais]

Not sure what kind of tests I could add but this looks exactly right:

#discr_tree_simp_key forall_fin_zero -- ∀  (Fin 0)
#discr_tree_simp_key exists_fin_zero -- @Exists (Fin 0) _

[nomeata]

(the last message was in response to a comment asking about the discrimination tree keys for these lemmas. it seems it was deleted by whoever wrote it, so if the conversation reads incomplete this is why)

[digama0]

I didn't delete it... not sure why it's gone now

[nomeata]

Curious, GitHub acting up then.

[TwoFX]

RFC approved.