From 10d52cfd888c78fb487a42541fa484139955f8e8 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <gitlab-sws@robbertkrebbers.nl>
Date: Mon, 13 Dec 2021 13:53:13 +0000
Subject: [PATCH] shorten the proof of `dec_pred_finite`

---
 theories/sets.v | 18 +++---------------
 1 file changed, 3 insertions(+), 15 deletions(-)

diff --git a/theories/sets.v b/theories/sets.v
index 09049410..5651531f 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -1169,23 +1169,11 @@ Proof.
   intros xs. exists (fresh xs). split; [set_solver|]. apply infinite_is_fresh.
 Qed.
 
-Lemma dec_pred_finite {A} (P : A → Prop) {Hdec : ∀ x, Decision (P x)} :
-  pred_finite P ↔ ∃ (xs : list A), ∀ x, P x ↔ x ∈ xs.
+Lemma dec_pred_finite {A} (P : A → Prop) `{!∀ x, Decision (P x)} :
+  pred_finite P ↔ ∃ xs : list A, ∀ x, P x ↔ x ∈ xs.
 Proof.
   split; intros [xs Hxs]; [|exists xs; set_solver].
-  cut (∀ n, ∃ ys, (∀ x, P x → x ∈ ys ++ drop n xs) ∧ (∀ x, x ∈ ys → P x)).
-  { intros H. specialize (H (length xs)) as (ys & H1 & H2).
-    rewrite drop_all, app_nil_r in H1. exists ys. set_solver. }
-  intros n. induction n as [ | n (ys & IH1 & IH2)].
-  { exists []. rewrite drop_0. set_solver. }
-  destruct (decide (n < length xs)) as [[y Hn]%lookup_lt_is_Some | ?].
-  { destruct (decide (P y)) as [Hy | Hy].
-    { exists (ys ++ [y]). pose proof (assoc app) as <-. cbn.
-      rewrite <-drop_S; set_solver. }
-    { exists ys. split; [|done]. intros x Hx.
-      specialize (IH1 x Hx) as [? | Hx_elem_of]%elem_of_app; [set_solver|].
-      erewrite drop_S in Hx_elem_of; set_solver. } }
-  { exists ys. revert IH1. rewrite !drop_ge, app_nil_r; [done|lia..]. }
+  exists (filter P xs). intros x. rewrite elem_of_list_filter. naive_solver.
 Qed.
 
 Lemma finite_sig_pred_finite {A} (P : A → Prop) `{Finite (sig P)} :
-- 
GitLab