Commit 9fbc1013 authored by Robbert Krebbers's avatar Robbert Krebbers

No longer break `gset` abstraction.

parent 8d7d9979
Pipeline #15732 failed with stage
in 10 minutes and 56 seconds
......@@ -80,7 +80,7 @@ Definition Gmon_graph (G : Gmon) : graph loc := omap excl_chlC_chl G.
Definition Gmon_graph_dom (G : Gmon) :
G dom (gset loc) (Gmon_graph G) = dom (gset _) G.
Proof.
intros Hvl; apply mapset_eq => i. rewrite ?elem_of_dom lookup_omap.
intros Hvl; apply elem_of_equiv_L=> i. rewrite !elem_of_dom lookup_omap.
specialize (Hvl i). split.
- revert Hvl; case _ : (G !! i) => [[]|] //=; eauto.
intros _ [? Hgi]; inversion Hgi.
......@@ -230,7 +230,7 @@ Proof. intros H. by rewrite lookup_op lookup_singleton_ne //= left_id_L. Qed.
Lemma of_graph_dom g G : dom (gset loc) (of_graph g G) = dom (gset _) g.
Proof.
apply mapset_eq=>i.
apply elem_of_equiv_L=>i.
rewrite ?elem_of_dom lookup_imap /of_graph_elem lookup_omap.
case _ : (g !! i) => [x|]; case _ : (G !! i) => [[]|] //=; split;
intros [? Hcn]; inversion Hcn; eauto.
......
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