From 996a098d10bede9b260ec1aeb1c5929f19109a77 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 29 Jan 2021 13:20:22 +0100
Subject: [PATCH] add pred_infinite_surj

---
 theories/sets.v | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/theories/sets.v b/theories/sets.v
index 7c144f92..28f75fe7 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -1044,6 +1044,18 @@ Section pred_finite_infinite.
     pred_infinite P → (∀ x, P x → Q x) → pred_infinite Q.
   Proof. unfold pred_infinite. set_solver. Qed.
 
+  (** If [f] is surjective onto [P], then pre-composing with [f] preserves
+  infinity. *)
+  Lemma pred_infinite_surj {A} (P : A → Prop) (f : A → A) :
+    (∀ x, P x → ∃ y, f y = x) →
+    pred_infinite P → pred_infinite (P ∘ f).
+  Proof.
+    intros Hf HP xs. destruct (HP (f <$> xs)) as [x [HPx Hx]].
+    destruct (Hf _ HPx) as [y Hf']. exists y. split.
+    - simpl. rewrite Hf'. done.
+    - intros Hy. apply Hx. apply elem_of_list_fmap. eauto.
+  Qed.
+
   Lemma pred_not_infinite_finite {A} (P : A → Prop) :
     pred_infinite P → pred_finite P → False.
   Proof. intros Hinf [xs ?]. destruct (Hinf xs). set_solver. Qed.
-- 
GitLab