Skip to content
Snippets Groups Projects
Commit fb90d2d8 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Merge branch 'ralf/map-forall-lookup' into 'master'

add map_Forall_lookup

See merge request iris/stdpp!158
parents 56a8ce93 a6d4d077
No related branches found
No related tags found
1 merge request!158add map_Forall_lookup
Pipeline #27814 passed
......@@ -1234,6 +1234,15 @@ Proof.
Qed.
Lemma map_Forall_delete m i : map_Forall P m map_Forall P (delete i m).
Proof. intros Hm j x; rewrite lookup_delete_Some. naive_solver. Qed.
Lemma map_Forall_lookup m :
map_Forall P m i x, m !! i = Some x P i x.
Proof. done. Qed.
Lemma map_Forall_lookup_1 m i x :
map_Forall P m m !! i = Some x P i x.
Proof. intros ?. by apply map_Forall_lookup. Qed.
Lemma map_Forall_lookup_2 m :
( i x, m !! i = Some x P i x) map_Forall P m.
Proof. intros ?. by apply map_Forall_lookup. Qed.
Lemma map_Forall_foldr_delete m is :
map_Forall P m map_Forall P (foldr delete m is).
Proof. induction is; eauto using map_Forall_delete. Qed.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment