From: Wilmer Ricciotti Date: Thu, 9 Jul 2009 11:38:42 +0000 (+0000) Subject: More updates to Fsub. X-Git-Tag: make_still_working~3715 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=56c4e355b88aa505b64c539053aba92eb86afc2a More updates to Fsub. --- diff --git a/helm/software/matita/contribs/POPLmark/Fsub/adeq.ma b/helm/software/matita/contribs/POPLmark/Fsub/adeq.ma index d4fdeca81..2a0f730ab 100644 --- a/helm/software/matita/contribs/POPLmark/Fsub/adeq.ma +++ b/helm/software/matita/contribs/POPLmark/Fsub/adeq.ma @@ -95,8 +95,7 @@ inductive NWFType : (list nbound) → NTyp → Prop ≝ | NWFT_Arrow : ∀G,T,U.(NWFType G T) → (NWFType G U) → (NWFType G (NArrow T U)) | NWFT_Forall : ∀G,X,T,U.(NWFType G T) → - (∀Y.Y ∉ (fv_Nenv G) → - (Y = X ∨ Y ∉ (fv_NTyp U)) → + (∀Y.Y ∉ (fv_Nenv G) → (Y ∈ (fv_NTyp U) → Y = X) → (NWFType ((mk_nbound true Y T) :: G) (swap_NTyp Y X U))) → (NWFType G (NForall X T U)). @@ -118,12 +117,10 @@ inductive NJSubtype : (list nbound) → NTyp → NTyp → Prop ≝ (NJSubtype G T1 S1) → (NJSubtype G S2 T2) → (NJSubtype G (NArrow S1 S2) (NArrow T1 T2)) | NSA_All : ∀G,X,Y,S1,S2,T1,T2. - (NWFType G (NForall X S1 S2)) → - (NWFType G (NForall Y T1 T2)) → (NJSubtype G T1 S1) → (∀Z.Z ∉ (fv_Nenv G) → - (Z = X ∨ Z ∉ (fv_NTyp S2)) → - (Z = Y ∨ Z ∉ (fv_NTyp T2)) → + (Z ∈ (fv_NTyp S2) → Z = X) → + (Z ∈ (fv_NTyp T2) → Z = Y) → (NJSubtype ((mk_nbound true Z T1) :: G) (swap_NTyp Z X S2) (swap_NTyp Z Y T2))) → (NJSubtype G (NForall X S1 S2) (NForall Y T1 T2)). @@ -138,8 +135,21 @@ let rec nt_len T ≝ definition encodeenv : list nbound → list bound ≝ map nbound bound (λb.match b with - [ mk_nbound b x T ⇒ mk_bound b x (encodetype T []) ]). + [ mk_nbound b x T ⇒ mk_bound b x (encodetype T []) ]). +notation < "⌈ T ⌉ \sub l" with precedence 25 for @{'encode2 $T $l}. +interpretation "Fsub names to LN type encoding" 'encode2 T l = (encodetype T l). +notation < "⌈ G ⌉" with precedence 25 for @{'encode $G}. +interpretation "Fsub names to LN env encoding" 'encode G = (encodeenv G). +notation < "| T |" with precedence 25 for @{'abs $T}. +interpretation "Fsub named type length" 'abs T = (nt_len T). +interpretation "list length" 'abs l = (length ? l). +notation < "〈a,b〉 · T" with precedence 60 for @{'swap $a $b $T}. +interpretation "natural swap" 'swap a b n = (swap a b n). +interpretation "Fsub name swap in a named type" 'swap a b T = (swap_NTyp a b T). +interpretation "Fsub name swap in a LN type" 'swap a b T = (swap_Typ a b T). +interpretation "natural list swap" 'swap a b l = (swap_list a b l). + lemma eq_fv_Nenv_fv_env : ∀G. fv_Nenv G = fv_env (encodeenv G). intro;elim G;simplify [reflexivity @@ -844,7 +854,7 @@ intros;elim H;simplify;unfold;intros; [intro;apply H7;rewrite > H8;apply in_list_head |elim (remove_inlist ? ? ? H6);assumption]] |intro;autobatch depth=4 - |right;intro;autobatch depth=5]]] + |intro;elim H7;autobatch]]] qed. lemma fv_NTyp_fv_Typ : ∀T,X,l.X ∈ (fv_NTyp T) → X ∉ l → @@ -879,11 +889,8 @@ intros;elim H;simplify [simplify in H4;apply H4 [rewrite > (eq_fv_Nenv_fv_env l);assumption |elim (decidable_eq_nat X n) - [left;assumption - |right;intro;apply H6;apply (fv_NTyp_fv_Typ ? ? ? H8);intro; - apply H7;inversion H9;intros;destruct; - [reflexivity - |elim (not_in_list_nil ? ? H10)]]] + [assumption + |elim H6;apply (fv_NTyp_fv_Typ ??? H8);autobatch]] |4:intro;elim (decidable_eq_nat X n) [assumption |elim H6;cut (¬(in_list ? X [n])) @@ -938,6 +945,18 @@ intro;elim T;simplify;unfold; |autobatch]]] qed. +lemma decidable_inlist_nat : ∀l:list nat.∀n.decidable (n ∈ l). +intros;elim l +[right;autobatch +|elim H + [left;autobatch + |elim (decidable_eq_nat n a) + [left;autobatch + |right;intro;apply H2;inversion H3;intros;destruct; + [reflexivity + |elim (H1 H4)]]]] +qed. + lemma adeq_WFT2 : ∀G1,T1.WFType G1 T1 → ∀G2,T2.G1 = encodeenv G2 → T1 = encodetype T2 [] → NWFType G2 T2. @@ -971,21 +990,19 @@ intros 3;elim H elim Hcut;elim H7;elim H8;clear Hcut H7 H8;rewrite > H9; rewrite > H9 in H6;simplify in H6;destruct;apply NWFT_Forall [autobatch - |intros;elim H6 - [rewrite > H7;cut (swap_NTyp a a a2 = a2) - [|elim a2;simplify;autobatch] - rewrite > Hcut;apply (H4 Y) - [4:rewrite > H7;(*** autobatch *) - change in ⊢ (? ? (? (? ? %) ? ?) ?) with ([]@[a]); - symmetry;rewrite < Hcut in ⊢ (??%?); - change in ⊢ (? ? ? (? ? ? %)) with (length nat []);autobatch - |*:autobatch] - |apply (H4 Y) - [1,3:autobatch - |intro;autobatch - |symmetry;apply (encode_subst a2 Y a []); - [3:intro;elim (H7 H8) - |*:autobatch]]]] + |intros;elim (decidable_inlist_nat (fv_NTyp a2) Y) + [lapply (H6 H7) as H8;rewrite > H8;rewrite > (? : swap_NTyp a a a2 = a2) + [apply (H4 Y) + [4:rewrite > H8;change in ⊢ (?? (? (??%) ??) ?) with ([]@[a]); + symmetry;change in ⊢ (??? (???%)) with (length nat []);autobatch + |*:autobatch] + |elim a2;simplify;autobatch] + |apply (H4 Y) + [1,3:autobatch + |intro;autobatch + |symmetry;apply (encode_subst a2 Y a []) + [3:intro;elim (H7 H8) + |*:autobatch]]]] qed. lemma adeq_WFE : ∀G.NWFEnv G → WFEnv (encodeenv G). @@ -1006,53 +1023,193 @@ intros 3;elim H |*:autobatch] qed. -lemma NJSubtype_to_NWFT : ∀G,T,U.NJSubtype G T U → NWFType G T ∧ NWFType G U. -intros;elim H - [1,2:split;autobatch - |elim H3;split; - [apply NWFT_TName;elim l in H1 - [elim (not_in_list_nil ? ? H1) - |inversion H6;intros;destruct; - [simplify;autobatch - |elim a;simplify;elim b;simplify;try apply in_list_cons; - apply H1;apply H7]] - |assumption] - |elim H2;elim H4;split;autobatch - |split;assumption] +lemma NJS_fv_to_fvNenv : ∀G,T,U.NJSubtype G T U → + fv_NTyp T ⊆ fv_Nenv G ∧ fv_NTyp U ⊆ fv_Nenv G. +intros;elim H;simplify; +[split + [autobatch + |unfold;intros;elim (not_in_list_nil ?? H3)] +|split;unfold;intros;rewrite > (in_list_singleton_to_eq ??? H3);assumption +|decompose;split;try autobatch;unfold;intros; + rewrite > (in_list_singleton_to_eq ??? H3); + generalize in match (refl_eq ? (mk_nbound true n n2)); + elim H1 in ⊢ (???% → %) + [rewrite < H6;simplify;apply in_list_head + |cases a1;cases b;simplify; + [apply in_list_cons;apply H7;assumption + |apply H7;assumption]] +|decompose;split;unfold;intros; + [elim (in_list_append_to_or_in_list ???? H4);autobatch + |elim (in_list_append_to_or_in_list ???? H4);autobatch] +|decompose;split;unfold;intros; + [elim (in_list_append_to_or_in_list ? ? ? ? H2) + [autobatch + |elim (fresh_name (x::fv_Nenv l@var_NTyp n3@var_NTyp n5));lapply (H4 a) + [cut (a ≠ x ∧ x ≠ n) + [elim Hcut;elim Hletin;lapply (H11 x) + [simplify in Hletin1;inversion Hletin1;intros;destruct; + [elim Hcut;elim H13;reflexivity + |assumption] + |elim n3 in H7 H8 + [simplify in H7;elim (decidable_eq_nat n n6) + [rewrite > (eq_to_eqb_true ? ? H13) in H7;simplify in H7; + elim (not_in_list_nil ? ? H7) + |rewrite > (not_eq_to_eqb_false ? ? H13) in H7; + simplify in H7;inversion H7;intros + [destruct;simplify;rewrite > swap_other + [apply in_list_head + |intro;apply H8;rewrite > H14;autobatch + |intro;apply H13;rewrite > H14;reflexivity] + |destruct;elim (not_in_list_nil ? ? H14)]] + |simplify in H7;elim (not_in_list_nil ? ? H7) + |simplify in H14;simplify;elim (remove_inlist ? ? ? H13); + simplify in H15;elim (in_list_append_to_or_in_list ? ? ? ? H15) + [apply in_list_to_in_list_append_l;apply H7 + [apply (in_remove ? ? ? H16 H17) + |intro;apply H14;simplify; + rewrite < (associative_append ? [x] (fv_Nenv l) ((var_NTyp n6 @ var_NTyp n7)@var_NTyp n5)); + elim (in_list_append_to_or_in_list ? ? (x::fv_Nenv l) (var_NTyp n6@var_NTyp n5) H18); + [apply in_list_to_in_list_append_l;apply H19 + |apply in_list_to_in_list_append_r; + elim (in_list_append_to_or_in_list ???? H19);autobatch]] + |apply in_list_to_in_list_append_r;apply H8 + [apply (in_remove ? ? ? H16 H17) + |intro;apply H14;simplify; + rewrite < (associative_append ? [x] (fv_Nenv l) ((var_NTyp n6 @ var_NTyp n7)@var_NTyp n5)); + elim (in_list_append_to_or_in_list ? ? (x::fv_Nenv l) (var_NTyp n7@var_NTyp n5) H18); + [apply in_list_to_in_list_append_l;apply H19 + |apply in_list_to_in_list_append_r; + elim (in_list_append_to_or_in_list ???? H19);autobatch]]] + |simplify in H14;simplify;elim (remove_inlist ? ? ? H13); + simplify in H15;elim (in_list_append_to_or_in_list ? ? ? ? H15) + [apply in_list_to_in_list_append_l;apply H7 + [apply (in_remove ? ? ? H16 H17) + |intro;apply H14;simplify; + rewrite < (associative_append ? [x] (fv_Nenv l) (n6::(var_NTyp n7 @ var_NTyp n8)@var_NTyp n5)); + elim (in_list_append_to_or_in_list ? ? (x::fv_Nenv l) (var_NTyp n7@var_NTyp n5) H18); + [apply in_list_to_in_list_append_l;apply H19 + |apply in_list_to_in_list_append_r;apply in_list_cons; + elim (in_list_append_to_or_in_list ???? H19);autobatch]] + |apply in_list_to_in_list_append_r;apply in_remove; + [elim (remove_inlist ??? H13);intro;apply H19; + elim (swap_case a n n6) + [elim H21 + [elim H14;rewrite < H22;rewrite < H20;apply in_list_head + |autobatch paramodulation] + |elim (remove_inlist ??? H17);elim H23;autobatch paramodulation] + |apply H8 + [apply (in_remove ? ? ? H16);elim (remove_inlist ??? H17);assumption + |intro;apply H14;simplify; + rewrite < (associative_append ? [x] (fv_Nenv l) (n6::(var_NTyp n7 @ var_NTyp n8)@var_NTyp n5)); + elim (in_list_append_to_or_in_list ? ? (x::fv_Nenv l) (var_NTyp n8@var_NTyp n5) H18); + [apply in_list_to_in_list_append_l;apply H19 + |apply in_list_to_in_list_append_r;apply in_list_cons; + elim (in_list_append_to_or_in_list ???? H19);autobatch]]]]]] + |split + [intro;apply H8;rewrite > H9;apply in_list_head + |elim (remove_inlist ? ? ? H7);assumption]] + |intro;autobatch depth=4 + |3,4:intro;elim H8;apply in_list_cons;autobatch depth=4]] + |elim (in_list_append_to_or_in_list ? ? ? ? H2) + [autobatch + |elim (fresh_name (x::fv_Nenv l@var_NTyp n3@var_NTyp n5));lapply (H4 a) + [cut (a ≠ x ∧ x ≠ n1) + [elim Hcut;elim Hletin;lapply (H12 x) + [simplify in Hletin1;inversion Hletin1;intros;destruct; + [elim Hcut;elim H13;reflexivity + |assumption] + |elim n5 in H7 H8 + [simplify in H7;elim (decidable_eq_nat n1 n6) + [rewrite > (eq_to_eqb_true ? ? H13) in H7;simplify in H7; + elim (not_in_list_nil ? ? H7) + |rewrite > (not_eq_to_eqb_false ? ? H13) in H7; + simplify in H7;inversion H7;intros + [destruct;simplify;rewrite > swap_other + [apply in_list_head + |intro;apply H8;rewrite > H14;autobatch + |intro;apply H13;rewrite > H14;reflexivity] + |destruct;elim (not_in_list_nil ? ? H14)]] + |simplify in H7;elim (not_in_list_nil ? ? H7) + |simplify in H14;simplify;elim (remove_inlist ? ? ? H13); + simplify in H15;elim (in_list_append_to_or_in_list ? ? ? ? H15) + [apply in_list_to_in_list_append_l;apply H7 + [apply (in_remove ? ? ? H16 H17) + |intro;apply H14;simplify; + rewrite < (associative_append ? [x] (fv_Nenv l) (var_NTyp n3 @ var_NTyp n6@var_NTyp n7)); + elim (in_list_append_to_or_in_list ? ? (x::fv_Nenv l) (var_NTyp n3@var_NTyp n6) H18); + [apply in_list_to_in_list_append_l;apply H19 + |apply in_list_to_in_list_append_r; + elim (in_list_append_to_or_in_list ???? H19);autobatch]] + |apply in_list_to_in_list_append_r;apply H8 + [apply (in_remove ? ? ? H16 H17) + |intro;apply H14;simplify; + rewrite < (associative_append ? [x] (fv_Nenv l) (var_NTyp n3 @ var_NTyp n6@var_NTyp n7)); + elim (in_list_append_to_or_in_list ? ? (x::fv_Nenv l) (var_NTyp n3@var_NTyp n7) H18); + [apply in_list_to_in_list_append_l;apply H19 + |apply in_list_to_in_list_append_r; + elim (in_list_append_to_or_in_list ???? H19);autobatch]]] + |simplify in H14;simplify;elim (remove_inlist ? ? ? H13); + simplify in H15;elim (in_list_append_to_or_in_list ? ? ? ? H15) + [apply in_list_to_in_list_append_l;apply H7 + [apply (in_remove ? ? ? H16 H17) + |intro;apply H14;simplify; + rewrite < (associative_append ? [x] (fv_Nenv l) (var_NTyp n3@n6::var_NTyp n7 @ var_NTyp n8)); + elim (in_list_append_to_or_in_list ? ? (x::fv_Nenv l) (var_NTyp n3@var_NTyp n7) H18); + [apply in_list_to_in_list_append_l;apply H19 + |apply in_list_to_in_list_append_r; + elim (in_list_append_to_or_in_list ???? H19);autobatch depth=4]] + |apply in_list_to_in_list_append_r;apply in_remove; + [elim (remove_inlist ??? H13);intro;apply H19; + elim (swap_case a n1 n6) + [elim H21 + [elim H14;rewrite < H22;rewrite < H20;apply in_list_head + |autobatch paramodulation] + |elim (remove_inlist ??? H17);elim H23;autobatch paramodulation] + |apply H8 + [apply (in_remove ? ? ? H16);elim (remove_inlist ??? H17);assumption + |intro;apply H14;simplify; + rewrite < (associative_append ? [x] (fv_Nenv l) (var_NTyp n3@n6::var_NTyp n7 @ var_NTyp n8)); + elim (in_list_append_to_or_in_list ? ? (x::fv_Nenv l) (var_NTyp n3@var_NTyp n8) H18); + [apply in_list_to_in_list_append_l;apply H19 + |apply in_list_to_in_list_append_r; + elim (in_list_append_to_or_in_list ???? H19);autobatch depth=4]]]]]] + |split + [intro;apply H8;rewrite > H9;apply in_list_head + |elim (remove_inlist ? ? ? H7);assumption]] + |intro;autobatch depth=4 + |3,4:intro;elim H8;apply in_list_cons;autobatch depth=4]]]] qed. - + theorem adequacy : ∀G,T,U.NJSubtype G T U → JSubtype (encodeenv G) (encodetype T []) (encodetype U []). intros;elim H;simplify [1,2,3,4:autobatch |apply SA_All [assumption - |intros;lapply (NSA_All ? ? ? ? ? ? ? H1 H2 H3 H5); + |intros;lapply (NSA_All ? ? ? ? ? ? ? H1 H3); rewrite < (encode_subst n3 X n []) [rewrite < (encode_subst n5 X n1 []) - [rewrite < eq_fv_Nenv_fv_env in H7; - elim (NJSubtype_to_NWFT ? ? ? Hletin); - lapply (in_fvNTyp_in_fvNenv ? ? H8); - lapply (in_fvNTyp_in_fvNenv ? ? H9); - simplify in Hletin1;simplify in Hletin2; - apply (H6 ? H7) + [rewrite < eq_fv_Nenv_fv_env in H5; + elim (NJS_fv_to_fvNenv ? ? ? Hletin); + simplify in H6;simplify in H7; + apply (H4 ? H5) [elim (decidable_eq_nat X n) - [left;assumption - |right;intro;autobatch depth=5] + [assumption + |elim H5;autobatch depth=5] |elim (decidable_eq_nat X n1) - [left;assumption - |right;intro;autobatch depth=5]] + [assumption + |elim H5;autobatch depth=5]] |2,3:autobatch - |intro;elim (NJSubtype_to_NWFT ? ? ? Hletin); - lapply (in_fvNTyp_in_fvNenv ? ? H10);simplify in Hletin1; + |intro;elim (NJS_fv_to_fvNenv ? ? ? Hletin); + simplify in H8; elim (decidable_eq_nat X n1) [assumption - |elim H7;autobatch depth=4]] + |elim H5;autobatch depth=4]] |2,3:autobatch - |intro;elim (NJSubtype_to_NWFT ? ? ? Hletin);lapply (in_fvNTyp_in_fvNenv ? ? H9); - simplify in Hletin1;elim (decidable_eq_nat X n) + |intro;elim (NJS_fv_to_fvNenv ? ? ? Hletin); + simplify in H7;elim (decidable_eq_nat X n) [assumption - |elim H7;autobatch depth=4]]]] + |elim H5;autobatch depth=4]]]] qed. let rec closed_type T n ≝ @@ -1243,7 +1400,7 @@ intros 4;elim H 0 destruct;lapply (SA_All ? ? ? ? ? H1 H3); lapply (JS_to_WFT1 ? ? ? Hletin);lapply (JS_to_WFT2 ? ? ? Hletin); apply NSA_All - [1,2,3:autobatch; + [autobatch; |intros;apply H4; [apply Z |2,3:autobatch @@ -1260,9 +1417,7 @@ intros 4;elim H 0 |intro;autobatch]]]] |rewrite < (encode_subst a5 Z a3 []) [1,2,3:autobatch - |intro;elim H7 - [assumption - |elim (H9 H8)]]]] + |intro;elim H7;autobatch]]] |generalize in match H6;elim T2 0;simplify;intros;destruct; generalize in match H7;elim U2 0;simplify;intros;destruct; autobatch depth=8 width=2 size=9]] diff --git a/helm/software/matita/contribs/POPLmark/Fsub/defndb.ma b/helm/software/matita/contribs/POPLmark/Fsub/defndb.ma index 4a61bcb2f..745090de4 100644 --- a/helm/software/matita/contribs/POPLmark/Fsub/defndb.ma +++ b/helm/software/matita/contribs/POPLmark/Fsub/defndb.ma @@ -18,8 +18,8 @@ include "nat/lt_arith.ma". (*** representation of Fsub types ***) inductive Typ : Set ≝ - | TVar : nat → Typ (* type var *) - | Top : Typ (* maximum type *) + | TVar : nat → Typ (* type var *) + | Top : Typ (* maximum type *) | Arrow : Typ → Typ → Typ (* functions *) | Forall : Typ → Typ → Typ. (* universal type *) @@ -224,7 +224,11 @@ definition lifter : nat → nat → nat → nat ≝ lemma extensional_perm : ∀T.∀f,g.(∀x.f x = g x) → perm T f = perm T g. intro;elim T [4:whd in ⊢ (??%%);cut (∀x.flift f 1 x = flift g 1 x) - [autobatch + [rewrite > (H f g); + [rewrite > (H1 (flift f 1) (flift g 1)); + [reflexivity + |assumption] + |assumption] |intro;simplify;cases x [reflexivity |simplify;rewrite > H2;reflexivity]] diff --git a/helm/software/matita/contribs/POPLmark/Fsub/part1a.ma b/helm/software/matita/contribs/POPLmark/Fsub/part1a.ma index 9e097b279..74ba49240 100644 --- a/helm/software/matita/contribs/POPLmark/Fsub/part1a.ma +++ b/helm/software/matita/contribs/POPLmark/Fsub/part1a.ma @@ -16,9 +16,8 @@ include "Fsub/defn.ma". (*** Lemma A.1 (Reflexivity) ***) theorem JS_Refl : ∀T,G.(G ⊢ T) → G ⊢ ♦ → G ⊢ T ⊴ T. -intros 3; elim H; - [1,2,3: autobatch - | apply SA_All; [ autobatch | intros;autobatch depth=4 size=10]] +intros 3; elim H;try autobatch; +apply SA_All; [ autobatch | intros;autobatch depth=4 size=10] qed. (* @@ -28,10 +27,9 @@ qed. *) lemma JS_weakening : ∀G,T,U.G ⊢ T ⊴ U → ∀H.H ⊢ ♦ → G ⊆ H → H ⊢ T ⊴ U. -intros 4; elim H; - [1,2,3,4: autobatch depth=4 size=7 - | apply (SA_All ? ? ? ? ? (H2 ? H6 H7)); - intros; apply H4;autobatch depth=4 size=7] +intros 4; elim H;try autobatch depth=4 size=7; +apply (SA_All ? ? ? ? ? (H2 ? H6 H7)); +intros; autobatch depth=6 width=4 size=13; qed. inverter JS_indinv for JSubtype (%?%). @@ -58,7 +56,7 @@ lemma JS_trans_prova: ∀T,G1.(G1 ⊢ T) → intros 3;elim H;clear H; [elim H3 using JS_indinv;destruct;autobatch |inversion H3; intros; destruct; assumption - |*: elim H6 using JS_indinv;destruct; + |*:elim H6 using JS_indinv;destruct; [1,3: autobatch |*: inversion H7; intros; destruct; [1,2: autobatch depth=4 width=4 size=9 @@ -84,4 +82,4 @@ theorem JS_narrow : ∀G1,G2,X,P,Q,T,U. G2 @ !X ⊴ P :: G1 ⊢ T ⊴ U. intros;apply (narrowing ? ? ? ? ? ? ? H1 ? H) [|autobatch] intros;apply (JS_trans ? ? ? ? ? H2);apply (JS_weakening ? ? ? H1);autobatch. -qed. +qed. \ No newline at end of file diff --git a/helm/software/matita/contribs/POPLmark/Fsub/part1adb.ma b/helm/software/matita/contribs/POPLmark/Fsub/part1adb.ma index 3b0b677b7..019d55cc5 100644 --- a/helm/software/matita/contribs/POPLmark/Fsub/part1adb.ma +++ b/helm/software/matita/contribs/POPLmark/Fsub/part1adb.ma @@ -49,25 +49,23 @@ intros 4; elim H; elim b in H10;simplify in H10;destruct;exists [apply t2] reflexivity] |*:assumption] - |simplify;apply SA_Arrow;autobatch width=4 + |simplify;autobatch width=5 size=11 |simplify;apply (SA_All ? ? ? ? ? (H2 ? H6 ?? H8 H9)) [assumption |apply H4 - [apply WFE_cons - [assumption - |lapply (H2 ? H6 ? H7);autobatch] - |change in ⊢ (???%) with (flift f 1);apply injective_flift;assumption + [autobatch depth=4 width=4 size=8 + |change in ⊢ (???%) with (flift f 1);autobatch; |intro;cases n;simplify;intros;autobatch depth=4 - |change in ⊢ (???%) with (flift f 1);apply incl_cons;assumption]]] + |change in ⊢ (???%) with (flift f 1);autobatch]]] qed. inverter JS_indinv for JSubtype (%?%). theorem narrowing:∀G,G1,U,P,M,N. - G1 ⊢ P ⊴ U → + G1 ⊢ P ⊴ U → (∀G2,S,T. G2@G1 ⊢ S ⊴ lift U (length ? G2) O → - G2@G1 ⊢ lift U (length ? G2) O ⊴ T \to + G2@G1 ⊢ lift U (length ? G2) O ⊴ T → G2@G1 ⊢ S ⊴ T) → G ⊢ M ⊴ N → ∀l.G=l@(mk_bound true U::G1) → l@(mk_bound true P::G1) ⊢ M ⊴ N. @@ -123,46 +121,32 @@ elim (decidable_eq_nat n (length ? l1)) |apply H6;reflexivity]] qed. -lemma JS_trans_prova: ∀T,G1.WFType G1 T → -∀G,R,U,f.injective ?? f → length ? G1 ≤ length ? G → G ⊢ R ⊴ perm T f → G ⊢ perm T f ⊴ U → G ⊢ R ⊴ U. -intros 3;elim H;clear H; try autobatch; - [simplify in H5;simplify in H6;elim H5 using JS_indinv;destruct;autobatch - |simplify in H4;inversion H4; intros; destruct; assumption - |simplify in H7;elim H7 using JS_indinv;intros;destruct; +lemma JS_trans_prova: ∀T,G,R,U,f.G ⊢ R ⊴ perm T f → G ⊢ perm T f ⊴ U → G ⊢ R ⊴ U. +intro;elim T; + [simplify in H;simplify in H1;elim H using JS_indinv;destruct;autobatch + |simplify in H1;inversion H1; intros; destruct; assumption + |simplify in H2;elim H2 using JS_indinv;intros;destruct; [autobatch - |simplify in H8;inversion H8;intros;destruct; - [apply SA_Top;autobatch; - |apply SA_Arrow - [apply (H2 ?????? H12 H);assumption - |apply (H4 ?????? H10 H14);assumption]]] - |simplify in H7;elim H7 using JS_indinv;intros;destruct; + |simplify in H3;inversion H3;intros;destruct;autobatch depth=4 size=7] + |simplify in H2;elim H2 using JS_indinv;intros;destruct; [autobatch - |simplify in H8;inversion H8;intros;destruct; + |simplify in H3;inversion H3;intros;destruct; [apply SA_Top;autobatch |apply SA_All - [apply (H2 ?????? H12 H);assumption - |apply H4 - [3:simplify;apply le_S_S;assumption - |4:apply (narrowing (mk_bound true (perm t f)::G) G ???? H12 ? H10 []) - [intros;rewrite > lift_perm2 in H16;rewrite > lift_perm2 in H17; - rewrite > perm_compose in H16; rewrite > perm_compose in H17; - apply H2 - [3:apply (trans_le ??? H6);rewrite > length_append;autobatch - |4:apply H16 - |5:apply H17 - |2:apply injective_compose;autobatch] + [apply (H ???? H8 H4);assumption + |apply H1 + [2:apply (narrowing (mk_bound true (perm t f)::G) G ???? H8 ? H6 []) + [intros;rewrite > lift_perm2 in H12;rewrite > lift_perm2 in H13; + rewrite > perm_compose in H12; rewrite > perm_compose in H13; + apply H + [2,3:autobatch] |reflexivity] - |5:assumption - |2:change in ⊢ (???%) with (flift f 1);autobatch]]]]] + |3:assumption]]]]] qed. theorem JS_trans : ∀G,T,U,V.G ⊢ T ⊴ U → G ⊢ U ⊴ V → G ⊢ T ⊴ V. intros 4;rewrite > (perm_id ? 0) in ⊢ (???% → ??%? → ?); -intros;apply (JS_trans_prova ????????? H H1) -[apply G -|rewrite < perm_id in H;autobatch -|simplify;intros;assumption -|apply le_n] +intros;autobatch; qed. theorem JS_narrow : ∀G1,G2,P,Q,T,U. @@ -170,4 +154,4 @@ theorem JS_narrow : ∀G1,G2,P,Q,T,U. (G2 @ (mk_bound true P :: G1)) ⊢ T ⊴ U. intros; apply (narrowing ? ? ? ? ? ? H1 ? H) [|autobatch] intros;autobatch; -qed. +qed. \ No newline at end of file