diff --git a/theories/channel/channel.v b/theories/channel/channel.v index 622e9b372d9ae6181a4f08046b91eae98b5ea40c..1fe1e31ab3c8ae6186b0cc4c1ab121da157afc2f 100644 --- a/theories/channel/channel.v +++ b/theories/channel/channel.v @@ -222,7 +222,7 @@ Section channel. (** A version written without Texan triples that is more convenient to use (via [iApply] in Coq. *) - Lemma send_proto_spec {TT} Φ c v (pc : TT → val * iProp Σ * iProto Σ) : + Lemma send_spec {TT} Φ c v (pc : TT → val * iProp Σ * iProto Σ) : c ↣ iProto_message Send pc -∗ (∃.. x : TT, ⌜ v = (pc x).1.1 ⌝ ∗ (pc x).1.2 ∗ ▷ (c ↣ (pc x).2 -∗ Φ #())) -∗ @@ -279,7 +279,7 @@ Section channel. (** A version written without Texan triples that is more convenient to use (via [iApply] in Coq. *) - Lemma recv_proto_spec {TT} Φ c (pc : TT → val * iProp Σ * iProto Σ) : + Lemma recv_spec {TT} Φ c (pc : TT → val * iProp Σ * iProto Σ) : c ↣ iProto_message Receive pc -∗ ▷ (∀.. x : TT, c ↣ (pc x).2 -∗ (pc x).1.2 -∗ Φ (pc x).1.1) -∗ WP recv c {{ Φ }}. @@ -296,7 +296,7 @@ Section channel. {{{ RET #(); c ↣ (if b then p1 else p2) }}}. Proof. rewrite /iProto_branch. iIntros (Φ) "[Hc HP] HΦ". - iApply (send_proto_spec with "Hc"); simpl; eauto with iFrame. + iApply (send_spec with "Hc"); simpl; eauto with iFrame. Qed. Lemma branch_spec c P1 P2 p1 p2 : @@ -305,7 +305,7 @@ Section channel. {{{ b, RET #b; c ↣ (if b : bool then p1 else p2) ∗ if b then P1 else P2 }}}. Proof. rewrite /iProto_branch. iIntros (Φ) "Hc HΦ". - iApply (recv_proto_spec with "Hc"); simpl. + iApply (recv_spec with "Hc"); simpl. iIntros "!>" (b) "Hc HP". iApply "HΦ". iFrame. Qed. End channel. diff --git a/theories/channel/proofmode.v b/theories/channel/proofmode.v index 2ee4e79faa27d842c3ee0c8b1b688502aa524e6e..2eecbbdf19bc7e496bc820c36b48315f64ec247a 100644 --- a/theories/channel/proofmode.v +++ b/theories/channel/proofmode.v @@ -178,7 +178,7 @@ Lemma tac_wp_recv `{!chanG Σ, !heapG Σ} {TT : tele} Δ i j K Proof. rewrite envs_entails_eq /ProtoNormalize /= tforall_forall right_id=> ? Hp HΦ. rewrite envs_lookup_sound //; simpl. rewrite -Hp. - rewrite -wp_bind. eapply bi.wand_apply; [by eapply recv_proto_spec|f_equiv]. + rewrite -wp_bind. eapply bi.wand_apply; [by eapply recv_spec|f_equiv]. rewrite -bi.later_intro bi_tforall_forall; apply bi.forall_intro=> x. specialize (HΦ x). destruct (envs_app _ _) as [Δ'|] eqn:HΔ'=> //. rewrite envs_app_sound //; simpl. @@ -262,7 +262,7 @@ Lemma tac_wp_send `{!chanG Σ, !heapG Σ} {TT : tele} Δ neg i js K Proof. rewrite envs_entails_eq /ProtoNormalize /= right_id texist_exist=> ? Hp [x HΦ]. rewrite envs_lookup_sound //; simpl. rewrite -Hp. - rewrite -wp_bind. eapply bi.wand_apply; [by eapply send_proto_spec|f_equiv]. + rewrite -wp_bind. eapply bi.wand_apply; [by eapply send_spec|f_equiv]. rewrite bi_texist_exist -(bi.exist_intro x). destruct (envs_split _ _ _) as [[Δ1 Δ2]|] eqn:? => //. destruct (envs_app _ _ _) as [Δ2'|] eqn:? => //.