prove that we can allocate an auth

algebra/cmra.v

@@ -601,14 +601,16 @@ Section iprod_cmra.
     { move: (Hg x). by rewrite iprod_lookup_op iprod_lookup_insert. }
     exists (iprod_insert x y2 g); split; [auto|].
     intros x'; destruct (decide (x' = x)) as [->|];
-      rewrite iprod_lookup_op ?iprod_lookup_insert //.
+      rewrite iprod_lookup_op ?iprod_lookup_insert //; [].
     move: (Hg x'). by rewrite iprod_lookup_op !iprod_lookup_insert_ne.
   Qed.
+
   Lemma iprod_insert_updateP' x (P : B x → Prop) g y1 :
     y1 ~~>: P →
     iprod_insert x y1 g ~~>: λ g', ∃ y2, g' = iprod_insert x y2 g ∧ P y2.
   Proof. eauto using iprod_insert_updateP. Qed.
   Lemma iprod_insert_update g x y1 y2 :
+
     y1 ~~> y2 → iprod_insert x y1 g ~~> iprod_insert x y2 g.
   Proof.
     rewrite !cmra_update_updateP;
@@ -623,14 +625,30 @@ Section iprod_cmra.
     * by rewrite iprod_lookup_op !iprod_lookup_singleton.
     * by rewrite iprod_lookup_op !iprod_lookup_singleton_ne // left_id.
   Qed.
+
   Lemma iprod_singleton_updateP x (P : B x → Prop) (Q : iprod B → Prop) y1 :
     y1 ~~>: P → (∀ y2, P y2 → Q (iprod_singleton x y2)) →
     iprod_singleton x y1 ~~>: Q.
   Proof. rewrite /iprod_singleton; eauto using iprod_insert_updateP. Qed.
+
   Lemma iprod_singleton_updateP' x (P : B x → Prop) y1 :
     y1 ~~>: P →
     iprod_singleton x y1 ~~>: λ g', ∃ y2, g' = iprod_singleton x y2 ∧ P y2.
   Proof. eauto using iprod_singleton_updateP. Qed.
+
+  Lemma iprod_singleton_updateP_empty x (P : B x → Prop) (Q : iprod B → Prop) :
+    (∅ ~~>: P) → (∀ y2, P y2 → Q (iprod_singleton x y2)) →
+    ∅ ~~>: Q.
+  Proof.
+    intros Hx HQ gf n Hg. destruct (Hx (gf x) n) as (y2&?&?).
+    { apply: Hg. }
+    exists (iprod_singleton x y2).
+    split; first by apply HQ.
+    intros x'; destruct (decide (x' = x)) as [->|];
+      rewrite iprod_lookup_op /iprod_singleton ?iprod_lookup_insert //; [].
+    move:(Hg x'). by rewrite iprod_lookup_insert_ne // left_id.
+  Qed.
+
   Lemma iprod_singleton_update x y1 y2 :
     y1 ~~> y2 → iprod_singleton x y1 ~~> iprod_singleton x y2.
   Proof. by intros; apply iprod_insert_update. Qed.

program_logic/auth.v

-Require Export algebra.auth.
-Require Import program_logic.functor program_logic.language program_logic.weakestpre.
+Require Export algebra.auth algebra.functor.
+Require Import program_logic.language program_logic.weakestpre.
+Import uPred.
 
 (* RJ: This is a work-in-progress playground.
    FIXME: Finish or remove. *)
@@ -42,20 +43,22 @@ Section auth.
     rewrite /tr' /tr. by destruct Ci.
   Qed.
 
-  Definition Tr j {H : i = j} (c: C i) : C j.
-  rewrite -H. exact c. Defined.
+  Lemma A_val a :
+    ✓a = ✓(tr a).
+  Proof.
+    rewrite /tr. by destruct Ci.
+  Qed.
 
   (* FIXME RJ: I'd rather not have to specify Σ by hand here. *)
-  Definition ownNothing : iProp Λ Σ := ownG (Σ:=Σ) (fun j => (∅ : mapRA positive (C j))).
+  Definition A2m (p : positive) (a : authRA A) : iGst Λ Σ :=
+    iprod_singleton i (<[p:=tr a]>∅).
   Definition ownA (p : positive) (a : authRA A) : iProp Λ Σ :=
-    ownG (Σ:=Σ) (fun j => match decide (i = j) with
-                                | left Heq => <[p:=Tr j (H:=Heq) $ tr a]>∅
-                                | right Hneq => ∅ end).
+    ownG (Σ:=Σ) (A2m p a).
 
   Lemma ownA_op p a1 a2 :
     (ownA p a1 ★ ownA p a2)%I ≡ ownA p (a1 ⋅ a2).
   Proof.
-    rewrite /ownA -ownG_op. apply ownG_proper=>j /=.
+    rewrite /ownA /A2m /iprod_singleton /iprod_insert -ownG_op. apply ownG_proper=>j /=.
     rewrite iprod_lookup_op. destruct (decide (i = j)).
     - move=>q. destruct e. rewrite lookup_op /=.
       destruct (decide (p = q)); first subst q.
@@ -67,6 +70,22 @@ Section auth.
     - by rewrite left_id.
   Qed.
 
+  (* TODO: This also holds if we just have ✓a at the current step-idx, as Iris
+     assertion. However, the map_updateP_alloc does not suffice to show this. *)
+  Lemma ownA_alloc E a :
+    ✓a → True ⊑ pvs E E (∃ p, ownA p a).
+  Proof.
+    intros Ha. set (P m := ∃ p, m = A2m p a).
+    set (a' := tr a).
+    rewrite -(pvs_mono _ _ (∃ m, ■P m ∧ ownG m)%I).
+    - rewrite -pvs_updateP_empty //; [].
+      subst P. eapply (iprod_singleton_updateP_empty i).
+      + eapply map_updateP_alloc' with (x:=a'). subst a'.
+        by rewrite -A_val.
+      + simpl. move=>? [p [-> ?]]. exists p. done.
+    - apply exist_elim=>m. apply const_elim_l.
+      move=>[p ->] {P}. by rewrite -(exist_intro p).
+  Qed.      
+    
 End auth.
 
-