From d7ee81fd058a2f4917a523c592e8d2742a1fbb47 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Tue, 6 Dec 2016 10:20:06 +0100 Subject: [PATCH] Factor out some common properties about lists. --- algebra/cmra_big_op.v | 6 +----- base_logic/big_op.v | 12 +++--------- prelude/list.v | 11 +++++++++++ 3 files changed, 15 insertions(+), 14 deletions(-) diff --git a/algebra/cmra_big_op.v b/algebra/cmra_big_op.v index 8a416043..0fbf131e 100644 --- a/algebra/cmra_big_op.v +++ b/algebra/cmra_big_op.v @@ -156,11 +156,7 @@ Section list. Proof. apply big_opL_forall; apply _. Qed. Lemma big_opL_permutation (f : A → M) l1 l2 : l1 ≡ₚ l2 → ([⋅ list] x ∈ l1, f x) ≡ ([⋅ list] x ∈ l2, f x). - Proof. - assert (∀ l, imap (λ _ x, f x) l = map f l) as EQ; - last by rewrite /big_opL !EQ=>->. - intros l; revert f. induction l as [|?? IH]=>// f. rewrite imap_cons IH //. - Qed. + Proof. intros Hl. by rewrite /big_opL !imap_const Hl. Qed. Global Instance big_opL_ne l n : Proper (pointwise_relation _ (pointwise_relation _ (dist n)) ==> (dist n)) diff --git a/base_logic/big_op.v b/base_logic/big_op.v index 0df566de..088389bb 100644 --- a/base_logic/big_op.v +++ b/base_logic/big_op.v @@ -137,11 +137,7 @@ Proof. intros. apply uPred_included. by apply: big_op_contains. Qed. Lemma big_sep_elem_of Ps P : P ∈ Ps → [∗] Ps ⊢ P. Proof. intros. apply uPred_included. by apply: big_sep_elem_of. Qed. Lemma big_sep_elem_of_acc Ps P : P ∈ Ps → [∗] Ps ⊢ P ∗ (P -∗ [∗] Ps). -Proof. - intros (Ps1&Ps2&->)%elem_of_list_split. - rewrite !big_sep_app /=. rewrite assoc (comm _ _ P) -assoc. - by apply sep_mono_r, wand_intro_l. -Qed. +Proof. intros [k ->]%elem_of_Permutation. by apply sep_mono_r, wand_intro_l. Qed. (** ** Persistence *) Global Instance big_sep_persistent Ps : PersistentL Ps → PersistentP ([∗] Ps). @@ -233,10 +229,8 @@ Section list. l !! i = Some x → ([∗ list] k↦y ∈ l, Φ k y) ⊢ Φ i x ∗ (Φ i x -∗ ([∗ list] k↦y ∈ l, Φ k y)). Proof. - intros Hli. apply big_sep_elem_of_acc. revert Φ l Hli. - induction i as [|? IH]=>Φ [] //= y l; rewrite imap_cons. - - intros [=->]. constructor. - - intros ?. constructor. by apply (IH (_ ∘ S)). + intros Hli. apply big_sep_elem_of_acc, (elem_of_list_lookup_2 _ i). + by rewrite list_lookup_imap Hli. Qed. Lemma big_sepL_lookup Φ l i x : diff --git a/prelude/list.v b/prelude/list.v index 8afbbf8a..72cd5c6a 100644 --- a/prelude/list.v +++ b/prelude/list.v @@ -1292,6 +1292,15 @@ Lemma imap_fmap {B C} (f : nat → B → C) (g : A → B) l : imap f (g <\$> l) = imap (λ n, f n ∘ g) l. Proof. unfold imap. generalize 0. induction l; csimpl; auto with f_equal. Qed. +Lemma imap_const {B} (f : A → B) l : imap (const f) l = f <\$> l. +Proof. unfold imap. generalize 0. induction l; csimpl; auto with f_equal. Qed. + +Lemma list_lookup_imap {B} (f : nat → A → B) l i : imap f l !! i = f i <\$> l !! i. +Proof. + revert f i. induction l as [|x l IH]; intros f [|i]; try done. + rewrite imap_cons; simpl. by rewrite IH. +Qed. + (** ** Properties of the [mask] function *) Lemma mask_nil f βs : mask f βs (@nil A) = []. Proof. by destruct βs. Qed. @@ -1401,6 +1410,8 @@ Proof. revert i; induction l as [|y l IH]; intros [|i] ?; simplify_eq/=; auto. by rewrite Permutation_swap, <-(IH i). Qed. +Lemma elem_of_Permutation l x : x ∈ l → ∃ k, l ≡ₚ x :: k. +Proof. intros [i ?]%elem_of_list_lookup. eauto using delete_Permutation. Qed. (** ** Properties of the [prefix_of] and [suffix_of] predicates *) Global Instance: PreOrder (@prefix_of A). -- GitLab