Simp doesn't find `Classical.em`

Stream: new members

[Niklas Halonen]

Hi all!

While trying to prove an easy lemma about indexed unions, I tried simplify a subexpression like p a ∨ ¬ p a but it didn't get rid of it (by rewriting it to True). What could be wrong? Here's my exact code:

import Mathlib.Tactic

open Set

lemma iUnion_split {ι : Type*} {part : Set ι} {f : ι → Set X} : ⋃ i, f i = (⋃ i ∈ part, f i) ∪ (⋃ i ∈ partᶜ, f i) := by
  ext x
  simp only [mem_iUnion, mem_union, mem_compl_iff, ← exists_or, exists_prop, ← or_and_right]
  -- ⊢ (∃ i, x ∈ f i) ↔ ∃ x_1, (x_1 ∈ part ∨ x_1 ∉ part) ∧ x ∈ f x_1

  -- simp -- doesn't work
  -- simp_all -- doesn't work
  -- tauto -- doesn't work
  -- aesop -- doesn't work
  simp [em] -- works

It seems like the simplifier doesn't have a lemma for situations like the above x_1 ∈ part ∨ x_1 ∉ part. Should docs#Classical.em be marked as @[simp]?

PS. Did not find a lemma from mathlib for generalizing the above lemma.

[Luigi Massacci]

I'm not sure why you would expect that to be a simp lemma, that is arguably not what simp is for

[Niklas Halonen]

Oh, maybe I have misunderstood what simp is for...

But even on the website you linked, there is a simp lemma eq_self which does b = b ==> True, which is not too different what I'm looking for, which is A ∨ ¬ A ==> True. Is there a clear distinction between the two which I'm not seeing?

I tried adding it to the simplifier like follows:

@[simp]
lemma em_iff_true {A : Prop} : A ∨ ¬ A ↔ True := iff_true_intro <| em A

and then simp found it immediately in my iUnion_split example! So the simplifier does appear to work better for my example, but of course it might have other unforeseen consequences.

I wonder if I should just make a PR for this...

[Luigi Massacci]

Note that you could have also proven your goal like this:

lemma iUnion_split {ι : Type*} {A : Set X} {part : Set ι} {f : ι → Set X} : ⋃ i, f i = (⋃ i ∈ part, f i) ∪ (⋃ i ∈ partᶜ, f i) := by
  rw [← Set.biUnion_union]
  simp? -- see what the simp lemmas look like

[Niklas Halonen]

Cool, I didn't see that.

Is the point here that simp must always be constructive? I tried with some De Morgan's laws and couldn't get simp to solve those, so I guess that's the case then. Never knew that before... I wonder if this is documented anywhere?

[Aaron Liu]

simp has docs#Classical.not_not, so it's not constructive

[Niklas Halonen]

Oh good point!

But now I'm very confused :sweat_smile: what is the reason for not having em or similar to simplify my goal in my initial example? Is it not what the simplifier is for, as suggested @Luigi Massacci ?

[Riccardo Brasca]

What's the difference between em and any other true statement?

[Riccardo Brasca]

I mean, following the same logic any theorem should be tagged by simp.

[Aaron Liu]

But docs#sup_compl_eq_top and docs#Bool.or_not_self are both @[simp]

[Edward van de Meent]

theorems with asumptions typically don't get tagged simp

[Edward van de Meent]

the only exceptions i can think of are implies_true and maybe False.elim

[Kevin Buzzard]

Oh aren't there many exceptions to that rule? Simp can quite happily use theorems with assumptions if my understanding is correct