Commit 19f8a53a authored by Robbert Krebbers's avatar Robbert Krebbers

Remove some old `_proto`s in names.

parent 085b698d
...@@ -222,7 +222,7 @@ Section channel. ...@@ -222,7 +222,7 @@ Section channel.
(** A version written without Texan triples that is more convenient to use (** A version written without Texan triples that is more convenient to use
(via [iApply] in Coq. *) (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 - c iProto_message Send pc -
(.. x : TT, (.. x : TT,
v = (pc x).1.1 (pc x).1.2 (c (pc x).2 - Φ #())) - v = (pc x).1.1 (pc x).1.2 (c (pc x).2 - Φ #())) -
...@@ -279,7 +279,7 @@ Section channel. ...@@ -279,7 +279,7 @@ Section channel.
(** A version written without Texan triples that is more convenient to use (** A version written without Texan triples that is more convenient to use
(via [iApply] in Coq. *) (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 - c iProto_message Receive pc -
(.. x : TT, c (pc x).2 - (pc x).1.2 - Φ (pc x).1.1) - (.. x : TT, c (pc x).2 - (pc x).1.2 - Φ (pc x).1.1) -
WP recv c {{ Φ }}. WP recv c {{ Φ }}.
...@@ -296,7 +296,7 @@ Section channel. ...@@ -296,7 +296,7 @@ Section channel.
{{{ RET #(); c (if b then p1 else p2) }}}. {{{ RET #(); c (if b then p1 else p2) }}}.
Proof. Proof.
rewrite /iProto_branch. iIntros (Φ) "[Hc HP] HΦ". 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. Qed.
Lemma branch_spec c P1 P2 p1 p2 : Lemma branch_spec c P1 P2 p1 p2 :
...@@ -305,7 +305,7 @@ Section channel. ...@@ -305,7 +305,7 @@ Section channel.
{{{ b, RET #b; c (if b : bool then p1 else p2) if b then P1 else P2 }}}. {{{ b, RET #b; c (if b : bool then p1 else p2) if b then P1 else P2 }}}.
Proof. Proof.
rewrite /iProto_branch. iIntros (Φ) "Hc HΦ". 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. iIntros "!>" (b) "Hc HP". iApply "HΦ". iFrame.
Qed. Qed.
End channel. End channel.
...@@ -178,7 +178,7 @@ Lemma tac_wp_recv `{!chanG Σ, !heapG Σ} {TT : tele} Δ i j K ...@@ -178,7 +178,7 @@ Lemma tac_wp_recv `{!chanG Σ, !heapG Σ} {TT : tele} Δ i j K
Proof. Proof.
rewrite envs_entails_eq /ProtoNormalize /= tforall_forall right_id=> ? Hp HΦ. rewrite envs_entails_eq /ProtoNormalize /= tforall_forall right_id=> ? Hp HΦ.
rewrite envs_lookup_sound //; simpl. rewrite -Hp. 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. rewrite -bi.later_intro bi_tforall_forall; apply bi.forall_intro=> x.
specialize (HΦ x). destruct (envs_app _ _) as [Δ'|] eqn:HΔ'=> //. specialize (HΦ x). destruct (envs_app _ _) as [Δ'|] eqn:HΔ'=> //.
rewrite envs_app_sound //; simpl. rewrite envs_app_sound //; simpl.
...@@ -262,7 +262,7 @@ Lemma tac_wp_send `{!chanG Σ, !heapG Σ} {TT : tele} Δ neg i js K ...@@ -262,7 +262,7 @@ Lemma tac_wp_send `{!chanG Σ, !heapG Σ} {TT : tele} Δ neg i js K
Proof. Proof.
rewrite envs_entails_eq /ProtoNormalize /= right_id texist_exist=> ? Hp [x HΦ]. rewrite envs_entails_eq /ProtoNormalize /= right_id texist_exist=> ? Hp [x HΦ].
rewrite envs_lookup_sound //; simpl. rewrite -Hp. 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). rewrite bi_texist_exist -(bi.exist_intro x).
destruct (envs_split _ _ _) as [[Δ1 Δ2]|] eqn:? => //. destruct (envs_split _ _ _) as [[Δ1 Δ2]|] eqn:? => //.
destruct (envs_app _ _ _) as [Δ2'|] eqn:? => //. destruct (envs_app _ _ _) as [Δ2'|] eqn:? => //.
......
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