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 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 dot_semtypes sem_kind_dot.

Unset Program Cases.

Implicit Types (Σ : gFunctors)
         (v w : vl) (e : tm) (d : dm) (ds : dms) (p : path)
         (ρ : env) (l : label) (T : ty) (K : kind) (Γ : ctx).

CTyInterp is an (operational) typeclass, implemented by the gDOT logical relation.
Class CTyInterp Σ :=
  clty_interp : ty clty Σ.
#[global] Arguments clty_interp {_ _} !_ /.
Notation "C⟦ T ⟧" := (clty_interp T).

Class SfKindInterp Σ :=
  sf_kind_interp : kind sf_kind Σ.
#[global] Arguments sf_kind_interp {_ _} !_ /.
Notation "K⟦ K ⟧" := (sf_kind_interp K).

Define various notations on top of clty_interp.

Definition interpretation of types (Fig. 9).
Notation "Ds⟦ T ⟧" := (clty_dslty C T ).

(* We could inline pty_interp inside the V _  notation, but I suspect
the V _ ⟧* notation needs pty_interp to be a first-class function. *)

Definition pty_interp `{CTyInterp Σ} T : oltyO Σ := clty_olty C T .
#[global] Arguments pty_interp : simpl never.

Value interpretation of types (Fig. 9).

Notation "V⟦ T ⟧" := (pty_interp T).
Notation "V⟦ Γ ⟧*" := (fmap (M := list) pty_interp Γ).
Notation "E⟦ T ⟧" := (sE V T ).

Binding lemmas about gDOT logical relations.

Corollaries of CTyInterpLemmas.
Section logrel_binding_lemmas.
  Context `{Htil : CTyInterpLemmas Σ}.
  #[local] Set Default Proof Using "Type*".

  Lemma interp_subst_compose T {args} ρ1 ρ2 ρ3 :
    ρ1 >> ρ2 = ρ3 V T.|[ρ1] args ρ2 V T args ρ3.
  Proof. move⇒ <- v. exact: interp_subst_compose_ind. Qed.

  Lemma interp_weaken_one τ ρ {args} :
    V shift τ args ρ V τ args (stail ρ).
  Proof. apply interp_subst_compose. autosubst. Qed.

  Lemma interp_subst_one T v w ρ {args} :
    V T.|[v/] args ρ V T args (v.[ρ] .: ρ).
  Proof. apply interp_subst_compose. autosubst. Qed.

  Lemma interp_subst_ids T ρ {args} : V T args ρ V T.|[ρ] args ids.
  Proof. symmetry. apply interp_subst_compose. autosubst. Qed.

We have, unconditionally, that V⟦ T.| σ ⟧ args ρ = V⟦ T ⟧ args (∞ σ >> ρ).
But σ >> ρ and σ.|[ρ] are only equal for length σ entries.
  Lemma interp_commute_finsubst_cl T σ ρ v (HclT : nclosed T (length σ)) args :
    V T.|[ σ] args ρ v V T args (∞ σ.|[ρ]) v.
    rewrite interp_subst_compose_ind !(interp_subst_ids T) -hsubst_comp.
    (* *The* step requiring HclT. *)
    by rewrite (subst_compose HclT).

Substitution on semantic types commutes with the semantics.
  Lemma interp_commute_subst T σ : V T.|[σ] V T .|[σ].
  Proof. intros ???; apply interp_subst_compose_ind. Qed.

  Lemma interp_commute_weaken T n : V shiftN n T shiftN n V T .
  Proof. apply (interp_commute_subst _ (ren (+n))). Qed.

  Lemma interp_commute_weaken_one T : V shift T shift V T .
  Proof. apply interp_commute_weaken. Qed.

  Lemma interp_commute_subst_one T v : V T.|[ v /] V T .|[ v /].
  Proof. apply (interp_commute_subst _ (v .: ids)). Qed.
End logrel_binding_lemmas.

Notation cBot := (olty2clty oBot).
Notation cOr T1 T2 := (olty2clty $ oOr T1 T2).
Notation cLater T := (olty2clty $ oLater T).
Notation cPrim b := (olty2clty $ oPrim b).
Notation cAll T1 T2 := (olty2clty $ oAll T1 T2).
Notation cMu T := (olty2clty $ oMu T).
Notation cSel p l := (olty2clty $ oSel p l).
Notation cSing p := (olty2clty $ oSing p).
Notation cLam T := (olty2clty $ oLam T).
Notation cApp T p := (olty2clty $ oTApp T p).

Section log_rel.
  Context `{HdotG : !dlangG Σ}.
The logical relation on values is VT. We also define the logical relation on definitions DsT.
Both definitions follow the one on paper; concretely, they are defined through CT in instance dot_ty_interp.
Binding and closing substitutions:
Both relations interprets *open* types into predicates over values that are meant to be closed. So for instance VT T args ρ v applies substitution ρ to T, but not to v. We don't actually require that v be closed.
Semantic judgements must apply instead to open subjects (terms/value/paths), so they apply substitutions to their subject.
Additionally, both apply to *stamped* syntax, hence they only expect dtysem and not dtysyn for type member definitions.
Dispatch function defining V T and Ds T .
  (* Observe the naming pattern for semantic type constructors:
  replace T by o (for most constructors) or by c (for constructors producing
  cltys). *)

  Implicit Type (hrec : ty -d> hoEnvD Σ).
  Implicit Type (clrec : ty -d> cltyO Σ).

  Fixpoint kind_rec clrec (K : kind) {struct K} : sf_kind Σ :=
    let rec_ty : CTyInterp Σ := ty_rec clrec in
    let rec_kind : SfKindInterp Σ := kind_rec clrec in
    match K with
    | kintv L Usf_kintv V L V U
    | kpi S Ksf_kpi V S K K
   with ty_rec clrec (T : ty) {struct T} : clty Σ :=
    let rec_ty : CTyInterp Σ := ty_rec clrec in
    let rec_kind : SfKindInterp Σ := kind_rec clrec in
    let hrec : RecTyInterp Σ := λ T, clty_olty $ clrec T in
    match T with
    | kTTMem l KcTMemK l K K
    | TVMem l T'cVMem l V T'
    | TAnd T1 T2cAnd C T1 C T2
    | TTopcTop

    (* The remaining types are not useful for definition typing. *)
    | TBotolty2clty oBot
    | TOr T1 T2olty2clty $ oOr V T1 V T2
    | TLater Tolty2clty $ oLater V T
    | TPrim bolty2clty $ oPrim b
    | TAll T1 T2olty2clty $ oAll V T1 V T2
    | TMu Tolty2clty $ oMu V T
    | kTSel n p lolty2clty $ oSel p l
    | TSing polty2clty $ oSing p
    | TLam Tolty2clty $ oLam V T
    | TApp T polty2clty $ oTApp V T p

  Section interp_contractive.
    Context (ri1 ri2 : ty -d> cltyO Σ).

    Lemma interp_contractive_mut n (Hri : dist_later n ri1 ri2) :
      ( T, ty_rec ri1 T ≡{n}≡ ty_rec ri2 T)
      ( K, kind_rec ri1 K ≡{n}≡ kind_rec ri2 K).
      apply tp_kn_mut_ind; simpl; [done|done|..]; intros ×.
      all: rewrite /pty_interp/clty_interp/sf_kind_interp.
      all: intros; try by repeat (hof_eq_app || f_equiv).
      all: repeat (hof_eq_app || f_contractive || f_equiv).
      all: intros ????; apply clty_olty_ne, Hri.
  End interp_contractive.

  #[global] Instance kind_rec_contractive :
    Contractive (kind_rec : _ -d> kind -d> sf_kindO Σ).
  Proof. by move⇒ /= n ri1 ri2 Hri x; apply interp_contractive_mut. Qed.
  #[global] Instance kind_rec_ne :
    NonExpansive (kind_rec : _ -d> kind -d> sf_kindO Σ) := _.
  #[global] Instance kind_rec_proper :
    Proper1 (kind_rec : _ -d> kind -d> sf_kindO Σ) := _.

  #[global] Instance ty_rec_contractive :
    Contractive (ty_rec : _ -d> ty -d> cltyO Σ).
  Proof. by move⇒ /= n ri1 ri2 Hri x; apply interp_contractive_mut. Qed.

  #[global] Instance ty_interp : CTyInterp Σ := fixpoint ty_rec.
  #[global] Arguments clty_interp {_ _} _ : simpl never.
  #[global] Instance dot_kind_interp : SfKindInterp Σ := kind_rec ty_interp.
  #[global] Arguments sf_kind_interp {_ _} _ : simpl never.
  #[global] Instance dot_rec_ty_interp : RecTyInterp Σ := pty_interp.

  Lemma fixpoint_interp_eq1 T : C T ty_rec ty_interp T.
  Proof. apply: (fixpoint_unfold ty_rec). Qed.
  Lemma fixpoint_interp_eq : ty_interp ≡@{ty -d> _} ty_rec ty_interp.
  Proof. apply: fixpoint_unfold. Qed.

  Section kinterp_lemmas.
    #[local] Lemma trec_fold0 : ty_rec ty_interp ≡@{ty -d> cltyO Σ} ty_interp.
    Proof. apply symmetry, fixpoint_unfold. Qed.

    Lemma kinterp_kintv L U : K kintv L U sf_kintv V L V U .
    Proof. apply sf_kintv_proper; apply trec_fold0. Qed.
    Lemma kinterp_kpi S K : K kpi S K sf_kpi V S K K .
    Proof. apply sf_kpi_proper. apply trec_fold0. done. Qed.
  End kinterp_lemmas.

  Definition klr := (kinterp_kintv, kinterp_kpi).

  Section cinterp_lemmas.
    Ltac fast_work :=
      rewrite !fixpoint_interp_eq1 /= /pty_interp/clty_interp//=.
    Ltac fast_go := by fast_work.
    Ltac go := fast_work; by rewrite -fixpoint_unfold.

    Lemma cinterp_TTop : C TTop cTop.
    Proof. fast_go. Qed.
    Lemma cinterp_TBot : C TBot cBot.
    Proof. fast_go. Qed.

    Lemma cinterp_kTTMem l K1 : C kTTMem l K1 cTMemK l K K1 .
    Proof. fast_go. Qed.
    Lemma cinterp_kTSel n p l : C kTSel n p l cSel p l.
    Proof. fast_go. Qed.

    Lemma cinterp_TAnd T1 T2 : C TAnd T1 T2 cAnd C T1 C T2 .
    Proof. fast_go. Qed.
    Lemma cinterp_TOr T1 T2 : C TOr T1 T2 cOr V T1 V T2 .
    Proof. go. Qed.
    Lemma cinterp_TLater T1 : C TLater T1 cLater V T1 .
    Proof. go. Qed.
    Lemma cinterp_TAll T1 T2 : C TAll T1 T2 cAll V T1 V T2 .
    Proof. go. Qed.
    Lemma cinterp_TMu T1 : C TMu T1 cMu V T1 .
    Proof. go. Qed.
    Lemma cinterp_TVMem l T1 : C TVMem l T1 cVMem l V T1 .
    Proof. go. Qed.
    Lemma cinterp_TPrim b : C TPrim b cPrim b.
    Proof. fast_go. Qed.
    Lemma cinterp_TSing p : C TSing p cSing p.
    Proof. fast_go. Qed.
    Lemma cinterp_TLam T1 : C TLam T1 cLam V T1 .
    Proof. go. Qed.
    Lemma cinterp_TApp T1 p : C TApp T1 p cApp V T1 p.
    Proof. go. Qed.
  End cinterp_lemmas.

  Definition clr :=
    (cinterp_TTop, cinterp_TBot, cinterp_TAnd,
    cinterp_TOr, cinterp_TLater, cinterp_TAll, cinterp_TMu, cinterp_TVMem,
    cinterp_kTTMem, cinterp_kTSel, cinterp_TPrim, cinterp_TSing, cinterp_TLam, cinterp_TApp).

  Section interp_lemmas.
    Ltac go := rewrite /pty_interp clr //.

    Lemma interp_TTop : V TTop oTop.
    Proof. go. Qed.
    Lemma interp_TBot : V TBot oBot.
    Proof. go. Qed.
    Lemma interp_TAnd T1 T2 : V TAnd T1 T2 oAnd V T1 V T2 .
    Proof. go. Qed.
    Lemma interp_TOr T1 T2 : V TOr T1 T2 oOr V T1 V T2 .
    Proof. go. Qed.
    Lemma interp_TLater T1 : V TLater T1 oLater V T1 .
    Proof. go. Qed.
    Lemma interp_TAll T1 T2 : V TAll T1 T2 oAll V T1 V T2 .
    Proof. go. Qed.
    Lemma interp_TMu T1 : V TMu T1 oMu V T1 .
    Proof. go. Qed.
    Lemma interp_TVMem l T1 : V TVMem l T1 oVMem l V T1 .
    Proof. go. Qed.
    Lemma interp_kTTMem l K1 : V kTTMem l K1 oTMemK l K K1 .
    Proof. go. Qed.
    Lemma interp_kTSel n p l : V kTSel n p l oSel p l.
    Proof. go. Qed.
    Lemma interp_TPrim b : V TPrim b oPrim b.
    Proof. go. Qed.
    Lemma interp_TSing p : V TSing p oSing p.
    Proof. go. Qed.
    Lemma interp_TLam T1 : V TLam T1 oLam V T1 .
    Proof. go. Qed.
    Lemma interp_TApp T1 p : V TApp T1 p oTApp V T1 p.
    Proof. go. Qed.
  End interp_lemmas.

  Definition vlr :=
    (interp_TTop, interp_TBot, interp_TAnd,
    interp_TOr, interp_TLater, interp_TAll, interp_TMu, interp_TVMem,
    interp_kTTMem, interp_kTSel, interp_TPrim, interp_TSing, interp_TLam, interp_TApp).

Binding lemmas for V T and K T .
  Lemma mut_interp_subst_compose_ind :
    ( T args ρ1 ρ2 v,
      V T.|[ρ1] args ρ2 v ⊣⊢ V T args (ρ1 >> ρ2) v)
    ( K ρ1 ρ2 τ1 τ2,
      K K.|[ρ1] ρ2 τ1 τ2 ⊣⊢ K K (ρ1 >> ρ2) τ1 τ2).
    apply tp_kn_mut_ind; intros;
      rewrite ?(vlr, klr) /= /sr_kintv /subtype_lty.
    all: properness.
    all: rewrite ?scons_up_swap ?hsubst_comp; trivial.
    all: try by apply path_wp_proper ⇒ ?.

  #[global] Instance pinterp_lemmas : CTyInterpLemmas Σ.
  Proof. split. apply mut_interp_subst_compose_ind. Qed.

  Lemma kind_interp_subst_compose_ind K ρ1 ρ2 τ1 τ2 :
      K K.|[ρ1] ρ2 τ1 τ2 ⊣⊢ K K (ρ1 >> ρ2) τ1 τ2.
  Proof. apply mut_interp_subst_compose_ind. Qed.

  Definition idtp Γ T l d := sdtp l d VΓ⟧* CT.
  Definition idstp Γ T ds := sdstp ds VΓ⟧* CT.
  Definition ietp Γ T e := setp e VΓ⟧* VT.
  Definition istpd i Γ T1 T2 := sstpd i VΓ⟧* VT1 VT2.
  Definition iptp Γ T p i := sptp p i VΓ⟧* VT.
End log_rel.

Notation "G⟦ Γ ⟧ ρ" := (sG V Γ ⟧* ⟧* ρ) (at level 10).

Single-definition typing
Notation "Γ ⊨ { l := d } : T" := (idtp Γ T l d) (at level 74, d, l, T at next level).
Multi-definition typing
Notation "Γ ⊨ds ds : T" := (idstp Γ T ds) (at level 74, ds, T at next level).
Expression typing
Notation "Γ ⊨ e : T" := (ietp Γ T e) (at level 74, e, T at next level).
Notation "Γ ⊨p p : T , i" := (iptp Γ T p i) (at level 74, p, T, i at next level).
Notation "Γ ⊨ T1 <:[ i ] T2" := (istpd i Γ T1 T2) (at level 74, T1, T2 at next level).

Show these typing judgments are equivalent to what we present in the paper.

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

  Lemma idstp_eq Γ T ds : Γ ds ds : T ⊣⊢
    <PB> (wf_ds ds ρ, path_includes (pv (ids 0)) ρ ds GΓ ρ DsT ρ ds.|[ρ]).
  Proof. reflexivity. Qed.

  Lemma ietp_eq Γ e T :
    Γ e : T ⊣⊢ <PB> ρ, GΓ ρ ET ρ (e.|[ρ]).
  Proof. reflexivity. Qed.

  Lemma istpd_eq Γ T1 i T2 :
    Γ T1 <:[i] T2 ⊣⊢
    <PB> ρ v, GΓ ρ ▷^i (VT1 anil ρ v VT2 anil ρ v).
  Proof. apply sstpd_eq. Qed.

  Lemma iptp_eq Γ p T i :
    Γ p p : T , i ⊣⊢
    <PB> ρ, GΓ ρ
      ▷^i path_wp (p.|[ρ]) (λ v, VT anil ρ v).
  Proof. reflexivity. Qed.
End judgment_definitions.

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

  Lemma iterate_TLater_oLater i (T : ty) :
    Viterate TLater i T oLaterN i VT.
  Proof. elim: i ⇒ [//|i IHi] ???. by rewrite !iterate_S vlr /= IHi. Qed.

End misc_lemmas.

Tactic to reduce the syntactic judgments and logical relation. To use when proving syntactic typing lemmas, e.g. Stp_Top over sStp_Top, or Mu_Stp over sMu_Stp. Due to the fix to issue #365(https://github.com/Blaisorblade/dot-iris/issues/365), this must now use non-definitional equalities.
Definition lr := (@fmap_cons, @iterate_TLater_oLater, @vlr, @klr, @clr).
Ltac rw := rewrite /ietp /idstp /idtp /iptp /istpd ?lr.

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

  Let fundamental_ty_path_repl_def p q T1 T2 := V T1 ¬sTpP[ p := q ]* V T2 .
  Let fundamental_kn_path_repl_def p q K1 K2 := K K1 ¬sKpP[ p := q ]* K K2 .

  #[local] Lemma fundamental_ty_kn_mut_path_repl p q :
    ( T1 T2 (Hrew : T1 ¬Tp[ p := q ] T2), fundamental_ty_path_repl_def p q T1 T2)
    ( K1 K2 (Hrew : K1 ¬Kp[ p := q ] K2), fundamental_kn_path_repl_def p q K1 K2).
    apply ty_kind_path_repl_mut_ind;
    rewrite /fundamental_ty_path_repl_def /fundamental_kn_path_repl_def
      /sem_ty_path_repl /sem_kind_path_repl; intros.
      all: rewrite ?vlr ?klr /=.
      all: rewrite /sr_kintv /subtype_lty/=; intros;
      try match goal with
      | H : context [equiv _ _] |- _rename H into IHHrew
    all: eauto 2.
    all: by [ apply: path_replacement_equiv
            | apply: rewrite_path_path_repl
            | apply IHHrew; rewrite ?hsubst_comp
            | apply: path_wp_proper ⇒ ?; exact: IHHrew ].
  Lemma fundamental_ty_path_repl {p q T1 T2}
    (Hrew : T1 ¬Tp[ p := q ] T2) :
    V T1 ¬sTpP[ p := q ]* V T2 .
  Proof. by apply fundamental_ty_kn_mut_path_repl. Qed.
  Lemma fundamental_kn_path_repl {p q K1 K2}
    (Hrew : K1 ¬Kp[ p := q ] K2) :
    K K1 ¬sKpP[ p := q ]* K K2 .
  Proof. by apply fundamental_ty_kn_mut_path_repl. Qed.

  Lemma fundamental_ty_path_repl_rtc {p q T1 T2}
    (Hrew : T1 ¬Tp[ p := q ]* T2) :
    V T1 ¬sTpP[ p := q ]* V T2 .
    moveargs ρ v Hal. elim: Hrew ⇒ [//|T {}T1 {}T2 Hr _ <-].
    apply (fundamental_ty_path_repl Hr), Hal.

  Lemma rewrite_ty_path_repl_rtc {p q T1 T2 args ρ}
    (Hrepl : T1 ¬Tp[ p := q ]* T2)
    (Hal : alias_paths p.|[ρ] q.|[ρ]) : (* p : q.type *)
    V T1 args ρ V T2 args ρ.
  Proof. intros v. apply: (fundamental_ty_path_repl_rtc Hrepl) Hal. Qed.

Prove that semantic and syntactic substitution of paths in types agree. However, this proof only works for paths that normalize; that's because V T .sTp[ p /] args ρ v asserts that p terminates, while V T' args ρ v need not assert that (say, because T' is TOr TTop (TSel p l).
  Lemma sem_psubst_one_eq {T T' args p v ρ}
    (Hrepl : T .Tp[ p /]~ T')
    (Hal : alias_paths p.|[ρ] (pv v)) :
    V T' args ρ V T .sTp[ p /] args ρ.
    rewrite -(interp_weaken_one T' (v .: ρ)) ⇒ w.
    rewrite -(rewrite_ty_path_repl_rtc Hrepl) /=.
    by rewrite (alias_paths_elim_eq _ Hal) path_wp_pv_eq.
    by rewrite hsubst_comp ren_scons /= alias_paths_symm.

  Lemma psubst_one_repl {T T' args p v w ρ}
    (Hr : T .Tp[ p /]~ T') (Hal : alias_paths p.|[ρ] (pv v)) :
    V T args (v .: ρ) w V T' args ρ w.
  Proof. by rewrite (sem_psubst_one_eq Hr Hal) (sem_psubst_one_repl Hal). Qed.
End path_repl_lemmas.

Backward compatibility.
Notation "⟦ T ⟧" := (oClose V T ).

Import dlang_adequacy.

Adequacy of normalization for gDOT paths.
Lemma ipwp_gs_adequacy Σ `{HdlangG : !dlangG Σ} `{!SwapPropI Σ} {p T i}
  (Hwp : `(Hdlang : !dlangG Σ) `(!SwapPropI Σ), [] p p : T , i) :
  terminates (path2tm p).
  apply (soundness (M := iResUR Σ) _ i).
  apply (bupd_plain_soundness _).
  iApply ipwp_terminates.
  iApply Hwp.