Commit 77eecb3c authored by Robbert's avatar Robbert

Merge branch 'ralf/proper-dom' into 'master'

show a Proper instance for dom

See merge request iris/stdpp!74
parents 4978faed 4f68d8a9
Pipeline #17826 passed with stage
in 8 minutes and 29 seconds
......@@ -119,6 +119,17 @@ Proof.
eauto using (empty_finite (C:=D)), (union_finite (C:=D)),
(singleton_finite (C:=D)).
Global Instance dom_proper `{!Equiv A} : Proper ((@{M A}) ==> ()) (dom D).
intros m1 m2 EQm. apply elem_of_equiv. intros i.
rewrite !elem_of_dom, EQm. done.
(** If [D] has Leibniz equality, we can show an even stronger result. This is a
common case e.g. when having a [gmap K A] where the key [K] has Leibniz equality
(and thus also [gset K], the usual domain) but the value type [A] does not. *)
Global Instance dom_proper_L `{!Equiv A, !LeibnizEquiv D} :
Proper ((@{M A}) ==> (=)) (dom D) | 0.
Proof. intros ???. unfold_leibniz. by apply dom_proper. Qed.
Context `{!LeibnizEquiv D}.
Lemma dom_empty_L {A} : dom D (@empty (M A) _) = .
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