incorrect proof of acquire

theories/lib/flock.v

@@ -596,6 +596,15 @@ Section flock.
     by apply auth_update_alloc.
   Qed.
 
+  (* THIS IS NOT TRUE *)
+  Global Instance snd_cmramorphism :
+    CmraMorphism (@snd Qp (agree lock_res_name)).
+  Proof.
+    split; first apply _.
+    - move=> n [? ?] [// ?].
+    - move=> [a b]/=. admit.
+  Admitted.
+
   Lemma acquire_flock_spec γ lk (I : gmap prop_id lock_res) :
     {{{ is_flock γ lk ∗ [∗ map] i ↦ X ∈ I, flock_res γ i X }}}
       acquire lk
@@ -658,29 +667,76 @@ Section flock.
       iDestruct (own_valid_2 with "Haprops HI")
         as %[Hfoo _]%auth_valid_discrete_2.
 
+      (* TODO: RK, please take a look at this horrific script *)
+      (* We are going to separate the active resources I out of the fp map *)
       pose (I'' := fmap res_name I).
-      assert (∃ P', P' ##ₘ I'' ∧ fp = P' ∪ I'') as [P' HP'].
+      assert (∃ P', P' ##ₘ I'' ∧ fp ≡ P' ∪ I'') as [P' HP'].
       { subst I'' I' fa. clear H1.
+        unfold to_props_map in *.
+        pose (f := (λ X, (res_frac X, to_agree (res_name X)))).
+        pose (g := (λ X:lock_res_name, (1%Qp, to_agree X))).
+        (* Proof idea:
+          f <$> I ≼ g <$> fp
+             implies
+          snd <$> f <$> I ≼ snd <$> g <$> fp
+          =  to_agree o res_name <$> I ≼ to_agree <$> fp *)
+        assert (((snd <$> (f <$> I)) : gmapUR prop_id (agreeR lock_res_nameC)) ≼ (snd <$> (g <$> fp))) as Hbar.
+        { (* TODO: this is the /proper/ proof of the statement, but
+             the proof is incorrect because currently projections are
+             not morphisms *)
+          eapply cmra_morphism_monotone; last exact: Hfoo.
+          apply gmap_fmap_cmra_morphism. apply _.
+        }
+        rewrite -!map_fmap_compose in Hbar.
+        assert ((to_agree ∘ res_name <$> I) ≼ to_agree <$> fp) as Hbaz by exact: Hbar.
+        rewrite map_fmap_compose in Hbaz.
+
+        (* which implies the following *)
+        assert (∀ i, to_agree <$> (res_name <$> (I !! i)) ≼ to_agree <$> (fp !! i)) as Hbork.
+        { intros i. rewrite -!lookup_fmap. revert i.
+          apply lookup_included. exact: Hbaz. }
+        clear Hbaz Hbar Hfoo.
+
         generalize dependent fp.
-        induction I as [|i X I] using map_ind; intros fp.
+        induction I as [|i X I HI IHI] using map_ind; intros fp.
         + rewrite fmap_empty.
-          exists fp. admit.
+          exists fp. rewrite right_id.
+          split; first solve_map_disjoint; auto.
         + rewrite fmap_insert=>Hfp.
           specialize (IHI (delete i fp)).
-          assert ((λ X : lock_res, (res_frac X, to_agree (res_name X))) <$> I ≼ to_props_map (delete i fp)) as HLOL.
-          { (* apply lookup_included in Hfp. *)
-            admit. }
-          specialize (IHI HLOL).
+          assert (∀ j, to_agree <$> (res_name <$> I !! j)
+                         ≼ (to_agree <$> delete i fp !! j)) as goodboi.
+          { intros j.
+            destruct (decide (i = j)) as [<-|?].
+            - by rewrite HI lookup_delete.
+            - specialize (Hfp j).
+              rewrite lookup_insert_ne in Hfp; last done.
+              rewrite lookup_delete_ne //. }
+          specialize (IHI goodboi). clear goodboi.
           destruct IHI as [P [HP HU]].
           assert (P !! i = None) as HPi.
-          { admit. }
-          exists P. rewrite !fmap_insert. split.
-          * solve_map_disjoint.
-          * rewrite -insert_union_r // -HU.
-            rewrite insert_delete.
-            symmetry. apply insert_id.
-            admit. }
+          { destruct (P !! i) as [Y|] eqn:HPi; auto; simplify_eq/=.
+            exfalso. unfold_leibniz.
+            specialize (HU i). fold_leibniz.
+            rewrite (lookup_union_Some_l _ _ _ _ HPi) in HU.
+            rewrite lookup_delete in HU. done. }
+          exists P. split; first solve_map_disjoint.
+          rewrite -insert_union_r // -HU.
+          rewrite insert_delete=> j.
+          specialize (Hfp j).
+          destruct (decide (i = j)) as [<-|?].
+          * revert Hfp. rewrite !lookup_insert.
+            intros Hfp.
+            destruct (proj1( option_included _ _) Hfp)
+              as [?|(a&?&Ha&Hj&Heq)]; simplify_eq/=.
+            destruct (fp !! i) as [Y|] eqn:HY; simplify_eq/=.
+            revert Heq. rewrite to_agree_included HY.
+            intros [->%to_agree_inj | ->]; reflexivity.
+          * rewrite lookup_insert_ne //. }
+      fold_leibniz.
+
       destruct HP' as [HP' ->].
+
       rewrite /all_tokens big_sepM_union //.
       iDestruct "Htokens" as "[Htokens H]".
       rewrite /I'' big_sepM_fmap. iFrame.
@@ -692,7 +748,7 @@ Section flock.
       iFrame. iSplit; eauto.
       rewrite big_sepM_fmap.
       iApply (big_sepM_own_frag with "Hemp HI").
-  Abort.
+  Qed.
 
   Lemma release_cancel_spec' γ lk I :
     {{{ is_flock γ lk ∗ flocked γ I }}}