From 1cf19e9c0cdfdbe999df5b6ae5021cc2dda84cc7 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Mon, 29 Feb 2016 20:39:28 +0100 Subject: [PATCH] prove a weaker derived form of recv_strengthen; more "\lam:" notation --- algebra/upred.v | 7 +++++++ barrier/proof.v | 7 +++++++ heap_lang/notation.v | 8 ++++++++ 3 files changed, 22 insertions(+) diff --git a/algebra/upred.v b/algebra/upred.v index 5e0cf611..659af0b6 100644 --- a/algebra/upred.v +++ b/algebra/upred.v @@ -747,6 +747,13 @@ Proof. Qed. Lemma wand_diag P : (P -★ P)%I ≡ True%I. Proof. apply (anti_symm _); auto. apply wand_intro_l; by rewrite right_id. Qed. +Lemma wand_entails P Q : True ⊑ (P -★ Q) → P ⊑ Q. +Proof. + intros HPQ. eapply sep_elim_True_r; first exact: HPQ. by rewrite wand_elim_r. +Qed. +Lemma entails_wand P Q : (P ⊑ Q) → True ⊑ (P -★ Q). +Proof. auto using wand_intro_l. Qed. + Lemma sep_and P Q : (P ★ Q) ⊑ (P ∧ Q). Proof. auto. Qed. Lemma impl_wand P Q : (P → Q) ⊑ (P -★ Q). diff --git a/barrier/proof.v b/barrier/proof.v index 4e128f74..c6b4caff 100644 --- a/barrier/proof.v +++ b/barrier/proof.v @@ -332,4 +332,11 @@ Proof. rewrite (later_intro (P1 -★ _)%I) -later_sep. apply later_mono. apply wand_intro_l. by rewrite !assoc wand_elim_r wand_elim_r. Qed. + +Lemma recv_mono l P1 P2 : + P1 ⊑ P2 → recv l P1 ⊑ recv l P2. +Proof. + intros HP%entails_wand. apply wand_entails. rewrite HP. apply recv_strengthen. +Qed. + End proof. diff --git a/heap_lang/notation.v b/heap_lang/notation.v index 1ec0f937..f79f1597 100644 --- a/heap_lang/notation.v +++ b/heap_lang/notation.v @@ -78,3 +78,11 @@ Notation "'rec:' f x y z := e" := (Rec f x (Lam y (Lam z e%L))) (at level 102, f, x, y, z at level 1, e at level 200) : lang_scope. Notation "'rec:' f x y z := e" := (RecV f x (Lam y (Lam z e%L))) (at level 102, f, x, y, z at level 1, e at level 200) : lang_scope. +Notation "λ: x y , e" := (Lam x (Lam y e%L)) + (at level 102, x, y at level 1, e at level 200) : lang_scope. +Notation "λ: x y , e" := (LamV x (Lam y e%L)) + (at level 102, x, y at level 1, e at level 200) : lang_scope. +Notation "λ: x y z , e" := (Lam x (LamV y (LamV z e%L))) + (at level 102, x, y, z at level 1, e at level 200) : lang_scope. +Notation "λ: x y z , e" := (LamV x (LamV y (LamV z e%L))) + (at level 102, x, y, z at level 1, e at level 200) : lang_scope. -- GitLab