Update dependency

coq-lambda-rust.opam

@@ -15,7 +15,7 @@ This branch uses a proper weak memory model.
 """
 
 depends: [
-  "coq-gpfsl" { (= "dev.2021-05-05.0.6c5a80f0") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2021-05-07.0.f60c92f1") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]

theories/typing/product_split.v

@@ -26,7 +26,7 @@ Section product_split.
     { by rewrite IHtyl assoc_L. }
     apply tctx_elt_interp_hasty_path. clear Hp. simpl.
     clear. destruct (eval_path p); last done. destruct v; try done.
-    destruct l; try done. rewrite shift_loc_assoc Nat2Z.inj_add //.
+    destruct l; try done. rewrite shift_loc_assoc !Nat2Z.id //.
   Qed.
 
   Lemma tctx_split_ptr_prod E L ptr tyl :
@@ -97,7 +97,7 @@ Section product_split.
     iDestruct "EQ" as %->. iSplitL "H↦1 H†1 H1".
     + iExists _. iFrame "#∗". iExists _. by iFrame.
     + iExists _. iSplitR; first (by simpl; iDestruct "Hp" as %->).
-      iFrame. iExists _. by iFrame.
+      rewrite Nat2Z.id. iFrame. iExists _. by iFrame.
   Qed.
 
   Lemma tctx_merge_own_prod2 E L p n ty1 ty2 :
@@ -110,7 +110,7 @@ Section product_split.
     iDestruct "H1" as "(H↦1 & H†1)".
     iDestruct "H2" as (v2) "(Hp2 & H2)". simpl. iDestruct "Hp1" as %Hρ1.
     rewrite Hρ1. iDestruct "Hp2" as %[=<-]. iDestruct "H2" as "[H↦2 H†2]".
-    iExists #l. iSplitR; first done. rewrite /= -freeable_sz_split. iFrame.
+    iExists #l. iSplitR; first done. rewrite /= -freeable_sz_split Nat2Z.id. iFrame.
     iDestruct "H↦1" as (vl1) "[H↦1 H1]". iDestruct "H↦2" as (vl2) "[H↦2 H2]".
     iExists (vl1 ++ vl2). rewrite heap_mapsto_vec_app. iFrame.
     iDestruct (ty_size_eq with "H1") as "#>EQ". iDestruct "EQ" as %->.
@@ -145,7 +145,7 @@ Section product_split.
     rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
     iDestruct "H" as ([[]|]) "[Hp H]"; try done. iDestruct "Hp" as %Hp.
     rewrite /= split_prod_mt. iMod (bor_sep with "LFT H") as "[H1 H2]"; first solve_ndisj.
-    rewrite /tctx_elt_interp /=.
+    rewrite /tctx_elt_interp /= Nat2Z.id.
     iSplitL "H1"; iExists _; (iSplitR; first by rewrite Hp); auto.
   Qed.
 
@@ -158,7 +158,8 @@ Section product_split.
     iDestruct "H" as "[H1 H2]". iDestruct "H1" as ([[]|]) "[Hp1 H1]"; try done.
     iDestruct "Hp1" as %Hp1. iDestruct "H2" as (v2) "(Hp2 & H2)". rewrite /= Hp1.
     iDestruct "Hp2" as %[=<-]. iExists #l. iFrame "%".
-    iMod (bor_combine with "LFT H1 H2") as "H"; first solve_ndisj. by rewrite /= split_prod_mt.
+    iMod (bor_combine with "LFT H1 H2") as "H"; first solve_ndisj.
+    by rewrite Nat2Z.id /= split_prod_mt.
   Qed.
 
   Lemma uniq_is_ptr κ ty tid (vl : list val) :
@@ -194,7 +195,7 @@ Section product_split.
     rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
     iDestruct "H" as ([[]|]) "[Hp H]"; try iDestruct "H" as "[]".
     iDestruct "H" as "[H1 H2]". iDestruct "Hp" as %Hp.
-    by iSplitL "H1"; iExists _; (iSplitR; first by rewrite /= Hp).
+    iSplitL "H1"; iExists _; (iSplitR; [by rewrite /= Hp|by rewrite ?Nat2Z.id]).
   Qed.
 
   Lemma tctx_merge_shr_prod2 E L p κ ty1 ty2 :
@@ -205,7 +206,7 @@ Section product_split.
     rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
     iDestruct "H" as "[H1 H2]". iDestruct "H1" as ([[]|]) "[Hp1 Hown1]"; try done.
     iDestruct "Hp1" as %Hp1. iDestruct "H2" as ([[]|]) "[Hp2 Hown2]"; try done.
-    rewrite /= Hp1. iDestruct "Hp2" as %[=<-]. iExists #l. by iFrame.
+    rewrite /= Hp1 Nat2Z.id. iDestruct "Hp2" as %[=<-]. iExists #l. by iFrame.
   Qed.
 
   Lemma shr_is_ptr κ ty tid (vl : list val) :

theories/typing/type.v

@@ -441,7 +441,7 @@ Section type.
   Proof.
     revert l; induction n; intros l.
     - rewrite shift_loc_0. set_solver+.
-    - rewrite -Nat.add_1_l Nat2Z.inj_add /= IHn shift_loc_assoc.
+    - rewrite -Nat.add_1_l /= IHn shift_loc_assoc.
       set_solver+.
   Qed.
 
@@ -450,12 +450,12 @@ Section type.
   Proof.
     revert l; induction n; intros l.
     - simpl. set_solver+.
-    - rewrite -Nat.add_1_l Nat2Z.inj_add /=.
-      apply disjoint_union_l. split; last (rewrite -shift_loc_assoc; exact: IHn).
+    - rewrite -Nat.add_1_l -shift_loc_assoc /=.
+      apply disjoint_union_l. split; last exact : IHn.
       clear IHn. revert n; induction m; intros n; simpl; first set_solver+.
       rewrite shift_loc_assoc. apply disjoint_union_r. split.
       + apply ndot_ne_disjoint. destruct l. intros [=]. lia.
-      + rewrite -Z.add_assoc. move:(IHm (n + 1)%nat). rewrite Nat2Z.inj_add //.
+      + move:(IHm (n + 1)%nat). by rewrite -!shift_loc_assoc.
   Qed.
 
   Lemma shr_locsE_shrN l n :

theories/typing/type_context.v

@@ -26,7 +26,7 @@ Section type_context.
     match p with
     | BinOp OffsetOp e (Lit (LitInt n)) =>
       match eval_path e with
-      | Some (#(LitLoc l)) => Some (#(l +ₗ n))
+      | Some (#(LitLoc l)) => Some (#(l +ₗ Z.to_nat n))
       | _ => None
       end
     | e => to_val e

theories/typing/type_sum.v

@@ -38,7 +38,7 @@ Section case.
       + rewrite shift_loc_0. iFrame. iExists [ #i]. rewrite heap_mapsto_vec_singleton.
         iFrame. auto.
       + eauto with iFrame.
-      + rewrite -EQlen app_length minus_plus shift_loc_assoc_nat.
+      + rewrite -EQlen app_length minus_plus shift_loc_assoc Nat2Z.id.
         iFrame. iExists _. iFrame. auto.
     - 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.