X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FPOPLmark%2FFsub%2Fdefn.ma;h=184166ed9346616940e739b222dd408a327e623b;hb=6302e8ebc63beb73aa672c9c23199bdfaa3f8715;hp=2a5367834890b395b980fd2de1e6af23989b8ca1;hpb=ef3e622c49ce8a0478c3ef1326d4f179aff3d1ed;p=helm.git diff --git a/helm/software/matita/contribs/POPLmark/Fsub/defn.ma b/helm/software/matita/contribs/POPLmark/Fsub/defn.ma index 2a5367834..184166ed9 100644 --- a/helm/software/matita/contribs/POPLmark/Fsub/defn.ma +++ b/helm/software/matita/contribs/POPLmark/Fsub/defn.ma @@ -12,7 +12,6 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/Fsub/defn". include "Fsub/util.ma". (*** representation of Fsub types ***) @@ -44,16 +43,6 @@ let rec subst_type_nat T U i \def | (Arrow T1 T2) \Rightarrow (Arrow (subst_type_nat T1 U i) (subst_type_nat T2 U i)) | (Forall T1 T2) \Rightarrow (Forall (subst_type_nat T1 U i) (subst_type_nat T2 U (S i))) ]. -(*** height of T's syntactic tree ***) - -let rec t_len T \def - match T with - [(TVar n) \Rightarrow (S O) - |(TFree X) \Rightarrow (S O) - |Top \Rightarrow (S O) - |(Arrow T1 T2) \Rightarrow (S (max (t_len T1) (t_len T2))) - |(Forall T1 T2) \Rightarrow (S (max (t_len T1) (t_len T2)))]. - (*** definitions about lists ***) definition fv_env : (list bound) \to (list nat) \def @@ -147,11 +136,6 @@ notation "hvbox(S [# n ↦ T])" interpretation "subst bound var" 'substvar S T n = (cic:/matita/Fsub/defn/subst_type_nat.con S T n). -notation "hvbox(|T|)" - non associative with precedence 30 for @{ 'tlen $T }. -interpretation "type length" 'tlen T = - (cic:/matita/Fsub/defn/t_len.con T). - notation "hvbox(!X ⊴ T)" non associative with precedence 60 for @{ 'subtypebound $X $T }. interpretation "subtyping bound" 'subtypebound X T = @@ -165,21 +149,22 @@ lemma boundinenv_natinfv : \forall x,G. (\exists B,T.(in_list ? (mk_bound B x T) G)) \to (in_list ? x (fv_env G)). 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 - |simplify;apply in_Skip;apply H;apply (ex_intro ? ? a); - apply (ex_intro ? ? a1);assumption]] + [elim H;elim H1;lapply (not_in_list_nil ? ? H2);elim Hletin + |elim H1;elim H2;elim (in_list_cons_case ? ? ? ? H3) + [rewrite < H4;simplify;apply in_list_head + |simplify;apply in_list_cons;apply H;apply (ex_intro ? ? a1); + apply (ex_intro ? ? a2);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 (H H2);elim H3;apply (ex_intro ? ? a); - apply (ex_intro ? ? a1);apply in_Skip;assumption]] + [simplify;intro;lapply (not_in_list_nil ? ? H);elim Hletin + |intros 3; + elim a;simplify in H1;elim (in_list_cons_case ? ? ? ? H1) + [rewrite < H2;apply (ex_intro ? ? b);apply (ex_intro ? ? t);apply in_list_head + |elim (H H2);elim H3;apply (ex_intro ? ? a1); + apply (ex_intro ? ? a2);apply in_list_cons;assumption]] qed. lemma incl_bound_fv : \forall l1,l2.(incl ? l1 l2) \to @@ -194,8 +179,8 @@ qed. 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|apply in_Skip;apply (H ? H2)] +intros.unfold in H.unfold.intros.elim (in_list_cons_case ? ? ? ? H1) + [rewrite > H2;apply in_list_head|apply in_list_cons;apply (H ? H2)] qed. lemma WFT_env_incl : \forall G,T.(WFType G T) \to @@ -215,7 +200,7 @@ lemma fv_env_extends : \forall H,x,B,C,T,U,G. (fv_env (H @ ((mk_bound B x T) :: G))) = (fv_env (H @ ((mk_bound C x U) :: G))). intros;elim H - [simplify;reflexivity|elim t;simplify;rewrite > H1;reflexivity] + [simplify;reflexivity|elim a;simplify;rewrite > H1;reflexivity] qed. lemma lookup_env_extends : \forall G,H,B,C,D,T,U,V,x,y. @@ -223,22 +208,22 @@ lemma lookup_env_extends : \forall G,H,B,C,D,T,U,V,x,y. (y \neq x) \to (in_list ? (mk_bound D y V) (H @ ((mk_bound B x T) :: G))). intros 10;elim H - [simplify in H1;elim (in_cons_case ? ? ? ? H1) + [simplify in H1;elim (in_list_cons_case ? ? ? ? H1) [destruct H3;elim (H2);reflexivity - |simplify;apply (in_Skip ? ? ? ? H3);] - |simplify in H2;simplify;elim (in_cons_case ? ? ? ? H2) - [rewrite > H4;apply in_Base - |apply (in_Skip ? ? ? ? (H1 H4 H3))]] + |simplify;apply (in_list_cons ? ? ? ? H3);] + |simplify in H2;simplify;elim (in_list_cons_case ? ? ? ? H2) + [rewrite > H4;apply in_list_head + |apply (in_list_cons ? ? ? ? (H1 H4 H3))]] qed. lemma in_FV_subst : \forall x,T,U,n.(in_list ? x (fv_type T)) \to (in_list ? x (fv_type (subst_type_nat T U n))). intros 3;elim T - [simplify in H;elim (in_list_nil ? ? H) + [simplify in H;elim (not_in_list_nil ? ? H) |2,3:simplify;simplify in H;assumption - |*: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)]] + |*:simplify in H2;simplify;elim (in_list_append_to_or_in_list ? ? ? ? H2) + [1,3:apply in_list_to_in_list_append_l;apply (H ? H3) + |*:apply in_list_to_in_list_append_r;apply (H1 ? H3)]] qed. (*** lemma on fresh names ***) @@ -250,14 +235,14 @@ cut (\forall l:(list nat).\exists n.\forall m. [apply a |apply H;constructor 1] |intros;elim l - [apply (ex_intro ? ? O);intros;unfold;intro;elim (in_list_nil ? ? H1) + [apply (ex_intro ? ? O);intros;unfold;intro;elim (not_in_list_nil ? ? H1) |elim H; - apply (ex_intro ? ? (S (max a t))). + apply (ex_intro ? ? (S (max a1 a))). intros.unfold. intro. - elim (in_cons_case ? ? ? ? H3) + elim (in_list_cons_case ? ? ? ? H3) [rewrite > H4 in H2.autobatch |elim H4 - [apply (H1 m ? H4).apply (trans_le ? (max a t));autobatch + [apply (H1 m ? H4).apply (trans_le ? (max a1 a));autobatch |assumption]]]] qed. @@ -266,24 +251,24 @@ qed. 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 (in_list_nil ? ? H3)] - |simplify in H1;elim (in_list_nil ? x H1) - |simplify in H5;elim (append_to_or_in_list ? ? ? ? H5);autobatch - |simplify in H5;elim (append_to_or_in_list ? ? ? ? H5) + [simplify in H2;elim (in_list_cons_case ? ? ? ? H2) + [rewrite > H3;assumption|elim (not_in_list_nil ? ? H3)] + |simplify in H1;elim (not_in_list_nil ? x H1) + |simplify in H5;elim (in_list_append_to_or_in_list ? ? ? ? H5);autobatch + |simplify in H5;elim (in_list_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) + [simplify in Hletin;elim (in_list_cons_case ? ? ? ? Hletin) [elim (Hcut1 H10) |assumption] |intro;apply H8;applyS H6] |apply in_FV_subst;assumption] |split - [intro;apply H7;apply in_list_append1;assumption - |intro;apply H7;apply in_list_append2;assumption]]]] + [intro;apply H7;apply in_list_to_in_list_append_l;assumption + |intro;apply H7;apply in_list_to_in_list_append_r;assumption]]]] qed. (*** lemmata relating subtyping and well-formedness ***) @@ -324,7 +309,7 @@ intros 7;elim H 0 [simplify;intros;(*FIXME*)generalize in match H1;intro;inversion H1;intros [lapply (nil_cons ? G (mk_bound B x T));elim (Hletin H4) |destruct H8;apply (WFE_cons ? ? ? ? H4 H6 H2)] - |intros;simplify;generalize in match H2;elim t;simplify in H4; + |intros;simplify;generalize in match H2;elim a;simplify in H4; inversion H4;intros [destruct H5 |destruct H9;apply WFE_cons @@ -339,13 +324,13 @@ 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 - |elim (in_cons_case ? ? ? ? H6) - [destruct H7;destruct;elim (in_cons_case ? ? ? ? H5) + [lapply (not_in_list_nil ? ? H1);elim Hletin + |elim (in_list_cons_case ? ? ? ? H6) + [destruct H7;destruct;elim (in_list_cons_case ? ? ? ? H5) [destruct H7;reflexivity |elim H7;elim H3;apply boundinenv_natinfv;apply (ex_intro ? ? B); apply (ex_intro ? ? T);assumption] - |elim (in_cons_case ? ? ? ? H5) + |elim (in_list_cons_case ? ? ? ? H5) [destruct H8;elim H3;apply boundinenv_natinfv;apply (ex_intro ? ? B); apply (ex_intro ? ? U);assumption |apply (H2 H8 H7)]]] @@ -376,6 +361,7 @@ intros.inversion H;intros |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. @@ -387,7 +373,8 @@ intros 4.cut (∀Y.TFree Y = TFree X → ∀U.G ⊢ (TFree Y) ⊴ U → G ⊢ T |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 +qed.