RSC.sysfCorrespondence

(* (c) 2018, Jonas Kaiser *)

Correspondence Result for System F

We ...

Require Import Omega List.
From Autosubst Require Export Autosubst.

From RSC Require Import Decidable lib vrel pts ARS.

Set Implicit Arguments.

We generate the System F FPTS


Reserved Notation "∗".
Reserved Notation "⬜".

Module SA.

  Module F_spec <: PTS_sig <: FPTS_sig.

    (* the inductive types cannot yet be used to directly instantitate signature parameters *)
    Inductive level : Type := Prp | Typ.

    Inductive ax : level level Prop := ax_base : ax Prp Typ.
    Inductive rl : level level level Prop := rl1 : rl Prp Prp Prp | rel2 : rl Typ Prp Prp.

    Definition S := level.
    Definition A := ax.
    Definition R := rl.

    Instance decide_eq_srt ( : S) : Dec ( = ). derive. Defined.

    (* now we have a PTS signature, the remainder is for functionality *)

    Lemma A_func : A A = .
    Proof. intros . inv . now inv . Qed.

    Lemma R_func : R R = .
    Proof. intros . inv ; now inv . Qed.

  End F_spec.

  Include FPTS (F_spec).

  Notation "∗" := (Srt Prp).
  Notation "⬜" := (Srt Typ).

  (* special results about this particular PTS ... *)

  Lemma typ_no_type a : hastype a.
  Proof. apply srt_no_type. intros s H. inv H. Qed.

  Lemma prp_prp_contra : hastype .
  Proof. intros H. apply hastype_srt_srt in H. inv H. Qed.

  Lemma typ_degeneracy a : valid hastype a a = .
  Proof.
    intros V H. inv H.
    - now inv .
    - exfalso. destruct (typ_no_type ).
    - exfalso. inv .
    - exfalso. destruct (hastype_beta_ty V ) as [_ [s [_ [_ Hd]]]].
      rewrite in Hd. destruct (typ_no_type Hd).
    - exfalso. destruct (typ_no_type ).
  Qed.


  (* For this PTS specification, we can show that sorts are only inhabited by normal terms.
     This allows us to later show that all instances of the conversion rule are effectively
     build with a reflexiv conversion, and can thus be discarded without loss from derivations.
   *)

  Lemma types_normal a s : valid hastype a (Srt s) normal a.
  Proof. intros V H. eapply srt_normal; eauto. intros _ _ _ s' []; intros C; inv C. Qed. (* new: semicolon/branching *)

  Lemma hastype_normal_ty a b : valid hastype a b normal b.
  Proof.
    intros V H. apply (propagation V) in H as [s [E|H]]; [subst|].
    - apply normal_srt.
    - apply (types_normal V H).
  Qed.


  (* a useful separate induction principles for PTS "types", i.e. terms in ∗, and "terms",
     following the distinctions of the stratified presentation. The principles heavily exploit
     the known PTS specification.
   *)

  Lemma type_induction (Q : list tm tm Prop) :
    ( n, valid atnd n Q (Var n))
    ( a b, valid hastype a Q a hastype (a :: ) b Q (a :: ) b Q (Prod a b))
    ( b, valid hastype ( :: ) b Q ( :: ) b Q (Prod b)) (* new *)
     a, valid hastype a Q a.
  Proof.
    intros Qvar Qimp Qall. intros a V H. remember as b. rewrite Heqb in Qvar, Qimp, Qall.
    revert V Heqb. induction H; intros V E.
      - exfalso. inv E. inv H.
      - subst. now apply Qvar.
      - destruct H.
        + specialize ( V (eq_refl _)). specialize ( (valid_ext V) (eq_refl _)). now apply Qimp.
        + clear E. specialize ( (valid_ext V) (eq_refl _)). apply (typ_degeneracy V) in . subst. now apply Qall. (* new *)
      - exfalso. subst. destruct (hastype_beta_ty V H ) as [ [ [ [HR Hd]]]].
        rewrite E in Hd. apply hastype_srt_srt in Hd. inv Hd. inv HR.
      - exfalso. inv E.
      - subst. apply (hastype_normal_ty V) in H. apply (bc_srt_normal_r H) in . auto.
  Qed.


  Lemma term_induction (Q : list tm tm tm Prop) :
    ( n a, valid atnd n a hastype a Q (Var n) a)
    ( a b c d d', valid hastype a (Prod c d) hastype c hastype (c :: ) d Q a (Prod c d) hastype b c Q b c d' = d.[b/] Q (App a b) d')
    ( a b c, valid hastype a hastype (a :: ) c hastype (a :: ) b c Q (a :: ) b c Q (Lam a b) (Prod a c))
    ( a b d d', valid hastype a (Prod d) hastype ( :: ) d Q a (Prod d) hastype b d' = d.[b/] Q (App a b) d') (* new *)
    ( b c, valid hastype ( :: ) c hastype ( :: ) b c Q ( :: ) b c Q (Lam b) (Prod c)) (* new *)
    ( a b, valid hastype b hastype a b Q a b).
  Proof.
    intros Qvar Qapp Qlam Qtyapp Qtylam. intros a b V HT H.
    revert V HT. induction H; intros V HT.
    - exfalso. apply hastype_srt_srt in HT. inv HT.
    - now apply Qvar.
    - exfalso. apply hastype_srt_srt in HT. inv HT.
    - destruct (hastype_prod_inv V H) as [_ [_ [_ [[] [Hc [Hd HP]]]]]].
      + eapply Qapp; eauto.
      + (* new *) apply (typ_degeneracy V) in Hc. subst c. eapply Qtyapp; eauto.
    - destruct H.
      + apply Qlam; eauto using valid.
      + (* new *) apply (typ_degeneracy V) in . subst a.
        assert (hastype ) by (constructor; constructor).
        apply Qtylam; eauto using valid.
    - apply (hastype_normal_ty V) in H. apply (types_normal V) in .
      apply normal_bc in ; trivial. subst. auto.
  Qed.


  Lemma hastype_type_strengthen a b :
    valid (a :: ) hastype (a :: ) b.[ren (+1)] hastype b .
  Proof. intros. change with .[ren (+1)] in . now apply hastype_strengthen in . Qed.

Internalising contexts


  Fixpoint intern ( : list tm) (a b : tm) : (tm * tm) :=
    match with
    | nil (a,b)
    | c :: intern (Lam c a) (Prod c b)
    end.

  Lemma intern_correct a b c d: valid intern a b = (c,d) (hastype b hastype a b hastype nil d hastype nil c d).
  Proof.
    intros H. revert a b c d. induction H; intros; simpl in *.
    - inv H. firstorder.
    - apply IHvalid in . eapply iff_trans; eauto. split; intros [Jty Jtm].
      + split; econstructor; eauto; destruct s; constructor.
      + split.
        * now apply (hastype_prod_inv ) in Jtm as [_ [_ [_ [[] [_ [K _]]]]]].
        * apply strip_prod in Jty as [_ [sb [_ [_ [_ [ _]]]]]].
          apply strip_lam in Jtm as [_ [_ [_ [b' [_ [_ [_ [ [_ C]]]]]]]]].
          apply bc_prod in C as [_ C]. eapply hastype_conv; eauto. now apply convS.
  Qed.


  Include F_spec.
  (* Include M. *)

End SA.

Notation "∗" := (SA.Srt SA.Prp).
Notation "⬜" := (SA.Srt SA.Typ).

Require sysf.

Module SB.

  Include sysf.

End SB.

Correspondence

Relating Types


Reserved Notation "Theta |- A ∼ a" (at level 70, no associativity).
Inductive tyrel ( : vrel) : SB.ty SA.tm Prop :=
| tyrel_var n m : n m SB.TyVar n SA.Var m
| tyrel_imp A B a b : A a vRS B b SB.Imp A B SA.Prod a b
| tyrel_all A a : vEXT A a SB.All A SA.Prod a (* new *)
where "Theta |- A ∼ a" := (tyrel A a).

Functionality and Injectivity of tyrel
Lemma tyrel_func : vr_func rel_func (tyrel ).
Proof.
  intros Rf A H. revert . induction H; intros a' J; inv J.
  - now rewrite (Rf _ _ _ H ).
  - f_equal; eauto using vr_func_rs.
  - f_equal; eauto using vr_func_ext. (* new *)
Qed.


(* note: diff wrt. stlc: two F constructor map to prod, hence four cases ... *)
Lemma tyrel_inj : vr_inj rel_inj (tyrel ).
Proof.
  intros Ri a H. revert . induction H; intros A' J; inv J.
  - now rewrite (Ri _ _ _ H ).
  - f_equal; eauto using vr_inj_rs.
  - (* new *) exfalso. inv H.
  - (* new *) exfalso. inv .
  - (* new *) f_equal; eauto using vr_inj_ext.
Qed.


Relating type variable contexts, totality and preservation of type formation

(* Invariant for totality & preservation for ∼ from B to A *)
Definition vr_tyctx_BA N ( : vrel) := (n : var), n < N (m : var), n m atnd m .
Notation "[ Theta ; N ↦ Psi ]" := (vr_tyctx_BA N ).

(* Invariant Extension Principles *)
Lemma vr_tyctx_BA_rs N a : [ ; N ] [vRS ; N a :: ].
Proof. intros VC n [m [Rnm Lm]]%VC. exists (S m). split; eauto using vrs. econstructor; eauto. Qed.

Lemma vr_tyctx_BA_ext N : [ ; N ] [vEXT ; 1 + N :: ].
Proof.
  intros VC [|n] L.
  - exists 0. split; auto using vext_head. now constructor.
  - apply lt_S_n in L. destruct (VC _ L) as [m [Rnm Lm]]. exists (S m). split; eauto using vext_tail. econstructor; eauto.
Qed.


(* Useful Instances *)
Lemma vr_tyctx_BA_nil : [ ; 0 ].
Proof. intros n H. omega. Qed.

(* Totality & Preservation *)
Lemma tyrel_BA_tot_pres N A : SB.istype N A , [ ; N ] a, A a SA.hastype a .
Proof.
  intros H; induction H; intros VC.
  - destruct (VC _ H) as [m [Rnm Lm]]. exists (SA.Var m). split.
    + now constructor.
    + econstructor; trivial. constructor. constructor.
  - specialize ( _ _ VC) as [a [Ra Ha]].
    specialize ( _ _ (vr_tyctx_BA_rs a VC)) as [b [Rb Hb]].
    exists (SA.Prod a b). split; econstructor; eauto. constructor.
  - (* new *) specialize (IHistype _ _ (vr_tyctx_BA_ext VC)) as [a [Ra Ha]].
    exists (SA.Prod a). assert (SA.hastype ) by (constructor; constructor).
    split; econstructor; eauto. constructor.
Qed.


(* Invariant for totality & preservation for ∼ from A to B *)
Definition vr_tyctx_AB N (: vrel) := (m: var), atnd m (n:var), n m n < N.
Notation "[ Theta ; N ↤ Psi ]" := (vr_tyctx_AB N ).

(* Invariant Extension Principles *)
Lemma vr_tyctx_AB_rs N a : [ ; N ] SA.hastype a [ vRS ; N a :: ].
Proof.
  intros VC Ta [|m] Lm; inv Lm.
  - exfalso. apply SA.srt_eq_ren_inv in ; subst. destruct (SA.prp_prp_contra Ta).
  - apply SA.srt_eq_ren_inv in ; subst.
    destruct (VC _ ) as [n [Rnm Ln]]. exists n; split; auto using vrs.
Qed.


Lemma vr_tyctx_AB_ext N : [ ; N ] [ vEXT ; S N :: ].
Proof.
  intros VC [|m] L; inv L.
  - exists 0. split; auto using vext_head. omega.
  - apply SA.srt_eq_ren_inv in ; subst.
    destruct (VC _ ) as [n [Rnm Ln]]. exists (S n). split; auto using vext_tail. omega.
Qed.


(* Useful Instances *)
Lemma vr_tyctx_AB_nil N : [ ; N nil ].
Proof. intros m H. inv H. Qed.

(* Totality & Preservation *)
Lemma tyrel_AB_tot_pres a : SA.valid SA.hastype a N, [ ; N ] A, A a SB.istype N A.
Proof.
  intros V H. pattern , a. revert a V H. apply SA.type_induction.
  - intros m V Lm N VC. destruct (VC _ Lm) as [n [Rnm Ln]].
    exists (SB.TyVar n); split; constructor; trivial.
  - intros a b V Ha IHa Hb IHb N VC.
    specialize (IHa _ _ VC) as [A [RA HA]].
    specialize (IHb _ _ (vr_tyctx_AB_rs VC Ha)) as [B [RB HB]].
    exists (SB.Imp A B). split; now constructor.
  - (* new *) intros a V Ha IHa N VC.
    specialize (IHa _ _ (vr_tyctx_AB_ext VC)) as [A [RA HA]].
    exists (SB.All A). split; now constructor.
Qed.


Substitution Theory for tyrel
Lemma tyrel_ren A a : A a vrm A.[ren ] a.[ren ].
Proof.
  intros H; revert ; induction H; intros .
  - constructor. eapply vr_map; eauto.
  - constructor; auto. asimpl. rewrite vrm_rs. auto.
  - (* new *) constructor. asimpl. rewrite vrm_ext. auto.
Qed.


Lemma tyrel_mono A a : A a A a.
Proof.
  intros HS H. revert HS. induction H; intros HS; eauto using tyrel, vr_mono;
  constructor; eauto using vrm_mono, vext_mono. (* new: vext_mono *)
Qed.


Corollary tyrel_weaken A a n m : A a (n,m) :: A a.
Proof. apply tyrel_mono; auto using incl_tl, incl_refl. Qed.

Corollary tyrel_rs A a : A a vRS A a.[ren (+1)].
Proof. intros. replace A with A.[ren id] by autosubst. now apply tyrel_ren. Qed.

Corollary tyrel_ext A a : A a vEXT A.[ren (+1)] a.[ren (+1)].
Proof. intros. now apply tyrel_weaken, tyrel_ren. Qed.

Definition cm_tyrel ( : vrel) ( : vrel) := x y, x y x y.

Lemma cm_tyrel_rs : cm_tyrel cm_tyrel (vRS ) (up ) (vRS ).
Proof. intros CM n m [m' E Rnm']%vrs_inv. subst. asimpl. now apply tyrel_rs, CM. Qed.

(* new *)
Lemma cm_tyrel_ext : cm_tyrel cm_tyrel (vEXT ) (up ) (up ) (vEXT ).
Proof.
  intros CM n m [[En Em]| [n' [m' [[En Em] ]]]]%vext_inv; subst.
  - constructor. now left.
  - asimpl. now apply tyrel_ext, CM.
Qed.


Lemma tyrel_subst A a : A a , cm_tyrel A.[] a.[].
Proof.
  intros H; induction H; intros CM.
  - asimpl; auto.
  - asimpl. pose proof (cm_tyrel_rs CM) as CM'. constructor; auto.
  - (* new *) pose proof (cm_tyrel_ext CM) as CM'. constructor; auto.
Qed.


(* new *)
Lemma cm_tyrel_beta B b : B b cm_tyrel (vEXT ) (B .: ids) (b .: ids) .
Proof. intros H x y [[Ex Ey]|[x' [y' [[Ex Ey] ]]]]%vext_inv; subst; trivial. asimpl. now constructor. Qed.

(* new *)
Lemma tyrel_beta A a B b : B b vEXT A a A.[B/] a.[b/].
Proof. intros HB HA. eapply tyrel_subst; eauto using cm_tyrel_beta. Qed.

Lemma tyrel_unmap A a : vrm A a A' a', A = A'.[ren ] a = a'.[ren ] A' a'.
Proof.
  intros H. remember (vrm ) as . revert HeqTheta'. induction H; intros S E; subst.
  - apply vr_unmap in H as [n' [m' [En [Em J]]]]. exists (SB.TyVar n'), (SA.Var m'); asimpl; subst.
    repeat split; trivial. now constructor.
  - specialize ( _ _ _ (eq_refl _)) as [A' [a' [EA [Ea RAa]]]]. rewrite vrm_rs in .
    specialize ( _ _ _ (eq_refl _)) as [B' [b' [EB [Eb RBb]]]].
    exists (SB.Imp A' B'), (SA.Prod a' b'). subst. asimpl. do 2 (split; trivial). now constructor.
  - (* new *) rewrite vrm_ext in IHtyrel. specialize (IHtyrel _ _ _ (eq_refl _)) as [A' [a' [EA [Ea RAa]]]].
    exists (SB.All A'), (SA.Prod a'). subst. asimpl. do 2 (split; trivial). now constructor.
Qed.


Corollary tyrel_vrs_inv A a : vRS A a a', a = a'.[ren (+1)] & A a'.
Proof.
  intros H. pose proof (tyrel_unmap _ _ _ H) as [A' [a' [EA [Ea ]]]].
  asimpl in *. subst A'. exists a'; trivial.
Qed.


Relating terms

Reserved Notation "⟨ Theta , Sigma ⟩ |- s ≈ b" (at level 70, no associativity).
Inductive tmrel ( : vrel) : SB.tm SA.tm Prop :=
| tmrel_var n m : n m , SB.Var n SA.Var m
| tmrel_app s t a b : , s a , t b , SB.App s t SA.App a b
| tmrel_lam A s a b: A a vRS , vEXT s b , SB.Lam A s SA.Lam a b
| tmrel_tyapp s B a b : , s a B b , SB.TyApp s B SA.App a b (* new *)
| tmrel_tylam s a: vEXT , vRS s a , SB.TyLam s SA.Lam a (* new *)
where "⟨ Theta , Sigma ⟩ |- s ≈ b" := (tmrel s b).

Functionality and Injectivity of tmrel
Lemma tmrel_func : vr_func vr_func rel_func (tmrel ).
Proof.
  intros Rtyf Rtmf s H. revert . induction H; intros a' J; inv J.
  - now rewrite (Rtmf _ _ _ H ).
  - f_equal; auto.
  - f_equal; eauto using vr_func_rs, vr_func_ext. eapply (tyrel_func Rtyf); eassumption.
  - f_equal; auto. eapply (tyrel_func Rtyf); eassumption. (* new *)
  - f_equal; eauto using vr_func_rs, vr_func_ext. (* new *)
Qed.


(* new *)
Lemma tyrel_tmrel_disjoint ( : vrel) A s a : A a , s a False.
Proof. intros D . destruct ; inv . firstorder. Qed.

(* we again obtain some actual new cases, as well as various impossible cases due to overlap, now on app and lam.  Note the extra disjointedness assumption. *)
Lemma tmrel_inj : vr_inj vr_inj rel_inj (tmrel ).
Proof.
  intros Rtyi Rtmi D a H. revert . induction H; intros A' J; inv J.
  - now rewrite (Rtmi _ _ _ H ).
  - f_equal; auto.
  - (* new, app-error *) exfalso. eauto using tyrel_tmrel_disjoint.
  - f_equal; eauto using vr_inj_rs, vr_inj_ext, vrd_rs_ext. eapply (tyrel_inj Rtyi); eassumption.
  - (* new, lam-error *) exfalso. inv H.
  - (* new, app-error *) exfalso. eauto using tyrel_tmrel_disjoint.
  - (* new, correct tyApp match *) f_equal; auto. eapply (tyrel_inj Rtyi); eassumption.
  - (* new, lam-error *) exfalso. inv .
  - (* new, correct tyLam match *) f_equal; eauto using vr_inj_rs, vr_inj_ext, vrd_ext_rs.
Qed.


Relating term variable contexts, totality and preservation of typing

(* Invariant for totality & preservation for ≈ from B to A *)
Definition vr_tmctx_BA ( : vrel) := (n:var) A, atn n A (m : var) a, A a n m atnd m a.
Notation "[ ⟨ Theta , Sigma ⟩ ; Gamma ↦ Psi ]" := (vr_tmctx_BA ).

(* Invariant Extension Principles *)
Lemma vr_tmctx_BA_rs_ext A a : [⟨, ; ] A a [⟨vRS ,vEXT ; A :: a :: ].
Proof.
  intros VC TyRAa [|n] B Ln; inv Ln.
  - exists 0, a.[ren (+1)]. split; auto using tyrel_rs. split; eauto using vext_head. now constructor.
  - destruct (VC _ _ ) as [m [b [TyRBb [Rnm Lm]]]]. exists (S m), b.[ren (+1)]; repeat split; auto using tyrel_rs, vext_tail. econstructor; eauto.
Qed.


Lemma vr_tmctx_BA_ext_rs : [⟨, ; ] [⟨vEXT ,vRS ; ..[ren (+1)] :: ].
Proof.
  intros VC n B Ln. destruct (mmap_atn Ln) as [B' [EB Ln']].
  specialize (VC _ _ Ln') as [m [b [ [Rnm Lm]]]]. subst.
  exists (S m), b.[ren (+1)]. do 2 ( split; auto using tyrel_ext, vrs). econstructor; eauto.
Qed.


(* Useful Instances *)
Lemma vr_tmctx_BA_nil : [⟨, ; nil ].
Proof. intros x A H. inv H. Qed.

(* Totality & Preservation *)
Lemma tmrel_BA_tot_pres N s A :
  SB.hastype N s A
   , SA.valid vr_func [ ; N ] [⟨, ; ]
                a b, A b , s a SA.hastype a b SA.hastype b .
Proof.
  intros H; induction H; intros V RtyF VCty VCtm.
  - destruct (tyrel_BA_tot_pres VCty) as [a [TyRa Ha]].
    apply VCtm in H as [m [a' [TyRa' [Rxm Lm]]]].
    pose proof (tyrel_func RtyF TyRa TyRa') as E; subst a'. clear TyRa'.
    exists (SA.Var m), a. do 3 (split; auto using tmrel). econstructor; eauto.
  - specialize ( _ _ _ V RtyF VCty VCtm) as [la [pr [TyRalpr [TmRsla [Hla _]]]]].
    specialize ( _ _ _ V RtyF VCty VCtm) as [c [a [TyRAa [TmRtc [Hc _]]]]].
    inv TyRalpr. assert (a = ) by (eapply tyrel_func; eauto); subst . clear .
    apply tyrel_vrs_inv in as [b' Eb TyRBb]. exists (SA.App la c), b'.
    assert (Hb' : SA.hastype b' )
      by now pose proof (SA.hastype_beta_ty V Hla Hc) as (_ & _ & _ & [] & Hb); subst b; asimpl in Hb.
    do 3 (split; auto using tmrel). econstructor; eauto. subst. autosubst.
  - destruct (tyrel_BA_tot_pres VCty) as [a [TyRa Ha]].
    eapply vr_tmctx_BA_rs_ext in VCtm; eauto.
    apply vr_tyctx_BA_rs with (a:=a) in VCty.
    apply vr_func_rs in RtyF.
    destruct (IHhastype _ _ (a :: ) (SA.valid_ext Ha V) RtyF VCty VCtm) as [c [b [TyRBb [TmRsc [Hc Hb]]]]].
    exists (SA.Lam a c), (SA.Prod a b). do 2 (split; eauto using tyrel, tmrel). split; econstructor; eauto; econstructor.
  - (* new *) subst. specialize (IHhastype _ _ _ V RtyF VCty VCtm) as [la [pr [TyRalpr [TmRsla [Tla _]]]]].
    destruct (tyrel_BA_tot_pres H VCty) as [b [TyRBb Tb]]. inv TyRalpr.
    exists (SA.App la b), a.[b/]. repeat split.
    + now apply tyrel_beta. (* note: we need tyrel beta here! *)
    + now constructor.
    + econstructor; eauto.
    + now pose proof (SA.hastype_beta_ty V Tla Tb) as (_ & _ & _ & [] & Hab).
  - (* new *) apply vr_tmctx_BA_ext_rs in VCtm.
    apply vr_tyctx_BA_ext in VCty.
    apply vr_func_ext in RtyF.
    assert (Hax : SA.hastype ) by (constructor; constructor).
    destruct (IHhastype _ _ _ (SA.valid_ext Hax V) RtyF VCty VCtm) as [b [a [TyRAa [TmRsb [Tb Ta]]]]].
    exists (SA.Lam b), (SA.Prod a). repeat split.
    + now constructor.
    + now constructor.
    + econstructor; eauto; constructor.
    + econstructor; eauto; constructor.
Qed.


(* Invariant for totality & preservation for ≈ from A to B *)
Definition vr_tmctx_AB ( : vrel) := m a, atnd m a SA.hastype a n A, A a n m atn n A.
Notation "[ ⟨ Theta , Sigma ⟩ ; Gamma ↤ Psi ]" := (vr_tmctx_AB ).

(* Invariant Extension Principles *)
Lemma vr_tmctx_AB_rs_ext A a : SA.valid (a :: ) [⟨, ; ] A a [⟨vRS ,vEXT ; A :: a :: ].
Proof.
  intros V VC TyRAa [|m'] b Lm' Hb; inv Lm'.
  - exists 0, A. repeat split; auto using tyrel_rs, vext_head. constructor.
  - rename B into b. apply (SA.hastype_type_strengthen _ V), (VC _ _ ) in Hb as [n [B [TyRBb [Rnm Ln]]]].
    exists (S n), B. repeat split; auto using tyrel_rs, vext_tail. now constructor.
Qed.


Lemma vr_tmctx_AB_ext_rs : SA.valid ( :: ) [⟨, ; ] [⟨vEXT ,vRS ; ..[ren (+1)] :: ].
Proof.
  intros V VC [|m'] b Lm' Hb; inv Lm'.
  - destruct (SA.prp_prp_contra Hb).
  - rename B into b. apply (SA.hastype_type_strengthen _ V), (VC _ _ ) in Hb as [n [B [TyRBb [Rnm Ln]]]].
    exists n, B.[ren (+1)]. split; [now apply tyrel_ext|]. split; [now apply vrs|]. eapply atn_mmap; eauto.
Qed.


(* Useful Instances *)
Lemma vr_tmctx_AB_nil : [⟨, ; nil].
Proof. intros y a H. inv H. Qed.

(* Totality & Preservation *)
Lemma tmrel_AB_tot_pres a b :
  SA.valid SA.hastype b SA.hastype a b
   N , vr_inj [ ; N ] [⟨, ; ]
                  s A, A b , s a SB.hastype N s A SB.istype N A.
Proof.
  intros V . pattern , a, b. revert a b V . apply SA.term_induction.
  - intros m a V Lm Ha N VI VCty VCtm.
    destruct (tyrel_AB_tot_pres V Ha VCty) as [A [TyRAa HA]].
    destruct (VCtm _ _ Lm Ha) as [n [A' [ [Rnm Ln]]]].
    pose proof (tyrel_inj VI TyRAa ) as E; subst A'; clear .
    exists (SB.Var n), A. split; eauto using tmrel, SB.hastype.
  - (* changed *) intros a b c d d' V Ha Hc _ IHa Hb IHb E N VI VCty VCtm.
    specialize (IHa _ _ _ _ VI VCty VCtm) as [f [F [TyRFpr [TmRfa [Hf HF]]]]].
    specialize (IHb _ _ _ _ VI VCty VCtm) as [s [C [TyRCc [TmRsb [Hs _]]]]].
    inversion TyRFpr; [|subst c; destruct (SA.prp_prp_contra Hc)]; subst F; clear TyRFpr. rename A into C', B into D.
    apply tyrel_vrs_inv in as [d'' Ed TyRDd''].
    rewrite Ed in E. asimpl in E. clear Ed. subst d''. inv HF; clear .
    pose proof (tyrel_inj VI TyRCc ) as E; subst C'; clear .
    exists (SB.App f s), D. split; eauto using tmrel, SB.hastype, SB.istype.
  - intros a b c V Ha _ _ IHb N VI VCty VCtm.
    destruct (tyrel_AB_tot_pres V Ha VCty) as [A [TyRAa HA]].
    eapply vr_tyctx_AB_rs in VCty; eauto.
    eapply vr_tmctx_AB_rs_ext in VCtm; eauto using SA.valid.
    apply vr_inj_rs in VI.
    specialize (IHb _ _ _ _ VI VCty VCtm) as [s [C [TyRCc [TmRsb [Hs HC]]]]].
    exists (SB.Lam A s), (SB.Imp A C). repeat split; eauto using tyrel, tmrel, SB.istype, SB.hastype.
  - (* new *) intros a b d d' V _ _ IHa Hb E N VI VCty VCtm.
    destruct (tyrel_AB_tot_pres V Hb VCty) as [B [TyRBb HB]].
    specialize (IHa _ _ _ _ VI VCty VCtm) as [f [F [TyRFpr [TmRfa [Hf HF]]]]].
    inv TyRFpr; [inv |]; rename A into D. inv HF.
    exists (SB.TyApp f B), D.[B/]. repeat split.
    + now apply tyrel_beta.
    + now constructor.
    + econstructor; eauto.
    + now apply SB.istype_beta.
  - (* new *) intros b c V _ _ IHb N VI VCty VCtm.
    eapply vr_tyctx_AB_ext in VCty; eauto.
    assert (Hax : SA.hastype ) by (constructor; constructor).
    eapply vr_tmctx_AB_ext_rs in VCtm; eauto using SA.valid.
    apply vr_inj_ext in VI.
    destruct (IHb _ _ _ _ VI VCty VCtm) as [s [C [TyRCc [TmRsb [Hs HC]]]]].
    exists (SB.TyLam s), (SB.All C). repeat split; now constructor.
Qed.


Substitution Theory for tmrel
(* new: rho instead of id, to allow for type renamings ... *)
Lemma tmrel_ren s a : , s a vrm ,vrm s.|[ren ].[ren ] a.[ren ].
Proof.
  intros H; revert ; induction H; intros .
  - constructor. eapply vr_map; eauto.
  - constructor; auto.
  - asimpl. constructor.
    + (* change *) now apply tyrel_ren.
    + rewrite vrm_ext, vrm_rs. auto.
  - (* new *) constructor; auto. now apply tyrel_ren.
  - (* new *) constructor. asimpl. rewrite vrm_ext, vrm_rs. auto.
Qed.


(* new: also consider monotonicity in the type context *)
Lemma tmrel_mono s a : , s a , s a.
Proof.
  intros HSty HStm H. revert HSty HStm. induction H; intros HSty HStm; eauto using tmrel, tyrel_mono;
  constructor; eauto using tyrel_mono, vrm_mono, vext_mono.
Qed.


(* new *)
Corollary tmrel_weaken_ty s a n m : , s a (n,m) :: , s a.
Proof. apply tmrel_mono; auto using incl_tl, incl_refl. Qed.

Corollary tmrel_weaken_tm s a n m : , s a ,(n,m) :: s a.
Proof. apply tmrel_mono; auto using incl_tl, incl_refl. Qed.

(* new: changed proof to incorporate type renaming. *)
Corollary tmrel_rs_ext s a : , s a vRS ,vEXT s.[ren (+1)] a.[ren (+1)].
Proof. intros. apply tmrel_weaken_tm. replace s with (s.|[ren id]) by autosubst. now apply tmrel_ren. Qed.

(* new *)
Lemma tmrel_ext_rs s a : , s a vEXT , vRS s.|[ren (+1)] a.[ren (+1)].
Proof. intros. apply tmrel_weaken_ty. replace (s.|[ren (+1)]) with (s.|[ren (+1)].[ren id]) by autosubst. now apply tmrel_ren. Qed.

Definition cm_tmrel ( : vrel) ( : vrel) := ( n m, n m n m) ( n m, n m , n m).

Lemma cm_tmrel_rs_ext : cm_tmrel cm_tmrel (vRS ) (vEXT ) (up ) (up ) (vRS ) (vEXT ).
Proof.
  intros CM. split.
  - apply cm_tyrel_rs. intros n m. apply CM.
  - intros n m [[En Em]| [n' [m' [[En Em] ]]]]%vext_inv; subst.
    + constructor. now left.
    + asimpl. now apply tmrel_rs_ext, CM.
Qed.


(* new *)
Lemma cm_tmrel_ext_rs : cm_tmrel cm_tmrel (vEXT ) (vRS ) (up ) ( >>| ren (+1)) (up ) (vEXT ) (vRS ).
Proof.
  intros CM. split.
  - apply cm_tyrel_ext. intros n m. apply CM.
  - intros n m [m' Em Rnm']%vrs_inv. subst. asimpl. now apply tmrel_ext_rs, CM.
Qed.


Lemma tmrel_subst s a : , s a , cm_tmrel , s.|[].[] a.[].
Proof.
  intros H; induction H; intros CM.
  - destruct CM. asimpl; eauto.
  - constructor; auto.
  - asimpl. constructor.
    + eapply tyrel_subst; eauto. destruct CM as [CM _]. exact CM.
    + pose proof (cm_tmrel_rs_ext CM) as CM'. auto.
  - (* new *) constructor; auto. eapply tyrel_subst; eauto. destruct CM as [CM _]. exact CM.
  - (* new *) constructor. pose proof (cm_tmrel_ext_rs CM) as CM'. auto.
Qed.


Lemma cm_tmrel_beta_tm B b : , B b cm_tmrel (vRS ) (vEXT ) ids (B .: ids) (b .: ids) .
Proof.
  intros CM. split.
  - intros n m [m' Em Rnm']%vrs_inv. subst. asimpl. now constructor.
  - intros n m [[En Em]|[n' [m' [[En Em] ]]]]%vext_inv; subst; trivial. asimpl. now constructor.
Qed.


Lemma tmrel_beta_tm s a t b : , t b vRS ,vEXT s a , s.[t/] a.[b/].
Proof. intros Ht Hs. pose proof (tmrel_subst Hs (cm_tmrel_beta_tm Ht)) as J. now asimpl in J. Qed.

Valid Contexts always have related Counterparts

While the following two proofs may appear lengthy they are actually quite straightforward. They simply analyse the composition of the respective well-formed context and accordingly employ the suitable base invariant instances and their respective extension principles.
Lemma ctxrel_BA N :
  SB.valid N ,
    SA.valid vr_func vr_inj vr_func vr_inj
    [ ; N ] [ ; N ] [⟨, ; ] [⟨, ; ].
Proof.
  intros H; induction H.
  - exists nil, nil, nil.
    repeat split; eauto using SA.valid, vr_func_nil, vr_inj_nil, vr_tyctx_BA_nil, vr_tyctx_AB_nil, vr_tmctx_BA_nil, vr_tmctx_AB_nil.
  - (* new *) destruct IHvalid as ( & & & V & Fty & Ity & Ftm & Itm & D & VCBAty & VCABty & VCBAtm & VCABtm).
    assert (Hax : SA.hastype ) by (constructor; constructor).
    assert (V' : SA.valid ( :: )) by (econstructor; eauto).
    apply vr_tmctx_BA_ext_rs in VCBAtm.
    apply (vr_tmctx_AB_ext_rs V') in VCABtm. asimpl in *.
    exists ( :: ), (vEXT ), (vRS ).
    repeat split; eauto using vr_func_ext, vr_inj_ext, vr_func_rs, vr_inj_rs, vrd_ext_rs, vr_tyctx_BA_ext, vr_tyctx_AB_ext.
  - destruct IHvalid as ( & & & V & Fty & Ity & Ftm & Itm & D & VCBAty & VCABty & VCBAtm & VCABtm).
    destruct (tyrel_BA_tot_pres H VCBAty) as [a [RAa Ha]].
    assert (V' : SA.valid (a :: )) by (econstructor; eauto).
    exists (a :: ), (vRS ), (vEXT ).
    repeat split; eauto using vr_func_ext, vr_inj_ext, vr_func_rs, vr_inj_rs, vrd_rs_ext, vr_tyctx_BA_rs, vr_tyctx_AB_rs, vr_tmctx_BA_rs_ext, vr_tmctx_AB_rs_ext.
Qed.


Lemma ctxrel_AB :
  SA.valid N ,
    SB.valid N vr_func vr_inj vr_func vr_inj
    [ ; N ] [ ; N ] [⟨, ; ] [⟨, ; ].
Proof.
  intros H; induction H.
  - exists 0, nil, nil, nil.
    repeat split; eauto using SB.valid_empty, vr_func_nil, vr_inj_nil, vr_tyctx_BA_nil, vr_tyctx_AB_nil, vr_tmctx_BA_nil, vr_tmctx_AB_nil.
  - assert (Va : SA.valid (a :: )) by (econstructor; eauto).
    destruct IHvalid as (N & & & & V & Fty & Ity & Ftm & Itm & D & VCBAty & VCABty & VCBAtm & VCABtm). destruct s.
    + destruct (tyrel_AB_tot_pres H VCABty) as [A [RAa HA]].
      assert (VA : SB.valid N (A :: )) by (econstructor; eauto).
      exists N, (A :: ), (vRS ), (vEXT ).
      repeat split; eauto using vr_func_ext, vr_inj_ext, vr_func_rs, vr_inj_rs, vrd_rs_ext, vr_tyctx_BA_rs, vr_tyctx_AB_rs, vr_tmctx_BA_rs_ext, vr_tmctx_AB_rs_ext.
    + apply (SA.typ_degeneracy ) in H; subst.
      exists (S N), ..[ren (+1)], (vEXT ), (vRS ).
      repeat split; eauto using SB.valid_shift, vr_func_ext, vr_inj_ext, vr_func_rs, vr_inj_rs, vrd_ext_rs,
                    vr_tyctx_BA_ext, vr_tyctx_AB_ext, vr_tmctx_BA_ext_rs, vr_tmctx_AB_ext_rs.
Qed.


Correspondence for Closed Judgements

Recall that both languages can fully internalise their contexts, so we obtain results for completely closed judgements. Note that we do not require the idR base instances from the STLC development for our invariants, here.

Theorem tyrel_BA_total_preserving A : SB.istype 0 A a, nil A a SA.hastype nil a .
Proof.
  split.
  - intros. now eapply tyrel_BA_tot_pres, vr_tyctx_BA_nil.
  - intros [a [RA Ha]]. apply tyrel_AB_tot_pres with (N:=0) (:=nil) in Ha as [A' [RA' HA']]; auto using vr_tyctx_AB_nil, SA.valid_nil.
    now rewrite (tyrel_inj vr_inj_nil RA RA').
Qed.


Theorem tyrel_AB_total_preserving a : SA.hastype nil a A, nil A a SB.istype 0 A.
Proof.
  split.
  - intros. now eapply (tyrel_AB_tot_pres SA.valid_nil), vr_tyctx_AB_nil.
  - intros [A [Ra HA]]. apply tyrel_BA_tot_pres with (:=nil) (:=nil) in HA as [a' [Ra' Ha']]; auto using vr_tyctx_BA_nil.
    now rewrite (tyrel_func vr_func_nil Ra Ra').
Qed.


Theorem tmrel_BA_total_preserving s A : SB.hastype 0 nil s A b a, nil A a nil,nil s b SA.hastype nil b a SA.hastype nil a .
Proof.
  split.
  - intros. eapply tmrel_BA_tot_pres; eauto using vr_func_nil, vr_tyctx_BA_nil, vr_tmctx_BA_nil, SA.valid_nil.
  - intros [b [a [RA [Rs [Hb Ha]]]]].
    eapply tmrel_AB_tot_pres with (:=nil) (N:=0) (:=nil) in Hb as [s' [A' [RA' [Rs' [Hs' HA']]]]];
      eauto using vr_inj_nil, vr_tyctx_AB_nil, vr_tmctx_AB_nil, SA.valid_nil.
    now rewrite (tyrel_inj vr_inj_nil RA RA'), (tmrel_inj vr_inj_nil vr_inj_nil vrd_nil Rs Rs').
Qed.


Theorem tmrel_AB_total_preserving a b : SA.hastype nil a SA.hastype nil b a s A, nil A a nil,nil s b SB.hastype 0 nil s A SB.istype 0 A.
Proof.
  split.
  - intros [Hb Ha]. eapply tmrel_AB_tot_pres; eauto using vr_inj_nil, vr_tyctx_AB_nil, vr_tmctx_AB_nil, SA.valid_nil.
  - intros [s [A [Rb [Ra [Hs HA]]]]].
    eapply tmrel_BA_tot_pres with (:=nil) in Hs as [a' [b' [Rb' [Ra' [Ha' Hb']]]]];
      eauto using vr_func_nil, vr_tyctx_BA_nil, vr_tmctx_BA_nil, SA.valid_nil.
    now rewrite (tyrel_func vr_func_nil Rb Rb'), (tmrel_func vr_func_nil vr_func_nil Ra Ra').
Qed.


Demos

DEMO 1: Transport of propagation from PTS to SysF
Theorem demo1 N s A : SB.valid N SB.hastype N s A SB.istype N A.
Proof.
  intros V H. destruct (ctxrel_BA V) as ( & & & Vp & Fty & Ity & _ & _ & _ & VCBAty & VCABty & VCBAtm & _).
  eapply tmrel_BA_tot_pres with ( := ) in H as (_ & a & HAa & _ & _ & Ha); try eassumption.
  eapply tyrel_AB_tot_pres in Ha as (A' & & J); try eassumption.
  now rewrite (tyrel_inj Ity HAa ).
Qed.


DEMO 2: Transport of beta-substitutivity from PTS to SysF
Theorem demo2 t B N s A: SB.valid N SB.hastype N t B SB.hastype N (B :: ) s A SB.hastype N s.[t/] A.
Proof.
  (* step 1: obtain suitable mapping relations and associated properties for the given valid context *)
  intros ( & & & Vp & Fty & Ity & _ & Itm & VD & VCBAty & VCABty & VCBAtm & VCABtm)%ctxrel_BA Ht Hs.
  (* step 2: map problem to PTS *)
  eapply tmrel_BA_tot_pres in Ht as (c & b & RBb & Rtc & Hc & Hb); try eassumption.
  eapply tmrel_BA_tot_pres with ( := b :: ) ( := vRS ) ( := vEXT ) in Hs as (d & a & RAa & Rsd & Hd & Ha);
    eauto using SA.valid, vr_func_rs, vr_tyctx_BA_rs, vr_tmctx_BA_rs_ext.
  (* step 3: use the desired property on the PTS side, and clean up. *)
  pose proof (SA.hastype_beta Vp Hc Hd) as J.
  destruct (tyrel_vrs_inv _ RAa) as [a' Ea RAa']. subst a. asimpl in J.
  (* step 4: prepare mapping backwards, using compatibility with beta of ≈. *)
  assert (RJ : , s.[t/] d.[c/]) by now apply tmrel_beta_tm.
  eapply SA.hastype_type_strengthen in Ha; eauto using SA.valid.
  (* step 5: map back into STLC, and fix diverged mappings, using injectivity. *)
  pose proof (tmrel_AB_tot_pres Vp Ha J Ity VCABty VCABtm) as [u [A' [ [Ru [Hu _]]]]].
  assert (E: A = A') by apply (tyrel_inj Ity RAa' ). subst A'. clear .
  assert (E: s.[t/] = u) by apply (tmrel_inj Ity Itm VD RJ Ru). subst u. clear Ru.
  (* step 6: profit *)
  assumption.
Qed.