(** The equivalence between PTS and PTSF.*) Require Import base. Require Import f_term f_env f_typ f_typ2 . Require Import ut_term ut_red ut_env ut_typ ut_sr ut_typ_eq. Require Import final_result. Require Import List Lt Le Gt Plus Minus Peano_dec Compare_dec. Require Import term red env typ_annot glue strip final_result. Module f_equiv_mod (X:term_sig) (Y:pts_sig X) (TM:term_mod X) (EM: env_mod X TM) (RM: red_mod X TM) (UTM:ut_term_mod X) (UEM: ut_env_mod X UTM) (URM: ut_red_mod X UTM) (PTS : ut_sr_mod X Y UTM UEM URM) (PTSe : ut_typ_eq_mod X Y UTM UEM URM PTS) (PTS_ATR: glue_mod X Y TM EM RM UTM UEM URM) (FTM: f_term_mod X) (FEM: f_env_mod X FTM). Import X Y UTM UEM URM TM EM RM PTS PTSe PTS_ATR FTM FEM. Include (final_mod X Y TM EM RM UTM UEM URM PTS PTSe PTS_ATR). Include (f_typ2_mod X Y FTM FEM UTM URM UEM PTS). (** tactics for PTSeq2PTSF*) (** This tactic will destruct an induction hypothesis H for the theorem PTSeq2PTSF, and then converts the context to Δ using context_conversion and then convert the types of the new terms to T. If Δ or T is empty, no conversion is done for that part.*) Ltac destruct_typ_equiv := fun H Δ T => let Γ := fresh "Γ" with HH := fresh "HH" with M := fresh "M" with N := fresh "N" with A := fresh "A" with eqΓ := fresh "eqΓ" with eqM := fresh "eqM" with eqN := fresh "eqN" with eqA := fresh "eqA" with HMN := fresh "HMN" with HM := fresh "HM" with HN := fresh "HN" with T0 := fresh "T" with S := fresh "S" with eqT := fresh "eqT" with eqS := fresh "eqS" with HT := fresh "HT" with H0 := fresh "H" with Hta := fresh "Hta" with HHta := fresh "HHta" with Δwf := fresh "Δwf" with eqΔ := fresh "eqΔ" with C := fresh "C" with D := fresh "D" with eqC := fresh "eqC" with eqD := fresh "eqD" with HCD := fresh "HCD" with hT := fresh "hT" with eqC1 := fresh "eqCC" with eqC2 := fresh "eqCCC" with T1 := fresh "TT" with eqT1 := fresh "eqTT" with HT1 := fresh "HHT" in match (type of H) with | exists _ _ _ _ _,_ => destruct H as (Γ&HH&M&N&A&eqΓ&eqM&eqN&eqA&HM&HN&HMN); match Δ with | True => match T with | True => idtac | _ => destruct (erasure_equality _ _ _ _ T _ HMN HM HN) as (T0&S&eqT&eqS&?HT&?HS&hT&HT);[eauto|try (left;eauto;fail);right;eauto| ]; rewrite eqM in eqT;rewrite eqN in eqS;clear M N eqM eqN HMN HM HN end | _ => assert (εc Δ = εc Γ) as eqΔ;[rewrite eqΓ;simpl;trivial;f_equal;trivial|]; destruct context_conversion as (temp1&temp2&_); assert (Δ⊣) as Δwf;[(eapply wf_typ;eassumption)||(eapply wf_cons;eassumption)|]; destruct (temp1 _ _ _ HM Δ Δwf) as (C&D&eqC&eqD&HCD);[symmetry;assumption|];rewrite eqM in eqC;rewrite eqA in eqD;clear HM; destruct (erasure_term _ T _ _ HCD) as (T0&eqT&HT);[eauto|try (left;eauto;fail);try (right;eauto;fail);eapply TypeCorrect;eassumption| ]; rewrite <- eqT in eqC;clear C D eqT eqD HCD; destruct (temp1 _ _ _ HN Δ Δwf) as (C&D&eqC1&eqD&HCD);[symmetry;assumption|];rewrite eqN in eqC1;rewrite eqA in eqD;clear HN; destruct (erasure_term _ T _ _ HCD) as (T1&eqT1&HT1);[eauto|try (left;eauto;fail);try (right;eauto;fail);eapply TypeCorrect;eassumption| ]; rewrite <- eqT1 in eqC1;clear C D eqT1 eqD HCD; destruct (temp2 _ _ _ _ HMN Δ Δwf) as (hT&C&D&eqC2&eqD&HCD);[symmetry;assumption|]; rewrite eqM in eqC2;rewrite <- eqC in eqC2;rewrite eqN in eqD;rewrite <- eqC1 in eqD; destruct (erasure_equality2 _ _ _ _ _ _ _ _ HCD HT HT1 eqC2 eqD); clear M N Γ temp1 temp2 Δwf eqM eqN C D eqC2 eqD HCD hT eqΔ eqΓ HMN end | _ => destruct H as (Γ&M&N&eqΓ&eqM&eqN&HMN); match Δ with | True => idtac | _ => assert (εc Δ = εc Γ) as eqΔ;[rewrite eqΓ;simpl;trivial;f_equal;trivial|]; destruct context_conversion as (temp&_&_); destruct (temp _ _ _ HMN Δ) as (C&D&eqC&eqD&HCD);[(eapply wf_typ;eassumption)||(eapply wf_cons;eassumption)|symmetry;assumption|clear temp]; try rewrite <- eqC in eqM;try rewrite <- eqD in eqN; clear M N Γ eqΓ eqΔ eqC eqD HMN;rename C into M, D into N,HCD into HMN end; match T with | True => idtac | _ => destruct (erasure_term _ T _ _ HMN) as (T0&eqT&HT);[eauto|try (left;eauto;fail);right;eauto| ]; rewrite <- eqT in eqM;clear M N eqT eqN HMN; rename eqM into eqT end end;subst. Ltac search_prod_equiv := let HeqX := fresh "HeqX" with Htp := fresh "Htp" with Hetp := fresh "Hetp" with s := fresh "s" in match goal with | eq : ε ?x = (Π (?A), ?B)%UT,HT : _ ⊢ _ : ?x |- _ => rewrite <- erasure_erasure_outer in eq at 1;remember (erasure_outer x) as X eqn:HeqX; destruct X;simpl in eq;try discriminate;[|symmetry in HeqX;apply erasure_outer_not_conv in HeqX; elim HeqX]; destruct (TypeCorrect _ _ _ HT) as [(?&Htp)|(s&Htp)];[subst;simpl in HeqX;discriminate|]; destruct (erasure_outer_typing _ _ _ Htp) as (?&Hetp); rewrite <- HeqX in Hetp; destruct (gen_pi _ _ _ _ Hetp) as (?s&?s&?s&?&_&?&?);injection eq;intros;subst end. (** The implication PTSeq -> PTSf*) Theorem PTSeq2PTSF : (forall Γ M N , Γ ⊢e M : N ->exists Γ' M' N' ,εc Γ'=Γ/\ε M'=M/\ε N'=N/\ Γ' ⊢ M' : N')/\ (forall Γ M N A, Γ ⊢e M = N : A->exists Γ' H M' N' A',εc Γ'=Γ/\ε M'=M/\ε N'=N/\ε A'=A/\Γ' ⊢ M' : A'/\Γ' ⊢ N' : A'/\Γ' ⊢ H : M' = N')/\ (forall Γ , Γ ⊣e ->exists Γ' ,εc Γ'=Γ/\ Γ' ⊣). apply (PTSe.typ_induc);intros. (*sort*) destruct H as (?&?&?). exists x,!s,!t;simpl;intuition. (*var*) destruct H as (?&?&?). destruct (erasure_item_lift_rev _ _ _ _ H i) as (?&?&?);subst. eexists x,#v,x0;simpl;intuition. (*prod*) destruct_typ_equiv H True !s. destruct_typ_equiv H0 (T::Γ0) !t. exists Γ0,(Π(T),T0),!u;intuition;eapply cProd;eassumption. (*abs*) destruct_typ_equiv H True !s1. destruct_typ_equiv H0 (T::Γ0) !s2. destruct_typ_equiv H1 (T::Γ0) T0. exists Γ0,(λ[T],T1),(Π(T),T0);intuition;eapply cAbs;eassumption. (*app*) destruct_typ_equiv H True True. search_prod_equiv. destruct (erasure_term _ (Π (X1), X2) _ _ HMN) as (T0&eqT&HT5);[rewrite <- erasure_erasure_outer at 1;rewrite HeqX;trivial|try (left;eauto;fail);right;eauto| ]. destruct_typ_equiv H0 Γ0 X1. exists Γ0,(T0·T),(X2 [ ← T]);simpl;rewrite erasure_subst;rewrite eqT;intuition;eapply cApp;eassumption. (*conv*) destruct_typ_equiv H True !s. destruct_typ_equiv H0 Γ0 T. exists Γ0,(T0∽hT),S;intuition;eapply cConv;eassumption. (*sort-eq*) destruct H as (?&?&?). eexists x,_,!s,!s,!t;intuition;eapply cRefl;eapply cSort;eassumption. (*var-eq*) destruct H as (?&?&?);destruct (erasure_item_lift_rev _ _ _ _ H i) as (?&?&?). eexists x,_,#v,#v,x0;intuition;eapply cRefl;eapply cVar;eassumption. (*prod-eq*) destruct_typ_equiv H True !s. destruct_typ_equiv H0 (T::Γ0) !t. assert (S :: Γ0 ⊢ (TT ↑ 1 # 1) [ ← #0 ∽ (hT †) ↑h 1] : !t). change !t with ((!t ↑ 1 # 1) [ ← #0 ∽ hT† ↑h 1]); eapply subst_typ; repeat (try eassumption;econstructor). edestruct erasure_injectivity_term. eexact HHT. eapply subst_typ;[eexact H0|eexact HT|repeat (try eassumption;econstructor)..]. rewrite erasure_lem2 at 1. rewrite erasure_lem2 at 1. reflexivity. eexists Γ0,_,(Π(T),T0),(Π(S),(TT ↑ 1 # 1) [ ← #0 ∽ hT† ↑h 1]),!u;intuition;try eapply cProd;try eassumption. simpl;f_equal;trivial. simpl;rewrite erasure_subst. change (ε (#0%F ∽ hT ↑h 1 †)) with (ε #0). rewrite <- erasure_subst; rewrite_l_rev erasure_lem1;f_equal;trivial. eapply cProdEq;try eassumption. eapply cTrans;[eexact H|eassumption]. (*abs-eq*) destruct_typ_equiv H True !s. destruct_typ_equiv H1 (T::Γ0) !t. destruct_typ_equiv H0 (T::Γ0) T0. assert (S :: Γ0 ⊢ (TT ↑ 1 # 1) [ ← #0 ∽ (hT †) ↑h 1] : (T0 ↑ 1 # 1) [ ← #0 ∽ hT† ↑h 1]). eapply subst_typ;repeat (try eassumption;econstructor). assert (S :: Γ0 ⊢ (T0 ↑ 1 # 1) [ ← #0 ∽ (hT †) ↑h 1] : !t). change !t with ((!t ↑ 1 # 1) [ ← #0 ∽ hT† ↑h 1]); eapply subst_typ;repeat (try eassumption;econstructor). edestruct erasure_injectivity_term. eexact HHT. eapply subst_typ; [eexact H0|eexact HT|repeat (try eassumption;econstructor)..]. rewrite erasure_lem2 at 1;rewrite erasure_lem2 at 1. reflexivity. assert (Γ0 ⊢ {hT †, [S]ρ(T0 ↑ 1 # 1) [ ← #0 ∽ (hT †) ↑h 1]} : Π (S), (T0 ↑ 1 # 1) [ ← #0 ∽ (hT †) ↑h 1] = Π (T), T0). repeat econstructor;try eassumption. subst. eexists Γ0,_,(λ[T],T1),((λ[S],(TT ↑ 1 # 1) [ ← #0 ∽ hT† ↑h 1])∽_),(Π(T),T0);intuition;try eapply cAbs;try eassumption. simpl;rewrite erasure_subst. change (ε (#0%F ∽ hT ↑h 1 †)) with (ε #0). rewrite <- erasure_subst; rewrite_l_rev erasure_lem1;f_equal;trivial. eapply cConv;[econstructor;eassumption..|eassumption]. eapply cTrans. Focus 2. eapply cIota. econstructor;eassumption. Focus 2. eassumption. econstructor;eassumption. eapply cAbsEq;try eassumption. eapply cTrans;[eexact H|eassumption]. (*app-eq*) destruct_typ_equiv H True True. search_prod_equiv. destruct (erasure_term _ (Π (X1), X2) _ _ HM) as (T0&eqT&HT5);[rewrite <- erasure_erasure_outer at 1;rewrite HeqX;trivial|try (left;eauto;fail);right;eauto| ]. destruct (erasure_term _ (Π (X1), X2) _ _ HN) as (T1&eqT1&HT6);[rewrite <- erasure_erasure_outer at 1;rewrite HeqX;trivial|try (left;eauto;fail);right;eauto| ]. edestruct erasure_equality2 as (L&HL). eexact HMN. eexact HT5. eexact HT6. symmetry;assumption. symmetry;assumption. destruct_typ_equiv H0 Γ0 X1. edestruct equality_subst as (K&HK); [eexact H2|eexact H|eassumption..|]. eexists Γ0,_,(T0·T),((T1·TT)∽_),(X2 [ ← T]);simpl;rewrite erasure_subst;rewrite eqT;rewrite eqT1;intuition. eapply cApp;eassumption. eapply cConv with (s:=s1). econstructor;eassumption. change (!s1) with (!s1 [ ← T]);eapply substitution;try eassumption. econstructor. econstructor;eassumption. eapply cSym;eassumption. eapply cTrans with (T1 · TT). eapply cAppEq;eassumption. eapply cIota with (s:=s1). econstructor;eassumption. Focus 2. econstructor;eassumption. change (!s1) with (!s1 [ ← T]). eapply substitution;try eassumption. econstructor. econstructor;eassumption. (*sym*) destruct_typ_equiv H True True. do 5 econstructor. intuition; eauto. (*trans*) destruct_typ_equiv H True True. destruct_typ_equiv H0 Γ0 A0. eapply erasure_injectivity_term in eqC as (?&?);[|eassumption..]. do 5 econstructor; intuition; eauto. (*conv-eq*) destruct_typ_equiv H True !s. destruct_typ_equiv H0 Γ0 T. eexists Γ0,_,(T0∽_),(TT∽_),S;intuition;[eapply cConv;eassumption..|]. eapply cTrans. eapply cSym;eapply cIota;try eassumption. eapply cTrans. eassumption. eapply cIota;try eassumption. (*beta*) destruct_typ_equiv H True !s. destruct_typ_equiv H2 Γ0 T. destruct_typ_equiv H0 (T::Γ0) !t. destruct_typ_equiv H1 (T::Γ0) T1. eexists Γ0,_,((λ [T], T2) · T0),(T2 [ ← T0]),(T1 [ ← T0]);intuition;try eapply erasure_subst. econstructor;[econstructor|];eassumption. eapply substitution;try eassumption. econstructor. econstructor;eassumption. eapply cBeta;eassumption. (*nil*) exists nil;intuition. (*cons*) destruct_typ_equiv H True !s. exists (T::Γ0);intuition;econstructor;eassumption. Qed. Theorem PTSl2PTSF : (forall Γ M N,(Γ ⊢' M : N)%UT -> exists Γ' M' N', εc Γ'=Γ/\ε M'=M/\ε N'=N/\Γ' ⊢ M' : N')/\ (forall Γ M N,(exists A B,(Γ ⊢' M : A)%UT/\(Γ ⊢' N : B)%UT/\ M ≡ N)-> exists Γ' M' N', εc Γ'=Γ/\ε M'=M/\ε N'=N/\Γ' ⊢ M' = N')/\ (forall Γ ,(exists M N,(Γ ⊢' M : N)%UT) -> exists Γ' , εc Γ'=Γ/\ Γ' ⊣). repeat split;intros. (*typ*) apply PTS.legacy2typ in H as (?&?). apply PTS_equiv_PTSe in H. apply PTSeq2PTSF in H. assumption. (*eq*) destruct H as (?&?&?&?&?). apply PTS.legacy2typ in H as (?&?);apply PTS.legacy2typ in H0 as (?&?). destruct (Betac_confl _ _ H1) as (?&?&?). set (SubjectRed _ _ _ H _ H4);set (SubjectRed _ _ _ H0 _ H5). destruct PTS_equiv_PTSe as (_&eq). destruct (eq Γ M x1 x) as (_&eq2). destruct (eq Γ x1 N x0) as (_&eq3). destruct PTSeq2PTSF as (_&eq2F&_). apply eq2F in eq2;[|repeat split;try assumption; econstructor;assumption]. apply eq2F in eq3;[|repeat split;try assumption;apply Betac_sym;econstructor;assumption]. destruct_typ_equiv eq2 True True. destruct_typ_equiv eq3 True True. destruct context_conversion as (_&temp&_). assert (Γ0⊣) as Γ0wf;[eapply wf_typ;eassumption|]. destruct (temp _ _ _ _ HMN0 Γ0 Γ0wf) as (hT&C&D&eqC2&eqD&HCD);[assumption|]. rewrite eqM in eqC2;symmetry in eqC2. edestruct equality_typing as ((?&?)&_). eexact HCD. destruct (erasure_injectivity_term _ _ _ _ _ HN H6 eqC2). do 3 econstructor. do 3 split. eassumption. econstructor. eapply cTrans. eassumption. eapply cTrans; eassumption. (*wf*) destruct H as (?&?&?). apply PTS.legacy2typ in H as (?&?). apply PTS_equiv_PTSe in H. apply PTSeq2PTSF in H as (?&?&?&?&?&?&?). subst;econstructor;repeat split. eapply wf_typ;eassumption. Qed. Theorem PTSF2PTSl : (forall Γ M N,Γ ⊢ M : N -> (εc Γ ⊢' ε M : ε N)%UT)/\ (forall Γ M N,Γ ⊢ M = N -> (exists A B,(εc Γ ⊢' ε M : A)%UT/\(εc Γ ⊢' ε N : B)%UT/\ ε M ≡ ε N))/\ (forall Γ ,Γ ⊣ -> (εc Γ ⊣')%UT). repeat split;intros. (*typ*) apply PTS.typ2legacy;apply PTSF2PTS;assumption. (*eq*) destruct H;edestruct equality_typing as ((?&?)&(?&?));[eexact H|]. do 2 econstructor;repeat split;try apply PTS.typ2legacy;try eapply PTSF2PTS;try eassumption. (*wf*) apply PTS.typ2legacy;apply PTSF2PTS;assumption. Qed. Theorem PTSlequivPTSF : (forall Γ M N,(Γ ⊢' M : N)%UT <-> exists Γ' M' N', εc Γ'=Γ/\ε M'=M/\ε N'=N/\Γ' ⊢ M' : N')/\ (forall Γ M N,(exists A B,(Γ ⊢' M : A)%UT/\(Γ ⊢' N : B)%UT/\ M ≡ N)<-> exists Γ' M' N', εc Γ'=Γ/\ε M'=M/\ε N'=N/\Γ' ⊢ M' = N')/\ (forall Γ ,(Γ ⊣')%UT <-> exists Γ' , εc Γ'=Γ/\ Γ' ⊣). repeat split;intros;try (eapply PTSl2PTSF;eassumption);try (destruct H as (?&?&?&?&?&?&?);subst;eapply PTSF2PTSl;eassumption); try (destruct H as (?&?&?);subst;eapply PTSF2PTSl;eassumption). destruct H. exists nil;repeat split;constructor. apply PTSl2PTSF in H as (?&?&?&?&?&?&?);subst. edestruct TypeCorrect as [(?&?)|(?&?)];[eexact H2| |]. subst;simpl in H1;injection H1;intros;subst. exists (x0::x);repeat split;econstructor;eassumption. edestruct erasure_injectivity_term_sort;[eexact H|eexact H1|]. edestruct equality_typing as (_&?&?);[eexact H0|]. edestruct gen_sort as (?&?&?);[eassumption| ]. subst. eexists (x0∽_::x);repeat split;do 2 econstructor;try eassumption. Qed. Theorem Prod_Injective : forall Γ A B A' B' H, Γ ⊢ H : Π(A), B = Π(A'), B' -> exists H K, Γ ⊢ H : A = A' /\ A::Γ ⊢ K : B = (B'↑1#1)[←#0∽H↑h1]. intros. edestruct equality_typing as ((?&?)&(?&?));[eexact H0|]. apply gen_pi in H1 as (?&?&?&?&?&?&?). apply gen_pi in H2 as (?&?&?&?&?&?&?);subst. destruct PTSF2PTSl as (Htyp&Heq&_). edestruct Heq as (_&_&_&_&?);[econstructor;eassumption|clear Heq]. simpl in *. edestruct URM.PiInj. eassumption. destruct PTSl2PTSF as (_&Heq&_). edestruct Heq as (?Γ&?A&?A'&?&?&?&?). do 2 econstructor;repeat split;[eapply Htyp;eexact H4|eapply Htyp;eexact H7|eassumption]. destruct H13. eapply context_conversion in H13 as (?&?&?&?&?&?);[rewrite H11 in H13;rewrite H12 in H14|eapply wf_typ;eexact H7|assumption]. edestruct equality_typing as ((?&?)&(?&?));[eexact H15|]. eapply erasure_injectivity_term in H13 as (?&?);[apply cSym in H13|eassumption..]. eapply erasure_injectivity_term in H14 as (?&?);[ |eassumption..]. assert (exists H,Γ ⊢ H : A = A') as (HH&?) by (econstructor;eapply cTrans;[eassumption|eapply cTrans;eassumption]). replace ε B' with (ε ((B'↑1#1)[←#0∽HH↑h1])) in H9 by (symmetry;apply erasure_lem2). assert (A :: Γ ⊢ (B' ↑ 1 # 1) [ ← #0 ∽ HH ↑h 1] : (!x5 ↑ 1 # 1) [ ← #0 ∽ HH ↑h 1]) as Btyp by (eapply subst_typ;[eassumption..|do 2 econstructor|econstructor]);simpl in Btyp. edestruct Heq as (?Γ&?B&?B'&?&?&?&?). do 2 econstructor;repeat split;[eapply Htyp;eexact H5|eapply Htyp;eassumption|eassumption]. destruct H22. eapply context_conversion in H22 as (?&?&?&?&?&?);[rewrite H20 in H22;rewrite H21 in H23|eapply wf_typ;eexact H5|assumption]. edestruct equality_typing as ((?&?)&(?&?));[eexact H24|]. eapply erasure_injectivity_term in H22 as (?&?);[apply cSym in H22|eassumption..]. eapply erasure_injectivity_term in H23 as (?&?);[ |eassumption..]. do 3 econstructor. eassumption. eapply cTrans;[eassumption|eapply cTrans;eassumption]. Qed. End f_equiv_mod.