From f807ece775e08e280aca217958f02644c21b3095 Mon Sep 17 00:00:00 2001 From: Hai Dang Date: Thu, 21 Feb 2019 17:57:32 +0100 Subject: [PATCH] Additionally lemmas for insert, nth, take, and list_find --- theories/list.v | 29 +++++++++++++++++++++++++++++ 1 file changed, 29 insertions(+) diff --git a/theories/list.v b/theories/list.v index f1e5b42..b04984f 100644 --- a/theories/list.v +++ b/theories/list.v @@ -523,6 +523,8 @@ Lemma list_insert_commute l i j x y : Proof. revert i j. by induction l; intros [|?] [|?] ?; f_equal/=; auto. Qed. 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_lookup_other l i x : length l ≠ 1 → l !! i = Some x → ∃ j y, j ≠ i ∧ l !! j = Some y. @@ -689,6 +691,13 @@ Proof. - intros (x&Hx&?). by induction Hx; csimpl; repeat case_match; simplify_eq; try constructor; auto. Qed. +Lemma list_elem_of_insert l i x : i < length l → x ∈ <[i:=x]>l. +Proof. intros. by eapply elem_of_list_lookup_2, list_lookup_insert. Qed. +Lemma nth_elem_of l i d : i < length l → nth i l d ∈ l. +Proof. + intros; eapply elem_of_list_lookup_2. + destruct (nth_lookup_or_length l i d); [done | by lia]. +Qed. (** ** Properties of the [NoDup] predicate *) Lemma NoDup_nil : NoDup (@nil A) ↔ True. @@ -851,6 +860,13 @@ Section find. [ 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. @@ -960,6 +976,11 @@ Proof. - by rewrite !lookup_take_ge. - by rewrite !lookup_take, !list_lookup_insert_ne by lia. Qed. +Lemma take_insert_lt l n i x : i < n → take n (<[i:=x]>l) = <[i:=x]>(take n l). +Proof. + revert l i. induction n as [|? IHn]; auto; simpl. + intros [|] [|] ?; auto; simpl. by rewrite IHn by lia. +Qed. (** ** Properties of the [drop] function *) Lemma drop_0 l : drop 0 l = l. @@ -2237,6 +2258,14 @@ Section Forall_Exists. Proof. by rewrite Forall_lookup. Qed. Lemma Forall_tail l : Forall P l → Forall P (tail l). Proof. destruct 1; simpl; auto. Qed. + Lemma Forall_nth d l : Forall P l ↔ ∀ i, i < length l → P (nth i l d). + Proof. + rewrite Forall_lookup. split. + - intros Hl ? [x Hl']%lookup_lt_is_Some_2. + rewrite (nth_lookup_Some _ _ _ _ Hl'). by eapply Hl. + - intros Hl i x Hl'. specialize (Hl _ (lookup_lt_Some _ _ _ Hl')). + by rewrite (nth_lookup_Some _ _ _ _ Hl') in Hl. + Qed. Lemma Forall_alter f l i : Forall P l → (∀ x, l!!i = Some x → P x → P (f x)) → Forall P (alter f i l). Proof. -- 2.26.2