From 7c8ab81cc628ed7d5d59c1fcc7db48293c5d458e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 13 Dec 2014 15:48:04 -0800 Subject: [PATCH] feat(library/logic/quantifiers): add decidable_forall_eq and decidable_exists_eq theorems --- library/logic/quantifiers.lean | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/library/logic/quantifiers.lean b/library/logic/quantifiers.lean index cd078af8a5..92c7d4ac8b 100644 --- a/library/logic/quantifiers.lean +++ b/library/logic/quantifiers.lean @@ -55,3 +55,22 @@ iff.intro theorem exists_imp_nonempty {A : Type} {P : A → Prop} (H : ∃x, P x) : nonempty A := obtain w Hw, from H, nonempty.intro w + +section + open decidable eq.ops + + variables {A : Type} (P : A → Prop) (a : A) [H : decidable (P a)] + include H + + definition decidable_forall_eq [instance] : decidable (∀ x, x = a → P x) := + decidable.rec_on H + (λ pa, inl (λ x heq, eq.rec_on (eq.rec_on heq rfl) pa)) + (λ npa, inr (λ h, absurd (h a rfl) npa)) + + definition decidable_exists_eq [instance] : decidable (∃ x, x = a ∧ P x) := + decidable.rec_on H + (λ pa, inl (exists_intro a (and.intro rfl pa))) + (λ npa, inr (λ h, + obtain (w : A) (Hw : w = a ∧ P w), from h, + absurd (and.rec_on Hw (λ h₁ h₂, h₁ ▸ h₂)) npa)) +end