Merge branch 'robbert/list_find' into 'master'

Generalize `list_find` lemmas to become bi-implications.

See merge request !99

CHANGELOG.md

@@ -6,6 +6,7 @@ API-breaking change is listed.
 - Rename `dom_map_filter` into `dom_map_filter_subseteq` and repurpose
   `dom_map_filter` for the version with the equality. This follows the naming
   convention for similar lemmas.
+- Generalize `list_find_Some` and `list_find_None` to become bi-implications.
 - Disambiguate Haskell-style notations for partially applied operators. For
   example, change `(!! i)` into `(.!! x)` so that `!!` can also be used as a
   prefix, as done in VST. A sed script to perform the renaming can be found at:

theories/finite.v

@@ -37,8 +37,8 @@ Lemma encode_lt_card `{finA: Finite A} (x : A) : encode_nat x < card A.
 Proof.
   destruct finA as [xs Hxs HA]; unfold encode_nat, encode, card; simpl.
   rewrite Nat2Pos.id by done; simpl.
-  destruct (list_find _ xs) as [[i y]|] eqn:?; simpl.
-  - destruct (list_find_Some (x =.) xs i y); eauto using lookup_lt_Some.
+  destruct (list_find _ xs) as [[i y]|] eqn:HE; simpl.
+  - apply list_find_Some in HE as (?&?&?); eauto using lookup_lt_Some.
   - destruct xs; simpl. exfalso; eapply not_elem_of_nil, (HA x). lia.
 Qed.
 Lemma encode_decode A `{finA: Finite A} i :
@@ -49,8 +49,8 @@ Proof.
   intros Hi. apply lookup_lt_is_Some in Hi. destruct Hi as [x Hx].
   exists x. rewrite !Nat2Pos.id by done; simpl.
   destruct (list_find_elem_of (x =.) xs x) as [[j y] Hj]; auto.
-  destruct (list_find_Some (x =.) xs j y) as [? ->]; auto.
-  rewrite Hj; csimpl; eauto using NoDup_lookup.
+  split; [done|]; rewrite Hj; simpl.
+  apply list_find_Some in Hj as (?&->&?). eauto using NoDup_lookup.
 Qed.
 Lemma find_Some `{finA: Finite A} P `{∀ x, Decision (P x)} (x : A) :
   find P = Some x → P x.
@@ -65,8 +65,8 @@ Lemma find_is_Some `{finA: Finite A} P `{∀ x, Decision (P x)} (x : A) :
 Proof.
   destruct finA as [xs Hxs HA]; unfold find, decode; simpl.
   intros Hx. destruct (list_find_elem_of P xs x) as [[i y] Hi]; auto.
-  rewrite Hi. destruct (list_find_Some P xs i y); simplify_eq/=; auto.
-  exists y. by rewrite !Nat2Pos.id by done.
+  rewrite Hi; simpl. rewrite !Nat2Pos.id by done. simpl.
+  apply list_find_Some in Hi; naive_solver.
 Qed.
 
 Definition encode_fin `{Finite A} (x : A) : fin (card A) :=

theories/list.v

@@ -921,46 +921,6 @@ Section list_set.
   Qed.
 End list_set.
 
-(** ** Properties of the [find] function *)
-Section find.
-  Context (P : A → Prop) `{∀ x, Decision (P x)}.
-  Lemma list_find_Some l i x :
-    list_find P l = Some (i,x) → l !! i = Some x ∧ P x.
-  Proof.
-    revert i; induction l; intros [] ?; repeat first
-      [ match goal with x : prod _ _ |- _ => destruct x end
-      | simplify_option_eq ]; eauto.
-  Qed.
-  Lemma list_find_None l :
-    list_find P l = None → Forall (λ x, ¬ P x) l.
-  Proof.
-    induction l as [|? l IHl]; [eauto|]. simpl. case_decide; [done|].
-    intros. constructor; [done|]. apply IHl.
-    by destruct (list_find P l).
-  Qed.
-  Lemma list_find_elem_of l x : x ∈ l → P x → is_Some (list_find P l).
-  Proof.
-    induction 1 as [|x y l ? IH]; intros; simplify_option_eq; eauto.
-    by destruct IH as [[i x'] ->]; [|exists (S i, x')].
-  Qed.
-
-  Lemma list_find_fmap {B : Type} (f : B → A) (l : list B) :
-    list_find P (f <$> l) = prod_map id f <$> list_find (P ∘ f) l.
-  Proof.
-    induction l as [|x l IH]; [done|]. csimpl. (* csimpl re-folds fmap *)
-    case_decide; [done|].
-    rewrite IH. by destruct (list_find (P ∘ f) l).
-  Qed.
-
-  Lemma list_find_ext (Q : A → Prop) `{∀ x, Decision (Q x)} l :
-    (∀ x, P x ↔ Q x) →
-    list_find P l = list_find Q l.
-  Proof.
-    intros HPQ. induction l as [|x l IH]; simpl; [done|].
-    by rewrite (decide_iff (P x) (Q x)), IH by done.
-  Qed.
-End find.
-
 (** ** Properties of the [omap] function *)
 Lemma list_fmap_omap {B C : Type} (f : A → option B) (g : B → C) (l : list A) :
   g <$> omap f l = omap (λ x, g <$> (f x)) l.
@@ -3154,6 +3114,59 @@ Section setoid.
   Qed.
 End setoid.
 
+(** * Properties of the [find] function *)
+Section find.
+  Context {A} (P : A → Prop) `{∀ x, Decision (P x)}.
+
+  Lemma list_find_Some l i x  :
+    list_find P l = Some (i,x) ↔
+      l !! i = Some x ∧ P x ∧ ∀ j, j < i → ∃ y, l !! j = Some y ∧ ¬P y.
+  Proof.
+    revert i. induction l as [|y l IH]; intros i; csimpl; [naive_solver|].
+    case_decide.
+    - split; [naive_solver lia|]. intros (Hi&HP&Hlt).
+      destruct i as [|i]; simplify_eq/=; [done|].
+      destruct (Hlt 0); naive_solver lia.
+    - split.
+      + intros ([i' x']&Hl&?)%fmap_Some; simplify_eq/=.
+        apply IH in Hl as (?&?&Hlt). split_and!; [done..|].
+        intros [|j] ?; naive_solver lia.
+      + intros (?&?&Hlt). destruct i as [|i]; simplify_eq/=; [done|].
+        rewrite (proj2 (IH i)); [done|]. split_and!; [done..|].
+        intros j ?. destruct (Hlt (S j)); naive_solver lia.
+  Qed.
+
+  Lemma list_find_elem_of l x : x ∈ l → P x → is_Some (list_find P l).
+  Proof.
+    induction 1 as [|x y l ? IH]; intros; simplify_option_eq; eauto.
+    by destruct IH as [[i x'] ->]; [|exists (S i, x')].
+  Qed.
+
+  Lemma list_find_None l :
+    list_find P l = None ↔ Forall (λ x, ¬P x) l.
+  Proof.
+    rewrite eq_None_not_Some, Forall_forall. split.
+    - intros Hl x Hx HP. destruct Hl. eauto using list_find_elem_of.
+    - intros HP [[i x] (?%elem_of_list_lookup_2&?&?)%list_find_Some]; naive_solver.
+  Qed.
+
+  Lemma list_find_fmap {B : Type} (f : B → A) (l : list B) :
+    list_find P (f <$> l) = prod_map id f <$> list_find (P ∘ f) l.
+  Proof.
+    induction l as [|x l IH]; [done|]; csimpl. (* csimpl re-folds fmap *)
+    case_decide; [done|].
+    rewrite IH. by destruct (list_find (P ∘ f) l).
+  Qed.
+
+  Lemma list_find_ext (Q : A → Prop) `{∀ x, Decision (Q x)} l :
+    (∀ x, P x ↔ Q x) →
+    list_find P l = list_find Q l.
+  Proof.
+    intros HPQ. induction l as [|x l IH]; simpl; [done|].
+    by rewrite (decide_iff (P x) (Q x)), IH by done.
+  Qed.
+End find.
+
 (** * Properties of the monadic operations *)
 Lemma list_fmap_id {A} (l : list A) : id <$> l = l.
 Proof. induction l; f_equal/=; auto. Qed.