From b91562fed309103869e68ca5257bf5cd84909b81 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Tue, 2 Feb 2016 02:30:14 +0100 Subject: [PATCH] Put arguments of lifting lemmas in more consistent order. --- barrier/lifting.v | 16 ++++++++-------- barrier/sugar.v | 10 +++++----- barrier/tests.v | 2 +- 3 files changed, 14 insertions(+), 14 deletions(-) diff --git a/barrier/lifting.v b/barrier/lifting.v index 5faa56d..cd947d2 100644 --- a/barrier/lifting.v +++ b/barrier/lifting.v @@ -126,7 +126,7 @@ Proof. Q (App (Rec ef) e)) //=; last by intros; inv_step; eauto. by apply later_mono, forall_intro=>e2; apply impl_intro_l, const_elim_l=>->. Qed. -Lemma wp_plus n1 n2 E Q : +Lemma wp_plus E n1 n2 Q : ▷ Q (LitNatV (n1 + n2)) ⊑ wp E (Plus (LitNat n1) (LitNat n2)) Q. Proof. rewrite -(wp_lift_pure_step E (λ e', e' = LitNat (n1 + n2))) //=; @@ -134,7 +134,7 @@ Proof. apply later_mono, forall_intro=>e2; apply impl_intro_l, const_elim_l=>->. by rewrite -wp_value'. Qed. -Lemma wp_le_true n1 n2 E Q : +Lemma wp_le_true E n1 n2 Q : n1 ≤ n2 → ▷ Q LitTrueV ⊑ wp E (Le (LitNat n1) (LitNat n2)) Q. Proof. @@ -143,7 +143,7 @@ Proof. apply later_mono, forall_intro=>e2; apply impl_intro_l, const_elim_l=>->. by rewrite -wp_value'. Qed. -Lemma wp_le_false n1 n2 E Q : +Lemma wp_le_false E n1 n2 Q : n1 > n2 → ▷ Q LitFalseV ⊑ wp E (Le (LitNat n1) (LitNat n2)) Q. Proof. @@ -152,7 +152,7 @@ Proof. apply later_mono, forall_intro=>e2; apply impl_intro_l, const_elim_l=>->. by rewrite -wp_value'. Qed. -Lemma wp_fst e1 v1 e2 v2 E Q : +Lemma wp_fst E e1 v1 e2 v2 Q : to_val e1 = Some v1 → to_val e2 = Some v2 → ▷Q v1 ⊑ wp E (Fst (Pair e1 e2)) Q. Proof. @@ -161,7 +161,7 @@ Proof. apply later_mono, forall_intro=>e2'; apply impl_intro_l, const_elim_l=>->. by rewrite -wp_value'. Qed. -Lemma wp_snd e1 v1 e2 v2 E Q : +Lemma wp_snd E e1 v1 e2 v2 Q : to_val e1 = Some v1 → to_val e2 = Some v2 → ▷ Q v2 ⊑ wp E (Snd (Pair e1 e2)) Q. Proof. @@ -170,7 +170,7 @@ Proof. apply later_mono, forall_intro=>e2'; apply impl_intro_l, const_elim_l=>->. by rewrite -wp_value'. Qed. -Lemma wp_case_inl e0 v0 e1 e2 E Q : +Lemma wp_case_inl E e0 v0 e1 e2 Q : to_val e0 = Some v0 → ▷ wp E e1.[e0/] Q ⊑ wp E (Case (InjL e0) e1 e2) Q. Proof. @@ -178,7 +178,7 @@ Proof. (Case (InjL e0) e1 e2)) //=; last by intros; inv_step; eauto. by apply later_mono, forall_intro=>e1'; apply impl_intro_l, const_elim_l=>->. Qed. -Lemma wp_case_inr e0 v0 e1 e2 E Q : +Lemma wp_case_inr E e0 v0 e1 e2 Q : to_val e0 = Some v0 → ▷ wp E e2.[e0/] Q ⊑ wp E (Case (InjR e0) e1 e2) Q. Proof. @@ -188,7 +188,7 @@ Proof. Qed. (** Some derived stateless axioms *) -Lemma wp_le n1 n2 E P Q : +Lemma wp_le E n1 n2 P Q : (n1 ≤ n2 → P ⊑ ▷ Q LitTrueV) → (n1 > n2 → P ⊑ ▷ Q LitFalseV) → P ⊑ wp E (Le (LitNat n1) (LitNat n2)) Q. diff --git a/barrier/sugar.v b/barrier/sugar.v index 6c39d0c..92869fe 100644 --- a/barrier/sugar.v +++ b/barrier/sugar.v @@ -31,17 +31,17 @@ Proof. to talk to the Autosubst guys. *) by asimpl. Qed. -Lemma wp_let e1 e2 E Q : +Lemma wp_let E e1 e2 Q : wp E e1 (λ v, ▷wp E (e2.[of_val v/]) Q) ⊑ wp E (Let e1 e2) Q. Proof. rewrite -(wp_bind [LetCtx e2]). apply wp_mono=>v. by rewrite -wp_lam //= to_of_val. Qed. -Lemma wp_if_true e1 e2 E Q : ▷ wp E e1 Q ⊑ wp E (If LitTrue e1 e2) Q. +Lemma wp_if_true E e1 e2 Q : ▷ wp E e1 Q ⊑ wp E (If LitTrue e1 e2) Q. Proof. rewrite -wp_case_inl //. by asimpl. Qed. -Lemma wp_if_false e1 e2 E Q : ▷ wp E e2 Q ⊑ wp E (If LitFalse e1 e2) Q. +Lemma wp_if_false E e1 e2 Q : ▷ wp E e2 Q ⊑ wp E (If LitFalse e1 e2) Q. Proof. rewrite -wp_case_inr //. by asimpl. Qed. -Lemma wp_lt n1 n2 E P Q : +Lemma wp_lt E n1 n2 P Q : (n1 < n2 → P ⊑ ▷ Q LitTrueV) → (n1 ≥ n2 → P ⊑ ▷ Q LitFalseV) → P ⊑ wp E (Lt (LitNat n1) (LitNat n2)) Q. @@ -49,7 +49,7 @@ Proof. intros; rewrite -(wp_bind [LeLCtx _]) -wp_plus -later_intro /=. auto using wp_le with lia. Qed. -Lemma wp_eq n1 n2 E P Q : +Lemma wp_eq E n1 n2 P Q : (n1 = n2 → P ⊑ ▷ Q LitTrueV) → (n1 ≠ n2 → P ⊑ ▷ Q LitFalseV) → P ⊑ wp E (Eq (LitNat n1) (LitNat n2)) Q. diff --git a/barrier/tests.v b/barrier/tests.v index 3a33c75..4f0107b 100644 --- a/barrier/tests.v +++ b/barrier/tests.v @@ -73,7 +73,7 @@ Module LiftingTests. { apply and_mono; first done. by rewrite -later_intro. } apply later_mono. (* Go on. *) - rewrite -(wp_let _ (FindPred' (LitNat n1) (Var 0) (LitNat n2) (FindPred \$ LitNat n2))). + rewrite -(wp_let _ _ (FindPred' (LitNat n1) (Var 0) (LitNat n2) (FindPred \$ LitNat n2))). rewrite -wp_plus. asimpl. rewrite -(wp_bind [CaseCtx _ _]). rewrite -!later_intro /=. -- GitLab