feat(library/init/data/list/instances): prove decidability of bounded quantification

library/init/data/list/instances.lean

@@ -20,3 +20,34 @@ by tactic.mk_dec_eq_instance
 
 instance : decidable_eq string :=
 list.decidable_eq
+
+namespace list
+
+variables {α : Type u} [decidable_eq α]
+variables (p : α → Prop) [decidable_pred p]
+
+instance decidable_bex : ∀ (l : list α), decidable (∃ x ∈ l, p x)
+| [] := is_false (by intro; cases a; cases a_2; cases a)
+| (x::xs) :=
+  if hx : p x then
+    is_true ⟨x, or.inl rfl, hx⟩
+  else
+    match decidable_bex xs with
+    | is_true  hxs := is_true $ begin
+        cases hxs with x' hx', cases hx' with hx' hpx',
+        existsi x', existsi (or.inr hx'), assumption, exact x' = x
+      end
+    | is_false hxs := is_false $ begin
+        intro hxxs, cases hxxs with x' hx', cases hx' with hx' hpx',
+        cases hx', cc,
+        apply hxs, existsi x', existsi a, assumption
+      end
+    end
+
+instance decidable_ball (l : list α) : decidable (∀ x ∈ l, p x) :=
+if h : ∃ x ∈ l, ¬ p x then
+  is_false $ begin cases h with x h, cases h with hx h, intro h', apply h, apply h', assumption end
+else
+  is_true $ λ x hx, if h' : p x then h' else false.elim $ h ⟨x, hx, h'⟩
+
+end list