-lemma boundin_envappend_case : \forall G,H,b.(var_bind_in_env b (H @ G)) \to
- (var_bind_in_env b G) \lor (var_bind_in_env b H).
-intros 3.elim H
- [simplify in H1;left;assumption
- |unfold in H2;inversion H2
- [intros;simplify in H4;lapply (inj_head ? ? ? ? H4);rewrite > Hletin;
- right;apply in_Base
- |intros;simplify in H6;lapply (inj_tail ? ? ? ? ? H6);rewrite < Hletin in H3;
- rewrite > H5 in H1;lapply (H1 H3);elim Hletin1
- [left;assumption|right;apply in_Skip;assumption]]]
-qed.
-
-lemma varin_envappend_case: \forall G,H,x.(var_in_env x (H @ G)) \to
- (var_in_env x G) \lor (var_in_env x H).
-intros 3.elim H 0
- [simplify;intro;left;assumption
- |intros 2;elim s;simplify in H2;inversion H2
- [intros;lapply (inj_head_nat ? ? ? ? H4);rewrite > Hletin;right;
- simplify;constructor 1
- |intros;lapply (inj_tail ? ? ? ? ? H6);
- lapply H1
- [rewrite < H5;elim Hletin1
- [left;assumption|right;simplify;constructor 2;assumption]
- |unfold var_in_env;unfold fv_env;rewrite > Hletin;rewrite > H5;
- assumption]]]
-qed.
-
-lemma boundinG_or_boundinH_to_boundinGH : \forall G,H,b.
- (var_bind_in_env b G) \lor (var_bind_in_env b H) \to
- (var_bind_in_env b (H @ G)).
-intros.elim H1
- [elim H
- [simplify;assumption
- |simplify;apply in_Skip;assumption]
- |generalize in match H2;elim H2
- [simplify;apply in_Base
- |lapply (H4 H3);simplify;apply in_Skip;assumption]]
-qed.
-
-
-lemma varinG_or_varinH_to_varinGH : \forall G,H,x.
- (var_in_env x G) \lor (var_in_env x H) \to
- (var_in_env x (H @ G)).
-intros.elim H1 0
- [elim H
- [simplify;assumption
- |elim s;simplify;constructor 2;apply (H2 H3)]
- |elim H 0
- [simplify;intro;lapply (in_list_nil nat x H2);elim Hletin
- |intros 2;elim s;simplify in H3;inversion H3
- [intros;lapply (inj_head_nat ? ? ? ? H5);rewrite > Hletin;simplify;
- constructor 1
- |intros;simplify;constructor 2;rewrite < H6;apply H2;
- lapply (inj_tail ? ? ? ? ? H7);rewrite > H6;unfold;unfold fv_env;
- rewrite > Hletin;assumption]]]
-qed.
-
-lemma varbind_to_append : \forall G,b.(var_bind_in_env b G) \to
- \exists G1,G2.(G = (G2 @ (b :: G1))).
-intros.generalize in match H.elim H
- [apply ex_intro [apply l|apply ex_intro [apply Empty|reflexivity]]
- |lapply (H2 H1);elim Hletin;elim H4;rewrite > H5;
- apply ex_intro
- [apply a2|apply ex_intro [apply (a1 :: a3)|simplify;reflexivity]]]
-qed.
-
-(*** Type Well-Formedness judgement ***)
-
-inductive WFType : Env \to Typ \to Prop \def
- | WFT_TFree : \forall X,G.(in_list ? X (fv_env G))
- \to (WFType G (TFree X))
- | WFT_Top : \forall G.(WFType G Top)
- | WFT_Arrow : \forall G,T,U.(WFType G T) \to (WFType G U) \to
- (WFType G (Arrow T U))
- | WFT_Forall : \forall G,T,U.(WFType G T) \to
- (\forall X:nat.
- (\lnot (in_list ? X (fv_env G))) \to
- (\lnot (in_list ? X (fv_type U))) \to
- (WFType ((mk_bound true X T) :: G)
- (subst_type_O U (TFree X)))) \to
- (WFType G (Forall T U)).
-
-(*** Environment Well-Formedness judgement ***)
-
-inductive WFEnv : Env \to Prop \def
- | WFE_Empty : (WFEnv Empty)
- | WFE_cons : \forall B,X,T,G.(WFEnv G) \to
- \lnot (in_list ? X (fv_env G)) \to
- (WFType G T) \to (WFEnv ((mk_bound B X T) :: G)).
-
-(*** Subtyping judgement ***)
-inductive JSubtype : Env \to Typ \to Typ \to Prop \def
- | SA_Top : \forall G:Env.\forall T:Typ.(WFEnv G) \to
- (WFType G T) \to (JSubtype G T Top)
- | SA_Refl_TVar : \forall G:Env.\forall X:nat.(WFEnv G) \to (var_in_env X G)
- \to (JSubtype G (TFree X) (TFree X))
- | SA_Trans_TVar : \forall G:Env.\forall X:nat.\forall T:Typ.
- \forall U:Typ.
- (var_bind_in_env (mk_bound true X U) G) \to
- (JSubtype G U T) \to (JSubtype G (TFree X) T)
- | SA_Arrow : \forall G:Env.\forall S1,S2,T1,T2:Typ.
- (JSubtype G T1 S1) \to (JSubtype G S2 T2) \to
- (JSubtype G (Arrow S1 S2) (Arrow T1 T2))
- | SA_All : \forall G:Env.\forall S1,S2,T1,T2:Typ.
- (JSubtype G T1 S1) \to
- (\forall X:nat.\lnot (var_in_env X G) \to
- (JSubtype ((mk_bound true X T1) :: G)
- (subst_type_O S2 (TFree X)) (subst_type_O T2 (TFree X)))) \to
- (JSubtype G (Forall S1 S2) (Forall T1 T2)).
-
-(*** Typing judgement ***)
-inductive JType : Env \to Term \to Typ \to Prop \def
- | T_Var : \forall G:Env.\forall x:nat.\forall T:Typ.
- (WFEnv G) \to (var_bind_in_env (mk_bound false x T) G) \to
- (JType G (Free x) T)
- | T_Abs : \forall G.\forall T1,T2:Typ.\forall t2:Term.
- \forall x:nat.
- (JType ((mk_bound false x T1)::G) (subst_term_O t2 (Free x)) T2) \to
- (JType G (Abs T1 t2) (Arrow T1 T2))
- | T_App : \forall G.\forall t1,t2:Term.\forall T2:Typ.
- \forall T1:Typ.(JType G t1 (Arrow T1 T2)) \to (JType G t2 T1) \to
- (JType G (App t1 t2) T2)
- | T_TAbs : \forall G:Env.\forall T1,T2:Typ.\forall t2:Term.
- \forall X:nat.
- (JType ((mk_bound true X T1)::G)
- (subst_term_tO t2 (TFree X)) (subst_type_O T2 (TFree X)))
- \to (JType G (TAbs T1 t2) (Forall T1 T2))
- | T_TApp : \forall G:Env.\forall t1:Term.\forall T2,T12:Typ.
- \forall X:nat.\forall T11:Typ.
- (JType G t1 (Forall T11 (subst_type_tfree_type T12 X (TVar O)))) \to
- (JSubtype G T2 T11)
- \to (JType G (TApp t1 T2) (subst_type_tfree_type T12 X T2))
- | T_Sub : \forall G:Env.\forall t:Term.\forall T:Typ.
- \forall S:Typ.(JType G t S) \to (JSubtype G S T) \to (JType G t T).
-
-