diff --git a/theories/list.v b/theories/list.v index b04984ffd2648f0be6810e441ef525565a5da38c..eb19fa71481cdd448c9f3799f3c49fe882790077 100644 --- a/theories/list.v +++ b/theories/list.v @@ -835,21 +835,6 @@ Section list_set. Qed. End list_set. -(** ** Properties of the [filter] function *) -Section filter. - Context (P : A → Prop) `{∀ x, Decision (P x)}. - Lemma elem_of_list_filter l x : x ∈ filter P l ↔ P x ∧ x ∈ l. - Proof. - unfold filter. induction l; simpl; repeat case_decide; - rewrite ?elem_of_nil, ?elem_of_cons; naive_solver. - Qed. - Lemma NoDup_filter l : NoDup l → NoDup (filter P l). - Proof. - unfold filter. induction 1; simpl; repeat case_decide; - rewrite ?NoDup_nil, ?NoDup_cons, ?elem_of_list_filter; tauto. - Qed. -End filter. - (** ** Properties of the [find] function *) Section find. Context (P : A → Prop) `{∀ x, Decision (P x)}. @@ -1539,6 +1524,44 @@ Proof. by rewrite Nat.sub_0_r, <-Hl. Qed. +(** ** Properties of the [filter] function *) +Section filter. + Context (P : A → Prop) `{∀ x, Decision (P x)}. + Local Arguments filter {_ _ _} _ {_} !_ /. + + Lemma filter_nil : filter P [] = []. + Proof. done. Qed. + Lemma filter_cons x l : + filter P (x :: l) = if decide (P x) then x :: filter P l else filter P l. + Proof. done. Qed. + Lemma filter_cons_True x l : P x → filter P (x :: l) = x :: filter P l. + Proof. intros. by rewrite filter_cons, decide_True. Qed. + Lemma filter_cons_False x l : ¬P x → filter P (x :: l) = filter P l. + Proof. intros. by rewrite filter_cons, decide_False. Qed. + + Lemma elem_of_list_filter l x : x ∈ filter P l ↔ P x ∧ x ∈ l. + Proof. + induction l; simpl; repeat case_decide; + rewrite ?elem_of_nil, ?elem_of_cons; naive_solver. + Qed. + Lemma NoDup_filter l : NoDup l → NoDup (filter P l). + Proof. + induction 1; simpl; repeat case_decide; + rewrite ?NoDup_nil, ?NoDup_cons, ?elem_of_list_filter; tauto. + Qed. + + Global Instance filter_Permutation : Proper ((≡ₚ) ==> (≡ₚ)) (filter P). + Proof. induction 1; repeat (simpl; repeat case_decide); by econstructor. Qed. + + Lemma filter_length l : length (filter P l) ≤ length l. + Proof. induction l; simpl; repeat case_decide; simpl; lia. Qed. + Lemma filter_length_lt l x : x ∈ l → ¬P x → length (filter P l) < length l. + Proof. + intros [k ->]%elem_of_Permutation ?; simpl. + rewrite decide_False, Nat.lt_succ_r by done. apply filter_length. + Qed. +End filter. + (** ** Properties of the [prefix] and [suffix] predicates *) Global Instance: PreOrder (@prefix A). Proof.