From 7c432dd72808d4f62e83c397973e901d53b26de2 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jjourdan@mpi-sws.org>
Date: Tue, 10 Jan 2017 22:40:11 +0100
Subject: [PATCH] More uses of [iDestruct ty_size_eq].

---
 theories/typing/product.v     | 8 +++-----
 theories/typing/programs.v    | 6 ++----
 theories/typing/type.v        | 1 -
 theories/typing/unsafe/cell.v | 6 ++----
 4 files changed, 7 insertions(+), 14 deletions(-)

diff --git a/theories/typing/product.v b/theories/typing/product.v
index f28f1f02..c4f827ea 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -119,12 +119,10 @@ Section product.
     - iNext. iSplitL "H↦1 H1". iExists vl1. by iFrame. iExists vl2. by iFrame.
     - iIntros "Htl [H1 H2]". iDestruct ("Htlclose" with "Htl") as "Htl".
       iDestruct "H1" as (vl1') "[H↦1 H1]". iDestruct "H2" as (vl2') "[H↦2 H2]".
-      iAssert (▷ ⌜length vl1' = ty1.(ty_size)⌝)%I with "[#]" as ">%".
-      { iNext. by iApply ty_size_eq. }
-      iAssert (▷ ⌜length vl2' = ty2.(ty_size)⌝)%I with "[#]" as ">%".
-      { iNext. by iApply ty_size_eq. }
+      iDestruct (ty_size_eq with "H1") as "#>%".
+      iDestruct (ty_size_eq with "H2") as "#>%".
       iCombine "H↦1" "H↦1f" as "H↦1". iCombine "H↦2" "H↦2f" as "H↦2".
-      rewrite !heap_mapsto_vec_op; try by congruence.
+      rewrite !heap_mapsto_vec_op; [|congruence..].
       iDestruct "H↦1" as "[_ H↦1]". iDestruct "H↦2" as "[_ H↦2]".
       iMod ("Hclose2" with "Htl [H2 H↦2]") as "[Htl $]". by iExists _; iFrame.
       iMod ("Hclose1" with "Htl [H1 H↦1]") as "[$$]". by iExists _; iFrame. done.
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index 291993fa..05fff696 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -185,8 +185,7 @@ Section typing_rules.
     wp_bind p1. iApply (wp_hasty with "Hp1"). iIntros (v1) "% Hown1".
     wp_bind p2. iApply (wp_hasty with "Hp2"). iIntros (v2) "_ Hown2".
     iMod (Hwrt with "* [] LFT HE HL Hown1") as (l vl) "([% %] & Hl & Hclose)"; first done.
-    subst v1. iAssert (⌜1%nat = ty_size ty⌝%I) with "[#]" as %Hsz.
-    { change (1%nat) with (length [v2]). by iApply ty_size_eq. }
+    subst v1. iDestruct (ty_size_eq with "Hown2") as "#Hsz". iDestruct "Hsz" as %Hsz.
     rewrite <-Hsz in *. destruct vl as [|v[|]]; try done.
     rewrite heap_mapsto_vec_singleton. wp_write.
     rewrite -heap_mapsto_vec_singleton.
@@ -212,8 +211,7 @@ Section typing_rules.
     iIntros (v) "% Hown".
     iMod (Hread with "* [] LFT Htl HE HL Hown") as
         (l vl q) "(% & Hl & Hown & Hclose)"; first done.
-    subst v. iAssert (▷⌜length vl = 1%nat⌝)%I with "[#]" as ">%".
-    { rewrite -Hsz. iApply ty_size_eq. done. }
+    subst v. iDestruct (ty_size_eq with "Hown") as "#>%". rewrite ->Hsz in *.
     destruct vl as [|v [|]]; try done.
     rewrite heap_mapsto_vec_singleton. wp_read.
     iMod ("Hclose" with "Hl") as "($ & $ & Hown2)".
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 12da7169..bf270f5b 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -444,7 +444,6 @@ Section weakening.
     - iDestruct "HL" as %HL. iPureIntro. intros ??. apply HL.
       rewrite HL12. set_solver.
   Qed.
-
 End weakening.
 
 Hint Resolve subtype_refl eqtype_refl : lrust_typing.
diff --git a/theories/typing/unsafe/cell.v b/theories/typing/unsafe/cell.v
index b6b1df8f..62195526 100644
--- a/theories/typing/unsafe/cell.v
+++ b/theories/typing/unsafe/cell.v
@@ -34,9 +34,8 @@ Section cell.
     { iMod (na_bor_acc with "LFT Hshr Htok Htl") as "(Hown & Htl & Hclose)"; [solve_ndisj..|].
       iDestruct "Hown" as (vl) "[H↦ #Hown]".
       simpl. assert (F ∖ ∅ = F) as -> by set_solver+.
-      iAssert (▷ ⌜length vl = ty_size ty⌝)%I with "[#]" as ">EQ".
-      { iNext. by iApply ty_size_eq. }
-      rewrite Hsz. iDestruct "EQ" as %EQ. iMod ("Hclose" with "[H↦] Htl") as "[$ $]".
+      iDestruct (ty_size_eq with "Hown") as "#>%". rewrite ->Hsz in *.
+      iMod ("Hclose" with "[H↦] Htl") as "[$ $]".
       { iExists vl. by iFrame. }
       iModIntro. iSplitL "".
       { iNext. iExists vl. destruct vl; last done. iFrame "Hown".
@@ -52,7 +51,6 @@ Section cell.
   Global Instance cell_send :
     Send ty → Send (cell ty).
   Proof. intros. split. simpl. apply send_change_tid. Qed.
-
 End cell.
 
 Section typing.
-- 
GitLab