From d455bb4c5b6e96aee947961e62ec29c2fc0c36fa Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 25 Apr 2015 21:38:03 -0700 Subject: [PATCH] feat(library/data/fintype): add decidable_exists_finite --- library/data/fintype.lean | 16 +++++++++++++++- 1 file changed, 15 insertions(+), 1 deletion(-) diff --git a/library/data/fintype.lean b/library/data/fintype.lean index 1dd5d3126..137daa160 100644 --- a/library/data/fintype.lean +++ b/library/data/fintype.lean @@ -117,7 +117,7 @@ theorem ex_of_check_pred_eq_ff {p : A → Prop} [h : decidable_pred p] : ∀ {l (λ npa : ¬ p a, exists.intro a npa) end check_pred -definition decidable_finite_pred [instance] {A : Type} {p : A → Prop} [h₁ : fintype A] [h₂ : decidable_pred p] +definition decidable_forall_finite [instance] {A : Type} {p : A → Prop} [h₁ : fintype A] [h₂ : decidable_pred p] : decidable (∀ x : A, p x) := match h₁ with | fintype.mk e u c := @@ -130,6 +130,20 @@ match h₁ with end rfl end +definition decidable_exists_finite [instance] {A : Type} {p : A → Prop} [h₁ : fintype A] [h₂ : decidable_pred p] + : decidable (∃ x : A, p x) := +match h₁ with +| fintype.mk e u c := + match check_pred (λ a, ¬ p a) e with + | tt := λ h : check_pred (λ a, ¬ p a) e = tt, inr (λ ex : (∃ x, p x), + obtain x px, from ex, + absurd px (all_of_check_pred_eq_tt h (c x))) + | ff := λ h : check_pred (λ a, ¬ p a) e = ff, inl ( + assert aux₁ : ∃ x, ¬¬p x, from ex_of_check_pred_eq_ff h, + obtain x nnpx, from aux₁, exists.intro x (not_not_elim nnpx)) + end rfl +end + open list.as_type -- Auxiliary function for returning a list with all elements of the type: (list.as_type l) -- Remark ⟪s⟫ is notation for (list.as_type l)