SysF_PTS.sysf_pts
(* (c) 2016, Jonas Kaiser & Tobias Tebbi *)
Equivalence of System F and System L in Coq based on Context Morphism Lemmas
Require Import Omega List Program.Equality.
From Autosubst Require Export Autosubst.
Require Import Decidable lib.
Set Implicit Arguments.
Inductive typeF : Type :=
| TyVarF (x : var)
| ImpF (A B : typeF)
| AllF (A : {bind typeF}).
Inductive termF : Type :=
| TmVarF (x : var)
| AppF (s t : termF)
| LamF (A : typeF) (s : {bind termF})
| TySpecF (s : termF) (A : typeF)
| TyAbsF (s : {bind typeF in termF}).
| TyVarF (x : var)
| ImpF (A B : typeF)
| AllF (A : {bind typeF}).
Inductive termF : Type :=
| TmVarF (x : var)
| AppF (s t : termF)
| LamF (A : typeF) (s : {bind termF})
| TySpecF (s : termF) (A : typeF)
| TyAbsF (s : {bind typeF in termF}).
Decidable Equality on the type and term syntax
Instance decide_eq_typeF (A B : typeF) : Dec (A = B). derive. Defined.
Instance decide_eq_termF (s t : termF) : Dec (s = t). derive. Defined.
Instance decide_eq_termF (s t : termF) : Dec (s = t). derive. Defined.
Autosubst machinery
Instance Ids_typeF : Ids typeF. derive. Defined.
Instance Rename_typeF : Rename typeF. derive. Defined.
Instance Subst_typeF : Subst typeF. derive. Defined.
Instance SubstLemmas_typeF : SubstLemmas typeF. derive. Qed.
Instance HSubst_termF : HSubst typeF termF. derive. Defined.
Instance Ids_termF : Ids termF. derive. Defined.
Instance Rename_termF : Rename termF. derive. Defined.
Instance Subst_termF : Subst termF. derive. Defined.
Instance HSubstLemmas_termF : HSubstLemmas typeF termF. derive. Qed.
Instance SubstHSubstComp_typeF_termF : SubstHSubstComp typeF termF. derive. Qed.
Instance SubstLemmas_termF : SubstLemmas termF. derive. Qed.
(* s.|tau.sigma is written stau,sigma in the paper, here are the reduction rules for reference *)
Goal forall x sigma tau, (TmVarF x).|[tau].[sigma] = sigma(x). autosubst. Qed.
Goal forall s t sigma tau, (AppF s t).|[tau].[sigma] = AppF s.|[tau].[sigma] t.|[tau].[sigma]. autosubst. Qed.
Goal forall A s sigma tau, (LamF A s).|[tau].[sigma] = LamF A.[tau] s.|[tau].[up sigma]. autosubst. Qed.
Goal forall s A sigma tau, (TySpecF s A).|[tau].[sigma] = TySpecF s.|[tau].[sigma] A.[tau]. autosubst. Qed.
Goal forall s sigma tau, (TyAbsF s).|[tau].[sigma] = TyAbsF s.|[up tau].[sigma >>| (ren (+1))]. autosubst. Qed.
Instance Rename_typeF : Rename typeF. derive. Defined.
Instance Subst_typeF : Subst typeF. derive. Defined.
Instance SubstLemmas_typeF : SubstLemmas typeF. derive. Qed.
Instance HSubst_termF : HSubst typeF termF. derive. Defined.
Instance Ids_termF : Ids termF. derive. Defined.
Instance Rename_termF : Rename termF. derive. Defined.
Instance Subst_termF : Subst termF. derive. Defined.
Instance HSubstLemmas_termF : HSubstLemmas typeF termF. derive. Qed.
Instance SubstHSubstComp_typeF_termF : SubstHSubstComp typeF termF. derive. Qed.
Instance SubstLemmas_termF : SubstLemmas termF. derive. Qed.
(* s.|tau.sigma is written stau,sigma in the paper, here are the reduction rules for reference *)
Goal forall x sigma tau, (TmVarF x).|[tau].[sigma] = sigma(x). autosubst. Qed.
Goal forall s t sigma tau, (AppF s t).|[tau].[sigma] = AppF s.|[tau].[sigma] t.|[tau].[sigma]. autosubst. Qed.
Goal forall A s sigma tau, (LamF A s).|[tau].[sigma] = LamF A.[tau] s.|[tau].[up sigma]. autosubst. Qed.
Goal forall s A sigma tau, (TySpecF s A).|[tau].[sigma] = TySpecF s.|[tau].[sigma] A.[tau]. autosubst. Qed.
Goal forall s sigma tau, (TyAbsF s).|[tau].[sigma] = TyAbsF s.|[up tau].[sigma >>| (ren (+1))]. autosubst. Qed.
Type Formation Judgement
Inductive istyF (N : nat) : typeF -> Prop :=
| istyF_var x : x < N -> istyF N (TyVarF x)
| istyF_imp A B : istyF N A -> istyF N B -> istyF N (ImpF A B)
| istyF_all A : istyF (1+N) A -> istyF N (AllF A).
| istyF_var x : x < N -> istyF N (TyVarF x)
| istyF_imp A B : istyF N A -> istyF N B -> istyF N (ImpF A B)
| istyF_all A : istyF (1+N) A -> istyF N (AllF A).
Typing Judgment
Inductive typingF (N : nat) (Gamma : list typeF) : termF -> typeF -> Prop :=
| typingF_var x A :
atn Gamma x A -> istyF N A ->
typingF N Gamma (TmVarF x) A
| typingF_app s t A B :
typingF N Gamma s (ImpF A B) -> typingF N Gamma t A ->
typingF N Gamma (AppF s t) B
| typingF_lam s A B :
istyF N A -> typingF N (A :: Gamma) s B ->
typingF N Gamma (LamF A s) (ImpF A B)
| typingF_tyspec s A A' B :
istyF N B -> typingF N Gamma s (AllF A) -> A' = A.[B/] ->
typingF N Gamma (TySpecF s B) A'
| typingF_tyabs s A :
typingF (1 + N) Gamma..[ren (+1)] s A ->
typingF N Gamma (TyAbsF s) (AllF A).
| typingF_var x A :
atn Gamma x A -> istyF N A ->
typingF N Gamma (TmVarF x) A
| typingF_app s t A B :
typingF N Gamma s (ImpF A B) -> typingF N Gamma t A ->
typingF N Gamma (AppF s t) B
| typingF_lam s A B :
istyF N A -> typingF N (A :: Gamma) s B ->
typingF N Gamma (LamF A s) (ImpF A B)
| typingF_tyspec s A A' B :
istyF N B -> typingF N Gamma s (AllF A) -> A' = A.[B/] ->
typingF N Gamma (TySpecF s B) A'
| typingF_tyabs s A :
typingF (1 + N) Gamma..[ren (+1)] s A ->
typingF N Gamma (TyAbsF s) (AllF A).
Terms
Inductive termL : Type :=
| VarL (x : var)
| ProdL (a : termL) (b : {bind termL})
| AppL (a b : termL)
| LamL (a : termL) (b : {bind termL})
| SortL (u : level).
| VarL (x : var)
| ProdL (a : termL) (b : {bind termL})
| AppL (a b : termL)
| LamL (a : termL) (b : {bind termL})
| SortL (u : level).
Decidable Equality on the Term Syntax
Instance decide_eq_level (u v : level) : Dec (u = v). derive. Defined.
Instance decide_eq_termL (a b : termL) : Dec (a = b). derive. Defined.
Instance decide_eq_termL (a b : termL) : Dec (a = b). derive. Defined.
Autosubst machinery
Instance Ids_termL : Ids termL. derive. Defined.
Instance Rename_termL : Rename termL. derive. Defined.
Instance Subst_termL : Subst termL. derive. Defined.
Instance SubstLemmas_termL : SubstLemmas termL. derive. Qed.
Instance Rename_termL : Rename termL. derive. Defined.
Instance Subst_termL : Subst termL. derive. Defined.
Instance SubstLemmas_termL : SubstLemmas termL. derive. Qed.
Inductive typingL (Gamma : list termL) : termL -> termL -> Prop :=
| typingL_ax :
typingL Gamma (SortL Prp) (SortL Typ)
| typingL_var x a u :
atnd Gamma x a -> typingL Gamma a (SortL u) ->
typingL Gamma (VarL x) a
| typingL_prod a b u :
typingL Gamma a (SortL u) -> typingL (a :: Gamma) b (SortL Prp) ->
typingL Gamma (ProdL a b) (SortL Prp)
| typingL_app a b c d d' :
typingL Gamma a (ProdL c d) -> typingL Gamma b c -> d' = d.[b/] ->
typingL Gamma (AppL a b) d'
| typingL_lam a b c u :
typingL Gamma a (SortL u) ->
typingL (a :: Gamma) c (SortL Prp) ->
typingL (a :: Gamma) b c ->
typingL Gamma (LamL a b) (ProdL a c).
Inductive istyP Gamma : termL -> Prop :=
| istyP_var x :
atnd Gamma x (SortL Prp) ->
istyP Gamma (VarL x)
| istyP_prod1 a :
istyP ((SortL Prp) :: Gamma) a ->
istyP Gamma (ProdL (SortL Prp) a)
| istyP_prod2 a b :
istyP Gamma a -> istyP (a :: Gamma) b ->
istyP Gamma (ProdL a b).
Inductive typingP Gamma : termL -> termL -> Prop :=
| typingP_var x a :
atnd Gamma x a -> istyP Gamma a ->
typingP Gamma (VarL x) a
| typingP_app1 a b c d d' :
typingP Gamma a (ProdL c d) -> typingP Gamma b c -> d' = d.[b/] ->
typingP Gamma (AppL a b) d'
| typingP_lam1 a b c :
istyP Gamma a -> typingP (a :: Gamma) b c ->
typingP Gamma (LamL a b) (ProdL a c)
| typingP_app2 a b b' c :
typingP Gamma a (ProdL (SortL Prp) b) -> istyP Gamma c -> b' = b.[c/] ->
typingP Gamma (AppL a c) b'
| typingP_lam2 a b :
typingP ((SortL Prp) :: Gamma) a b ->
typingP Gamma (LamL (SortL Prp) a) (ProdL (SortL Prp) b).
Definition cr_istyF (rho xi : var -> var) N M := forall x, istyF N (TyVarF (rho x)) -> istyF M (TyVarF (xi x)).
Lemma cr_istyF_id N : cr_istyF id id N N.
Proof. intros n. auto. Qed.
Lemma cr_istyF_up rho xi N M : cr_istyF rho xi N M -> cr_istyF (upren rho) (upren xi) (1 + N) (1 + M).
Proof.
intros CR [|n] L; asimpl in *.
- constructor. omega.
- ainv. cut (rho n < N); [intros H|omega]. aspec. constructor. ainv. omega.
Qed.
Lemma istyF_ren N A rho:
istyF N A.[ren rho] -> forall M xi, cr_istyF rho xi N M -> istyF M A.[ren xi].
Proof.
intros H. depind H; intros M xi CR; destruct A; ainv.
- apply CR. now constructor.
- constructor; eauto.
- constructor. asimpl. eapply IHistyF; eauto using cr_istyF_up. autosubst.
Qed.
Lemma cr_istyF_shift N : cr_istyF id (+1) N (1 + N).
Proof. intros n H. asimpl in *. ainv. constructor. omega. Qed.
Lemma cr_istyF_ushift N : cr_istyF (+1) id (1 + N) N.
Proof. intros n H. asimpl in *. ainv. constructor. omega. Qed.
Corollary istyF_weaken N A: istyF N A -> istyF (1 + N) A.[ren (+1)].
Proof. intros H. eapply istyF_ren; eauto using cr_istyF_shift. now asimpl. Qed.
Corollary istyF_strengthen N A: istyF (1 + N) A.[ren (+1)] -> istyF N A.
Proof. intros H. eapply istyF_ren in H; eauto using cr_istyF_ushift. now asimpl in *. Qed.
Definition cr_typingF zeta N Gamma Delta := forall x A, typingF N Gamma (TmVarF x) A -> typingF N Delta (TmVarF (zeta x)) A.
Lemma cr_typingF_id N Gamma : cr_typingF id N Gamma Gamma.
Proof. intros n A. auto. Qed.
Lemma cr_typingF_up A zeta N Gamma Delta :
cr_typingF zeta N Gamma Delta -> cr_typingF (upren zeta) N (A :: Gamma) (A :: Delta).
Proof.
intros CR [|n] B L; ainv; asimpl.
- constructor; trivial. constructor.
- constructor; trivial. constructor.
cut (typingF N Gamma (TmVarF n) B); [intros J| now constructor]. apply CR in J. ainv.
Qed.
Lemma cr_typingF_ren zeta N Gamma Delta :
cr_typingF zeta N Gamma Delta ->
forall M xi, cr_istyF xi id M N -> cr_typingF zeta M Gamma..[ren xi] Delta..[ren xi].
Proof.
intros CR2 M xi CR1. intros x B L. inversion L; subst.
destruct (mmap_atn H0) as [B' [EB' L']]; subst.
assert (H2' : istyF N B'). eapply istyF_ren in H1; eauto. now asimpl in *.
assert (H3 : typingF N Gamma (TmVarF x) B') by now constructor.
apply CR2 in H3. inversion H3; subst.
constructor; trivial. eapply atn_mmap; eauto.
Qed.
Corollary cr_typingF_ren_ushift zeta N Gamma Delta :
cr_typingF zeta N Gamma Delta -> cr_typingF zeta (1 + N) Gamma..[ren (+1)] Delta..[ren (+1)].
Proof. intros CR. eapply cr_typingF_ren; eauto using cr_istyF_ushift. Qed.
Lemma typingF_ren N Gamma s A:
typingF N Gamma s A ->
forall M Delta xi zeta,
cr_istyF id xi N M ->
cr_typingF zeta N Gamma Delta ->
typingF M Delta..[ren xi] s.[ren zeta].|[ren xi] A.[ren xi].
Proof.
intros H. induction H; intros M Delta xi zeta CR1 CR2; subst; asimpl.
- constructor.
+ eapply atn_mmap; eauto.
cut (typingF N Gamma (TmVarF x) A); [intros J | now constructor].
apply CR2 in J. ainv.
+ eapply istyF_ren; eauto. now asimpl.
- econstructor.
+ specialize (IHtypingF1 _ _ _ _ CR1 CR2); asimpl in *; eauto.
+ specialize (IHtypingF2 _ _ _ _ CR1 CR2); asimpl in *; eauto.
- constructor.
+ eapply istyF_ren; eauto. now asimpl.
+ apply cr_typingF_up with (A:=A) in CR2.
specialize (IHtypingF _ _ _ _ CR1 CR2). asimpl in *; eauto.
- econstructor.
+ eapply istyF_ren; eauto. now asimpl.
+ specialize (IHtypingF _ _ _ _ CR1 CR2). asimpl in *; eauto.
+ autosubst.
- constructor. asimpl.
replace (Delta..[ren (xi >>> (+1))]) with (Delta..[ren (+1)]..[ren (upren xi)]) by autosubst.
replace (s.|[ren (upren xi)].[ren zeta]) with (s.[ren zeta].|[ren (upren xi)]) by autosubst.
apply IHtypingF.
+ apply cr_istyF_up in CR1. now asimpl in *.
+ now apply cr_typingF_ren_ushift.
Qed.
Lemma cr_typingF_shift B N Gamma : cr_typingF (+1) N Gamma (B :: Gamma).
Proof. intros n A H. ainv. constructor; trivial. now constructor. Qed.
Corollary typingF_weaken B N Gamma s A:
typingF N Gamma s A -> typingF N (B :: Gamma) s.[ren (+1)] A.
Proof.
intros H.
pose proof (typingF_ren H (@cr_istyF_id N) (@cr_typingF_shift B N Gamma)) as J.
asimpl in *. now replace (mmap id Gamma) with Gamma in J by autosubst.
Qed.
Corollary typingF_ren_ty N Gamma s A:
typingF N Gamma s A ->
forall M xi, cr_istyF id xi N M ->
typingF M Gamma..[ren xi] s.|[ren xi] A.[ren xi].
Proof.
intros H M xi CR. pose proof (typingF_ren H CR (@cr_typingF_id N Gamma)) as J.
now asimpl in *.
Qed.
Corollary typingF_weaken_ty N Gamma s A :
typingF N Gamma s A -> typingF (1 + N) Gamma..[ren (+1)] s.|[ren (+1)] A.[ren (+1)].
Proof. intros H. eapply typingF_ren_ty; eauto using cr_istyF_shift. Qed.
Lemma cr_istyF_id N : cr_istyF id id N N.
Proof. intros n. auto. Qed.
Lemma cr_istyF_up rho xi N M : cr_istyF rho xi N M -> cr_istyF (upren rho) (upren xi) (1 + N) (1 + M).
Proof.
intros CR [|n] L; asimpl in *.
- constructor. omega.
- ainv. cut (rho n < N); [intros H|omega]. aspec. constructor. ainv. omega.
Qed.
Lemma istyF_ren N A rho:
istyF N A.[ren rho] -> forall M xi, cr_istyF rho xi N M -> istyF M A.[ren xi].
Proof.
intros H. depind H; intros M xi CR; destruct A; ainv.
- apply CR. now constructor.
- constructor; eauto.
- constructor. asimpl. eapply IHistyF; eauto using cr_istyF_up. autosubst.
Qed.
Lemma cr_istyF_shift N : cr_istyF id (+1) N (1 + N).
Proof. intros n H. asimpl in *. ainv. constructor. omega. Qed.
Lemma cr_istyF_ushift N : cr_istyF (+1) id (1 + N) N.
Proof. intros n H. asimpl in *. ainv. constructor. omega. Qed.
Corollary istyF_weaken N A: istyF N A -> istyF (1 + N) A.[ren (+1)].
Proof. intros H. eapply istyF_ren; eauto using cr_istyF_shift. now asimpl. Qed.
Corollary istyF_strengthen N A: istyF (1 + N) A.[ren (+1)] -> istyF N A.
Proof. intros H. eapply istyF_ren in H; eauto using cr_istyF_ushift. now asimpl in *. Qed.
Definition cr_typingF zeta N Gamma Delta := forall x A, typingF N Gamma (TmVarF x) A -> typingF N Delta (TmVarF (zeta x)) A.
Lemma cr_typingF_id N Gamma : cr_typingF id N Gamma Gamma.
Proof. intros n A. auto. Qed.
Lemma cr_typingF_up A zeta N Gamma Delta :
cr_typingF zeta N Gamma Delta -> cr_typingF (upren zeta) N (A :: Gamma) (A :: Delta).
Proof.
intros CR [|n] B L; ainv; asimpl.
- constructor; trivial. constructor.
- constructor; trivial. constructor.
cut (typingF N Gamma (TmVarF n) B); [intros J| now constructor]. apply CR in J. ainv.
Qed.
Lemma cr_typingF_ren zeta N Gamma Delta :
cr_typingF zeta N Gamma Delta ->
forall M xi, cr_istyF xi id M N -> cr_typingF zeta M Gamma..[ren xi] Delta..[ren xi].
Proof.
intros CR2 M xi CR1. intros x B L. inversion L; subst.
destruct (mmap_atn H0) as [B' [EB' L']]; subst.
assert (H2' : istyF N B'). eapply istyF_ren in H1; eauto. now asimpl in *.
assert (H3 : typingF N Gamma (TmVarF x) B') by now constructor.
apply CR2 in H3. inversion H3; subst.
constructor; trivial. eapply atn_mmap; eauto.
Qed.
Corollary cr_typingF_ren_ushift zeta N Gamma Delta :
cr_typingF zeta N Gamma Delta -> cr_typingF zeta (1 + N) Gamma..[ren (+1)] Delta..[ren (+1)].
Proof. intros CR. eapply cr_typingF_ren; eauto using cr_istyF_ushift. Qed.
Lemma typingF_ren N Gamma s A:
typingF N Gamma s A ->
forall M Delta xi zeta,
cr_istyF id xi N M ->
cr_typingF zeta N Gamma Delta ->
typingF M Delta..[ren xi] s.[ren zeta].|[ren xi] A.[ren xi].
Proof.
intros H. induction H; intros M Delta xi zeta CR1 CR2; subst; asimpl.
- constructor.
+ eapply atn_mmap; eauto.
cut (typingF N Gamma (TmVarF x) A); [intros J | now constructor].
apply CR2 in J. ainv.
+ eapply istyF_ren; eauto. now asimpl.
- econstructor.
+ specialize (IHtypingF1 _ _ _ _ CR1 CR2); asimpl in *; eauto.
+ specialize (IHtypingF2 _ _ _ _ CR1 CR2); asimpl in *; eauto.
- constructor.
+ eapply istyF_ren; eauto. now asimpl.
+ apply cr_typingF_up with (A:=A) in CR2.
specialize (IHtypingF _ _ _ _ CR1 CR2). asimpl in *; eauto.
- econstructor.
+ eapply istyF_ren; eauto. now asimpl.
+ specialize (IHtypingF _ _ _ _ CR1 CR2). asimpl in *; eauto.
+ autosubst.
- constructor. asimpl.
replace (Delta..[ren (xi >>> (+1))]) with (Delta..[ren (+1)]..[ren (upren xi)]) by autosubst.
replace (s.|[ren (upren xi)].[ren zeta]) with (s.[ren zeta].|[ren (upren xi)]) by autosubst.
apply IHtypingF.
+ apply cr_istyF_up in CR1. now asimpl in *.
+ now apply cr_typingF_ren_ushift.
Qed.
Lemma cr_typingF_shift B N Gamma : cr_typingF (+1) N Gamma (B :: Gamma).
Proof. intros n A H. ainv. constructor; trivial. now constructor. Qed.
Corollary typingF_weaken B N Gamma s A:
typingF N Gamma s A -> typingF N (B :: Gamma) s.[ren (+1)] A.
Proof.
intros H.
pose proof (typingF_ren H (@cr_istyF_id N) (@cr_typingF_shift B N Gamma)) as J.
asimpl in *. now replace (mmap id Gamma) with Gamma in J by autosubst.
Qed.
Corollary typingF_ren_ty N Gamma s A:
typingF N Gamma s A ->
forall M xi, cr_istyF id xi N M ->
typingF M Gamma..[ren xi] s.|[ren xi] A.[ren xi].
Proof.
intros H M xi CR. pose proof (typingF_ren H CR (@cr_typingF_id N Gamma)) as J.
now asimpl in *.
Qed.
Corollary typingF_weaken_ty N Gamma s A :
typingF N Gamma s A -> typingF (1 + N) Gamma..[ren (+1)] s.|[ren (+1)] A.[ren (+1)].
Proof. intros H. eapply typingF_ren_ty; eauto using cr_istyF_shift. Qed.
Lemma sortL_ren u xi a : SortL u = a.[ren xi] -> a = SortL u.
Proof. intros E. destruct a; try discriminate E. asimpl in *. congruence. Qed.
Lemma sortL_p1 u : SortL u = (SortL u).[ren (+1)].
Proof. reflexivity. Qed.
Lemma sortL_add_ren {u} xi : SortL u = (SortL u).[ren xi].
Proof. reflexivity. Qed.
Lemma istyP_notSort Gamma u : ~ istyP Gamma (SortL u).
Proof. intros H. ainv. Qed.
Definition cr_istyP (rho xi : var -> var) Gamma Delta := forall x, istyP Gamma (VarL (rho x)) -> istyP Delta (VarL (xi x)).
Lemma cr_cr_istyP xi Gamma Delta : cr xi Gamma Delta -> cr_istyP id xi Gamma Delta.
Proof. intros CR n H. ainv. apply CR in H1. constructor. now asimpl in *. Qed.
Lemma cr_istyP_id Gamma : cr_istyP id id Gamma Gamma.
Proof. intros n. auto. Qed.
(* PR: Lemma 1 *)
Lemma cr_istyP_up a rho xi Gamma Delta : cr_istyP rho xi Gamma Delta -> cr_istyP (upren rho) (upren xi) (a.[ren rho] :: Gamma) (a.[ren xi] :: Delta).
Proof.
intros CR [|n] L; ainv; asimpl in *.
- apply sortL_ren in H1. subst. constructor. now econstructor.
- apply sortL_ren in H1. rewrite H1 in H3.
cut (istyP Gamma (VarL (rho n))); [intros J| now constructor]. aspec. ainv.
constructor. rewrite sortL_p1. econstructor; eauto.
Qed.
Corollary cr_istyP_up_id a xi Gamma Delta : cr_istyP id xi Gamma Delta -> cr_istyP id (upren xi) (a:: Gamma) (a.[ren xi] :: Delta).
Proof.
replace id with (upren id) at 2 by autosubst. replace a with (a.[ren id]) at 1 by autosubst.
apply cr_istyP_up.
Qed.
(* PR: Lemma 2 (Renaming CML for P Type Formation) *)
Lemma istyP_ren Gamma a rho :
istyP Gamma a.[ren rho] -> forall Delta xi, cr_istyP rho xi Gamma Delta -> istyP Delta a.[ren xi].
Proof.
intros H. depind H; intros Delta xi CR; destruct a; ainv.
- apply CR; auto using istyP.
- apply sortL_ren in H2; subst. asimpl. constructor.
apply IHistyP with (rho0 := upren rho); try autosubst.
rewrite (sortL_add_ren rho) at 1. rewrite (sortL_add_ren xi) at 2.
now apply cr_istyP_up.
- constructor; eauto. asimpl.
apply IHistyP2 with (rho0 := upren rho); try autosubst; auto using cr_istyP_up.
Qed.
Lemma cr_istyP_shift Gamma a : cr_istyP id (+1) Gamma (a :: Gamma).
Proof. intros n H. ainv. constructor. rewrite sortL_p1. econstructor; eauto. Qed.
Lemma cr_istyP_ushift Gamma a : cr_istyP (+1) id (a :: Gamma) Gamma.
Proof. intros n H. ainv. apply sortL_ren in H1. subst. now constructor. Qed.
(* PR: Theorem 3 (Weakening for P Type Formation) *)
Theorem istyP_weaken Gamma a b : istyP Gamma a -> istyP (b :: Gamma) a.[ren (+1)].
Proof. intros H. eapply istyP_ren; eauto using cr_istyP_shift. now asimpl. Qed.
(* PR: Theorem 4 (Strengthening for P Type Formation) *)
Theorem istyP_strengthen Gamma a b: istyP (b :: Gamma) a.[ren (+1)] -> istyP Gamma a.
Proof. intros H. eapply istyP_ren in H; eauto using cr_istyP_ushift. now asimpl in *. Qed.
Definition cm_istyP sigma Gamma Delta := forall x, istyP Gamma (VarL x) -> istyP Delta (sigma x).
Lemma cr_cm_istyP xi Gamma Delta : cr_istyP id xi Gamma Delta -> cm_istyP (ren xi) Gamma Delta.
Proof. intros CR x H. asimpl. eapply CR. trivial. Qed.
(* PR: Lemma 5 *)
Lemma cm_istyP_up a sigma Gamma Delta :
cm_istyP sigma Gamma Delta -> cm_istyP (up sigma) (a :: Gamma) (a.[sigma] :: Delta).
Proof.
intros c [|]; ainv; atom_ren.
- econstructor. now constructor.
- asimpl. apply istyP_weaken. auto using istyP.
Qed.
Lemma cm_istyP_beta_type Gamma a :
istyP Gamma a -> cm_istyP (a .: ids) ((SortL Prp) :: Gamma) Gamma.
Proof. intros H [|x] L; simpl in *; ainv; atom_ren. now constructor. Qed.
Lemma cm_istyP_beta_term Gamma a b :
typingP Gamma a b -> istyP Gamma b -> cm_istyP (a .: ids) (b :: Gamma) Gamma.
Proof. intros H1 H2 [|x] L; simpl in *; ainv; atom_ren. now constructor. Qed.
(* PR: Lemma 6 (CML for P Type Formation) *)
Lemma istyP_subst a sigma Gamma Delta :
istyP Gamma a -> cm_istyP sigma Gamma Delta -> istyP Delta a.[sigma].
Proof.
intros H. revert sigma Delta; induction H; intros.
- eauto using istyP.
- constructor. eauto using (@cm_istyP_up (SortL Prp)).
- constructor; eauto. eauto using cm_istyP_up.
Qed.
(* PR: Lemma 7 is for paper presentation only, all instances are handled directly via Lemma 6. *)
Definition cr_typingP xi Gamma Delta := forall x a, typingP Gamma (VarL x) a -> typingP Delta (VarL (xi x)) a.[ren xi].
(* PR: Lemma 8 *)
Lemma cr_typingP_up a xi Gamma Delta :
cr_istyP id xi Gamma Delta -> cr_typingP xi Gamma Delta -> cr_typingP (upren xi) (a :: Gamma) (a.[ren xi] :: Delta).
Proof.
intros CR1 CR2 [|n] L; ainv; asimpl in *.
- constructor.
+ econstructor. autosubst.
+ replace (a.[ren (xi >>> (+1))]) with (a.[ren xi].[ren (+1)]) by autosubst.
apply istyP_strengthen in H2. apply istyP_weaken.
eapply istyP_ren; eauto. now asimpl.
- apply istyP_strengthen in H2.
cut (typingP Gamma (VarL n) B); [intros J| now constructor]. aspec. ainv.
replace (B.[ren (xi >>> (+1))]) with (B.[ren xi].[ren (+1)]) by autosubst.
constructor; eauto using istyP_weaken. econstructor; eauto.
Qed.
(* PR: Lemma 9 (Renaming CML for P Typing) *)
Lemma typingP_ren Gamma a b :
typingP Gamma a b -> forall Delta xi, cr_istyP id xi Gamma Delta -> cr_typingP xi Gamma Delta -> typingP Delta a.[ren xi] b.[ren xi].
Proof.
intros H; induction H; intros Delta xi CR1 CR2; asimpl.
- apply CR2. now constructor.
- eapply typingP_app1; eauto. subst. autosubst.
- constructor.
+ eapply istyP_ren; eauto. autosubst.
+ eapply IHtypingP; eauto using cr_typingP_up, cr_istyP_up_id.
- eapply typingP_app2; eauto.
+ eapply istyP_ren; eauto. now asimpl.
+ subst. autosubst.
- eapply typingP_lam2. rewrite (sortL_add_ren xi).
eapply IHtypingP; eauto using cr_typingP_up, cr_istyP_up_id.
Qed.
Lemma cr_typingP_shift Gamma a : cr_typingP (+1) Gamma (a :: Gamma).
Proof.
intros n b H. ainv. constructor.
- econstructor; eauto.
- now apply istyP_weaken.
Qed.
(* PR: Theorem 10 (Weakening for P Typing) *)
Lemma typingP_weaken Gamma a b c : typingP Gamma a b -> typingP (c :: Gamma) a.[ren (+1)] b.[ren (+1)].
Proof. intros H. eapply typingP_ren; eauto using cr_istyP_shift, cr_typingP_shift. Qed.
Definition cm_typingP sigma (Gamma Delta : list termL) :=
forall x a, typingP Gamma (VarL x) a -> typingP Delta (sigma x) a.[sigma].
Lemma cm_typingP_up a sigma Gamma Delta :
cm_istyP sigma Gamma Delta ->
cm_typingP sigma Gamma Delta ->
cm_typingP (up sigma) (a :: Gamma) (a.[sigma] :: Delta).
Proof.
intros CM1 CM2 [|n] b H; ainv; asimpl.
- constructor.
+ constructor; autosubst.
+ replace (a.[sigma >> ren (+1)]) with (a.[sigma].[ren (+1)]) by autosubst.
apply istyP_weaken. eapply istyP_subst; eauto using istyP_strengthen.
- replace (B.[sigma >> ren (+1)]) with (B.[sigma].[ren (+1)]) by autosubst.
apply typingP_weaken, CM2. constructor; eauto using istyP_strengthen.
Qed.
Lemma typingP_subst Gamma a b:
typingP Gamma a b ->
forall Delta sigma,
cm_istyP sigma Gamma Delta ->
cm_typingP sigma Gamma Delta ->
typingP Delta a.[sigma] b.[sigma].
Proof.
intros H; induction H; intros Delta sigma CM1 CM2.
- apply CM2. now constructor.
- subst. econstructor; eauto; autosubst.
- asimpl. constructor; eauto using istyP_subst, cm_istyP_up, cm_typingP_up.
- subst. econstructor 4; eauto using istyP_subst. autosubst.
- asimpl. constructor 5.
replace (SortL Prp) with ((SortL Prp).[sigma]) by autosubst.
eauto using cm_istyP_up, cm_typingP_up.
Qed.
Lemma cm_typingP_beta_term Gamma a b :
typingP Gamma a b -> istyP Gamma b -> cm_typingP (a .: ids) (b :: Gamma) Gamma.
Proof.
intros H J [|n] c K; ainv; asimpl; trivial.
constructor; eauto using istyP_strengthen.
Qed.
Lemma cm_typingP_beta_type Gamma a :
istyP Gamma a -> cm_typingP (a .: ids) (SortL Prp :: Gamma) Gamma.
Proof.
intros H [|n] c K; ainv; asimpl.
constructor; eauto using istyP_strengthen.
Qed.
Theorem typingP_beta_term Gamma a b c d:
istyP Gamma d -> typingP Gamma c d -> typingP (d :: Gamma) a b -> typingP Gamma a.[c/] b.[c/].
Proof.
intros. eapply typingP_subst; eauto using cm_istyP_beta_term, cm_typingP_beta_term.
Qed.
Theorem typingP_beta_type Gamma a b c:
istyP Gamma c -> typingP ((SortL Prp) :: Gamma) a b -> typingP Gamma a.[c/] b.[c/].
Proof.
intros. eapply typingP_subst; eauto using cm_istyP_beta_type, cm_typingP_beta_type.
Qed.
Some facts regarding Sorts, in particular SortL Prp
Lemma istyP_neqPrp Gamma a : istyP Gamma a -> a <> SortL Prp.
Proof. destruct 1; congruence. Qed.
Lemma sortP_neq_ren xi a u : a.[ren xi] <> SortL u -> a <> SortL u.
Proof. destruct a; try discriminate. now asimpl. Qed.
Lemma sortP_eqPrp_f a : a <> SortL Prp -> eqPrp (Some a) = false.
Proof. intros H. destruct a; trivial. destruct u; trivial. congruence. Qed.
Lemma atnd_eqPrp_t Gamma x :
atnd Gamma x (SortL Prp) -> eqPrp (get Gamma x) = true.
Proof.
intros H. apply atnd_getD in H. rewrite getD_get in H.
simpl in *. ca. ainv. atom_ren.
Qed.
Lemma atnd_notPrp_eqPrp_f Gamma x a :
atnd Gamma x a -> a <> (SortL Prp) -> eqPrp (get Gamma x) = false.
Proof.
intros H. apply atnd_getD in H. rewrite getD_get in H.
simpl in *. unfold eqPrp. ca. ainv. congruence.
Qed.
Corollary atnd_type_eqPrp_f Gamma x a :
atnd Gamma x a -> istyP Gamma a -> eqPrp (get Gamma x) = false.
Proof. intros H1 H2. eapply atnd_notPrp_eqPrp_f; eauto using istyP_neqPrp. Qed.
Lemma eqPrp_ren a xi : eqPrp (Some a.[ren xi]) = eqPrp (Some a).
Proof. destruct a; reflexivity. Qed.
Lemma eqPrp_t_subst_t a sigma : eqPrp (Some a) = true -> eqPrp (Some a.[sigma]) = true.
Proof. intros E. destruct a; trivial; discriminate. Qed.
Proof. destruct 1; congruence. Qed.
Lemma sortP_neq_ren xi a u : a.[ren xi] <> SortL u -> a <> SortL u.
Proof. destruct a; try discriminate. now asimpl. Qed.
Lemma sortP_eqPrp_f a : a <> SortL Prp -> eqPrp (Some a) = false.
Proof. intros H. destruct a; trivial. destruct u; trivial. congruence. Qed.
Lemma atnd_eqPrp_t Gamma x :
atnd Gamma x (SortL Prp) -> eqPrp (get Gamma x) = true.
Proof.
intros H. apply atnd_getD in H. rewrite getD_get in H.
simpl in *. ca. ainv. atom_ren.
Qed.
Lemma atnd_notPrp_eqPrp_f Gamma x a :
atnd Gamma x a -> a <> (SortL Prp) -> eqPrp (get Gamma x) = false.
Proof.
intros H. apply atnd_getD in H. rewrite getD_get in H.
simpl in *. unfold eqPrp. ca. ainv. congruence.
Qed.
Corollary atnd_type_eqPrp_f Gamma x a :
atnd Gamma x a -> istyP Gamma a -> eqPrp (get Gamma x) = false.
Proof. intros H1 H2. eapply atnd_notPrp_eqPrp_f; eauto using istyP_neqPrp. Qed.
Lemma eqPrp_ren a xi : eqPrp (Some a.[ren xi]) = eqPrp (Some a).
Proof. destruct a; reflexivity. Qed.
Lemma eqPrp_t_subst_t a sigma : eqPrp (Some a) = true -> eqPrp (Some a.[sigma]) = true.
Proof. intros E. destruct a; trivial; discriminate. Qed.
(* PR: Lemma 11 (Propagation for P) *)
Lemma typingP_istyP Gamma a b : typingP Gamma a b -> istyP Gamma b.
Proof.
intros H. induction H.
- trivial.
- subst. inversion IHtypingP1; subst; ainv. eauto using istyP_subst, cm_istyP_beta_term.
- econstructor; eauto.
- subst. inv IHtypingP; try now asimpl. eauto using istyP_subst, cm_istyP_beta_type.
- constructor; eauto.
Qed.
Definition gentypingP Gamma a b :=
match b with
| (SortL Typ) => a = (SortL Prp)
| (SortL Prp) => istyP Gamma a
| _ => typingP Gamma a b
end.
Lemma gentypingP_typingP Gamma a b :
istyP Gamma b -> (gentypingP Gamma a b <-> typingP Gamma a b).
Proof.
unfold gentypingP.
split; intros; destruct b; intuition; now destruct (istyP_notSort $?).
Qed.
(* PR: Lemma 12 (Correspondence of L and P) -- part (c) *)
Lemma typingL_typingP Gamma a b : typingL Gamma a b -> gentypingP Gamma a b.
Proof.
induction 1; simpl in *; trivial.
- destruct u; subst; try now constructor.
rewrite gentypingP_typingP by assumption. now constructor.
- destruct u; subst; now constructor.
- pose proof (typingP_istyP $?) as I. inv I.
+ simpl in *. rewrite gentypingP_typingP;
eauto using typingP, istyP_subst, cm_istyP_beta_type.
+ rewrite gentypingP_typingP in *;
eauto using typingP, istyP_subst, cm_istyP_beta_term.
- rewrite gentypingP_typingP in * by assumption.
destruct u; subst; eauto using typingP, istyP.
Qed.
(* PR: Lemma 12 (Correspondence of L and P) -- part (a) *)
Lemma istyP_typingL Gamma a : istyP Gamma a -> typingL Gamma a (SortL Prp).
Proof. induction 1; eauto using typingL. Qed.
(* PR: Lemma 12 (Correspondence of L and P) -- part (b) *)
Lemma typingP_typingL Gamma a b : typingP Gamma a b -> typingL Gamma a b.
Proof. induction 1; eauto using istyP_typingL, typingP_istyP, typingL. Qed.
(* PR: Theorem 13 (Equivalence of L and P) *)
Theorem typingPL_equiv Gamma a b :
typingP Gamma a b <-> (typingL Gamma a b /\ typingL Gamma b (SortL Prp)).
Proof.
split.
- eauto using typingP_typingL, typingP_istyP, istyP_typingL.
- intros [H1 H2]. apply typingL_typingP in H1. apply typingL_typingP in H2.
simpl in H2. now rewrite gentypingP_typingP in H1.
Qed.
Fixpoint trTypeFP (A : typeF) : termL :=
match A with
| TyVarF x => VarL x
| ImpF A B => ProdL (trTypeFP A) (trTypeFP B).[ren(+1)]
| AllF A => ProdL (SortL Prp) (trTypeFP A)
end.
Fixpoint trTermFP (tau sigma : var -> termL) (s : termF) : termL :=
match s with
| TmVarF x => sigma x
| AppF s t => AppL (trTermFP tau sigma s) (trTermFP tau sigma t)
| LamF A s => LamL (trTypeFP A).[tau] (trTermFP (tau >> ren (+1)) (up sigma) s)
| TySpecF s A => AppL (trTermFP tau sigma s) (trTypeFP A).[tau]
| TyAbsF s => LamL (SortL Prp) (trTermFP (up tau) (sigma >> ren (+1)) s)
end.
match A with
| TyVarF x => VarL x
| ImpF A B => ProdL (trTypeFP A) (trTypeFP B).[ren(+1)]
| AllF A => ProdL (SortL Prp) (trTypeFP A)
end.
Fixpoint trTermFP (tau sigma : var -> termL) (s : termF) : termL :=
match s with
| TmVarF x => sigma x
| AppF s t => AppL (trTermFP tau sigma s) (trTermFP tau sigma t)
| LamF A s => LamL (trTypeFP A).[tau] (trTermFP (tau >> ren (+1)) (up sigma) s)
| TySpecF s A => AppL (trTermFP tau sigma s) (trTypeFP A).[tau]
| TyAbsF s => LamL (SortL Prp) (trTermFP (up tau) (sigma >> ren (+1)) s)
end.
Fixpoint trTypePF (gamma : var -> bool) (a : termL) : option typeF :=
match a with
| VarL x => if gamma x then Some (TyVarF x) else None
| ProdL a b =>
do B <- trTypePF (eqPrp (Some a) .: gamma) b;
if decide(a = (SortL Prp))
then Some(AllF B)
else do A <- trTypePF gamma a; Some (ImpF A B.[ren (-1)])
| _ => None
end.
Arguments trTypePF gamma !a.
Fixpoint trTermPF (gamma : var -> bool) (a : termL) : option termF :=
match a with
| VarL x => if gamma x then None else Some (TmVarF x)
| AppL a b =>
do s <- trTermPF gamma a;
match trTypePF gamma b with
Some B => Some (TySpecF s B)
| None =>
do t <- trTermPF gamma b; Some (AppF s t) end
| LamL a b =>
do s <- trTermPF (eqPrp (Some a) .: gamma) b;
if decide (a = (SortL Prp))
then Some (TyAbsF s.[ren(-1)])
else do A <- trTypePF gamma a; Some (LamF A s.|[ren(-1)])
| _ => None
end.
match a with
| VarL x => if gamma x then Some (TyVarF x) else None
| ProdL a b =>
do B <- trTypePF (eqPrp (Some a) .: gamma) b;
if decide(a = (SortL Prp))
then Some(AllF B)
else do A <- trTypePF gamma a; Some (ImpF A B.[ren (-1)])
| _ => None
end.
Arguments trTypePF gamma !a.
Fixpoint trTermPF (gamma : var -> bool) (a : termL) : option termF :=
match a with
| VarL x => if gamma x then None else Some (TmVarF x)
| AppL a b =>
do s <- trTermPF gamma a;
match trTypePF gamma b with
Some B => Some (TySpecF s B)
| None =>
do t <- trTermPF gamma b; Some (AppF s t) end
| LamL a b =>
do s <- trTermPF (eqPrp (Some a) .: gamma) b;
if decide (a = (SortL Prp))
then Some (TyAbsF s.[ren(-1)])
else do A <- trTypePF gamma a; Some (LamF A s.|[ren(-1)])
| _ => None
end.
Lemma trTypeFP_ren A xi : trTypeFP A.[ren xi] = (trTypeFP A).[ren xi].
Proof. revert xi. induction A; intros; asimpl; autorew; autosubst. Qed.
Lemma trTypeFP_subst A sigma :
trTypeFP A.[sigma] = (trTypeFP A).[sigma >>> trTypeFP].
Proof.
revert sigma. induction A; intros; asimpl; autorew; try autosubst.
do 2 f_equal. f_ext; intros[|x].
- reflexivity.
- asimpl. apply trTypeFP_ren.
Qed.
Lemma trTermFP_ren_ren s xi1 xi2 zeta1 zeta2 :
trTermFP (ren xi2) (ren zeta2) s.|[ren xi1].[ren zeta1] =
trTermFP (ren id) (ren id) s.|[ren (xi1 >>> xi2)].[ren (zeta1 >>> zeta2)].
Proof.
revert xi1 xi2 zeta1 zeta2. induction s;
intros; simpl; asimpl; f_equal; rewrite ?trTypeFP_ren; asimpl; eauto.
- rewrite IHs. symmetry. replace ids with (ren id) by trivial. rewrite IHs. autosubst.
- rewrite IHs. symmetry. replace ids with (ren id) by trivial. rewrite IHs. autosubst.
Qed.
Corollary trTermFP_ren s xi zeta :
trTermFP (ren xi) (ren zeta) s = trTermFP (ren id) (ren id) s.|[ren xi].[ren zeta].
Proof. pose proof (trTermFP_ren_ren s id xi id zeta) as H. now asimpl in *. Qed.
Lemma trTypePF_eqPrp_f gamma a A :
trTypePF gamma a = Some A -> eqPrp (Some a) = false.
Proof. intros H. now destruct a. Qed.
Lemma trTypePF_free_res a gamma A sigma tau :
trTypePF gamma a = Some A -> subst_coinc gamma sigma tau ->
A.[sigma] = A.[tau].
Proof.
revert gamma A sigma tau. induction a; intros; simpl in *; try discriminate.
- destruct (gamma x) eqn:E; ainv; eauto.
- ca. decide (a = SortL Prp); subst.
+ inv $$(AllF); simpl; f_equal.
eapply IHa0, subst_coinc_up; eauto.
+ ca. inv $$(ImpF). asimpl. f_equal; eauto.
eapply IHa0, subst_coinc_hd_f; eauto using trTypePF_eqPrp_f.
Qed.
Lemma trTypePF_free_arg a gamma A sigma tau :
trTypePF gamma a = Some A -> subst_coinc gamma sigma tau ->
a.[sigma] = a.[tau].
Proof.
revert gamma A sigma tau. induction a; intros; simpl in *; try discriminate.
- destruct (gamma x) eqn:E; ainv; eauto.
- ca. decide (a = SortL Prp); subst.
+ inv $$(AllF); simpl; f_equal. eapply IHa0, subst_coinc_up; eauto.
+ ca. inv $$(ImpF). f_equal; eauto. eapply IHa0, subst_coinc_up; eauto.
Qed.
Lemma typingP_trTypePF Gamma a b :
typingP Gamma a b -> trTypePF (get Gamma >>> eqPrp) a = None.
Proof. destruct 1; simpl; trivial. erewrite atnd_type_eqPrp_f; eauto. Qed.
Lemma istyP_trTypePF Gamma a :
istyP Gamma a -> exists A, trTypePF (get Gamma >>> eqPrp) a = Some A.
Proof.
induction 1; simpl trTypePF.
- exists (TyVarF x). now rewrite atnd_eqPrp_t.
- destruct IHistyP as [A EA]. exists (AllF A).
asimpl in *. now rewrite EA.
- destruct IHistyP1 as [A EA]. destruct IHistyP2 as [B EB].
asimpl in *. rewrite EA, EB. exists (ImpF A B.[ids 0/]).
decide (a = SortL Prp); subst; trivial.
exfalso. destruct (istyP_notSort $?).
Qed.
Lemma trTypePF_ren a A xi delta gamma:
trTypePF gamma a = Some A -> bfr xi delta gamma ->
trTypePF delta a.[ren xi] = Some A.[ren xi].
Proof.
revert A xi delta gamma. induction a; intros; try discriminate.
- simpl in *. destruct (gamma x) eqn:E; ainv. aspec. simpl. now rewrite $$(delta).
- simpl in *. ca. asimpl. erewrite eqPrp_ren, IHa0; eauto using bfr_up.
decide (a = (SortL Prp)); subst; simpl.
+ inv $$(AllF). autosubst.
+ rewrite (sortP_eqPrp_f $?) in *. ca. erewrite IHa; try eassumption.
decide (a.[ren xi] = SortL Prp).
* exfalso. apply f. destruct a; trivial; discriminate.
* ainv. asimpl. do 2 f_equal. eapply trTypePF_free_res; eauto.
apply subst_coinc_hd_f; trivial using subst_coinc_id.
Qed.
Definition cm_trTypePF (tau : var -> typeF) (sigma : var -> termL) delta gamma :=
forall x, gamma x = true -> trTypePF delta (sigma x) = Some (tau x).
Lemma cm_trTypePF_up a tau sigma delta gamma :
cm_trTypePF tau sigma delta gamma ->
cm_trTypePF (up tau) (up sigma) (eqPrp (Some a.[sigma]) .: delta) (eqPrp (Some a) .: gamma).
Proof.
intros H [|x] E; asimpl in *.
- simpl. now rewrite eqPrp_t_subst_t.
- eapply trTypePF_ren; eauto using bfr_shift.
Qed.
Lemma cm_trTypePF_beta a gamma A :
trTypePF gamma a = Some A ->
cm_trTypePF (A .: ids) (a .: ids) (gamma) (true .: gamma).
Proof. intros H [|x] E; simpl in *; trivial. now rewrite E. Qed.
Lemma trTypePF_subst a A tau sigma delta gamma:
trTypePF gamma a = Some A -> cm_trTypePF tau sigma delta gamma ->
trTypePF delta a.[sigma] = Some A.[tau].
Proof.
revert A tau sigma delta gamma. induction a; intros; try discriminate.
- simpl in *. destruct (gamma x) eqn:E; ainv. eauto.
- simpl in *. ca. asimpl. erewrite IHa0; eauto using cm_trTypePF_up.
decide (a = (SortL Prp)); subst; simpl.
+ inv $$(AllF). autosubst.
+ rewrite (sortP_eqPrp_f $?) in *. ca. erewrite IHa; try eassumption.
decide (a.[sigma] = SortL Prp).
* exfalso. specialize (IHa _ _ _ _ _ $? $?). rewrite $$(@eq) in IHa. discriminate.
* ainv. asimpl. do 2 f_equal. eapply trTypePF_free_res; eauto.
apply subst_coinc_hd_f; trivial using subst_coinc_id.
Qed.
Lemma trTermPF_free sigma1 sigma2 tau1 tau2 a gamma s :
trTermPF gamma a = Some s ->
subst_coinc gamma sigma1 sigma2 -> subst_coinc (gamma >>> negb) tau1 tau2 ->
s.|[sigma1].[tau1] = s.|[sigma2].[tau2].
Proof.
revert gamma s sigma1 sigma2 tau1 tau2.
induction a; intros; simpl in *; try discriminate.
- destruct (gamma x) eqn:E; ainv. apply H1. simpl. now autorew.
- destruct (trTypePF gamma a2) eqn:?; ca; ainv; asimpl; erewrite IHa1;
eauto; f_equal; eauto. eapply trTypePF_free_res; eauto.
- ca. decide (a = SortL Prp); subst.
+ inv $$(TyAbsF). asimpl. f_equal.
eapply IHa0; eauto; try now apply subst_coinc_up.
(* eauto using subst_coinc_up. with Hint Extern 4 => exact _. does not work here*)
asimpl. apply subst_coinc_hd_f, subst_coinc_hcomp; trivial.
+ ca. inv $$(LamF). asimpl. f_equal; eauto using trTypePF_free_res.
eapply IHa0; eauto; asimpl; try now apply subst_coinc_up.
apply subst_coinc_hd_f; trivial. now destruct a.
Qed.
Corollary trTermPF_free_tm a gamma s tau :
trTermPF gamma a = Some s -> subst_coinc (gamma >>> negb) ids tau ->
s = s.[tau].
Proof.
pose proof (@trTermPF_free ids ids ids tau).
asimpl in *; eauto using subst_coinc_id.
Qed.
Corollary trTermPF_free_ty a gamma s sigma :
trTermPF gamma a = Some s -> subst_coinc gamma ids sigma -> s = s.|[sigma].
Proof.
pose proof (@trTermPF_free ids sigma ids ids).
asimpl in*; eauto using subst_coinc_id.
Qed.
Definition cr_istyFP (xi : var -> var) N Gamma := forall x, istyF N (TyVarF x) -> istyP Gamma (VarL (xi x)).
Lemma cr_istyFP_vac xi Gamma : cr_istyFP xi 0 Gamma.
Proof. intros ? K. inversion K. omega. Qed.
(* PR: Lemma 14 -- rule 1 *)
Lemma cr_istyFP_up xi N Gamma :
cr_istyFP xi N Gamma -> cr_istyFP (upren xi) (1 + N) ((SortL Prp) :: Gamma).
Proof.
intros H [|x] K; asimpl.
- repeat constructor.
- inversion K. cut (x < N); [intros|omega].
cut (istyF N (TyVarF x)); [intros J|now constructor].
replace (VarL (S (xi x))) with (VarL (xi x)).[ren (+1)] by autosubst.
apply istyP_weaken; auto.
Qed.
(* PR: Lemma 14 -- rule 2 *)
Lemma cr_istyFP_shift A xi N Gamma :
cr_istyFP xi N Gamma -> cr_istyFP (xi >>> (+1)) N ((trTypeFP A).[ren xi] :: Gamma).
Proof.
intros H x K. aspec. asimpl.
replace (VarL (S (xi x))) with (VarL (xi x)).[ren (+1)] by autosubst.
now apply istyP_weaken.
Qed.
(* PR: Lemma 15 (CML: F to P -- Type Formation) *)
Lemma trIstyFP_morph A xi N Gamma:
istyF N A -> cr_istyFP xi N Gamma ->
istyP Gamma (trTypeFP A).[ren xi].
Proof.
intros H; revert Gamma xi; induction H; intros; simpl.
- auto using istyF.
- econstructor; asimpl; eauto using cr_istyFP_shift.
- econstructor. asimpl; eauto using cr_istyFP_up.
Qed.
Lemma cr_istyFP_vac xi Gamma : cr_istyFP xi 0 Gamma.
Proof. intros ? K. inversion K. omega. Qed.
(* PR: Lemma 14 -- rule 1 *)
Lemma cr_istyFP_up xi N Gamma :
cr_istyFP xi N Gamma -> cr_istyFP (upren xi) (1 + N) ((SortL Prp) :: Gamma).
Proof.
intros H [|x] K; asimpl.
- repeat constructor.
- inversion K. cut (x < N); [intros|omega].
cut (istyF N (TyVarF x)); [intros J|now constructor].
replace (VarL (S (xi x))) with (VarL (xi x)).[ren (+1)] by autosubst.
apply istyP_weaken; auto.
Qed.
(* PR: Lemma 14 -- rule 2 *)
Lemma cr_istyFP_shift A xi N Gamma :
cr_istyFP xi N Gamma -> cr_istyFP (xi >>> (+1)) N ((trTypeFP A).[ren xi] :: Gamma).
Proof.
intros H x K. aspec. asimpl.
replace (VarL (S (xi x))) with (VarL (xi x)).[ren (+1)] by autosubst.
now apply istyP_weaken.
Qed.
(* PR: Lemma 15 (CML: F to P -- Type Formation) *)
Lemma trIstyFP_morph A xi N Gamma:
istyF N A -> cr_istyFP xi N Gamma ->
istyP Gamma (trTypeFP A).[ren xi].
Proof.
intros H; revert Gamma xi; induction H; intros; simpl.
- auto using istyF.
- econstructor; asimpl; eauto using cr_istyFP_shift.
- econstructor. asimpl; eauto using cr_istyFP_up.
Qed.
Definition cr_typingFP (xi zeta : var -> var) N Delta Gamma :=
forall x A, typingF N Delta (TmVarF x) A -> typingP Gamma (VarL (zeta x)) (trTypeFP A).[ren xi].
Lemma cr_typingFP_vac xi zeta N Gamma : cr_typingFP xi zeta N nil Gamma.
Proof. intros ? ? L; ainv. Qed.
(* PR: Lemma 16 -- rule 1 *)
Lemma cr_typingFP_up_shift xi zeta N Delta Gamma :
cr_typingFP xi zeta N Delta Gamma ->
cr_typingFP (upren xi) (zeta >>> (+1)) (1 + N) Delta..[ren (+1)] (SortL Prp :: Gamma).
Proof.
intros CR x A L. ainv. destruct (mmap_atn H0) as [B [? ?]]. subst.
rewrite trTypeFP_ren. asimpl.
replace (trTypeFP B).[ren (xi >>> (+1))] with (trTypeFP B).[ren (xi)].[ren(+1)] by autosubst.
replace (VarL (S (zeta x))) with (VarL (zeta x)).[ren (+1)] by autosubst.
apply typingP_weaken. apply CR. apply istyF_strengthen in H1. now constructor.
Qed.
(* PR: Lemma 16 -- rule 2 *)
Lemma cr_typingFP_shift_up A xi zeta N Delta Gamma :
cr_istyFP xi N Gamma -> cr_typingFP xi zeta N Delta Gamma ->
cr_typingFP (xi >>> (+1)) (upren zeta) N (A :: Delta) ((trTypeFP A).[ren xi] :: Gamma).
Proof.
intros CR1 CR2 [|x] B L; ainv; asimpl;
replace (trTypeFP B).[ren (xi >>> (+1))] with (trTypeFP B).[ren (xi)].[ren(+1)] by autosubst.
- econstructor.
+ constructor; autosubst.
+ eapply istyP_weaken, trIstyFP_morph; eauto.
- replace (VarL (S (zeta x))) with (VarL (zeta x)).[ren (+1)] by autosubst.
apply typingP_weaken. apply CR2. now constructor.
Qed.
(* PR: Lemma 17 (CML: F to P -- Typing) *)
Lemma trTypingFP_morph s A xi zeta N Delta Gamma :
typingF N Delta s A -> cr_istyFP xi N Gamma ->
cr_typingFP xi zeta N Delta Gamma ->
typingP Gamma (trTermFP (ren xi) (ren zeta) s) (trTypeFP A).[ren xi].
Proof.
intros H; revert xi zeta Gamma. induction H; intros xi zeta Phi CR1 CR2; simpl in *.
- apply CR2. now constructor.
- econstructor; eauto. autosubst.
- econstructor; asimpl; eauto using trIstyFP_morph, cr_istyFP_shift, cr_typingFP_shift_up.
- eapply typingP_app2; eauto using trIstyFP_morph.
subst. rewrite trTypeFP_subst. autosubst.
- eapply typingP_lam2; asimpl; eauto using cr_istyFP_up, cr_typingFP_up_shift.
Qed.
(* PR: Lemma 18 is for paper presentation only, all instances are handled directly via Lemma 17. *)
forall x A, typingF N Delta (TmVarF x) A -> typingP Gamma (VarL (zeta x)) (trTypeFP A).[ren xi].
Lemma cr_typingFP_vac xi zeta N Gamma : cr_typingFP xi zeta N nil Gamma.
Proof. intros ? ? L; ainv. Qed.
(* PR: Lemma 16 -- rule 1 *)
Lemma cr_typingFP_up_shift xi zeta N Delta Gamma :
cr_typingFP xi zeta N Delta Gamma ->
cr_typingFP (upren xi) (zeta >>> (+1)) (1 + N) Delta..[ren (+1)] (SortL Prp :: Gamma).
Proof.
intros CR x A L. ainv. destruct (mmap_atn H0) as [B [? ?]]. subst.
rewrite trTypeFP_ren. asimpl.
replace (trTypeFP B).[ren (xi >>> (+1))] with (trTypeFP B).[ren (xi)].[ren(+1)] by autosubst.
replace (VarL (S (zeta x))) with (VarL (zeta x)).[ren (+1)] by autosubst.
apply typingP_weaken. apply CR. apply istyF_strengthen in H1. now constructor.
Qed.
(* PR: Lemma 16 -- rule 2 *)
Lemma cr_typingFP_shift_up A xi zeta N Delta Gamma :
cr_istyFP xi N Gamma -> cr_typingFP xi zeta N Delta Gamma ->
cr_typingFP (xi >>> (+1)) (upren zeta) N (A :: Delta) ((trTypeFP A).[ren xi] :: Gamma).
Proof.
intros CR1 CR2 [|x] B L; ainv; asimpl;
replace (trTypeFP B).[ren (xi >>> (+1))] with (trTypeFP B).[ren (xi)].[ren(+1)] by autosubst.
- econstructor.
+ constructor; autosubst.
+ eapply istyP_weaken, trIstyFP_morph; eauto.
- replace (VarL (S (zeta x))) with (VarL (zeta x)).[ren (+1)] by autosubst.
apply typingP_weaken. apply CR2. now constructor.
Qed.
(* PR: Lemma 17 (CML: F to P -- Typing) *)
Lemma trTypingFP_morph s A xi zeta N Delta Gamma :
typingF N Delta s A -> cr_istyFP xi N Gamma ->
cr_typingFP xi zeta N Delta Gamma ->
typingP Gamma (trTermFP (ren xi) (ren zeta) s) (trTypeFP A).[ren xi].
Proof.
intros H; revert xi zeta Gamma. induction H; intros xi zeta Phi CR1 CR2; simpl in *.
- apply CR2. now constructor.
- econstructor; eauto. autosubst.
- econstructor; asimpl; eauto using trIstyFP_morph, cr_istyFP_shift, cr_typingFP_shift_up.
- eapply typingP_app2; eauto using trIstyFP_morph.
subst. rewrite trTypeFP_subst. autosubst.
- eapply typingP_lam2; asimpl; eauto using cr_istyFP_up, cr_typingFP_up_shift.
Qed.
(* PR: Lemma 18 is for paper presentation only, all instances are handled directly via Lemma 17. *)
Definition cr_istyPF xi Gamma N := forall x, istyP Gamma (VarL x) -> istyF N (TyVarF (xi x)).
Lemma cr_istyPF_vac xi N : cr_istyPF xi nil N .
Proof. intros ? L. ainv. Qed.
(* PR: Lemma 19 -- rule 1 *)
Lemma cr_istyPF_up a xi Gamma N: cr_istyPF xi Gamma N -> cr_istyPF (upren xi) (a :: Gamma) (1 + N).
Proof.
intros H [|x] L; asimpl.
- constructor. omega.
- ainv. atom_ren.
replace (TyVarF (S (xi x))) with (TyVarF (xi x)).[ren (+1)] by autosubst.
apply istyF_weaken. apply H. now constructor.
Qed.
(* PR: Lemma 19 -- rule 2 *)
Lemma cr_istyPF_ushift a xi Gamma N :
istyP Gamma a -> cr_istyPF xi Gamma N -> cr_istyPF ((-1) >>> xi) (a :: Gamma) N.
Proof.
intros H CR [|x] L.
- exfalso. ainv; atom_ren.
- asimpl. apply CR. apply istyP_strengthen with (b:=a). autosubst.
Qed.
(* PR: Lemma 20 (CML: P to F -- Type Formation) *)
Lemma trIstyPF_morph Gamma a:
istyP Gamma a ->
GET A <- trTypePF (get Gamma >>> eqPrp) a;
forall xi N, cr_istyPF xi Gamma N -> istyF N A.[ren xi].
Proof.
intros H; induction H; simpl.
- rewrite (atnd_eqPrp_t $?). intros xi N CR. apply CR. now constructor.
- asimpl in *. ca. intros xi N CR. constructor. asimpl. eauto using cr_istyPF_up.
- asimpl in *. decide (a = (SortL Prp)); subst.
+ exfalso. destruct (istyP_notSort $?).
+ rewrite (sortP_eqPrp_f $?) in *. ca. intros xi N CR. constructor; eauto; asimpl.
apply (cr_istyPF_ushift H) in CR. eapply IHistyP2. now asimpl in *.
Qed.
Lemma cr_istyPF_vac xi N : cr_istyPF xi nil N .
Proof. intros ? L. ainv. Qed.
(* PR: Lemma 19 -- rule 1 *)
Lemma cr_istyPF_up a xi Gamma N: cr_istyPF xi Gamma N -> cr_istyPF (upren xi) (a :: Gamma) (1 + N).
Proof.
intros H [|x] L; asimpl.
- constructor. omega.
- ainv. atom_ren.
replace (TyVarF (S (xi x))) with (TyVarF (xi x)).[ren (+1)] by autosubst.
apply istyF_weaken. apply H. now constructor.
Qed.
(* PR: Lemma 19 -- rule 2 *)
Lemma cr_istyPF_ushift a xi Gamma N :
istyP Gamma a -> cr_istyPF xi Gamma N -> cr_istyPF ((-1) >>> xi) (a :: Gamma) N.
Proof.
intros H CR [|x] L.
- exfalso. ainv; atom_ren.
- asimpl. apply CR. apply istyP_strengthen with (b:=a). autosubst.
Qed.
(* PR: Lemma 20 (CML: P to F -- Type Formation) *)
Lemma trIstyPF_morph Gamma a:
istyP Gamma a ->
GET A <- trTypePF (get Gamma >>> eqPrp) a;
forall xi N, cr_istyPF xi Gamma N -> istyF N A.[ren xi].
Proof.
intros H; induction H; simpl.
- rewrite (atnd_eqPrp_t $?). intros xi N CR. apply CR. now constructor.
- asimpl in *. ca. intros xi N CR. constructor. asimpl. eauto using cr_istyPF_up.
- asimpl in *. decide (a = (SortL Prp)); subst.
+ exfalso. destruct (istyP_notSort $?).
+ rewrite (sortP_eqPrp_f $?) in *. ca. intros xi N CR. constructor; eauto; asimpl.
apply (cr_istyPF_ushift H) in CR. eapply IHistyP2. now asimpl in *.
Qed.
Weaker form that is easier to use ...
Corollary trIstyPF_morph' a xi Gamma N:
istyP Gamma a -> cr_istyPF xi Gamma N ->
GET A <- trTypePF (get Gamma >>> eqPrp) a; istyF N A.[ren xi].
Proof.
intros H CR. pose proof (trIstyPF_morph H) as J.
destruct (istyP_trTypePF $?) as [A EA]. rewrite EA in *; auto.
Qed.
istyP Gamma a -> cr_istyPF xi Gamma N ->
GET A <- trTypePF (get Gamma >>> eqPrp) a; istyF N A.[ren xi].
Proof.
intros H CR. pose proof (trIstyPF_morph H) as J.
destruct (istyP_trTypePF $?) as [A EA]. rewrite EA in *; auto.
Qed.
Definition cr_typingPF xi zeta Gamma N Delta :=
forall x a, typingP Gamma (VarL x) a ->
GET A <- trTypePF (get Gamma >>> eqPrp) a;
typingF N Delta (TmVarF (zeta x)) A.[ren xi].
Lemma cr_typingPF_vac xi zeta N Delta : cr_typingPF xi zeta nil N Delta.
Proof. intros ? ? L. ainv. Qed.
(* PR: Lemma 21 -- rule 2 *)
Lemma cr_typingPF_up_ushift xi zeta Gamma N Delta :
cr_istyPF xi Gamma N -> cr_typingPF xi zeta Gamma N Delta ->
cr_typingPF (upren xi) ((-1) >>> zeta) (SortL Prp :: Gamma) (1 + N) Delta..[ren (+1)].
Proof.
intros CR1 CR2 [|x] a L; ainv. apply istyP_strengthen in H1.
assert (J : typingP Gamma (VarL x) B) by now constructor. apply CR2 in J.
pose proof (trIstyPF_morph' $? CR1). ca. asimpl.
erewrite trTypePF_ren; eauto using bfr_shift.
apply typingF_weaken_ty in J. now asimpl in *.
Qed.
(* PR: Lemma 21 -- rule 2 *)
Lemma cr_typingPF_ushift_up a A xi zeta Gamma N Delta :
trTypePF (get Gamma >>> eqPrp) a = Some A -> cr_istyPF xi Gamma N -> cr_typingPF xi zeta Gamma N Delta ->
cr_typingPF ((-1) >>> xi) (upren zeta) (a :: Gamma) N (A.[ren xi] :: Delta).
Proof.
intros E CR1 CR2 [|x] b L; asimpl; ainv.
- erewrite trTypePF_ren; eauto using bfr_shift. asimpl. constructor.
+ constructor.
+ apply istyP_strengthen in H1. pose proof (trIstyPF_morph' $? CR1).
now rewrite H2 in H.
- apply istyP_strengthen in H1.
assert (J : typingP Gamma (VarL x) B) by now constructor. apply CR2 in J.
pose proof (trIstyPF_morph' $? CR1). ca.
erewrite trTypePF_ren; eauto using bfr_shift.
apply typingF_weaken with (B:=A.[ren xi]) in J.
now asimpl in *.
Qed.
(* PR: Lemma 22 (CML: P to F -- Typing) *)
Lemma trTypingPF_morph Gamma a b:
typingP Gamma a b ->
GET s <- trTermPF (get Gamma >>> eqPrp) a;
GET A <- trTypePF (get Gamma >>> eqPrp) b;
forall xi zeta N Delta,
cr_istyPF xi Gamma N -> cr_typingPF xi zeta Gamma N Delta ->
typingF N Delta s.|[ren xi].[ren zeta] A.[ren xi].
Proof.
intros H; induction H; simpl in *.
- erewrite atnd_type_eqPrp_f; try eassumption.
destruct (istyP_trTypePF $?) as [A EA]; rewrite EA.
intros xi zeta N Delta CR1 CR2. asimpl.
assert (J: typingP Gamma (VarL x) a) by now constructor. apply CR2 in J. ca.
inversion EA; now subst.
- subst. ca. erewrite typingP_trTypePF; eauto.
decide (c = SortL Prp); subst; try discriminate. inv $$(ImpF).
rewrite (sortP_eqPrp_f $?) in *.
assert (Ed: d = d.[ren (-1)].[ren (+1)]).
+ asimpl. replace d with d.[ids] at 1 by autosubst.
eapply trTypePF_free_arg; eauto. apply subst_coinc_hd_f; trivial.
asimpl. apply subst_coinc_id.
+ rewrite Ed. asimpl.
erewrite trTypePF_ren; eauto using bfr_ushift. intros.
specialize (IHtypingP1 _ _ _ _ $? $?). asimpl in *.
econstructor; eauto.
- asimpl in *. ca. destruct (istyP_trTypePF $?) as [A EA]; rewrite EA.
decide (a = SortL Prp); subst; try now destruct (istyP_notSort $?).
intros. pose proof (trIstyPF_morph' $? $?) as J. rewrite EA in J.
constructor; eauto. asimpl.
apply (cr_typingPF_ushift_up EA H1) in H2.
apply (cr_istyPF_ushift H) in H1.
apply IHtypingP; now asimpl in *.
- subst. ca. destruct (istyP_trTypePF $?) as [C EC]; rewrite EC. inv $$(AllF).
erewrite trTypePF_subst; eauto using cm_trTypePF_beta.
intros. pose proof (trIstyPF_morph' $? $?) as J. rewrite EC in J.
econstructor; eauto. autosubst.
- asimpl in *. ca. intros. econstructor. asimpl.
apply (cr_typingPF_up_ushift H0) in H1.
apply cr_istyPF_up with (a:=SortL Prp) in H0.
apply IHtypingP; now asimpl in *.
Qed.
(* PR: Lemma 23 is for paper presentation only, all instances are handled directly via Lemma 22. *)
(* PR: Lemma 24 -- first implication *)
Lemma cancellation_trTypePFP a A gamma xi :
trTypePF gamma a.[ren xi] = Some A -> trTypeFP A = a.[ren xi].
Proof.
revert A gamma xi. induction a; ainv.
- destruct (gamma (xi x)) eqn:E; ainv.
- asimpl. ca. decide (a.[ren xi] = SortL Prp); subst.
+ inv $$(AllF). asimpl. f_equal; eauto. eapply IHa0. asimpl in *. eauto.
+ ca. inv $$(ImpF). asimpl. f_equal; eauto.
rewrite <- trTypeFP_ren. asimpl. erewrite IHa0; eauto.
asimpl in *. erewrite Heqo. f_equal.
replace t with t.[ren id] at 1 by autosubst.
eapply trTypePF_free_res, subst_coinc_hd_f, subst_coinc_id;
eauto using trTypePF_eqPrp_f.
Qed.
(* PR: Lemma 24 -- second implication *)
Lemma cancellation_trTermPFP a s gamma xi:
trTermPF gamma a.[ren xi] = Some s -> trTermFP (ren id) (ren id) s = a.[ren xi].
Proof.
revert s gamma xi. induction a; intros; try now simpl in *.
- ainv. destruct (gamma(xi x)) eqn:E; ainv.
- simpl in *. ca.
destruct (trTypePF gamma a2.[ren xi]) eqn:?; ca; ainv; asimpl;
erewrite IHa1; eauto; f_equal; eauto.
eapply cancellation_trTypePFP; eauto.
- simpl in *. ca. decide (a.[ren xi] = SortL Prp); ainv.
+ asimpl. autorew. f_equal. replace ids with (ren id) by trivial. rewrite trTermFP_ren.
asimpl. erewrite IHa0; eauto. asimpl in *. rewrite Heqo. f_equal.
eapply trTermPF_free_tm; eauto. asimpl. rewrite H0.
apply subst_coinc_hd_f; eauto using subst_coinc_id.
+ ca. ainv. asimpl. (* replace t0 with t0.ren id by autosubst. *)
erewrite cancellation_trTypePFP; eauto. f_equal.
replace ids with (ren id) by trivial. rewrite trTermFP_ren. erewrite IHa0; eauto. asimpl in *. autorew. f_equal.
eapply trTermPF_free_ty; eauto.
apply subst_coinc_hd_f; eauto using subst_coinc_id. now destruct a.
Qed.
Definition cm_vdP Gamma (xi zeta : var -> var) :=
(forall x a, atnd Gamma (xi x) a -> a = (SortL Prp)) /\
(forall x a, atnd Gamma (zeta x) a -> a <> (SortL Prp)).
Lemma cm_vdP_vac xi zeta: cm_vdP nil xi zeta.
Proof. split; intros x a L; ainv. Qed.
Lemma cm_vdP_up_shift Gamma xi zeta:
cm_vdP Gamma xi zeta ->
cm_vdP (SortL Prp :: Gamma) (upren xi) (zeta >>> (+1)).
Proof.
intros [HL HR]. split.
- intros [|x] a L; ainv. now rewrite (HL _ _ $?).
- intros x a L. ainv. aspec. intro. atom_ren; congruence.
Qed.
Lemma cm_vdP_shift_up a Gamma xi zeta:
istyP Gamma a -> cm_vdP Gamma xi zeta ->
cm_vdP (a :: Gamma) (xi >>> (+1)) (upren zeta).
Proof.
intros H [HL HR]. split.
- intros x b L. ainv. aspec. atom_ren.
- intros [|x] b L; ainv; try discriminate. aspec. intro. atom_ren. congruence.
Qed.
Lemma trTermFP_not_istyP Gamma xi zeta s :
cm_vdP Gamma xi zeta -> ~ istyP Gamma (trTermFP (ren xi) (ren zeta) s).
Proof. intros [_ J] C. destruct s; ainv. aspec. congruence. Qed.
Lemma trTypeFP_not_typingP Gamma xi zeta A b :
cm_vdP Gamma xi zeta -> ~ typingP Gamma (trTypeFP A).[ren xi] b.
Proof.
intros [J _] C. destruct A; ainv. aspec; subst.
now destruct (istyP_notSort $?).
Qed.
(forall x a, atnd Gamma (xi x) a -> a = (SortL Prp)) /\
(forall x a, atnd Gamma (zeta x) a -> a <> (SortL Prp)).
Lemma cm_vdP_vac xi zeta: cm_vdP nil xi zeta.
Proof. split; intros x a L; ainv. Qed.
Lemma cm_vdP_up_shift Gamma xi zeta:
cm_vdP Gamma xi zeta ->
cm_vdP (SortL Prp :: Gamma) (upren xi) (zeta >>> (+1)).
Proof.
intros [HL HR]. split.
- intros [|x] a L; ainv. now rewrite (HL _ _ $?).
- intros x a L. ainv. aspec. intro. atom_ren; congruence.
Qed.
Lemma cm_vdP_shift_up a Gamma xi zeta:
istyP Gamma a -> cm_vdP Gamma xi zeta ->
cm_vdP (a :: Gamma) (xi >>> (+1)) (upren zeta).
Proof.
intros H [HL HR]. split.
- intros x b L. ainv. aspec. atom_ren.
- intros [|x] b L; ainv; try discriminate. aspec. intro. atom_ren. congruence.
Qed.
Lemma trTermFP_not_istyP Gamma xi zeta s :
cm_vdP Gamma xi zeta -> ~ istyP Gamma (trTermFP (ren xi) (ren zeta) s).
Proof. intros [_ J] C. destruct s; ainv. aspec. congruence. Qed.
Lemma trTypeFP_not_typingP Gamma xi zeta A b :
cm_vdP Gamma xi zeta -> ~ typingP Gamma (trTypeFP A).[ren xi] b.
Proof.
intros [J _] C. destruct A; ainv. aspec; subst.
now destruct (istyP_notSort $?).
Qed.
(* PR: Lemma 25 *)
Lemma cancellation_trTypeFPF A Gamma xi :
istyP Gamma (trTypeFP A).[ren xi] ->
trTypePF (get Gamma >>> eqPrp) (trTypeFP A).[ren xi] = Some A.[ren xi].
Proof.
revert Gamma xi. induction A; intros; trivial; asimpl; autorew.
- simpl in *. ainv. rewrite atnd_eqPrp_t; eauto.
- simpl in *. inv $$(istyP).
+ destruct A1; simpl in *; discriminate.
+ asimplH $$(istyP). specialize (IHA2 _ _ H3). rewrite IHA1; trivial.
asimpl in *. rewrite IHA2; try (asimpl; now destruct A1).
- ainv. specialize (IHA (SortL Prp :: Gamma) (upren xi)).
asimpl in *. erewrite IHA; eauto.
Qed.
(* PR: Lemma 26 *)
Lemma cancellation_trTermFPF Gamma s b xi zeta :
typingP Gamma (trTermFP (ren xi) (ren zeta) s) b -> cm_vdP Gamma xi zeta ->
trTermPF (get Gamma >>> eqPrp) (trTermFP (ren xi) (ren zeta) s) = Some s.|[ren xi].[ren zeta].
Proof.
revert Gamma b xi zeta. induction s; intros.
- asimpl. ainv. simpl. erewrite atnd_type_eqPrp_f; eauto.
- asimpl. inv $$(typingP).
+ erewrite IHs1, IHs2, typingP_trTypePF; eauto.
+ exfalso. now destruct (trTermFP_not_istyP _ $? $?).
- asimpl. inv $$(typingP).
+ rewrite cancellation_trTypeFPF; eauto.
specialize (IHs ((trTypeFP A).[ren xi] :: Gamma)).
specialize (IHs c (xi >>> (+1)) (upren zeta)). (* specialize is a workaround for asimpl bug *)
asimpl in *. erewrite IHs; eauto using cm_vdP_shift_up.
decide ((trTypeFP A).[ren xi] = SortL Prp); try now destruct A. autosubst.
+ exfalso. now destruct A.
- asimpl. inv $$(typingP).
+ exfalso. now destruct (trTypeFP_not_typingP _ $? $?).
+ rewrite cancellation_trTypeFPF; trivial. erewrite IHs; eauto.
- asimpl. inv $$(typingP).
+ exfalso. inv $$(istyP).
+ specialize (IHs (SortL Prp :: Gamma)).
specialize (IHs b0 (upren xi ) (zeta >>> (+1))). (* specialize is a workaround for asimpl bug *)
asimpl in *.
erewrite IHs; asimpl; eauto using cm_vdP_up_shift.
Qed.
Lemma cancellation_trTypeFPF A Gamma xi :
istyP Gamma (trTypeFP A).[ren xi] ->
trTypePF (get Gamma >>> eqPrp) (trTypeFP A).[ren xi] = Some A.[ren xi].
Proof.
revert Gamma xi. induction A; intros; trivial; asimpl; autorew.
- simpl in *. ainv. rewrite atnd_eqPrp_t; eauto.
- simpl in *. inv $$(istyP).
+ destruct A1; simpl in *; discriminate.
+ asimplH $$(istyP). specialize (IHA2 _ _ H3). rewrite IHA1; trivial.
asimpl in *. rewrite IHA2; try (asimpl; now destruct A1).
- ainv. specialize (IHA (SortL Prp :: Gamma) (upren xi)).
asimpl in *. erewrite IHA; eauto.
Qed.
(* PR: Lemma 26 *)
Lemma cancellation_trTermFPF Gamma s b xi zeta :
typingP Gamma (trTermFP (ren xi) (ren zeta) s) b -> cm_vdP Gamma xi zeta ->
trTermPF (get Gamma >>> eqPrp) (trTermFP (ren xi) (ren zeta) s) = Some s.|[ren xi].[ren zeta].
Proof.
revert Gamma b xi zeta. induction s; intros.
- asimpl. ainv. simpl. erewrite atnd_type_eqPrp_f; eauto.
- asimpl. inv $$(typingP).
+ erewrite IHs1, IHs2, typingP_trTypePF; eauto.
+ exfalso. now destruct (trTermFP_not_istyP _ $? $?).
- asimpl. inv $$(typingP).
+ rewrite cancellation_trTypeFPF; eauto.
specialize (IHs ((trTypeFP A).[ren xi] :: Gamma)).
specialize (IHs c (xi >>> (+1)) (upren zeta)). (* specialize is a workaround for asimpl bug *)
asimpl in *. erewrite IHs; eauto using cm_vdP_shift_up.
decide ((trTypeFP A).[ren xi] = SortL Prp); try now destruct A. autosubst.
+ exfalso. now destruct A.
- asimpl. inv $$(typingP).
+ exfalso. now destruct (trTypeFP_not_typingP _ $? $?).
+ rewrite cancellation_trTypeFPF; trivial. erewrite IHs; eauto.
- asimpl. inv $$(typingP).
+ exfalso. inv $$(istyP).
+ specialize (IHs (SortL Prp :: Gamma)).
specialize (IHs b0 (upren xi ) (zeta >>> (+1))). (* specialize is a workaround for asimpl bug *)
asimpl in *.
erewrite IHs; asimpl; eauto using cm_vdP_up_shift.
Qed.
(* PR: Theorem 27 (Reduction of Typability from F to P) *)
Theorem trTypingFP_red s A :
typingF 0 nil s A <-> typingP nil (trTermFP (ren id) (ren id) s) (trTypeFP A).
Proof.
split; intros.
- replace (trTypeFP A) with (trTypeFP A).[ren id] by autosubst.
apply trTypingFP_morph with (N := 0) (Delta := nil); trivial using cr_istyFP_vac, cr_typingFP_vac.
- replace (typingP nil (trTermFP (ren id) (ren id) s) (trTypeFP A))
with (typingP nil (trTermFP (ren id) (ren id) s) (trTypeFP A).[ren id]) in * by autosubst.
pose proof (typingP_istyP H) as H'.
pose proof (cancellation_trTypeFPF _ _ H') as C1.
pose proof (cancellation_trTermFPF _ H (cm_vdP_vac id id)) as C2.
asimpl in *. apply trTypingPF_morph in H. ca. inv C1. inv C2.
aspec. asimpl in *. eauto using cr_istyPF_vac, cr_typingPF_vac.
Qed.
(* PR: Theorem 28 (Reduction of Typability from P to F) *)
Theorem trTypingPF_red a b :
typingP nil a b <->
GET s <- trTermPF (fun _ => false) a;
GET A <- trTypePF (fun _ => false) b;
typingF 0 nil s A.
Proof.
split; intros H.
- pose proof (trTypingPF_morph H) as PF. asimpl in *.
replace ((fun _ : var => None) >>> eqPrp)
with (fun _ : var => false) in PF by reflexivity.
ca. aspec. asimpl in *. eauto using cr_istyPF_vac, cr_typingPF_vac.
- ca.
eapply trTypingFP_morph with (xi := id) (zeta := id) (Gamma := nil) in H;
trivial using cr_istyFP_vac, cr_typingFP_vac.
erewrite <- trTypeFP_ren, (cancellation_trTypePFP b (fun _ : var => false) id) in H; try autosubst.
rewrite cancellation_trTermPFP with (a := a) (s := t) (xi := id) (gamma := fun _ => false) in H;
now asimpl in *.
Qed.
(* PR: Lemma 29 (Reduction of Typability from F to L) *)
Lemma trTypingFL_red s A :
typingF 0 nil s A <->
(typingL nil (trTermFP (ren id) (ren id) s) (trTypeFP A) /\
typingL nil (trTypeFP A) (SortL Prp)).
Proof. rewrite trTypingFP_red. now rewrite typingPL_equiv. Qed.
(* PR: Lemma 30 (Reduction of Typability from L to F) *)
Lemma trTypingLF_red a b :
(typingL nil a b /\ typingL nil b (SortL Prp)) <->
GET s <- trTermPF (fun _ => false) a;
GET A <- trTypePF (fun _ => false) b;
typingF 0 nil s A.
Proof. rewrite <- trTypingPF_red. now rewrite typingPL_equiv. Qed.
(* PR: Theorem 31 is a plain conjunction of 29 and 30 and hence omitted. *)