From 949feb25a47774f90b8859ee1dcd6ec7d65b66cf Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Mon, 30 Sep 2024 22:38:18 -0700 Subject: [PATCH] chore: move `@[simp]` from `exists_prop'` to `exists_prop` (#5529) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The lemma `exists_const` already handles all real cases of `(∃ _ : α, p) ↔ p` for general types `α`. If there are no `Nonempty` instances and this lemma cannot apply, it seems unlikely that simp could make more progress with `(∃ _ : α, p) ↔ Nonempty α ∧ p`. However, it is still worth simplifying `(∃ _ : p, q)` to `p ∧ q`. Also adds a `Nonempty (Decidable a)` instance, which is used by Mathlib. --- src/Init/Classical.lean | 2 ++ src/Init/PropLemmas.lean | 4 ++-- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/src/Init/Classical.lean b/src/Init/Classical.lean index d05aea8f2a..16db2812f3 100644 --- a/src/Init/Classical.lean +++ b/src/Init/Classical.lean @@ -80,6 +80,8 @@ noncomputable scoped instance (priority := low) propDecidable (a : Prop) : Decid noncomputable def decidableInhabited (a : Prop) : Inhabited (Decidable a) where default := inferInstance +instance (a : Prop) : Nonempty (Decidable a) := ⟨propDecidable a⟩ + noncomputable def typeDecidableEq (α : Sort u) : DecidableEq α := fun _ _ => inferInstance diff --git a/src/Init/PropLemmas.lean b/src/Init/PropLemmas.lean index aa8946f6a4..697eb73e3e 100644 --- a/src/Init/PropLemmas.lean +++ b/src/Init/PropLemmas.lean @@ -352,10 +352,10 @@ theorem not_forall_of_exists_not {p : α → Prop} : (∃ x, ¬p x) → ¬∀ x, @[simp] theorem exists_or_eq_left' (y : α) (p : α → Prop) : ∃ x : α, y = x ∨ p x := ⟨y, .inl rfl⟩ @[simp] theorem exists_or_eq_right' (y : α) (p : α → Prop) : ∃ x : α, p x ∨ y = x := ⟨y, .inr rfl⟩ -@[simp] theorem exists_prop' {p : Prop} : (∃ _ : α, p) ↔ Nonempty α ∧ p := +theorem exists_prop' {p : Prop} : (∃ _ : α, p) ↔ Nonempty α ∧ p := ⟨fun ⟨a, h⟩ => ⟨⟨a⟩, h⟩, fun ⟨⟨a⟩, h⟩ => ⟨a, h⟩⟩ -theorem exists_prop : (∃ _h : a, b) ↔ a ∧ b := +@[simp] theorem exists_prop : (∃ _h : a, b) ↔ a ∧ b := ⟨fun ⟨hp, hq⟩ => ⟨hp, hq⟩, fun ⟨hp, hq⟩ => ⟨hp, hq⟩⟩ @[simp] theorem exists_apply_eq_apply (f : α → β) (a' : α) : ∃ a, f a = f a' := ⟨a', rfl⟩