Commit a01453ed authored by Robbert Krebbers's avatar Robbert Krebbers

Relate map_to_list to nil.

parent 8b9a96ad
......@@ -707,6 +707,11 @@ Lemma map_to_list_empty_inv_alt {A} (m : M A) : map_to_list m ≡ₚ [] → m =
Proof. rewrite <-map_to_list_empty. apply map_to_list_inj. Qed.
Lemma map_to_list_empty_inv {A} (m : M A) : map_to_list m = [] m = .
Proof. intros Hm. apply map_to_list_empty_inv_alt. by rewrite Hm. Qed.
Lemma map_to_list_empty' {A} (m : M A) : map_to_list m = [] m = .
Proof.
split. apply map_to_list_empty_inv. intros ->. apply map_to_list_empty.
Qed.
Lemma map_to_list_insert_inv {A} (m : M A) l i x :
map_to_list m ≡ₚ (i,x) :: l m = <[i:=x]>(map_of_list l).
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