Commit 48067dec authored by Robbert's avatar Robbert

Merge branch 'master' into 'master'

Several simple lemmas.

See merge request iris/stdpp!85
parents f9830af6 6bc8803a
Pipeline #19084 passed with stage
in 9 minutes and 5 seconds
......@@ -4,7 +4,8 @@ API-breaking change is listed.
## std++ 1.2.1 (unreleased)
This release of std++ received contributions by Michael Sammler, Paolo
G. Giarrusso, Ralf Jung, Robbert Krebbers, Simon Spies, and Rodolphe Lepigre.
G. Giarrusso, Ralf Jung, Robbert Krebbers, Simon Spies, Rodolphe Lepigre and
Paulo Emílio de Vilhena.
Noteworthy additions and changes:
......@@ -12,7 +13,7 @@ Noteworthy additions and changes:
- Make `solve_ndisj` tactic more powerful.
- Add typeclass `Involutive`.
- Improved `naive_solver` performance in case the goal is trivially solvable.
- A bunch of new lemmas for list operations.
- A bunch of new lemmas for list, set, and map operations.
- `lookup_imap` renamed into `map_lookup_imap`.
## std++ 1.2.0 (released 2019-04-26)
......
......@@ -1114,13 +1114,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.
......@@ -1139,6 +1144,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