From 2a85b279378df4193bbe927e3cdbaffd7d229279 Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Mon, 24 Sep 2007 16:22:16 +0000 Subject: [PATCH] Last version of poplmark 1a, featuring new proof, only 558 lines! --- matita/library/Fsub/defn.ma | 206 +++++++------------- matita/library/Fsub/part1a.ma | 344 +++++++++++++--------------------- matita/library/Fsub/util.ma | 67 ++++++- 3 files changed, 255 insertions(+), 362 deletions(-) diff --git a/matita/library/Fsub/defn.ma b/matita/library/Fsub/defn.ma index 573b2afe8..177edbb45 100644 --- a/matita/library/Fsub/defn.ma +++ b/matita/library/Fsub/defn.ma @@ -168,58 +168,18 @@ intros 2;elim G [elim H;elim H1;lapply (in_list_nil ? ? H2);elim Hletin |elim H1;elim H2;elim (in_cons_case ? ? ? ? H3) [rewrite < H4;simplify;apply in_Base - |elim H4;elim t;simplify;apply in_Skip2;apply H;apply (ex_intro ? ? a); + |simplify;apply in_Skip;apply H;apply (ex_intro ? ? a); apply (ex_intro ? ? a1);assumption]] qed. -lemma nat_in_list_case : \forall G,H,n.(in_list nat n (H @ G)) \to - (in_list nat n G) \lor (in_list nat n H). -intros 3.elim H - [simplify in H1;left;assumption - |simplify in H2;elim (in_cons_case ? ? ? ? H2) - [right;rewrite > H3;apply in_Base - |elim H3;elim (H1 H5) [left;assumption|right;apply in_Skip2;assumption]]] -qed. - -lemma natinG_or_inH_to_natinGH : \forall G,H,n. - (in_list nat n G) \lor (in_list nat n H) \to - (in_list nat n (H @ G)). -intros.elim H1 - [elim H - [simplify;assumption - |simplify;apply in_Skip2;assumption] - |generalize in match H2;elim H2 - [simplify;apply in_Base - |lapply (H4 H3);simplify;apply in_Skip;assumption]] -qed. - lemma natinfv_boundinenv : \forall x,G.(in_list ? x (fv_env G)) \to \exists B,T.(in_list ? (mk_bound B x T) G). intros 2;elim G 0 [simplify;intro;lapply (in_list_nil ? ? H);elim Hletin |intros 3;elim t;simplify in H1;elim (in_cons_case ? ? ? ? H1) [rewrite < H2;apply (ex_intro ? ? b);apply (ex_intro ? ? t1);apply in_Base - |elim H2;elim (H H4);elim H5;apply (ex_intro ? ? a); - apply (ex_intro ? ? a1);apply in_Skip - [assumption - |intro;destruct H7;elim (H3 Hcut1)]]] -qed. - -theorem varinT_varinT_subst : \forall X,Y,T. - (in_list ? X (fv_type T)) \to \forall n. - (in_list ? X (fv_type (subst_type_nat T (TFree Y) n))). -intros 3;elim T - [simplify in H;elim (in_list_nil ? ? H) - |simplify in H;simplify;assumption - |simplify in H;elim (in_list_nil ? ? H) - |simplify in H2;simplify;elim (nat_in_list_case ? ? ? H2); - apply natinG_or_inH_to_natinGH; - [left;apply (H1 H3) - |right;apply (H H3)] - |simplify in H2;simplify;elim (nat_in_list_case ? ? ? H2); - apply natinG_or_inH_to_natinGH; - [left;apply (H1 H3); - |right;apply (H H3)]] + |elim (H H2);elim H3;apply (ex_intro ? ? a); + apply (ex_intro ? ? a1);apply in_Skip;assumption]] qed. lemma incl_bound_fv : \forall l1,l2.(incl ? l1 l2) \to @@ -232,10 +192,10 @@ lapply (natinfv_boundinenv ? ? H1).elim Hletin.elim H2.apply ex_intro |apply (H ? H3)]] qed. -lemma incl_nat_cons : \forall x,l1,l2. - (incl nat l1 l2) \to (incl nat (x :: l1) (x :: l2)). +lemma incl_cons : \forall x,l1,l2. + (incl ? l1 l2) \to (incl nat (x :: l1) (x :: l2)). intros.unfold in H.unfold.intros.elim (in_cons_case ? ? ? ? H1) - [rewrite > H2;apply in_Base|elim H2;apply in_Skip2;apply (H ? H4)] + [rewrite > H2;apply in_Base|apply in_Skip;apply (H ? H2)] qed. lemma WFT_env_incl : \forall G,T.(WFType G T) \to @@ -248,7 +208,7 @@ intros 3.elim H [apply (H2 ? H6) |intros;apply (H4 ? ? H8) [unfold;intro;apply H7;apply(H6 ? H9) - |simplify;apply (incl_nat_cons ? ? ? H6)]]] + |simplify;apply (incl_cons ? ? ? H6)]]] qed. lemma fv_env_extends : \forall H,x,B,C,T,U,G. @@ -265,11 +225,10 @@ lemma lookup_env_extends : \forall G,H,B,C,D,T,U,V,x,y. intros 10;elim H [simplify in H1;elim (in_cons_case ? ? ? ? H1) [destruct H3;elim (H2 Hcut1) - |simplify;elim H3;apply (in_Skip ? ? ? ? H5);intro;destruct H6; - apply (H2 Hcut1)] + |simplify;apply (in_Skip ? ? ? ? H3);] |simplify in H2;simplify;elim (in_cons_case ? ? ? ? H2) [rewrite > H4;apply in_Base - |elim H4;apply (in_Skip ? ? ? ? (H1 H6 H3) H5)]] + |apply (in_Skip ? ? ? ? (H1 H4 H3))]] qed. lemma in_FV_subst : \forall x,T,U,n.(in_list ? x (fv_type T)) \to @@ -277,10 +236,9 @@ lemma in_FV_subst : \forall x,T,U,n.(in_list ? x (fv_type T)) \to intros 3;elim T [simplify in H;elim (in_list_nil ? ? H) |2,3:simplify;simplify in H;assumption - |*:simplify in H2;simplify;apply natinG_or_inH_to_natinGH; - lapply (nat_in_list_case ? ? ? H2);elim Hletin - [1,3:left;apply (H1 ? H3) - |*:right;apply (H ? H3)]] + |*:simplify in H2;simplify;elim (append_to_or_in_list ? ? ? ? H2) + [1,3:apply in_list_append1;apply (H ? H3) + |*:apply in_list_append2;apply (H1 ? H3)]] qed. (*** lemma on fresh names ***) @@ -298,8 +256,9 @@ cut (\forall l:(list nat).\exists n.\forall m. intros.unfold. intro. elim (in_cons_case ? ? ? ? H3) [rewrite > H4 in H2.autobatch - |elim H4.apply (H1 m ? H6). - apply (trans_le ? (max a t));autobatch]]] + |elim H4 + [apply (H1 m ? H4).apply (trans_le ? (max a t));autobatch + |assumption]]]] qed. (*** lemmata on well-formedness ***) @@ -308,89 +267,23 @@ lemma fv_WFT : \forall T,x,G.(WFType G T) \to (in_list ? x (fv_type T)) \to (in_list ? x (fv_env G)). intros 4.elim H [simplify in H2;elim (in_cons_case ? ? ? ? H2) - [rewrite > H3;assumption|elim H3;elim (in_list_nil ? ? H5)] + [rewrite > H3;assumption|elim (in_list_nil ? ? H3)] |simplify in H1;elim (in_list_nil ? x H1) - |simplify in H5;elim (nat_in_list_case ? ? ? H5);autobatch - |simplify in H5;elim (nat_in_list_case ? ? ? H5) - [elim (fresh_name ((fv_type t1) @ (fv_env l))); - cut ((¬ (in_list ? a (fv_type t1))) ∧ - (¬ (in_list ? a (fv_env l)))) + |simplify in H5;elim (append_to_or_in_list ? ? ? ? H5);autobatch + |simplify in H5;elim (append_to_or_in_list ? ? ? ? H5) + [apply (H2 H6) + |elim (fresh_name ((fv_type t1) @ (fv_env l))); + cut (¬ (a ∈ (fv_type t1)) ∧ ¬ (a ∈ (fv_env l))) [elim Hcut;lapply (H4 ? H9 H8) [cut (x ≠ a) [simplify in Hletin;elim (in_cons_case ? ? ? ? Hletin) - [elim (Hcut1 H10)|elim H10;assumption] - |intro;apply H8;rewrite < H10;assumption] + [elim (Hcut1 H10) + |assumption] + |intro;apply H8;applyS H6] |apply in_FV_subst;assumption] |split - [intro;apply H7;apply natinG_or_inH_to_natinGH;right;assumption - |intro;apply H7;apply natinG_or_inH_to_natinGH;left;assumption]] - |apply (H2 H6)]] -qed. - -(*** some exotic inductions and related lemmas ***) - -lemma O_lt_t_len: \forall T.O < (t_len T). -intros;elim T - [1,2,3:simplify;apply le_n - |*:simplify;apply lt_O_S] -qed. - -(* -lemma not_t_len_lt_SO : \forall T.\lnot (t_len T) < (S O). -intros;elim T - [1,2,3:simplify;unfold;intro;unfold in H;elim (not_le_Sn_n ? H) - |*:simplify;unfold;rewrite > max_case;elim (leb (t_len t) (t_len t1)) - [1,3:simplify in H2;apply H1;apply (trans_lt ? ? ? ? H2);unfold;constructor 1 - |*:simplify in H2;apply H;apply (trans_lt ? ? ? ? H2);unfold;constructor 1]] -qed. -*) - -lemma Typ_len_ind : \forall P:Typ \to Prop. - (\forall U.(\forall V.((t_len V) < (t_len U)) \to (P V)) - \to (P U)) - \to \forall T.(P T). -cut (\forall P:Typ \to Prop. - (\forall U.(\forall V.((t_len V) < (t_len U)) \to (P V)) - \to (P U)) - \to \forall T,n.(n = (t_len T)) \to (P T)) - [intros;apply (Hcut ? H ? (t_len T));reflexivity - |intros 4;generalize in match T;apply (nat_elim1 n);intros; - generalize in match H2;elim t - [1,2,3:apply H;intros;simplify in H4;elim (lt_to_not_le ? ? H4 (O_lt_t_len ?)) - |*:apply H;intros;apply (H1 (t_len V)) - [1,3:rewrite > H5;assumption - |*:reflexivity]]] -qed. - -lemma t_len_arrow1 : \forall T1,T2.(t_len T1) < (t_len (Arrow T1 T2)). -intros.simplify. -apply le_S_S.apply le_m_max_m_n. -qed. - -lemma t_len_arrow2 : \forall T1,T2.(t_len T2) < (t_len (Arrow T1 T2)). -intros.simplify. -apply le_S_S.apply le_n_max_m_n. -qed. - -lemma t_len_forall1 : \forall T1,T2.(t_len T1) < (t_len (Forall T1 T2)). -intros.simplify. -apply le_S_S.apply le_m_max_m_n. -qed. - -lemma t_len_forall2 : \forall T1,T2.(t_len T2) < (t_len (Forall T1 T2)). -intros.simplify. -apply le_S_S.apply le_n_max_m_n. -qed. - -lemma eq_t_len_TFree_subst : \forall T,n,X.(t_len T) = - (t_len (subst_type_nat T (TFree X) n)). -intro.elim T - [simplify;elim (eqb n n1);simplify;reflexivity - |2,3:simplify;reflexivity - |simplify;lapply (H n X);lapply (H1 n X);rewrite < Hletin;rewrite < Hletin1; - reflexivity - |simplify;lapply (H n X);lapply (H1 (S n) X);rewrite < Hletin; - rewrite < Hletin1;reflexivity] + [intro;apply H7;apply in_list_append1;assumption + |intro;apply H7;apply in_list_append2;assumption]]]] qed. (*** lemmata relating subtyping and well-formedness ***) @@ -454,8 +347,49 @@ intros 6;elim H [destruct H7;assumption |elim H7;elim H3;apply boundinenv_natinfv;apply (ex_intro ? ? b); apply (ex_intro ? ? T);assumption] - |elim H7;elim (in_cons_case ? ? ? ? H5) - [destruct H10;elim H3;apply boundinenv_natinfv;apply (ex_intro ? ? B); + |elim (in_cons_case ? ? ? ? H5) + [destruct H8;elim H3;apply boundinenv_natinfv;apply (ex_intro ? ? B); apply (ex_intro ? ? U);rewrite < Hcut1;assumption - |elim H10;apply (H2 H12 H9)]]] + |apply (H2 H8 H7)]]] +qed. + +lemma WFT_to_incl: ∀G,T,U. + (∀X.(¬(X ∈ fv_env G)) → (¬(X ∈ fv_type U)) → + (WFType (mk_bound true X T::G) (subst_type_nat U (TFree X) O))) + → incl ? (fv_type U) (fv_env G). +intros.elim (fresh_name ((fv_type U)@(fv_env G))).lapply(H a) + [unfold;intros;lapply (fv_WFT ? x ? Hletin) + [simplify in Hletin1;inversion Hletin1;intros + [destruct H4;elim H1;rewrite > Hcut;rewrite < H3.autobatch + |destruct H6;rewrite > Hcut1;assumption] + |apply in_FV_subst;assumption] + |*:intro;apply H1;autobatch] +qed. + +lemma incl_fv_env: ∀X,G,G1,U,P. + incl ? (fv_env (G1@(mk_bound true X U::G))) + (fv_env (G1@(mk_bound true X P::G))). +intros.rewrite < fv_env_extends.apply incl_A_A. +qed. + +lemma JSubtype_Top: ∀G,P.G ⊢ ⊤ ⊴ P → P = ⊤. +intros.inversion H;intros + [assumption|reflexivity + |destruct H5|*:destruct H6] +qed. + +(* elim vs inversion *) +lemma JS_trans_TFree: ∀G,T,X.G ⊢ T ⊴ (TFree X) → + ∀U.G ⊢ (TFree X) ⊴ U → G ⊢ T ⊴ U. +intros 4.cut (∀Y.TFree Y = TFree X → ∀U.G ⊢ (TFree Y) ⊴ U → G ⊢ T ⊴ U) + [apply Hcut;reflexivity + |elim H;intros + [rewrite > H3 in H4;rewrite > (JSubtype_Top ? ? H4);apply SA_Top;assumption + |rewrite < H3;assumption + |apply (SA_Trans_TVar ? ? ? ? H1);apply (H3 Y);assumption + |*:destruct H5]] qed. + +lemma fv_append : ∀G,H.fv_env (G @ H) = (fv_env G @ fv_env H). +intro;elim G;simplify;autobatch paramodulation; +qed. \ No newline at end of file diff --git a/matita/library/Fsub/part1a.ma b/matita/library/Fsub/part1a.ma index 7fb8fed9c..86cde322b 100644 --- a/matita/library/Fsub/part1a.ma +++ b/matita/library/Fsub/part1a.ma @@ -16,237 +16,149 @@ set "baseuri" "cic:/matita/Fsub/part1a/". include "Fsub/defn.ma". (*** Lemma A.1 (Reflexivity) ***) - theorem JS_Refl : ∀T,G.WFType G T → WFEnv G → G ⊢ T ⊴ T. -intros 3;elim H - [apply (SA_Refl_TVar l n H2 H1); - |apply (SA_Top l Top H1 (WFT_Top l)); - |apply (SA_Arrow l t t1 t t1 (H2 H5) (H4 H5)) - |apply (SA_All ? ? ? ? ? (H2 H5));intros;apply (H4 X H6) - [intro;apply H6;apply (fv_WFT (Forall t t1) X l) - [apply (WFT_Forall ? ? ? H1 H3) - |simplify;autobatch] +intros 3.elim H + [apply SA_Refl_TVar [apply H2|assumption] + |apply SA_Top [assumption|apply WFT_Top] + |apply (SA_Arrow ? ? ? ? ? (H2 H5) (H4 H5)) + |apply (SA_All ? ? ? ? ? (H2 H5));intros;apply (H4 ? H6) + [intro;apply H6;apply (fv_WFT ? ? ? (WFT_Forall ? ? ? H1 H3)); + simplify;autobatch |autobatch]] qed. -(* +(* * A slightly more general variant to lemma A.2.2, where weakening isn't * defined as concatenation of any two disjoint environments, but as * set inclusion. *) - -lemma JS_weakening : \forall G,T,U.(JSubtype G T U) \to - \forall H.(WFEnv H) \to (incl ? G H) \to (JSubtype H T U). + +lemma JS_weakening : ∀G,T,U.G ⊢ T ⊴ U → ∀H.WFEnv H → incl ? G H → H ⊢ T ⊴ U. intros 4;elim H - [apply (SA_Top ? ? H4);lapply (incl_bound_fv ? ? H5); - apply (WFT_env_incl ? ? H2 ? Hletin) - |apply (SA_Refl_TVar ? ? H4);lapply (incl_bound_fv ? ? H5); - apply (Hletin ? H2) - |lapply (H3 ? H5 H6);lapply (H6 ? H1); - apply (SA_Trans_TVar ? ? ? ? Hletin1 Hletin) - |lapply (H2 ? H6 H7);lapply (H4 ? H6 H7); - apply (SA_Arrow ? ? ? ? ? Hletin Hletin1) - |lapply (H2 ? H6 H7);apply (SA_All ? ? ? ? ? Hletin);intros;apply H4 - [unfold;intro;apply H8;lapply (incl_bound_fv ? ? H7);apply (Hletin1 ? H9) - |apply WFE_cons - [1,2:assumption - |apply (JS_to_WFT1 ? ? ? Hletin)] - |unfold;intros;elim (in_cons_case ? ? ? ? H9) - [rewrite > H10;apply in_Base - |elim H10;apply (in_Skip ? ? ? ? ? H11);apply (H7 ? H12)]]] + [apply (SA_Top ? ? H4);apply (WFT_env_incl ? ? H2 ? (incl_bound_fv ? ? H5)) + |apply (SA_Refl_TVar ? ? H4);apply (incl_bound_fv ? ? H5 ? H2) + |apply (SA_Trans_TVar ? ? ? ? ? (H3 ? H5 H6));apply H6;assumption + |apply (SA_Arrow ? ? ? ? ? (H2 ? H6 H7) (H4 ? H6 H7)) + |apply (SA_All ? ? ? ? ? (H2 ? H6 H7));intros;apply H4 + [unfold;intro;apply H8;apply (incl_bound_fv ? ? H7 ? H9) + |apply (WFE_cons ? ? ? ? H6 H8);autobatch + |unfold;intros;inversion H9;intros + [destruct H11;rewrite > Hcut;apply in_Base + |destruct H13;rewrite < Hcut1 in H10;apply in_Skip;apply (H7 ? H10)]]] qed. -lemma decidable_eq_Typ : \forall S,T:Typ.(S = T) ∨ (S ≠ T). -intro;elim S - [elim T - [elim (decidable_eq_nat n n1) - [rewrite > H;left;reflexivity - |right;intro;destruct H1;apply (H Hcut)] - |2,3:right;intro;destruct H - |*:right;intro;destruct H2] - |elim T - [2:elim (decidable_eq_nat n n1) - [rewrite > H;left;reflexivity - |right;intro;destruct H1;apply (H Hcut)] - |1,3:right;intro;destruct H - |*:right;intro;destruct H2] - |elim T - [3:left;reflexivity - |1,2:right;intro;destruct H - |*:right;intro;destruct H2] - |elim T - [1,2,3:right;intro;destruct H2 - |elim (H t2) - [rewrite > H4;elim (H1 t3) - [rewrite > H5;left;reflexivity - |right;intro;apply H5;destruct H6;assumption] - |right;intro;apply H4;destruct H5;assumption] - |right;intro;destruct H4] - |elim T - [1,2,3:right;intro;destruct H2 - |right;intro;destruct H4 - |elim (H t2) - [rewrite > H4;elim (H1 t3) - [rewrite > H5;left;reflexivity - |right;intro;apply H5;destruct H6;assumption] - |right;intro;apply H4;destruct H5;assumption]]] +theorem narrowing:∀X,G,G1,U,P,M,N. + G1 ⊢ P ⊴ U → (∀G2,T.G2@G1 ⊢ U ⊴ T → G2@G1 ⊢ P ⊴ T) → G ⊢ M ⊴ N → + ∀l.G=l@(mk_bound true X U::G1) → l@(mk_bound true X P::G1) ⊢ M ⊴ N. +intros 10.elim H2 + [apply SA_Top + [rewrite > H5 in H3; + apply (WFE_Typ_subst ? ? ? ? ? ? ? H3 (JS_to_WFT1 ? ? ? H)) + |rewrite > H5 in H4;apply (WFT_env_incl ? ? H4);apply incl_fv_env] + |apply SA_Refl_TVar + [rewrite > H5 in H3;apply (WFE_Typ_subst ? ? ? ? ? ? ? H3); + apply (JS_to_WFT1 ? ? ? H) + |rewrite > H5 in H4;rewrite < fv_env_extends;apply H4] + |elim (decidable_eq_nat X n) + [apply (SA_Trans_TVar ? ? ? P) + [rewrite < H7;elim l1;simplify + [constructor 1|constructor 2;assumption] + |rewrite > append_cons;apply H1; + lapply (WFE_bound_bound true n t1 U ? ? H3) + [apply (JS_to_WFE ? ? ? H4) + |rewrite < Hletin;rewrite < append_cons;apply (H5 ? H6) + |rewrite < H7;rewrite > H6;elim l1;simplify + [constructor 1|constructor 2;assumption]]] + |apply (SA_Trans_TVar ? ? ? t1) + [rewrite > H6 in H3;apply (lookup_env_extends ? ? ? ? ? ? ? ? ? ? H3); + unfold;intro;apply H7;symmetry;assumption + |apply (H5 ? H6)]] + |apply (SA_Arrow ? ? ? ? ? (H4 ? H7) (H6 ? H7)) + |apply (SA_All ? ? ? ? ? (H4 ? H7));intros; + apply (H6 ? ? (mk_bound true X1 t2::l1)) + [rewrite > H7;rewrite > fv_env_extends;apply H8 + |simplify;rewrite < H7;reflexivity]] qed. -lemma decidable_eq_bound: ∀b1,b2:bound.(b1 = b2) ∨ (b1 ≠ b2). -intros;elim b1;elim b2;elim (decidable_eq_nat n n1) - [rewrite < H;elim (decidable_eq_Typ t t1) - [rewrite < H1;elim (bool_to_decidable_eq b b3) - [rewrite > H2;left;reflexivity - |right;intro;destruct H3;apply (H2 Hcut)] - |right;intro;destruct H2;apply (H1 Hcut1)] - |right;intro;destruct H1;apply (H Hcut1)] -qed. - -(* Lemma A.3 (Transitivity and Narrowing) *) - -lemma JS_trans_narrow : \forall Q. - (\forall G,T,U. - (JSubtype G T Q) \to (JSubtype G Q U) \to - (JSubtype G T U)) \land - (\forall G,H,X,P,M,N. - (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)). -apply Typ_len_ind;intros 2; -cut (\forall G,T,P. - (JSubtype G T U) \to - (JSubtype G U P) \to - (JSubtype G T P)) - [split - [assumption - |cut (\forall G,M,N.(JSubtype G M N) \to - \forall G1,X,G2,P. - (G = G2 @ ((mk_bound true X U) :: G1)) \to - (JSubtype G1 P U) \to - (JSubtype (G2 @ ((mk_bound true X P) :: G1)) M N)) - [intros;apply (Hcut1 ? ? ? H2 ? ? ? ? ? H3);reflexivity - |intros;cut (incl ? (fv_env (G2 @ ((mk_bound true X U)::G1))) - (fv_env (G2 @ ((mk_bound true X P)::G1)))) - [intros;generalize in match H2;generalize in match Hcut1; - generalize in match Hcut;generalize in match G2;elim H1 - [apply SA_Top - [rewrite > H8 in H4;lapply (JS_to_WFT1 ? ? ? H3); - apply (WFE_Typ_subst ? ? ? ? ? ? ? H4 Hletin) - |rewrite > H8 in H5;apply (WFT_env_incl ? ? H5 ? H7)] - |apply SA_Refl_TVar - [rewrite > H8 in H4;apply (WFE_Typ_subst ? ? ? ? ? ? ? H4); - apply (JS_to_WFT1 ? ? ? H3) - |rewrite > H8 in H5;apply (H7 ? H5)] - |elim (decidable_eq_nat X n) - [apply (SA_Trans_TVar ? ? ? P) - [rewrite < H10;elim l1 - [simplify;constructor 1 - |simplify;elim (decidable_eq_bound (mk_bound true X P) t2) - [rewrite < H12;apply in_Base - |apply (in_Skip ? ? ? ? ? H12);assumption]] - |apply H7 - [lapply (H6 ? H7 H8 H9);lapply (JS_to_WFE ? ? ? Hletin); - apply (JS_weakening ? ? ? H3 ? Hletin1);unfold;intros; - elim l1 - [simplify; - elim (decidable_eq_bound x (mk_bound true X P)) - [rewrite < H12;apply in_Base - |apply (in_Skip ? ? ? ? ? H12);assumption] - |simplify;elim (decidable_eq_bound x t2) - [rewrite < H13;apply in_Base - |apply (in_Skip ? ? ? ? ? H13);assumption]] - |lapply (WFE_bound_bound true n t1 U ? ? H4) - [apply (JS_to_WFE ? ? ? H5) - |rewrite < Hletin;apply (H6 ? H7 H8 H9) - |rewrite > H9;rewrite > H10;elim l1;simplify - [constructor 1 - |elim (decidable_eq_bound (mk_bound true n U) t2) - [rewrite > H12;apply in_Base - |apply (in_Skip ? ? ? ? ? H12);assumption]]]]] - |apply (SA_Trans_TVar ? ? ? t1) - [rewrite > H9 in H4; - apply (lookup_env_extends ? ? ? ? ? ? ? ? ? ? H4); - unfold;intro;apply H10;symmetry;assumption - |apply (H6 ? H7 H8 H9)]] - |apply SA_Arrow - [apply (H5 ? H8 H9 H10) - |apply (H7 ? H8 H9 H10)] - |apply SA_All - [apply (H5 ? H8 H9 H10) - |intros;apply (H7 ? ? (mk_bound true X1 t2::l1) H8) - [rewrite > H10;cut ((fv_env (l1@(mk_bound true X P::G1))) = - (fv_env (l1@(mk_bound true X U::G1)))) - [unfold;intro;apply H11;rewrite > Hcut2;assumption - |elim l1 - [simplify;reflexivity - |elim t4;simplify;rewrite > H12;reflexivity]] - |simplify;apply (incl_nat_cons ? ? ? H9) - |simplify;rewrite < H10;reflexivity]]] - |cut ((fv_env (G2@(mk_bound true X U::G1))) = - (fv_env (G2@(mk_bound true X P::G1)))) - [rewrite > Hcut1;unfold;intros;assumption - |elim G2 - [simplify;reflexivity - |elim t;simplify;rewrite > H4;reflexivity]]]]] - |intros 4;generalize in match H;elim H1 - [inversion H5 - [intros;rewrite < H8;apply (SA_Top ? ? H2 H3) - |intros;destruct H9 - |intros;destruct H10 - |*:intros;destruct H11] - |assumption - |apply (SA_Trans_TVar ? ? ? ? H2);apply (H4 H5 H6) - |inversion H7 - [intros;apply (SA_Top ? ? H8);rewrite < H10;apply WFT_Arrow - [apply (JS_to_WFT2 ? ? ? H2) - |apply (JS_to_WFT1 ? ? ? H4)] - |intros;destruct H11 - |intros;destruct H12 - |intros;destruct H13;apply SA_Arrow - [rewrite > H12 in H2;rewrite < Hcut in H8; - lapply (H6 t2) - [elim Hletin;apply (H15 ? ? ? H8 H2) - |apply (t_len_arrow1 t2 t3)] - |rewrite > H12 in H4;rewrite < Hcut1 in H10; - lapply (H6 t3) - [elim Hletin;apply (H15 ? ? ? H4 H10) - |apply (t_len_arrow2 t2 t3)]] - |intros;destruct H13] - |inversion H7 - [intros;apply (SA_Top ? ? H8);rewrite < H10;apply WFT_Forall - [apply (JS_to_WFT2 ? ? ? H2) - |intros;lapply (H4 ? H13);lapply (JS_to_WFT1 ? ? ? Hletin); - apply (WFT_env_incl ? ? Hletin1);simplify;unfold;intros; - assumption] - |intros;destruct H11 - |intros;destruct H12 - |intros;destruct H13 - |intros;destruct H13;subst;apply SA_All - [lapply (H6 t4) - [elim Hletin;apply (H12 ? ? ? H8 H2) - |apply t_len_forall1] - |intros;(*destruct H12;*)subst; - lapply (H6 (subst_type_nat t5 (TFree X) O)) - [elim Hletin;apply H13 - [lapply (H6 t4) - [elim Hletin1;apply (H16 l1 [] X t6); - [simplify;apply H4;assumption - |assumption] - |apply t_len_forall1] - |apply (H10 ? H12)] - |rewrite < eq_t_len_TFree_subst; - apply t_len_forall2]]]]] +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 + [apply (JS_trans_TFree ? ? ? H3 ? H4) + |rewrite > (JSubtype_Top ? ? H3);apply SA_Top;autobatch + |cut (∃T.T = Arrow t t1) as Htriv + [elim Htriv;clear Htriv;rewrite < H in H6;rewrite < H in H7; + generalize in match H7;generalize in match H4;generalize in match H2; + generalize in match H5;generalize in match H;clear H7 H4 H2 H5 H;elim H6 + [1,2:destruct H4 + |apply (SA_Trans_TVar ? ? ? ? H);apply (H4 H5 H7 H8 H9);assumption + |inversion H11;intros + [apply SA_Top;rewrite < H14;autobatch + |destruct H15 + |destruct H16 + |destruct H17;apply SA_Arrow;rewrite < H16;destruct H7 + [apply H9 + [autobatch + |rewrite < Hcut2;rewrite > Hcut;rewrite > H16;assumption + |rewrite < Hcut2;assumption] + |apply H10 + [autobatch + |rewrite < Hcut3;rewrite < Hcut1;rewrite < H16;assumption + |rewrite > H16;rewrite < Hcut3;rewrite > Hcut1;assumption]] + |destruct H17] + |destruct H7] + |apply (ex_intro ? ? (Arrow t t1));reflexivity] + |cut (∃T.T = Forall t t1) as Htriv + [elim Htriv;clear Htriv;rewrite < H in H7;rewrite < H in H6. + generalize in match H7;generalize in match H4;generalize in match H2; + generalize in match H5;generalize in match H;clear H7 H4 H2 H5 H; + elim H6 + [1,2:destruct H4 + |apply (SA_Trans_TVar ? ? ? ? H);apply (H4 H5 H7 H8 H9 H10) + |destruct H7 + |inversion H11;intros + [apply SA_Top + [assumption + |rewrite < H14;apply WFT_Forall + [autobatch + |intros;lapply (H4 ? H17);autobatch]] + |destruct H15 + |destruct H16 + |destruct H17 + |destruct H17;apply SA_All;destruct H7 + [rewrite < H16;apply H9; + [autobatch + |rewrite < Hcut2;rewrite > Hcut;rewrite > H16;assumption + |rewrite < Hcut2. assumption] + |intros;apply (H10 X) + [intro;apply H19;rewrite < H16;apply H8;assumption + |intro;apply H19;rewrite < H16;apply H8; + apply (WFT_to_incl ? ? ? H3);assumption + |simplify;apply incl_cons;rewrite < H16;assumption + |apply (narrowing X ((mk_bound true X t6)::l2) + ? ? ? ? ? H12 ? ? []) + [intros;apply H9 + [unfold;intros;lapply (H8 ? H21);rewrite < H16; + rewrite > fv_append;autobatch + |rewrite < Hcut2;rewrite > Hcut; + apply (JS_weakening ? ? ? H12) + [autobatch + |unfold;intros;autobatch] + |rewrite < Hcut2;rewrite > Hcut;assumption] + |rewrite < Hcut;rewrite < Hcut3;rewrite < H16;apply H4; + rewrite > H16;assumption + |reflexivity] + |rewrite < Hcut3;rewrite > Hcut1;apply H14;assumption]]]] + |apply (ex_intro ? ? (Forall t t1));reflexivity]] qed. -theorem JS_trans : \forall G,T,U,V.(JSubtype G T U) \to - (JSubtype G U V) \to - (JSubtype G T V). -intros;elim JS_trans_narrow;autobatch; +theorem JS_trans : ∀G,T,U,V.G ⊢ T ⊴ U → G ⊢ U ⊴ V → G ⊢ T ⊴ V. +intros 5;apply (JS_trans_prova ? G);autobatch; qed. -theorem JS_narrow : \forall G1,G2,X,P,Q,T,U. - (JSubtype (G2 @ (mk_bound true X Q :: G1)) T U) \to - (JSubtype G1 P Q) \to - (JSubtype (G2 @ (mk_bound true X P :: G1)) T U). -intros;elim JS_trans_narrow;autobatch; +theorem JS_narrow : ∀G1,G2,X,P,Q,T,U. + (G2 @ (mk_bound true X Q :: G1)) ⊢ T ⊴ U → G1 ⊢ P ⊴ Q → + (G2 @ (mk_bound true X P :: G1)) ⊢ T ⊴ U. +intros;apply (narrowing ? ? ? ? ? ? ? H1 ? H) [|autobatch] +intros;apply (JS_trans ? ? ? ? ? H2);apply (JS_weakening ? ? ? H1); + [autobatch|unfold;intros;autobatch] qed. diff --git a/matita/library/Fsub/util.ma b/matita/library/Fsub/util.ma index 5446efe56..ac93f8ccf 100644 --- a/matita/library/Fsub/util.ma +++ b/matita/library/Fsub/util.ma @@ -45,7 +45,7 @@ qed. inductive in_list (A:Type): A → (list A) → Prop ≝ | in_Base : ∀ x,l.(in_list A x (x::l)) -| in_Skip : ∀ x,y,l.(in_list A x l) → (x ≠ y) → (in_list A x (y::l)). +| in_Skip : ∀ x,y,l.(in_list A x l) → (in_list A x (y::l)). notation > "hvbox(x ∈ l)" non associative with precedence 30 for @{ 'inlist $x $l }. @@ -54,12 +54,6 @@ notation < "hvbox(x \nbsp ∈ \nbsp l)" interpretation "item in list" 'inlist x l = (cic:/matita/Fsub/util/in_list.ind#xpointer(1/1) _ x l). -lemma in_Skip2 : ∀x,y,l.(in_list nat x l) → (in_list nat x (y::l)). -intros;elim (decidable_eq_nat x y) - [rewrite > H1;apply in_Base - |apply (in_Skip ? ? ? ? H H1)] -qed. - definition incl : \forall A.(list A) \to (list A) \to Prop \def \lambda A,l,m.\forall x.(in_list A x l) \to (in_list A x m). @@ -74,17 +68,70 @@ definition map : \forall A,B,f.((list A) \to (list B)) \def lemma in_list_nil : \forall A,x.\lnot (in_list A x []). intros.unfold.intro.inversion H [intros;lapply (sym_eq ? ? ? H2);destruct Hletin - |intros;destruct H5] + |intros;destruct H4] qed. -lemma in_cons_case : ∀A.∀x,h:A.∀t:list A.x ∈ h::t → x = h ∨ (x ≠ h ∧ (x ∈ t)). +lemma in_cons_case : ∀A.∀x,h:A.∀t:list A.x ∈ h::t → x = h ∨ (x ∈ t). intros;inversion H;intros [destruct H2;left;symmetry;assumption - |destruct H5;right;split [rewrite > Hcut|rewrite > Hcut1] assumption ] + |destruct H4;right;applyS H1] +qed. + +lemma append_nil:\forall A:Type.\forall l:list A. l@[]=l. +intros. +elim l;intros;autobatch. +qed. + +lemma append_cons:\forall A.\forall a:A.\forall l,l1. +l@(a::l1)=(l@[a])@l1. +intros. +rewrite > associative_append. +reflexivity. +qed. + +lemma in_list_append1: \forall A.\forall x:A. +\forall l1,l2. x \in l1 \to x \in l1@l2. +intros. +elim H + [simplify.apply in_Base + |simplify.apply in_Skip.assumption + ] +qed. + +lemma in_list_append2: \forall A.\forall x:A. +\forall l1,l2. x \in l2 \to x \in l1@l2. +intros 3. +elim l1 + [simplify.assumption + |simplify.apply in_Skip.apply H.assumption + ] +qed. + +theorem append_to_or_in_list: \forall A:Type.\forall x:A. +\forall l,l1. x \in l@l1 \to (x \in l) \lor (x \in l1). +intros 3. +elim l + [right.apply H + |simplify in H1.inversion H1;intros + [destruct H3.left.rewrite < Hcut. + apply in_Base + |destruct H5. + elim (H l2) + [left.apply in_Skip. + rewrite < H4.assumption + |right.rewrite < H4.assumption + |rewrite > Hcut1.rewrite > H4.assumption + ] + ] + ] qed. lemma max_case : \forall m,n.(max m n) = match (leb m n) with [ false \Rightarrow n | true \Rightarrow m ]. intros;elim m;simplify;reflexivity; +qed. + +lemma incl_A_A: ∀T,A.incl T A A. +intros.unfold incl.intros.assumption. qed. \ No newline at end of file -- 2.39.2