michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/data/fintype): add decidable_exists_finite

Browse source
This commit is contained in:
Leonardo de Moura 2015-04-25 21:38:03 -07:00
parent 6bb6644c25
commit d455bb4c5b
1 changed files with 15 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
library/data/fintype.lean
View file

@ -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)