Commit 8307c4c3 by David Swasey

```This is derived from `wp_forget_not_stuck` and a trivial preorder on
stuckness bits. (The two lemmas are redundant, but I have examples
where each seems more natural than the other.)

I did *not* bake `wp_stuckness_mono` into `strong_mono` for two
reasons. Mainly, I didn't see a nice way to combine the two proofs
(beyond `cut`). Less important, changing the type of `wp_strong_mono`
will break code.```
parent 7dc00c5f
 ... @@ -57,6 +57,9 @@ Proof. solve_proper. Qed. ... @@ -57,6 +57,9 @@ Proof. solve_proper. Qed. Lemma ht_mono s E P P' Φ Φ' e : Lemma ht_mono s E P P' Φ Φ' e : (P ⊢ P') → (∀ v, Φ' v ⊢ Φ v) → {{ P' }} e @ s; E {{ Φ' }} ⊢ {{ P }} e @ s; 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. 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 : Global Instance ht_mono' s E : Proper (flip (⊢) ==> eq ==> pointwise_relation _ (⊢) ==> (⊢)) (ht s E). Proper (flip (⊢) ==> eq ==> pointwise_relation _ (⊢) ==> (⊢)) (ht s E). Proof. solve_proper. Qed. Proof. solve_proper. Qed. ... ...
 ... @@ -44,6 +44,18 @@ Instance language_ctx_id Λ : LanguageCtx Λ id. ... @@ -44,6 +44,18 @@ Instance language_ctx_id Λ : LanguageCtx Λ id. Proof. constructor; naive_solver. Qed. Proof. constructor; naive_solver. Qed. Variant stuckness := not_stuck | maybe_stuck. 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. Section language. Context {Λ : language}. Context {Λ : language}. ... ...
 ... @@ -311,6 +311,9 @@ Proof. ... @@ -311,6 +311,9 @@ Proof. iIntros (HΦ) "H"; iApply (wp_strong_mono s E E); auto. iIntros (HΦ) "H"; iApply (wp_strong_mono s E E); auto. iIntros "{\$H}" (v) "?". by iApply HΦ. iIntros "{\$H}" (v) "?". by iApply HΦ. Qed. 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 {{ Φ }}. 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. Proof. iIntros (?) "H"; iApply (wp_strong_mono s E1 E2); auto. iFrame; eauto. Qed. Global Instance wp_mono' s E e : Global Instance wp_mono' s E e : ... ...
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!