adapt Iris to the less-dependant Agreement construction

iris_meta.v

@@ -441,11 +441,7 @@ Module Type IRIS_META (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
           - simpl in HSt. rewrite HSt. exact I. }
         exists pv'. split.
         + rewrite HSt. reflexivity.
-        + move=>{HS HSt} i agP Heq.
-          move:(HI i agP Heq).
-          destruct (i ∈ (m ∪ mf))%de; last tauto.
-          destruct (rs i); last tauto. simpl=>H.
-          erewrite ra_ag_unInj_pi. eassumption.
+        + assumption.
     Qed.
 
     (* The "nicer looking" (ht-based) lemma is now a derived form. *)

iris_plog.v

@@ -138,8 +138,7 @@ Module Type IRIS_PLOG (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
         (State wt ⊑ ex_own σ) /\
         forall i agP (Heq: (Invs wt) i = S n' = Some agP),
           match (i ∈ m)%de, s i with
-          | true , Some w => let P := ra_ag_unInj agP (S n') (HVal:=world_inv_val pv Heq) in
-                             unhalved (ı P) w n'
+          | true , Some w => let P := ra_ag_unInj agP (S n') in unhalved (ı P) w n'
           | false, None   => True
           | _    , _      => False
           end.
@@ -155,11 +154,9 @@ Module Type IRIS_PLOG (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
       { rewrite <-HS. apply pordR. destruct EQwt as [_ [HwtS _]].
         symmetry. exact HwtS. }
       move=>i agP Heq.
-      move:(HI i agP). case/(_ _)/Wrap; last move=>{HI} Heq' HI.
+      move:(HI i agP). case/(_ _)/Wrap; last move=>{HI} HI.
       { rewrite -Heq. rewrite EQwt. reflexivity. }
-      rewrite -EQm. destruct (i ∈ m1)%de; last exact HI.
-      destruct (s i); last exact HI.
-      simpl. simpl in HI. erewrite ra_ag_unInj_pi. eassumption.
+      rewrite -EQm. assumption.
     Qed.
 
     Lemma wsatTotal_dclosed n'1 n'2 σ s m wt:
@@ -173,7 +170,7 @@ Module Type IRIS_PLOG (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
       split; [assumption|]. move => {Hσ} i agP Heq.
       case HagP':(Invs wt i) => [agP'|]; last first.
       { exfalso. rewrite HagP' in Heq. exact Heq. }
-      move:(H i agP'). case/(_ _)/Wrap; last move=>{H} Heq'.
+      move:(H i agP'). case/(_ _)/Wrap; last move=>{H}.
       { now apply equivR. }
       destruct (s i) as [ws|], (i ∈ m)%de; simpl; tauto || (try contradiction); []=>H.
       eapply spredNE; last first.
@@ -182,10 +179,10 @@ Module Type IRIS_PLOG (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
         apply met_morph_nonexp. move:(Heq). rewrite HagP' in Heq=>Heq''.
         etransitivity.
         + symmetry. eapply ra_ag_unInj_move. omega.
-        + eapply ra_ag_unInj_dist. simpl in Heq'. exact Heq.
-    Grab Existential Variables.
-    { eapply world_invs_valid; first eexact pv'; first reflexivity.
-      rewrite Heq. eassumption. }
+          eapply world_inv_val; first eassumption. apply equivR. eassumption.
+        + eapply ra_ag_unInj_dist; last assumption. 
+          eapply world_invs_valid; first eexact pv'; first reflexivity.
+          rewrite Heq. eassumption.
     Qed.  
 
     (* It may be possible to use "later_sp" here, but let's avoid indirections where possible. *)

iris_vs_rules.v

@@ -38,7 +38,7 @@ Module Type IRIS_VS_RULES (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP:
       destruct HE as [rs [pv [HS HM]]].
       case HLu:(Invs w i) => [μ |] ; simpl in HInv; last first.
       { exfalso. rewrite HLu in HInv. destruct HInv. }
-      move:(HM i (ra_ag_inj (ı' (halved P)))). case/(_ _)/Wrap; last move=>Heq.
+      move:(HM i (ra_ag_inj (ı' (halved P)))). case/(_ _)/Wrap.
       { clear -HLu HInv pv HLe. eapply world_invs_extract; first assumption; last first.
         - eapply mono_dist, HInv. omega.
         - etransitivity; last eapply comp_finmap_le. exists wf. now rewrite comm. }
@@ -57,14 +57,13 @@ Module Type IRIS_VS_RULES (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP:
       exists pv'. split.
       - rewrite /= -Heqwt. assumption.
       - move=>j agP Hlu. rewrite (comm de_emp) de_emp_union. move:(HM j agP)=>{HM}.
-        case/(_ _)/Wrap; last move=>Heq'.
+        case/(_ _)/Wrap.
         { rewrite Heqwt. exact Hlu. }
         destruct (j ∈ mf) eqn:Hm.
         + erewrite de_in_true by de_tauto.
           destruct (dec_eq i j) as [EQ|NEQ].
           { exfalso. subst j. move:(HD i) Hm. clear. de_tauto. }
-          erewrite fdStrongUpdate_neq by assumption. destruct (rs j); last tauto.
-          simpl=>H. erewrite ra_ag_unInj_pi. eassumption.
+          erewrite fdStrongUpdate_neq by assumption. tauto.
         + destruct (dec_eq i j) as [EQ|NEQ].
           { move=>_. subst j. rewrite fdStrongUpdate_eq. exact I. }
           erewrite de_in_false by de_tauto.
@@ -106,19 +105,14 @@ Module Type IRIS_VS_RULES (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP:
           rewrite ->Heqwt, ->Hlu in HeqP. simpl. simpl in HeqP.
           etransitivity; last first.
           * assert(Heq:=halve_eq (T:=Props) (S k)). apply Heq=>{Heq}.
-            eapply (met_morph_nonexp ı). eapply ra_ag_unInj_dist.
-            symmetry. eexact HeqP.
+            eapply (met_morph_nonexp ı). eapply ra_ag_unInj_dist; last (symmetry; eexact HeqP).
+            exact I.
           * simpl. rewrite isoR. reflexivity.
-        + move:(HM j agP)=>{HM}. case/(_ _)/Wrap; last move=>Heq'.
+        + move:(HM j agP)=>{HM}. case/(_ _)/Wrap.
           { rewrite Heqwt. assumption. }
           rewrite comm de_emp_union. destruct (j ∈ mf) eqn:Hjin.
-          * erewrite de_in_true by de_tauto. erewrite fdStrongUpdate_neq by assumption.
-            destruct (rs j); last tauto. simpl.
-            move=>H. erewrite ra_ag_unInj_pi. eassumption.
-          * erewrite de_in_false by de_tauto. erewrite fdStrongUpdate_neq by assumption.
-            tauto.
-    Grab Existential Variables.
-    { exact I. }
+          * erewrite de_in_true by de_tauto. erewrite fdStrongUpdate_neq by assumption. tauto.
+          * erewrite de_in_false by de_tauto. erewrite fdStrongUpdate_neq by assumption. tauto.
     Qed.
 
     Lemma pvsTrans P m1 m2 m3 (HMS : m2 ⊑ m1 ∪ m3) :
@@ -198,11 +192,7 @@ Module Type IRIS_VS_RULES (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP:
           assert (pv':(cmra_valid ((I0, (S0, g1 · g')) · comp_finmap wf rs)) (S (S k))).
           { split; last split; try assumption; [].
             now rewrite ->assoc in HVal1. }
-          exists pv'. split; first assumption.
-          move=>i agP Heq. move:(HI i agP Heq). 
-          destruct (i ∈ _); last tauto.
-          destruct (rs i); last tauto.
-          move=>H. erewrite ra_ag_unInj_pi. eassumption.
+          exists pv'. split; assumption.
     Qed.
 
     Program Definition inv' m : Props -n> {n : nat | n ∈ m = true } -n> Props :=
@@ -259,18 +249,14 @@ Module Type IRIS_VS_RULES (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP:
           eapply mmorph_proper; last reflexivity.
           etransitivity; last first.
           * assert(Hheq:=halve_eq (T:=Props) (S k)). apply Hheq=>{Hheq}.
-            eapply (met_morph_nonexp ı). eapply ra_ag_unInj_dist.
-            eexact Heq.
+            eapply (met_morph_nonexp ı). eapply ra_ag_unInj_dist; last eexact Heq.
+            exact I.
           * simpl. rewrite isoR. reflexivity.
         + erewrite fdStrongUpdate_neq by assumption.
-          move:(HI j agP)=>{HI Hrsi HLi Hm}. case/(_ _)/Wrap; last move=>Heq'.
+          move:(HI j agP)=>{HI Hrsi HLi Hm}. case/(_ _)/Wrap.
           { rewrite -Heq. simpl. destruct (dec_eq i j); last reflexivity.
             contradiction. }
-          destruct (j ∈ (m ∪ mf)); last tauto.
-          destruct (rs j); last tauto.
-          move=>/= H. erewrite ra_ag_unInj_pi. eassumption.
-    Grab Existential Variables.
-    { exact I. }
+          tauto.
     Qed.
 
     Lemma pvsNotOwnInvalid m1 m2 w: