Merge branch 'master' of gitlab.mpi-sws.org:FP/LambdaRust-coq

theories/typing/function.v

@@ -109,7 +109,26 @@ Section typing.
     (∀ x, subtype (E0 ++ E x) L0 (ty1 x) (ty2 x)) →
     subtype E0 L0 (fn E tys1 ty1) (fn E tys2 ty2).
   Proof.
-    intros. apply fn_subtype_full; try done. intros. apply elctx_incl_refl.
+    intros. apply fn_subtype_full; try done.
+  Qed.
+
+  (* This proper and the next can probably not be inferred, but oh well. *)
+  Global Instance fn_subtype_ty' {A n} E0 L0 E :
+    Proper (flip (pointwise_relation A (λ (v1 v2 : vec type n), Forall2 (subtype E0 L0) v1 v2)) ==>
+            pointwise_relation A (subtype E0 L0) ==> subtype E0 L0) (fn E).
+  Proof.
+    intros tys1 tys2 Htys ty1 ty2 Hty. apply fn_subtype_ty.
+    - intros. eapply Forall2_impl; first eapply Htys. intros ??.
+      eapply subtype_weaken; last done. by apply contains_inserts_r.
+    - intros. eapply subtype_weaken, Hty; last done. by apply contains_inserts_r.
+  Qed.
+
+  Global Instance fn_eqtype_ty' {A n} E0 L0 E :
+    Proper (pointwise_relation A (λ (v1 v2 : vec type n), Forall2 (eqtype E0 L0) v1 v2) ==>
+            pointwise_relation A (eqtype E0 L0) ==> eqtype E0 L0) (fn E).
+  Proof.
+    intros tys1 tys2 Htys ty1 ty2 Hty. split; eapply fn_subtype_ty'; try (by intro; apply Hty);
+      intros x; (apply Forall2_flip + idtac); (eapply Forall2_impl; first by eapply (Htys x)); by intros ??[].
   Qed.
 
   Lemma fn_subtype_elctx_sat {A n} E0 L0 E E' (tys : A → vec type n) ty :
@@ -126,7 +145,7 @@ Section typing.
     intros Hκκ'. apply fn_subtype_full; try done. intros.
     apply elctx_incl_lft_incl; last by apply elctx_incl_refl.
     iIntros "#HE #HL". iApply (Hκκ' with "[HE] HL").
-    rewrite /elctx_interp_0 big_sepL_app. iDestruct "HE" as "[_ $]".
+    rewrite /elctx_interp_0 big_sepL_app. iDestruct "HE" as "[$ _]".
   Qed.
 
   Lemma fn_subtype_specialize {A B n} (σ : A → B) E0 L0 E tys ty :

theories/typing/lft_contexts.v

@@ -311,7 +311,10 @@ End lft_contexts.
 
 Section elctx_incl.
   (* External lifetime context inclusion, in a persistent context.
-     (Used for function types subtyping). *)
+     (Used for function types subtyping).
+     On paper, this corresponds to using only the inclusions from E, L
+     to show E1; [] |- E2.
+  *)
 
   Context `{invG Σ, lftG Σ} (E : elctx) (L : llctx).
 
@@ -320,8 +323,19 @@ Section elctx_incl.
     ∀ qE1, elctx_interp E1 qE1 ={F}=∗ ∃ qE2, elctx_interp E2 qE2 ∗
        (elctx_interp E2 qE2 ={F}=∗ elctx_interp E1 qE1).
 
+  Global Instance elctx_incl_preorder : PreOrder elctx_incl.
+  Proof.
+    split.
+    - iIntros (???) "_ _ * ?". iExists _. iFrame. eauto.
+    - iIntros (x y z Hxy Hyz ??) "#HE #HL * HE1".
+      iMod (Hxy with "HE HL * HE1") as (qy) "[HE1 Hclose1]"; first done.
+      iMod (Hyz with "HE HL * HE1") as (qz) "[HE1 Hclose2]"; first done.
+      iModIntro. iExists qz. iFrame "HE1". iIntros "HE1".
+      iApply ("Hclose1" with ">"). iApply "Hclose2". done.
+  Qed.
+
   Lemma elctx_incl_refl E' : elctx_incl E' E'.
-  Proof. iIntros (??) "_ _ * ?". iExists _. iFrame. eauto. Qed.
+  Proof. reflexivity. Qed.
 
   Lemma elctx_incl_nil E' : elctx_incl E' [].
   Proof.
@@ -329,22 +343,50 @@ Section elctx_incl.
     rewrite /elctx_interp big_sepL_nil. auto.
   Qed.
 
+  Global Instance elctx_incl_app :
+    Proper (elctx_incl ==> elctx_incl ==> elctx_incl) app.
+  Proof.
+    iIntros (?? HE1 ?? HE2 ??) "#HE #HL *". rewrite {1}/elctx_interp big_sepL_app.
+    iIntros "[HE1 HE2]".
+    iMod (HE1 with "HE HL * HE1") as (q1) "[HE1 Hclose1]"; first done.
+    iMod (HE2 with "HE HL * HE2") as (q2) "[HE2 Hclose2]"; first done.
+    destruct (Qp_lower_bound q1 q2) as (q & ? & ? & -> & ->).
+    iModIntro. iExists q. rewrite /elctx_interp !big_sepL_app.
+    iDestruct "HE1" as "[$ HE1]". iDestruct "HE2" as "[$ HE2]".
+    iIntros "[HE1' HE2']".
+    iMod ("Hclose1" with "[$HE1 $HE1']") as "$".
+    iMod ("Hclose2" with "[$HE2 $HE2']") as "$".
+    done.
+  Qed.
+
+  Lemma elctx_incl_dup E1 :
+    elctx_incl E1 (E1 ++ E1).
+  Proof.
+    iIntros (??) "#HE #HL * [HE1 HE1']".
+    iModIntro. iExists (qE1 / 2)%Qp.
+    rewrite /elctx_interp !big_sepL_app. iFrame.
+    iIntros "[HE1 HE1']". by iFrame.
+  Qed.
+
+  Lemma elctx_sat_incl E1 E2 :
+    elctx_sat E1 [] E2 → elctx_incl E1 E2.
+   Proof.
+    iIntros (H12 ??) "#HE #HL * HE1".
+    iMod (H12 _ 1%Qp with "HE1 []") as (qE2) "[HE2 Hclose]". done.
+    { by rewrite /llctx_interp big_sepL_nil. }
+    iExists qE2. iFrame. iIntros "!> HE2".
+    by iMod ("Hclose" with "HE2") as "[$ _]".
+   Qed.
+
   Lemma elctx_incl_lft_alive E1 E2 κ :
     lctx_lft_alive E1 [] κ → elctx_incl E1 E2 → elctx_incl E1 ((☀κ) :: E2).
   Proof.
-    iIntros (Hκ HE2 ??) "#HE #HL * [HE11 HE12]".
-    iMod (Hκ _ _ 1%Qp with "HE11 []") as (qE21) "[Hκ Hclose]". done.
-    { by rewrite /llctx_interp big_sepL_nil. }
-    iMod (HE2 with "HE HL * HE12") as (qE22) "[HE2 Hclose']". done.
-    destruct (Qp_lower_bound qE21 qE22) as (qE2 & ? & ? & -> & ->).
-    iExists qE2. rewrite /elctx_interp big_sepL_cons /=.
-    iDestruct "HE2" as "[$ HE2]". iDestruct "Hκ" as "[$ Hκ]". iIntros "!> [Hκ' HE2']".
-    iMod ("Hclose" with "[$Hκ $Hκ']") as "[$ _]".
-    iApply "Hclose'". by iFrame.
+    intros Hκ HE2. rewrite ->elctx_incl_dup. apply (elctx_incl_app _ [_]); last done.
+    apply elctx_sat_incl. apply elctx_sat_alive, elctx_sat_nil; first done.
   Qed.
 
   Lemma elctx_incl_lft_incl E1 E2 κ κ' :
-    lctx_lft_incl (E1 ++ E) L κ κ' → elctx_incl E1 E2 →
+    lctx_lft_incl (E ++ E1) L κ κ' → elctx_incl E1 E2 →
     elctx_incl E1 ((κ ⊑ κ') :: E2).
   Proof.
     iIntros (Hκκ' HE2 ??) "#HE #HL * HE1".
@@ -356,14 +398,20 @@ Section elctx_incl.
     iIntros "!> [_ HE2']". by iApply "Hclose'".
   Qed.
 
-  Lemma elctx_sat_incl E1 E2 :
-    elctx_sat E1 [] E2 → elctx_incl E1 E2.
+  Lemma elctx_incl_lft_incl_alive E1 E2 κ κ' :
+    lctx_lft_incl (E ++ E1) L κ κ' → elctx_incl E1 E2 →
+    elctx_incl ((☀κ) :: E1) ((☀κ') :: E2).
   Proof.
-    iIntros (H12 ??) "#HE #HL * HE1".
-    iMod (H12 _ 1%Qp with "HE1 []") as (qE2) "[HE2 Hclose]". done.
-    { by rewrite /llctx_interp big_sepL_nil. }
-    iExists qE2. iFrame. iIntros "!> HE2".
-    by iMod ("Hclose" with "HE2") as "[$ _]".
+    intros Hκκ' HE2%(elctx_incl_lft_incl _ _ _ _ Hκκ').
+    (* TODO: can we do this more in rewrite-style? *)
+    trans ((☀ κ) :: (κ ⊑ κ') :: E2)%EL.
+    { by apply (elctx_incl_app [_] [_]). }
+    apply (elctx_incl_app [_; _] [_]); last done.
+    (* TODO: Can we test the auto-context stuff here? *)
+    clear. apply elctx_sat_incl. apply elctx_sat_alive, elctx_sat_nil.
+    eapply lctx_lft_alive_external'.
+    - left.
+    - right. by apply elem_of_list_singleton.
   Qed.
 End elctx_incl.
 
@@ -376,4 +424,4 @@ Hint Resolve
      elctx_incl_refl elctx_incl_nil elctx_incl_lft_alive elctx_incl_lft_incl
   : lrust_typing.
 
-Hint Resolve lctx_lft_alive_external' | 100 : lrust_typing.
\ No newline at end of file
+Hint Resolve lctx_lft_alive_external' | 100 : lrust_typing.

theories/typing/type.v

 From iris.base_logic.lib Require Export na_invariants.
+From iris.base_logic Require Import big_op.
 From lrust.lang Require Export proofmode notation.
 From lrust.lifetime Require Import borrow frac_borrow reborrow.
 From lrust.typing Require Import lft_contexts.
@@ -428,6 +429,23 @@ Section subtyping.
   Qed.
 End subtyping.
 
+Section weakening.
+  Context `{typeG Σ}.
+
+  Lemma subtype_weaken E1 E2 L1 L2 ty1 ty2 :
+    E1 `contains` E2 → L1 `contains` L2 →
+    subtype E1 L1 ty1 ty2 → subtype E2 L2 ty1 ty2.
+  Proof.
+    (* TODO: There's no lemma relating `contains` to membership (∈)...?? *)
+    iIntros (HE12 [L' HL12]%contains_Permutation Hsub) "#LFT HE HL".
+    iApply (Hsub with "LFT [HE] [HL]").
+    - rewrite /elctx_interp_0. by iApply big_sepL_contains.
+    - iDestruct "HL" as %HL. iPureIntro. intros ??. apply HL.
+      rewrite HL12. set_solver.
+  Qed.
+
+End weakening.
+
 Hint Resolve subtype_refl eqtype_refl : lrust_typing.
 
 Ltac solve_typing := by eauto 100 with lrust_typing.

theories/typing/type_context.v

@@ -197,21 +197,20 @@ Section type_context.
     rewrite /tctx_incl. iIntros (Hc ???) "_ $ $ H". by iApply big_sepL_contains.
   Qed.
 
-  Lemma tctx_incl_frame E L T11 T12 T21 T22 :
-    tctx_incl E L T11 T12 → tctx_incl E L T21 T22 →
-    tctx_incl E L (T11++T21) (T12++T22).
+  Global Instance tctx_incl_app E L :
+    Proper (tctx_incl E L ==> tctx_incl E L ==> tctx_incl E L) app.
   Proof.
-    intros Hincl1 Hincl2 ???. rewrite /tctx_interp !big_sepL_app.
+    intros ?? Hincl1 ?? Hincl2 ???. rewrite /tctx_interp !big_sepL_app.
     iIntros "#LFT HE HL [H1 H2]".
     iMod (Hincl1 with "LFT HE HL H1") as "(HE & HL & $)".
     iApply (Hincl2 with "LFT HE HL H2").
   Qed.
   Lemma tctx_incl_frame_l E L T T1 T2 :
     tctx_incl E L T1 T2 → tctx_incl E L (T++T1) (T++T2).
-  Proof. by apply tctx_incl_frame. Qed.
+  Proof. by apply tctx_incl_app. Qed.
   Lemma tctx_incl_frame_r E L T T1 T2 :
     tctx_incl E L T1 T2 → tctx_incl E L (T1++T) (T2++T).
-  Proof. by intros; apply tctx_incl_frame. Qed.
+  Proof. by intros; apply tctx_incl_app. Qed.
 
   Lemma copy_tctx_incl E L p `{!Copy ty} :
     tctx_incl E L [p ◁ ty] [p ◁ ty; p ◁ ty].