-lemma t_len_pred: \forall T,m.(S (t_len T)) \leq m \to (t_len T) \leq (pred m).
-intros 2;elim m
- [elim (not_le_Sn_O ? H)
- |simplify;apply (le_S_S_to_le ? ? H1)]
-qed.
-
-lemma pred_m_lt_m : \forall m,T.(t_len T) \leq m \to (pred m) < m.
-intros 2;elim m 0
- [elim T
- [simplify in H;elim (not_le_Sn_n ? H)
- |simplify in H;elim (not_le_Sn_n ? H)
- |simplify in H;elim (not_le_Sn_n ? H)
- |simplify in H2;elim (not_le_Sn_O ? H2)
- |simplify in H2;elim (not_le_Sn_O ? H2)]
- |intros;simplify;unfold;constructor 1]
-qed.
-
-lemma WFE_bound_bound : \forall B,x,T,U,G. (WFEnv G) \to
- (in_list ? (mk_bound B x T) G) \to
- (in_list ? (mk_bound B x U) G) \to T = U.
-intros 6;elim H
- [lapply (in_list_nil ? ? H1);elim Hletin
- |inversion H6
- [intros;rewrite < H7 in H8;lapply (inj_head ? ? ? ? H8);
- rewrite > Hletin in H5;inversion H5
- [intros;rewrite < H9 in H10;lapply (inj_head ? ? ? ? H10);
- destruct Hletin1;symmetry;assumption
- |intros;lapply (inj_tail ? ? ? ? ? H12);rewrite < Hletin1 in H9;
- rewrite < H11 in H9;lapply (boundinenv_natinfv x e)
- [destruct Hletin;rewrite < Hcut1 in Hletin2;lapply (H3 Hletin2);
- elim Hletin3
- |apply ex_intro
- [apply B|apply ex_intro [apply T|assumption]]]]
- |intros;lapply (inj_tail ? ? ? ? ? H10);rewrite < H9 in H7;
- rewrite < Hletin in H7;(*FIXME*)generalize in match H5;intro;inversion H5
- [intros;rewrite < H12 in H13;lapply (inj_head ? ? ? ? H13);
- destruct Hletin1;rewrite < Hcut1 in H7;
- lapply (boundinenv_natinfv n e)
- [lapply (H3 Hletin2);elim Hletin3
- |apply ex_intro
- [apply B|apply ex_intro [apply U|assumption]]]
- |intros;apply (H2 ? H7);rewrite > H14;lapply (inj_tail ? ? ? ? ? H15);
- rewrite > Hletin1;assumption]]]
-qed.
-
-lemma JS_trans_narrow : \forall n.
- (\forall G,T,Q,U.
- (t_len Q) \leq n \to (JSubtype G T Q) \to (JSubtype G Q U) \to
- (JSubtype G T U)) \land
- (\forall G,H,X,P,Q,M,N.
- (t_len Q) \leq n \to
- (JSubtype (H @ ((mk_bound true X Q) :: G)) M N) \to
- (JSubtype G P Q) \to
- (JSubtype (H @ ((mk_bound true X P) :: G)) M N)).
-intro;apply (nat_elim1 n);intros 2;
-cut (\forall G,T,Q.(JSubtype G T Q) \to
- \forall U.(t_len Q \leq m) \to (JSubtype G Q U) \to (JSubtype G T U))
- [cut (\forall G,M,N.(JSubtype G M N) \to
- \forall G1,X,Q,G2,P.
- (G = G2 @ ((mk_bound true X Q) :: G1)) \to (t_len Q) \leq m \to
- (JSubtype G1 P Q) \to
- (JSubtype (G2 @ ((mk_bound true X P) :: G1)) M N))
- [split
- [intros;apply (Hcut ? ? ? H2 ? H1 H3)
- |intros;apply (Hcut1 ? ? ? H3 ? ? ? ? ? ? H2 H4);reflexivity]
- |intros 9;cut (incl ? (fv_env (G2 @ ((mk_bound true X Q)::G1)))
- (fv_env (G2 @ ((mk_bound true X P)::G1))))
- [intros;
-(* [rewrite > H6 in H2;lapply (JS_to_WFT1 ? ? ? H8);
- apply (WFE_Typ_subst ? ? ? ? ? ? ? H2 Hletin) *)
- generalize in match Hcut1;generalize in match H2;
- generalize in match H1;generalize in match H4;
- generalize in match G1;generalize in match G2;elim H1
- [apply SA_Top
- [rewrite > H9 in H5;lapply (JS_to_WFT1 ? ? ? H7);
- apply (WFE_Typ_subst ? ? ? ? ? ? ? H5 Hletin)
- |rewrite > H9 in H6;apply (WFT_env_incl ? ? H6);elim l
- [simplify;unfold;intros;assumption
- |simplify;apply (incl_nat_cons ? ? ? H11)]]
- |apply SA_Refl_TVar
- [rewrite > H9 in H5;lapply (JS_to_WFT1 ? ? ? H7);
- apply (WFE_Typ_subst ? ? ? ? ? ? ? H5 Hletin)
- |apply H10;rewrite < H9;assumption]
- |elim (decidable_eq_nat X n1)
- [apply (SA_Trans_TVar ? ? ? P)
- [rewrite < H12;elim l
- [simplify;apply in_Base
- |simplify;apply in_Skip;assumption]
- |lapply (JS_to_WFE ? ? ? H9);rewrite > H10 in Hletin;
- rewrite > H10 in H5;
- lapply (WFE_bound_bound ? ? ? Q ? Hletin H5)
- [lapply (H7 ? ? H8 H6 H10 H11);rewrite > Hletin1 in Hletin2;
- apply (Hcut ? ? ? ? ? H3 Hletin2);
- lapply (JS_to_WFE ? ? ? Hletin2);
- apply (JS_weakening ? ? ? H8 ? Hletin3);unfold;intros;
- elim l;simplify;apply in_Skip;assumption
- |rewrite > H12;elim l
- [simplify;apply in_Base
- |simplify;apply in_Skip;assumption]]]
- |rewrite > H10 in H5;apply (SA_Trans_TVar ? ? ? t1)
- [apply (lookup_env_extends ? ? ? ? ? ? ? ? ? ? H5);unfold;
- intro;apply H12;symmetry;assumption
- |apply (H7 ? ? H8 H6 H10 H11)]]
- |apply SA_Arrow
- [apply (H6 ? ? H9 H5 H11 H12)
- |apply (H8 ? ? H9 H7 H11 H12)]
+lemma JS_trans_prova: ∀T,G1.WFType G1 T →
+∀G,R,U.incl ? (fv_env G1) (fv_env G) → G ⊢ R ⊴ T → G ⊢ T ⊴ U → G ⊢ R ⊴ U.
+intros 3;elim H;clear H; try autobatch;
+ [rewrite > (JSubtype_Top ? ? H3);autobatch
+ |generalize in match H7;generalize in match H4;generalize in match H2;
+ generalize in match H5;clear H7 H4 H2 H5;
+ generalize in match (refl_eq ? (Arrow t t1));
+ elim H6 in ⊢ (? ? ? %→%); clear H6; intros; destruct;
+ [apply (SA_Trans_TVar ? ? ? ? H);apply (H4 ? ? H8 H9);autobatch
+ |inversion H11;intros; destruct; autobatch depth=4 width=4 size=9;
+ ]
+ |generalize in match H7;generalize in match H4;generalize in match H2;
+ generalize in match H5;clear H7 H4 H2 H5;
+ generalize in match (refl_eq ? (Forall t t1));elim H6 in ⊢ (? ? ? %→%);destruct;
+ [apply (SA_Trans_TVar ? ? ? ? H);apply (H4 ? H7 H8 H9 H10);reflexivity
+ |inversion H11;intros;destruct;
+ [apply SA_Top
+ [autobatch
+ |apply WFT_Forall
+ [autobatch
+ |intros;lapply (H4 ? H13);autobatch]]