Commit 4fea482a authored by Robbert Krebbers's avatar Robbert Krebbers

LeibnizEquiv properties for fin_maps.

parent 051644fb
...@@ -30,6 +30,10 @@ Proof. ...@@ -30,6 +30,10 @@ Proof.
Qed. Qed.
Canonical Structure mapC : cofeT := CofeT map_cofe_mixin. Canonical Structure mapC : cofeT := CofeT map_cofe_mixin.
(* why doesn't this go automatic? *)
Global Instance mapC_leibniz: LeibnizEquiv A LeibnizEquiv mapC.
Proof. intros; change (LeibnizEquiv (gmap K A)); apply _. Qed.
Global Instance lookup_ne n k : Global Instance lookup_ne n k :
Proper (dist n ==> dist n) (lookup k : gmap K A option A). Proper (dist n ==> dist n) (lookup k : gmap K A option A).
Proof. by intros m1 m2. Qed. Proof. by intros m1 m2. Qed.
...@@ -164,6 +168,8 @@ Proof. ...@@ -164,6 +168,8 @@ Proof.
* by intros m i; rewrite /= lookup_op lookup_empty (left_id_L None _). * by intros m i; rewrite /= lookup_op lookup_empty (left_id_L None _).
* apply map_empty_timeless. * apply map_empty_timeless.
Qed. Qed.
Global Instance mapRA_leibniz : LeibnizEquiv A LeibnizEquiv mapRA.
Proof. intros; change (LeibnizEquiv (gmap K A)); apply _. Qed.
(** Internalized properties *) (** Internalized properties *)
Lemma map_equivI {M} m1 m2 : (m1 m2)%I ( i, m1 !! i m2 !! i : uPred M)%I. Lemma map_equivI {M} m1 m2 : (m1 m2)%I ( i, m1 !! i m2 !! i : uPred M)%I.
......
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