RSC.stlcCorrespondence
(* (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 STLC_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.
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 STLC_spec.
Include FPTS (STLC_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 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.
Lemma prp_prp_contra Psi : ~ hastype Psi ∗ ∗.
Proof. intros H. apply hastype_srt_srt in H. inv H. 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.
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 a, valid Psi -> hastype Psi a ∗ -> Q Psi a.
Proof.
intros Qvar Qimp. intros Psi a V H. remember ∗ as b. rewrite Heqb in Qvar, Qimp.
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.
- exfalso. subst. destruct (hastype_beta_ty V H H0) as [_ [_ [_ [[] Hd]]]].
rewrite E in Hd. destruct (prp_prp_contra Hd).
- 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, valid Psi -> hastype Psi b ∗ -> hastype Psi a b -> Q Psi a b).
Proof.
intros Qvar Qapp Qlam. 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.
- destruct H. apply Qlam; 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.
(* Since the STLC cannot internalise type variables, we will be left with an all ∗ context after internalisation. *)
Fixpoint prps (n : nat) : list tm :=
match n with
| O => nil
| Datatypes.S m => ∗ :: prps m
end.
Lemma prps_valid n : valid (prps n).
Proof. induction n; eauto using valid. simpl. eapply valid_ext; eauto. econstructor. constructor. Qed.
Lemma prps_atnd n x a : atnd (prps n) x a -> a = ∗.
Proof.
intros H. remember (prps n) as Psi. revert n HeqPsi. induction H; intros [|n] E; try discriminate E; cbn in E.
- now inv E.
- subst. inv E. now rewrite (IHatnd n (eq_refl _)).
Qed.
Fixpoint prps (n : nat) : list tm :=
match n with
| O => nil
| Datatypes.S m => ∗ :: prps m
end.
Lemma prps_valid n : valid (prps n).
Proof. induction n; eauto using valid. simpl. eapply valid_ext; eauto. econstructor. constructor. Qed.
Lemma prps_atnd n x a : atnd (prps n) x a -> a = ∗.
Proof.
intros H. remember (prps n) as Psi. revert n HeqPsi. induction H; intros [|n] E; try discriminate E; cbn in E.
- now inv E.
- subst. inv E. now rewrite (IHatnd n (eq_refl _)).
Qed.
REMARK:
Internalisation should technically be possible for this system, but due to the mixed nature of dependent PTS contexts a development would be rather involved, since permutations are required to sort such contexts as a first step (and proof this correct). Since we furtehr observe that the statements for closed judgements are only marginally useful, the additional effort does not justify this detour.Include STLC_spec.
(* Include M. *)
End SA.
Notation "∗" := (SA.Srt SA.Prp).
Notation "⬜" := (SA.Srt SA.Typ).
Require stlc.
Module SB.
Include stlc.
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
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.
Qed.
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.
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.
Qed.
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.
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.
(* only needed for STLC *)
Lemma vr_tyctx_BA_idR N : [idR N ; N ↦ SA.prps N].
Proof. induction N; cbn; eauto using vr_tyctx_BA_nil, vr_tyctx_BA_ext. 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.
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.
(* only needed for STLC *)
Lemma vr_tyctx_AB_idR N : [idR N ; N ↤ SA.prps N].
Proof. induction N; cbn; eauto using vr_tyctx_AB_nil, vr_tyctx_AB_ext. 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.
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.
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.
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.
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.
Qed.
Lemma tyrel_unmap R A a xi zeta : vrm R xi zeta |- A ∼ a -> exists A' a', A = A'.[ren xi] /\ a = a'.[ren zeta] /\ R |- A' ∼ a'.
Proof.
intros H. remember (vrm R xi zeta) as R'. revert R xi zeta HeqR'. 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.
Qed.
Corollary tyrel_vrs_inv R A a : vRS R |- A ∼ a -> exists2 a', a = a'.[ren (+1)] & R |- 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.
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.
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.
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.
Qed.
Lemma tyrel_unmap R A a xi zeta : vrm R xi zeta |- A ∼ a -> exists A' a', A = A'.[ren xi] /\ a = a'.[ren zeta] /\ R |- A' ∼ a'.
Proof.
intros H. remember (vrm R xi zeta) as R'. revert R xi zeta HeqR'. 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.
Qed.
Corollary tyrel_vrs_inv R A a : vRS R |- A ∼ a -> exists2 a', a = a'.[ren (+1)] & R |- 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
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
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.
Qed.
Lemma tmrel_inj Theta Sigma : vr_inj Theta -> vr_inj Sigma -> rel_inj (tmrel Theta Sigma).
Proof.
intros Rtyi Rtmi s1 s2 a H. revert s2. induction H; intros A' J; inv J.
- now rewrite (Rtmi _ _ _ H H2).
- f_equal; auto.
- f_equal; eauto using vr_inj_rs, vr_inj_ext. eapply (tyrel_inj Rtyi); eassumption.
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.
Qed.
Lemma tmrel_inj Theta Sigma : vr_inj Theta -> vr_inj Sigma -> rel_inj (tmrel Theta Sigma).
Proof.
intros Rtyi Rtmi s1 s2 a H. revert s2. induction H; intros A' J; inv J.
- now rewrite (Rtmi _ _ _ H H2).
- f_equal; auto.
- f_equal; eauto using vr_inj_rs, vr_inj_ext. eapply (tyrel_inj Rtyi); eassumption.
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.
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.
(* only needed for STLC *)
Lemma vr_tmctx_AB_prps N Gamma Theta Sigma : [⟨Theta,Sigma⟩ ; Gamma ↤ SA.prps N].
Proof. intros y a L H. apply SA.prps_atnd in L. subst. destruct (SA.prp_prp_contra 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.
- intros Psi a b c d d' V Ha _ _ 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 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.
Qed.
Substitution Theory for tmrel
Lemma tmrel_ren Theta Sigma s a xi zeta : ⟨Theta,Sigma⟩ |- s ≈ a -> ⟨vrm Theta id zeta,vrm Sigma xi zeta⟩ |- s.[ren xi] ≈ a.[ren zeta].
Proof.
intros H; revert xi zeta; induction H; intros xi zeta.
- constructor. eapply vr_map; eauto.
- constructor; auto.
- asimpl. constructor.
+ replace A with (A.[ren id]) by autosubst. now apply tyrel_ren.
+ rewrite vrm_ext, vrm_rs. auto.
Qed.
Lemma tmrel_mono_tm Theta Sigma1 Sigma2 s a : Sigma1 ⊑ Sigma2 -> ⟨Theta,Sigma1⟩ |- s ≈ a -> ⟨Theta,Sigma2⟩ |- s ≈ a.
Proof.
intros HS H. revert Sigma2 HS. induction H; intros Sigma2 HS; eauto using tmrel, vr_mono.
constructor; eauto using vext_mono.
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_tm; auto using incl_tl, incl_refl. Qed.
Corollary tmrel_rs_ext Theta Sigma s a : ⟨Theta,Sigma⟩ |- s ≈ a -> ⟨vRS Theta,vEXT Sigma⟩ |- s.[ren (+1)] ≈ a.[ren (+1)].
Proof. intros. now apply tmrel_weaken_tm, 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.
Lemma tmrel_subst_tm Theta1 Sigma1 s a : ⟨Theta1,Sigma1⟩ |- s ≈ a -> forall sigma tau Theta2 Sigma2, cm_tmrel Theta1 Sigma1 ids sigma tau Theta2 Sigma2 -> ⟨Theta2,Sigma2⟩ |- s.[sigma] ≈ a.[tau].
Proof.
intros H; induction H; intros sigma tau Theta2 Sigma2 CM.
- destruct CM. asimpl; eauto.
- constructor; auto.
- asimpl. constructor.
+ replace A with A.[ids] by autosubst. eapply tyrel_subst; eauto. destruct CM as [CM _]. exact CM.
+ pose proof (cm_tmrel_rs_ext 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.
- intros [m' Em Rnm']%vrs_inv. subst. asimpl. now constructor.
- intros [[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. eapply tmrel_subst_tm; eauto using cm_tmrel_beta_tm. Qed.
Proof.
intros H; revert xi zeta; induction H; intros xi zeta.
- constructor. eapply vr_map; eauto.
- constructor; auto.
- asimpl. constructor.
+ replace A with (A.[ren id]) by autosubst. now apply tyrel_ren.
+ rewrite vrm_ext, vrm_rs. auto.
Qed.
Lemma tmrel_mono_tm Theta Sigma1 Sigma2 s a : Sigma1 ⊑ Sigma2 -> ⟨Theta,Sigma1⟩ |- s ≈ a -> ⟨Theta,Sigma2⟩ |- s ≈ a.
Proof.
intros HS H. revert Sigma2 HS. induction H; intros Sigma2 HS; eauto using tmrel, vr_mono.
constructor; eauto using vext_mono.
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_tm; auto using incl_tl, incl_refl. Qed.
Corollary tmrel_rs_ext Theta Sigma s a : ⟨Theta,Sigma⟩ |- s ≈ a -> ⟨vRS Theta,vEXT Sigma⟩ |- s.[ren (+1)] ≈ a.[ren (+1)].
Proof. intros. now apply tmrel_weaken_tm, 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.
Lemma tmrel_subst_tm Theta1 Sigma1 s a : ⟨Theta1,Sigma1⟩ |- s ≈ a -> forall sigma tau Theta2 Sigma2, cm_tmrel Theta1 Sigma1 ids sigma tau Theta2 Sigma2 -> ⟨Theta2,Sigma2⟩ |- s.[sigma] ≈ a.[tau].
Proof.
intros H; induction H; intros sigma tau Theta2 Sigma2 CM.
- destruct CM. asimpl; eauto.
- constructor; auto.
- asimpl. constructor.
+ replace A with A.[ids] by autosubst. eapply tyrel_subst; eauto. destruct CM as [CM _]. exact CM.
+ pose proof (cm_tmrel_rs_ext 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.
- intros [m' Em Rnm']%vrs_inv. subst. asimpl. now constructor.
- intros [[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. eapply tmrel_subst_tm; eauto using cm_tmrel_beta_tm. 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 ; N ↦ Psi] /\ [Theta ; N ↤ Psi ] /\ [⟨Theta,Sigma⟩ ; Gamma ↦ Psi] /\ [⟨Theta,Sigma⟩ ; Gamma ↤ Psi].
Proof.
intros H; induction H.
- exists (SA.prps N), (idR N), nil.
repeat split; eauto using SA.prps_valid, vr_func_nil, vr_inj_nil, vr_func_idR, vr_inj_idR, vr_tyctx_BA_idR, vr_tyctx_AB_idR, vr_tmctx_BA_nil, vr_tmctx_AB_prps.
- destruct IHvalid as (Psi & Theta & Sigma & V & Fty & Ity & Ftm & Itm & 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, 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 ; 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_nil, 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 & 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, 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,
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 ; N ↦ Psi] /\ [Theta ; N ↤ Psi ] /\ [⟨Theta,Sigma⟩ ; Gamma ↦ Psi] /\ [⟨Theta,Sigma⟩ ; Gamma ↤ Psi].
Proof.
intros H; induction H.
- exists (SA.prps N), (idR N), nil.
repeat split; eauto using SA.prps_valid, vr_func_nil, vr_inj_nil, vr_func_idR, vr_inj_idR, vr_tyctx_BA_idR, vr_tyctx_AB_idR, vr_tmctx_BA_nil, vr_tmctx_AB_prps.
- destruct IHvalid as (Psi & Theta & Sigma & V & Fty & Ity & Ftm & Itm & 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, 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 ; 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_nil, 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 & 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, 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,
vr_tyctx_BA_ext, vr_tyctx_AB_ext, vr_tmctx_BA_ext_rs, vr_tmctx_AB_ext_rs.
Qed.
Correspondence for Closed Judgements
Since the STLC cannot internalise type variables, the follwoing four theorems are the closest we can get to a correspondence of closed judgemnts, using an all ∗ PTS context of size N which is related via an identity relation to the STLC context N;nil.Theorem tyrel_BA_total_preserving N A : SB.istype N A <-> exists a, idR N |- A ∼ a /\ SA.hastype (SA.prps N) a ∗.
Proof.
split.
- intros. now eapply tyrel_BA_tot_pres, vr_tyctx_BA_idR.
- intros [a [RA Ha]]. eapply tyrel_AB_tot_pres in Ha as [A' [RA' H]]; auto using vr_tyctx_AB_idR, SA.prps_valid.
now rewrite (tyrel_inj (vr_inj_idR _) RA RA').
Qed.
Theorem tyrel_AB_total_preserving N a : SA.hastype (SA.prps N) a ∗ <-> exists A, idR N |- A ∼ a /\ SB.istype N A.
Proof.
split.
- intros. now eapply (tyrel_AB_tot_pres (SA.prps_valid _)), vr_tyctx_AB_idR.
- intros [A [Ra HA]]. eapply tyrel_BA_tot_pres in HA as [a' [Ra' H]]; auto using vr_tyctx_BA_idR.
now rewrite (tyrel_func (vr_func_idR _) Ra Ra').
Qed.
Theorem tmrel_BA_total_preserving N s A : SB.hastype N nil s A <-> exists b a, idR N |- A ∼ a /\ ⟨idR N,nil⟩ |- s ≈ b /\ SA.hastype (SA.prps N) b a /\ SA.hastype (SA.prps N) a ∗.
Proof.
split.
- intros. eapply tmrel_BA_tot_pres; eauto using vr_func_nil, vr_func_idR, vr_tyctx_BA_idR, vr_tmctx_BA_nil, SA.prps_valid.
- intros [b [a [RA [Rs [Hb Ha]]]]].
eapply tmrel_AB_tot_pres with (Sigma:=nil) (Gamma:=nil) in Hb as [s' [A' [RA' [Rs' [Hs' HA']]]]];
eauto using vr_inj_idR, vr_tyctx_AB_idR, vr_tmctx_AB_prps, SA.prps_valid.
now rewrite (tyrel_inj (vr_inj_idR _) RA RA'), (tmrel_inj (vr_inj_idR _) vr_inj_nil Rs Rs').
Qed.
Theorem tmrel_AB_total_preserving N a b : SA.hastype (SA.prps N) a ∗ /\ SA.hastype (SA.prps N) b a <-> exists s A, idR N |- A ∼ a /\ ⟨idR N,nil⟩ |- s ≈ b /\ SB.hastype N nil s A /\ SB.istype N A.
Proof.
split.
- intros [Hb Ha]. eapply tmrel_AB_tot_pres; eauto using vr_inj_idR, vr_tyctx_AB_idR, vr_tmctx_AB_prps, SA.prps_valid.
- 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_idR, vr_tyctx_BA_idR, vr_tmctx_BA_nil, SA.prps_valid.
now rewrite (tyrel_func (vr_func_idR _) Rb Rb'), (tmrel_func (vr_func_idR _) 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 STLC
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 & 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 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 & 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 RJ Ru). subst u. clear Ru.
(* step 6: profit *)
assumption.
Qed.