From a1527a825c9b18e6cc8105b657ac7ea942d0fa2c Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 18 Feb 2015 15:12:46 +0100
Subject: [PATCH] port iris_vs

---
 iris_core.v      |  57 +++++-----
 iris_vs.v        | 280 +++++++++++++++++++++--------------------------
 iris_wp.v        |   2 +
 lib/ModuRes/RA.v |  65 +++++++++--
 4 files changed, 211 insertions(+), 193 deletions(-)

diff --git a/iris_core.v b/iris_core.v
index a55a82d96..0768793fd 100644
--- a/iris_core.v
+++ b/iris_core.v
@@ -1,6 +1,9 @@
+Require Import ssreflect.
 Require Import world_prop core_lang masks.
 Require Import ModuRes.RA ModuRes.UPred ModuRes.BI ModuRes.PreoMet ModuRes.Finmap.
 
+Set Bullet Behavior "Strict Subproofs".
+
 Module IrisRes (RL : RA_T) (C : CORE_LANG) <: RA_T.
   Instance state_type : Setoid C.state := discreteType.
   
@@ -67,7 +70,7 @@ Module IrisCore (RL : RA_T) (C : CORE_LANG).
     Program Definition box : Props -n> Props :=
       n[(fun p => m[(fun w => mkUPred (fun n r => p w n ra_pos_unit) _)])].
     Next Obligation.
-      intros n m r s HLe _ Hp; rewrite HLe; assumption.
+      intros n m r s HLe _ Hp; rewrite-> HLe; assumption.
     Qed.
     Next Obligation.
       intros w1 w2 EQw m r HLt; simpl.
@@ -91,7 +94,7 @@ Module IrisCore (RL : RA_T) (C : CORE_LANG).
     Program Definition intEqP (t1 t2 : T) : UPred pres :=
       mkUPred (fun n r => t1 = S n = t2) _.
     Next Obligation.
-      intros n1 n2 _ _ HLe _; apply mono_dist; now auto with arith.
+      intros n1 n2 _ _ HLe _; apply mono_dist; omega.
     Qed.
 
     Definition intEq (t1 t2 : T) : Props := pcmconst (intEqP t1 t2).
@@ -101,7 +104,7 @@ Module IrisCore (RL : RA_T) (C : CORE_LANG).
       intros l1 l2 EQl r1 r2 EQr n r.
       split; intros HEq; do 2 red.
       - rewrite <- EQl, <- EQr; assumption.
-      - rewrite EQl, EQr; assumption.
+      - rewrite ->EQl, EQr; assumption.
     Qed.
 
     Instance intEq_dist n : Proper (dist n ==> dist n ==> dist n) intEqP.
@@ -187,7 +190,7 @@ Module IrisCore (RL : RA_T) (C : CORE_LANG).
       ownR (u · t) == ownR u * ownR t.
     Proof.
       intros w n r; split; [intros Hut | intros [r1 [r2 [EQr [Hu Ht] ] ] ] ].
-      - destruct Hut as [s Heq]. rewrite assoc in Heq.
+      - destruct Hut as [s Heq]. rewrite-> assoc in Heq.
         exists✓ (s · u) by auto_valid.
         exists✓ t by auto_valid.
         split; [|split].
@@ -217,7 +220,7 @@ Module IrisCore (RL : RA_T) (C : CORE_LANG).
 
     (** Proper ghost state: ownership of logical **)
     Program Definition ownL : RL.res -n> Props :=
-      n[(fun r => ownR (ex_unit _, r))].
+      n[(fun r => ownR (1%ra, r))].
     Next Obligation.
       intros r1 r2 EQr. destruct n as [| n]; [apply dist_bound |eapply dist_refl].
       simpl in EQr. intros w m t. simpl. change ( (ex_unit state, r1) ⊑ (ra_proj t) <->  (ex_unit state, r2) ⊑ (ra_proj t)). rewrite EQr. reflexivity.
@@ -271,7 +274,7 @@ Module IrisCore (RL : RA_T) (C : CORE_LANG).
     m[(fun w => mkUPred (fun n r => timelessP p w n) _)].
   Next Obligation.
     intros n1 n2 _ _ HLe _ HT w' k r HSw HLt Hp; eapply HT, Hp; [eassumption |].
-    now eauto with arith.
+    omega.
   Qed.
   Next Obligation.
     intros w1 w2 EQw k; simpl; intros _ HLt; destruct n as [| n]; [now inversion HLt |].
@@ -304,48 +307,48 @@ Module IrisCore (RL : RA_T) (C : CORE_LANG).
     Lemma comp_list_app rs1 rs2 :
       comp_list (rs1 ++ rs2) == comp_list rs1 · comp_list rs2.
     Proof.
-      induction rs1; simpl comp_list; [now rewrite ra_op_unit by apply _ |].
-      now rewrite IHrs1, assoc.
+      induction rs1; simpl comp_list; [now rewrite ->ra_op_unit by apply _ |].
+      now rewrite ->IHrs1, assoc.
     Qed.
 
     Definition cod (m : nat -f> pres) : list pres := List.map snd (findom_t m).
     Definition comp_map (m : nat -f> pres) : res := comp_list (cod m).
 
-    Lemma comp_map_remove (rs : nat -f> pres) i r (HLu : rs i = Some r) :
+    Lemma comp_map_remove (rs : nat -f> pres) i r (HLu : rs i == Some r) :
       comp_map rs == ra_proj r · comp_map (fdRemove i rs).
     Proof.
       destruct rs as [rs rsP]; unfold comp_map, cod, findom_f in *; simpl findom_t in *.
-      induction rs as [| [j s] ]; [discriminate |]; simpl comp_list; simpl in HLu.
-      destruct (comp i j); [inversion HLu; reflexivity | discriminate |].
-      simpl comp_list; rewrite IHrs by eauto using SS_tail.
-      rewrite !assoc, (comm (_ s)); reflexivity.
+      induction rs as [| [j s] ]; [contradiction |]; simpl comp_list; simpl in HLu.
+      destruct (comp i j); [do 5 red in HLu; rewrite-> HLu; reflexivity | contradiction |].
+      simpl comp_list; rewrite ->IHrs by eauto using SS_tail.
+      rewrite-> !assoc, (comm (_ s)); reflexivity.
     Qed.
 
-    Lemma comp_map_insert_new (rs : nat -f> pres) i r (HNLu : rs i = None) :
+    Lemma comp_map_insert_new (rs : nat -f> pres) i r (HNLu : rs i == None) :
       ra_proj r · comp_map rs == comp_map (fdUpdate i r rs).
     Proof.
       destruct rs as [rs rsP]; unfold comp_map, cod, findom_f in *; simpl findom_t in *.
       induction rs as [| [j s] ]; [reflexivity | simpl comp_list; simpl in HNLu].
-      destruct (comp i j); [discriminate | reflexivity |].
+      destruct (comp i j); [contradiction | reflexivity |].
       simpl comp_list; rewrite <- IHrs by eauto using SS_tail.
-      rewrite !assoc, (comm (_ r)); reflexivity.
+      rewrite-> !assoc, (comm (_ r)); reflexivity.
     Qed.
 
     Lemma comp_map_insert_old (rs : nat -f> pres) i r1 r2 r
-          (HLu : rs i = Some r1) (HEq : ra_proj r1 · ra_proj r2 == ra_proj r) :
+          (HLu : rs i == Some r1) (HEq : ra_proj r1 · ra_proj r2 == ra_proj r) :
       ra_proj r2 · comp_map rs == comp_map (fdUpdate i r rs).
     Proof.
       destruct rs as [rs rsP]; unfold comp_map, cod, findom_f in *; simpl findom_t in *.
-      induction rs as [| [j s] ]; [discriminate |]; simpl comp_list; simpl in HLu.
-      destruct (comp i j); [inversion HLu; subst; clear HLu | discriminate |].
-      - simpl comp_list; rewrite assoc, (comm (_ r2)), <- HEq; reflexivity.
+      induction rs as [| [j s] ]; [contradiction |]; simpl comp_list; simpl in HLu.
+      destruct (comp i j); [do 5 red in HLu; rewrite-> HLu; clear HLu | contradiction |].
+      - simpl comp_list; rewrite ->assoc, (comm (_ r2)), <- HEq; reflexivity.
       - simpl comp_list; rewrite <- IHrs by eauto using SS_tail.
-        rewrite !assoc, (comm (_ r2)); reflexivity.
+        rewrite-> !assoc, (comm (_ r2)); reflexivity.
     Qed.
 
     Definition state_sat (r: res) σ: Prop := ✓r /\
-      match r with
-        | (ex_own s, _) => s = σ
+      match fst r with
+        | ex_own s => s = σ
         | _ => True
       end.
 
@@ -386,17 +389,17 @@ Module IrisCore (RL : RA_T) (C : CORE_LANG).
       split; intros [rs [HE HM] ]; exists rs.
       - split; [assumption | split; [rewrite <- (domeq _ _ _ EQw); apply HM, Hm |] ].
         intros; destruct (HM _ Hm) as [_ HR]; clear HE HM Hm.
-        assert (EQÏ€ := EQw i); rewrite HLw in EQÏ€; clear HLw.
+        assert (EQÏ€ := EQw i); rewrite-> HLw in EQÏ€; clear HLw.
         destruct (w1 i) as [Ï€' |]; [| contradiction]; do 3 red in EQÏ€.
         apply ı in EQπ; apply EQπ; [now auto with arith |].
-        apply (met_morph_nonexp _ _ (ı π')) in EQw; apply EQw; [now auto with arith |].
+        apply (met_morph_nonexp _ _ (ı π')) in EQw; apply EQw; [omega |].
         apply HR; [reflexivity | assumption].
       - split; [assumption | split; [rewrite (domeq _ _ _ EQw); apply HM, Hm |] ].
         intros; destruct (HM _ Hm) as [_ HR]; clear HE HM Hm.
-        assert (EQÏ€ := EQw i); rewrite HLw in EQÏ€; clear HLw.
+        assert (EQÏ€ := EQw i); rewrite-> HLw in EQÏ€; clear HLw.
         destruct (w2 i) as [Ï€' |]; [| contradiction]; do 3 red in EQÏ€.
         apply ı in EQπ; apply EQπ; [now auto with arith |].
-        apply (met_morph_nonexp _ _ (ı π')) in EQw; apply EQw; [now auto with arith |].
+        apply (met_morph_nonexp _ _ (ı π')) in EQw; apply EQw; [omega |].
         apply HR; [reflexivity | assumption].
     Qed.
 
diff --git a/iris_vs.v b/iris_vs.v
index f28b541bc..d11ee2cde 100644
--- a/iris_vs.v
+++ b/iris_vs.v
@@ -1,7 +1,10 @@
+Require Import ssreflect.
 Require Import world_prop core_lang masks iris_core.
-Require Import ModuRes.PCM ModuRes.UPred ModuRes.BI ModuRes.PreoMet ModuRes.Finmap.
+Require Import ModuRes.RA ModuRes.UPred ModuRes.BI ModuRes.PreoMet ModuRes.Finmap.
 
-Module IrisVS (RL : PCM_T) (C : CORE_LANG).
+Set Bullet Behavior "Strict Subproofs".
+
+Module IrisVS (RL : RA_T) (C : CORE_LANG).
   Module Export CORE := IrisCore RL C.
 
   Delimit Scope iris_scope with iris.
@@ -9,27 +12,27 @@ Module IrisVS (RL : PCM_T) (C : CORE_LANG).
 
   Section ViewShifts.
     Local Open Scope mask_scope.
-    Local Open Scope pcm_scope.
+    Local Open Scope ra_scope.
     Local Obligation Tactic := intros.
 
-    Program Definition preVS (m1 m2 : mask) (p : Props) (w : Wld) : UPred res :=
-      mkUPred (fun n r => forall w1 rf mf σ k (HSub : w ⊑ w1) (HLe : k < n)
+    Program Definition preVS (m1 m2 : mask) (p : Props) (w : Wld) : UPred pres :=
+      mkUPred (fun n r => forall w1 (rf: res) mf σ k (HSub : w ⊑ w1) (HLe : k < n)
                                  (HD : mf # m1 ∪ m2)
-                                 (HE : wsat σ (m1 ∪ mf) (Some r · rf) w1 @ S k),
+                                 (HE : wsat σ (m1 ∪ mf) (ra_proj r · rf) w1 @ S k),
                           exists w2 r',
                             w1 ⊑ w2 /\ p w2 (S k) r'
-                            /\ wsat σ (m2 ∪ mf) (Some r' · rf) w2 @ S k) _.
+                            /\ wsat σ (m2 ∪ mf) (r' · rf) w2 @ S k) _.
     Next Obligation.
       intros n1 n2 r1 r2 HLe [rd HR] HP; intros.
-      destruct (HP w1 (Some rd · rf) mf σ k) as [w2 [r1' [HW [HP' HE'] ] ] ];
+      destruct (HP w1 (rd · rf) mf σ k) as [w2 [r1' [HW [HP' HE'] ] ] ];
         try assumption; [now eauto with arith | |].
       - eapply wsat_equiv, HE; try reflexivity.
-        rewrite assoc, (comm (Some r1)), HR; reflexivity.
-      - rewrite assoc, (comm (Some r1')) in HE'.
-        destruct (Some rd · Some r1') as [r2' |] eqn: HR';
-          [| apply wsat_not_empty in HE'; [contradiction | now erewrite !pcm_op_zero by apply _] ].
-        exists w2 r2'; split; [assumption | split; [| assumption] ].
-        eapply uni_pred, HP'; [| exists rd; rewrite HR']; reflexivity.
+        rewrite ->assoc, (comm (_ r1)), HR; reflexivity.
+      - rewrite ->assoc, (comm (_ r1')) in HE'.
+        exists w2. exists✓ (rd · ra_proj r1').
+        { apply wsat_not_empty in HE'. auto_valid. }
+        split; [assumption | split; [| assumption] ].
+        eapply uni_pred, HP'; [reflexivity|]. exists rd. reflexivity.
     Qed.
 
     Program Definition pvs (m1 m2 : mask) : Props -n> Props :=
@@ -39,20 +42,20 @@ Module IrisVS (RL : PCM_T) (C : CORE_LANG).
       - symmetry in EQw; assert (HDE := extend_dist _ _ _ _ EQw HSub).
         assert (HSE := extend_sub _ _ _ _ EQw HSub); specialize (HP (extend w2' w1)).
         edestruct HP as [w1'' [r' [HW HH] ] ]; try eassumption; clear HP; [ | ].
-        + eapply wsat_dist, HE; [symmetry; eassumption | now eauto with arith].
+        + eapply wsat_dist, HE; [symmetry; eassumption | omega].
         + symmetry in HDE; assert (HDE' := extend_dist _ _ _ _ HDE HW).
           assert (HSE' := extend_sub _ _ _ _ HDE HW); destruct HH as [HP HE'];
           exists (extend w1'' w2') r'; split; [assumption | split].
-          * eapply (met_morph_nonexp _ _ p), HP ; [symmetry; eassumption | now eauto with arith].
-          * eapply wsat_dist, HE'; [symmetry; eassumption | now eauto with arith].
+          * eapply (met_morph_nonexp _ _ p), HP ; [symmetry; eassumption | omega].
+          * eapply wsat_dist, HE'; [symmetry; eassumption | omega].
       - assert (HDE := extend_dist _ _ _ _ EQw HSub); assert (HSE := extend_sub _ _ _ _ EQw HSub); specialize (HP (extend w2' w2)).
         edestruct HP as [w1'' [r' [HW HH] ] ]; try eassumption; clear HP; [ | ].
-        + eapply wsat_dist, HE; [symmetry; eassumption | now eauto with arith].
+        + eapply wsat_dist, HE; [symmetry; eassumption | omega].
         + symmetry in HDE; assert (HDE' := extend_dist _ _ _ _ HDE HW).
           assert (HSE' := extend_sub _ _ _ _ HDE HW); destruct HH as [HP HE'];
           exists (extend w1'' w2') r'; split; [assumption | split].
-          * eapply (met_morph_nonexp _ _ p), HP ; [symmetry; eassumption | now eauto with arith].
-          * eapply wsat_dist, HE'; [symmetry; eassumption | now eauto with arith].
+          * eapply (met_morph_nonexp _ _ p), HP ; [symmetry; eassumption | omega].
+          * eapply wsat_dist, HE'; [symmetry; eassumption | omega].
     Qed.
     Next Obligation.
       intros w1 w2 EQw n r HP w2'; intros; eapply HP; try eassumption; [].
@@ -75,7 +78,7 @@ Module IrisVS (RL : PCM_T) (C : CORE_LANG).
 
   Section ViewShiftProps.
     Local Open Scope mask_scope.
-    Local Open Scope pcm_scope.
+    Local Open Scope ra_scope.
     Local Open Scope bi_scope.
 
     Implicit Types (p q r : Props) (i : nat) (m : mask).
@@ -85,11 +88,11 @@ Module IrisVS (RL : PCM_T) (C : CORE_LANG).
     Lemma vsTimeless m p :
       timeless p ⊑ vs m m (▹ p) p.
     Proof.
-      intros w' n r1 HTL w HSub; rewrite HSub in HTL; clear w' HSub.
+      intros w' n r1 HTL w HSub; rewrite ->HSub in HTL; clear w' HSub.
       intros np rp HLe HS Hp w1; intros.
       exists w1 rp; split; [reflexivity | split; [| assumption] ]; clear HE HD.
       destruct np as [| np]; [now inversion HLe0 |]; simpl in Hp.
-      unfold lt in HLe0; rewrite HLe0.
+      unfold lt in HLe0; rewrite ->HLe0.
       rewrite <- HSub; apply HTL, Hp; [reflexivity | assumption].
     Qed.
 
@@ -99,20 +102,20 @@ Module IrisVS (RL : PCM_T) (C : CORE_LANG).
       intros pw nn r w _; clear r pw.
       intros n r _ _ HInv w'; clear nn; intros.
       do 14 red in HInv; destruct (w i) as [μ |] eqn: HLu; [| contradiction].
-      apply ı in HInv; rewrite (isoR p) in HInv.
+      apply ı in HInv; rewrite ->(isoR p) in HInv.
       (* get rid of the invisible 1/2 *)
       do 8 red in HInv.
       destruct HE as [rs [HE HM] ].
       destruct (rs i) as [ri |] eqn: HLr.
-      - rewrite comp_map_remove with (i := i) (r := ri) in HE by assumption.
-        rewrite assoc, <- (assoc (Some r)), (comm rf), assoc in HE.
-        destruct (Some r · Some ri) as [rri |] eqn: HR;
-          [| erewrite !pcm_op_zero in HE by apply _; now contradiction].
-        exists w' rri; split; [reflexivity |].
+      - rewrite ->comp_map_remove with (i := i) (r := ri) in HE by (rewrite HLr; reflexivity).
+        rewrite ->assoc, <- (assoc (_ r)), (comm rf), assoc in HE.
+        exists w'.
+        exists✓ (ra_proj r · ra_proj ri). { destruct HE as [HE _]. eapply ra_op_valid, ra_op_valid; eauto with typeclass_instances. }
+        split; [reflexivity |].
         split.
         + simpl; eapply HInv; [now auto with arith |].
           eapply uni_pred, HM with i;
-            [| exists r; rewrite <- HR | | | rewrite HLr]; try reflexivity; [|].
+            [| exists (ra_proj r) | | | rewrite HLr]; try reflexivity; [reflexivity| |].
           * left; unfold mask_sing, mask_set.
             destruct (Peano_dec.eq_nat_dec i i); tauto.
           * specialize (HSub i); rewrite HLu in HSub.
@@ -124,7 +127,7 @@ Module IrisVS (RL : PCM_T) (C : CORE_LANG).
           rewrite fdLookup_in; setoid_rewrite (fdRemove_neq _ _ _ n0); rewrite <- fdLookup_in; unfold mcup in HM; now auto.
       - rewrite <- fdLookup_notin_strong in HLr; contradiction HLr; clear HLr.
         specialize (HSub i); rewrite HLu in HSub; clear - HM HSub.
-        destruct (HM i) as [HD _]; [left | rewrite HD, fdLookup_in_strong; destruct (w' i); [eexists; reflexivity | contradiction] ].
+        destruct (HM i) as [HD _]; [left | rewrite ->HD, fdLookup_in_strong; destruct (w' i); [eexists; reflexivity | contradiction] ].
         clear; unfold mask_sing, mask_set.
         destruct (Peano_dec.eq_nat_dec i i); tauto.
     Qed.
@@ -135,58 +138,58 @@ Module IrisVS (RL : PCM_T) (C : CORE_LANG).
       intros pw nn r w _; clear r pw.
       intros n r _ _ [r1 [r2 [HR [HInv HP] ] ] ] w'; clear nn; intros.
       do 14 red in HInv; destruct (w i) as [μ |] eqn: HLu; [| contradiction].
-      apply ı in HInv; rewrite (isoR p) in HInv.
+      apply ı in HInv; rewrite ->(isoR p) in HInv.
       (* get rid of the invisible 1/2 *)
       do 8 red in HInv.
       destruct HE as [rs [HE HM] ].
-      exists w' (pcm_unit _); split; [reflexivity | split; [exact I |] ].
-      rewrite (comm (Some r)), <-assoc in HE.
-      remember (match rs i with Some ri => ri | None => pcm_unit _ end) as ri eqn: EQri.
-      destruct (Some ri · Some r) as [rri |] eqn: EQR.
-      - exists (fdUpdate i rri rs); split; [| intros j Hm].
-        + erewrite pcm_op_unit by apply _.
-          clear - HE EQR EQri. destruct (rs i) as [rsi |] eqn: EQrsi; subst.
-          * erewrite <-comp_map_insert_old; try eassumption. rewrite<- EQR; reflexivity.
-          * erewrite <-comp_map_insert_new; try eassumption. rewrite <-EQR.
-            erewrite pcm_op_unit by apply _. assumption.
-        + specialize (HD j); unfold mask_sing, mask_set, mcup in *; simpl in Hm, HD.
-          destruct (Peano_dec.eq_nat_dec i j);
-            [subst j; clear Hm |
-             destruct Hm as [Hm | Hm]; [contradiction | rewrite fdLookup_in_strong, fdUpdate_neq, <- fdLookup_in_strong by assumption; now auto] ].
-          rewrite !fdLookup_in_strong, fdUpdate_eq.
-          destruct n as [| n]; [now inversion HLe | simpl in HP].
-          rewrite HSub in HP; specialize (HSub i); rewrite HLu in HSub.
-          destruct (w' i) as [Ï€' |]; [| contradiction].
-          split; [intuition now eauto | intros].
-          simpl in HLw, HLrs, HSub. subst ri0. rewrite <- HLw, <- HSub.
-          apply HInv; [now auto with arith |].
-          eapply uni_pred, HP; [now auto with arith |].
-          assert (HT : Some ri · Some r1 · Some r2 == Some rri)
-            by (rewrite <- EQR, <- HR, assoc; reflexivity); clear - HT.
-          destruct (Some ri · Some r1) as [rd |];
-            [| now erewrite pcm_op_zero in HT by apply _].
-          exists rd; assumption.
-      - destruct (rs i) as [rsi |] eqn: EQrsi; subst;
-        [| erewrite pcm_op_unit in EQR by apply _; discriminate].
-        clear - HE EQrsi EQR.
-        assert (HH : rf · (Some r · comp_map rs) = 0); [clear HE | rewrite HH in HE; contradiction].
-        eapply ores_equiv_eq; rewrite comp_map_remove by eassumption.
-        rewrite (assoc (Some r)), (comm (Some r)), EQR, comm.
-        erewrite !pcm_op_zero by apply _; reflexivity.
+      exists w' ra_pos_unit; split; [reflexivity | split; [exact I |] ].
+      rewrite ->(comm (_ r)), <-assoc in HE.
+      remember (match rs i with Some ri => ri | None => ra_pos_unit end) as ri eqn: EQri.
+      pose✓ rri := (ra_proj ri · ra_proj r).
+      { destruct (rs i) as [rsi |] eqn: EQrsi; subst;
+        [| simpl; rewrite ->ra_op_unit by apply _; now apply ra_pos_valid].
+        clear - HE EQrsi. destruct HE as [HE _].
+        rewrite ->comp_map_remove with (i:=i) in HE by (erewrite EQrsi; reflexivity).
+        rewrite ->(assoc (_ r)), (comm (_ r)), comm, assoc, <-(assoc (_ rsi) _), (comm _ (ra_proj r)), assoc in HE.
+        eapply ra_op_valid, ra_op_valid; now eauto with typeclass_instances.
+      }
+      exists (fdUpdate i rri rs); split; [| intros j Hm].
+      - simpl. erewrite ra_op_unit by apply _.
+        clear - HE EQri. destruct (rs i) as [rsi |] eqn: EQrsi.
+        + subst rsi. erewrite <-comp_map_insert_old; [ eassumption | rewrite EQrsi; reflexivity | reflexivity ].
+        + unfold rri. subst ri. simpl. erewrite <-comp_map_insert_new; [|rewrite EQrsi; reflexivity]. simpl.
+          erewrite ra_op_unit by apply _. assumption.
+      - specialize (HD j); unfold mask_sing, mask_set, mcup in *; simpl in Hm, HD.
+        destruct (Peano_dec.eq_nat_dec i j);
+          [subst j; clear Hm |
+           destruct Hm as [Hm | Hm]; [contradiction | rewrite ->fdLookup_in_strong, fdUpdate_neq, <- fdLookup_in_strong by assumption; now auto] ].
+        rewrite ->!fdLookup_in_strong, fdUpdate_eq.
+        destruct n as [| n]; [now inversion HLe | simpl in HP].
+        rewrite ->HSub in HP; specialize (HSub i); rewrite HLu in HSub.
+        destruct (w' i) as [Ï€' |]; [| contradiction].
+        split; [intuition now eauto | intros].
+        simpl in HLw, HSub. change (equiv rri ri0) in HLrs. rewrite <- HLw, <- HSub.
+        apply HInv; [now auto with arith |].
+        eapply uni_pred, HP; [now auto with arith |].
+        rewrite <-HLrs. clear dependent ri0.
+        exists (ra_proj ri · ra_proj r1).
+        subst rri.
+        (* Coq, are you serious?!?? *)
+        change (ra_proj ri · ra_proj r1 · ra_proj r2 == (ra_proj ri · ra_proj r)).
+        rewrite <-HR, assoc. reflexivity.
     Qed.
 
     Lemma vsTrans p q r m1 m2 m3 (HMS : m2 ⊆ m1 ∪ m3) :
       vs m1 m2 p q ∧ vs m2 m3 q r ⊑ vs m1 m3 p r.
     Proof.
-      intros w' n r1 [Hpq Hqr] w HSub; specialize (Hpq _ HSub); rewrite HSub in Hqr; clear w' HSub.
+      intros w' n r1 [Hpq Hqr] w HSub; specialize (Hpq _ HSub); rewrite ->HSub in Hqr; clear w' HSub.
       intros np rp HLe HS Hp w1; intros; specialize (Hpq _ _ HLe HS Hp).
       edestruct Hpq as [w2 [rq [HSw12 [Hq HEq] ] ] ]; try eassumption; [|].
       { clear - HD HMS; intros j [Hmf Hm12]; apply (HD j); split; [assumption |].
         destruct Hm12 as [Hm1 | Hm2]; [left; assumption | apply HMS, Hm2].
       }
-      clear HS; assert (HS : pcm_unit _ ⊑ rq) by (exists rq; now erewrite comm, pcm_op_unit by apply _).
       rewrite <- HLe, HSub in Hqr; specialize (Hqr _ HSw12); clear Hpq HE w HSub Hp.
-      edestruct (Hqr (S k) _ HLe0 HS Hq w2) as [w3 [rR [HSw23 [Hr HEr] ] ] ];
+      edestruct (Hqr (S k) _ HLe0 (unit_min _ _) Hq w2) as [w3 [rR [HSw23 [Hr HEr] ] ] ];
         try (reflexivity || eassumption); [now auto with arith | |].
       { clear - HD HMS; intros j [Hmf Hm23]; apply (HD j); split; [assumption |].
         destruct Hm23 as [Hm2 | Hm3]; [apply HMS, Hm2 | right; assumption].
@@ -198,11 +201,11 @@ Module IrisVS (RL : PCM_T) (C : CORE_LANG).
     Lemma vsEnt p q m :
       □ (p → q) ⊑ vs m m p q.
     Proof.
-      intros w' n r1 Himp w HSub; rewrite HSub in Himp; clear w' HSub.
+      intros w' n r1 Himp w HSub; rewrite ->HSub in Himp; clear w' HSub.
       intros np rp HLe HS Hp w1; intros.
       exists w1 rp; split; [reflexivity | split; [| assumption ] ].
-      eapply Himp; [assumption | now eauto with arith | exists rp; now erewrite comm, pcm_op_unit by apply _ |].
-      unfold lt in HLe0; rewrite HLe0, <- HSub; assumption.
+      eapply Himp; [assumption | now eauto with arith | now apply ord_res_pres, unit_min | ].
+      unfold lt in HLe0; rewrite ->HLe0, <- HSub; assumption.
     Qed.
 
     Lemma vsFrame p q r m1 m2 mf (HDisj : mf # m1 ∪ m2) :
@@ -210,96 +213,61 @@ Module IrisVS (RL : PCM_T) (C : CORE_LANG).
     Proof.
       intros w' n r1 HVS w HSub; specialize (HVS _ HSub); clear w' r1 HSub.
       intros np rpr HLe _ [rp [rr [HR [Hp Hr] ] ] ] w'; intros.
-      assert (HS : pcm_unit _ ⊑ rp) by (exists rp; now erewrite comm, pcm_op_unit by apply _).
-      specialize (HVS _ _ HLe HS Hp w' (Some rr · rf) (mf ∪ mf0) σ k); clear HS.
+      assert (HS : ra_unit _ ⊑ ra_proj rp) by (eapply unit_min).
+      specialize (HVS _ _ HLe HS Hp w' (ra_proj rr · rf) (mf ∪ mf0) σ k); clear HS.
       destruct HVS as [w'' [rq [HSub' [Hq HEq] ] ] ]; try assumption; [| |].
       - (* disjointness of masks: possible lemma *)
         clear - HD HDisj; intros i [ [Hmf | Hmf] Hm12]; [eapply HDisj; now eauto |].
         unfold mcup in *; eapply HD; split; [eassumption | tauto].
-      - rewrite assoc, HR; eapply wsat_equiv, HE; try reflexivity; [].
+      - rewrite ->assoc, HR; eapply wsat_equiv, HE; try reflexivity; [].
         clear; intros i; unfold mcup; tauto.
-      - rewrite assoc in HEq; destruct (Some rq · Some rr) as [rqr |] eqn: HR';
-        [| apply wsat_not_empty in HEq; [contradiction | now erewrite !pcm_op_zero by apply _] ].
-        exists w'' rqr; split; [assumption | split].
-        + unfold lt in HLe0; rewrite HSub, HSub', <- HLe0 in Hr; exists rq rr.
-          rewrite HR'; split; now auto.
+      - rewrite ->assoc in HEq.
+        exists w''. exists✓ (ra_proj rq · ra_proj rr).
+        { apply wsat_not_empty in HEq. auto_valid. }
+        split; [assumption | split].
+        + unfold lt in HLe0; rewrite ->HSub, HSub', <- HLe0 in Hr; exists rq rr.
+          split; now auto.
         + eapply wsat_equiv, HEq; try reflexivity; [].
           clear; intros i; unfold mcup; tauto.
     Qed.
 
-    Instance LP_optres (P : option RL.res -> Prop) : LimitPreserving P.
+    Instance limit_preserving_res (P : RL.res -> Prop) : LimitPreserving P.
     Proof.
-      intros σ σc HPc; simpl; unfold option_compl.
-      generalize (@eq_refl _ (σ 1%nat)).
-      pattern (σ 1%nat) at 1 3; destruct (σ 1%nat); [| intros HE; rewrite HE; apply HPc].
-      intros HE; simpl; unfold discreteCompl, unSome.
-      generalize (@eq_refl _ (σ 2)); pattern (σ 2) at 1 3; destruct (σ 2).
-      + intros HE'; rewrite HE'; apply HPc.
-      + intros HE'; exfalso; specialize (σc 1 1 2)%nat.
-        rewrite <- HE, <- HE' in σc; contradiction σc; auto with arith.
+      intros σ σc HPc; simpl. unfold discreteCompl.
+      now auto.
     Qed.
 
-    Definition ownLP (P : option RL.res -> Prop) : {s : option RL.res | P s} -n> Props :=
+    Definition ownLP (P : RL.res -> Prop) : {s : RL.res | P s} -n> Props :=
       ownL <M< inclM.
 
-    Lemma pcm_op_split rp1 rp2 rp sp1 sp2 sp :
-      Some (rp1, sp1) · Some (rp2, sp2) == Some (rp, sp) <->
-      Some rp1 · Some rp2 == Some rp /\ Some sp1 · Some sp2 == Some sp.
-    Proof.
-      unfold pcm_op at 1, res_op at 2, pcm_op_prod at 1.
-      destruct (Some rp1 · Some rp2) as [rp' |]; [| simpl; tauto].
-      destruct (Some sp1 · Some sp2) as [sp' |]; [| simpl; tauto].
-      simpl; split; [| intros [EQ1 EQ2]; subst; reflexivity].
-      intros EQ; inversion EQ; tauto.
-    Qed.
-
-    Lemma vsGhostUpd m rl (P : option RL.res -> Prop)
-          (HU : forall rf (HD : rl · rf <> None), exists sl, P sl /\ sl · rf <> None) :
+    Lemma vsGhostUpd m rl (P : RL.res -> Prop)
+          (HU : forall rf (HD : ✓(rl · rf)), exists sl, P sl /\ ✓(sl · rf)) :
       valid (vs m m (ownL rl) (xist (ownLP P))).
     Proof.
-      unfold ownLP; intros _ _ _ w _ n [rp' rl'] _ _ HG w'; intros.
-      destruct rl as [rl |]; simpl in HG; [| contradiction].
-      destruct HE as [rs HE].
-      destruct HG as [ [rdp rdl] EQr]; rewrite pcm_op_split in EQr; destruct EQr as [EQrp EQrl].
-      erewrite comm, pcm_op_unit in EQrp by apply _; simpl in EQrp; subst rp'.
-      destruct (Some (rdp, rl') · rf · comp_map rs) as [t |] eqn: EQt;
-        [| destruct HE as [HES _]; setoid_rewrite EQt in HES; contradiction].
-      assert (EQt' : Some (rdp, rl') · rf · comp_map rs == Some t) by (rewrite EQt; reflexivity).
-      clear EQt; rename EQt' into EQt.
-      destruct rf as [ [rfp rfl] |]; [| now erewrite (comm _ 0), !pcm_op_zero in EQt by apply _].
-      destruct (comp_map rs) as [ [sp sl] |] eqn:EQrs; [| now erewrite (comm _ 0), pcm_op_zero in EQt by apply _].
-      destruct (Some (rdp, rl') · Some (rfp, rfl)) as [ [rdfp rdfl] |] eqn: EQdf;
-        setoid_rewrite EQdf in EQt; [| now erewrite pcm_op_zero in EQt by apply _].
-      destruct (HU (Some rdl · Some rfl · Some sl)) as [rsl [HPrsl HCrsl] ].
-      - intros HEq; destruct t as [tp tl]; apply pcm_op_split in EQt; destruct EQt as [_ EQt].
-        assert (HT : Some (rdp, rl') · Some (rfp, rfl) == Some (rdfp, rdfl)) by (rewrite EQdf; reflexivity); clear EQdf.
-        apply pcm_op_split in HT; destruct HT as [_ EQdf].
-        now rewrite <- EQdf, <- EQrl, (comm (Some rdl)), <- (assoc (Some rl)), <- assoc, HEq in EQt.
-      - destruct (rsl · Some rdl) as [rsl' |] eqn: EQrsl;
-        [| contradiction HCrsl; eapply ores_equiv_eq; now erewrite !assoc, EQrsl, !pcm_op_zero by apply _ ].
-        exists w' (rdp, rsl'); split; [reflexivity | split].
-        + exists (exist _ rsl HPrsl); destruct rsl as [rsl |];
-          [simpl | now erewrite pcm_op_zero in EQrsl by apply _].
-          exists (rdp, rdl); rewrite pcm_op_split.
-          split; [now erewrite comm, pcm_op_unit by apply _ | now rewrite comm, EQrsl].
-        + destruct HE as [HES HEL]. exists rs. split; [| assumption]; clear HEL.
-          assert (HT := ores_equiv_eq _ _ _ EQt); setoid_rewrite EQdf in HES;
-          setoid_rewrite HT in HES; clear HT; destruct t as [tp tl].
-          rewrite EQrs; clear rs EQrs.
-          destruct (rsl · (Some rdl · Some rfl · Some sl)) as [tl' |] eqn: EQtl;
-          [| now contradiction HCrsl]; clear HCrsl.
-          assert (HT : Some (rdp, rsl') · Some (rfp, rfl) · Some (sp, sl) = Some (tp, tl')); [| setoid_rewrite HT; apply HES].
-          rewrite <- EQdf, <- assoc in EQt; clear EQdf; eapply ores_equiv_eq; rewrite <- assoc.
-          destruct (Some (rfp, rfl) · Some (sp, sl)) as [ [up ul] |] eqn: EQu;
-            setoid_rewrite EQu in EQt; [| now erewrite comm, pcm_op_zero in EQt by apply _].
-          apply pcm_op_split in EQt; destruct EQt as [EQt _]; apply pcm_op_split; split; [assumption |].
-          assert (HT : Some rfl · Some sl == Some ul);
-            [| now rewrite <- EQrsl, <- EQtl, <- HT, !assoc].
-          apply (proj2 (A := Some rfp · Some sp == Some up)), pcm_op_split.
-          now erewrite EQu.
+      unfold ownLP; intros _ _ _ w _ n [ [rp' rl'] Hrval] _ _ HG w'; intros.
+      destruct HE as [rs [ Hsat HE] ]. rewrite <-assoc in Hsat. simpl in Hsat. destruct Hsat as [Hval Hst].
+      destruct HG as [ [rdp rdl] [_ EQrl] ]. simpl in EQrl. clear rdp.
+      destruct (HU (rdl · snd(rf · comp_map rs))) as [rsl [HPrsl HCrsl] ].
+      - clear - Hval EQrl. eapply ra_prod_valid2 in Hval. destruct Hval as [_ Hsnd].
+        rewrite ->assoc, (comm rl), EQrl.
+        rewrite ra_op_prod_snd in Hsnd. exact Hsnd.
+      - exists w'. exists✓ (rp', rsl).
+        { clear - Hval HCrsl.
+          apply ra_prod_valid. split; [|auto_valid].
+          eapply ra_prod_valid2 in Hval. destruct Hval as [Hfst _].
+          rewrite ra_op_prod_fst in Hfst. auto_valid. }
+        split; first reflexivity. split.
+        + exists (exist _ rsl HPrsl). simpl.
+          exists (rp', 1:RL.res). simpl.
+          rewrite ra_op_unit ra_op_unit2. split; reflexivity.
+        + exists rs. split; [| assumption]; clear HE. rewrite <-assoc. split; [eapply ra_prod_valid2; split|].
+          * clear - Hval. eapply ra_prod_valid2 in Hval. destruct Hval as [Hfst _].
+            rewrite ra_op_prod_fst in Hfst.
+            rewrite ra_op_prod_fst. exact Hfst.
+          * clear -HCrsl. rewrite ->!assoc, (comm rsl), <-assoc in HCrsl.
+            apply ra_op_valid2 in HCrsl. rewrite ra_op_prod_snd. exact HCrsl.
+          * clear -Hst. rewrite ra_op_prod_fst. rewrite ra_op_prod_fst in Hst. exact Hst.
     Qed.
-    (* The above proof is rather ugly in the way it handles the monoid elements,
-       but it works *)
 
     Program Definition inv' m : Props -n> {n : nat | m n} -n> Props :=
       n[(fun p => n[(fun n => inv n p)])].
@@ -335,16 +303,16 @@ Module IrisVS (RL : PCM_T) (C : CORE_LANG).
       intros pw nn r w _; clear r pw.
       intros n r _ _ HP w'; clear nn; intros.
       destruct n as [| n]; [now inversion HLe | simpl in HP].
-      rewrite HSub in HP; clear w HSub; rename w' into w.
+      rewrite ->HSub in HP; clear w HSub; rename w' into w.
       destruct (fresh_region w m HInf) as [i [Hm HLi] ].
       assert (HSub : w ⊑ fdUpdate i (ı' p) w).
       { intros j; destruct (Peano_dec.eq_nat_dec i j); [subst j; rewrite HLi; exact I|].
-        now rewrite fdUpdate_neq by assumption.
+        now rewrite ->fdUpdate_neq by assumption.
       }
-      exists (fdUpdate i (ı' p) w) (pcm_unit _); split; [assumption | split].
-      - exists (exist _ i Hm); do 22 red.
-        unfold proj1_sig; rewrite fdUpdate_eq; reflexivity.
-      - erewrite pcm_op_unit by apply _.
+      exists (fdUpdate i (ı' p) w) (ra_pos_unit); split; [assumption | split].
+      - exists (exist _ i Hm). do 22 red.
+        unfold proj1_sig. rewrite fdUpdate_eq; reflexivity.
+      - unfold ra_pos_unit, proj1_sig. erewrite ra_op_unit by apply _.
         destruct HE as [rs [HE HM] ].
         exists (fdUpdate i r rs).
         assert (HRi : rs i = None).
@@ -353,15 +321,15 @@ Module IrisVS (RL : PCM_T) (C : CORE_LANG).
         }
         split.
         {
-          rewrite <-comp_map_insert_new by assumption.
-          rewrite assoc, (comm rf). assumption.
+          rewrite <-comp_map_insert_new by (rewrite HRi; reflexivity).
+          rewrite ->assoc, (comm rf). assumption.
         }
         intros j Hm'.
         rewrite !fdLookup_in_strong; destruct (Peano_dec.eq_nat_dec i j).
         + subst j; rewrite !fdUpdate_eq; split; [intuition now eauto | intros].
-          simpl in HLw, HLrs; subst ri; rewrite <- HLw, isoR, <- HSub.
-          eapply uni_pred, HP; [now auto with arith | reflexivity].
-        + rewrite !fdUpdate_neq, <- !fdLookup_in_strong by assumption.
+          simpl in HLw. do 3 red in HLrs. rewrite <- HLw, isoR, <- HSub.
+          eapply uni_pred, HP; [now auto with arith |]. rewrite HLrs. reflexivity.
+        + rewrite ->!fdUpdate_neq, <- !fdLookup_in_strong by assumption.
           setoid_rewrite <- HSub.
           apply HM; assumption.
     Qed.
diff --git a/iris_wp.v b/iris_wp.v
index b83248e48..0d75c9f71 100644
--- a/iris_wp.v
+++ b/iris_wp.v
@@ -2,6 +2,8 @@ Require Import ssreflect.
 Require Import world_prop core_lang lang masks iris_vs.
 Require Import ModuRes.PCM ModuRes.UPred ModuRes.BI ModuRes.PreoMet ModuRes.Finmap.
 
+Set Bullet Behavior "Strict Subproofs".
+
 Module IrisWP (RL : PCM_T) (C : CORE_LANG).
   Module Export L  := Lang C.
   Module Export VS := IrisVS RL C.
diff --git a/lib/ModuRes/RA.v b/lib/ModuRes/RA.v
index 9ded5c261..74377673c 100644
--- a/lib/ModuRes/RA.v
+++ b/lib/ModuRes/RA.v
@@ -35,7 +35,7 @@ Notation "'✓' p" := (ra_valid p = true) (at level 35) : ra_scope.
 Notation "'~' '✓' p" := (ra_valid p <> true) (at level 35) : ra_scope.
 Delimit Scope ra_scope with ra.
 
-Tactic Notation "decide✓" ident(t1) "eqn:" ident(H) := destruct (ra_valid t1) eqn:H; [|apply not_true_iff_false in H].
+Tactic Notation "decide✓" ident(t1) "as" ident(H) := destruct (ra_valid t1) eqn:H; [|apply not_true_iff_false in H].
 
 
 (* General RA lemmas *)
@@ -95,9 +95,42 @@ Section Products.
       + eapply ra_op_valid; now eauto.
       + eapply ra_op_valid; now eauto.
   Qed.
-
 End Products.
 
+Section ProductLemmas.
+  Context {S T} `{raS : RA S, raT : RA T}.
+  Local Open Scope ra_scope.
+    
+  Lemma ra_op_prod_fst (st1 st2: S*T):
+    fst (st1 · st2) = fst st1 · fst st2.
+  Proof.
+    destruct st1 as [s1 t1]. destruct st2 as [s2 t2]. reflexivity.
+  Qed.
+  
+  Lemma ra_op_prod_snd (st1 st2: S*T):
+    snd (st1 · st2) = snd st1 · snd st2.
+  Proof.
+    destruct st1 as [s1 t1]. destruct st2 as [s2 t2]. reflexivity.
+  Qed.
+
+  Lemma ra_prod_valid (s: S) (t: T):
+    ✓(s, t) <-> ✓s /\ ✓t.
+  Proof.
+    unfold ra_valid, ra_valid_prod.
+    rewrite andb_true_iff.
+    reflexivity.
+  Qed.
+
+  Lemma ra_prod_valid2 (st: S*T):
+    ✓st <-> ✓(fst st) /\ ✓(snd st).
+  Proof.
+    destruct st as [s t]. unfold ra_valid, ra_valid_prod.
+    rewrite andb_true_iff.
+    tauto.
+  Qed.
+
+End ProductLemmas.
+
 Section PositiveCarrier.
   Context {T} `{raT : RA T}.
   Local Open Scope ra_scope.
@@ -125,6 +158,13 @@ Section PositiveCarrier.
     rewrite comm. now eapply ra_op_pos_valid.
   Qed.
 
+  Lemma ra_pos_valid (r : ra_pos):
+    ✓(ra_proj r).
+  Proof.
+    destruct r as [r VAL].
+    exact VAL.
+  Qed.
+
 End PositiveCarrier.
 Global Arguments ra_pos T {_}.
 
@@ -197,7 +237,7 @@ Section Order.
     rewrite <- assoc, (comm y), <- assoc, assoc, (comm y1), EQx, EQy; reflexivity.
   Qed.
 
-  Lemma ord_res_optRes r s :
+  Lemma ord_res_pres r s :
     (r ⊑ s) <-> (ra_proj r ⊑ ra_proj s).
   Proof.
     split; intros HR.
@@ -224,15 +264,20 @@ Section Exclusive.
       | _, _ => False
     end.
 
-  Global Program Instance ra_type_ex : Setoid ra_res_ex :=
-    mkType ra_res_ex_eq.
+  Global Program Instance ra_eq_equiv : Equivalence ra_res_ex_eq.
   Next Obligation.
-    split.
-    - intros [t| |]; simpl; now auto.
-    - intros [t1| |] [t2| |]; simpl; now auto.
-    - intros [t1| |] [t2| |] [t3| |]; simpl; try now auto.
-      + intros ? ?. etransitivity; eassumption.
+    intros [t| |]; simpl; now auto.
   Qed.
+  Next Obligation.
+    intros [t1| |] [t2| |]; simpl; now auto.
+  Qed.
+  Next Obligation.
+    intros [t1| |] [t2| |] [t3| |]; simpl; try now auto.
+    - intros ? ?. etransitivity; eassumption.
+  Qed.
+
+  Global Program Instance ra_type_ex : Setoid ra_res_ex :=
+    mkType ra_res_ex_eq.
       
   Global Instance ra_unit_ex : RA_unit ra_res_ex := ex_unit.
   Global Instance ra_op_ex : RA_op ra_res_ex :=
-- 
GitLab