nice derived lemma for Le

barrier/lifting.v

@@ -259,14 +259,14 @@ Proof.
 Qed.
 
 Lemma wp_le_false n1 n2 E Q :
-  ~(n1 ≤ n2) →
+  n1 > n2 →
   ▷Q LitFalseV ⊑ wp (Σ:=Σ) E (Le (LitNat n1) (LitNat n2)) Q.
 Proof.
   intros Hle. etransitivity; last eapply wp_lift_pure_step with
     (φ := λ e', e' = LitFalse); last first.
   - intros ? ? ? ? Hstep. inversion_clear Hstep; last done.
-    exfalso. omega.
-  - intros ?. do 3 eexists. econstructor; omega.
+    exfalso. eapply le_not_gt with (n := n1); eassumption.
+  - intros ?. do 3 eexists. econstructor; done.
   - reflexivity.
   - apply later_mono, forall_intro=>e2. apply impl_intro_l.
     apply const_elim_l=>->.
@@ -327,7 +327,7 @@ Proof.
     by apply const_elim_l=>->.
 Qed.
 
-(** Some stateless axioms that incorporate bind *)
+(** Some derived stateless axioms *)
 
 Lemma wp_let e1 e2 E Q :
   wp (Σ:=Σ) E e1 (λ v, ▷wp (Σ:=Σ) E (e2.[v2e v/]) Q) ⊑ wp (Σ:=Σ) E (Let e1 e2) Q.
@@ -335,3 +335,15 @@ Proof.
   rewrite -(wp_bind (LetCtx EmptyCtx e2)). apply wp_mono=>v.
   rewrite -wp_lam //. by rewrite v2v.
 Qed.
+
+Lemma wp_le n1 n2 E P Q :
+  (n1 ≤ n2 → P ⊑ ▷Q LitTrueV) →
+  (n1 > n2 → P ⊑ ▷Q LitFalseV) →
+  P ⊑ wp (Σ:=Σ) E (Le (LitNat n1) (LitNat n2)) Q.
+Proof.
+  intros HPle HPgt.
+  assert (Decision (n1 ≤ n2)) as Hn12 by apply _.
+  destruct Hn12 as [Hle|Hgt].
+  - rewrite -wp_le_true; auto.
+  - assert (n1 > n2) by omega. rewrite -wp_le_false; auto.
+Qed.

barrier/tests.v

@@ -84,15 +84,14 @@ Module LiftingTests.
     rewrite -(wp_bind (CaseCtx EmptyCtx _ _)).
     rewrite -(wp_bind (LeLCtx EmptyCtx _)).
     rewrite -wp_plus -!later_intro. simpl.
-    assert (Decision (S n1 + 1 ≤ n2)) as Hn12 by apply _.
-    destruct Hn12 as [Hle|Hgt].
-    - rewrite -wp_le_true /= //. rewrite -wp_case_inl //.
+    apply wp_le; intros Hn12.
+    - rewrite -wp_case_inl //.
       rewrite -!later_intro. asimpl.
       rewrite (forall_elim (S n1)).
       eapply impl_elim; first by eapply and_elim_l. apply and_intro.
       + apply const_intro; omega.
       + by rewrite !and_elim_r.
-    - rewrite -wp_le_false /= // -wp_case_inr //.
+    - rewrite -wp_case_inr //.
       rewrite -!later_intro -wp_value' //.
       rewrite and_elim_r. apply const_elim_l=>Hle.
       assert (Heq: n1 = pred n2) by omega. by subst n1.
@@ -107,13 +106,12 @@ Module LiftingTests.
   Proof.
     rewrite -wp_lam //. asimpl.
     rewrite -(wp_bind (CaseCtx EmptyCtx _ _)).
-    assert (Decision (n ≤ 0)) as Hn by apply _.
-    destruct Hn as [Hle|Hgt].
-    - rewrite -wp_le_true /= //. rewrite -wp_case_inl //.
-      apply later_mono. rewrite -!later_intro -wp_value' //.
+    apply later_mono, wp_le; intros Hn.
+    - rewrite -wp_case_inl //.
+      rewrite -!later_intro -wp_value' //.
       assert (Heq: n = 0) by omega. by subst n.
-    - rewrite -wp_le_false /= // -wp_case_inr //.
-      apply later_mono. rewrite -!later_intro -FindPred_spec. apply and_intro.
+    - rewrite -wp_case_inr //.
+      rewrite -!later_intro -FindPred_spec. apply and_intro.
       + by apply const_intro; omega.
       + done.
   Qed.