From 620ac27ce7a739f8688564fe3337ce4d9b5bfb75 Mon Sep 17 00:00:00 2001
From: David Swasey <swasey@mpi-sws.org>
Date: Sun, 26 Nov 2017 18:52:57 +0100
Subject: [PATCH] Rename stuckness lemmas.

---
 theories/program_logic/hoare.v      | 8 ++++----
 theories/program_logic/weakestpre.v | 6 +++---
 2 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/theories/program_logic/hoare.v b/theories/program_logic/hoare.v
index 3b4142dc5..0f2136dee 100644
--- a/theories/program_logic/hoare.v
+++ b/theories/program_logic/hoare.v
@@ -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 :
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index a10f60275..3fe7e6336 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -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 :
-- 
GitLab