From 7745dcad8994b3165438d50bfb3ec027cb2f8c21 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Thu, 15 Sep 2016 00:54:22 +0200
Subject: [PATCH] Proof of [perm_split_own_prod].
---
perm.v | 4 +--
perm_incl.v | 74 ++++++++++++++++++++++++++++++++++++++++++++++++++++-
type.v | 10 ++++----
3 files changed, 80 insertions(+), 8 deletions(-)
diff --git a/perm.v b/perm.v
index 5880427f..da600e7f 100644
--- a/perm.v
+++ b/perm.v
@@ -7,8 +7,8 @@ Bind Scope perm_scope with perm.
(* TODO : find a better place for this. *)
Definition valuable := option val.
-Definition proj_valuable (n : Z) :=
- (≫= λ v, match v with LitV (LitLoc l) => Some (shift_loc l n) | _ => None end).
+Definition proj_valuable (n : Z) : valuable → valuable :=
+ (≫= λ v, match v with LitV (LitLoc l) => Some (#(shift_loc l n)) | _ => None end).
Module Perm.
diff --git a/perm_incl.v b/perm_incl.v
index d46618ba..c0ae9022 100644
--- a/perm_incl.v
+++ b/perm_incl.v
@@ -1,8 +1,9 @@
+From Coq Require Import Qcanon.
From iris.algebra Require Import upred_big_op.
From iris.program_logic Require Import thread_local.
From lrust Require Export type perm.
-Import Perm.
+Import Perm Types.
Section defs.
@@ -48,6 +49,14 @@ Section props.
Proper ((⇔) ==> (⇔) ==> iff) (⇒).
Proof. intros ??[??]??[??]; split; intros ?; by simplify_order. Qed.
+ Global Instance perm_sep_proper :
+ Proper ((⇔) ==> (⇔) ==> (⇔)) (sep).
+ Proof.
+ intros ??[A B]??[C D]; split; iIntros (tid) "[A B]".
+ iVs (A with "A") as "$". iApply (C with "B").
+ iVs (B with "A") as "$". iApply (D with "B").
+ Qed.
+
Lemma perm_incl_top ρ : ρ ⇒ ⊤.
Proof. iIntros (tid) "H". eauto. Qed.
@@ -101,4 +110,67 @@ Section props.
admit. set_solver. iVsIntro. iExists _. iSplit. done. done.
Admitted.
+ Lemma perm_split_own_prod tyl (q : Qp) (ql : list Qp) v :
+ length tyl = length ql →
+ foldr (λ (q : Qp) acc, q + acc)%Qc 0%Qc ql = q →
+ v ◁ own q (product tyl) ⇔
+ foldr (λ qtysz acc,
+ proj_valuable (Z.of_nat (qtysz.2.2)) v ◁
+ own (qtysz.1) (qtysz.2.1) ★ acc)
+ ⊤ (combine ql (combine_offs tyl 0)).
+ Proof.
+ destruct tyl as [|ty0 tyl], ql as [|q0 ql]; try done.
+ { simpl. intros _?. 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 "[[]_]"].
+ intros [= EQ]. revert EQ.
+ rewrite -{1}(shift_loc_0 l). change 0 with (Z.of_nat 0). generalize O at 2 3.
+ revert q ty0 q0 ql. induction tyl as [|ty1 tyl IH]=>q ty0 q0 ql offs Hlen Hq;
+ destruct ql as [|q1 ql]; try done.
+ - simpl in Hq. rewrite ->Qcplus_0_r, <-Qp_eq in Hq. subst q.
+ rewrite /= right_id. split; iIntros (tid) "H!==>/="; rewrite Nat.add_0_r.
+ + iDestruct "H" as (l') "(%&?&H)". iExists l'. iSplit. done. iFrame. iNext.
+ iDestruct "H" as (vl) "[Hvl H]".
+ iDestruct "H" as ([|?[|??]]) "(%&%&?)"; try done.
+ iExists _. subst. rewrite /= app_nil_r big_sepL_singleton. by iFrame.
+ + iDestruct "H" as (l') "(%&?&Hown)". iExists l'. iSplit. done. iFrame. iNext.
+ iDestruct "Hown" as (vl) "[Hmt Hown]". iExists vl. iFrame.
+ iExists [vl]. rewrite /= app_nil_r big_sepL_singleton. iFrame. by iSplit.
+ - assert (Hq' : (0 < q1 + foldr (λ (q : Qp) acc, q + acc) 0 ql)%Qc).
+ { apply Qcplus_pos_nonneg. done. clear. induction ql. done.
+ apply Qcplus_nonneg_nonneg; last done. by apply Qclt_le_weak. }
+ 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".
+ + 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.
+ rewrite big_sepL_cons heap_mapsto_vec_app -heap_freeable_op_eq.
+ iDestruct "Hf" as "[Hf0 Hfq]". iDestruct "Hvl" as "[Hvl0 Hvll]".
+ iDestruct "Hown" as "[Hown0 Hown]".
+ iAssert (▷ (length vl0 = ty_size ty0))%I with "[#]" as "#>Hlenvl0".
+ { iNext. iApply (ty_size_eq with "Hown0"). }
+ iDestruct "Hlenvl0" as %Hlenvl0. iVsIntro. iSplitL "Hf0 Hvl0 Hown0".
+ * iExists _. iSplit. done. iFrame. iNext. iExists vl0. by iFrame.
+ * iExists _. iSplit. done. rewrite !shift_loc_assoc -!Nat2Z.inj_add Hlenvl0.
+ iFrame. iNext. iExists (concat (vl1 :: vll)). iFrame. iExists (_ :: _).
+ iSplit. done. iFrame. iPureIntro. simpl in *. congruence.
+ + iDestruct "H" as "[H0 H]".
+ iDestruct "H0" as (vl0) "(Heq&Hf0&Hmt0)". iDestruct "Heq" as %[= ?]. subst vl0.
+ iDestruct "H" as (vl) "(Heq&Hf&Hmt)". iDestruct "Heq" as %[= ?]. subst vl.
+ iVsIntro. iExists (shift_loc l offs). iSplit. done. iNext.
+ iSplitL "Hf Hf0".
+ * rewrite -heap_freeable_op_eq shift_loc_assoc Nat2Z.inj_add. by iFrame.
+ * iDestruct "Hmt0" as (vl0) "[Hmt0 Hown0]". iDestruct "Hmt" as (vl) "[Hmt Hown]".
+ iDestruct (ty_size_eq with "Hown0") as %<-.
+ iExists (vl0 ++ vl). iSplitL "Hmt Hmt0".
+ { rewrite heap_mapsto_vec_app shift_loc_assoc Nat2Z.inj_add. by iFrame. }
+ iDestruct "Hown" as (vll) "(%&%&Hown)". subst.
+ iExists (_ :: _). iSplit. done. iSplit. iPureIntro; simpl in *; congruence.
+ rewrite big_sepL_cons. by iFrame.
+ Qed.
+
End props.
diff --git a/type.v b/type.v
index bbdad947..af88dfbd 100644
--- a/type.v
+++ b/type.v
@@ -255,10 +255,10 @@ Section types.
iIntros (κ ty tid vl) "H". iDestruct "H" as (l) "[% _]". by subst.
Qed.
- Fixpoint combine_accu_size (tyl : list type) (accu : nat) :=
+ Fixpoint combine_offs (tyl : list type) (accu : nat) :=
match tyl with
| [] => []
- | ty :: q => (ty, accu) :: combine_accu_size q (accu + ty.(ty_size))
+ | ty :: q => (ty, accu) :: combine_offs q (accu + ty.(ty_size))
end.
Lemma list_ty_type_eq tid (tyl : list type) (vll : list (list val)) :
@@ -277,7 +277,7 @@ Section types.
(l ↦★{q}: λ vl,
∃ vll, vl = concat vll ★ length tyl = length vll
★ [★ list] tyvl ∈ combine tyl vll, ty_own (tyvl.1) tid (tyvl.2))%I
- ⊣⊢ [★ list] tyoffs ∈ combine_accu_size tyl 0,
+ ⊣⊢ [★ list] tyoffs ∈ combine_offs tyl 0,
shift_loc l (tyoffs.2) ↦★{q}: ty_own (tyoffs.1) tid.
Proof.
rewrite -{1}(shift_loc_0 l). change 0%Z with (Z.of_nat 0).
@@ -331,7 +331,7 @@ Section types.
(∃ vll, vl = concat vll ★ length tyl = length vll ★
[★ list] tyvl ∈ combine tyl vll, tyvl.1.(ty_own) tid (tyvl.2))%I;
ty_shr κ tid N l :=
- ([★ list] i ↦ tyoffs ∈ combine_accu_size tyl 0,
+ ([★ list] i ↦ tyoffs ∈ combine_offs tyl 0,
tyoffs.1.(ty_shr) κ tid (N .@ i) (shift_loc l (tyoffs.2)))%I
|}.
Next Obligation.
@@ -350,7 +350,7 @@ Section types.
Next Obligation.
intros tyl E N κ l tid q ??. rewrite split_prod_mt.
change (ndot (A:=nat)) with (λ N i, N .@ (0+i)%nat). generalize O at 3.
- induction (combine_accu_size tyl 0) as [|[ty offs] ll IH].
+ induction (combine_offs tyl 0) as [|[ty offs] ll IH].
- iIntros (?) "_$!==>". by rewrite big_sepL_nil.
- iIntros (i) "Hown Htoks". rewrite big_sepL_cons.
iVs (lft_borrow_split with "Hown") as "[Hownh Hownq]". set_solver.
--
GitLab