X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Flibrary%2FFsub%2Fdefn.ma;h=550f8271e236324182697029b591ac9f3d8a1d09;hb=72e7d9c9d410ded571b9d3c396197b26181c1e2a;hp=8ff30ce1f7411f5424506ff6f011fbd75584fe23;hpb=59f20005cd1064eb12c2dbdb829c4380100bd40f;p=helm.git diff --git a/matita/library/Fsub/defn.ma b/matita/library/Fsub/defn.ma index 8ff30ce1f..550f8271e 100644 --- a/matita/library/Fsub/defn.ma +++ b/matita/library/Fsub/defn.ma @@ -21,7 +21,7 @@ include "list/list.ma". include "Fsub/util.ma". (*** representation of Fsub types ***) -inductive Typ : Set \def +inductive Typ : Type \def | TVar : nat \to Typ (* type var *) | TFree: nat \to Typ (* free type name *) | Top : Typ (* maximum type *) @@ -29,7 +29,7 @@ inductive Typ : Set \def | Forall : Typ \to Typ \to Typ. (* universal type *) (*** representation of Fsub terms ***) -inductive Term : Set \def +inductive Term : Type \def | Var : nat \to Term (* variable *) | Free : nat \to Term (* free name *) | Abs : Typ \to Term \to Term (* abstraction *) @@ -39,7 +39,7 @@ inductive Term : Set \def (* representation of bounds *) -record bound : Set \def { +record bound : Type \def { istype : bool; (* is subtyping bound? *) name : nat ; (* name *) btype : Typ (* type to which the name is bound *) @@ -354,11 +354,11 @@ 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 s;simplify in H1;inversion H1 + |intros 3;elim t;simplify in H1;inversion H1 [intros;rewrite < H2;simplify;apply ex_intro [apply b |apply ex_intro - [apply t + [apply t1 |lapply (inj_head_nat ? ? ? ? H3);rewrite > H2;rewrite < Hletin; apply in_Base]] |intros;lapply (inj_tail ? ? ? ? ? H5);rewrite < Hletin in H2; @@ -411,7 +411,7 @@ 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 2;elim t;simplify in H2;inversion H2 [intros;lapply (inj_head_nat ? ? ? ? H4);rewrite > Hletin;right; simplify;constructor 1 |intros;lapply (inj_tail ? ? ? ? ? H6); @@ -441,10 +441,10 @@ lemma varinG_or_varinH_to_varinGH : \forall G,H,x. intros.elim H1 0 [elim H [simplify;assumption - |elim s;simplify;constructor 2;apply (H2 H3)] + |elim t;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 2;elim t;simplify in H3;inversion H3 [intros;lapply (inj_head_nat ? ? ? ? H5);rewrite > Hletin;simplify; constructor 1 |intros;simplify;constructor 2;rewrite < H6;apply H2; @@ -481,7 +481,7 @@ lemma fv_env_extends : \forall H,x,B,C,T,U,G. (fv_env (H @ ((mk_bound C x U) :: G))). intros;elim H [simplify;reflexivity - |elim s;simplify;rewrite > H1;reflexivity] + |elim t;simplify;rewrite > H1;reflexivity] qed. lemma lookup_env_extends : \forall G,H,B,C,D,T,U,V,x,y. @@ -542,8 +542,8 @@ intros 3;elim T 0 [1,3:elim Hcut;elim H4;elim H5;clear Hcut H4 H5;rewrite > (H H6 H8); rewrite > (H1 H7 H9);reflexivity |*:split - [1,3:split;unfold;intro;apply H2;apply natinG_or_inH_to_natinGH;auto - |*:split;unfold;intro;apply H3;apply natinG_or_inH_to_natinGH;auto]]] + [1,3:split;unfold;intro;apply H2;apply natinG_or_inH_to_natinGH;autobatch + |*:split;unfold;intro;apply H3;apply natinG_or_inH_to_natinGH;autobatch]]] qed. lemma subst_type_nat_swap : \forall u,v,T,X,m. @@ -597,7 +597,7 @@ lemma lookup_swap : \forall x,u,v,T,B,G.(in_list ? (mk_bound B x T) G) \to (in_list ? (mk_bound B (swap u v x) (swap_Typ u v T)) (swap_Env u v G)). intros 6;elim G 0 [intros;elim (in_list_nil ? ? H) - |intro;elim s;simplify;inversion H1 + |intro;elim t;simplify;inversion H1 [intros;lapply (inj_head ? ? ? ? H3);rewrite < H2 in Hletin; destruct Hletin;rewrite > Hcut;rewrite > Hcut1;rewrite > Hcut2; apply in_Base @@ -628,13 +628,13 @@ lemma in_dom_swap : \forall u,v,x,G. intros;split [elim G 0 [simplify;intro;elim (in_list_nil ? ? H) - |intro;elim s 0;simplify;intros;inversion H1 + |intro;elim t 0;simplify;intros;inversion H1 [intros;lapply (inj_head_nat ? ? ? ? H3);rewrite > Hletin;apply in_Base |intros;lapply (inj_tail ? ? ? ? ? H5);rewrite < Hletin in H2; rewrite > H4 in H;apply in_Skip;apply (H H2)]] |elim G 0 [simplify;intro;elim (in_list_nil ? ? H) - |intro;elim s 0;simplify;intros;inversion H1 + |intro;elim t 0;simplify;intros;inversion H1 [intros;lapply (inj_head_nat ? ? ? ? H3);rewrite < H2 in Hletin; lapply (swap_inj ? ? ? ? Hletin);rewrite > Hletin1;apply in_Base |intros;lapply (inj_tail ? ? ? ? ? H5);rewrite < Hletin in H2; @@ -657,7 +657,7 @@ cut (\forall l:(list nat).\exists n.\forall m. [assumption|apply nil_cons] |intros;lapply (sym_eq ? ? ? H5);absurd (a1::l1 = []) [assumption|apply nil_cons]]] - |elim H;lapply (decidable_eq_nat a s);elim Hletin + |elim H;lapply (decidable_eq_nat a t);elim Hletin [apply ex_intro [apply (S a) |intros;unfold;intro;inversion H4 @@ -668,23 +668,23 @@ cut (\forall l:(list nat).\exists n.\forall m. rewrite < H7 in H5; apply (H1 m ? H5);lapply (le_S ? ? H3); apply (le_S_S_to_le ? ? Hletin2)]] - |cut ((leb a s) = true \lor (leb a s) = false) + |cut ((leb a t) = true \lor (leb a t) = false) [elim Hcut [apply ex_intro - [apply (S s) + [apply (S t) |intros;unfold;intro;inversion H5 [intros;lapply (inj_head_nat ? ? ? ? H7);rewrite > H6 in H4; rewrite < Hletin1 in H4;apply (not_le_Sn_n ? H4) |intros;lapply (inj_tail ? ? ? ? ? H9); rewrite < Hletin1 in H6;lapply (H1 a1) [apply (Hletin2 H6) - |lapply (leb_to_Prop a s);rewrite > H3 in Hletin2; + |lapply (leb_to_Prop a t);rewrite > H3 in Hletin2; simplify in Hletin2;rewrite < H8; apply (trans_le ? ? ? Hletin2); apply (trans_le ? ? ? ? H4);constructor 2;constructor 1]]] |apply ex_intro [apply a - |intros;lapply (leb_to_Prop a s);rewrite > H3 in Hletin1; + |intros;lapply (leb_to_Prop a t);rewrite > H3 in Hletin1; simplify in Hletin1;lapply (not_le_to_lt ? ? Hletin1); unfold in Hletin2;unfold;intro;inversion H5 [intros;lapply (inj_head_nat ? ? ? ? H7); @@ -693,7 +693,7 @@ cut (\forall l:(list nat).\exists n.\forall m. |intros;lapply (inj_tail ? ? ? ? ? H9); rewrite < Hletin3 in H6;rewrite < H8 in H6; apply (H1 ? H4 H6)]]] - |elim (leb a s);auto]]]] + |elim (leb a t);autobatch]]]] qed. (*** lemmas on well-formedness ***) @@ -794,17 +794,17 @@ qed. lemma WFE_swap : \forall u,v,G.(WFEnv G) \to (WFEnv (swap_Env u v G)). intros 3.elim G 0 [intro;simplify;assumption - |intros 2;elim s;simplify;constructor 2 + |intros 2;elim t;simplify;constructor 2 [apply H;apply (WFE_consG_WFE_G ? ? H1) |unfold;intro;lapply (in_dom_swap u v n l);elim Hletin;lapply (H4 H2); (* FIXME trick *)generalize in match H1;intro;inversion H1 - [intros;absurd ((mk_bound b n t)::l = []) + [intros;absurd ((mk_bound b n t1)::l = []) [assumption|apply nil_cons] |intros;lapply (inj_head ? ? ? ? H10);lapply (inj_tail ? ? ? ? ? H10); destruct Hletin2;rewrite < Hcut1 in H8;rewrite < Hletin3 in H8; apply (H8 Hletin1)] - |apply (WFT_swap u v l t);inversion H1 - [intro;absurd ((mk_bound b n t)::l = []) + |apply (WFT_swap u v l t1);inversion H1 + [intro;absurd ((mk_bound b n t1)::l = []) [assumption|apply nil_cons] |intros;lapply (inj_head ? ? ? ? H6);lapply (inj_tail ? ? ? ? ? H6); destruct Hletin;rewrite > Hletin1;rewrite > Hcut2;assumption]]] @@ -858,7 +858,7 @@ cut ((max (t_len T1) (t_len T2)) = match (leb (t_len T1) (t_len T2)) with [rewrite > H;rewrite > H in Hletin;simplify;constructor 1 |rewrite > H;rewrite > H in Hletin;simplify;simplify in Hletin; unfold;apply le_S_S;assumption] - |elim (leb (t_len T1) (t_len T2));auto] + |elim (leb (t_len T1) (t_len T2));autobatch] |elim T1;simplify;reflexivity] qed. @@ -875,7 +875,7 @@ cut ((max (t_len T1) (t_len T2)) = match (leb (t_len T1) (t_len T2)) with lapply (not_le_to_lt ? ? Hletin);unfold in Hletin1;unfold; constructor 2;assumption |rewrite > H;simplify;unfold;constructor 1] - |elim (leb (t_len T1) (t_len T2));auto] + |elim (leb (t_len T1) (t_len T2));autobatch] |elim T1;simplify;reflexivity] qed. @@ -891,7 +891,7 @@ cut ((max (t_len T1) (t_len T2)) = match (leb (t_len T1) (t_len T2)) with [rewrite > H;rewrite > H in Hletin;simplify;constructor 1 |rewrite > H;rewrite > H in Hletin;simplify;simplify in Hletin; unfold;apply le_S_S;assumption] - |elim (leb (t_len T1) (t_len T2));auto] + |elim (leb (t_len T1) (t_len T2));autobatch] |elim T1;simplify;reflexivity] qed. @@ -908,7 +908,7 @@ cut ((max (t_len T1) (t_len T2)) = match (leb (t_len T1) (t_len T2)) with lapply (not_le_to_lt ? ? Hletin);unfold in Hletin1;unfold; constructor 2;assumption |rewrite > H;simplify;unfold;constructor 1] - |elim (leb (t_len T1) (t_len T2));auto] + |elim (leb (t_len T1) (t_len T2));autobatch] |elim T1;simplify;reflexivity] qed. @@ -929,11 +929,11 @@ lemma swap_env_not_free : \forall u,v,G.(WFEnv G) \to (swap_Env u v G) = G. intros 3.elim G 0 [simplify;intros;reflexivity - |intros 2;elim s 0;simplify;intros;lapply (notin_cons ? ? ? ? H2); + |intros 2;elim t 0;simplify;intros;lapply (notin_cons ? ? ? ? H2); lapply (notin_cons ? ? ? ? H3);elim Hletin;elim Hletin1; lapply (swap_other ? ? ? H4 H6);lapply (WFE_consG_to_WFT ? ? ? ? H1); - cut (\lnot (in_list ? u (fv_type t))) - [cut (\lnot (in_list ? v (fv_type t))) + cut (\lnot (in_list ? u (fv_type t1))) + [cut (\lnot (in_list ? v (fv_type t1))) [lapply (swap_Typ_not_free ? ? ? Hcut Hcut1); lapply (WFE_consG_WFE_G ? ? H1); lapply (H Hletin5 H5 H7); @@ -1123,9 +1123,9 @@ intros 7;elim H 0 |intros;lapply (inj_tail ? ? ? ? ? H8);lapply (inj_head ? ? ? ? H8); destruct Hletin1;rewrite < Hletin in H6;rewrite < Hletin in H4; rewrite < Hcut1 in H6;apply (WFE_cons ? ? ? ? H4 H6 H2)] - |intros;simplify;generalize in match H2;elim s;simplify in H4; + |intros;simplify;generalize in match H2;elim t;simplify in H4; inversion H4 - [intros;absurd (mk_bound b n t::l@(mk_bound B x T::G)=Empty) + [intros;absurd (mk_bound b n t1::l@(mk_bound B x T::G)=Empty) [assumption |apply nil_cons] |intros;lapply (inj_tail ? ? ? ? ? H9);lapply (inj_head ? ? ? ? H9);