Commit 69c36292 authored by Robbert Krebbers's avatar Robbert Krebbers

Generalize `list_find` lemmas to become bi-implications.

Thanks to @jules for the suggestion and an initial proof.
parent 9041e6d8
...@@ -6,6 +6,7 @@ API-breaking change is listed. ...@@ -6,6 +6,7 @@ API-breaking change is listed.
- Rename `dom_map_filter` into `dom_map_filter_subseteq` and repurpose - Rename `dom_map_filter` into `dom_map_filter_subseteq` and repurpose
`dom_map_filter` for the version with the equality. This follows the naming `dom_map_filter` for the version with the equality. This follows the naming
convention for similar lemmas. 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 - Disambiguate Haskell-style notations for partially applied operators. For
example, change `(!! i)` into `(.!! x)` so that `!!` can also be used as a 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: prefix, as done in VST. A sed script to perform the renaming can be found at:
......
...@@ -37,8 +37,8 @@ Lemma encode_lt_card `{finA: Finite A} (x : A) : encode_nat x < card A. ...@@ -37,8 +37,8 @@ Lemma encode_lt_card `{finA: Finite A} (x : A) : encode_nat x < card A.
Proof. Proof.
destruct finA as [xs Hxs HA]; unfold encode_nat, encode, card; simpl. destruct finA as [xs Hxs HA]; unfold encode_nat, encode, card; simpl.
rewrite Nat2Pos.id by done; simpl. rewrite Nat2Pos.id by done; simpl.
destruct (list_find _ xs) as [[i y]|] eqn:?; simpl. destruct (list_find _ xs) as [[i y]|] eqn:HE; simpl.
- destruct (list_find_Some (x =.) xs i y); eauto using lookup_lt_Some. - apply list_find_Some in HE as (?&?&?); eauto using lookup_lt_Some.
- destruct xs; simpl. exfalso; eapply not_elem_of_nil, (HA x). lia. - destruct xs; simpl. exfalso; eapply not_elem_of_nil, (HA x). lia.
Qed. Qed.
Lemma encode_decode A `{finA: Finite A} i : Lemma encode_decode A `{finA: Finite A} i :
...@@ -49,8 +49,8 @@ Proof. ...@@ -49,8 +49,8 @@ Proof.
intros Hi. apply lookup_lt_is_Some in Hi. destruct Hi as [x Hx]. intros Hi. apply lookup_lt_is_Some in Hi. destruct Hi as [x Hx].
exists x. rewrite !Nat2Pos.id by done; simpl. exists x. rewrite !Nat2Pos.id by done; simpl.
destruct (list_find_elem_of (x =.) xs x) as [[j y] Hj]; auto. destruct (list_find_elem_of (x =.) xs x) as [[j y] Hj]; auto.
destruct (list_find_Some (x =.) xs j y) as [? ->]; auto. split; [done|]; rewrite Hj; simpl.
rewrite Hj; csimpl; eauto using NoDup_lookup. apply list_find_Some in Hj as (?&->&?). eauto using NoDup_lookup.
Qed. Qed.
Lemma find_Some `{finA: Finite A} P `{ x, Decision (P x)} (x : A) : Lemma find_Some `{finA: Finite A} P `{ x, Decision (P x)} (x : A) :
find P = Some x P x. find P = Some x P x.
...@@ -65,8 +65,8 @@ Lemma find_is_Some `{finA: Finite A} P `{∀ x, Decision (P x)} (x : A) : ...@@ -65,8 +65,8 @@ Lemma find_is_Some `{finA: Finite A} P `{∀ x, Decision (P x)} (x : A) :
Proof. Proof.
destruct finA as [xs Hxs HA]; unfold find, decode; simpl. 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. 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. rewrite Hi; simpl. rewrite !Nat2Pos.id by done. simpl.
exists y. by rewrite !Nat2Pos.id by done. apply list_find_Some in Hi; naive_solver.
Qed. Qed.
Definition encode_fin `{Finite A} (x : A) : fin (card A) := Definition encode_fin `{Finite A} (x : A) : fin (card A) :=
......
...@@ -921,46 +921,6 @@ Section list_set. ...@@ -921,46 +921,6 @@ Section list_set.
Qed. Qed.
End list_set. 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 *) (** ** Properties of the [omap] function *)
Lemma list_fmap_omap {B C : Type} (f : A → option B) (g : B → C) (l : list A) : 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. g <$> omap f l = omap (λ x, g <$> (f x)) l.
...@@ -3154,6 +3114,59 @@ Section setoid. ...@@ -3154,6 +3114,59 @@ Section setoid.
Qed. Qed.
End setoid. 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 *) (** * Properties of the monadic operations *)
Lemma list_fmap_id {A} (l : list A) : id <$> l = l. Lemma list_fmap_id {A} (l : list A) : id <$> l = l.
Proof. induction l; f_equal/=; auto. Qed. Proof. induction l; f_equal/=; auto. Qed.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment