Commit 620ac27c by David Swasey

### Rename stuckness lemmas.

parent dd0a95de
 ... ... @@ -57,9 +57,9 @@ Proof. solve_proper. Qed. Lemma ht_mono s E P P' Φ Φ' e : (P ⊢ P') → (∀ v, Φ' v ⊢ Φ v) → {{ P' }} e @ s; E {{ Φ' }} ⊢ {{ P }} e @ s; E {{ Φ }}. Proof. by intros; apply persistently_mono, wand_mono, wp_mono. Qed. Lemma ht_stuckness_mono s1 s2 E P Φ e : Lemma ht_stuck_mono s1 s2 E P Φ e : (s1 ≤ s2)%stuckness → {{ P }} e @ s1; E {{ Φ }} ⊢ {{ P }} e @ s2; E {{ Φ }}. Proof. by intros; apply persistently_mono, wand_mono, wp_stuckness_mono. Qed. Proof. by intros; apply persistently_mono, wand_mono, wp_stuck_mono. Qed. Global Instance ht_mono' s E : Proper (flip (⊢) ==> eq ==> pointwise_relation _ (⊢) ==> (⊢)) (ht s E). Proof. solve_proper. Qed. ... ... @@ -98,10 +98,10 @@ Proof. iIntros (v) "Hv". by iApply "HwpK". Qed. Lemma ht_forget_not_stuck s E P Φ e : Lemma ht_stuck_weaken s E P Φ e : {{ P }} e @ s; E {{ Φ }} ⊢ {{ P }} e @ E ?{{ Φ }}. Proof. by iIntros "#Hwp !# ?"; iApply wp_forget_not_stuck; iApply "Hwp". by iIntros "#Hwp !# ?"; iApply wp_stuck_weaken; iApply "Hwp". Qed. Lemma ht_mask_weaken s E1 E2 P Φ e : ... ...
 ... ... @@ -210,7 +210,7 @@ Proof. iMod "Hclose" as "_". by iApply ("IH" with "HΦ"). Qed. Lemma wp_forget_not_stuck s E e Φ : Lemma wp_stuck_weaken s E e Φ : WP e @ s; E {{ Φ }} ⊢ WP e @ E ?{{ Φ }}. Proof. iIntros "H". iLöb as "IH" forall (E e Φ). rewrite !wp_unfold /wp_pre. ... ... @@ -311,9 +311,9 @@ Proof. iIntros (HΦ) "H"; iApply (wp_strong_mono s E E); auto. iIntros "{\$H}" (v) "?". by iApply HΦ. Qed. Lemma wp_stuckness_mono s1 s2 E e Φ : Lemma wp_stuck_mono s1 s2 E e Φ : (s1 ≤ s2)%stuckness → WP e @ s1; E {{ Φ }} ⊢ WP e @ s2; E {{ Φ }}. Proof. case: s1; case: s2 => // _. exact: wp_forget_not_stuck. Qed. Proof. case: s1; case: s2 => // _. exact: wp_stuck_weaken. Qed. Lemma wp_mask_mono s E1 E2 e Φ : E1 ⊆ E2 → WP e @ s; E1 {{ Φ }} ⊢ WP e @ s; E2 {{ Φ }}. Proof. iIntros (?) "H"; iApply (wp_strong_mono s E1 E2); auto. iFrame; eauto. Qed. Global Instance wp_mono' s E e : ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment