Logical relation and semantic judgments.

From D Require Export iris_prelude proper lty lr_syn_aux.
From D Require Import iris_extra.det_reduction.
From D Require Export iris_extra.proofmode_pupd.
From D Require Import swap_later_impl.
From D.Dot Require Import syn path_repl.
From D.Dot Require Export dlang_inst path_wp.
From D.pure_program_logic Require Import weakestpre.

From D.Dot Require Export dot_lty sem_kind_dot.

Unset Program Cases.

Implicit Types (Σ : gFunctors)
         (v w : vl) (e : tm) (d : dm) (ds : dms) (p : path)
         (ρ : env) (l : label).

Define fully semantic judgments. They accept arbitrary semantic types.

Section judgments.
  Context {Σ}.
  Implicit Types (τ : oltyO Σ).

Expression typing
  Definition setp `{!dlangG Σ} e Γ τ : iProp Σ :=
    <PB> ρ, sGΓ⟧* ρ sE τ ρ (e.|[ρ]).
  #[global] Arguments setp : simpl never.

Delayed subtyping.
  Definition sstpd `{!dlangG Σ} i Γ τ1 τ2 : iProp Σ :=
    <PB> ρ,
      sGΓ⟧*ρ ▷^i (oClose τ1 ρ oClose τ2 ρ).
  #[global] Arguments sstpd : simpl never.

Multi-definition typing
  Definition sdstp `{!dlangG Σ} ds Γ (T : clty Σ) : iProp Σ :=
    <PB> (wf_ds ds ρ, path_includes (pv (ids 0)) ρ ds sGΓ⟧* ρ T ρ ds.|[ρ]).
  #[global] Arguments sdstp : simpl never.

Definition typing
  Definition sdtp `{!dlangG Σ} l d Γ (φ : clty Σ) : iProp Σ := sdstp [(l, d)] Γ φ.
  #[global] Arguments sdtp : simpl never.

Path typing
  Definition sptp `{!dlangG Σ} p i Γ τ : iProp Σ :=
    <PB> ρ, sGΓ⟧* ρ
      ▷^i path_wp p.|[ρ] (oClose τ ρ).
  #[global] Arguments sptp : simpl never.

  Section persistence.
    Context `{!dlangG Σ}.

    Avoid auto-dropping box (and unfolding) when introducing judgments persistently.

    We use cost 0 to take precedence over Iris.

    The instance for sdtp overlaps with sdstp and must take priority; since
    there's no cost lower than 0, the instance for sdtp comes after the one for sdstp.

    #[global] Instance sdstp_into_persistent Γ Tds ds : IntoPersistent' (sdstp ds Γ Tds) | 0 := _.
    #[global] Instance sdtp_into_persistent Γ Td l d : IntoPersistent' (sdtp l d Γ Td) | 0 := _.
    #[global] Instance setp_into_persistent Γ T e : IntoPersistent' (setp e Γ T) | 0 := _.
    #[global] Instance sstpd_into_persistent Γ T1 T2 i : IntoPersistent' (sstpd i Γ T1 T2) | 0 := _.
    #[global] Instance sptp_into_persistent Γ T p i : IntoPersistent' (sptp p i Γ T) | 0 := _.
  End persistence.
End judgments.

Expression typing
Notation "Γ s⊨ e : τ" := (setp e Γ τ) (at level 74, e, τ at next level).
Delayed subtyping.
Notation "Γ s⊨ T1 <:[ i ] T2" := (sstpd i Γ T1 T2) (at level 74, T1, T2 at next level).
Single-definition typing
Notation "Γ s⊨ { l := d } : T" := (sdtp l d Γ T) (at level 64, d, l, T at next level).
Multi-definition typing
Notation "Γ s⊨ds ds : T" := (sdstp ds Γ T) (at level 74, ds, T at next level).
Path typing
Notation "Γ s⊨p p : τ , i" := (sptp p i Γ τ) (at level 74, p, τ, i at next level).

Section JudgEqs.
  Context `{HdotG : !dlangG Σ}.

  Lemma sstpd_eq_1 Γ T1 i T2 :
    Γ s T1 <:[i] T2 ⊣⊢
    <PB> ρ, sGΓ⟧* ρ v, ▷^i (T1 anil ρ v T2 anil ρ v).
    rewrite /sstpd /subtype_lty; repeat f_equiv.
    by rewrite laterN_forall.

  Lemma sstpd_eq Γ T1 i T2 :
    Γ s T1 <:[i] T2 ⊣⊢
    <PB> ρ v, sGΓ⟧* ρ ▷^i (T1 anil ρ v T2 anil ρ v).
  Proof. rewrite sstpd_eq_1; properness. apply: forall_swap_impl. Qed.
End JudgEqs.

gDOT semantic types.

Definition vl_sel `{!dlangG Σ} vp l args v `{!RecTyInterp Σ} : iProp Σ :=
   d ψ, vp ,, l d d ψ packHoLtyO ψ args v.

Definition oSel `{!dlangG Σ} p l `{!RecTyInterp Σ} : oltyO Σ :=
  Olty (λI args ρ v, path_wp p.|[ρ] (λ vp, vl_sel vp l args v)).

Section sel_types_lemmas.
  Context `{HdotG : !dlangG Σ}.

  #[global] Instance vl_sel_contractive vp l args v : Contractive (@vl_sel _ _ vp l args v).
  Proof. solve_contractive_ho. Qed.
  (* Deducible. *)
  Definition vl_sel_ne vp l args v : NonExpansive (@vl_sel _ _ vp l args v) :=
    contractive_ne _.
  #[global] Instance vl_sel_proper vp l args v : Proper1 (@vl_sel _ _ vp l args v) :=
    ne_proper _.

  #[global] Instance oSel_contractive p l : Contractive (@oSel _ _ p l).
    moven ri1 ri2 Hri args ρ v /=.
  Definition oSel_ne p l : NonExpansive (@oSel _ _ p l) :=
    contractive_ne _.
  #[global] Instance oSel_proper p l : Proper1 (@oSel _ _ p l) :=
    ne_proper _.
End sel_types_lemmas.

Section sem_types.
  Context `{HdotG : !dlangG Σ}.
  Implicit Types (τ : oltyO Σ).

D { a : τ } .
  Definition oDVMem τ : dltyO Σ := Dlty (λI ρ d,
     pmem, d = dpt pmem path_wp pmem (oClose τ ρ)).
  #[global] Instance oDVMem_ne : NonExpansive oDVMem.
  Proof. solve_proper_ho. Qed.
  #[global] Instance oDVMem_proper : Proper1 oDVMem :=
    ne_proper _.

  Lemma oDVMem_eq T ρ p :
    oDVMem T ρ (dpt p) path_wp p (oClose T ρ).
  Proof. simpl; iSplit; last by eauto. by iDestruct 1 as (pmem [= ->]) "$". Qed.

Define cVMem by lifting oDVMem to cltys.
Ds { l : τ } and V { l : τ } .
  Definition cVMem l τ : clty Σ := dty2clty l (oDVMem τ).
  #[global] Instance cVMem_ne l : NonExpansive (cVMem l).
  Proof. solve_proper. Qed.
  #[global] Instance cVMem_proper l : Proper1 (cVMem l) :=
    ne_proper _.

  Lemma cVMem_eq l T d ρ :
    cVMem l T ρ [(l, d)] ⊣⊢ oDVMem T ρ d.
  Proof. apply dty2clty_singleton. Qed.

V p.type .
  Definition oSing `{!dlangG Σ} p : olty Σ := olty0 (λI ρ v, alias_paths p.|[ρ] (pv v)).

V x: τ1. τ2 .
  (* Function types; this definition is contractive (similarly to what's
     useful for equi-recursive types). *)

  Definition oAll τ1 τ2 := olty0
    (λI ρ v,
    ( t, v = vabs t
      w, τ1 anil ρ w sE τ2 (w .: ρ) t.|[w/])).

  #[global] Instance oAll_ne : NonExpansive2 oAll.
  Proof. solve_proper_ho. Qed.

  #[global] Instance oAll_proper : Proper2 oAll :=
    ne_proper_2 _.

Semantics of primitive types.
  Definition oPrim b : olty Σ := olty0 (λI ρ v, pure_interp_prim b v).

End sem_types.

#[global] Instance : Params (@oAll) 2 := {}.

Notation oInt := (oPrim tint).
Notation oBool := (oPrim tbool).

Semantics of type members in the ICFP'20 paper: Ds { l >: τ1 <: τ2 } and V { l >: τ1 <: τ2 } .
Notation cTMemL l L U := (cTMem l (oLater L) (oLater U)).
Notation oTMemL l L U := (clty_olty (cTMemL l L U)).
Notation oVMem l τ := (clty_olty (cVMem l τ)).

Section misc_lemmas.
  Context `{HdotG : !dlangG Σ} `{!RecTyInterp Σ}.
  Implicit TypesL T U : olty Σ).

  Lemma oSel_pv w l args ρ v :
    oSel (pv w) l args ρ v ⊣⊢
       d ψ, w.[ρ] ,, l d d ψ ψ args v.
  Proof. by rewrite /= path_wp_pv_eq. Qed.

  Lemma oVMem_eq l T anil ρ v :
    oVMem l T anil ρ v ⊣⊢
     pmem, v ,, l dpt pmem path_wp pmem (oClose T ρ).
    etrans; [apply bi_exist_nested_swap|]; apply bi.exist_properp.
    rewrite and2_exist_r.
    apply bi.and_proper, reflexivity; iIntros "!% /="; naive_solver.

Core lemmas about type selections and bounds.
  Lemma vl_sel_ub w l L U ρ v :
    vl_sel w l anil v -∗
    oTMem l L U anil ρ w -∗
    U anil ρ v.
    rewrite oTMem_unfold.
    iIntros "Hφ"; iDestruct 1 as (d1 Hl1 φ1) "(Hdφ1 & _ & HφU)".
    iApply "HφU".
    iDestruct "Hφ" as (d2 φ2 Hl2) "[Hdφ2 Hφ2v]".
    objLookupDet; iDestruct (dm_to_type_agree anil v with "Hdφ2 Hdφ1") as "Hag".
    iNext. by iRewrite "Hag" in "Hφ2v".

  Lemma vl_sel_lb w l L U ρ v :
    L anil ρ v -∗
    oTMem l L U anil ρ w -∗
    vl_sel w l anil v.
    rewrite oTMem_unfold.
    iIntros "HL"; iDestruct 1 as (d Hl φ) "[Hdφ [HLφ _]]".
    iExists d, φ; iFrame (Hl) "Hdφ". iApply ("HLφ" with "HL").

  Lemma lift_sub_dty2cltyN i (T1 T2 : dlty Σ) l ρ :
    ( d, ▷^i T1 ρ d -∗ ▷^i T2 ρ d)
    oLaterN i (lift_dty_vl l T1) anil ρ oLaterN i ((lift_dty_vl l T2)) anil ρ.
    iIntros "Hsub %v". iDestruct 1 as (d) "[Hl #H1]"; iExists d; iFrame "Hl".
    by iApply ("Hsub" with "H1").

  Lemma lift_sub_dty2clty (T1 T2 : dlty Σ) l ρ :
    ( d, T1 ρ d -∗ T2 ρ d)
    lift_dty_vl l T1 anil ρ lift_dty_vl l T2 anil ρ.
  Proof. apply (lift_sub_dty2cltyN 0). Qed.

  Lemma oDTMem_respects_sub L1 L2 U1 U2 ρ d :
     (L2 anil ρ L1 anil ρ) -∗
     (U1 anil ρ U2 anil ρ) -∗
    oDTMem L1 U1 ρ d -∗ oDTMem L2 U2 ρ d.
    rewrite !oDTMem_unfold.
    iIntros "#HsubL #HsubU"; iDestruct 1 as (φ) "#(Hφl & #HLφ & #HφU)".
    rewrite /= /dot_intv_type_pred.
    iExists φ; iSplit; first done; iModIntro; iSplit; iIntros "%w #Hw".
    - iApply ("HLφ" with "(HsubL Hw)").
    - iApply ("HsubU" with "(HφU Hw)").

  Lemma oTMem_respects_sub L1 L2 U1 U2 ρ l :
     (L2 anil ρ L1 anil ρ) -∗
     (U1 anil ρ U2 anil ρ) -∗
    oTMem l L1 U1 anil ρ oTMem l L2 U2 anil ρ.
    rewrite -lift_sub_dty2clty; iIntros "#HsubL #HsubU %d".
    iApply (oDTMem_respects_sub with "HsubL HsubU").

  Lemma oDVMem_respects_subN i T1 T2 ρ d :
    oClose (oLaterN i T1) ρ oClose (oLaterN i T2) ρ
    ▷^i oDVMem T1 ρ d -∗ ▷^i oDVMem T2 ρ d.
    iIntros "Hsub"; iDestruct 1 as (pmem) "[Heq HT1]"; iExists pmem; iFrame "Heq".
    iApply (path_wp_wand_laterN with "HT1"); iIntros "%v HT1".
    by iApply ("Hsub" with "HT1").
  Definition oDVMem_respects_sub := oDVMem_respects_subN 0.

  Lemma oVMem_respects_subN i T1 T2 l ρ :
    oClose (oLaterN i T1) ρ oClose (oLaterN i T2) ρ
    oLaterN i (oVMem l T1) anil ρ oLaterN i (oVMem l T2) anil ρ.
    rewrite -lift_sub_dty2cltyN. iIntros "Hsub %d".
    iApply (oDVMem_respects_subN with "Hsub").
  Definition oVMem_respects_sub := oVMem_respects_subN 0.

  Lemma sdtp_eq (Γ : sCtx Σ) (T : clty Σ) l d :
    Γ s { l := d } : T ⊣⊢
      <PB> ρ, path_includes (pv (ids 0)) ρ [(l, d)] sGΓ⟧* ρ T ρ [(l, d.|[ρ])].
    rewrite /sdtp /sdstp pure_True ?(left_id _ bi_and);
      by [> | exact: NoDup_singleton].

  Lemma sdtp_eq' (Γ : sCtx Σ) (T : dlty Σ) l d :
    Γ s { l := d } : dty2clty l T ⊣⊢
      <PB> ρ, path_includes (pv (ids 0)) ρ [(l, d)] sGΓ⟧* ρ T ρ d.|[ρ].
  Proof. by rewrite sdtp_eq; properness; last apply dty2clty_singleton. Qed.

  Lemma ipwp_terminates {p T i} :
    [] sp p : T , i |==> ▷^i terminates (path2tm p) .
    iIntros "#H".
    rewrite /sptp.
    iDestruct "H" as "#>#H".
    iSpecialize ("H" $! ids with "[//]"); rewrite hsubst_id.
    iApply (path_wp_terminates with "H").

This typing lemma is here to be usable in proof of other lemmas.
  Lemma sT_Path {Γ τ p} :
    Γ sp p : τ, 0 -∗ Γ s path2tm p : τ.
    pupd; iIntros "#Hep !> %ρ #Hg /=". rewrite path2tm_subst.
    by iApply (path_wp_to_wp with "(Hep Hg)").
End misc_lemmas.

Section path_repl_lemmas.
  Context `{!dlangG Σ}.
  Implicit Types (φ : vl -d> iPropO Σ).

Beware: we can do path replacement *before* substitution, even tho substitution and path replacement don't commute nicely.
As a special case, we get the less surprising: alias_paths_subst p r ids path_wp q φ path_wp (q .p[p := r]) φ.
But we do need the general form.
  Lemma path_replacement_equiv {p q ρ} p1 p2 φ :
    p1 ¬pp[ p := q ] p2
    alias_paths p.|[ρ] q.|[ρ]
    path_wp p1.|[ρ] φ path_wp p2.|[ρ] φ.
    moveHrepl; elim: Hrepl φ ⇒ {p1 p2} [| p1' p2' l Hrepl IHrepl] φ /=.
    exact: alias_paths_elim_eq.
    rewrite !path_wp_pself_eq /= ⇒ Hal.
    properness ⇒ //. exact: IHrepl.

  Lemma rewrite_path_path_repl {p q p1 p2 ρ v} :
    p1 ¬pp[ p := q ] p2
    alias_paths p.|[ρ] q.|[ρ] (* p : q.type *)
    alias_paths p1.|[ρ] (pv v) ⊣⊢@{iPropI Σ} alias_paths p2.|[ρ] (pv v).
    (* alias_paths p1.|ρ (pv v) ↔ alias_paths p2.|ρ (pv v). *)
  Proof using Type×.
    intros Hrew Hal.
    rewrite !alias_paths_pv_eq_1 -!path_wp_pureable.
    exact: path_replacement_equiv.
End path_repl_lemmas.

Proper instances.
This instance doesn't allow setoid rewriting in the function argument to iterate. That's appropriate for this project.
#[global] Instance : Params (@iterate) 3 := {}.
#[global] Instance iterate_proper {n} {A : ofe} (f : A A) :
  Proper (equiv ==> equiv) f
  Proper (equiv ==> equiv) (iterate f n).
  elim: n ⇒ [|n IHn] Hp x y Heq; rewrite ?(iterate_0, iterate_S) //.
  f_equiv. exact: IHn.

Section Propers.
  Context `{HdotG : !dlangG Σ}.

  #[global] Instance sstpd_proper i : Proper3 (sstpd i).
    (* intros ?? HG ?? H1 ?? H2; rewrite /sstpd /subtype_lty;
    properness; by rewrite HG|apply H1|apply H2. *)

  #[global] Instance : Params (@sstpd) 3 := {}.

  #[global] Instance setp_proper e : Proper2 (setp e).
    (* intros ?? HG ?? HT ???; simplify_eq/=. by properness; rewrite HG|apply HT. *)
  #[global] Instance : Params (@setp) 3 := {}.

  #[global] Instance sdstp_proper ds : Proper2 (sdstp ds).
    rewrite /sdstp ⇒ ??? [?? _] [?? _] [/= ??]; properness; by f_equiv.
  #[global] Instance : Params (@sdstp) 3 := {}.

  #[global] Instance sdtp_proper l d : Proper2 (sdtp l d) := _.
  #[global] Instance : Params (@sdtp) 4 := {}.

  #[global] Instance sptp_proper p i : Proper2 (sptp p i).
  Proof. solve_proper_ho. Qed.
  #[global] Instance : Params (@sptp) 4 := {}.
End Propers.