X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FPOPLmark%2FFsub%2Fadeq.ma;h=2a0f730abdc5b307c4675601ab1ad3e9f93452cf;hb=56c4e355b88aa505b64c539053aba92eb86afc2a;hp=d4fdeca8193a1ffef50cb709d56821ed0cbd0c35;hpb=9883f04161a9972f0641dd85faf224b4f2846f05;p=helm.git 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]]