New notation for product type. Only functions can be generalized. Fix...

New notation for product type. Only functions can be generalized. Fix perm_incl_share by adding tokens.

perm_incl.v

@@ -104,23 +104,20 @@ Section props.
   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.
+  Lemma perm_incl_share q v κ ty :
+    v ◁ &uniq{κ} ty ★ [κ]{q} ⇒ v ◁ &shr{κ} ty ★ [κ]{q}.
   Proof.
-    iIntros (tid) "Huniq". destruct v; last done.
+    iIntros (tid) "[Huniq [Htok Hlft]]". destruct v; last by iDestruct "Huniq" as "[]".
     iDestruct "Huniq" as (l) "[% Hown]".
-    (* FIXME : we need 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 _]".
+    iVs (ty.(ty_share) _ lrustN with "Hown Htok") as "[Hown Htok]".
     apply disjoint_union_l; solve_ndisj. set_solver. iVsIntro.
-    iExists _. iSplit. done. done.
-  Admitted.
+    iFrame. iExists _. iSplit. done. done.
+  Qed.
 
   Lemma split_own_prod tyl (q0: Qp) (ql : list Qp) (l : loc) tid :
     length tyl = length ql →
-      (own (foldr Qp_plus q0 ql) (product tyl)).(ty_own) tid [ #l] ⊣⊢
-    ▷ †{q0}(shift_loc l (0 + (product tyl).(ty_size))%nat)…0 ★
+      (own (foldr Qp_plus q0 ql) (Π tyl)).(ty_own) tid [ #l] ⊣⊢
+    ▷ †{q0}(shift_loc l (0 + (Π tyl).(ty_size))%nat)…0 ★
     [★ list] qtyoffs ∈ (combine ql (combine_offs tyl 0)),
          (own (qtyoffs.1) (qtyoffs.2.1)).(ty_own)
               tid [ #(shift_loc l (qtyoffs.2.2))].
@@ -146,7 +143,7 @@ Section props.
   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) ⇔
+    v ◁ own q (Π tyl) ⇔
       foldr (λ qtyoffs acc,
              proj_valuable (Z.of_nat (qtyoffs.2.2)) v ◁
                            own (qtyoffs.1) (qtyoffs.2.1) ★ acc)
@@ -180,7 +177,7 @@ Section props.
   Qed.
 
   Lemma perm_split_uniq_borrow_prod tyl κ v :
-    v ◁ &uniq{κ} (product tyl) ⇒
+    v ◁ &uniq{κ} (Π tyl) ⇒
       foldr (λ tyoffs acc,
              proj_valuable (Z.of_nat (tyoffs.2)) v ◁ &uniq{κ} (tyoffs.1) ★ acc)%P
             ⊤ (combine_offs tyl 0).
@@ -189,16 +186,15 @@ Section props.
     destruct v as [[[|l|]|]|];
       iIntros "H"; try iDestruct "H" as "[]";
         iDestruct "H" as (l0) "[EQ H]"; iDestruct "EQ" as %[=]. subst l0.
-    rewrite split_prod_mt. iRevert "H".
-    induction (combine_offs tyl 0) as [|[ty offs] ll IH]. by auto.
-    iIntros "H". rewrite big_sepL_cons /=.
+    rewrite split_prod_mt.
+    iInduction (combine_offs tyl 0) as [|[ty offs] ll] "IH". by auto.
+    rewrite big_sepL_cons /=.
     iVs (lft_borrow_split with "H") as "[H0 H]". set_solver.
-    iVs (IH with "[] H") as "$". done.
-    iVsIntro. iExists _. eauto.
+    iVs ("IH" with "H") as "$". iVsIntro. iExists _. eauto.
   Qed.
 
   Lemma perm_split_shr_borrow_prod tyl κ v :
-    v ◁ &shr{κ} (product tyl) ⇒
+    v ◁ &shr{κ} (Π tyl) ⇒
       foldr (λ tyoffs acc,
              proj_valuable (Z.of_nat (tyoffs.2)) v ◁ &shr{κ} (tyoffs.1) ★ acc)%P
             ⊤ (combine_offs tyl 0).
@@ -209,6 +205,7 @@ Section props.
         iDestruct "H" as (l0) "[EQ H]"; iDestruct "EQ" as %[=]. subst l0.
     simpl. iVsIntro. iRevert "H".
     change (ndot (A:=nat)) with (λ N i, N .@ (0+i)%nat). generalize O at 2.
+    (* TODO : use iInduction, but we need to do it under generalization of O. *)
     induction (combine_offs tyl 0) as [|[ty offs] ll IH]. by auto.
     iIntros (i) "H". rewrite big_sepL_cons /=. iDestruct "H" as "[H0 H]".
     setoid_rewrite <-Nat.add_succ_comm. iDestruct (IH with "[] H") as "$". done.

type.v

@@ -417,8 +417,9 @@ Section types.
   Class LstTySize (n : nat) (tyl : list type) :=
     size_eq : Forall ((= n) ∘ ty_size) tyl.
   Instance LstTySize_nil n : LstTySize n nil := List.Forall_nil _.
-  Hint Extern 1 (LstTySize _ (_ :: _)) =>
-    apply List.Forall_cons; [reflexivity|] : typeclass_instances.
+  Lemma LstTySize_cons n ty tyl :
+    ty.(ty_size) = n → LstTySize n tyl → LstTySize n (ty :: tyl).
+  Proof. intros. constructor; done. Qed.
 
   Lemma sum_size_eq n tid i tyl vl {Hn : LstTySize n tyl} :
     ty_own (nth i tyl emp) tid vl ⊢ length vl = n.
@@ -510,34 +511,23 @@ Section types.
   Next Obligation. intros. by iIntros "_ _". Qed.
   Next Obligation. done. Qed.
 
-  Program Definition fn {n : nat} (ρ : vec val n → @perm Σ):=
-    ty_of_st {| st_size := 1;
-       st_own tid vl := (∃ f, vl = [f] ★
-          ∀ vl, {{ ρ vl tid ★ tl_own tid ⊤ }} f (map of_val vl) {{λ _, False}})%I |}.
+  Program Definition fn {A : Type} {n : nat} (ρ : A -> vec val n → @perm Σ):=
+    ty_of_st {|
+        st_size := 1;
+        st_own tid vl := (∃ f, vl = [f] ★
+          ∀ x vl, {{ ρ x vl tid ★ tl_own tid ⊤ }} f (map of_val vl) {{λ _, False}})%I |}.
   Next Obligation.
-    iIntros (n ρ tid vl) "H". iDestruct "H" as (f) "[% _]". by subst.
+    iIntros (x n ρ tid vl) "H". iDestruct "H" as (f) "[% _]". by subst.
   Qed.
 
-  (* TODO *)
-  (* Program Definition forall_ty {A : Type} n dup (ty : A -> type) {_:Inhabited A} *)
-  (*         (Hsz : ∀ x, (ty x).(ty_size) = n) (Hdup : ∀ x, (ty x).(ty_dup) = dup) := *)
-  (*   ty_of_st {| st_size := n; st_dup := dup; *)
-  (*               st_own tid vl := (∀ x, (ty x).(ty_own) tid vl)%I |}. *)
-  (* Next Obligation. *)
-  (*   intros A n dup ty ? Hn Hdup tid vl. iIntros "H". iSpecialize ("H" $! inhabitant). *)
-  (*   rewrite -(Hn inhabitant). by iApply ty_size_eq. *)
-  (* Qed. *)
-  (* Next Obligation. *)
-  (*   intros A n [] ty ? Hn Hdup tid vl []. *)
-  (*   (* FIXME: A quantified assertion is not necessarilly dupicable if *)
-  (*      its contents is.*) *)
-  (*   admit. *)
-  (* Admitted. *)
-
 End types.
 
 End Types.
 
+Existing Instance Types.LstTySize_nil.
+Hint Extern 1 (Types.LstTySize _ (_ :: _)) =>
+  apply Types.LstTySize_cons; [compute; reflexivity|] : typeclass_instances.
+
 Import Types.
 
 Notation "!" := emp : lrust_type_scope.
@@ -546,12 +536,8 @@ Notation "&uniq{ κ } ty" := (uniq_borrow κ ty)
 Notation "&shr{ κ } ty" := (shared_borrow κ ty)
   (format "&shr{ κ } ty", at level 20, right associativity) : lrust_type_scope.
 
-(* FIXME : these notations do not work. *)
-Notation "( ty1 * ty2 * .. * tyn )" :=
-  (product (cons ty1 (cons ty2 ( .. (cons tyn nil) .. ))))
-  (format "( ty1  *  ty2  *  ..  *  tyn )") : lrust_type_scope.
-Notation "( ty1 + ty2 + .. + tyn )" :=
-  (sum (cons ty1 (cons ty2 ( .. (cons tyn nil) .. ))))
-  (format "( ty1  +  ty2  +  ..  +  tyn )") : lrust_type_scope.
-
-(* TODO : notation for forall *)
\ No newline at end of file
+Notation Π := product.
+(* Σ is commonly used for the current functor. So it cannot be defined
+   as Π for products. We stick to the following form. *)
+Notation "Σ[ ty1 ; .. ; tyn ]" :=
+  (sum (cons ty1 (..(cons tyn nil)..))) : lrust_type_scope.

type_incl.v

@@ -90,8 +90,7 @@ Section ty_incl.
      The only way I can see to circumvent this limitation is to deeply
      embed permissions (and their inclusion). Not sure this is worth it. *)
   Lemma ty_incl_prod ρ tyl1 tyl2 :
-    Duplicable ρ → Forall2 (ty_incl ρ) tyl1 tyl2 →
-    ty_incl ρ (product tyl1) (product tyl2).
+    Duplicable ρ → Forall2 (ty_incl ρ) tyl1 tyl2 → ty_incl ρ (Π tyl1) (Π tyl2).
   Proof.
     intros Hρ HFA. iIntros (tid) "#Hρ". iSplitL "".
     - assert (Himpl : ρ tid ={⊤}=>
@@ -109,13 +108,12 @@ Section ty_incl.
       iVs (Himpl with "Hρ") as "#Himpl". iIntros "!==>!#*H".
       iDestruct "H" as (vll) "(%&%&H)". iExists _. iSplit. done. iSplit.
       by rewrite -(Forall2_length _ _ _ HFA). by iApply ("Himpl" with "[] H").
-    - rewrite /product /=. iRevert "Hρ". generalize O.
+    - rewrite /Π /=. iRevert "Hρ". generalize O.
       change (ndot (A:=nat)) with (λ N i, N .@ (0+i)%nat). generalize O.
+      (* TODO : use iInduction, but we need to do it under generalization of O. *)
       induction HFA as [|ty1 ty2 tyl1 tyl2 Hincl HFA IH].
       + iIntros (i offs) "_!==>!#*_/=". rewrite big_sepL_nil. eauto.
-      + iIntros (i offs) "#Hρ". iVs (IH with "[] []") as "#Hqimpl".
-          by iClear "Hρ". (* TODO : get rid of this by doing induction in the proof mode. *)
-          done.
+      + iIntros (i offs) "#Hρ". iVs (IH with "[] []") as "#Hqimpl". by iClear "Hρ". done.
         iVs (Hincl with "Hρ") as "[_ #Hhimpl]". iIntros "!==>!#*".
         rewrite !big_sepL_cons. iIntros "[Hh Hq]".
         setoid_rewrite <-Nat.add_succ_comm.
@@ -126,7 +124,7 @@ Section ty_incl.
   Qed.
 
   Lemma ty_incl_prod_cons_l ρ ty tyl :
-    ty_incl ρ (product (ty :: tyl)) (product [ty ; product tyl]).
+    ty_incl ρ (Π(ty :: tyl)) (Π[ty ; Π tyl]).
   Proof.
     iIntros (tid) "_!==>". iSplit; iIntros "!#/=".
     - iIntros (vl) "H". iDestruct "H" as ([|vlh vllq]) "(%&%&H)". done. subst.
@@ -141,8 +139,8 @@ Section ty_incl.
 
   (* TODO *)
   Lemma ty_incl_prod_flatten ρ tyl1 tyl2 tyl3 :
-    ty_incl ρ (product (tyl1 ++ product tyl2 :: tyl3))
-              (product (tyl1 ++ tyl2 ++ tyl3)).
+    ty_incl ρ (Π(tyl1 ++ Π tyl2 :: tyl3))
+              (Π(tyl1 ++ tyl2 ++ tyl3)).
   Admitted.
 
   Lemma ty_incl_sum ρ n tyl1 tyl2 (_ : LstTySize n tyl1) (_ : LstTySize n tyl2) :
@@ -174,7 +172,7 @@ Section ty_incl.
   Qed.
 
   Lemma ty_incl_uninit_split ρ n1 n2 :
-    ty_incl ρ (uninit (n1+n2)) (product [uninit n1; uninit n2]).
+    ty_incl ρ (uninit (n1+n2)) (Π[uninit n1; uninit n2]).
   Proof.
     iIntros (tid) "_!==>". iSplit; iIntros "!#*H".
     - iDestruct "H" as %Hlen. iExists [take n1 vl; drop n1 vl].
@@ -194,7 +192,7 @@ Section ty_incl.
   Admitted.
 
   Lemma ty_incl_uninit_combine ρ n1 n2 :
-    ty_incl ρ (product [uninit n1; uninit n2]) (uninit (n1+n2)).
+    ty_incl ρ (Π[uninit n1; uninit n2]) (uninit (n1+n2)).
   Proof.
   (* FIXME : idem : cannot combine the fractured borrow. *)
   Admitted.
@@ -209,29 +207,40 @@ Section ty_incl.
     by iApply ("Hwp" with "[-Htl] Htl").
   Qed.
 
-  Lemma ty_incl_fn {n} ρ ρ1 ρ2 :
-    Duplicable ρ → (∀ vl : vec val n, ρ ★ ρ2 vl ⇒ ρ1 vl) →
+  Lemma ty_incl_fn {A n} ρ ρ1 ρ2 :
+    Duplicable ρ → (∀ (x : A) (vl : vec val n), ρ ★ ρ2 x vl ⇒ ρ1 x vl) →
     ty_incl ρ (fn ρ1) (fn ρ2).
   Proof.
     iIntros (? Hρ1ρ2 tid) "#Hρ!==>". iSplit; iIntros "!#*#H".
     - iDestruct "H" as (f) "[% Hwp]". subst. iExists _. iSplit. done.
-      iIntros (vl) "!#[Hρ2 Htl]". iVs (Hρ1ρ2 with "[Hρ2]"). by iFrame.
+      iIntros (x vl) "!#[Hρ2 Htl]". iVs (Hρ1ρ2 with "[Hρ2]"). by iFrame.
       iApply "Hwp". by iFrame.
     - iSplit; last done. simpl. iDestruct "H" as (vl0) "[? Hvl]".
       iExists vl0. iFrame "#". iNext. iDestruct "Hvl" as (f) "[% Hwp]".
       iExists f. iSplit. done.
-      iIntros (vl) "!#[Hρ2 Htl]". iVs (Hρ1ρ2 with "[Hρ2]"). by iFrame.
+      iIntros (x vl) "!#[Hρ2 Htl]". iVs (Hρ1ρ2 with "[Hρ2]"). by iFrame.
       iApply "Hwp". by iFrame.
   Qed.
 
-  Lemma ty_incl_fn_cont {n} ρ ρf : ty_incl ρ (fn ρf) (cont (n:=n) ρf).
+  Lemma ty_incl_fn_cont {A n} ρ ρf (x : A) :
+    ty_incl ρ (fn ρf) (cont (n:=n) (ρf x)).
   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_fn_specialize {A B n} (f : A → B) ρ ρfn :
+    ty_incl ρ (fn (n:=n) ρfn) (fn (ρfn ∘ f)).
+  Proof.
+    iIntros (tid) "_!==>". iSplit; iIntros "!#*H".
+    - iDestruct "H" as (fv) "[%#H]". subst. iExists _. iSplit. done.
+      iIntros (x vl). by iApply "H".
+    - iSplit; last done.
+      iDestruct "H" as (fvl) "[?Hown]". iExists _. iFrame. iNext.
+      iDestruct "Hown" as (fv) "[%H]". subst. iExists _. iSplit. done.
+      iIntros (x vl). by iApply "H".
+  Qed.
 
   Lemma ty_incl_perm_incl ρ ty1 ty2 v :
     ty_incl ρ ty1 ty2 → ρ ★ v ◁ ty1 ⇒ v ◁ ty2.