Commit a6d4d077 authored by Ralf Jung's avatar Ralf Jung

prove lemma in both directions

parent a6f30595
......@@ -1234,9 +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 i x :
m !! i = Some x map_Forall P m P i x.
Proof. intros Hlk Hm. by apply Hm. 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.
......
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