Skip to content
Snippets Groups Projects

Add `set_solver` support for `dom`

Merged Robbert Krebbers requested to merge robbert/set_unfold_dom into master
Files
3
+ 12
1
From stdpp Require Import fin_maps.
From stdpp Require Import fin_maps fin_map_dom.
Section map_disjoint.
Context `{FinMap K M}.
@@ -11,3 +11,14 @@ Section map_disjoint.
m2 !! i = None m1 ## {[ i := x ]} m2 m2 ## <[i:=x]> m1 m1 !! i = None.
Proof. intros. solve_map_disjoint. Qed.
End map_disjoint.
Section map_dom.
Context `{FinMapDom K M D}.
Lemma set_solver_dom_subseteq {A} (i j : K) (x y : A) :
{[i; j]} dom D (<[i:=x]> (<[j:=y]> ( : M A))).
Proof. set_solver. Qed.
Lemma set_solver_dom_disjoint {A} (X : D) : dom D ( : M A) ## X.
Proof. set_solver. Qed.
End map_dom.
Loading