From a06b94986df4131471185b4cd6bd2ddb30ef8663 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 15 Apr 2020 20:46:51 +0200
Subject: [PATCH] Misc cleanup.

---
 theories/logrel/session_types.v |  68 ++++------------
 theories/logrel/subtyping.v     | 134 +++++++++++++-------------------
 theories/logrel/types.v         |  62 +++++----------
 3 files changed, 86 insertions(+), 178 deletions(-)

diff --git a/theories/logrel/session_types.v b/theories/logrel/session_types.v
index 4264ba5..dc70d5a 100644
--- a/theories/logrel/session_types.v
+++ b/theories/logrel/session_types.v
@@ -26,14 +26,10 @@ Section protocols.
   Definition lsty_branch (Ps : gmap Z (lsty Î£)) : lsty Î£ :=
     lsty_choice Recv Ps.
 
-  Definition lsty_rec1 (C : lsty Î£ â†’ lsty Î£)
-             `{!Contractive C}
-             (rec : lsty Î£) : lsty Î£ :=
-    Lsty (C rec).
-
+  Definition lsty_rec1 (C : lsty Î£ â†’ lsty Î£) `{!Contractive C}
+    (rec : lsty Î£) : lsty Î£ := Lsty (C rec).
   Instance lsty_rec1_contractive C `{!Contractive C} : Contractive (lsty_rec1 C).
   Proof. solve_contractive. Qed.
-
   Definition lsty_rec (C : lsty Î£ â†’ lsty Î£) `{!Contractive C} : lsty Î£ :=
     fixpoint (lsty_rec1 C).
 
@@ -41,93 +37,57 @@ Section protocols.
     Lsty (iProto_dual P).
 
   Definition lsty_app (P1 P2 : lsty Î£) : lsty Î£ :=
-    Lsty (iProto_app P1 P2).
-
+    Lsty (P1 <++> P2).
 End protocols.
 
 Section Propers.
   Context `{heapG Î£, protoG Î£}.
 
   Global Instance lsty_message_ne a : NonExpansive2 (@lsty_message Î£ a).
-  Proof.
-    intros n A A' H1 P P' H2.
-    rewrite /lsty_send.
-    apply Lsty_ne.
-    apply iProto_message_ne; simpl; try done.
-  Qed.
-
+  Proof. intros n A A' ? P P' ?. by apply iProto_message_ne; simpl. Qed.
   Global Instance lsty_message_contractive n a :
     Proper (dist_later n ==> dist_later n ==> dist n) (@lsty_message Î£ a).
   Proof.
-    intros A A' H1 P P' H2.
-    rewrite /lsty_send.
-    apply Lsty_ne.
-    apply iProto_message_contractive; simpl; try done.
-    intros v.
-    destruct n as [|n]; try done.
-    apply H1.
+    intros A A' ? P P' ?.
+    apply iProto_message_contractive; simpl; done || by destruct n.
   Qed.
 
   Global Instance lsty_send_ne : NonExpansive2 (@lsty_send Î£).
   Proof. solve_proper. Qed.
-
   Global Instance lsty_send_contractive n :
     Proper (dist_later n ==> dist_later n ==> dist n) (@lsty_send Î£).
   Proof. solve_contractive. Qed.
 
   Global Instance lsty_recv_ne : NonExpansive2 (@lsty_recv Î£).
   Proof. solve_proper. Qed.
-
   Global Instance lsty_recv_contractive n :
     Proper (dist_later n ==> dist_later n ==> dist n) (@lsty_recv Î£).
   Proof. solve_contractive. Qed.
 
   Global Instance lsty_choice_ne a : NonExpansive (@lsty_choice Î£ a).
   Proof.
-    intros n Ps1 Ps2 Pseq.
-    apply Lsty_ne.
-    apply iProto_message_ne; simpl; try done; solve_proper.
+    intros n Ps1 Ps2 Pseq. apply iProto_message_ne; simpl; solve_proper.
   Qed.
-
-  Global Instance lsty_choice_contractive n a :
-    Proper (dist_later n ==> dist n) (@lsty_choice Î£ a).
+  Global Instance lsty_choice_contractive a : Contractive (@lsty_choice Î£ a).
   Proof.
-    intros Ps1 Ps2 Pseq.
-    apply Lsty_ne.
-    apply iProto_message_contractive; simpl; try done;
-      destruct n=> //=; solve_proper.
+    intros ? Ps1 Ps2 ?.
+    apply iProto_message_contractive; destruct n; simpl; done || solve_proper.
   Qed.
 
   Global Instance lsty_select_ne : NonExpansive (@lsty_select Î£).
   Proof. solve_proper. Qed.
-
-  Global Instance lsty_select_contractive n :
-    Proper (dist_later n ==> dist n) (@lsty_select Î£).
+  Global Instance lsty_select_contractive : Contractive (@lsty_select Î£).
   Proof. solve_contractive. Qed.
 
   Global Instance lsty_branch_ne : NonExpansive (@lsty_branch Î£).
   Proof. solve_proper. Qed.
-
-  Global Instance lsty_branch_contractive n :
-    Proper (dist_later n ==> dist n) (@lsty_branch Î£).
+  Global Instance lsty_branch_contractive : Contractive (@lsty_branch Î£).
   Proof. solve_contractive. Qed.
 
   Global Instance lsty_dual_ne : NonExpansive (@lsty_dual Î£).
-  Proof.
-    intros n P P' HP.
-    rewrite /lsty_dual.
-    apply Lsty_ne.
-    by apply iProto_dual_ne.
-  Qed.
-
+  Proof. solve_proper. Qed.
   Global Instance lsty_app_ne : NonExpansive2 (@lsty_app Î£).
-  Proof.
-    intros n P1 P1' H1 P2 P2' H2.
-    rewrite /lsty_app.
-    apply Lsty_ne.
-    by apply iProto_app_ne.
-  Qed.
-
+  Proof. solve_proper. Qed.
 End Propers.
 
 Notation "'END'" := lsty_end : lsty_scope.
diff --git a/theories/logrel/subtyping.v b/theories/logrel/subtyping.v
index 6b6df0d..443e38e 100644
--- a/theories/logrel/subtyping.v
+++ b/theories/logrel/subtyping.v
@@ -5,30 +5,26 @@ From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import proofmode.
 
 Definition lty_le {Î£} (A1 A2 : lty Î£) : iProp Î£ :=
-  â–¡ âˆ€ v, (A1 v -âˆ— A2 v).
-
+  â–¡ âˆ€ v, A1 v -âˆ— A2 v.
 Arguments lty_le {_} _%lty _%lty.
 Infix "<:" := lty_le (at level 70).
 Instance: Params (@lty_le) 1 := {}.
 
 Instance lty_le_ne {Î£} : NonExpansive2 (@lty_le Î£).
 Proof. solve_proper. Qed.
-Instance lty_le_proper {Î£} :
-  Proper ((â‰¡) ==> (â‰¡) ==> (â‰¡)) (@lty_le Î£).
+Instance lty_le_proper {Î£} : Proper ((â‰¡) ==> (â‰¡) ==> (â‰¡)) (@lty_le Î£).
 Proof. solve_proper. Qed.
 
 Definition lsty_le {Î£} (P1 P2 : lsty Î£) : iProp Î£ :=
-  â–¡ (iProto_le P1 P2).
-
+  â–¡ iProto_le P1 P2.
 Arguments lsty_le {_} _%lsty _%lsty.
 Infix "<p:" := lsty_le (at level 70).
 Instance: Params (@lsty_le) 1 := {}.
 
 Instance lsty_le_ne {Î£} : NonExpansive2 (@lsty_le Î£).
-Proof. solve_proper_prepare. f_equiv. solve_proper. Qed.
-Instance lsty_le_proper {Î£} :
-  Proper ((â‰¡) ==> (â‰¡) ==> (â‰¡)) (@lsty_le Î£).
-Proof. apply ne_proper_2. apply _. Qed.
+Proof. solve_proper. Qed.
+Instance lsty_le_proper {Î£} : Proper ((â‰¡) ==> (â‰¡) ==> (â‰¡)) (@lsty_le Î£).
+Proof. solve_proper. Qed.
 
 Section subtype.
   Context `{heapG Î£, chanG Î£}.
@@ -153,21 +149,11 @@ Section subtype.
     mutex A1 <: mutex A2.
   Proof.
     iIntros "#Hle1 #Hle2" (v) "!>". iDestruct 1 as (Î³ l lk ->) "Hinv".
-    rewrite /spin_lock.is_lock.
     iExists Î³, l, lk. iSplit; first done.
-    rewrite /spin_lock.is_lock.
-    iDestruct "Hinv" as (l' ->) "Hinv".
-    iExists l'.
-    iSplit; first done.
-    iApply (inv_iff with "Hinv"); iIntros "!> !>". iSplit.
-    - iDestruct 1 as (v) "[Hl HA]". iExists v. iFrame "Hl".
-      destruct v; first done.
-      iDestruct "HA" as "[Hown HA]". iDestruct "HA" as (inner) "[Hinner HA]".
-      iDestruct ("Hle1" with "HA") as "HA". eauto with iFrame.
-    - iDestruct 1 as (v) "[Hl HA]". iExists v. iFrame "Hl".
-      destruct v; first done.
-      iDestruct "HA" as "[Hown HA]". iDestruct "HA" as (inner) "[Hinner HA]".
-      iDestruct ("Hle2" with "HA") as "HA". eauto with iFrame.
+    iApply (spin_lock.is_lock_iff with "Hinv").
+    iIntros "!> !>". iSplit.
+    - iDestruct 1 as (v) "[Hl HA]". iExists v. iFrame "Hl". by iApply "Hle1".
+    - iDestruct 1 as (v) "[Hl HA]". iExists v. iFrame "Hl". by iApply "Hle2".
   Qed.
 
   Lemma lty_mutexguard_le A1 A2 :
@@ -176,22 +162,11 @@ Section subtype.
   Proof.
     iIntros "#Hle1 #Hle2" (v) "!>".
     iDestruct 1 as (Î³ l lk w ->) "[Hinv [Hlock Hinner]]".
-    rewrite /spin_lock.is_lock.
     iExists Î³, l, lk, w. iSplit; first done.
-    rewrite /spin_lock.is_lock.
-    iFrame "Hlock Hinner".
-    iDestruct "Hinv" as (l' ->) "Hinv".
-    iExists l'.
-    iSplit; first done.
-    iApply (inv_iff with "Hinv"); iIntros "!> !>". iSplit.
-    - iDestruct 1 as (v) "[Hl HA]". iExists v. iFrame "Hl".
-      destruct v; first done.
-      iDestruct "HA" as "[Hown HA]". iDestruct "HA" as (inner) "[Hinner HA]".
-      iDestruct ("Hle1" with "HA") as "HA". eauto with iFrame.
-    - iDestruct 1 as (v) "[Hl HA]". iExists v. iFrame "Hl".
-      destruct v; first done.
-      iDestruct "HA" as "[Hown HA]". iDestruct "HA" as (inner) "[Hinner HA]".
-      iDestruct ("Hle2" with "HA") as "HA". eauto with iFrame.
+    iFrame "Hlock Hinner". iApply (spin_lock.is_lock_iff with "Hinv").
+    iIntros "!> !>". iSplit.
+    - iDestruct 1 as (v) "[Hl HA]". iExists v. iFrame "Hl". by iApply "Hle1".
+    - iDestruct 1 as (v) "[Hl HA]". iExists v. iFrame "Hl". by iApply "Hle2".
   Qed.
 
   Lemma lsty_le_refl P : âŠ¢ P <p: P.
@@ -216,7 +191,7 @@ Section subtype.
     (<??> A1 ; P1) <p: (<??> A2 ; P2).
   Proof.
     iIntros "#HAle #HPle !>".
-    iApply iProto_le_recv=> /=.
+    iApply iProto_le_recv; simpl.
     iIntros (x) "H !>".
     iDestruct ("HAle" with "H") as "H".
     eauto with iFrame.
@@ -230,31 +205,29 @@ Section subtype.
     iExists _, _,
       (tele_app (TT:=[tele _]) (Î» x2, (x2, A2 x2, (P:iProto Î£)))),
       (tele_app (TT:=[tele _]) (Î» x1, (x1, A1 x1, (P:iProto Î£)))),
-    x2, x1.
-    simpl.
+      x2, x1; simpl.
     do 2 (iSplit; [done|]).
     iFrame "HP1 HP2".
     iModIntro.
     do 2 (iSplitR; [iApply iProto_le_refl|]). by iFrame.
   Qed.
 
-  Lemma lsty_select_le_insert (Ps1 Ps2 : gmap Z (lsty Î£)) :
+  Lemma lsty_select_le_subseteq (Ps1 Ps2 : gmap Z (lsty Î£)) :
     Ps2 âŠ† Ps1 â†’
     âŠ¢ lsty_select Ps1 <p: lsty_select Ps2.
   Proof.
     iIntros (Hsub) "!>".
-    iApply iProto_le_send.
-    iIntros (x) ">% !>"=> /=.
-    iExists _. iSplit=> //.
+    iApply iProto_le_send; simpl.
+    iIntros (x) ">% !> /=".
+    iExists _. iSplit; first done.
     iSplit.
-    - iNext. iPureIntro. by eapply lookup_weaken_is_Some.
-    - iNext.
-      destruct H1 as [P H1].
-      assert (Ps1 !! x = Some P).
-      { by eapply lookup_weaken. }
-      rewrite (lookup_total_correct Ps1 x P)=> //.
-      rewrite (lookup_total_correct Ps2 x P)=> //.
-      iApply iProto_le_refl.
+    { iNext. iPureIntro. by eapply lookup_weaken_is_Some. }
+    iNext.
+    destruct H1 as [P H1].
+    assert (Ps1 !! x = Some P) by eauto using lookup_weaken.
+    rewrite (lookup_total_correct Ps1 x P) //.
+    rewrite (lookup_total_correct Ps2 x P) //.
+    iApply iProto_le_refl.
   Qed.
 
   Lemma lsty_select_le (Ps1 Ps2 : gmap Z (lsty Î£)) :
@@ -262,54 +235,52 @@ Section subtype.
     lsty_select Ps1 <p: lsty_select Ps2.
   Proof.
     iIntros "#H1 !>".
-    iApply iProto_le_send=> /=.
-    iIntros (x) "H !>".
+    iApply iProto_le_send; simpl.
+    iIntros (x) ">H !>"; iDestruct "H" as %Hsome.
     iExists x. iSplit=> //. iSplit.
-    - iNext. iDestruct "H" as %Hsome.
+    - iNext. 
       iDestruct (big_sepM2_forall with "H1") as "[% _]".
-      iPureIntro. by apply H1.
-    - iNext. iDestruct "H" as %Hsome.
+      iPureIntro. naive_solver.
+    - iNext.
       iDestruct (big_sepM2_forall with "H1") as "[% H]".
       iApply ("H" with "[] []").
-      + iPureIntro. by apply lookup_lookup_total, H1.
+      + iPureIntro. apply lookup_lookup_total; naive_solver.
       + iPureIntro. by apply lookup_lookup_total.
   Qed.
 
-  Lemma lsty_branch_le_insert (Ps1 Ps2 : gmap Z (lsty Î£)) :
+  Lemma lsty_branch_le_subseteq (Ps1 Ps2 : gmap Z (lsty Î£)) :
     Ps1 âŠ† Ps2 â†’
     âŠ¢ lsty_branch Ps1 <p: lsty_branch Ps2.
   Proof.
     iIntros (Hsub) "!>".
-    iApply iProto_le_recv.
-    iIntros (x) ">% !>"=> /=.
-    iExists _. iSplit=> //.
+    iApply iProto_le_recv; simpl.
+    iIntros (x) ">% !> /=".
+    iExists _. iSplit; first done.
     iSplit.
-    - iNext. iPureIntro. by eapply lookup_weaken_is_Some.
-    - iNext.
-      destruct H1 as [P H1].
-      assert (Ps2 !! x = Some P).
-      { by eapply lookup_weaken. }
-      rewrite (lookup_total_correct Ps1 x P)=> //.
-      rewrite (lookup_total_correct Ps2 x P)=> //.
-      iApply iProto_le_refl.
+    { iNext. iPureIntro. by eapply lookup_weaken_is_Some. }
+    iNext.
+    destruct H1 as [P ?].
+    assert (Ps2 !! x = Some P) by eauto using lookup_weaken.
+    rewrite (lookup_total_correct Ps1 x P) //.
+    rewrite (lookup_total_correct Ps2 x P) //.
+    iApply iProto_le_refl.
   Qed.
 
   Lemma lsty_branch_le (Ps1 Ps2 : gmap Z (lsty Î£)) :
     (â–· [âˆ— map] i â†¦ P1;P2 âˆˆ Ps1; Ps2, P1 <p: P2) -âˆ—
     lsty_branch Ps1 <p: lsty_branch Ps2.
   Proof.
-    iIntros "#H1 !>".
-    iApply iProto_le_recv=> /=.
-    iIntros (x) "H !>".
-    iExists x. iSplit=> //. iSplit.
-    - iNext. iDestruct "H" as %Hsome.
+    iIntros "#H1 !>". iApply iProto_le_recv.
+    iIntros (x) ">H !>"; iDestruct "H" as %Hsome.
+    iExists x. iSplit; first done. iSplit.
+    - iNext.
       iDestruct (big_sepM2_forall with "H1") as "[% _]".
-      iPureIntro. by apply H1.
-    - iNext. iDestruct "H" as %Hsome.
+      iPureIntro. by naive_solver.
+    - iNext.
       iDestruct (big_sepM2_forall with "H1") as "[% H]".
       iApply ("H" with "[] []").
       + iPureIntro. by apply lookup_lookup_total.
-      + iPureIntro. by apply lookup_lookup_total, H1.
+      + iPureIntro. by apply lookup_lookup_total; naive_solver.
   Qed.
 
   Lemma lsty_app_le P11 P12 P21 P22 :
@@ -337,9 +308,8 @@ Section subtype.
     (â–¡ âˆ€ P P', â–· (P <p: P') -âˆ— C1 P <p: C2 P') -âˆ—
     lsty_rec C1 <p: lsty_rec C2.
   Proof.
-    iIntros "#Hle".
+    iIntros "#Hle !>".
     iLÃ¶b as "IH".
-    iIntros "!>".
     rewrite /lsty_rec.
     iEval (rewrite fixpoint_unfold).
     iEval (rewrite (fixpoint_unfold (lsty_rec1 C2))).
diff --git a/theories/logrel/types.v b/theories/logrel/types.v
index a42b205..d456a3c 100644
--- a/theories/logrel/types.v
+++ b/theories/logrel/types.v
@@ -737,10 +737,9 @@ Section properties.
     Proof.
       iIntros (Hin) "#Hc !>".
       iIntros (vs) "H /=".
-      rewrite /chanselect. simpl.
-      iDestruct ("Hc" with "H") as "Hc'".
-      iMod (wp_value_inv with "Hc'") as "Hc'".
-      wp_send with "[]"=> //; eauto.
+      rewrite /chanselect.
+      iMod (wp_value_inv with "(Hc H)") as "Hc'".
+      wp_send with "[]"; [by eauto|].
       rewrite (lookup_total_correct Ps i P)=> //.
       by wp_pures.
     Qed.
@@ -753,54 +752,33 @@ Section properties.
     Lemma ltyped_chanbranch Ps A xs :
       (âˆ€ x, x âˆˆ xs â†” is_Some (Ps !! x)) â†’
       âŠ¢ âˆ… âŠ¨ chanbranch xs : chan (lsty_branch Ps) âŠ¸
-                              lty_arr_list
-                                ((Î» x, (chan (Ps !!! x) âŠ¸ A)%lty) <$> xs) A.
+        lty_arr_list ((Î» x, (chan (Ps !!! x) âŠ¸ A)%lty) <$> xs) A.
     Proof.
       iIntros (Hdom) "!>". iIntros (vs) "Hvs".
-      iApply wp_value.
-      iIntros (c) "Hc".
-      wp_lam=> /=.
+      iApply wp_value. iIntros (c) "Hc". wp_lam.
       rewrite -subst_map_singleton.
-      iApply (lty_arr_list_spec).
+      iApply lty_arr_list_spec.
       { by rewrite fmap_length. }
       iIntros (ws) "H".
       rewrite big_sepL2_fmap_l.
       iDestruct (big_sepL2_length with "H") as %Heq.
-      rewrite -insert_union_singleton_r=> /=;
-        last by apply lookup_map_string_seq_None=> /=.
-      rewrite lookup_insert.
-      wp_recv (x) as "%". rename H1 into HPs_Some.
+      rewrite -insert_union_singleton_r; last by apply lookup_map_string_seq_None.
+      rewrite /= lookup_insert.
+      wp_recv (x) as "HPsx". iDestruct "HPsx" as %HPs_Some.
       wp_pures.
       rewrite -subst_map_insert.
-      assert (x âˆˆ xs) as Hin.
-      { by apply Hdom. }
-      pose proof (list_find_elem_of (eq x) xs x Hin eq_refl) as Hfind_Some.
-      destruct Hfind_Some as [[n z] Hfind_Some].
-      iApply switch_body_spec=> //=.
-      2: { by rewrite lookup_insert. }
-      { rewrite Hfind_Some. simpl. reflexivity. }
-      do 2 rewrite lookup_insert_ne=> //.
-      rewrite lookup_map_string_seq_Some.
+      assert (x âˆˆ xs) as Hin by naive_solver.
+      pose proof (list_find_elem_of (x =.) xs x) as [[n z] Hfind_Some]; [done..|].
+      iApply switch_body_spec.
+      { apply fmap_Some_2, Hfind_Some. }
+      { by rewrite lookup_insert. }
+      simplify_map_eq. rewrite lookup_map_string_seq_Some.
       assert (xs !! n = Some x) as Hxs_Some.
-      {
-        pose proof (@list_find_Some Z) as Hlist_find_Some.
-        specialize (Hlist_find_Some (eq x) _ xs n z).
-        destruct Hlist_find_Some as [Hlist_find_Some _].
-        specialize (Hlist_find_Some Hfind_Some).
-        destruct Hlist_find_Some as [Heq1 [-> _]]=> //.
-      }
-      assert (is_Some (ws !! n)) as Hws_Some.
-      {
-        apply lookup_lt_is_Some_2. rewrite -Heq.
-        apply lookup_lt_is_Some_1. by exists x.
-      }
-      destruct Hws_Some as [w Hws_Some].
-      iDestruct (big_sepL2_lookup _ xs ws n with "H") as "HA"=> //.
-      rewrite Hws_Some.
-      rewrite insert_commute=> //.
-      rewrite lookup_insert.
-      by iApply "HA".
+      { by apply list_find_Some in Hfind_Some as [? [-> _]]. }
+      assert (is_Some (ws !! n)) as [w Hws_Some].
+      { apply lookup_lt_is_Some_2. rewrite -Heq. eauto using lookup_lt_Some. }
+      iDestruct (big_sepL2_lookup _ xs ws n with "H") as "HA"; [done..|].
+      rewrite Hws_Some. by iApply "HA".
     Qed.
-
   End with_chan.
 End properties.
-- 
GitLab