WIP sum: prove subtyping

theories/typing/sum.v

+From iris.base_logic Require Import big_op.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import list.
 From iris.base_logic Require Import fractional.
@@ -130,19 +131,27 @@ Section sum.
   Global Instance sum_mono E L :
     Proper (Forall2 (subtype E L) ==> subtype E L) sum.
   Proof.
-    iIntros (tyl1 tyl2 Htyl) "#? %".
-    iAssert (⌜max_list_with ty_size tyl1 = max_list_with ty_size tyl2⌝%I) with "[#]" as %Hleq.
-    { iInduction Htyl as [|???? Hsub] "IH"; first done.
-      iDestruct (Hsub with "[] []") as "(% & _ & _)"; [done..|].
-      iDestruct "IH" as %IH. iPureIntro. simpl. inversion_clear IH. by f_equal. }
+    iIntros (tyl1 tyl2 Htyl qL) "HL".
+    iAssert (□ (lft_contexts.elctx_interp E -∗ ⌜max_list_with ty_size tyl1 = max_list_with ty_size tyl2⌝))%I with "[#]" as "#Hleq".
+    { iInduction Htyl as [|???? Hsub] "IH".
+      { iClear "∗". iIntros "!# _". done. }
+      iDestruct (Hsub with "HL") as "#Hsub". iDestruct ("IH" with "HL") as "{IH} #IH".
+      (* FIXME: WHy does the previous iDestruvt remove HL? *)
+      iAlways. iIntros "#HE". iDestruct ("Hsub" with "HE") as "(% & _ & _)".
+      iDestruct ("IH" with "HE") as %IH. iPureIntro. simpl. inversion_clear IH. by f_equal. }
+    iDestruct (subtype_Forall2_llctx with "HL") as "#Htyl"; first done.
+    iClear "HL". iIntros "!# #HE".
+    iDestruct ("Hleq" with "HE") as %Hleq. iSpecialize ("Htyl" with "HE"). iClear "Hleq HE".
     iAssert (∀ i, type_incl (nth i tyl1 ∅) (nth i tyl2 ∅))%I with "[#]" as "#Hty".
       { iIntros (i). edestruct (nth_lookup_or_length tyl1 i) as [Hl1|Hl]; last first.
         { rewrite nth_overflow // nth_overflow; first by iApply type_incl_refl.
           by erewrite <-Forall2_length. }
-        edestruct @Forall2_lookup_l as (ty2 & Hl2 & Hty2); [done..|].
-        rewrite (nth_lookup_Some tyl2 _ _ ty2) //.
-        by iApply (Hty2 with "[] []"). }
-    clear -Hleq. iSplit; last iSplit.
+        edestruct @Forall2_lookup_l as (ty2 & Hl2 & _); [done..|].
+        iDestruct (big_sepL_lookup with "Htyl") as "Hty".
+        { rewrite lookup_zip_with. erewrite Hl1. simpl.
+          rewrite Hl2 /=. done. }
+        rewrite (nth_lookup_Some tyl2 _ _ ty2) //. }
+    clear -Hleq. iClear "∗". iSplit; last iSplit.
     - simpl. by rewrite Hleq.
     - iAlways. iIntros (tid vl) "H". iDestruct "H" as (i vl' vl'') "(% & % & Hown)".
       iExists i, vl', vl''. iSplit; first done.
@@ -174,7 +183,7 @@ Section sum.
   Lemma emp_sum E L :
     eqtype E L emp (sum []).
   Proof.
-    split; (iIntros; iSplit; first done; iSplit; iAlways).
+    split; (iIntros (q) "_ _"; iSplit; first done; iSplit; iAlways).
     - iIntros (??) "[]".
     - iIntros (κ tid l) "[]".
     - iIntros (??) "H". iDestruct "H" as (i vl' vl'') "(% & % & Hown)".

theories/typing/type.v

@@ -515,6 +515,21 @@ Section subtyping.
     iClear "∗". iIntros "!# #HE".
     iApply (type_incl_trans with "[#]"). by iApply "H12". by iApply "H23".
   Qed.
+  
+  Lemma subtype_Forall2_llctx E L tys1 tys2 qL : 
+    Forall2 (subtype E L) tys1 tys2 →
+    llctx_interp L qL -∗ □ (elctx_interp E -∗
+           [∗ list] tys ∈ (zip tys1 tys2), type_incl (tys.1) (tys.2)).
+  Proof.
+    iIntros (Htys) "HL".
+    iAssert ([∗ list] tys ∈ zip tys1 tys2,
+             □ (elctx_interp _ -∗ type_incl (tys.1) (tys.2)))%I as "#Htys".
+    { iApply big_sepL_forall. iIntros (k [ty1 ty2] Hlookup).
+      move:Htys => /Forall2_Forall /Forall_forall=>Htys.
+      iApply (Htys (ty1, ty2)); first by exact: elem_of_list_lookup_2. done. }
+    iClear "∗". iIntros "!# #HE". iApply (big_sepL_impl with "[$Htys]").
+    iIntros "!# * % #Hincl". by iApply "Hincl".
+  Qed.
 
   Lemma equiv_subtype E L ty1 ty2 : ty1 ≡ ty2 → subtype E L ty1 ty2.
   Proof. unfold subtype, type_incl=>EQ. setoid_rewrite EQ. apply subtype_refl. Qed.