Tracked change to wsat and merged wpUnsafe into htUnsafe for consistency.

iris_unsafe.v

@@ -22,26 +22,21 @@ Module RobustSafety (RL : PCM_T) (C : CORE_LANG).
 
   Implicit Types (P Q R : Props) (i : nat) (safe : bool) (m : mask) (e : expr) (φ : value -n> Props) (r : res) (w : Wld).
 
-  Lemma wpUnsafe m e φ : wp true m e φ ⊑ wp false m e φ.
+  Lemma htUnsafe m P e φ : ht true m P e φ ⊑ ht false m P e φ.
   Proof.
-    move=> w n r He; move: n e φ w r He; elim/wf_nat_ind; move=> n IH e φ w r /unfold_wp He.
-    rewrite unfold_wp; move=> w' k s rf mf σ HSw HLt HD Hw.
+    move=> wz nz rz He w HSw n r HLe Hr HP.
+    move: {He P wz nz rz HSw HLe Hr HP} (He _ HSw _ _ HLe Hr HP).
+    move: n e φ w r; elim/wf_nat_ind; move=> n IH e φ w r He.
+    rewrite unfold_wp; move=> w' k rf mf σ HSw HLt HD Hw.
     move: {IH} (IH _ HLt) => IH.
-    move: {He HSw HLt HD Hw} (He _ _ _ _ _ _ HSw HLt HD Hw) => [HV [HS [HF _] ] ].
+    move: He => /unfold_wp He; move: {He HSw HLt HD Hw} (He _ _ _ _ _ HSw HLt HD Hw) => [HV [HS [HF _] ] ].
     split; [done | clear HV; split; [clear HF | split; [clear HS | done] ] ].
-    - move=> σ' ei ei' K HK Hstep.
-      move: {HS HK Hstep} (HS _ _ _ _ HK Hstep) => [w'' [r' [s' [HSw' [He' Hw'] ] ] ] ].
-      exists w'' r' s'; split; [done | split; [exact: IH | done] ].
+    - move=> σ' ei ei' K HK Hs.
+      move: {HS HK Hs} (HS _ _ _ _ HK Hs) => [w'' [r' [HSw' [He' Hw'] ] ] ].
+      exists w'' r'; split; [done | split; [exact: IH | done] ].
     move=> e' K HK.
-    move: {HF HK} (HF _ _ HK) => [w'' [rfk [rret [s' [HSw' [Hk [He' Hw'] ] ] ] ] ] ].
-    exists w'' rfk rret s'; split; [done | split; [exact: IH | split; [exact: IH | done] ] ].
-  Qed.
-
-  Lemma htUnsafe m P e φ : ht true m P e φ ⊑ ht false m P e φ.
-  Proof.
-    move=> w n rz He w' HSw n' r HLe Hr HP.
-    move: {He P w n rz HSw HLe Hr HP} (He _ HSw _ _ HLe Hr HP).
-    exact: wpUnsafe.
+    move: {HF HK} (HF _ _ HK) => [w'' [rfk [rret [HSw' [Hk [He' Hw'] ] ] ] ] ].
+    exists w'' rfk rret; split; [done | split; [exact: IH | split; [exact: IH | done] ] ].
   Qed.
 
 End RobustSafety.