SysF_PTS.sysf
(* (c) 2017, Jonas Kaiser, based on major contributions from Tobias Tebbi *)
Traditional, 2-sorted System F with explicits type variable contexts, a la Harper
Require Import Omega List Program.Equality.
From Autosubst Require Export Autosubst.
Require Import Decidable lib.
Set Implicit Arguments.
Terms
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}).
| 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.
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.
Illustration of heterogeneos subst s.|tau.sigma (also written stau,sigma) 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.
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.
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).
Theory
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 cm_istyF (sigma : var -> typeF) N M := forall x, istyF N (TyVarF x) -> istyF M (sigma x).
Lemma cm_istyF_up sigma N M : cm_istyF sigma N M -> cm_istyF (up sigma) (1 + N) (1 + M).
Proof.
intros CM [|x] T; ainv; asimpl.
- constructor. omega.
- apply lt_S_n in H0. apply istyF_weaken. apply CM. now constructor.
Qed.
Lemma istyF_subst N A : istyF N A -> forall M sigma, cm_istyF sigma N M -> istyF M A.[sigma].
Proof.
intros H. induction H; intros M sigma CM.
- apply CM. now constructor.
- constructor; auto.
- constructor; auto using cm_istyF_up.
Qed.
Lemma cm_istyF_beta N B : istyF N B -> cm_istyF (B .: ids) (1 + N) N.
Proof. intros T [|x] H; asimpl; trivial. now apply istyF_strengthen. Qed.
Theorem istyF_beta N A B : istyF N B -> istyF (1 + N) A -> istyF N A.[B/].
Proof. intros H T. eapply istyF_subst; eauto using cm_istyF_beta. 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 cm_istyF (sigma : var -> typeF) N M := forall x, istyF N (TyVarF x) -> istyF M (sigma x).
Lemma cm_istyF_up sigma N M : cm_istyF sigma N M -> cm_istyF (up sigma) (1 + N) (1 + M).
Proof.
intros CM [|x] T; ainv; asimpl.
- constructor. omega.
- apply lt_S_n in H0. apply istyF_weaken. apply CM. now constructor.
Qed.
Lemma istyF_subst N A : istyF N A -> forall M sigma, cm_istyF sigma N M -> istyF M A.[sigma].
Proof.
intros H. induction H; intros M sigma CM.
- apply CM. now constructor.
- constructor; auto.
- constructor; auto using cm_istyF_up.
Qed.
Lemma cm_istyF_beta N B : istyF N B -> cm_istyF (B .: ids) (1 + N) N.
Proof. intros T [|x] H; asimpl; trivial. now apply istyF_strengthen. Qed.
Theorem istyF_beta N A B : istyF N B -> istyF (1 + N) A -> istyF N A.[B/].
Proof. intros H T. eapply istyF_subst; eauto using cm_istyF_beta. 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.
Fixpoint internF_ty (N : nat) (s : termF) (A : typeF) : (termF * typeF) :=
match N with
| 0 => (s,A)
| (S M) => internF_ty M (TyAbsF s) (AllF A)
end.
Fixpoint internF (N : nat) (Gamma : list typeF) (s : termF) (A : typeF) : (termF * typeF) :=
match Gamma with
| nil => internF_ty N s A
| (B :: Delta) => internF N Delta (LamF B s) (ImpF B A)
end.
Inductive wfF : nat -> list typeF -> Prop :=
| wfF_empty : wfF 0 nil
| wfF_ext_ty N : wfF N nil -> wfF (S N) nil (* note: restriction to nil *)
| wfF_ext_tm N Gamma A : istyF N A -> wfF N Gamma -> wfF N (A :: Gamma).
Lemma internF_correct N Gamma s A t B: wfF N Gamma -> internF N Gamma s A = (t,B) -> (typingF N Gamma s A <-> typingF 0 nil t B).
Proof.
intros H. revert s A t B. induction H; intros; simpl in *.
- inversion H; firstorder.
- apply IHwfF in H0. eapply iff_trans; eauto. split.
+ intros. econstructor. eauto.
+ intros. now inversion H1.
- apply IHwfF in H1. eapply iff_trans; eauto. split.
+ intros. econstructor; eauto.
+ intros. now inversion H2.
Qed.