From 6aac4455ce7ba9788152e3dca5409db078474154 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 27 Aug 2013 10:40:31 +0200
Subject: [PATCH] Prove decidability of quantification over finite types.

---
 theories/finite.v | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)

diff --git a/theories/finite.v b/theories/finite.v
index 62a1d6c7..75cbd9db 100644
--- a/theories/finite.v
+++ b/theories/finite.v
@@ -129,6 +129,27 @@ Lemma bijective_card `{Finite A} `{Finite B} (f : A → B)
   `{!Injective (=) (=) f} `{!Surjective (=) f} : card A = card B.
 Proof. apply finite_bijective. eauto. Qed.
 
+(** Decidability of quantification over finite types *)
+Section forall_exists.
+  Context `{Finite A} (P : A → Prop) `{∀ x, Decision (P x)}.
+
+  Lemma Forall_finite : Forall P (enum A) ↔ (∀ x, P x).
+  Proof. rewrite Forall_forall. intuition auto using elem_of_enum. Qed.
+  Lemma Exists_finite : Exists P (enum A) ↔ (∃ x, P x).
+  Proof. rewrite Exists_exists. naive_solver eauto using elem_of_enum. Qed.
+
+  Global Instance forall_dec: Decision (∀ x, P x).
+  Proof.
+   refine (cast_if (decide (Forall P (enum A))));
+    abstract by rewrite <-Forall_finite.
+  Defined.
+  Global Instance exists_dec: Decision (∃ x, P x).
+  Proof.
+   refine (cast_if (decide (Exists P (enum A))));
+    abstract by rewrite <-Exists_finite.
+  Defined.
+End forall_exists.
+
 (** Instances *)
 Section enc_finite.
   Context `{∀ x y : A, Decision (x = y)}.
-- 
GitLab