diff --git a/theories/program_logic/hoare.v b/theories/program_logic/hoare.v index 44d6aed64f27def546f4beb6f625d81d15577daa..629e50a993d4cd04a9e1de83e0212d9454ae6e90 100644 --- a/theories/program_logic/hoare.v +++ b/theories/program_logic/hoare.v @@ -57,6 +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 : + (s1 ≤ s2)%stuckness → {{ P }} e @ s1; E {{ Φ }} ⊢ {{ P }} e @ s2; E {{ Φ }}. +Proof. by intros; apply persistently_mono, wand_mono, wp_stuckness_mono. Qed. Global Instance ht_mono' s E : Proper (flip (⊢) ==> eq ==> pointwise_relation _ (⊢) ==> (⊢)) (ht s E). Proof. solve_proper. Qed. diff --git a/theories/program_logic/language.v b/theories/program_logic/language.v index 6d96db0b1f4f04b00c9ac9b2861c6751b889ae8f..0d2f2bbbfec98d8b63313d0b22170d2403590fb8 100644 --- a/theories/program_logic/language.v +++ b/theories/program_logic/language.v @@ -44,6 +44,18 @@ Instance language_ctx_id Λ : LanguageCtx Λ id. Proof. constructor; naive_solver. Qed. Variant stuckness := not_stuck | maybe_stuck. +Definition stuckness_le (s1 s2 : stuckness) : bool := + match s1, s2 with + | maybe_stuck, not_stuck => false + | _, _ => true + end. +Instance: @PreOrder stuckness stuckness_le. +Proof. + split; first by case. move=>s1 s2 s3. by case: s1; case: s2; case: s3. +Qed. +Bind Scope stuckness_scope with stuckness. +Delimit Scope stuckness_scope with stuckness. +Infix "≤" := stuckness_le : stuckness_scope. Section language. Context {Λ : language}. diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v index aa228e7062321526b85dcb2f940bb261c47ad7e0..efa2340a5475f048539124eeae5843d63a719283 100644 --- a/theories/program_logic/weakestpre.v +++ b/theories/program_logic/weakestpre.v @@ -311,6 +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 Φ : + (s1 ≤ s2)%stuckness → WP e @ s1; E {{ Φ }} ⊢ WP e @ s2; E {{ Φ }}. +Proof. case: s1; case: s2 => // _. exact: wp_forget_not_stuck. 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 :