From 25c44d0cab46863331fe64e3ebb523b18b984e68 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Thu, 15 Sep 2016 01:31:31 +0200
Subject: [PATCH] Simplifications
---
perm_incl.v | 5 +++--
type.v | 11 +----------
2 files changed, 4 insertions(+), 12 deletions(-)
diff --git a/perm_incl.v b/perm_incl.v
index c0ae9022..f28a5847 100644
--- a/perm_incl.v
+++ b/perm_incl.v
@@ -107,7 +107,8 @@ Section props.
iAssert (∃ q, [κ]{q})%I as "Htok". admit.
iDestruct "Htok" as (q) "Htok".
iVs (ty.(ty_share) _ lrustN with "Hown Htok") as "[Hown _]".
- admit. set_solver. iVsIntro. iExists _. iSplit. done. done.
+ apply disjoint_union_l; solve_ndisj. set_solver. iVsIntro.
+ iExists _. iSplit. done. done.
Admitted.
Lemma perm_split_own_prod tyl (q : Qp) (ql : list Qp) v :
@@ -144,7 +145,7 @@ Section props.
pose (q' := mk_Qp _ Hq').
assert (q = q0 + q')%Qp as -> by rewrite Qp_eq -Hq //. clear Hq.
injection Hlen. clear Hlen. intro Hlen.
- simpl in IH|-*. rewrite -(IH q') //. split; iIntros (tid) "H".
+ simpl in IH|-*. rewrite -(IH q') //. clear IH. split; iIntros (tid) "H".
+ iDestruct "H" as (l') "(Hl'&Hf&H)". iDestruct "Hl'" as %[= Hl']. subst.
iDestruct "H" as (vl) "[Hvl H]".
iDestruct "H" as ([|vl0[|vl1 vll]]) "(>%&>%&Hown)"; try done. subst.
diff --git a/type.v b/type.v
index af88dfbd..6bd03ec7 100644
--- a/type.v
+++ b/type.v
@@ -101,17 +101,8 @@ Section types.
Context `{heapG Σ, lifetimeG Σ, thread_localG Σ}.
Program Definition bot :=
- {| ty_size := 0; ty_dup := true;
- ty_own tid vl := False%I; ty_shr κ tid N l := False%I |}.
+ ty_of_st {| st_size := 0; st_own tid vl := False%I |}.
Next Obligation. iIntros (tid vl) "[]". Qed.
- Next Obligation.
- iIntros (????????) "Hb Htok".
- iVs (lft_borrow_exists with "Hb Htok") as (vl) "[Hb Htok]". set_solver.
- iVs (lft_borrow_split with "Hb") as "[_ Hb]". set_solver.
- iVs (lft_borrow_persistent with "Hb Htok") as "[>[] _]". set_solver.
- Qed.
- Next Obligation. iIntros (?????) "_ []". Qed.
- Next Obligation. intros. iIntros "[]". Qed.
Program Definition unit :=
ty_of_st {| st_size := 0; st_own tid vl := (vl = [])%I |}.
--
GitLab