Cleanned up perm_incl.v. Proved new ways of proving such permission inclusions.

perm_incl.v

@@ -2,43 +2,106 @@ From iris.algebra Require Import upred_big_op.
 From iris.program_logic Require Import thread_local.
 From lrust Require Export type perm.
 
-Section perm_incl.
+Import Perm.
+
+Section defs.
 
   Context `{heapG Σ, lifetimeG Σ, thread_localG Σ}.
 
+  (* Definitions *)
   Definition perm_incl (ρ1 ρ2 : perm) :=
     ∀ tid, ρ1 tid ={⊤}=> ρ2 tid.
 
-  Lemma perm_incl_top ρ : perm_incl ρ ⊤.
-  Proof. iIntros (tid) "H". eauto. Qed.
+  Global Instance perm_equiv : Equiv perm :=
+    λ ρ1 ρ2, perm_incl ρ1 ρ2 ∧ perm_incl ρ2 ρ1.
+
+  Class Duplicable (ρ : @perm Σ) :=
+    perm_incl_duplicable : perm_incl ρ (ρ ★ ρ).
+
+End defs.
+
+Infix "⇒" := perm_incl (at level 95, no associativity) : C_scope.
+Notation "(⇒)" := perm_incl (only parsing) : C_scope.
 
-  Global Instance perm_incl_refl : Reflexive perm_incl.
-  Proof. iIntros (? tid) "H". eauto. Qed.
+Notation "ρ1 ⇔ ρ2" := (equiv (A:=perm) ρ1%P ρ2%P)
+   (at level 95, no associativity) : C_scope.
+Notation "(⇔)" := (equiv (A:=perm)) (only parsing) : C_scope.
+
+Section props.
+
+  Context `{heapG Σ, lifetimeG Σ, thread_localG Σ}.
+
+  (* Properties *)
+  Global Instance perm_incl_preorder : PreOrder (⇒).
+  Proof.
+    split.
+    - iIntros (? tid) "H". eauto.
+    - iIntros (??? H12 H23 tid) "H". iVs (H12 with "H") as "H". by iApply H23.
+  Qed.
 
-  Global Instance perm_incl_trans : Transitive perm_incl.
+  Global Instance perm_equiv_equiv : Equivalence (⇔).
   Proof.
-    iIntros (??? H12 H23 tid) "H". iVs (H12 with "H") as "H". by iApply H23.
+    split.
+    - by split.
+    - by intros x y []; split.
+    - intros x y z [] []. split; by transitivity y.
   Qed.
 
-  Lemma perm_incl_frame_l ρ ρ1 ρ2 :
-    perm_incl ρ1 ρ2 → perm_incl (ρ ★ ρ1) (ρ ★ ρ2).
+  Global Instance perm_incl_proper :
+    Proper ((⇔) ==> (⇔) ==> iff) (⇒).
+  Proof. intros ??[??]??[??]; split; intros ?; by simplify_order. Qed.
+
+  Lemma perm_incl_top ρ : ρ ⇒ ⊤.
+  Proof. iIntros (tid) "H". eauto. Qed.
+
+  Lemma perm_incl_frame_l ρ ρ1 ρ2 : ρ1 ⇒ ρ2 → ρ ★ ρ1 ⇒ ρ ★ ρ2.
   Proof. iIntros (Hρ tid) "[$?]". by iApply Hρ. Qed.
 
   Lemma perm_incl_frame_r ρ ρ1 ρ2 :
-    perm_incl ρ1 ρ2 → perm_incl (ρ1 ★ ρ) (ρ2 ★ ρ).
+    ρ1 ⇒ ρ2 → ρ1 ★ ρ ⇒ ρ2 ★ ρ.
   Proof. iIntros (Hρ tid) "[?$]". by iApply Hρ. Qed.
 
-End perm_incl.
+  Lemma perm_incl_exists_intro {A} P x : P x ⇒ ∃ x : A, P x.
+  Proof. iIntros (tid) "H!==>". by iExists x. Qed.
 
-Section duplicable.
+  Global Instance perm_sep_assoc : Assoc (⇔) sep.
+  Proof. intros ???; split. by iIntros (tid) "[$[$$]]". by iIntros (tid) "[[$$]$]". Qed.
 
-  Context `{heapG Σ, lifetimeG Σ, thread_localG Σ}.
+  Global Instance perm_sep_comm : Comm (⇔) sep.
+  Proof. intros ??; split; by iIntros (tid) "[$$]". Qed.
 
-  Class Duplicable (ρ : perm) :=
-    perm_incl_duplicable : perm_incl ρ (ρ ★ ρ).
+  Global Instance perm_top_right_id : RightId (⇔) ⊤ sep.
+  Proof. intros ρ; split. by iIntros (tid) "[? _]". by iIntros (tid) "$". Qed.
+
+  Global Instance perm_top_left_id : LeftId (⇔) ⊤ sep.
+  Proof. intros ρ. by rewrite comm right_id. Qed.
+
+  Lemma perm_tok_plus κ q1 q2 :
+    tok κ q1 ★ tok κ q2 ⇔ tok κ (q1 + q2).
+  Proof.
+    rewrite /tok /sep /=; split; intros tid; rewrite -lft_own_op;
+      iIntros "[[$$]H]!==>". by iDestruct "H" as "[$?]". by auto.
+  Qed.
+
+  Lemma perm_lftincl_refl κ : ⊤ ⇒ κ ⊑ κ.
+  Proof. iIntros (tid) "_!==>". iApply lft_incl_refl. Qed.
+
+  Lemma perm_lftincl_trans κ1 κ2 κ3 : κ1 ⊑ κ2 ★ κ2 ⊑ κ3 ⇒ κ1 ⊑ κ3.
+  Proof. iIntros (tid) "[#?#?]!==>". iApply lft_incl_trans. auto. Qed.
+
+  Lemma perm_incl_share v κ ty :
+    v ◁ &uniq{κ} ty ⇒ v ◁ &shr{κ} ty.
+  Proof.
+    iIntros (tid) "Huniq". iDestruct "Huniq" as (l) "[% Hown]".
+    (* FIXME : we nee some tokens here. *)
+    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.
+  Admitted.
 
   Lemma has_type_dup v ty : ty.(ty_dup) → Duplicable (v ◁ ty).
-  Proof. iIntros (Hdup tid) "H!==>". by iApply ty_dup_dup. Qed.
+  Proof. iIntros (Hdup tid) "H". by iApply ty_dup_dup. Qed.
 
   Global Instance lft_incl_dup κ κ' : Duplicable (κ ⊑ κ').
   Proof. iIntros (tid) "#H!==>". by iSplit. Qed.
@@ -53,39 +116,6 @@ Section duplicable.
   Global Instance top_dup : Duplicable ⊤.
   Proof. iIntros (tid) "_!==>". by iSplit. Qed.
 
-End duplicable.
+End props.
 
 Hint Extern 0 (Duplicable (_ ◁ _)) => apply has_type_dup; exact I.
-
-Section perm_equiv.
-
-  Context `{heapG Σ, lifetimeG Σ, thread_localG Σ}.
-
-  Definition perm_equiv ρ1 ρ2 := perm_incl ρ1 ρ2 ∧ perm_incl ρ2 ρ1.
-
-  Global Instance perm_equiv_refl : Reflexive perm_equiv.
-  Proof. by split. Qed.
-
-  Global Instance perm_equiv_trans : Transitive perm_equiv.
-  Proof. intros x y z [] []. split; by transitivity y. Qed.
-
-  Global Instance perm_equiv_sym : Symmetric perm_equiv.
-  Proof. by intros x y []; split. Qed.
-
-  Global Instance perm_incl_proper :
-    Proper (perm_equiv ==> perm_equiv ==> iff) perm_incl.
-  Proof. intros ??[??]??[??]; split; eauto using perm_incl_trans. Qed.
-
-  Global Instance sep_assoc : Assoc perm_equiv Perm.sep.
-  Proof. intros ???; split. by iIntros (tid) "[$[$$]]". by iIntros (tid) "[[$$]$]". Qed.
-
-  Global Instance sep_comm : Comm perm_equiv Perm.sep.
-  Proof. intros ??; split; by iIntros (tid) "[$$]". Qed.
-
-  Global Instance top_right_id : RightId perm_equiv ⊤ Perm.sep.
-  Proof. intros ρ; split. by iIntros (tid) "[? _]". by iIntros (tid) "$". Qed.
-
-  Global Instance top_left_id : LeftId perm_equiv ⊤ Perm.sep.
-  Proof. intros ρ. by rewrite comm right_id. Qed.
-
-End perm_equiv.
\ No newline at end of file

type.v

@@ -22,7 +22,8 @@ Section defs.
       ty_shr_persistent κ tid N l : PersistentP (ty_shr κ tid N l);
 
       ty_size_eq tid vl : ty_own tid vl ⊢ length vl = ty_size;
-      ty_dup_dup tid vl : ty_dup → ty_own tid vl ⊢ ty_own tid vl ★ ty_own tid vl;
+      ty_dup_dup tid vl E :
+        ty_dup → ty_own tid vl ={E}=> ty_own tid vl ★ ty_own tid vl;
       (* The mask for starting the sharing does /not/ include the
          namespace N, for allowing more flexibility for the user of
          this type (typically for the [own] type). AFAIK, there is no
@@ -59,7 +60,7 @@ Section defs.
                  (∃ vl, (&frac{κ} λ q, l ↦★{q} vl) ★ ▷ st.(st_own) tid vl)%I
     |}.
   Next Obligation. apply st_size_eq. Qed.
-  Next Obligation. iIntros (st tid vl _) "H". eauto. Qed.
+  Next Obligation. iIntros (st tid vl E _) "H". eauto. Qed.
   Next Obligation.
     intros st E N κ l tid q ??. iIntros "Hmt Htok".
     iVs (lft_borrow_exists with "Hmt Htok") as (vl) "[Hmt Htok]". set_solver.
@@ -105,7 +106,7 @@ Section types.
     {| ty_size := 0; ty_dup := true;
        ty_own tid vl := False%I; ty_shr κ tid N l := False%I |}.
   Next Obligation. iIntros (tid vl) "[]". Qed.
-  Next Obligation. iIntros (???) "[]". Qed.
+  Next Obligation. iIntros (????) "[]". Qed.
   Next Obligation.
     iIntros (????????) "Hb Htok".
     iVs (lft_borrow_exists with "Hb Htok") as (vl) "[Hb Htok]". set_solver.
@@ -341,15 +342,15 @@ Section types.
     subst. by iApply (list_ty_type_eq with "Hown").
   Qed.
   Next Obligation.
-    induction tyl as [|ty tyq IH]; iIntros (tid vl Hfa) "H";
+    induction tyl as [|ty tyq IH]; iIntros (tid vl E Hfa) "H";
       iDestruct "H" as ([|vl0 vlq]) "(%&#Hlen&Hown)"; subst vl;
       iDestruct "Hlen" as %Hlen; inversion Hlen; simpl in *.
-    - iSplit; iExists []; by repeat iSplit.
+    - iIntros "!==>". iSplit; iExists []; by repeat iSplit.
     - apply andb_prop_elim in Hfa. destruct Hfa as [Hfah Hfaq].
       iDestruct (big_sepL_cons with "Hown") as "[Hh Hq]".
-      iDestruct (ty_dup_dup with "Hh") as "[Hh1 Hh2]". done.
-      iDestruct (IH tid (concat vlq) Hfaq with "[Hq]") as "[Hq1 Hq2]". by eauto.
-      iSplitL "Hh1 Hq1".
+      iVs (ty_dup_dup with "Hh") as "[Hh1 Hh2]". done.
+      iVs (IH tid (concat vlq) _ Hfaq with "[Hq]") as "[Hq1 Hq2]". by eauto.
+      iVsIntro. iSplitL "Hh1 Hq1".
       + iDestruct "Hq1" as (vllq) "(%&%&?)". iExists (vl0::vllq).
         rewrite big_sepL_cons/=. iFrame. iSplit; iPureIntro; congruence.
       + iDestruct "Hq2" as (vllq) "(%&%&?)". iExists (vl0::vllq).
@@ -443,9 +444,9 @@ Section types.
     simpl. by iDestruct (sum_size_eq with "Hown") as %->.
   Qed.
   Next Obligation.
-    iIntros (n tyl Hn tid vl Hdup%Is_true_eq_true) "Hown".
+    iIntros (n tyl Hn tid vl E Hdup%Is_true_eq_true) "Hown".
     iDestruct "Hown" as (i vl') "[% Hown]". subst.
-    iDestruct ((nth i tyl bot).(ty_dup_dup) with "Hown") as "[Hown1 Hown2]".
+    iVs ((nth i tyl bot).(ty_dup_dup) with "Hown") as "[Hown1 Hown2]".
     - edestruct nth_in_or_default as [| ->]; last done.
       rewrite ->forallb_forall in Hdup. auto using Is_true_eq_left.
     - iSplitR "Hown1"; eauto.

type_incl.v

@@ -19,9 +19,7 @@ Section ty_incl.
                   ty2.(ty_shr) κ tid E l ★ ty1.(ty_size) = ty2.(ty_size)).
 
   Global Instance ty_incl_refl ρ : Reflexive (ty_incl ρ).
-  Proof.
-    iIntros (ty tid) "_!==>". iSplit; iIntros "!#"; eauto.
-  Qed.
+  Proof. iIntros (ty tid) "_!==>". iSplit; iIntros "!#"; eauto. Qed.
 
   Lemma ty_incl_trans ρ θ ty1 ty2 ty3 :
     ty_incl ρ ty1 ty2 → ty_incl θ ty2 ty3 → ty_incl (ρ ★ θ) ty1 ty3.
@@ -37,11 +35,15 @@ Section ty_incl.
   Qed.
 
   Lemma ty_incl_weaken ρ θ ty1 ty2 :
-    perm_incl ρ θ → ty_incl θ ty1 ty2 → ty_incl ρ ty1 ty2.
+    ρ ⇒ θ → ty_incl θ ty1 ty2 → ty_incl ρ ty1 ty2.
   Proof. iIntros (Hρθ Hρ' tid) "H". iVs (Hρθ with "H"). by iApply Hρ'. Qed.
 
-  Global Instance ty_incl_trans' ρ: Duplicable ρ → Transitive (ty_incl ρ).
-  Proof. intros ??????. eauto using ty_incl_weaken, ty_incl_trans. Qed.
+  Global Instance ty_incl_preorder ρ: Duplicable ρ → PreOrder (ty_incl ρ).
+  Proof.
+    split.
+    - apply _.
+    - intros ?????. eauto using ty_incl_weaken, ty_incl_trans.
+  Qed.
 
   Lemma ty_incl_bot ρ ty : ty_incl ρ ! ty.
   Proof. iIntros (tid) "_!==>". iSplit; iIntros "!#*/=[]". Qed.
@@ -197,30 +199,42 @@ Section ty_incl.
   (* FIXME : idem : cannot combine the fractured borrow. *)
   Admitted.
 
-  (* Lemma ty_incl_cont_frame {n} ρ ρ1 ρ2 : *)
-  (*   Duplicable ρ → (∀ vl : vec val n, perm_incl (ρ ★ ρ2 vl) (ρ1 vl)) → *)
-  (*   ty_incl ρ (cont ρ1) (cont ρ2). *)
-  (* Proof. *)
-  (*   iIntros (? Hρ1ρ2 tid) "Hρ". *)
-  (*   iVs (inv_alloc lrustN _ (ρ tid) with "[Hρ]") as "#INV". by auto. *)
-  (*   iIntros "!==>". iSplit; iIntros "!#*H"; last by auto. *)
-  (*   iDestruct "H" as (f xl e ?) "[% Hwp]". subst. iExists _, _, _, _. iSplit. done. *)
-  (*   iIntros (vl) "Htl Hown". *)
-  (*   iApply pvs_wp. iInv lrustN as "Hρ" "Hclose". *)
-
-  (*   iSplit; last by iIntros "{Hρ}!#*_"; auto. *)
-  (*   (* FIXME : I do not know how to prove this. Should we put this *)
-  (*      under a view modality and then put Hρ in an invariant? *) *)
-  (*   admit. *)
-  (* Admitted. *)
-
-  (* Lemma ty_incl_fn_frame {n} ρ ρ1 ρ2 : *)
-  (*   Duplicable ρ → (∀ vl : vec val n, perm_incl (ρ ★ ρ2 vl) (ρ1 vl)) → *)
-  (*   ty_incl ρ (fn ρ1) (fn ρ2). *)
-  (*   (* FIXME : idem. *) *)
-  (*   admit. *)
-  (* Admitted. *)
+  Lemma ty_incl_cont {n} ρ ρ1 ρ2 :
+    Duplicable ρ → (∀ vl : vec val n, ρ ★ ρ2 vl ⇒ ρ1 vl) →
+    ty_incl ρ (cont ρ1) (cont ρ2).
+  Proof.
+    iIntros (? Hρ1ρ2 tid) "Hρ".
+    iVs (inv_alloc lrustN _ (ρ tid) with "[Hρ]") as "#INV". by auto.
+    iIntros "!==>". iSplit; iIntros "!#*H"; last by auto.
+    iDestruct "H" as (f) "[% Hwp]". subst. iExists _. iSplit. done.
+    iIntros (vl) "Htl Hown".
+    iApply pvs_wp. iInv lrustN as "Hρ" "Hclose".
+    (* FIXME : we need some kind of "Invariant of duplicable
+       propositions" that we can open several times. *)
+    admit.
+  Admitted.
+
+  Lemma ty_incl_fn {n} ρ ρ1 ρ2 :
+    Duplicable ρ → (∀ vl : vec val n, ρ ★ ρ2 vl ⇒ ρ1 vl) →
+    ty_incl ρ (fn ρ1) (fn ρ2).
+    (* FIXME : idem. *)
+    admit.
+  Admitted.
+
+  Lemma ty_incl_fn_cont {n} ρ ρf : ty_incl ρ (fn ρf) (cont (n:=n) ρf).
+  Proof.
+    iIntros (tid) "_!==>". iSplit; iIntros "!#*H"; last by iSplit.
+    iDestruct "H" as (f) "[%#H]". subst. iExists _. iSplit. done.
+    iIntros (vl) "Hρf Htl". iApply "H". by iFrame.
+  Qed.
 
   (* TODO : forall, when we will have figured out the right definition. *)
 
+  Lemma ty_incl_perm_incl ρ ty1 ty2 v :
+    ty_incl ρ ty1 ty2 → ρ ★ v ◁ ty1 ⇒ v ◁ ty2.
+  Proof.
+    iIntros (Hincl tid) "[Hρ Hty1]". iVs (Hincl with "Hρ") as "[#Hownincl _]".
+    by iApply "Hownincl".
+  Qed.
+
 End ty_incl.
\ No newline at end of file