Merge branch 'master' of git.fp.mpi-sws.org:nowbook

iris_check.v

 Require Import Arith ssreflect.
-Require Import world_prop world_prop_recdom core_lang lang masks iris_core iris_plog iris_meta iris_vs_rules iris_ht_rules.
+Require Import world_prop world_prop_recdom core_lang lang masks iris_core iris_plog iris_meta iris_vs_rules iris_ht_rules iris_derived_rules.
 Require Import ModuRes.RA ModuRes.UPred ModuRes.BI ModuRes.PreoMet ModuRes.Finmap.
 
 Set Bullet Behavior "Strict Subproofs".
@@ -182,6 +182,7 @@ Module Import Plog := IrisPlog TrivialRA StupidLang Res World Core.
 Module Import Meta := IrisMeta TrivialRA StupidLang Res World Core Plog.
 Module Import HTRules := IrisHTRules TrivialRA StupidLang Res World Core Plog.
 Module Import VSRules := IrisVSRules TrivialRA StupidLang Res World Core Plog.
+Module Import DRRules := IrisDerivedRules TrivialRA StupidLang Res World Core Plog VSRules HTRules.
 
 (* And now we check for axioms *)
 Print Assumptions adequacy_obs.

iris_core.v

@@ -99,14 +99,18 @@ Module Type IRIS_CORE (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
   Lemma propsMR {P w n r r'} (HSr : r ⊑ r') : P w n r -> P w n r'.
   Proof. exact: (propsMNR (lerefl n) HSr). Qed.
 
-  Lemma propsMWN {P w n r w' n'} (HSw : w ⊑ w') (HLe : n' <= n) :
-    P w n r -> P w' n' r.
-  Proof. move=> HP; by apply: (propsMW HSw); exact: (propsMNR HLe (prefl r)). Qed.
-  
   Lemma propsM {P w n r w' n' r'} (HSw : w ⊑ w') (HLe : n' <= n) (HSr : r ⊑ r') :
     P w n r -> P w' n' r'.
   Proof. move=> HP; by apply: (propsMW HSw); exact: (propsMNR HLe HSr). Qed.
 
+  Lemma propsMWR {P w n r w' r'} (HLe : w ⊑ w') (HSr : r ⊑ r') : P w n r -> P w' n r'.
+  Proof. move=> HP; eapply propsM; (eassumption || reflexivity). Qed.
+
+  Lemma propsMWN {P w n r w' n'} (HSw : w ⊑ w') (HLe : n' <= n) :
+    P w n r -> P w' n' r.
+  Proof. move=> HP; eapply propsM; (eassumption || reflexivity). Qed.
+
+
   (** And now we're ready to build the IRIS-specific connectives! *)
 
   Section Resources.

iris_derived_rules.v

@@ -13,7 +13,11 @@ Module Type IRIS_DERIVED_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (W
   Local Open Scope bi_scope.
   Local Open Scope iris_scope.
 
-  Section DerivedRules.
+  (* Ideally, these rules should never talk about worlds or such.
+     At the very least, they should not open the definition of the complex assertrtions:
+     invariants, primitive view shifts, weakest pre. *)
+
+  Section DerivedVSRules.
 
     Implicit Types (P : Props) (i : nat) (m : mask) (e : expr) (r : res).
 
@@ -26,7 +30,25 @@ Module Type IRIS_DERIVED_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (W
       apply bot_false.
     Qed.
 
-  End DerivedRules. 
+    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 w0 n0 r0 [HPQ HQR] w1 HSub n1 r1 Hlt _ HP.
+      eapply pvsTrans; eauto.
+      eapply pvsImpl; split; first eapply propsMWN; 
+      [eassumption | eassumption | exact HQR | ].
+      eapply HPQ; by eauto using unit_min.
+    Qed.
+
+    Lemma vsEnt P Q m :
+      □(P → Q) ⊑ vs m m P Q.
+    Proof.
+      move => w0 n r0 HPQ w1 HSub n1 r1 Hlt _ /(HPQ _ HSub _ _ Hlt) HQ.
+      eapply pvsEnt, HQ; exact unit_min.
+    Qed.    
+
+
+  End DerivedVSRules. 
 
 End IRIS_DERIVED_RULES.
 

iris_vs_rules.v

@@ -116,14 +116,11 @@ Module Type IRIS_VS_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WO
       exists w3 r3; split; [ by rewrite -> HSub2 | by split ].
     Qed.
     
-    Lemma pvsEnt P m1 m2 (HMS : m2 ⊆ m1) :
-      P ⊑ pvs m1 m2 P.
+    Lemma pvsEnt P m :
+      P ⊑ pvs m m P.
     Proof.
       intros w0 n r0 HP w1 rf mf σ k HSub Hnk HD HSat.
-      exists w1 r0; repeat split; [ reflexivity | eapply propsMWN; eauto | ].
-      destruct HSat as (s & HSat & H).
-      exists s; split; first by auto.
-      move => i [/HMS|] IN; eapply H; [by left | by right].
+      exists w1 r0; repeat split; [ reflexivity | eapply propsMWN; eauto | assumption ].
     Qed.
     
     Lemma pvsImpl P Q m1 m2 :
@@ -136,23 +133,6 @@ Module Type IRIS_VS_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WO
       eapply HQ; [by rewrite -> HSub1 | omega | exact unit_min].
     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 w0 n0 r0 [HPQ HQR] w1 HSub n1 r1 Hlt _ HP.
-      eapply pvsTrans; eauto.
-      eapply pvsImpl; split; first eapply propsMWN; 
-      [eassumption | eassumption | exact HQR | ].
-      eapply HPQ; by eauto using unit_min.
-    Qed.
-
-    Lemma vsEnt P Q m :
-      □(P → Q) ⊑ vs m m P Q.
-    Proof.
-      move => w0 n r0 HPQ w1 HSub n1 r1 Hlt _ /(HPQ _ HSub _ _ Hlt) HQ.
-      eapply pvsEnt, HQ; [reflexivity | exact unit_min].
-    Qed.
-    
     Lemma pvsFrame P Q m1 m2 mf (HDisj : mf # m1 ∪ m2) :
       pvs m1 m2 P * Q ⊑ pvs (m1 ∪ mf) (m2 ∪ mf) (P * Q).
     Proof.
@@ -170,15 +150,6 @@ Module Type IRIS_VS_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WO
         * setoid_rewrite <- ra_op_assoc.
           eapply wsat_equiv; last eassumption; [|reflexivity|reflexivity].
           unfold mcup in *; split; intros i; tauto.
-    Qed.          
-          
-    Lemma vsFrame P Q R m1 m2 mf (HDisj : mf # m1 ∪ m2) :
-      vs m1 m2 P Q ⊑ vs (m1 ∪ mf) (m2 ∪ mf) (P * R) (Q * R).
-    Proof.
-      intros w0 n0 r0 HVS w1 HSub n1 r1 Hlt _ [r21 [r22 [HEr [HP HR]]]].
-      eapply pvsFrame; first assumption. 
-      eapply HVS in HP; eauto using unit_min; [].
-      do 2!eexists; split; last split; eauto.
     Qed.
 
     Instance LP_res (P : RL.res -> Prop) : LimitPreserving P.