From 497199d6b281271c9fb26781eddd8c25a17e36bb Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Fri, 16 Sep 2016 15:06:29 +0200
Subject: [PATCH] Simplify it further.
---
perm_incl.v | 40 ++++++++++++++++------------------------
1 file changed, 16 insertions(+), 24 deletions(-)
diff --git a/perm_incl.v b/perm_incl.v
index b6e1e1e2..41855a1d 100644
--- a/perm_incl.v
+++ b/perm_incl.v
@@ -149,39 +149,31 @@ Section props.
own (qtyoffs.1) (qtyoffs.2.1) ★ acc)
⊤ (combine ql (combine_offs tyl 0)).
Proof.
- intros Hlen Hq.
- assert (DEC : Decision (∃ (l : loc), v = Some #l)).
- { destruct v as [[[]|]|]; try by right; intros [l [=]]. left; eauto. }
- destruct DEC as [[l ->]|Hv]; last first.
- { destruct tyl as [|ty0 tyl], ql as [|q0 ql]; try done.
- { destruct q as [q ?]. simpl in *. by subst. }
- destruct v as [[[|l|]|]|];
- try by split; iIntros (tid) "H";
- [iDestruct "H" as (l) "[% _]" || iDestruct "H" as "[]" |
- iDestruct "H" as "[[]_]"].
- naive_solver. }
- destruct (@exists_last _ ql) as (ql'&q0&->).
+ intros Hlen Hq. assert (ql ≠ []).
{ destruct ql as [|q0 ql]; last done. destruct q. simpl in *. by subst. }
+ destruct v as [[[|l|]|]|];
+ try by (destruct tyl as [|ty0 tyl], ql as [|q0 ql]; try done;
+ by split; iIntros (tid) "H";
+ [iDestruct "H" as (l) "[% _]" || iDestruct "H" as "[]" |
+ iDestruct "H" as "[[]_]"]).
+ destruct (@exists_last _ ql) as (ql'&q0&->). done.
+ apply uPred_equiv_perm_equiv=>tid.
assert (foldr Qp_plus (q0/2) (ql' ++ [q0/2]) = q)%Qp as <-.
- { destruct q as [q Hqpos]. apply Qp_eq. simpl in *. subst. clear. induction ql'.
- - by rewrite /fold_right /app Qp_div_2 Qcplus_0_r.
- - by rewrite /= IHql'. }
- revert Hlen. assert (length (ql' ++ [q0]) = length (ql' ++ [q0/2]%Qp)) as ->.
- { rewrite !app_length /=. lia. }
- intros Hlen. apply uPred_equiv_perm_equiv=>tid.
- rewrite /has_type /from_option split_own_prod //.
+ { destruct q as [q ?]. apply Qp_eq. simpl in *. subst. clear. induction ql'.
+ by rewrite /fold_right /app Qp_div_2 Qcplus_0_r. by rewrite /= IHql'. }
+ rewrite /has_type /from_option split_own_prod ?Hlen ?app_length //.
clear -Hlen. revert ql' Hlen. generalize 0%nat at -2.
- induction tyl as [|ty tyl IH]; destruct ql' as [|q ql']=>Hlen; try done.
+ induction tyl as [|ty tyl IH]; destruct ql' as [|q ql']; intros [= Hlen]; try done.
- destruct tyl; last done. clear IH Hlen.
rewrite big_sepL_singleton /= /sep !right_id comm uPred.sep_exist_r.
apply uPred.exist_proper=>l0.
rewrite -{3}(Qp_div_2 q0) -{3}(right_id O plus ty.(ty_size))
-heap_freeable_op_eq uPred.later_sep -!assoc.
- iSplit; iIntros "[#Eq [? [? ?]]]"; iFrame "# ★";
+ iSplit; iIntros "[#Eq[?[??]]]"; iFrame "# ★";
iDestruct "Eq" as %[=]; subst; rewrite shift_loc_assoc_nat //.
- - simpl in *. rewrite big_sepL_cons /sep -IH; last by congruence. clear IH.
- rewrite !uPred.sep_exist_r !uPred.sep_exist_l. apply uPred.exist_proper=>l0.
- rewrite -!assoc /=. by iSplit; iIntros "[$[$[$[$$]]]]".
+ - rewrite /= big_sepL_cons /sep -IH // !uPred.sep_exist_r uPred.sep_exist_l.
+ apply uPred.exist_proper=>l0. rewrite -!assoc /=.
+ by iSplit; iIntros "[$[$[$[$$]]]]".
Qed.
End props.
--
GitLab