derive some more rules

theories/examples/refinements/derived.v

@@ -21,6 +21,29 @@ Section derived.
   Notation "'|==>src' P" := (weak_src_update ⊤ P)%I (at level 99) : stdpp_scope.
 
 
+  Lemma Conseq (e: expr) P P' Q Q':
+    (P ⊢ P') →
+    (∀ v, Q' v ⊢ Q v) →
+    ({{P'}} e {{v, Q' v}} ⊢ {{P}} e {{v, Q v}})%I.
+  Proof.
+    iIntros (He1 He2) "#Hh". iModIntro. rewrite He1.
+    iIntros "HP Hna". iApply (rwp_wand with "(Hh HP Hna)").
+    iIntros (v) "[$ HQ]". rewrite He2 //.
+  Qed.
+
+  Lemma HoareExists {X} (e: expr) P Q :
+    (∀ x, {{P x}} e {{v, Q v}})  ⊢ {{ ∃ x: X, P x}} e {{v, Q v}}%I.
+  Proof.
+    iIntros "#H !>". iDestruct 1 as (x) "HP". iApply ("H" with "HP").
+  Qed.
+
+  Lemma HoarePure (e: expr) φ P Q :
+    (P ⊢ ⌜φ⌝) →  (⌜φ⌝ -∗ {{P}} e {{v, Q v}}) ⊢ {{P}} e {{v, Q v}}%I.
+  Proof.
+    iIntros (Hent) "#H !> HP". iDestruct (Hent with "HP") as %Hent'.
+    iApply ("H" with "[//] HP").
+  Qed.
+
   Lemma Value (v: val): (⊢ {{True}} v {{w, ⌜v = w⌝}})%I.
   Proof.
     iIntros "!> _ $". by iApply rwp_value.
@@ -112,8 +135,8 @@ Section derived.
   Qed.
 
   Lemma HoareLöb X P Q e :
-    (∀ x :X, {{P x ∗ ▷ (∀ x, {{P x}} e {{v, Q x v}})}} e {{ v, Q x v}})
-    ⊢ ∀ x, {{ P x }} e {{v, Q x v}}.
+    (∀ x : X, {{P x ∗ ▷ (∀ x, {{P x}} e x {{v, Q x v}})}} e x {{ v, Q x v}})
+    ⊢ ∀ x, {{ P x }} e x {{v, Q x v}}.
   Proof.
     iIntros "#H". iApply bi.löb.
     iIntros "#H1" (x).
@@ -121,6 +144,15 @@ Section derived.
     iFrame "#". iFrame.
   Qed.
 
+  Lemma HoareLöbNoArgs P Q e :
+    ({{P ∗ ▷ ({{P}} e {{v, Q v}})}} e {{ v, Q v}})
+    ⊢ {{ P }} e {{v, Q v}}.
+  Proof.
+    iIntros "#H". iApply bi.löb.
+    iIntros "#H1".
+    iModIntro. iIntros "HP". iApply "H".
+    iFrame "#". iFrame.
+  Qed.
 
   (* Extended Refinement Program Logic of Transfinite Iris *)
   Lemma value_tgt_tpr (v: val): (⊢ {{True}} v {{w, ⌜v = w⌝}})%I.