From 886c824e333908af1195dfa7dbe2b3949d894e46 Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Thu, 16 Mar 2017 08:58:27 +0100
Subject: [PATCH] feat(library/init/data/list/instances): prove decidability of
 bounded quantification

---
 library/init/data/list/instances.lean | 31 +++++++++++++++++++++++++++
 1 file changed, 31 insertions(+)

diff --git a/library/init/data/list/instances.lean b/library/init/data/list/instances.lean
index 1ae4565e3e..a02490ac26 100644
--- a/library/init/data/list/instances.lean
+++ b/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