Commit 2776d930 authored by Robbert Krebbers's avatar Robbert Krebbers

Support singletons in `solve_map_disjoint`.

parent b7f1f6b1
Pipeline #12598 passed with stage
in 32 minutes and 21 seconds
From stdpp Require Import fin_maps.
Section map_disjoint.
Context `{FinMap K M}.
Lemma solve_map_disjoint_singleton_1 {A} (m1 m2 : M A) i x :
m1 ## <[i:=x]> m2 {[ i:= x ]} m2 ## m1 m2 ## .
Proof. intros. solve_map_disjoint. Qed.
Lemma solve_map_disjoint_singleton_2 {A} (m1 m2 : M A) i x :
m2 !! i = None m1 ## {[ i := x ]} m2 m2 ## <[i:=x]> m1 m1 !! i = None.
Proof. intros. solve_map_disjoint. Qed.
End map_disjoint.
......@@ -1932,6 +1932,8 @@ Hint Extern 2 (_ ##ₘ {[ _ := _ ]}) =>
apply map_disjoint_singleton_r_2 : map_disjoint.
Hint Extern 2 (_ _ ## _) => apply map_disjoint_union_l_2 : map_disjoint.
Hint Extern 2 (_ ## _ _) => apply map_disjoint_union_r_2 : map_disjoint.
Hint Extern 2 ({[_:= _]} ## _) => apply map_disjoint_singleton_l : map_disjoint.
Hint Extern 2 (_ ## {[_:= _]}) => apply map_disjoint_singleton_r : map_disjoint.
Hint Extern 2 (<[_:=_]>_ ## _) => apply map_disjoint_insert_l_2 : map_disjoint.
Hint Extern 2 (_ ## <[_:=_]>_) => apply map_disjoint_insert_r_2 : map_disjoint.
Hint Extern 2 (delete _ _ ## _) => apply map_disjoint_delete_l : map_disjoint.
......
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