bex_and

Stream: Is there code for X?

[Yaël Dillies]

I can't find such a lemma in mathlib. Do you know whether we already have anything close?

@[simp] lemma bex_and {α : Type*} {q : Prop} {p : α → Prop} (A : set α) :
  (∃ a ∈ A, p a ∧ q) ↔ (∃ a ∈ A, p a) ∧ q :=
⟨λ ⟨a, ha, hp, hq⟩, ⟨⟨a, ha, hp⟩, hq⟩, λ ⟨⟨a, ha, hp⟩, hq⟩, ⟨a, ha, hp, hq⟩⟩

[Anne Baanen]

It wouldn't surprise me if we did not have this (or the more general version below). However, simp can prove this:

@[simp] lemma exists_and' {α : Type*} {β : α → Sort*} {q : Prop} {p : α → Prop} :
  (∃ (a : α) (b : β a), p a ∧ q) ↔ (∃ (a : α) (b : β a), p a) ∧ q :=
by squeeze_simp -- Try this: simp only [exists_and_distrib_right]

@[simp] lemma bex_and {α : Type*} {q : Prop} {p : α → Prop} (A : set α) :
  (∃ a ∈ A, p a ∧ q) ↔ (∃ a ∈ A, p a) ∧ q :=
exists_and'

[Anne Baanen]

In fact, it's just two applications of exists_and_distrib_right

[Anne Baanen]

Interestingly though, simp gets stuck on bex_and because it tries exists_prop first, and then you get ∃ a, a ∈ A ∧ (p a ∧ q), to which exists_and_distrib_right doesn't apply.

[Anne Baanen]

Probably Definitely not a good idea, but add the following lemma and bex_and can be proven by simp:

@[simp] lemma and_assoc' {α : Type*} {q : Prop} {p p' : α → Prop} (a : α) :
  p a ∧ (p' a ∧ q) ↔ (p a ∧ p' a) ∧ q := (and_assoc _ _).symm

[Yaël Dillies]

Yeah, I came to the same conclusion. Maybe we can prove exists_and_distrib_right later than exists_prop to let it override?

[Yakov Pechersky]

import tactic.basic

@[simp] lemma bex_and {α : Type*} {q : Prop} {p : α → Prop} (A : set α) :
  (∃ a ∈ A, p a ∧ q) ↔ (∃ a ∈ A, p a) ∧ q :=
by simp [and.comm, and.assoc, and.left_comm]

[Yakov Pechersky]

A poor man's ring for one possible boolean ring

[Yakov Pechersky]

Where the actual simp lemmas are by simp only [and.comm, iff_self, exists_and_distrib_left]

[Yakov Pechersky]

by simp_rw exists_and_distrib_right also works

[Floris van Doorn]

Yaël Dillies said:

Yeah, I came to the same conclusion. Maybe we can prove exists_and_distrib_right later than exists_prop to let it override?

This is also achievable by setting priorities for the simp lemmas.