Commit 1cf19e9c authored by Ralf Jung's avatar Ralf Jung

prove a weaker derived form of recv_strengthen; more "\lam:" notation

parent bf610ff2
......@@ -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).
......
......@@ -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.
......@@ -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.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment