Commit f37ad033 authored by Rodolphe Lepigre's avatar Rodolphe Lepigre Committed by Robbert

More lemmas about [map_imap].

parent d983fe55
...@@ -4,7 +4,7 @@ API-breaking change is listed. ...@@ -4,7 +4,7 @@ API-breaking change is listed.
## std++ 1.2.1 (unreleased) ## std++ 1.2.1 (unreleased)
This release of std++ received contributions by Michael Sammler, Paolo This release of std++ received contributions by Michael Sammler, Paolo
G. Giarrusso, Ralf Jung, Robbert Krebbers, and Simon Spies. G. Giarrusso, Ralf Jung, Robbert Krebbers, Simon Spies, and Rodolphe Lepigre.
Noteworthy additions and changes: Noteworthy additions and changes:
...@@ -13,6 +13,7 @@ Noteworthy additions and changes: ...@@ -13,6 +13,7 @@ Noteworthy additions and changes:
- Add typeclass `Involutive`. - Add typeclass `Involutive`.
- Improved `naive_solver` performance in case the goal is trivially solvable. - 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 operations.
- `lookup_imap` renamed into `map_lookup_imap`.
## std++ 1.2.0 (released 2019-04-26) ## std++ 1.2.0 (released 2019-04-26)
......
...@@ -860,7 +860,7 @@ Proof. ...@@ -860,7 +860,7 @@ Proof.
Defined. Defined.
(** Properties of the imap function *) (** Properties of the imap function *)
Lemma lookup_imap {A B} (f : K A option B) (m : M A) i : Lemma map_lookup_imap {A B} (f : K A option B) (m : M A) i :
map_imap f m !! i = m !! i = f i. map_imap f m !! i = m !! i = f i.
Proof. Proof.
unfold map_imap; destruct (m !! i = f i) as [y|] eqn:Hi; simpl. unfold map_imap; destruct (m !! i = f i) as [y|] eqn:Hi; simpl.
...@@ -876,6 +876,39 @@ Proof. ...@@ -876,6 +876,39 @@ Proof.
rewrite elem_of_map_to_list in Hj; simplify_option_eq. rewrite elem_of_map_to_list in Hj; simplify_option_eq.
Qed. Qed.
Lemma map_imap_Some {A} (m : M A) : map_imap (λ _, Some) m = m.
Proof.
apply map_eq. intros i. rewrite map_lookup_imap. by destruct (m !! i).
Qed.
Lemma map_imap_insert {A B} (f : K A option B) (i : K) (v : A) (m : M A) :
map_imap f (<[i:=v]> m) = match f i v with
| None => delete i (map_imap f m)
| Some w => <[i:=w]> (map_imap f m)
end.
Proof.
destruct (f i v) as [w|] eqn:Hw.
- apply map_eq. intros k. rewrite map_lookup_imap.
destruct (decide (k = i)) as [->|Hk_not_i].
+ by rewrite lookup_insert, lookup_insert.
+ rewrite !lookup_insert_ne by done.
by rewrite map_lookup_imap.
- apply map_eq. intros k. rewrite map_lookup_imap.
destruct (decide (k = i)) as [->|Hk_not_i].
+ by rewrite lookup_insert, lookup_delete.
+ rewrite lookup_insert_ne, lookup_delete_ne by done.
by rewrite map_lookup_imap.
Qed.
Lemma map_imap_ext {A1 A2 B} (f1 : K A1 option B)
(f2 : K A2 option B) (m1 : M A1) (m2 : M A2) :
( k, f1 k <$> (m1 !! k) = f2 k <$> (m2 !! k))
map_imap f1 m1 = map_imap f2 m2.
Proof.
intros HExt. apply map_eq. intros i. rewrite !map_lookup_imap.
specialize (HExt i). destruct (m1 !! i), (m2 !! i); naive_solver.
Qed.
(** ** Properties of the size operation *) (** ** Properties of the size operation *)
Lemma map_size_empty {A} : size ( : M A) = 0. Lemma map_size_empty {A} : size ( : M A) = 0.
Proof. unfold size, map_size. by rewrite map_to_list_empty. Qed. Proof. unfold size, map_size. by rewrite map_to_list_empty. Qed.
......
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