Solve some todos about automation.

theories/typing/cont_context.v

@@ -92,7 +92,7 @@ Section cont_context.
     iApply ("H" with "HE * [%]"). by apply HC1C2.
   Qed.
 
-  Lemma cctx_incl_cons E k L n (T1 T2 : vec val n → _) C1 C2:
+  Lemma cctx_incl_cons E k L n (T1 T2 : vec val n → tctx) C1 C2 :
     cctx_incl E C1 C2 → (∀ args, tctx_incl E L (T2 args) (T1 args)) →
     cctx_incl E (k ◁cont(L, T1) :: C1) (k ◁cont(L, T2) :: C2).
   Proof.
@@ -107,4 +107,8 @@ Section cont_context.
       iIntros "HE". iIntros (x') "%".
       iApply ("H" with "HE * [%]"). by apply elem_of_cons; auto.
   Qed.
+
+  Lemma cctx_incl_nil E C : cctx_incl E C [].
+  Proof. apply incl_cctx_incl. by set_unfold. Qed.
+
 End cont_context.

theories/typing/lft_contexts.v

@@ -361,7 +361,7 @@ Section elctx_incl.
     rewrite /elctx_interp big_sepL_nil. auto.
   Qed.
 
-  Global Instance elctx_incl_app :
+  Global Instance elctx_incl_app_proper :
     Proper (elctx_incl ==> elctx_incl ==> elctx_incl) app.
   Proof.
     iIntros (?? HE1 ?? HE2 ??) "#HE #HL *". rewrite {1}/elctx_interp big_sepL_app.
@@ -377,6 +377,10 @@ Section elctx_incl.
     done.
   Qed.
 
+  Global Instance elctx_incl_cons_proper x :
+    Proper (elctx_incl ==> elctx_incl) (cons x).
+  Proof. intros ???. by apply (elctx_incl_app_proper [_] [_]). Qed.
+
   Lemma elctx_incl_dup E1 :
     elctx_incl E1 (E1 ++ E1).
   Proof.
@@ -399,7 +403,8 @@ Section elctx_incl.
   Lemma elctx_incl_lft_alive E1 E2 κ :
     lctx_lft_alive E1 [] κ → elctx_incl E1 E2 → elctx_incl E1 ((☀κ) :: E2).
   Proof.
-    intros Hκ HE2. rewrite ->elctx_incl_dup. apply (elctx_incl_app _ [_]); last done.
+    intros Hκ HE2. rewrite ->elctx_incl_dup.
+    apply (elctx_incl_app_proper _ [_]); last done.
     apply elctx_sat_incl. apply elctx_sat_alive, elctx_sat_nil; first done.
   Qed.
 
@@ -415,25 +420,11 @@ Section elctx_incl.
     iExists qE2. rewrite /elctx_interp big_sepL_cons /=. iFrame "∗#".
     iIntros "!> [_ HE2']". by iApply "Hclose'".
   Qed.
-
-  Lemma elctx_incl_lft_incl_alive E1 E2 κ κ' :
-    lctx_lft_incl (E ++ E1) L κ κ' → elctx_incl E1 E2 →
-    elctx_incl ((☀κ) :: E1) ((☀κ') :: E2).
-  Proof.
-    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.
 
-Hint Constructors Forall elem_of_list : lrust_typing.
+Ltac solve_typing := by eauto 100 with lrust_typing.
+
+Hint Constructors Forall : lrust_typing.
 Hint Resolve
      lctx_lft_incl_relf lctx_lft_incl_static lctx_lft_incl_local'
      lctx_lft_incl_external'
@@ -442,4 +433,19 @@ Hint Resolve
      elctx_incl_refl elctx_incl_nil elctx_incl_lft_alive elctx_incl_lft_incl
   : lrust_typing.
 
+(* We declare these as hint extern, so that the [B] parameter of elem_of does
+   not have to be [list _] and can be an alias of this. *)
+Hint Extern 0 (@elem_of _ _ (@elem_of_list _) _ (_ :: _)) =>
+  eapply @elem_of_list_here.
+Hint Extern 1 (@elem_of _ _ (@elem_of_list _) _ (_ :: _)) =>
+  eapply @elem_of_list_further.
+
 Hint Resolve lctx_lft_alive_external' | 100 : lrust_typing.
+
+Lemma elctx_incl_lft_incl_alive `{invG Σ, lftG Σ} E L E1 E2 κ κ' :
+  lctx_lft_incl (E ++ E1) L κ κ' → elctx_incl E L E1 E2 →
+  elctx_incl E L ((☀κ) :: E1) ((☀κ') :: E2).
+Proof.
+  intros Hκκ' ->%(elctx_incl_lft_incl _ _ _ _ _ _ Hκκ').
+  apply (elctx_incl_app_proper _ _ [_; _] [_]); solve_typing.
+Qed.

theories/typing/type.v

@@ -447,5 +447,3 @@ Section weakening.
 End weakening.
 
 Hint Resolve subtype_refl eqtype_refl : lrust_typing.
-
-Ltac solve_typing := by eauto 100 with lrust_typing.