From 83746e0a3105f31f4f0c6aba6a94988f1d6455b3 Mon Sep 17 00:00:00 2001 From: Michael Sammler Date: Wed, 26 Jun 2019 12:01:20 +0200 Subject: [PATCH] some list related lemmas --- theories/list.v | 48 ++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 48 insertions(+) diff --git a/theories/list.v b/theories/list.v index ab606e0..0004d9d 100644 --- a/theories/list.v +++ b/theories/list.v @@ -565,6 +565,9 @@ Lemma list_insert_id l i x : l !! i = Some x → <[i:=x]>l = l. Proof. revert i. induction l; intros [|i] [=]; f_equal/=; auto. Qed. Lemma list_insert_ge l i x : length l ≤ i → <[i:=x]>l = l. Proof. revert i. induction l; intros [|i] ?; f_equal/=; auto with lia. Qed. +Lemma list_insert_insert l i x y : + <[i:=x]> (<[i:=y]> l) = <[i:=x]> l. +Proof. revert i. induction l; intros [|i]; f_equal/=; auto. Qed. Lemma list_lookup_other l i x : length l ≠ 1 → l !! i = Some x → ∃ j y, j ≠ i ∧ l !! j = Some y. @@ -955,6 +958,8 @@ Proof. Qed. Lemma take_nil n : take n [] =@{list A} []. Proof. by destruct n. Qed. +Lemma take_S_r l n x : l !! n = Some x → take (S n) l = take n l ++ [x]. +Proof. revert n. induction l; intros []; naive_solver eauto with f_equal. Qed. Lemma take_app l k : take (length l) (l ++ k) = l. Proof. induction l; f_equal/=; auto. Qed. Lemma take_app_alt l k n : n = length l → take n (l ++ k) = l. @@ -1012,6 +1017,9 @@ Lemma drop_0 l : drop 0 l = l. Proof. done. Qed. Lemma drop_nil n : drop n [] =@{list A} []. Proof. by destruct n. Qed. +Lemma drop_S l x n : + l !! n = Some x → drop n l = x :: drop (S n) l. +Proof. revert n. induction l; intros []; naive_solver. Qed. Lemma drop_length l n : length (drop n l) = length l - n. Proof. revert n. by induction l; intros [|i]; f_equal/=. Qed. Lemma drop_ge l n : length l ≤ n → drop n l = []. @@ -1110,6 +1118,9 @@ Proof. done. Qed. Lemma replicate_plus n m x : replicate (n + m) x = replicate n x ++ replicate m x. Proof. induction n; f_equal/=; auto. Qed. +Lemma replicate_cons_app n x : + x :: replicate n x = replicate n x ++ [x]. +Proof. induction n; f_equal/=; eauto. Qed. Lemma take_replicate n m x : take n (replicate m x) = replicate (min n m) x. Proof. revert m. by induction n; intros [|?]; f_equal/=. Qed. Lemma take_replicate_plus n m x : take n (replicate (n + m) x) = replicate n x. @@ -3606,6 +3617,35 @@ Section zip_with. Forall (λ x, ∀ y, P y → Q (f x y)) l → Forall P k → Forall Q (zip_with f l k). Proof. intros Hl. revert k. induction Hl; destruct 1; simpl in *; auto. Qed. + + Lemma elem_of_lookup_zip_with_1 l k (z : C) : + z ∈ zip_with f l k → ∃ i x y, z = f x y ∧ l !! i = Some x ∧ k !! i = Some y. + Proof. + intros [i Hin]%elem_of_list_lookup. rewrite lookup_zip_with in Hin. + simplify_option_eq; naive_solver. + Qed. + + Lemma elem_of_lookup_zip_with_2 l k x y (z : C) i : + l !! i = Some x → k !! i = Some y → f x y ∈ zip_with f l k. + Proof. + intros Hl Hk. rewrite elem_of_list_lookup. + exists i. by rewrite lookup_zip_with, Hl, Hk. + Qed. + + Lemma elem_of_lookup_zip_with l k (z : C) : + z ∈ zip_with f l k ↔ ∃ i x y, z = f x y ∧ l !! i = Some x ∧ k !! i = Some y. + Proof. + naive_solver eauto using + elem_of_lookup_zip_with_1, elem_of_lookup_zip_with_2. + Qed. + + Lemma elem_of_zip_with l k (z : C) : + z ∈ zip_with f l k → ∃ x y, z = f x y ∧ x ∈ l ∧ y ∈ k. + Proof. + intros ?%elem_of_lookup_zip_with. + naive_solver eauto using elem_of_list_lookup_2. + Qed. + End zip_with. Lemma zip_with_sublist_alter {A B} (f : A → B → A) g l k i n l' k' : @@ -3644,6 +3684,14 @@ Section zip. rewrite <-Forall2_same_length. intros Hlk1 Hlk2. revert l1 k1 Hlk1. induction Hlk2; intros ?? [|??????]; simpl; auto. Qed. + + Lemma elem_of_zip_l x1 x2 l k : + (x1, x2) ∈ zip l k → x1 ∈ l. + Proof. intros ?%elem_of_zip_with. naive_solver. Qed. + + Lemma elem_of_zip_r x1 x2 l k : + (x1, x2) ∈ zip l k → x2 ∈ k. + Proof. intros ?%elem_of_zip_with. naive_solver. Qed. End zip. Lemma elem_of_zipped_map {A B} (f : list A → list A → A → B) l k x : -- 2.26.2