RSC.sysfCorrespondence
(* (c) 2018, Jonas Kaiser *)
Require Import Omega List.
From Autosubst Require Export Autosubst.
From RSC Require Import Decidable lib vrel pts ARS.
Set Implicit Arguments.
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 (s1 s2 : S) : Dec (s1 = s2). derive. Defined.
(* now we have a PTS signature, the remainder is for functionality *)
Lemma A_func s1 s2 s2' : A s1 s2 -> A s1 s2' -> s2 = s2'.
Proof. intros H1 H2. inv H1. now inv H2. Qed.
Lemma R_func s1 s2 s3 s3' : R s1 s2 s3 -> R s1 s2 s3' -> s3 = s3'.
Proof. intros H1 H2. inv H1; now inv H2. Qed.
End F_spec.
Include FPTS (F_spec).
Notation "∗" := (Srt Prp).
Notation "⬜" := (Srt Typ).
(* special results about this particular PTS ... *)
Lemma typ_no_type Psi a : ~ hastype Psi ⬜ a.
Proof. apply srt_no_type. intros s H. inv H. Qed.
Lemma prp_prp_contra Psi : ~ hastype Psi ∗ ∗.
Proof. intros H. apply hastype_srt_srt in H. inv H. Qed.
Lemma typ_degeneracy Psi a : valid Psi -> hastype Psi a ⬜ -> a = ∗.
Proof.
intros V H. inv H.
- now inv H2.
- exfalso. destruct (typ_no_type H1).
- exfalso. inv H1.
- exfalso. destruct (hastype_beta_ty V H0 H1) as [_ [s [_ [_ Hd]]]].
rewrite <- H2 in Hd. destruct (typ_no_type Hd).
- exfalso. destruct (typ_no_type H1).
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 Psi a s : valid Psi -> hastype Psi 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 Psi a b : valid Psi -> hastype Psi 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) :
(forall Psi n, valid Psi -> atnd Psi n ∗ -> Q Psi (Var n)) ->
(forall Psi a b, valid Psi -> hastype Psi a ∗ -> Q Psi a -> hastype (a :: Psi) b ∗ -> Q (a :: Psi) b -> Q Psi (Prod a b)) ->
(forall Psi b, valid Psi -> hastype (∗ :: Psi) b ∗ -> Q (∗ :: Psi) b -> Q Psi (Prod ∗ b)) -> (* new *)
forall Psi a, valid Psi -> hastype Psi a ∗ -> Q Psi a.
Proof.
intros Qvar Qimp Qall. intros Psi 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 (IHhastype1 V (eq_refl _)). specialize (IHhastype2 (valid_ext H0 V) (eq_refl _)). now apply Qimp.
+ clear IHhastype1 E. specialize (IHhastype2 (valid_ext H0 V) (eq_refl _)). apply (typ_degeneracy V) in H0. subst. now apply Qall. (* new *)
- exfalso. subst. destruct (hastype_beta_ty V H H0) as [s1 [s2 [s3 [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 H1. auto.
Qed.
Lemma term_induction (Q : list tm -> tm -> tm -> Prop) :
(forall Psi n a, valid Psi -> atnd Psi n a -> hastype Psi a ∗ -> Q Psi (Var n) a) ->
(forall Psi a b c d d', valid Psi -> hastype Psi a (Prod c d) -> hastype Psi c ∗ -> hastype (c :: Psi) d ∗ -> Q Psi a (Prod c d) -> hastype Psi b c -> Q Psi b c -> d' = d.[b/] -> Q Psi (App a b) d') ->
(forall Psi a b c, valid Psi -> hastype Psi a ∗ -> hastype (a :: Psi) c ∗ -> hastype (a :: Psi) b c -> Q (a :: Psi) b c -> Q Psi (Lam a b) (Prod a c)) ->
(forall Psi a b d d', valid Psi -> hastype Psi a (Prod ∗ d) -> hastype (∗ :: Psi) d ∗ -> Q Psi a (Prod ∗ d) -> hastype Psi b ∗ -> d' = d.[b/] -> Q Psi (App a b) d') -> (* new *)
(forall Psi b c, valid Psi -> hastype (∗ :: Psi) c ∗ -> hastype (∗ :: Psi) b c -> Q (∗ :: Psi) b c -> Q Psi (Lam ∗ b) (Prod ∗ c)) -> (* new *)
(forall Psi a b, valid Psi -> hastype Psi b ∗ -> hastype Psi a b -> Q Psi a b).
Proof.
intros Qvar Qapp Qlam Qtyapp Qtylam. intros Psi 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 H0. subst a.
assert (hastype Psi ∗ ⬜) by (constructor; constructor).
apply Qtylam; eauto using valid.
- apply (hastype_normal_ty V) in H. apply (types_normal V) in H0.
apply normal_bc in H1; trivial. subst. auto.
Qed.
Lemma hastype_type_strengthen Psi a b :
valid (a :: Psi) -> hastype (a :: Psi) b.[ren (+1)] ∗ -> hastype Psi b ∗.
Proof. intros. change ∗ with ∗.[ren (+1)] in H0. now apply hastype_strengthen in H0. Qed.
Fixpoint intern (Psi : list tm) (a b : tm) : (tm * tm) :=
match Psi with
| nil => (a,b)
| c :: Psi => intern Psi (Lam c a) (Prod c b)
end.
Lemma intern_correct Psi a b c d: valid Psi -> intern Psi a b = (c,d) -> (hastype Psi b ∗ /\ hastype Psi 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 H1. eapply iff_trans; eauto. split; intros [Jty Jtm].
+ split; econstructor; eauto; destruct s; constructor.
+ split.
* now apply (hastype_prod_inv H0) in Jtm as [_ [_ [_ [[] [_ [K _]]]]]].
* apply strip_prod in Jty as [_ [sb [_ [_ [_ [J1 _]]]]]].
apply strip_lam in Jtm as [_ [_ [_ [b' [_ [_ [_ [Ha0 [_ 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.
Reserved Notation "Theta |- A ∼ a" (at level 70, no associativity).
Inductive tyrel (Theta : vrel) : SB.ty -> SA.tm -> Prop :=
| tyrel_var n m : Theta |- n ≃ m -> Theta |- SB.TyVar n ∼ SA.Var m
| tyrel_imp A B a b : Theta |- A ∼ a -> vRS Theta |- B ∼ b -> Theta |- SB.Imp A B ∼ SA.Prod a b
| tyrel_all A a : vEXT Theta |- A ∼ a -> Theta |- SB.All A ∼ SA.Prod ∗ a (* new *)
where "Theta |- A ∼ a" := (tyrel Theta A a).
Functionality and Injectivity of tyrel
Lemma tyrel_func Theta : vr_func Theta -> rel_func (tyrel Theta).
Proof.
intros Rf A a1 a2 H. revert a2. induction H; intros a' J; inv J.
- now rewrite (Rf _ _ _ H H1).
- 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 Theta : vr_inj Theta -> rel_inj (tyrel Theta).
Proof.
intros Ri A1 A2 a H. revert A2. induction H; intros A' J; inv J.
- now rewrite (Ri _ _ _ H H2).
- f_equal; eauto using vr_inj_rs.
- (* new *) exfalso. inv H.
- (* new *) exfalso. inv H3.
- (* new *) f_equal; eauto using vr_inj_ext.
Qed.
Proof.
intros Rf A a1 a2 H. revert a2. induction H; intros a' J; inv J.
- now rewrite (Rf _ _ _ H H1).
- 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 Theta : vr_inj Theta -> rel_inj (tyrel Theta).
Proof.
intros Ri A1 A2 a H. revert A2. induction H; intros A' J; inv J.
- now rewrite (Ri _ _ _ H H2).
- f_equal; eauto using vr_inj_rs.
- (* new *) exfalso. inv H.
- (* new *) exfalso. inv H3.
- (* 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 (Theta : vrel) Psi := forall (n : var), n < N -> exists (m : var), Theta |- n ≃ m /\ atnd Psi m ∗.
Notation "[ Theta ; N ↦ Psi ]" := (vr_tyctx_BA N Theta Psi).
(* Invariant Extension Principles *)
Lemma vr_tyctx_BA_rs N Theta Psi a : [Theta ; N ↦ Psi] -> [vRS Theta ; N ↦ a :: Psi].
Proof. intros VC n [m [Rnm Lm]]%VC. exists (S m). split; eauto using vrs. econstructor; eauto. Qed.
Lemma vr_tyctx_BA_ext N Theta Psi : [Theta ; N ↦ Psi] -> [vEXT Theta ; 1 + N ↦ ∗ :: Psi].
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 Theta Psi : [Theta ; 0 ↦ Psi].
Proof. intros n H. omega. Qed.
(* Totality & Preservation *)
Lemma tyrel_BA_tot_pres N A : SB.istype N A -> forall Theta Psi, [Theta ; N ↦ Psi] -> exists a, Theta |- A ∼ a /\ SA.hastype Psi a ∗.
Proof.
intros H; induction H; intros Theta Psi VC.
- destruct (VC _ H) as [m [Rnm Lm]]. exists (SA.Var m). split.
+ now constructor.
+ econstructor; trivial. constructor. constructor.
- specialize (IHistype1 _ _ VC) as [a [Ra Ha]].
specialize (IHistype2 _ _ (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 Psi ∗ ⬜) by (constructor; constructor).
split; econstructor; eauto. constructor.
Qed.
(* Invariant for totality & preservation for ∼ from A to B *)
Definition vr_tyctx_AB N (Theta: vrel) Psi := forall (m: var), atnd Psi m ∗ -> exists (n:var), Theta |- n ≃ m /\ n < N.
Notation "[ Theta ; N ↤ Psi ]" := (vr_tyctx_AB N Theta Psi).
(* Invariant Extension Principles *)
Lemma vr_tyctx_AB_rs N Theta Psi a : [ Theta ; N ↤ Psi ] -> SA.hastype Psi a ∗ -> [ vRS Theta ; N ↤ a :: Psi ].
Proof.
intros VC Ta [|m] Lm; inv Lm.
- exfalso. apply SA.srt_eq_ren_inv in H0; subst. destruct (SA.prp_prp_contra Ta).
- apply SA.srt_eq_ren_inv in H4; subst.
destruct (VC _ H2) as [n [Rnm Ln]]. exists n; split; auto using vrs.
Qed.
Lemma vr_tyctx_AB_ext N Theta Psi : [ Theta ; N ↤ Psi ] -> [ vEXT Theta ; S N ↤ ∗ :: Psi ].
Proof.
intros VC [|m] L; inv L.
- exists 0. split; auto using vext_head. omega.
- apply SA.srt_eq_ren_inv in H4; subst.
destruct (VC _ H2) as [n [Rnm Ln]]. exists (S n). split; auto using vext_tail. omega.
Qed.
(* Useful Instances *)
Lemma vr_tyctx_AB_nil N Theta : [ Theta ; N ↤ nil ].
Proof. intros m H. inv H. Qed.
(* Totality & Preservation *)
Lemma tyrel_AB_tot_pres Psi a : SA.valid Psi -> SA.hastype Psi a ∗ -> forall Theta N, [ Theta ; N ↤ Psi ] -> exists A, Theta |- A ∼ a /\ SB.istype N A.
Proof.
intros V H. pattern Psi, a. revert Psi a V H. apply SA.type_induction.
- intros Psi m V Lm Theta N VC. destruct (VC _ Lm) as [n [Rnm Ln]].
exists (SB.TyVar n); split; constructor; trivial.
- intros Psi a b V Ha IHa Hb IHb Theta 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 Psi a V Ha IHa Theta 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 Theta A a xi zeta : Theta |- A ∼ a -> vrm Theta xi zeta |- A.[ren xi] ∼ a.[ren zeta].
Proof.
intros H; revert xi zeta; induction H; intros xi zeta.
- constructor. eapply vr_map; eauto.
- constructor; auto. asimpl. rewrite vrm_rs. auto.
- (* new *) constructor. asimpl. rewrite vrm_ext. auto.
Qed.
Lemma tyrel_mono Theta1 Theta2 A a : Theta1 ⊑ Theta2 -> Theta1 |- A ∼ a -> Theta2 |- A ∼ a.
Proof.
intros HS H. revert Theta2 HS. induction H; intros Theta2 HS; eauto using tyrel, vr_mono;
constructor; eauto using vrm_mono, vext_mono. (* new: vext_mono *)
Qed.
Corollary tyrel_weaken Theta A a n m : Theta |- A ∼ a -> (n,m) :: Theta |- A ∼ a.
Proof. apply tyrel_mono; auto using incl_tl, incl_refl. Qed.
Corollary tyrel_rs Theta A a : Theta |- A ∼ a -> vRS Theta |- A ∼ a.[ren (+1)].
Proof. intros. replace A with A.[ren id] by autosubst. now apply tyrel_ren. Qed.
Corollary tyrel_ext Theta A a : Theta |- A ∼ a -> vEXT Theta |- A.[ren (+1)] ∼ a.[ren (+1)].
Proof. intros. now apply tyrel_weaken, tyrel_ren. Qed.
Definition cm_tyrel (Theta1 : vrel) sigma tau (Theta2 : vrel) := forall x y, Theta1 |- x ≃ y -> Theta2 |- sigma x ∼ tau y.
Lemma cm_tyrel_rs Theta1 sigma tau Theta2 : cm_tyrel Theta1 sigma tau Theta2 -> cm_tyrel (vRS Theta1) sigma (up tau) (vRS Theta2).
Proof. intros CM n m [m' E Rnm']%vrs_inv. subst. asimpl. now apply tyrel_rs, CM. Qed.
(* new *)
Lemma cm_tyrel_ext Theta1 sigma tau Theta2 : cm_tyrel Theta1 sigma tau Theta2 -> cm_tyrel (vEXT Theta1) (up sigma) (up tau) (vEXT Theta2).
Proof.
intros CM n m [[En Em]| [n' [m' [[En Em] Rn'm']]]]%vext_inv; subst.
- constructor. now left.
- asimpl. now apply tyrel_ext, CM.
Qed.
Lemma tyrel_subst Theta1 A a : Theta1 |- A ∼ a -> forall sigma tau Theta2, cm_tyrel Theta1 sigma tau Theta2 -> Theta2 |- A.[sigma] ∼ a.[tau].
Proof.
intros H; induction H; intros sigma tau Theta2 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 Theta B b : Theta |- B ∼ b -> cm_tyrel (vEXT Theta) (B .: ids) (b .: ids) Theta.
Proof. intros H x y [[Ex Ey]|[x' [y' [[Ex Ey] Rx'y']]]]%vext_inv; subst; trivial. asimpl. now constructor. Qed.
(* new *)
Lemma tyrel_beta Theta A a B b : Theta |- B ∼ b -> vEXT Theta |- A ∼ a -> Theta |- A.[B/] ∼ a.[b/].
Proof. intros HB HA. eapply tyrel_subst; eauto using cm_tyrel_beta. Qed.
Lemma tyrel_unmap Theta A a xi zeta : vrm Theta xi zeta |- A ∼ a -> exists A' a', A = A'.[ren xi] /\ a = a'.[ren zeta] /\ Theta |- A' ∼ a'.
Proof.
intros H. remember (vrm Theta xi zeta) as Theta'. revert Theta xi zeta HeqTheta'. induction H; intros S xi zeta 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 (IHtyrel1 _ _ _ (eq_refl _)) as [A' [a' [EA [Ea RAa]]]]. rewrite vrm_rs in IHtyrel2.
specialize (IHtyrel2 _ _ _ (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 Theta A a : vRS Theta |- A ∼ a -> exists2 a', a = a'.[ren (+1)] & Theta |- A ∼ a'.
Proof.
intros H. pose proof (tyrel_unmap _ _ _ H) as [A' [a' [EA [Ea RA'a']]]].
asimpl in *. subst A'. exists a'; trivial.
Qed.
Proof.
intros H; revert xi zeta; induction H; intros xi zeta.
- constructor. eapply vr_map; eauto.
- constructor; auto. asimpl. rewrite vrm_rs. auto.
- (* new *) constructor. asimpl. rewrite vrm_ext. auto.
Qed.
Lemma tyrel_mono Theta1 Theta2 A a : Theta1 ⊑ Theta2 -> Theta1 |- A ∼ a -> Theta2 |- A ∼ a.
Proof.
intros HS H. revert Theta2 HS. induction H; intros Theta2 HS; eauto using tyrel, vr_mono;
constructor; eauto using vrm_mono, vext_mono. (* new: vext_mono *)
Qed.
Corollary tyrel_weaken Theta A a n m : Theta |- A ∼ a -> (n,m) :: Theta |- A ∼ a.
Proof. apply tyrel_mono; auto using incl_tl, incl_refl. Qed.
Corollary tyrel_rs Theta A a : Theta |- A ∼ a -> vRS Theta |- A ∼ a.[ren (+1)].
Proof. intros. replace A with A.[ren id] by autosubst. now apply tyrel_ren. Qed.
Corollary tyrel_ext Theta A a : Theta |- A ∼ a -> vEXT Theta |- A.[ren (+1)] ∼ a.[ren (+1)].
Proof. intros. now apply tyrel_weaken, tyrel_ren. Qed.
Definition cm_tyrel (Theta1 : vrel) sigma tau (Theta2 : vrel) := forall x y, Theta1 |- x ≃ y -> Theta2 |- sigma x ∼ tau y.
Lemma cm_tyrel_rs Theta1 sigma tau Theta2 : cm_tyrel Theta1 sigma tau Theta2 -> cm_tyrel (vRS Theta1) sigma (up tau) (vRS Theta2).
Proof. intros CM n m [m' E Rnm']%vrs_inv. subst. asimpl. now apply tyrel_rs, CM. Qed.
(* new *)
Lemma cm_tyrel_ext Theta1 sigma tau Theta2 : cm_tyrel Theta1 sigma tau Theta2 -> cm_tyrel (vEXT Theta1) (up sigma) (up tau) (vEXT Theta2).
Proof.
intros CM n m [[En Em]| [n' [m' [[En Em] Rn'm']]]]%vext_inv; subst.
- constructor. now left.
- asimpl. now apply tyrel_ext, CM.
Qed.
Lemma tyrel_subst Theta1 A a : Theta1 |- A ∼ a -> forall sigma tau Theta2, cm_tyrel Theta1 sigma tau Theta2 -> Theta2 |- A.[sigma] ∼ a.[tau].
Proof.
intros H; induction H; intros sigma tau Theta2 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 Theta B b : Theta |- B ∼ b -> cm_tyrel (vEXT Theta) (B .: ids) (b .: ids) Theta.
Proof. intros H x y [[Ex Ey]|[x' [y' [[Ex Ey] Rx'y']]]]%vext_inv; subst; trivial. asimpl. now constructor. Qed.
(* new *)
Lemma tyrel_beta Theta A a B b : Theta |- B ∼ b -> vEXT Theta |- A ∼ a -> Theta |- A.[B/] ∼ a.[b/].
Proof. intros HB HA. eapply tyrel_subst; eauto using cm_tyrel_beta. Qed.
Lemma tyrel_unmap Theta A a xi zeta : vrm Theta xi zeta |- A ∼ a -> exists A' a', A = A'.[ren xi] /\ a = a'.[ren zeta] /\ Theta |- A' ∼ a'.
Proof.
intros H. remember (vrm Theta xi zeta) as Theta'. revert Theta xi zeta HeqTheta'. induction H; intros S xi zeta 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 (IHtyrel1 _ _ _ (eq_refl _)) as [A' [a' [EA [Ea RAa]]]]. rewrite vrm_rs in IHtyrel2.
specialize (IHtyrel2 _ _ _ (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 Theta A a : vRS Theta |- A ∼ a -> exists2 a', a = a'.[ren (+1)] & Theta |- A ∼ a'.
Proof.
intros H. pose proof (tyrel_unmap _ _ _ H) as [A' [a' [EA [Ea RA'a']]]].
asimpl in *. subst A'. exists a'; trivial.
Qed.
Reserved Notation "⟨ Theta , Sigma ⟩ |- s ≈ b" (at level 70, no associativity).
Inductive tmrel (Theta Sigma : vrel) : SB.tm -> SA.tm -> Prop :=
| tmrel_var n m : Sigma |- n ≃ m -> ⟨Theta,Sigma⟩ |- SB.Var n ≈ SA.Var m
| tmrel_app s t a b : ⟨Theta,Sigma⟩ |- s ≈ a -> ⟨Theta,Sigma⟩ |- t ≈ b -> ⟨Theta,Sigma⟩ |- SB.App s t ≈ SA.App a b
| tmrel_lam A s a b: Theta |- A ∼ a -> ⟨vRS Theta, vEXT Sigma⟩ |- s ≈ b -> ⟨Theta,Sigma⟩ |- SB.Lam A s ≈ SA.Lam a b
| tmrel_tyapp s B a b : ⟨Theta,Sigma⟩ |- s ≈ a -> Theta |- B ∼ b -> ⟨Theta,Sigma⟩ |- SB.TyApp s B ≈ SA.App a b (* new *)
| tmrel_tylam s a: ⟨vEXT Theta, vRS Sigma⟩ |- s ≈ a -> ⟨Theta,Sigma⟩ |- SB.TyLam s ≈ SA.Lam ∗ a (* new *)
where "⟨ Theta , Sigma ⟩ |- s ≈ b" := (tmrel Theta Sigma s b).
Inductive tmrel (Theta Sigma : vrel) : SB.tm -> SA.tm -> Prop :=
| tmrel_var n m : Sigma |- n ≃ m -> ⟨Theta,Sigma⟩ |- SB.Var n ≈ SA.Var m
| tmrel_app s t a b : ⟨Theta,Sigma⟩ |- s ≈ a -> ⟨Theta,Sigma⟩ |- t ≈ b -> ⟨Theta,Sigma⟩ |- SB.App s t ≈ SA.App a b
| tmrel_lam A s a b: Theta |- A ∼ a -> ⟨vRS Theta, vEXT Sigma⟩ |- s ≈ b -> ⟨Theta,Sigma⟩ |- SB.Lam A s ≈ SA.Lam a b
| tmrel_tyapp s B a b : ⟨Theta,Sigma⟩ |- s ≈ a -> Theta |- B ∼ b -> ⟨Theta,Sigma⟩ |- SB.TyApp s B ≈ SA.App a b (* new *)
| tmrel_tylam s a: ⟨vEXT Theta, vRS Sigma⟩ |- s ≈ a -> ⟨Theta,Sigma⟩ |- SB.TyLam s ≈ SA.Lam ∗ a (* new *)
where "⟨ Theta , Sigma ⟩ |- s ≈ b" := (tmrel Theta Sigma s b).
Functionality and Injectivity of tmrel
Lemma tmrel_func Theta Sigma : vr_func Theta -> vr_func Sigma -> rel_func (tmrel Theta Sigma).
Proof.
intros Rtyf Rtmf s a1 a2 H. revert a2. induction H; intros a' J; inv J.
- now rewrite (Rtmf _ _ _ H H1).
- 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 (Theta Sigma : vrel) A s a : Theta ∥ Sigma -> Theta |- A ∼ a -> ⟨Theta,Sigma⟩ |- s ≈ a -> False.
Proof. intros D H1 H2. destruct H1; inv H2. 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 Theta Sigma : vr_inj Theta -> vr_inj Sigma -> Theta ∥ Sigma -> rel_inj (tmrel Theta Sigma).
Proof.
intros Rtyi Rtmi D s1 s2 a H. revert s2. induction H; intros A' J; inv J.
- now rewrite (Rtmi _ _ _ H H2).
- 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 H3.
- (* new, correct tyLam match *) f_equal; eauto using vr_inj_rs, vr_inj_ext, vrd_ext_rs.
Qed.
Proof.
intros Rtyf Rtmf s a1 a2 H. revert a2. induction H; intros a' J; inv J.
- now rewrite (Rtmf _ _ _ H H1).
- 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 (Theta Sigma : vrel) A s a : Theta ∥ Sigma -> Theta |- A ∼ a -> ⟨Theta,Sigma⟩ |- s ≈ a -> False.
Proof. intros D H1 H2. destruct H1; inv H2. 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 Theta Sigma : vr_inj Theta -> vr_inj Sigma -> Theta ∥ Sigma -> rel_inj (tmrel Theta Sigma).
Proof.
intros Rtyi Rtmi D s1 s2 a H. revert s2. induction H; intros A' J; inv J.
- now rewrite (Rtmi _ _ _ H H2).
- 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 H3.
- (* 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 Gamma (Theta Sigma : vrel) Psi := forall (n:var) A, atn Gamma n A -> exists (m : var) a, Theta |- A ∼ a /\ Sigma |- n ≃ m /\ atnd Psi m a.
Notation "[ ⟨ Theta , Sigma ⟩ ; Gamma ↦ Psi ]" := (vr_tmctx_BA Gamma Theta Sigma Psi).
(* Invariant Extension Principles *)
Lemma vr_tmctx_BA_rs_ext Gamma Theta Sigma Psi A a : [⟨Theta,Sigma⟩ ; Gamma ↦ Psi] -> Theta |- A ∼ a -> [⟨vRS Theta,vEXT Sigma⟩ ; A :: Gamma ↦ a :: Psi].
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 _ _ H3) 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 Gamma Theta Sigma Psi : [⟨Theta,Sigma⟩ ; Gamma ↦ Psi] -> [⟨vEXT Theta,vRS Sigma⟩ ; Gamma..[ren (+1)] ↦ ∗ :: Psi].
Proof.
intros VC n B Ln. destruct (mmap_atn Ln) as [B' [EB Ln']].
specialize (VC _ _ Ln') as [m [b [TyRB'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 Theta Sigma Psi : [⟨Theta,Sigma⟩ ; nil ↦ Psi].
Proof. intros x A H. inv H. Qed.
(* Totality & Preservation *)
Lemma tmrel_BA_tot_pres N Gamma s A :
SB.hastype N Gamma s A ->
forall Theta Sigma Psi, SA.valid Psi -> vr_func Theta -> [Theta ; N ↦ Psi] -> [⟨Theta,Sigma⟩ ; Gamma ↦ Psi] ->
exists a b, Theta |- A ∼ b /\ ⟨Theta,Sigma⟩ |- s ≈ a /\ SA.hastype Psi a b /\ SA.hastype Psi b ∗.
Proof.
intros H; induction H; intros Theta Sigma Psi V RtyF VCty VCtm.
- destruct (tyrel_BA_tot_pres H0 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 (IHhastype1 _ _ _ V RtyF VCty VCtm) as [la [pr [TyRalpr [TmRsla [Hla _]]]]].
specialize (IHhastype2 _ _ _ V RtyF VCty VCtm) as [c [a [TyRAa [TmRtc [Hc _]]]]].
inv TyRalpr. assert (a = a0) by (eapply tyrel_func; eauto); subst a0. clear H3.
apply tyrel_vrs_inv in H5 as [b' Eb TyRBb]. exists (SA.App la c), b'.
assert (Hb' : SA.hastype Psi 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 H0 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 :: Psi) (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 Psi ∗ ⬜) 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 Gamma (Theta Sigma : vrel) Psi := forall m a, atnd Psi m a -> SA.hastype Psi a ∗ -> exists n A, Theta |- A ∼ a /\ Sigma |- n ≃ m /\ atn Gamma n A.
Notation "[ ⟨ Theta , Sigma ⟩ ; Gamma ↤ Psi ]" := (vr_tmctx_AB Gamma Theta Sigma Psi).
(* Invariant Extension Principles *)
Lemma vr_tmctx_AB_rs_ext Gamma Theta Sigma Psi A a : SA.valid (a :: Psi) -> [⟨Theta,Sigma⟩ ; Gamma ↤ Psi] -> Theta |- A ∼ a -> [⟨vRS Theta,vEXT Sigma⟩ ; A :: Gamma ↤ a :: Psi].
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 _ _ H2) 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 Gamma Theta Sigma Psi : SA.valid (∗ :: Psi) -> [⟨Theta,Sigma⟩ ; Gamma ↤ Psi] -> [⟨vEXT Theta,vRS Sigma⟩ ; Gamma..[ren (+1)] ↤ ∗ :: Psi].
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 _ _ H2) 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 Gamma Theta Sigma : [⟨Theta,Sigma⟩ ; Gamma ↤ nil].
Proof. intros y a H. inv H. Qed.
(* Totality & Preservation *)
Lemma tmrel_AB_tot_pres Psi a b :
SA.valid Psi -> SA.hastype Psi b ∗ -> SA.hastype Psi a b ->
forall Theta Sigma N Gamma, vr_inj Theta -> [Theta ; N ↤ Psi] -> [⟨Theta,Sigma⟩ ; Gamma ↤ Psi] ->
exists s A, Theta |- A ∼ b /\ ⟨Theta,Sigma⟩ |- s ≈ a /\ SB.hastype N Gamma s A /\ SB.istype N A.
Proof.
intros V H1 H2. pattern Psi, a, b. revert Psi a b V H1 H2. apply SA.term_induction.
- intros Psi m a V Lm Ha Theta Sigma N Gamma VI VCty VCtm.
destruct (tyrel_AB_tot_pres V Ha VCty) as [A [TyRAa HA]].
destruct (VCtm _ _ Lm Ha) as [n [A' [TyRA'a [Rnm Ln]]]].
pose proof (tyrel_inj VI TyRAa TyRA'a) as E; subst A'; clear TyRA'a.
exists (SB.Var n), A. split; eauto using tmrel, SB.hastype.
- (* changed *) intros Psi a b c d d' V Ha Hc _ IHa Hb IHb E Theta Sigma N Gamma 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 a0 b0 F; clear TyRFpr. rename A into C', B into D.
apply tyrel_vrs_inv in H3 as [d'' Ed TyRDd''].
rewrite Ed in E. asimpl in E. clear Ed. subst d''. inv HF; clear H1.
pose proof (tyrel_inj VI TyRCc H2) as E; subst C'; clear H2.
exists (SB.App f s), D. split; eauto using tmrel, SB.hastype, SB.istype.
- intros Psi a b c V Ha _ _ IHb Theta Sigma N Gamma 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 Psi a b d d' V _ _ IHa Hb E Theta Sigma N Gamma 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 H2|]; 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 Psi b c V _ _ IHb Theta Sigma N Gamma VI VCty VCtm.
eapply vr_tyctx_AB_ext in VCty; eauto.
assert (Hax : SA.hastype Psi ∗ ⬜) 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 Theta Sigma s a rho xi zeta : ⟨Theta,Sigma⟩ |- s ≈ a -> ⟨vrm Theta rho zeta,vrm Sigma xi zeta⟩ |- s.|[ren rho].[ren xi] ≈ a.[ren zeta].
Proof.
intros H; revert rho xi zeta; induction H; intros rho xi zeta.
- 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 Theta1 Theta2 Sigma1 Sigma2 s a : Theta1 ⊑ Theta2 -> Sigma1 ⊑ Sigma2 -> ⟨Theta1,Sigma1⟩ |- s ≈ a -> ⟨Theta2,Sigma2⟩ |- s ≈ a.
Proof.
intros HSty HStm H. revert Theta2 Sigma2 HSty HStm. induction H; intros Theta2 Sigma2 HSty HStm; eauto using tmrel, tyrel_mono;
constructor; eauto using tyrel_mono, vrm_mono, vext_mono.
Qed.
(* new *)
Corollary tmrel_weaken_ty Theta Sigma s a n m : ⟨Theta,Sigma⟩ |- s ≈ a -> ⟨(n,m) :: Theta,Sigma⟩ |- s ≈ a.
Proof. apply tmrel_mono; auto using incl_tl, incl_refl. Qed.
Corollary tmrel_weaken_tm Theta Sigma s a n m : ⟨Theta,Sigma⟩ |- s ≈ a -> ⟨Theta,(n,m) :: Sigma⟩ |- s ≈ a.
Proof. apply tmrel_mono; auto using incl_tl, incl_refl. Qed.
(* new: changed proof to incorporate type renaming. *)
Corollary tmrel_rs_ext Theta Sigma s a : ⟨Theta,Sigma⟩ |- s ≈ a -> ⟨vRS Theta,vEXT Sigma⟩ |- 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 Theta Sigma s a : ⟨Theta,Sigma⟩ |- s ≈ a -> ⟨ vEXT Theta, vRS Sigma ⟩ |- 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 (Theta1 Sigma1 : vrel) rho sigma tau (Theta2 Sigma2 : vrel) := (forall n m, Theta1 |- n ≃ m -> Theta2 |- rho n ∼ tau m) /\ (forall n m, Sigma1 |- n ≃ m -> ⟨Theta2,Sigma2⟩ |- sigma n ≈ tau m).
Lemma cm_tmrel_rs_ext Theta1 Sigma1 rho sigma tau Theta2 Sigma2 : cm_tmrel Theta1 Sigma1 rho sigma tau Theta2 Sigma2 -> cm_tmrel (vRS Theta1) (vEXT Sigma1) rho (up sigma) (up tau) (vRS Theta2) (vEXT Sigma2).
Proof.
intros CM. split.
- apply cm_tyrel_rs. intros n m. apply CM.
- intros n m [[En Em]| [n' [m' [[En Em] Rn'm']]]]%vext_inv; subst.
+ constructor. now left.
+ asimpl. now apply tmrel_rs_ext, CM.
Qed.
(* new *)
Lemma cm_tmrel_ext_rs Theta1 Sigma1 rho sigma tau Theta2 Sigma2 : cm_tmrel Theta1 Sigma1 rho sigma tau Theta2 Sigma2 -> cm_tmrel (vEXT Theta1) (vRS Sigma1) (up rho) (sigma >>| ren (+1)) (up tau) (vEXT Theta2) (vRS Sigma2).
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 Theta1 Sigma1 s a : ⟨Theta1,Sigma1⟩ |- s ≈ a -> forall rho sigma tau Theta2 Sigma2, cm_tmrel Theta1 Sigma1 rho sigma tau Theta2 Sigma2 -> ⟨Theta2,Sigma2⟩ |- s.|[rho].[sigma] ≈ a.[tau].
Proof.
intros H; induction H; intros rho sigma tau Theta2 Sigma2 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 Theta Sigma B b : ⟨Theta,Sigma⟩ |- B ≈ b -> cm_tmrel (vRS Theta) (vEXT Sigma) ids (B .: ids) (b .: ids) Theta Sigma.
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] Rn'm']]]]%vext_inv; subst; trivial. asimpl. now constructor.
Qed.
Lemma tmrel_beta_tm Theta Sigma s a t b : ⟨Theta,Sigma⟩ |- t ≈ b -> ⟨vRS Theta,vEXT Sigma⟩ |- s ≈ a -> ⟨Theta,Sigma⟩ |- 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.
Lemma tmrel_ren Theta Sigma s a rho xi zeta : ⟨Theta,Sigma⟩ |- s ≈ a -> ⟨vrm Theta rho zeta,vrm Sigma xi zeta⟩ |- s.|[ren rho].[ren xi] ≈ a.[ren zeta].
Proof.
intros H; revert rho xi zeta; induction H; intros rho xi zeta.
- 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 Theta1 Theta2 Sigma1 Sigma2 s a : Theta1 ⊑ Theta2 -> Sigma1 ⊑ Sigma2 -> ⟨Theta1,Sigma1⟩ |- s ≈ a -> ⟨Theta2,Sigma2⟩ |- s ≈ a.
Proof.
intros HSty HStm H. revert Theta2 Sigma2 HSty HStm. induction H; intros Theta2 Sigma2 HSty HStm; eauto using tmrel, tyrel_mono;
constructor; eauto using tyrel_mono, vrm_mono, vext_mono.
Qed.
(* new *)
Corollary tmrel_weaken_ty Theta Sigma s a n m : ⟨Theta,Sigma⟩ |- s ≈ a -> ⟨(n,m) :: Theta,Sigma⟩ |- s ≈ a.
Proof. apply tmrel_mono; auto using incl_tl, incl_refl. Qed.
Corollary tmrel_weaken_tm Theta Sigma s a n m : ⟨Theta,Sigma⟩ |- s ≈ a -> ⟨Theta,(n,m) :: Sigma⟩ |- s ≈ a.
Proof. apply tmrel_mono; auto using incl_tl, incl_refl. Qed.
(* new: changed proof to incorporate type renaming. *)
Corollary tmrel_rs_ext Theta Sigma s a : ⟨Theta,Sigma⟩ |- s ≈ a -> ⟨vRS Theta,vEXT Sigma⟩ |- 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 Theta Sigma s a : ⟨Theta,Sigma⟩ |- s ≈ a -> ⟨ vEXT Theta, vRS Sigma ⟩ |- 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 (Theta1 Sigma1 : vrel) rho sigma tau (Theta2 Sigma2 : vrel) := (forall n m, Theta1 |- n ≃ m -> Theta2 |- rho n ∼ tau m) /\ (forall n m, Sigma1 |- n ≃ m -> ⟨Theta2,Sigma2⟩ |- sigma n ≈ tau m).
Lemma cm_tmrel_rs_ext Theta1 Sigma1 rho sigma tau Theta2 Sigma2 : cm_tmrel Theta1 Sigma1 rho sigma tau Theta2 Sigma2 -> cm_tmrel (vRS Theta1) (vEXT Sigma1) rho (up sigma) (up tau) (vRS Theta2) (vEXT Sigma2).
Proof.
intros CM. split.
- apply cm_tyrel_rs. intros n m. apply CM.
- intros n m [[En Em]| [n' [m' [[En Em] Rn'm']]]]%vext_inv; subst.
+ constructor. now left.
+ asimpl. now apply tmrel_rs_ext, CM.
Qed.
(* new *)
Lemma cm_tmrel_ext_rs Theta1 Sigma1 rho sigma tau Theta2 Sigma2 : cm_tmrel Theta1 Sigma1 rho sigma tau Theta2 Sigma2 -> cm_tmrel (vEXT Theta1) (vRS Sigma1) (up rho) (sigma >>| ren (+1)) (up tau) (vEXT Theta2) (vRS Sigma2).
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 Theta1 Sigma1 s a : ⟨Theta1,Sigma1⟩ |- s ≈ a -> forall rho sigma tau Theta2 Sigma2, cm_tmrel Theta1 Sigma1 rho sigma tau Theta2 Sigma2 -> ⟨Theta2,Sigma2⟩ |- s.|[rho].[sigma] ≈ a.[tau].
Proof.
intros H; induction H; intros rho sigma tau Theta2 Sigma2 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 Theta Sigma B b : ⟨Theta,Sigma⟩ |- B ≈ b -> cm_tmrel (vRS Theta) (vEXT Sigma) ids (B .: ids) (b .: ids) Theta Sigma.
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] Rn'm']]]]%vext_inv; subst; trivial. asimpl. now constructor.
Qed.
Lemma tmrel_beta_tm Theta Sigma s a t b : ⟨Theta,Sigma⟩ |- t ≈ b -> ⟨vRS Theta,vEXT Sigma⟩ |- s ≈ a -> ⟨Theta,Sigma⟩ |- 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 Gamma :
SB.valid N Gamma -> exists Psi Theta Sigma,
SA.valid Psi /\ vr_func Theta /\ vr_inj Theta /\ vr_func Sigma /\ vr_inj Sigma /\ Theta ∥ Sigma /\
[Theta ; N ↦ Psi] /\ [Theta ; N ↤ Psi ] /\ [⟨Theta,Sigma⟩ ; Gamma ↦ Psi] /\ [⟨Theta,Sigma⟩ ; Gamma ↤ Psi].
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 (Psi & Theta & Sigma & V & Fty & Ity & Ftm & Itm & D & VCBAty & VCABty & VCBAtm & VCABtm).
assert (Hax : SA.hastype Psi ∗ ⬜) by (constructor; constructor).
assert (V' : SA.valid (∗ :: Psi)) by (econstructor; eauto).
apply vr_tmctx_BA_ext_rs in VCBAtm.
apply (vr_tmctx_AB_ext_rs V') in VCABtm. asimpl in *.
exists (∗ :: Psi), (vEXT Theta), (vRS Sigma).
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 (Psi & Theta & Sigma & 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 :: Psi)) by (econstructor; eauto).
exists (a :: Psi), (vRS Theta), (vEXT Sigma).
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 Psi :
SA.valid Psi -> exists N Gamma Theta Sigma,
SB.valid N Gamma /\ vr_func Theta /\ vr_inj Theta /\ vr_func Sigma /\ vr_inj Sigma /\ Theta ∥ Sigma /\
[Theta ; N ↦ Psi] /\ [Theta ; N ↤ Psi ] /\ [⟨Theta,Sigma⟩ ; Gamma ↦ Psi] /\ [⟨Theta,Sigma⟩ ; Gamma ↤ Psi].
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 :: Psi)) by (econstructor; eauto).
destruct IHvalid as (N & Gamma & Theta & Sigma & V & Fty & Ity & Ftm & Itm & D & VCBAty & VCABty & VCBAtm & VCABtm). destruct s.
+ destruct (tyrel_AB_tot_pres H0 H VCABty) as [A [RAa HA]].
assert (VA : SB.valid N (A :: Gamma)) by (econstructor; eauto).
exists N, (A :: Gamma), (vRS Theta), (vEXT Sigma).
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 H0) in H; subst.
exists (S N), Gamma..[ren (+1)], (vEXT Theta), (vRS Sigma).
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.
SB.valid N Gamma -> exists Psi Theta Sigma,
SA.valid Psi /\ vr_func Theta /\ vr_inj Theta /\ vr_func Sigma /\ vr_inj Sigma /\ Theta ∥ Sigma /\
[Theta ; N ↦ Psi] /\ [Theta ; N ↤ Psi ] /\ [⟨Theta,Sigma⟩ ; Gamma ↦ Psi] /\ [⟨Theta,Sigma⟩ ; Gamma ↤ Psi].
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 (Psi & Theta & Sigma & V & Fty & Ity & Ftm & Itm & D & VCBAty & VCABty & VCBAtm & VCABtm).
assert (Hax : SA.hastype Psi ∗ ⬜) by (constructor; constructor).
assert (V' : SA.valid (∗ :: Psi)) by (econstructor; eauto).
apply vr_tmctx_BA_ext_rs in VCBAtm.
apply (vr_tmctx_AB_ext_rs V') in VCABtm. asimpl in *.
exists (∗ :: Psi), (vEXT Theta), (vRS Sigma).
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 (Psi & Theta & Sigma & 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 :: Psi)) by (econstructor; eauto).
exists (a :: Psi), (vRS Theta), (vEXT Sigma).
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 Psi :
SA.valid Psi -> exists N Gamma Theta Sigma,
SB.valid N Gamma /\ vr_func Theta /\ vr_inj Theta /\ vr_func Sigma /\ vr_inj Sigma /\ Theta ∥ Sigma /\
[Theta ; N ↦ Psi] /\ [Theta ; N ↤ Psi ] /\ [⟨Theta,Sigma⟩ ; Gamma ↦ Psi] /\ [⟨Theta,Sigma⟩ ; Gamma ↤ Psi].
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 :: Psi)) by (econstructor; eauto).
destruct IHvalid as (N & Gamma & Theta & Sigma & V & Fty & Ity & Ftm & Itm & D & VCBAty & VCABty & VCBAtm & VCABtm). destruct s.
+ destruct (tyrel_AB_tot_pres H0 H VCABty) as [A [RAa HA]].
assert (VA : SB.valid N (A :: Gamma)) by (econstructor; eauto).
exists N, (A :: Gamma), (vRS Theta), (vEXT Sigma).
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 H0) in H; subst.
exists (S N), Gamma..[ren (+1)], (vEXT Theta), (vRS Sigma).
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 <-> exists 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) (Theta:=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 ∗ <-> exists 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 (Psi:=nil) (Theta:=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 <-> exists 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 (Sigma:=nil) (N:=0) (Gamma:=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 <-> exists 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 (Sigma:=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.
Theorem demo1 N Gamma s A : SB.valid N Gamma -> SB.hastype N Gamma s A -> SB.istype N A.
Proof.
intros V H. destruct (ctxrel_BA V) as (Psi & Theta & Sigma & Vp & Fty & Ity & _ & _ & _ & VCBAty & VCABty & VCBAtm & _).
eapply tmrel_BA_tot_pres with (Theta := Theta) in H as (_ & a & HAa & _ & _ & Ha); try eassumption.
eapply tyrel_AB_tot_pres in Ha as (A' & HA'a & J); try eassumption.
now rewrite (tyrel_inj Ity HAa HA'a).
Qed.
Proof.
intros V H. destruct (ctxrel_BA V) as (Psi & Theta & Sigma & Vp & Fty & Ity & _ & _ & _ & VCBAty & VCABty & VCBAtm & _).
eapply tmrel_BA_tot_pres with (Theta := Theta) in H as (_ & a & HAa & _ & _ & Ha); try eassumption.
eapply tyrel_AB_tot_pres in Ha as (A' & HA'a & J); try eassumption.
now rewrite (tyrel_inj Ity HAa HA'a).
Qed.
DEMO 2: Transport of beta-substitutivity from PTS to SysF
Theorem demo2 t B N Gamma s A: SB.valid N Gamma -> SB.hastype N Gamma t B -> SB.hastype N (B :: Gamma) s A -> SB.hastype N Gamma s.[t/] A.
Proof.
(* step 1: obtain suitable mapping relations and associated properties for the given valid context *)
intros (Psi & Theta & Sigma & 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 (Psi := b :: Psi) (Theta := vRS Theta) (Sigma := vEXT Sigma) 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 : ⟨ Theta, Sigma ⟩ |- 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' [RA'a [Ru [Hu _]]]]].
assert (E: A = A') by apply (tyrel_inj Ity RAa' RA'a). subst A'. clear RA'a.
assert (E: s.[t/] = u) by apply (tmrel_inj Ity Itm VD RJ Ru). subst u. clear Ru.
(* step 6: profit *)
assumption.
Qed.
Proof.
(* step 1: obtain suitable mapping relations and associated properties for the given valid context *)
intros (Psi & Theta & Sigma & 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 (Psi := b :: Psi) (Theta := vRS Theta) (Sigma := vEXT Sigma) 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 : ⟨ Theta, Sigma ⟩ |- 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' [RA'a [Ru [Hu _]]]]].
assert (E: A = A') by apply (tyrel_inj Ity RAa' RA'a). subst A'. clear RA'a.
assert (E: s.[t/] = u) by apply (tmrel_inj Ity Itm VD RJ Ru). subst u. clear Ru.
(* step 6: profit *)
assumption.
Qed.