Governing philosophy/guidelines about what to include?

Stream: mathlib4

[Kent Van Vels]

I am interested to know if I would be welcome to submit a few (almost trivial) propositions to Mathlib.

As an exercise, I tried to find as many propositions equivalent to $A \subseteq B$. I came up with ten of them. Some of these are in Mathlib, but most aren't. I have written and proved the equivalent theorems in the context of a BooleanAlgebra.

Here is what I mean:

import Mathlib.Order.BooleanAlgebra
import Mathlib.Data.Set.Basic

variable {X: Type*}

section boolalg
variable [BooleanAlgebra X]

--already in mathlib
theorem my_sdiff_eq_bot_iff (A B : X) : A \ B = ⊥ ↔ A ≤ B :=
  sdiff_eq_bot_iff

theorem my_sdiff_le_bot_iff (A B : X) : A \ B ≤ ⊥ ↔ A ≤ B := by
  simp only [le_bot_iff, sdiff_eq_bot_iff]

@[simp]
theorem my_inf_compl_eq_bot_iff (A B : X) : A ⊓ Bᶜ = ⊥ ↔ A ≤ B := by
  rw [←sdiff_eq]
  exact sdiff_eq_bot_iff

--no need for simp
theorem my_inf_compl_le_bot_iff (A B : X) : A ⊓ Bᶜ ≤ ⊥ ↔ A ≤ B := by
  simp only [le_bot_iff, my_inf_compl_eq_bot_iff]

@[simp]
theorem my_compl_inf_eq_bot_iff (A B : X) : Aᶜ ⊓ B = ⊥ ↔ B ≤ A := by
  rw [inf_comm]
  exact my_inf_compl_eq_bot_iff B A

theorem compl_inf_le_bot_iff (A B : X) : Aᶜ ⊓ B ≤ ⊥ ↔ B ≤ A := by
  simp only [le_bot_iff, my_compl_inf_eq_bot_iff]

@[simp]
theorem my_sup_compl_eq_top_iff (A B : X) : A ⊔ Bᶜ = ⊤ ↔ B ≤ A:= by
  rw [←compl_inj_iff]
  simp only [compl_sup, compl_compl, compl_top, my_compl_inf_eq_bot_iff]

@[simp]
theorem my_compl_sup_eq_top_iff (A B : X) : Aᶜ ⊔ B = ⊤ ↔ A ≤ B := by
  rw [sup_comm]
  exact my_sup_compl_eq_top_iff B A

theorem my_top_le_sup_compl_iff (A B : X) : ⊤ ≤ A ⊔ Bᶜ ↔ B ≤ A := by
  simp only [top_le_iff, my_sup_compl_eq_top_iff]

theorem my_top_le_compl_sup_iff (A B : X) : ⊤ ≤ Aᶜ ⊔ B ↔ A ≤ B := by
  simp only [top_le_iff, my_compl_sup_eq_top_iff]

end boolalg

--already in mathlib
@[simp]
theorem diff_eq_empty (A B : Set X) : A \ B = ∅ ↔ A ⊆ B := by
  exact Set.diff_eq_empty


theorem diff_subset_empty (A B : Set X) : A \ B ⊆ ∅ ↔ A ⊆ B := by
  simp only [Set.subset_empty_iff, Set.diff_eq_empty]

@[simp]
theorem union_compl_eq_empty_iff (A B : Set X) : A ∩ Bᶜ = ∅ ↔ A ⊆ B :=
  my_inf_compl_eq_bot_iff A B

theorem union_compl_subset_empty_iff (A B : Set X) : A ∩ Bᶜ ⊆ ∅ ↔ A ⊆ B := by
  simp only [Set.subset_empty_iff, union_compl_eq_empty_iff]

@[simp]
theorem compl_union_eq_emtpy_iff (A B : Set X) : Aᶜ ∩ B = ∅ ↔ B ⊆ A :=
  my_compl_inf_eq_bot_iff A B

theorem compl_union_subset_empty_iff (A B : Set X) : Aᶜ ∩ B ⊆ ∅ ↔ B ⊆ A := by
  simp only [Set.subset_empty_iff, compl_union_eq_emtpy_iff]

@[simp]
theorem union_compl_eq_univ_iff(A B : Set X) : A ∪ Bᶜ = Set.univ ↔ B ⊆ A :=
  my_sup_compl_eq_top_iff A B

@[simp]
theorem compl_union_eq_univ_iff (A B : Set X) : Aᶜ ∪ B = Set.univ ↔ A ⊆ B :=
  my_compl_sup_eq_top_iff A B

theorem univ_subset_union_compl_iff (A B : Set X) : Set.univ ⊆ A ∪ Bᶜ ↔ B ⊆ A := by
  simp only [Set.univ_subset_iff, union_compl_eq_univ_iff]

theorem univ_subset_compl_union_iff (A B : Set X) : Set.univ ⊆ Aᶜ ∪ B ↔ A ⊆ B := by
  simp only [Set.univ_subset_iff, compl_union_eq_univ_iff]

Any recommendations are appreciated. I, of course, would remove the "my_" prefix on the boolean algebra theorems. And I would change everything I could into a "term-wise" proof, instead of a tactic based proof.

[Kent Van Vels]

I also had $B^\mathrm{C} \subseteq A^\mathrm{C}$, but if I remember correctly that is in mathlib in both places.

[Edward van de Meent]

I don't think there is any need for changing these to be term-wise? I'd say these proofs are all short enough...

[Kent Van Vels]

Is there an issue with term-wise proofs being faster in some way? I think I remember reading that.

[Edward van de Meent]

They are, but for these proofs (particularly when they use simp only rather than plain simp) I don't think there is such a large difference

[Kent Van Vels]

Is simp only about as slow (fast) as simp with?

[Kyle Miller]

I think "simp with" is a typo for "simp only", unless there's some new tactic I don't know about.

[Kyle Miller]

I'd say, unless you can tell that the tactic proof is slow, don't worry about creating a term proof.

There's not even a guarantee that term proofs are faster than tactic proofs.

[Kyle Miller]

There's guidance to not use simp only if simp will do, if the simp closes the goal (and if simp isn't slow). This is for reasons of maintainability.

[Yaël Dillies]

(You'll be forgiven for being unaware of the guidance. It was formally recording in the contributing guidelines only today)

[Eric Wieser]

Regarding the lemmas with expressions of the form _ ⊓ _ ≤ ⊥ or _ ⊓ _ = ⊥; Mathlib prefers to spell these as Disjoint _ _, which cuts down on the number of ways to spell the same thing

[Eric Wieser]

Similarly for _ ⊔ _ and ⊤ as docs#Codisjoint

[Kent Van Vels]

@Eric Wieser, please check my understanding.

You are saying that we can use disjoint in weaker structure (A type with a partial order imposed on it and not necessarily something with inf and sup defined (a lattice structure)), so we want the lemmas defined on a partial Order and not necessarily on a lattice structure. Or at least have the more specialized theorems inherit from the more-general ones.

[Eric Wieser]

I think my comments is more that it's better to pick one spelling (the most general) and write $n$ lemmas translating it to equivalent concepts, than to write all $\frac{n(n+1)}{2}$ lemmas translating every concept to every other

[Kent Van Vels]

Ah, Ok. That makes sense.

Are there guidelines on what lemmata belong in mathlib? I would be happy to contribute this, but I don't want to waste my or anyone else's time if these aren't useful.