Improve "choosing an element" of a finite collection.

theories/fin_collections.v

@@ -6,6 +6,7 @@ principles on finite collections . *)
 Require Import Permutation ars.
 Require Export collections numbers listset.
 
+Definition choose `{Elements A C} (X : C) : option A := head (elements X).
 Instance collection_size `{Elements A C} : Size C := length ∘ elements.
 Definition collection_fold `{Elements A C} {B}
   (f : A → B → B) (b : B) : C → B := foldr f b ∘ elements.
@@ -26,9 +27,8 @@ Proof. intros ?? E. apply Permutation_length. by rewrite E. Qed.
 Lemma size_empty : size (∅ : C) = 0.
 Proof.
   unfold size, collection_size. simpl.
-  rewrite (elem_of_nil_inv (elements ∅)).
-  * done.
-  * intro. rewrite <-elements_spec. solve_elem_of.
+  rewrite (elem_of_nil_inv (elements ∅)); [done |].
+  intro. rewrite <-elements_spec. solve_elem_of.
 Qed.
 Lemma size_empty_inv (X : C) : size X = 0 → X ≡ ∅.
 Proof.
@@ -52,41 +52,44 @@ Qed.
 Lemma size_singleton_inv X x y : size X = 1 → x ∈ X → y ∈ X → x = y.
 Proof.
   unfold size, collection_size. simpl. rewrite !elements_spec.
-  generalize (elements X). intros [|? l].
-  * done.
-  * injection 1. intro. rewrite (nil_length l) by done.
-    simpl. rewrite !elem_of_list_singleton. congruence.
+  generalize (elements X). intros [|? l]; intro; simplify_equality.
+  rewrite (nil_length l), !elem_of_list_singleton by done. congruence.
 Qed.
 
+Lemma choose_Some X x : choose X = Some x → x ∈ X.
+Proof.
+  unfold choose. destruct (elements X) eqn:E; intros; simplify_equality.
+  rewrite elements_spec, E. by left.
+Qed.
+Lemma choose_None X : choose X = None → X ≡ ∅.
+Proof.
+  unfold choose. destruct (elements X) eqn:E; intros; simplify_equality.
+  apply equiv_empty. intros x. by rewrite elements_spec, E, elem_of_nil.
+Qed.
 Lemma elem_of_or_empty X : (∃ x, x ∈ X) ∨ X ≡ ∅.
+Proof. destruct (choose X) eqn:?; eauto using choose_Some, choose_None. Qed.
+Lemma choose_is_Some X : X ≢ ∅ ↔ is_Some (choose X).
 Proof.
-  destruct (elements X) as [|x xs] eqn:E.
-  * right. apply equiv_empty. intros x Ex.
-    by rewrite elements_spec, E, elem_of_nil in Ex.
-  * left. exists x. rewrite elements_spec, E.
-    by constructor.
+  rewrite is_Some_alt. destruct (choose X) eqn:?.
+  * rewrite elem_of_equiv_empty. split; eauto using choose_Some.
+  * split. intros []; eauto using choose_None. by intros [??].
 Qed.
-
-Lemma choose X : X ≢ ∅ → ∃ x, x ∈ X.
+Lemma not_elem_of_equiv_empty X : X ≢ ∅ ↔ (∃ x, x ∈ X).
 Proof.
-  destruct (elem_of_or_empty X) as [[x ?]|?].
-  * by exists x.
-  * done.
+  destruct (elem_of_or_empty X) as [?|E]; [esolve_elem_of |].
+  setoid_rewrite E. setoid_rewrite elem_of_empty. naive_solver.
 Qed.
-Lemma size_pos_choose X : 0 < size X → ∃ x, x ∈ X.
+Lemma size_pos_elem_of X : 0 < size X → ∃ x, x ∈ X.
 Proof.
-  intros E1. apply choose.
-  intros E2. rewrite E2, size_empty in E1.
-  by apply (Lt.lt_n_0 0).
+  intros E1. apply not_elem_of_equiv_empty. intros E2.
+  rewrite E2, size_empty in E1. lia.
 Qed.
-Lemma size_1_choose X : size X = 1 → ∃ x, X ≡ {[ x ]}.
+Lemma size_1_elem_of X : size X = 1 → ∃ x, X ≡ {[ x ]}.
 Proof.
-  intros E. destruct (size_pos_choose X).
-  * rewrite E. auto with arith.
-  * exists x. apply elem_of_equiv. split.
-    + intro. rewrite elem_of_singleton.
-      eauto using size_singleton_inv.
-    + solve_elem_of.
+  intros E. destruct (size_pos_elem_of X); auto with lia.
+  exists x. apply elem_of_equiv. split.
+  * rewrite elem_of_singleton. eauto using size_singleton_inv.
+  * solve_elem_of.
 Qed.
 
 Lemma size_union X Y : X ∩ Y ≡ ∅ → size (X ∪ Y) = size X + size Y.
@@ -111,16 +114,12 @@ Global Program Instance collection_subseteq_dec_slow (X Y : C) :
   | right E1 => right _
   end.
 Next Obligation.
-  intros x Ex; apply dec_stable; intro.
-  destruct (proj1 (elem_of_empty x)).
-  apply (size_empty_inv _ E1).
-  by rewrite elem_of_difference.
+  intros x Ex; apply dec_stable; intro. destruct (proj1 (elem_of_empty x)).
+  apply (size_empty_inv _ E1). by rewrite elem_of_difference.
 Qed.
 Next Obligation.
-  intros E2. destruct E1.
-  apply size_empty_iff, equiv_empty. intros x.
-  rewrite elem_of_difference. intros [E3 ?].
-  by apply E2 in E3.
+  intros E2. destruct E1. apply size_empty_iff, equiv_empty. intros x.
+  rewrite elem_of_difference. intros [E3 ?]. by apply E2 in E3.
 Qed.
 
 Lemma size_union_alt X Y : size (X ∪ Y) = size X + size (Y ∖ X).
@@ -131,9 +130,7 @@ Proof.
 Qed.
 
 Lemma subseteq_size X Y : X ⊆ Y → size X ≤ size Y.
-Proof.
-  intros. rewrite (union_difference X Y), size_union_alt by done. lia.
-Qed.
+Proof. intros. rewrite (union_difference X Y), size_union_alt by done. lia. Qed.
 Lemma subset_size X Y : X ⊂ Y → size X < size Y.
 Proof.
   intros. rewrite (union_difference X Y) by solve_elem_of.
@@ -147,9 +144,7 @@ Proof. apply well_founded_lt_compat with size, subset_size. Qed.
 
 Lemma collection_ind (P : C → Prop) :
   Proper ((≡) ==> iff) P →
-  P ∅ →
-  (∀ x X, x ∉ X → P X → P ({[ x ]} ∪ X)) →
-  ∀ X, P X.
+  P ∅ → (∀ x X, x ∉ X → P X → P ({[ x ]} ∪ X)) → ∀ X, P X.
 Proof.
   intros ? Hemp Hadd. apply well_founded_induction with (⊂).
   { apply collection_wf. }
@@ -180,11 +175,7 @@ Lemma collection_fold_proper {B} (R : relation B) `{!Equivalence R}
     (f : A → B → B) (b : B) `{!Proper ((=) ==> R ==> R) f}
     (Hf : ∀ a1 a2 b, R (f a1 (f a2 b)) (f a2 (f a1 b))) :
   Proper ((≡) ==> R) (collection_fold f b).
-Proof.
-  intros ?? E. apply (foldr_permutation R f b).
-  * auto.
-  * by rewrite E.
-Qed.
+Proof. intros ?? E. apply (foldr_permutation R f b); auto. by rewrite E. Qed.
 
 Global Instance set_Forall_dec `(P : A → Prop)
   `{∀ x, Decision (P x)} X : Decision (set_Forall P X) | 100.