Commit 36ca289a authored by Ralf Jung's avatar Ralf Jung
Browse files

avoid some deprecated functions

parent e051894d
......@@ -236,9 +236,9 @@ Section heap.
iDestruct "Hown1" as "[Hown1 _]". iDestruct "Hown2" as "[Hown2 _]".
iCombine "Hown1" "Hown2" as "Hown". rewrite heap_mapsto_vec_op; last first.
{ rewrite !firstn_length. subst ll.
rewrite -!min_assoc min_idempotent min_comm -min_assoc min_idempotent min_comm. done. }
rewrite -!Nat.min_assoc Nat.min_idempotent Nat.min_comm -Nat.min_assoc Nat.min_idempotent Nat.min_comm. done. }
iDestruct "Hown" as "[H Hown]". iDestruct "H" as %Hl. iExists (take ll vl1). iFrame.
destruct (min_spec (length vl1) (length vl2)) as [[Hne Heq]|[Hne Heq]].
destruct (Nat.min_spec (length vl1) (length vl2)) as [[Hne Heq]|[Hne Heq]].
+ iClear "HP2". rewrite take_ge; last first.
{ rewrite -Heq /ll. done. }
rewrite drop_ge; first by rewrite app_nil_r. by rewrite -Heq.
......
......@@ -773,13 +773,13 @@ Section arc.
iApply wp_mask_mono; last iApply (wp_step_fupd with "H†"); [solve_ndisj..|].
iDestruct "Hown" as (???) "(_ & Hlen & _)". wp_write. iIntros "(#Hν & Hown & H†)!>".
wp_seq. wp_op. wp_op. iDestruct "Hown" as (?) "[H↦ Hown]".
iDestruct (ty_size_eq with "Hown") as %?. rewrite Max.max_0_r.
iDestruct (ty_size_eq with "Hown") as %?. rewrite Nat.max_0_r.
iDestruct "Hlen" as %[= ?]. wp_apply (wp_memcpy with "[$H↦1 $H↦]"); [congruence..|].
iIntros "[? Hrc']". wp_seq. iMod ("Hdrop" with "[Hrc' H†]") as "Htok".
{ unfold P2. auto with iFrame. }
wp_apply (drop_weak_spec with "[//] Htok"). unlock. iIntros ([]); last first.
{ iIntros "_". wp_if. unlock. iFrame. iExists (_::_). rewrite heap_mapsto_vec_cons.
iFrame. iExists 1%nat, _, []. rewrite /= right_id_L Max.max_0_r.
iFrame. iExists 1%nat, _, []. rewrite /= right_id_L Nat.max_0_r.
auto 10 with iFrame. }
iIntros "([H† H1] & H2 & H3)". iDestruct "H1" as (vl1) "[H1 Heq]".
iDestruct "Heq" as %<-. wp_if.
......
......@@ -111,7 +111,7 @@ Section product.
iMod (@copy_shr_acc with "LFT H1 Htl Htok1") as (q1) "(Htl & H1 & Hclose1)"; first solve_ndisj.
{ rewrite <-HF. apply shr_locsE_subseteq. simpl. clear. lia. }
iMod (@copy_shr_acc with "LFT H2 Htl Htok2") as (q2) "(Htl & H2 & Hclose2)"; first solve_ndisj.
{ move: HF. rewrite /= -plus_assoc shr_locsE_shift.
{ move: HF. rewrite /= -Nat.add_assoc shr_locsE_shift.
assert (shr_locsE l (ty_size ty1) ## shr_locsE (l + (ty_size ty1)) (ty_size ty2 + 1))
by exact: shr_locsE_disj.
set_solver. }
......
......@@ -75,7 +75,7 @@ Section product_split.
by iApply "Heq". }
iMod ("IH" with "[] HL [Htyl]") as "(HL & Htyl)"; first done.
{ change (ty_size ty) with (0+ty_size ty)%nat at 1.
rewrite plus_comm -hasty_ptr_offsets_offset //. }
rewrite Nat.add_comm -hasty_ptr_offsets_offset //. }
iClear "IH". iMod (Hmerge with "LFT HE HL [Hty Htyl]") as "($ & ?)";
last by rewrite tctx_interp_singleton.
rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton. iFrame.
......
......@@ -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 Nat.add_comm Nat.add_sub shift_loc_assoc_nat.
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.
......
......@@ -84,7 +84,7 @@ Section uninit.
subtype E L (uninit n) (Π(ty :: tyl)).
Proof.
intros ?%Nat2Z.inj_le. rewrite -!uninit_uninit0_eqtype /uninit0=>Hty Htyl.
rewrite (le_plus_minus ty.(ty_size) n) // replicate_add
rewrite -(Nat.sub_add ty.(ty_size) n) // Nat.add_comm // replicate_add
-(prod_flatten_r _ _ [_]) /= -prod_app. repeat (done || f_equiv).
Qed.
Lemma uninit_product_subtype_cons_l {E L} (n : nat) ty tyl :
......@@ -94,7 +94,7 @@ Section uninit.
subtype E L (Π(ty :: tyl)) (uninit n).
Proof.
intros ?%Nat2Z.inj_le. rewrite -!uninit_uninit0_eqtype /uninit0=>Hty Htyl.
rewrite (le_plus_minus ty.(ty_size) n) // replicate_add
rewrite -(Nat.sub_add ty.(ty_size) n) // Nat.add_comm replicate_add
-(prod_flatten_r _ _ [_]) /= -prod_app. repeat (done || f_equiv).
Qed.
Lemma uninit_product_eqtype_cons_r {E L} (n : nat) ty tyl :
......
Supports Markdown
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