diff --git a/barrier/lifting.v b/barrier/lifting.v index 1410d8cb9579c7286a37f4efc903716199d8393b..ca3181d9746895bdf3b143bd30c9bf6889d951bf 100644 --- a/barrier/lifting.v +++ b/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. diff --git a/barrier/tests.v b/barrier/tests.v index b7e4c82af316924a07d4d1ce0af71fb646734231..32a2d738ad0f033b6dcd8f1425909ff44c9543a2 100644 --- a/barrier/tests.v +++ b/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.