Heapbij util lemmas prog

theories/vir/heapbij.v

@@ -197,8 +197,61 @@ Section definitions.
   Definition target_bij_set (L : gset (loc * loc)) : gset loc :=
     gset_fmap fst L.
 
+  Lemma dom_mapset_car {X} `{!EqDecision X} `{!Countable X} A :
+    (dom A : gset X) = {| mapset_car := A |}.
+  Proof.
+    induction A as [| y Y not_in IH] using map_ind.
+    - rewrite dom_empty_L. done.
+    - rewrite dom_insert_L.
+      rewrite insert_union_singleton_l.
+      rewrite IHA. destruct Y; cbn. done.
+  Qed.
+
+  Lemma mapset_car_insert_union_singleton_l {X} `{!EqDecision X} `{!Countable X} y
+    (A : gset X):
+    mapset_car ({[y]} ∪ A) = <[ y := () ]> (mapset_car A).
+  Proof.
+    destruct A as [mX]. simpl.
+    by rewrite insert_union_singleton_l.
+  Qed.
+
+  Lemma insert_gset_fmap_fst:
+    ∀ (l_t l_s : loc) (X : gset (loc * loc)),
+      (l_t, l_s) ∉ X
+      → (λ '(a, b), (a.1, b)) <$> map_to_list (<[(l_t, l_s):=()]> (mapset_car X))
+          ≡ₚ (l_t, ()) :: ((λ '(a, b), (a.1, b)) <$> map_to_list (mapset_car X)).
+  Proof.
+    intros l_t l_s X not_in.
+    rewrite map_to_list_insert; cbn; cycle 1.
+    { destruct X. rewrite -dom_mapset_car in not_in.
+      apply not_elem_of_dom_1 in not_in. by cbn. }
+    reflexivity.
+  Qed.
+
+  Lemma insert_gset_fmap_snd:
+    ∀ (l_t l_s : loc) (X : gset (loc * loc)),
+      (l_t, l_s) ∉ X
+      → (λ '(a, b), (a.2, b)) <$> map_to_list (<[(l_t, l_s):=()]> (mapset_car X))
+          ≡ₚ (l_s, ()) :: ((λ '(a, b), (a.2, b)) <$> map_to_list (mapset_car X)).
+  Proof.
+    intros l_t l_s X not_in.
+    rewrite map_to_list_insert; cbn; cycle 1.
+    { destruct X. rewrite -dom_mapset_car in not_in.
+      apply not_elem_of_dom_1 in not_in. by cbn. }
+    reflexivity.
+  Qed.
+
+  Instance list_to_map_permute `{!Insert K A M} `{!Empty M}:
+    Proper (Permutation ==> eq) (@list_to_map K A M _ _).
+  Proof.
+    repeat intro.
+    revert y H.
+    induction x; intros; cbn.
+    { apply Permutation_nil in H; by subst. }
+  Admitted.
+
   Lemma target_bij_set_union l_t l_s L :
-    target_bij_set ({[(l_t, l_s)]} ∪ L) = {[ l_t ]} ∪ target_bij_set L.
+    target_bij_set ({[(l_t, l_s)]} ∪ L) ≡ {[ l_t ]} ∪ target_bij_set L.
   Proof.
     induction L as [| y X not_in IH] using set_ind_L.
     - rewrite union_empty_r_L.
@@ -211,19 +264,117 @@ Section definitions.
       rewrite (union_comm_L ({[(l_t, l_s)]})).
       rewrite -union_assoc_L.
       rewrite {1} /target_bij_set /gset_fmap; cbn.
+      rewrite !mapset_car_insert_union_singleton_l.
+
+      destruct (decide (y = (l_t, l_s))).
+      { subst. rewrite insert_insert.
+        pose proof (insert_gset_fmap_fst _ _ _ not_in).
+        pose proof (list_to_map_permute (M := gmap _ _) _ _ H).
+        rewrite H0; cbn; clear H0.
+        rewrite insert_union_singleton_l.
+        rewrite subseteq_union_1_L.
+        { symmetry. etransitivity.
+          - apply IH.
+          - reflexivity. }
+        rewrite /target_bij_set /gset_fmap.
+        rewrite mapset_car_insert_union_singleton_l.
+        pose proof (list_to_map_permute (M := gmap _ _) _ _ H).
+        rewrite H0; clear H0.
+        cbn. rewrite insert_union_singleton_l.
+        etransitivity.
+        { eapply union_subseteq_l. }
+        Unshelve.
+        2 : exact {| mapset_car := list_to_map ((λ '(a, b), (a.1, b)) <$> map_to_list (mapset_car X)) |}.
+        set_solver. }
 
-      assert (mapset_car ({[y]} ∪ ({[(l_t, l_s)]} ∪ X)) =
-               <[ y := () ]> (mapset_car ({[(l_t, l_s)]} ∪ X))).
-      { destruct X as [mX]. simpl.
-        by rewrite insert_union_singleton_l. }
-      rewrite H; clear H.
-
-      pose proof (map_to_list_insert (mapset_car ({[(l_t, l_s)]} ∪ X)) y tt).
-  Admitted.
+      { rewrite -mapset_car_insert_union_singleton_l.
+        assert (y ∉ ({[(l_t, l_s)]} ∪ X)).
+        { set_solver. }
+        pose proof (insert_gset_fmap_fst _ _ _ H).
+        pose proof (list_to_map_permute (M := gmap _ _) _ _ H0).
+        destruct y. cbn in *.
+        rewrite H1; cbn; clear H1.
+        rewrite insert_union_singleton_l.
+        change ({| mapset_car := {[l := ()]} ∪
+            list_to_map
+            ((λ '(a, b), (a.1, b)) <$> map_to_list (mapset_car ({[(l_t, l_s)]} ∪ X))) |}) with
+        ({[ l ]} ∪ target_bij_set ({[ (l_t, l_s) ]} ∪ X)).
+        rewrite IH; clear IH H0.
+        rewrite {2} /target_bij_set /gset_fmap.
+        rewrite mapset_car_insert_union_singleton_l.
+        pose proof (insert_gset_fmap_fst _ _ _ not_in).
+        pose proof (list_to_map_permute (M := gmap _ _) _ _ H0).
+        rewrite H1; cbn; clear H1.
+        rewrite insert_union_singleton_l.
+        change {| mapset_car :=
+          {[l := ()]} ∪
+            list_to_map ((λ '(a, b), (a.1, b)) <$> map_to_list (mapset_car X)) |} with
+          ({[ l ]} ∪ target_bij_set X).
+        set_solver. }
+  Qed.
 
   Lemma source_bij_set_union l_t l_s L :
     source_bij_set ({[(l_t, l_s)]} ∪ L) = {[ l_s ]} ∪ source_bij_set L.
-  Proof. Admitted. (* Utility *)
+  Proof.
+    induction L as [| y X not_in IH] using set_ind_L.
+    - rewrite union_empty_r_L.
+      rewrite /source_bij_set /gset_fmap; cbn.
+      rewrite map_to_list_empty; cbn.
+      rewrite union_empty_r_L.
+      rewrite map_to_list_singleton; cbn.
+      rewrite insert_empty; reflexivity.
+    - rewrite union_assoc_L.
+      rewrite (union_comm_L ({[(l_t, l_s)]})).
+      rewrite -union_assoc_L.
+      rewrite {1} /source_bij_set /gset_fmap; cbn.
+      rewrite !mapset_car_insert_union_singleton_l.
+
+      destruct (decide (y = (l_t, l_s))).
+      { subst. rewrite insert_insert.
+        pose proof (insert_gset_fmap_snd _ _ _ not_in).
+        pose proof (list_to_map_permute (M := gmap _ _) _ _ H).
+        rewrite H0; cbn; clear H0.
+        rewrite insert_union_singleton_l.
+        rewrite subseteq_union_1_L.
+        { symmetry. etransitivity.
+          - apply IH.
+          - reflexivity. }
+        rewrite /source_bij_set /gset_fmap.
+        rewrite mapset_car_insert_union_singleton_l.
+        pose proof (list_to_map_permute (M := gmap _ _) _ _ H).
+        rewrite H0; clear H0.
+        cbn. rewrite insert_union_singleton_l.
+        etransitivity.
+        { eapply union_subseteq_l. }
+        Unshelve.
+        2 : exact {| mapset_car := list_to_map ((λ '(a, b), (a.2, b)) <$> map_to_list (mapset_car X)) |}.
+        set_solver. }
+
+      { rewrite -mapset_car_insert_union_singleton_l.
+        assert (y ∉ ({[(l_t, l_s)]} ∪ X)).
+        { set_solver. }
+        pose proof (insert_gset_fmap_snd _ _ _ H).
+        pose proof (list_to_map_permute (M := gmap _ _) _ _ H0).
+        destruct y. cbn in *.
+        rewrite H1; cbn; clear H1.
+        rewrite insert_union_singleton_l.
+        change ({| mapset_car := {[l0 := ()]} ∪
+            list_to_map
+            ((λ '(a, b), (a.2, b)) <$> map_to_list (mapset_car ({[(l_t, l_s)]} ∪ X))) |}) with
+        ({[ l0 ]} ∪ source_bij_set ({[ (l_t, l_s) ]} ∪ X)).
+        rewrite IH; clear IH H0.
+        rewrite {2} /source_bij_set /gset_fmap.
+        rewrite mapset_car_insert_union_singleton_l.
+        pose proof (insert_gset_fmap_snd _ _ _ not_in).
+        pose proof (list_to_map_permute (M := gmap _ _) _ _ H0).
+        rewrite H1; cbn; clear H1.
+        rewrite insert_union_singleton_l.
+        change {| mapset_car :=
+          {[l0 := ()]} ∪
+            list_to_map ((λ '(a, b), (a.2, b)) <$> map_to_list (mapset_car X)) |} with
+          ({[ l0 ]} ∪ source_bij_set X).
+        set_solver. }
+  Qed.
 
   Lemma alloc_rel_read_None C b_t b_s σ_s σ_t v G mf L LS B:
     σ_s !! b_s = Some v →