Commit 13680b70 authored by Robbert Krebbers's avatar Robbert Krebbers

Properties about maps and is_Some.

parent 8ee34859
......@@ -337,6 +337,9 @@ Proof.
rewrite ?lookup_delete, ?lookup_delete_ne; intuition congruence.
* intros [??]. by rewrite lookup_delete_ne.
Qed.
Lemma lookup_delete_is_Some {A} (m : M A) i j :
is_Some (delete i m !! j) i j is_Some (m !! j).
Proof. unfold is_Some; setoid_rewrite lookup_delete_Some; naive_solver. Qed.
Lemma lookup_delete_None {A} (m : M A) i j :
delete i m !! j = None i = j m !! j = None.
Proof.
......@@ -411,6 +414,9 @@ Proof.
rewrite ?lookup_insert, ?lookup_insert_ne; intuition congruence.
* intros [[-> ->]|[??]]; [apply lookup_insert|]. by rewrite lookup_insert_ne.
Qed.
Lemma lookup_insert_is_Some {A} (m : M A) i j x :
is_Some (<[i:=x]>m !! j) i = j i j is_Some (m !! j).
Proof. unfold is_Some; setoid_rewrite lookup_insert_Some; naive_solver. Qed.
Lemma lookup_insert_None {A} (m : M A) i j x :
<[i:=x]>m !! j = None m !! j = None i j.
Proof.
......
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