(* This files proves the fundamental lemma for D<:.

   It also proves any typing lemmas that depend on swap_later_impl.v (extra
   modality swap lemmas, depending on `CmraSwappable` instances for Σ). They are
   kept separate, because we might have to extend Σ with resources without a
   CmraSwappable instance.

From iris.proofmode Require Import proofmode.
From D Require Import proofmode_extra swap_later_impl.
From D.DSub Require Import unary_lr semtyp_lemmas.

Implicit Types (L T U : ty) (v : vl) (e : tm) (Γ : ctx).

Set Default Proof Using "Type*".

Section swap_based_typing_lemmas.
  Context `{!dsubSynG Σ} `{!SwapPropI Σ} {Γ}.

  Lemma All_Sub_All T1 T2 U1 U2 i :
    Γ T2, S i <: T1, S i -∗
    iterate TLater (S i) (shift T2) :: Γ U1, S i <: U2, S i -∗
    Γ TAll T1 U1, i <: TAll T2 U2, i .
    rewrite iterate_S /=.
    pupd; iIntros "#HsubT #HsubU !> /= %ρ %v #Hg".
    iDestruct 1 as (t) "#[Heq #HT1]". iExists t; iSplit ⇒ //.
    iIntros (w).
    iSpecialize ("HsubT" $! ρ w with "Hg").
    rewrite -!mlaterN_pers -mlater_impl -mlaterN_impl !swap_later.
    iIntros "!> #HwT2".
    iSpecialize ("HsubT" with "HwT2").
    iAssert ( ▷^i ( v0, U1 (w .: ρ) v0
         U2 (w .: ρ) v0))%I as "{HsubU} #HsubU". {
      iIntros (v0); rewrite -!mlaterN_impl -mlater_impl.
      iIntros "!> #HUv0".
      iApply ("HsubU" $! (w .: ρ) v0 with "[# $Hg] HUv0").
      unfold_interp; rewrite iterate_TLater_later.
      by iApply (interp_weaken_one T2).
    iNext 1; iNext i. iApply wp_wand.
    - iApply "HT1". by iApply "HsubT".
    - iIntros (u) "#HuU1". by iApply "HsubU".

  Lemma DSub_TAll_ConCov T1 T2 U1 U2 i :
    Γ ⊨[S i] T2 <: T1 -∗
    iterate TLater (S i) (shift T2) :: Γ ⊨[S i] U1 <: U2 -∗
    Γ ⊨[i] TAll T1 U1 <: TAll T2 U2.
    rewrite iterate_S /=.
    pupd; iIntros "#HsubT #HsubU !> /= %ρ #Hg %v".
    rewrite -mlaterN_impl; unfold_interp.
    iDestruct 1 as (t) "#[Heq #HT1]"; iExists t; iFrame "Heq".
    iIntros (w).
    rewrite -!mlaterN_pers -!laterN_later/= -!mlaterN_impl -!mlater_impl.
    iIntros "!> #HwT2".
    iSpecialize ("HsubT" with "Hg").
    iSpecialize ("HsubU" $! (w .: ρ) with "[# $Hg]"). {
      unfold_interp. rewrite iterate_TLater_later.
      by iApply (interp_weaken_one T2).
    iNext 1; iNext i. iApply wp_wand.
    - iApply "HT1". by iApply "HsubT".
    - iIntros (u) "#HuU1". by iApply "HsubU".

  Lemma Typ_Sub_Typ L1 L2 U1 U2 i :
    Γ L2, i <: L1, i -∗
    Γ U1, i <: U2, i -∗
    Γ TTMem L1 U1, i <: TTMem L2 U2, i.
    pupd; iIntros "#IHT #IHT1 !> /= %ρ %v #Hg".
    iDestruct 1 as (φ) "#[Hφl [HLφ #HφU]]".
    setoid_rewrite mlaterN_impl.
    iExists φ; repeat iSplitL; first done;
      iIntros "" (w);
      iSpecialize ("IHT" $! ρ w with "Hg");
      iSpecialize ("IHT1" $! ρ w with "Hg");
      iNext; iIntros "!> **".
    - iApply "HLφ" ⇒ //. by iApply "IHT".
    - iApply "IHT1". by iApply "HφU".
End swap_based_typing_lemmas.

From D.DSub Require Import storeless_typing.

Section Fundamental.
  Context `{!dsubSynG Σ} `{!SwapPropI Σ}.

  Lemma fundamental_subtype Γ T1 i1 T2 i2 (HT : Γ ⊢ₜ T1, i1 <: T2, i2) :
     Γ T1, i1 <: T2, i2
  fundamental_typed Γ e T (HT : Γ ⊢ₜ e : T) :
     Γ e : T.
    - iInduction HT as [] "IHT".
      + by iApply Sub_Refl.
      + by iApply Sub_Trans.
      + by pupd; iIntros "/= !> **".
      + by iApply Sub_Index_Incr.
      + by iApply Later_Sub.
      + by iApply Sub_Later.
      + by iApply Sub_Top.
      + by iApply Bot_Sub.
      + iApply Sel_Sub. by iApply fundamental_typed.
      + iApply Sub_Sel. by iApply fundamental_typed.
      + by iApply All_Sub_All.
      + by iApply Typ_Sub_Typ.
    - iInduction HT as [] "IHT".
      + by iApply T_All_Ex.
      + by iApply T_All_E.
      + by iApply T_All_I.
      + by iApply T_Nat_I.
      + by iApply T_Var.
      + iApply T_ISub ⇒ //.
        by iApply fundamental_subtype.
      + iApply T_Vty_abs_I ⇒ //;
        by iApply fundamental_subtype.
End Fundamental.

From D.pure_program_logic Require Import adequacy.
From D.iris_extra Require Import det_reduction.

Theorem adequacy Σ `{HdsubG : dsubSynG Σ} `{!SwapPropI Σ} e T :
  ( `(dsubSynG Σ) `(SwapPropI Σ), [] e : T)
  safe e.
  rewrite /safe; intros Htyp ?*.
  cut (adequate e (λ _, True)); first by intros [_ ?]; eauto.
  eapply (wp_adequacy (Σ := Σ) e) ⇒ /=.
  iIntros "!>". iPoseProof (Htyp _ _) as "#>Htyp".
  iSpecialize ("Htyp" $! ids with "[//]"); rewrite hsubst_id /=.
  iApply (wp_wand with "Htyp"); by iIntros.

#[global] Instance dsubSynG_empty : dsubSynG #[] := {}.

Corollary type_soundness e T :
  [] ⊢ₜ e : T
  safe e.
  intros; eapply (adequacy #[]) ⇒ //; iIntros.
  by iApply fundamental_typed.

From iris Require Import later_credits.
From iris.base_logic Require Import fancy_updates.
Section tests.
  Context `{!dsubSynG Σ} `{!invGS Σ}.

  Definition istpl i Γ T1 T2 : iProp Σ :=
    <PB> ∀ ρ v, G⟦Γ⟧ ρ → £ i -∗ ⟦T1⟧ ρ v → ⟦T2⟧ ρ v.

  [global] Arguments istpl /. global Instance istpl_persistent i Γ T1 T2 : Persistent (istpl i Γ T1 T2) := _.
  Notation "Γ ⊨ T1 <: i  T2" := (istpl i Γ T1 T2) (at level 74, T1, T2 at next level).

  Lemma lTyp_Sub_Typ Γ L1 L2 U1 U2 i j :
    Γ ⊨ L2 <: i  L1 -∗
    Γ ⊨ U1 <: j  U2 -∗
    Γ ⊨ TTMem L1 U1 <: i + j  TTMem L2 U2.
    pupd. iIntros "HT1 HT2 !> v Hg [Ci Cj] /=". unfold_interp. iDestruct 1 as (φ) "Hφl [HLφ #HφU]"; iExists φ.
    iSplit; first done.
    iSplitL "Ci"; iIntros "" (w).
    1: iSpecialize ("HT1" ! ρ w with "Hg Cj").
    (* iSpecialize ("HT1" *)

    (* setoid_rewrite mlaterN_impl. *)
    repeat iSplitL; first done;
      iIntros "" (w).
      iNext; iIntros "!> **".
    - iApply "HLφ" => //. by iApply "IHT".
    - iApply "IHT1". by iApply "HφU".