Commit 84719674 authored by Robbert Krebbers's avatar Robbert Krebbers

Add a variant of lookup_insert_is_Some.

parent 3103b7bf
......@@ -425,6 +425,9 @@ 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_is_Some' {A} (m : M A) i j x :
is_Some (<[i:=x]>m !! j) i = j is_Some (m !! j).
Proof. rewrite lookup_insert_is_Some. destruct (decide (i=j)); 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