Add new lemmas for list, set, and map operations.

parent 3eb9d489
Pipeline #19080 canceled with stage
......@@ -1081,13 +1081,18 @@ Section map_filter.
naive_solver.
Qed.
Lemma map_filter_insert_not m i x :
( y, ¬ P (i, y)) filter P (<[i:=x]> m) = filter P m.
Lemma map_filter_insert_not' m i x :
¬ P (i, x) ( y, m !! i = Some y ¬ P (i, y))
filter P (<[i:=x]> m) = filter P m.
Proof.
intros HP. apply map_filter_lookup_eq. intros j y Hy.
by rewrite lookup_insert_ne by naive_solver.
intros Hx HP. apply map_filter_lookup_eq. intros j y Hy.
rewrite lookup_insert_Some. naive_solver.
Qed.
Lemma map_filter_insert_not m i x :
( y, ¬ P (i, y)) filter P (<[i:=x]> m) = filter P m.
Proof. intros HP. by apply map_filter_insert_not'. Qed.
Lemma map_filter_delete m i : filter P (delete i m) = delete i (filter P m).
Proof.
apply map_eq. intros j. apply option_eq; intros y.
......@@ -1106,6 +1111,16 @@ Section map_filter.
Lemma map_filter_empty : filter P ( : M A) = .
Proof. apply map_fold_empty. Qed.
Lemma map_filter_alt m : filter P m = list_to_map (filter P (map_to_list m)).
Proof.
apply list_to_map_flip. induction m as [|k x m ? IH] using map_ind.
{ by rewrite map_to_list_empty, map_filter_empty, map_to_list_empty. }
rewrite map_to_list_insert, filter_cons by done. destruct (decide (P _)).
- rewrite map_filter_insert by done.
by rewrite map_to_list_insert, IH by (rewrite map_filter_lookup_None; auto).
- by rewrite map_filter_insert_not' by naive_solver.
Qed.
End map_filter.
(** ** Properties of the [map_Forall] predicate *)
......
......@@ -279,6 +279,13 @@ Section gset.
- by rewrite option_guard_True by (rewrite elem_of_dom; eauto).
- by rewrite option_guard_False by (rewrite not_elem_of_dom; eauto).
Qed.
Lemma dom_gset_to_gmap {A} (X : gset K) (x : A) :
dom _ (gset_to_gmap x X) = X.
Proof.
induction X as [| y X not_in IH] using set_ind_L.
- rewrite gset_to_gmap_empty, dom_empty_L; done.
- rewrite gset_to_gmap_union_singleton, dom_insert_L, IH; done.
Qed.
End gset.
Typeclasses Opaque gset.
......@@ -668,6 +668,42 @@ Proof.
revert i j. induction k; intros i j ?; simpl;
rewrite 1?list_insert_commute by lia; auto with f_equal.
Qed.
Lemma list_inserts_app_l l1 l2 l3 i :
list_inserts i (l1 ++ l2) l3 = list_inserts (length l1 + i) l2 (list_inserts i l1 l3).
Proof.
revert l1 i; induction l1 as [|x l1 IH]; [done|].
intro i. simpl. rewrite IH, Nat.add_succ_r. apply list_insert_inserts_lt. lia.
Qed.
Lemma list_inserts_app_r l1 l2 l3 i :
list_inserts (length l2 + i) l1 (l2 ++ l3) = l2 ++ list_inserts i l1 l3.
Proof.
revert l1 i; induction l1 as [|x l1 IH]; [done|].
intros i. simpl. by rewrite plus_n_Sm, IH, insert_app_r.
Qed.
Lemma list_inserts_nil l1 i : list_inserts i l1 [] = [].
Proof.
revert i; induction l1 as [|x l1 IH]; [done|].
intro i. simpl. by rewrite IH.
Qed.
Lemma list_inserts_cons l1 l2 i x :
list_inserts (S i) l1 (x :: l2) = x :: list_inserts i l1 l2.
Proof.
revert i; induction l1 as [|y l1 IH]; [done|].
intro i. simpl. by rewrite IH.
Qed.
Lemma list_inserts_0_r l1 l2 l3 :
length l1 = length l2 list_inserts 0 l1 (l2 ++ l3) = l1 ++ l3.
Proof.
revert l2. induction l1 as [|x l1 IH]; intros [|y l2] ?; simplify_eq/=; [done|].
rewrite list_inserts_cons. simpl. by rewrite IH.
Qed.
Lemma list_inserts_0_l l1 l2 l3 :
length l1 = length l3 list_inserts 0 (l1 ++ l2) l3 = l1.
Proof.
revert l3. induction l1 as [|x l1 IH]; intros [|z l3] ?; simplify_eq/=.
{ by rewrite list_inserts_nil. }
rewrite list_inserts_cons. simpl. by rewrite IH.
Qed.
(** ** Properties of the [elem_of] predicate *)
Lemma not_elem_of_nil x : x [].
......
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