From 3f39048dec610092e963c74c8995eee456cb0328 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 9 May 2017 13:39:06 +0200
Subject: [PATCH] Make ty_own simpl nomatch to avoid many matches in proof
 states.

---
 theories/typing/function.v                        | 3 ++-
 theories/typing/lib/rc/rc.v                       | 4 ++--
 theories/typing/lib/rc/weak.v                     | 4 ++--
 theories/typing/lib/rwlock/rwlockreadguard_code.v | 2 +-
 theories/typing/type.v                            | 2 +-
 theories/typing/type_sum.v                        | 8 ++++----
 6 files changed, 12 insertions(+), 11 deletions(-)

diff --git a/theories/typing/function.v b/theories/typing/function.v
index 55183c08..4071d4c6 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -76,7 +76,8 @@ Section fn.
     intros tid vl. unfold typed_body.
     do 12 f_equiv. f_contractive. do 16 ((eapply fp_E_proper; try reflexivity) || exact: Hfp || f_equiv).
     - rewrite !cctx_interp_singleton /=. do 5 f_equiv.
-      rewrite !tctx_interp_singleton /tctx_elt_interp /=. repeat (apply Hfp || f_equiv).
+      rewrite !tctx_interp_singleton /tctx_elt_interp /=.
+      do 5 f_equiv. apply type_dist2_dist. apply Hfp.
     - rewrite /tctx_interp !big_sepL_zip_with /=. do 4 f_equiv.
       cut (∀ n tid p i, Proper (dist n ==> dist n)
         (λ (l : list _), ∀ ty, ⌜l !! i = Some ty⌝ → tctx_elt_interp tid (p ◁ ty))%I).
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index 7e63812f..86f711a8 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -590,8 +590,8 @@ Section code.
     iApply (type_type _ _ _ [ x ◁ box (&shr{α} rc ty); #lr ◁ box (rc ty)]
         with "[] LFT HE Hna HL Hk [-]"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
-      unlock. iFrame "Hx". iFrame "Hr†". iExists [_].
-      rewrite heap_mapsto_vec_singleton /=. eauto 10 with iFrame. }
+      unlock. iFrame "Hx". iFrame "Hr†". iExists [# #l'].
+      rewrite heap_mapsto_vec_singleton /=. simpl. eauto 10 with iFrame. }
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
   Qed.
diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v
index 90b45aec..456d4a80 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -279,7 +279,7 @@ Section code.
     iApply (type_type _ _ _ [ x ◁ box (&shr{α} rc ty); #lr ◁ box (weak ty)]
         with "[] LFT HE Hna HL Hk [-]"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
-      unlock. iFrame "Hx". iFrame "Hr†". iExists [_].
+      unlock. iFrame "Hx". iFrame "Hr†". iExists [# #l'].
       rewrite heap_mapsto_vec_singleton /=. eauto 10 with iFrame. }
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
@@ -352,7 +352,7 @@ Section code.
     iApply (type_type _ _ _ [ x ◁ box (&shr{α} weak ty); #lr ◁ box (weak ty)]
         with "[] LFT HE Hna HL Hk [-]"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
-      unlock. iFrame. iExists [_]. rewrite heap_mapsto_vec_singleton /=.
+      unlock. iFrame. iExists [# #l']. rewrite heap_mapsto_vec_singleton /=.
       auto 10 with iFrame. }
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index a7b8630e..7267fbf5 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -137,7 +137,7 @@ Section rwlockreadguard_functions.
       iApply (type_type _ _ _ [ x ◁ box (uninit 1); #lx' ◁ rwlockreadguard α ty]
               with "[] LFT HE Hna HL Hk"); first last.
       { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val
-                tctx_hasty_val' //=. auto 10 with iFrame. }
+                tctx_hasty_val' //=; simpl. auto 10 with iFrame. }
       iApply type_jump; solve_typing.
   Qed.
 End rwlockreadguard_functions.
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 9b2a19ae..aa4fc414 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -51,7 +51,7 @@ Instance: Params (@ty_size) 2.
 Instance: Params (@ty_own) 2.
 Instance: Params (@ty_shr) 2.
 
-Arguments ty_own {_ _} _ _ !_ /.
+Arguments ty_own {_ _} _ _ !_ / : simpl nomatch.
 
 Class TyWf `{typeG Σ} (ty : type) := { ty_lfts : list lft; ty_wf_E : elctx }.
 Arguments ty_lfts {_ _} _ {_}.
diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v
index 33dbb662..dfa4a438 100644
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
@@ -31,15 +31,15 @@ Section case.
     edestruct @Forall2_lookup_l as (e & He & Hety); eauto.
     wp_read. iApply wp_case; [lia|by rewrite Nat2Z.id|]. iNext.
     destruct Hety as [Hety|Hety]; iApply (Hety with "LFT HE Hna HL HC");
-      rewrite !tctx_interp_cons !tctx_hasty_val' /= ?Hv //; iFrame "HT".
-    - iDestruct (ty.(ty_size_eq) with "Hown") as %<-.
+      rewrite !tctx_interp_cons !tctx_hasty_val' /= ?Hv //=; iFrame "HT".
+    - rewrite /own_ptr /=. iDestruct (ty.(ty_size_eq) with "Hown") as %<-.
       iSplitL "H↦i Hfi"; last iSplitR "H↦vl'' Hfvl''".
       + rewrite shift_loc_0. iFrame. iExists [ #i]. rewrite heap_mapsto_vec_singleton.
         iFrame. iExists [_], []. auto.
-      + iFrame. iExists _. iFrame.
+      + eauto with iFrame.
       + rewrite -EQlen app_length minus_plus -(shift_loc_assoc_nat _ 1).
         iFrame. iExists _. iFrame. rewrite uninit_own. auto.
-    - rewrite -EQlen app_length -(Nat.add_1_l (_+_)) -!freeable_sz_split. iFrame.
+    - rewrite /= -EQlen app_length -(Nat.add_1_l (_+_)) -!freeable_sz_split. iFrame.
       iExists (#i :: vl' ++ vl''). iNext. rewrite heap_mapsto_vec_cons heap_mapsto_vec_app.
       iFrame. iExists i, vl', vl''. rewrite /= -EQlen app_length nth_lookup EQty /=. auto.
   Qed.
-- 
GitLab