add some lemmas about `Finite` and `pred_finite`

CHANGELOG.md

@@ -15,6 +15,7 @@ Coq 8.10 is no longer supported by this release.
 - Rename `decide_iff` → `decide_ext` and `bool_decide_iff` → `bool_decide_ext`.
 - Remove a spurious `Global Arguments Pos.of_nat : simpl never`.
 - Add tactics `destruct select <pat>` and `destruct select <pat> as <intro_pat>`.
+- Add some more lemmas about `Finite` and `pred_finite`.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).

theories/fin_sets.v

@@ -475,6 +475,14 @@ Proof.
   - intros [X Hfin]. exists (elements X). set_solver.
 Qed.
 
+Lemma dec_pred_finite_set (P : A → Prop) {Hdec : ∀ x : A, Decision (P x)} :
+  pred_finite P ↔ (∃ X : C, ∀ x, P x ↔ x ∈ X).
+Proof.
+  rewrite dec_pred_finite; [|done]. split.
+  - intros [xs Hfin]. exists (list_to_set xs). set_solver.
+  - intros [X Hfin]. exists (elements X). set_solver.
+Qed.
+
 Lemma pred_infinite_set (P : A → Prop) :
   pred_infinite P ↔ (∀ X : C, ∃ x, P x ∧ x ∉ X).
 Proof.

theories/finite.v

@@ -373,6 +373,34 @@ Qed.
 Lemma fin_card n : card (fin n) = n.
 Proof. unfold card; simpl. induction n; simpl; rewrite ?fmap_length; auto. Qed.
 
+Lemma finite_dec (P : Prop) `{Hfin : Finite P} : Decision P.
+Proof.
+  destruct Hfin as [[ | p proofs'] _ Hproofs].
+  { right. intros p. specialize (Hproofs p) as ?%not_elem_of_nil. naive_solver. }
+  { left. done. }
+Qed.
+
+(* shouldn’t be an instance (cycle with [sig_finite]): *)
+Lemma finite_sig_dec {A} {Heqdec : EqDecision A} (P : A → Prop) `{Hfin : Finite (sig P)} :
+  ∀ x, Decision (P x).
+Proof.
+  intros x. destruct Hfin as [elems _ Helems'].
+  assert (∀ px, (x ↾ px) ∈ elems) as Helems by done; clear Helems'.
+  assert (Decision {px | (x ↾ px) ∈ elems}) as [[px ?] | no_px].
+  {
+    induction elems as [ | [y py] elems' IH].
+    { right. intros [? ?%not_elem_of_nil]. naive_solver. }
+    { destruct (decide (x = y)) as [-> | ?].
+      { left. by exists py. }
+      { destruct IH as [[px ?] | no_px].
+        { intros px. specialize (Helems px) as ?%elem_of_cons. naive_solver. }
+        { left. by exists px. }
+        { right. intros [px ?%elem_of_cons]. naive_solver. } } }
+  }
+  { by left. }
+  { right. intros px. apply no_px. by exists px. }
+Qed.
+
 Section sig_finite.
   Context {A} (P : A → Prop) `{∀ x, Decision (P x)}.
 

theories/sets.v

@@ -1169,6 +1169,46 @@ 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.
+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..]. }
+Qed.
+
+Lemma finite_sig_pred_finite {A} (P : A → Prop) `{Hfin : Finite (sig P)} :
+  pred_finite P.
+Proof.
+  exists (proj1_sig <$> enum _). intros x px.
+  apply elem_of_list_fmap_1_alt with (x ↾ px); [apply elem_of_enum|]; done.
+Qed.
+
+Lemma pred_finite_arg2 {A B} (P : A → B → Prop) :
+  pred_finite (uncurry P) → ∀ x, pred_finite (P x).
+Proof.
+  intros [xys ?] x. exists (xys.*2). intros y ?.
+  apply elem_of_list_fmap_1_alt with (x, y); by auto.
+Qed.
+
+Lemma pred_finite_arg1 {A B} (P : A → B → Prop) :
+  pred_finite (uncurry P) → ∀ y, pred_finite (flip P y).
+Proof.
+  intros [xys ?] y. exists (xys.*1). intros x ?.
+  apply elem_of_list_fmap_1_alt with (x, y); by auto.
+Qed.
+
 (** Sets of sequences of natural numbers *)
 (* The set [seq_seq start len] of natural numbers contains the sequence
 [start, start + 1, ..., start + (len-1)]. *)