From 23de7622988fbd10a11b1dbe3536572af7acf16e Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Fri, 2 May 2008 13:40:56 +0000 Subject: [PATCH] Some destruct tactics got broken after last update. Small axiomatization still included. --- .../matita/contribs/POPLmark/Fsub/adeq.ma | 556 ++++++++++++++---- 1 file changed, 444 insertions(+), 112 deletions(-) diff --git a/helm/software/matita/contribs/POPLmark/Fsub/adeq.ma b/helm/software/matita/contribs/POPLmark/Fsub/adeq.ma index a85b01ddb..a8a5a2340 100644 --- a/helm/software/matita/contribs/POPLmark/Fsub/adeq.ma +++ b/helm/software/matita/contribs/POPLmark/Fsub/adeq.ma @@ -19,7 +19,7 @@ include "datatypes/bool.ma". include "list/list.ma". include "nat/compare.ma". include "Fsub/util.ma". -include "Fsub/defn.ma". +include "Fsub/defn2.ma". inductive NTyp : Set \def | TName : nat \to NTyp @@ -204,10 +204,10 @@ let rec head (A:Type) l on l \def [ nil \Rightarrow None A | (cons (x:A) l2) \Rightarrow Some A x]. -let rec tail (A:Type) l \def +(*let rec tail (A:Type) l \def match l with [ nil \Rightarrow nil A - | (cons (x:A) l2) \Rightarrow l2]. + | (cons (x:A) l2) \Rightarrow l2].*) let rec nth n l on n \def match n with @@ -297,12 +297,16 @@ inductive NJSubtype : (list nbound) → NTyp → NTyp → Prop ≝ | NSA_Arrow : ∀G,S1,S2,T1,T2. (NJSubtype G T1 S1) → (NJSubtype G S2 T2) → (NJSubtype G (NArrow S1 S2) (NArrow T1 T2)) - | NSA_All : ∀G,X,S1,S2,T1,T2. + | NSA_All : ∀G,X,Y,S1,S2,T1,T2. + (NWFType G (NForall X S1 S2)) \to + (NWFType G (NForall Y T1 T2)) \to (NJSubtype G T1 S1) → - (∀Y.¬(Y ∈ fv_Nenv G) → - (NJSubtype ((mk_nbound true Y T1) :: G) - (swap_NTyp Y X S2) (swap_NTyp Y X T2))) → - (NJSubtype G (NForall X S1 S2) (NForall X T1 T2)) + (∀Z.¬(Z ∈ fv_Nenv G) → + (Z = X \lor \lnot in_list ? Z (fv_NTyp S2)) \to + (Z = Y \lor \lnot in_list ? Z (fv_NTyp T2)) \to + (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)) | NSA_alpha : ∀G,T1,T2,U1,U2.(NJSubtype G T1 U1) → (alpha_eq T1 T2) → (alpha_eq U1 U2) → @@ -336,8 +340,8 @@ lemma in_Nenv_to_in_env: ∀l,n,n2.mk_nbound true n n2 ∈ l → intros 3;elim l [elim (not_in_list_nil ? ? H) |inversion H1;intros - [destruct H3;destruct;simplify;apply in_list_head - |destruct H5;elim t;simplify;apply in_list_cons;apply H;assumption]] + [destruct;simplify;apply in_list_head + |destruct;elim t;simplify;apply in_list_cons;apply H;assumption]] qed. lemma in_lookup : \forall x,l.(in_list ? x l) \to (lookup x l = true). @@ -360,9 +364,9 @@ lemma posn_length : \forall x,vars.(in_list ? x vars) \to intros 2;elim vars [elim (not_in_list_nil ? ? H) |inversion H1 - [intros;destruct H3;destruct;simplify;rewrite > eqb_n_n;simplify; + [intros;destruct;simplify;rewrite > eqb_n_n;simplify; apply lt_O_S - |intros;destruct H5;simplify;elim (eqb x t);simplify + |intros;destruct;simplify;elim (eqb x t);simplify [apply lt_O_S |apply le_S_S;apply H;assumption]]] qed. @@ -372,10 +376,10 @@ lemma in_remove : \forall a,b,l.(a \neq b) \to (in_list ? a l) \to intros 4;elim l [elim (not_in_list_nil ? ? H1) |inversion H2;intros; - [destruct H4;destruct;simplify;rewrite > not_eq_to_eqb_false + [destruct;simplify;rewrite > not_eq_to_eqb_false [simplify;apply in_list_head |intro;apply H;symmetry;assumption] - |destruct H6;simplify;elim (eqb b t) + |destruct;simplify;elim (eqb b t) [simplify;apply H1;assumption |simplify;apply in_list_cons;apply H1;assumption]]] qed. @@ -518,7 +522,7 @@ intros 3;elim T [elim (not_in_list_nil ? ? H3) |inversion H4 [intros;simplify;rewrite > eqb_n_n;reflexivity - |intros;simplify;destruct H8;rewrite > (H3 ? H5); + |intros;simplify;destruct;rewrite > (H3 ? H5); elim (eqb n1 t);reflexivity]]] |elim (decidable_eq_nat n a); [rewrite < H3;simplify;rewrite < posn_swap;rewrite > lookup_swap; @@ -559,8 +563,8 @@ intros 3;elim T |simplify in H11;rewrite < (H7 H11);reflexivity]] |*:assumption]]] |inversion H4 - [intros;destruct H6;destruct;reflexivity - |intros;destruct H8;elim (not_in_list_nil ? ? H5)]] + [intros;destruct;reflexivity + |intros;destruct;elim (not_in_list_nil ? ? H5)]] |*:assumption]]] |simplify;reflexivity |simplify;simplify in H2;rewrite < H @@ -603,10 +607,10 @@ intros 3;elim l 0 |assumption] |rewrite > (not_eq_to_eqb_false ? ? H) in H2;simplify in H2; inversion H2 - [intros;destruct H4;split + [intros;destruct;split [apply in_list_head |intro;autobatch] - |intros;destruct H6; + |intros;destruct; elim (H1 H3);split [apply in_list_cons;assumption |assumption]]]] @@ -619,13 +623,13 @@ intros 3;elim l |simplify;elim (decidable_eq_nat y t) [rewrite > (eq_to_eqb_true ? ? H3);simplify;apply H [(*FIXME*)generalize in match H1;intro;inversion H1 - [intros;destruct H6;destruct;elim H2;reflexivity - |intros;destruct H8;assumption] + [intros;destruct;elim H2;reflexivity + |intros;destruct;assumption] |assumption] |rewrite > (not_eq_to_eqb_false ? ? H3);simplify; (*FIXME*)generalize in match H1;intro;inversion H4 - [intros;destruct H6;destruct;apply in_list_head - |intros;destruct H8;destruct;apply in_list_cons;apply (H H5 H2) + [intros;destruct;apply in_list_head + |intros;destruct;apply in_list_cons;apply (H H5 H2) ]]] qed. @@ -663,10 +667,10 @@ intros;elim H [rewrite > H7;apply in_list_head |apply in_list_cons;(*FIXME*)generalize in match H6;intro; inversion H6 - [intros;destruct H10;destruct;apply in_list_head - |intros;destruct H12;apply in_list_cons;inversion H9 - [intros;destruct H12;elim H7;reflexivity - |intros;destruct H14; + [intros;destruct;apply in_list_head + |intros;destruct;apply in_list_cons;inversion H9 + [intros;destruct;elim H7;reflexivity + |intros;destruct; elim (in_list_append_to_or_in_list ? ? ? ? H11) [apply in_list_to_in_list_append_r;assumption |apply in_list_to_in_list_append_l;assumption]]]]]] @@ -680,18 +684,18 @@ intros 4;elim T [simplify in H;simplify;simplify in H1;elim (decidable_eq_nat y n) [rewrite > H2 in H1;rewrite > swap_right in H1; inversion H1 - [intros;destruct H4;split + [intros;destruct;split [unfold;intro;apply H;rewrite > H2;apply in_list_head |left;reflexivity] - |intros;destruct H6;elim (not_in_list_nil ? ? H3)] + |intros;destruct;elim (not_in_list_nil ? ? H3)] |elim (decidable_eq_nat b n) [rewrite > H3 in H;elim H;apply in_list_cons;apply in_list_head |rewrite > swap_other in H1 [split [inversion H1 - [intros;destruct H5;intro;apply H2; + [intros;destruct;intro;apply H2; symmetry;assumption - |intros;destruct H7; + |intros;destruct; elim (not_in_list_nil ? ? H4)] |autobatch] |intro;autobatch @@ -708,8 +712,8 @@ intros 4;elim T [apply (in_list_to_in_list_append_r ? ? (y::var_NTyp n) (var_NTyp n1)); assumption |inversion H6 - [intros;destruct H8;apply in_list_head - |intros;destruct H10; + [intros;destruct;apply in_list_head + |intros;destruct; elim (not_in_list_nil ? ? H7)]] |assumption] |elim H @@ -719,8 +723,8 @@ intros 4;elim T [left;assumption |right;apply in_list_to_in_list_append_l;assumption]] |intro;apply H2;inversion H5 - [intros;destruct H7;apply in_list_head - |intros;destruct H9;apply in_list_cons; + [intros;destruct;apply in_list_head + |intros;destruct;apply in_list_cons; apply in_list_to_in_list_append_l;assumption] |assumption]] |simplify;simplify in H3;simplify in H2;elim (nat_in_list_case ? ? ? H3) @@ -738,8 +742,8 @@ intros 4;elim T destruct;apply in_list_cons;apply in_list_head |destruct;assumption]]]] |intro;apply H2;inversion H5 - [intros;destruct H7;apply in_list_head - |intros;destruct H9; + [intros;destruct;apply in_list_head + |intros;destruct; apply in_list_cons; cut ((n::var_NTyp n1)@(var_NTyp n2) = n::var_NTyp n1@var_NTyp n2) [rewrite < Hcut;elim (n::var_NTyp n1) @@ -757,8 +761,8 @@ intros 4;elim T |right;apply in_list_to_in_list_append_l; assumption]] |intro;apply H2;inversion H5 - [intros;destruct H7;apply in_list_head - |intros;destruct H9;apply in_list_cons; + [intros;destruct;apply in_list_head + |intros;destruct;apply in_list_cons; elim (decidable_eq_nat b n) [rewrite > H8;apply in_list_head |apply in_list_cons;apply in_list_to_in_list_append_l; @@ -777,14 +781,14 @@ intros 4;elim T [elim H2;cut (y = n) [rewrite > Hcut1;rewrite > swap_right;rewrite > H3;apply in_list_head |inversion H4 - [intros;destruct H6;autobatch - |intros;destruct H8;elim (not_in_list_nil ? ? H5)]] + [intros;destruct;autobatch + |intros;destruct;elim (not_in_list_nil ? ? H5)]] |elim H2;inversion H4 - [intros;destruct H6;destruct;rewrite > (swap_other b y x) + [intros;destruct;rewrite > (swap_other b y x) [apply in_list_head |intro;autobatch |assumption] - |intros;destruct H8;elim (not_in_list_nil ? ? H5)]] + |intros;destruct;elim (not_in_list_nil ? ? H5)]] |intro;apply H;apply (in_list_to_in_list_append_r ? ? [y] [n]); rewrite > H2;apply in_list_head] |simplify in H1;elim H1;elim H2;elim (not_in_list_nil ? ? H4) @@ -806,13 +810,13 @@ intros 4;elim T [assumption |right;split;assumption]]] |intro;apply H2;inversion H4 - [intros;destruct H6;apply in_list_head - |intros;destruct H8;apply in_list_cons; + [intros;destruct;apply in_list_head + |intros;destruct;apply in_list_cons; simplify;apply in_list_to_in_list_append_l; assumption]] |intro;apply H2;inversion H4 - [intros;destruct H6;apply in_list_head - |intros;destruct H8;apply in_list_cons; + [intros;destruct;apply in_list_head + |intros;destruct;apply in_list_cons; simplify;apply in_list_to_in_list_append_r; assumption]] |simplify;simplify in H3;cut (\lnot (in_list ? b (y::var_NTyp n1))) @@ -855,14 +859,14 @@ intros 4;elim T |intro;autobatch |intro;autobatch]]]]]] |intro;apply H2;inversion H4 - [intros;destruct H6;apply in_list_head - |simplify;intros;destruct H8; + [intros;destruct;apply in_list_head + |simplify;intros;destruct; apply in_list_cons; apply (in_list_to_in_list_append_r ? ? (n::var_NTyp n1) (var_NTyp n2)); assumption]] |intro;apply H2;inversion H4 - [intros;destruct H6;apply in_list_head - |simplify;intros;destruct H8; + [intros;destruct;apply in_list_head + |simplify;intros;destruct; apply in_list_cons; apply (in_list_to_in_list_append_l ? ? (n::var_NTyp n1) (var_NTyp n2)); apply in_list_cons;assumption]]] @@ -896,8 +900,8 @@ intros;elim H assumption] |apply (Hletin ? Hletin1)] |intro;apply H7;inversion H10 - [intros;destruct H12;apply in_list_head - |intros;destruct H14;do 2 apply in_list_cons; + [intros;destruct;apply in_list_head + |intros;destruct;do 2 apply in_list_cons; apply in_list_to_in_list_append_l;assumption] |right;split;assumption] |intros;intro;lapply (inlist_fv_swap_r x n4 a n1) @@ -911,8 +915,8 @@ intros;elim H |apply in_list_cons;apply in_list_to_in_list_append_r; assumption]]] |intro;apply H7;inversion H11 - [intros;destruct H13;apply in_list_head - |intros;destruct H15;do 2 apply in_list_cons; + [intros;destruct;apply in_list_head + |intros;destruct;do 2 apply in_list_cons; apply in_list_to_in_list_append_l;assumption] |right;split;assumption]]]] qed. @@ -977,9 +981,9 @@ intros 3;elim H elim (inlist_fv_swap ? ? ? ? ? Hletin5) [assumption |intro;apply H5;inversion H8 - [intros;destruct H10; + [intros;destruct; apply in_list_head - |intros;destruct H12; + |intros;destruct; do 2 apply in_list_cons; apply in_list_to_in_list_append_l;assumption]] |elim (inlist_fv_swap ? ? ? ? ? H6) @@ -1173,7 +1177,7 @@ apply NTyp_len_ind;intro;elim U [rewrite < (encode_swap X Y n2); [rewrite < (fv_encode ? (Y::l) (Y::l@[Y])) [rewrite > encode_append; - [rewrite < (fv_encode n2 (Y::l) (Y::l@[Y])); + [reflexivity(*rewrite < (fv_encode n2 (Y::l) (Y::l@[Y])); [reflexivity |intros;elim (decidable_eq_nat x Y) [rewrite > H8;simplify;rewrite > eqb_n_n;simplify; @@ -1189,7 +1193,7 @@ apply NTyp_len_ind;intro;elim U [split [reflexivity |intro;rewrite < (H12 H13);reflexivity] - |split [reflexivity|intro;destruct H13]]]]]] + |split [reflexivity|intro;destruct H13]]]]]]*) |simplify;constructor 1] |intros;simplify;elim (decidable_eq_nat x Y) [rewrite > (eq_to_eqb_true ? ? H8);simplify;split @@ -1209,7 +1213,7 @@ apply NTyp_len_ind;intro;elim U |apply in_list_head] |intros;simplify;rewrite > swap_right;rewrite < Hcut; split [reflexivity|intro;reflexivity]] - |rewrite < Hcut;elim (decidable_eq_nat n X) + |(*rewrite < Hcut;*)elim (decidable_eq_nat n X) [rewrite > H7;rewrite > (fv_encode (swap_NTyp X Y n2) (swap X Y X::l) (swap_list X Y (X::l))) [rewrite > (encode_swap X Y n2); @@ -1225,7 +1229,7 @@ apply NTyp_len_ind;intro;elim U |simplify;rewrite < H8;reflexivity]] |simplify;elim l [simplify;rewrite > swap_right;reflexivity - |simplify;destruct H8;rewrite > Hcut1;reflexivity]] + |simplify;destruct;rewrite > Hcut1;reflexivity]] |intro;apply in_list_head |apply in_list_cons;elim l [simplify;apply in_list_head @@ -1239,11 +1243,11 @@ apply NTyp_len_ind;intro;elim U [reflexivity |autobatch |intro;apply H7;inversion H8;intros - [destruct H10;reflexivity - |destruct H12;destruct;elim (H3 H9)] + [destruct;reflexivity + |destruct;elim (H3 H9)] |intro;apply H6;inversion H8;intros - [destruct H10;reflexivity - |destruct H12;destruct;elim (H4 H9)] + [destruct;reflexivity + |destruct;elim (H4 H9)] |intro;apply H5;simplify;apply in_list_to_in_list_append_r; apply (in_remove ? ? ? ? H8);intro;apply H7;symmetry;assumption] |*:assumption]]] @@ -1260,8 +1264,8 @@ qed. lemma in_fvNTyp_in_fvNenv : ∀G,T.(NWFType G T) → (incl ? (fv_NTyp T) (fv_Nenv G)). intros;elim H [simplify;unfold;intros;inversion H2;intros - [destruct H4;assumption - |destruct H6;elim (not_in_list_nil ? ? H3)] + [destruct;assumption + |destruct;elim (not_in_list_nil ? ? H3)] |simplify;unfold;intros;elim (not_in_list_nil ? ? H1) |simplify;unfold;intros;elim (in_list_append_to_or_in_list ? ? ? ? H5) [apply (H2 ? H6)|apply (H4 ? H6)] @@ -1271,26 +1275,25 @@ intros;elim H [cut (a ≠ x ∧ x ≠ n) [elim Hcut;lapply (Hletin x) [simplify in Hletin1;inversion Hletin1;intros; - [destruct H11;elim H8;reflexivity - |destruct H13;assumption] + [destruct;elim H8;reflexivity + |destruct;assumption] |generalize in match H6;generalize in match H7;elim n2 [simplify in H11;elim (decidable_eq_nat n n3) [rewrite > (eq_to_eqb_true ? ? H12) in H11;simplify in H11; elim (not_in_list_nil ? ? H11) |rewrite > (not_eq_to_eqb_false ? ? H12) in H11; simplify in H11;inversion H11;intros - [destruct H14;simplify; + [destruct;simplify; rewrite > swap_other [apply in_list_head |intro;apply H8;rewrite > H13;reflexivity |intro;apply H9;rewrite > H13;reflexivity] - |destruct H16;elim (not_in_list_nil ? ? H13)]] + |destruct;elim (not_in_list_nil ? ? H13)]] |simplify in H11;elim (not_in_list_nil ? ? H11) |simplify in H13;simplify;elim (remove_inlist ? ? ? H13); elim (in_list_append_to_or_in_list ? ? ? ? H14) [apply in_list_to_in_list_append_l;apply H10 - [rewrite < (append_associative ? [x] (fv_Nenv l) (var_NTyp n4)); - intro;apply H12;simplify; + [intro;apply H12;simplify; rewrite < (append_associative ? [x] (fv_Nenv l) (var_NTyp n3 @ var_NTyp n4)); elim (in_list_append_to_or_in_list ? ? (x::fv_Nenv l) (var_NTyp n3) H17); [apply in_list_to_in_list_append_l;assumption @@ -1298,8 +1301,7 @@ intros;elim H apply in_list_to_in_list_append_l;assumption] |apply (in_remove ? ? ? H15 H16)] |apply in_list_to_in_list_append_r;apply H11 - [rewrite < (append_associative ? [x] (fv_Nenv l) (var_NTyp n3)); - intro;apply H12;simplify; + [intro;apply H12;simplify; rewrite < (append_associative ? [x] (fv_Nenv l) (var_NTyp n3 @ var_NTyp n4)); elim (in_list_append_to_or_in_list ? ? (x::fv_Nenv l) (var_NTyp n4) H17); [apply in_list_to_in_list_append_l;assumption @@ -1353,8 +1355,8 @@ intros 2;elim T [elim H1;apply H2;reflexivity |simplify;apply in_list_head] |(*FIXME*)generalize in match H;intro;inversion H;intros; - [destruct H4;reflexivity - |destruct H6;elim (not_in_list_nil ? ? H3)]] + [destruct;reflexivity + |destruct;elim (not_in_list_nil ? ? H3)]] |simplify in H;elim (not_in_list_nil ? ? H) |simplify;simplify in H2; elim (in_list_append_to_or_in_list ? ? ? ? H2); @@ -1366,8 +1368,8 @@ intros 2;elim T |apply in_list_to_in_list_append_r; elim (remove_inlist ? ? ? H4);apply (H1 ? H5);intro;apply H6; inversion H7;intros - [destruct H9;reflexivity - |destruct H11;elim (H3 H8)]]] + [destruct;reflexivity + |destruct;elim (H3 H8)]]] qed. lemma adeq_WFT : ∀G,T.NWFType G T → WFType (encodeenv G) (encodetype T []). @@ -1384,8 +1386,8 @@ intros;elim H [left;assumption |right;intro;apply H6;apply (fv_NTyp_fv_Typ ? ? ? H8);intro; apply H7;inversion H9;intros - [destruct H11;reflexivity - |destruct H13; + [destruct;reflexivity + |destruct; elim (not_in_list_nil ? ? H10)]]] |4:intro;elim (decidable_eq_nat X n) [assumption @@ -1393,11 +1395,11 @@ intros;elim H [generalize in match Hcut;generalize in match [n]; generalize in match H7;elim n2 [simplify in H9;generalize in match H9;intro;inversion H9;intros; - [destruct H13;destruct;simplify; + [destruct;simplify; generalize in match (lookup_in X l1);elim (lookup X l1) [elim H10;apply H12;reflexivity |simplify;apply in_list_head] - |destruct H15; + |destruct; elim (not_in_list_nil ? ? H12)] |simplify in H9;elim (not_in_list_nil ? ? H9) |simplify;simplify in H11; @@ -1409,11 +1411,11 @@ intros;elim H apply in_list_to_in_list_append_r; apply (H10 H14); intro;inversion H16;intros; - [destruct H18;destruct;elim H15;reflexivity - |destruct H20;elim H12;assumption]]] + [destruct;elim H15;reflexivity + |destruct;elim H12;assumption]]] |intro;elim H8;inversion H9;intros - [destruct H11;autobatch - |destruct H13;elim (not_in_list_nil ? ? H10)]]] + [destruct;autobatch + |destruct;elim (not_in_list_nil ? ? H10)]]] |*:apply not_in_list_nil]]] qed. @@ -1423,9 +1425,9 @@ intro;elim T;simplify [apply (bool_elim ? (lookup n l));intro [simplify;apply not_in_list_nil |simplify;intro;inversion H2;intros - [destruct H4; + [destruct; rewrite > (in_lookup ? ? H) in H1;destruct H1 - |destruct H6;apply (not_in_list_nil ? ? H3)]] + |destruct;apply (not_in_list_nil ? ? H3)]] |apply not_in_list_nil |intro;elim (nat_in_list_case ? ? ? H3) [apply H1;assumption @@ -1460,7 +1462,7 @@ intros 3;elim H [rewrite > H2 in H1;rewrite < eq_fv_Nenv_fv_env in H1; cut (T2 = TName n) [|generalize in match H3;elim T2 - [simplify in H4;destruct H4;reflexivity + [simplify in H4;destruct;reflexivity |simplify in H4;destruct H4 |simplify in H6;destruct H6 |simplify in H6;destruct H6]] @@ -1477,7 +1479,7 @@ intros 3;elim H [1,2:simplify in H7;destruct H7 |apply (ex_intro ? ? n);apply (ex_intro ? ? n1);reflexivity |simplify in H9;destruct H9]] - elim Hcut;elim H7;rewrite > H8 in H6;simplify in H6;destruct H6; + elim Hcut;elim H7;rewrite > H8 in H6;simplify in H6;destruct; apply NWFT_Arrow;autobatch |cut (\exists Z,U,V.T2 = NForall Z U V) [|generalize in match H6;elim T2 @@ -1486,7 +1488,7 @@ intros 3;elim H |apply (ex_intro ? ? n);apply (ex_intro ? ? n1); apply (ex_intro ? ? n2);reflexivity]] elim Hcut;elim H7;elim H8;clear Hcut H7 H8;rewrite > H9; - rewrite > H9 in H6;simplify in H6;destruct H6;apply NWFT_Forall + rewrite > H9 in H6;simplify in H6;destruct;apply NWFT_Forall [autobatch |intros;elim H6 [rewrite > H7;cut (swap_NTyp a a a2 = a2) @@ -1499,7 +1501,7 @@ intros 3;elim H [rewrite < eq_fv_Nenv_fv_env;assumption |rewrite > H7;apply not_in_list_encodetype; apply in_list_head - |rewrite > H7;simplify;rewrite < Hcut;reflexivity + |rewrite > H7;simplify;reflexivity |rewrite > H7;autobatch] |apply (H4 Y) [rewrite < eq_fv_Nenv_fv_env;assumption @@ -1531,10 +1533,30 @@ intros 3;elim H |intros;apply (H4 ? ? H8); [intro;apply H7;apply (H6 ? H9) |unfold;intros;simplify;simplify in H9;inversion H9;intros - [destruct H11;apply in_list_head - |destruct H13;apply in_list_cons;apply (H6 ? H10)]]]] + [destruct;apply in_list_head + |destruct;apply in_list_cons;apply (H6 ? H10)]]]] qed. +(*lemma NWFT_subst : + \forall T,U,a,X,Y,G. + NWFType (mk_nbound true a U::G) (swap_NTyp a X T) \to + \lnot (in_list ? a (Y::X::fv_NTyp T@fv_Nenv G)) \to + \lnot (in_list ? Y (fv_Nenv G)) \to + (Y = X \lor \lnot (in_list ? Y (fv_NTyp T))) \to + NWFType (mk_nbound true Y U::G) (swap_NTyp Y X T). +apply NTyp_len_ind;intro;cases U + [4:simplify;intros;apply NWFT_Forall + [ + |intros;apply (H ? ? ? Y) + [2:inversion H1;simplify;intros;destruct; + [ + +intros 7;elim T + [4:simplify;apply NWFT_Forall + [ + |intros;*) + + lemma NJSubtype_to_NWFT : ∀G,T,U.NJSubtype G T U → NWFType G T ∧ NWFType G U. intros;elim H [split [assumption|apply NWFT_Top] @@ -1544,17 +1566,11 @@ intros;elim H [elim (not_in_list_nil ? ? H6) |inversion H7;intros [rewrite < H8;simplify;apply in_list_head - |destruct H11;elim t;simplify;apply in_list_cons; + |destruct;elim t;simplify;apply in_list_cons; apply H6;assumption]] |assumption] |elim H2;elim H4;split;apply NWFT_Arrow;assumption - |elim H2;split;apply NWFT_Forall - [1,3:assumption - |*:intros;elim (H4 Y H7); - [apply (NWFT_env_incl ? ? H9);unfold;simplify;intros;inversion H11;intros - [destruct H13;apply in_list_head - |destruct H15;apply in_list_cons;assumption] - |assumption]] + |split;assumption |elim H2;split [lapply (adeq_WFT ? ? H5);apply (adeq_WFT2 ? ? Hletin);autobatch |lapply (adeq_WFT ? ? H6);apply (adeq_WFT2 ? ? Hletin);autobatch]] @@ -1568,22 +1584,338 @@ intros;elim H;simplify [apply (adeq_WFE ? H1)|rewrite < eq_fv_Nenv_fv_env;assumption] |apply SA_All [assumption - |intros;lapply (NSA_All ? ? ? ? ? ? H1 H3);rewrite < (encode_subst n2 X n []) - [rewrite < (encode_subst n4 X n []) - [rewrite < eq_fv_Nenv_fv_env in H5;apply (H4 ? H5) + |intros;lapply (NSA_All ? ? ? ? ? ? ? H1 H2 H3 H5); + 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) + [elim (decidable_eq_nat X n) + [left;assumption + |right;intro;lapply (in_remove ? ? ? H10 H11);elim H7; + apply Hletin1;apply in_list_to_in_list_append_r;assumption] + |elim (decidable_eq_nat X n1) + [left;assumption + |right;intro;lapply (in_remove ? ? ? H10 H11);elim H7; + apply Hletin2;apply in_list_to_in_list_append_r;assumption]] |2,3:apply not_in_list_nil |intro;elim (NJSubtype_to_NWFT ? ? ? Hletin); - lapply (in_fvNTyp_in_fvNenv ? ? H8);simplify in Hletin1; - elim (decidable_eq_nat X n) + lapply (in_fvNTyp_in_fvNenv ? ? H10);simplify in Hletin1; + elim (decidable_eq_nat X n1) [assumption - |lapply (in_remove ? ? ? H9 H6);elim H5;rewrite < eq_fv_Nenv_fv_env; + |lapply (in_remove ? ? ? H11 H8);elim H7;rewrite < eq_fv_Nenv_fv_env; apply Hletin1;apply in_list_to_in_list_append_r;assumption]] |2,3:apply not_in_list_nil - |intro;elim (NJSubtype_to_NWFT ? ? ? Hletin);lapply (in_fvNTyp_in_fvNenv ? ? H7); + |intro;elim (NJSubtype_to_NWFT ? ? ? Hletin);lapply (in_fvNTyp_in_fvNenv ? ? H9); simplify in Hletin1;elim (decidable_eq_nat X n) [assumption - |lapply (in_remove ? ? ? H9 H6);elim H5;rewrite < eq_fv_Nenv_fv_env; + |lapply (in_remove ? ? ? H11 H8);elim H7;rewrite < eq_fv_Nenv_fv_env; apply Hletin1;apply in_list_to_in_list_append_r;assumption]]] |rewrite < (alpha_to_encode ? ? H3);rewrite < (alpha_to_encode ? ? H4); assumption] -qed. \ No newline at end of file +qed. + +let rec closed_type T n ≝ + match T with + [ TVar m ⇒ m < n + | TFree X ⇒ True + | Top ⇒ True + | Arrow T1 T2 ⇒ closed_type T1 n ∧ closed_type T2 n + | Forall T1 T2 ⇒ closed_type T1 n ∧ closed_type T2 (S n)]. + +alias id "nth" = "cic:/matita/list/list/nth.con". +alias id "length" = "cic:/matita/list/list/length.con". +definition distinct_list ≝ +λl.∀n,m.n < length ? l → m < length ? l → n ≠ m → nth ? l O n ≠ nth ? l O m. + +lemma posn_nth: ∀l,n.distinct_list l → n < length ? l → + posn l (nth ? l O n) = n. +intro;elim l + [simplify in H1;elim (not_le_Sn_O ? H1) + |simplify in H2;generalize in match H2;elim n + [simplify;rewrite > eqb_n_n;simplify;reflexivity + |simplify;cut (nth ? (t::l1) O (S n1) ≠ nth ? (t::l1) O O) + [simplify in Hcut;rewrite > (not_eq_to_eqb_false ? ? Hcut);simplify; + rewrite > (H n1) + [reflexivity + |unfold;intros;unfold in H1;lapply (H1 (S n2) (S m)); + [simplify in Hletin;assumption + |2,3:simplify;autobatch + |intro;apply H7;destruct H8;reflexivity] + |autobatch] + |intro;apply H1; + [6:apply H5 + |skip + |skip + |*:autobatch]]]] +qed. + +lemma nth_in_list : ∀l,n. n < length ? l → nth ? l O n ∈ l. +intro;elim l + [simplify in H;elim (not_le_Sn_O ? H) + |generalize in match H1;elim n + [simplify;apply in_list_head + |simplify;apply in_list_cons;apply H;simplify in H3;apply (le_S_S_to_le ? ? H3)]] +qed. + +lemma lookup_nth : \forall l,n.n < length ? l \to + lookup (nth nat l O n) l = true. +intro;elim l + [elim (not_le_Sn_O ? H); + |generalize in match H1;elim n + [simplify;rewrite > eqb_n_n;reflexivity + |simplify;elim (eqb (nth nat l1 O n1) t) + [reflexivity + |simplify;apply H;apply le_S_S_to_le;assumption]]] +qed. + +lemma decoder : ∀T,n.closed_type T n → + ∀l.length ? l = n → distinct_list l → + (\forall x. in_list ? x (fv_type T) \to \lnot in_list ? x l) \to + ∃U.T = encodetype U l. +intro;elim T + [simplify in H;apply (ex_intro ? ? (TName (nth ? l O n)));simplify; + rewrite > lookup_nth + [simplify;rewrite > posn_nth; + [reflexivity|assumption|rewrite > H1;assumption] + |rewrite > H1;assumption] + |apply (ex_intro ? ? (TName n));rewrite > (fv_encode (TName n) l []); + [simplify;reflexivity + |intros;simplify in H3;simplify in H4;lapply (H3 ? H4); + cut (lookup x l = false) + [rewrite > Hcut;simplify;split + [reflexivity|intro;destruct H5] + |elim (bool_to_decidable_eq (lookup x l) true) + [lapply (lookup_in ? ? H5);elim (Hletin Hletin1) + |generalize in match H5;elim (lookup x l); + [elim H6;reflexivity|reflexivity]]]] + |apply (ex_intro ? ? NTop);simplify;reflexivity + |simplify in H2;elim H2;lapply (H ? H6 ? H3 H4); + [lapply (H1 ? H7 ? H3 H4) + [elim Hletin;elim Hletin1; + apply (ex_intro ? ? (NArrow a a1));simplify; + rewrite < H9;rewrite < H8;reflexivity + |intros;apply H5;simplify;apply in_list_to_in_list_append_r;assumption] + |intros;apply H5;simplify;apply in_list_to_in_list_append_l;assumption] + |simplify in H2;elim H2;elim (H ? H6 ? H3 H4);elim (fresh_name (fv_type t1@l)); + [elim (H1 ? H7 (a1::l)) + [apply (ex_intro ? ? (NForall a1 a a2));simplify;rewrite < H8;rewrite < H10; + reflexivity + |simplify;rewrite > H3;reflexivity + |unfold;intros;intro;apply H12;generalize in match H13;generalize in match H10; + generalize in match H11;generalize in match H9; + generalize in match m;generalize in match n1; + apply nat_elim2 + [intro;elim n2 + [reflexivity + |simplify in H18;rewrite > H18 in H9;elim H9;simplify in H16; + lapply (le_S_S_to_le ? ? H16);apply in_list_to_in_list_append_r; + autobatch] + |intro;intros;change in H17:(? ? % ?) with (nth nat l O n2); + simplify in H17:(? ? ? %);elim H9;rewrite < H17; + apply in_list_to_in_list_append_r;apply nth_in_list; + simplify in H16;apply (le_S_S_to_le ? ? H16) + |intros;change in H18 with (nth nat l O n2 = nth nat l O m1); + unfold in H4;elim (decidable_eq_nat n2 m1) + [rewrite > H19;reflexivity + |simplify in H17;simplify in H16;elim (H4 ? ? ? ? H19) + [assumption + |apply (le_S_S_to_le ? ? H17) + |apply (le_S_S_to_le ? ? H16)]]] + |intro;elim (in_list_cons_case ? ? ? ? H11) + [apply H9;apply in_list_to_in_list_append_l;rewrite < H12;assumption + |apply (H5 x) + [simplify;apply in_list_to_in_list_append_r;assumption + |assumption]]] + |apply H5;simplify;apply in_list_to_in_list_append_l;assumption]] +qed. + +lemma closed_subst : \forall T,X,n.closed_type (subst_type_nat T (TFree X) n) n + \to closed_type T (S n). +intros 2;elim T 0;simplify;intros + [elim (decidable_eq_nat n n1) + [rewrite > H1;apply le_n + |rewrite > (not_eq_to_eqb_false ? ? H1) in H;simplify in H; + apply le_S;assumption] + |2,3:apply I + |elim H2;split;autobatch + |elim H2;split;autobatch] +qed. + +lemma WFT_to_closed: ∀G,T.WFType G T → closed_type T O. +intros;elim H;simplify + [apply I + |apply I + |split;assumption + |split + [assumption + |elim (fresh_name (fv_env l@fv_type t1));lapply (H4 a) + [autobatch + |intro;apply H5;apply in_list_to_in_list_append_l;assumption + |intro;apply H5;apply in_list_to_in_list_append_r;assumption]]] +qed. + +lemma adeq_WFE2 : ∀G1.WFEnv G1 → ∀G2.(G1 = encodeenv G2) → NWFEnv G2. +intros 2;elim H 0 + [intro;elim G2 + [apply NWFE_Empty + |simplify in H2;destruct H2] + |intros 9;elim G2 + [simplify in H5;destruct H5 + |generalize in match H6;elim t1;simplify in H7;destruct H7;apply NWFE_cons + [apply H2;reflexivity + |rewrite > eq_fv_Nenv_fv_env;assumption + |autobatch]]] +qed. + +lemma xxx : \forall b,X,T,l. + in_list ? (mk_bound b X (encodetype T [])) (encodeenv l) \to + \exists U.encodetype U [] = encodetype T [] \land + in_list ? (mk_nbound b X U) l. +intros 4;elim l + [simplify in H;elim (not_in_list_nil ? ? H) + |simplify in H1;inversion H1;elim t 0;simplify;intros;destruct; + [apply (ex_intro ? ? n1);split;autobatch + |elim (H H2);elim H4;apply (ex_intro ? ? a);split;autobatch]] +qed. + +lemma eq_swap_NTyp_to_case : + \forall X,Y,Z,T.\lnot in_list ? Y (X::var_NTyp T) \to + swap_NTyp Z Y (swap_NTyp Y X T) = swap_NTyp Z X T \to + Z = X \lor \lnot in_list ? Z (fv_NTyp T). +intros 4;elim T + [simplify in H;simplify in H1;elim (decidable_eq_nat X n) + [rewrite > H2;simplify;elim (decidable_eq_nat Z n) + [left;assumption + |right;intro;apply H3;apply in_list_singleton_to_eq;assumption] + |elim (decidable_eq_nat Y n) + [elim H;rewrite > H3;apply in_list_cons;apply in_list_head + |rewrite > (swap_other Y X n) in H1 + [elim (decidable_eq_nat Z n) + [rewrite > H4 in H1;do 2 rewrite > swap_left in H1; + destruct H1;elim H;apply in_list_head + |elim (decidable_eq_nat Z X) + [left;assumption + |rewrite > (swap_other Z X n) in H1 + [right;intro;apply H3;simplify in H6; + rewrite > (in_list_singleton_to_eq ? ? ? H6) in H1; + rewrite > swap_left in H1;destruct H1;reflexivity + |intro;apply H4;symmetry;assumption + |intro;apply H2;symmetry;assumption]]] + |intro;apply H3;symmetry;assumption + |intro;apply H2;symmetry;assumption]]] + |simplify;right;apply not_in_list_nil + |elim H + [left;assumption + |elim H1 + [left;assumption + |right;simplify;intro;elim (in_list_append_to_or_in_list ? ? ? ? H6) + [elim (H4 H7) + |elim (H5 H7)] + |intro;apply H2;simplify;inversion H5;intros;destruct; + [apply in_list_head + |apply in_list_cons;apply in_list_to_in_list_append_r;assumption] + |simplify in H3;destruct H3;assumption] + |intro;apply H2;simplify;inversion H4;intros;destruct; + [apply in_list_head + |apply in_list_cons;apply in_list_to_in_list_append_l;assumption] + |simplify in H3;destruct H3;assumption] + |elim H + [left;assumption + |elim H1 + [left;assumption + |right;simplify;intro;elim (in_list_append_to_or_in_list ? ? ? ? H6) + [elim (H4 H7) + |elim H5;elim (remove_inlist ? ? ? H7);assumption] + |intro;apply H2;simplify;inversion H5;intros;destruct; + [apply in_list_head + |do 2 apply in_list_cons;apply in_list_to_in_list_append_r;assumption] + |simplify in H3;destruct H3;assumption] + |intro;apply H2;simplify;inversion H4;intros;destruct; + [apply in_list_head + |do 2 apply in_list_cons;apply in_list_to_in_list_append_l;assumption] + |simplify in H3;destruct H3;assumption]] +qed. + + +theorem faithfulness : ∀G1,T1,U1.G1 ⊢ T1 ⊴ U1 → + ∀G2,T2,U2. + G1 = encodeenv G2 → + T1 = encodetype T2 [] → + U1 = encodetype U2 [] → + NJSubtype G2 T2 U2. +intros 4;elim H 0 + [intros;cut (U2 = NTop) + [|generalize in match H5;elim U2 0;simplify;intros;destruct;reflexivity] + rewrite > Hcut;apply NSA_Top; + [apply (adeq_WFE2 ? H1);assumption + |apply (adeq_WFT2 ? ? H2);assumption] + |intros;cut (T2 = TName n ∧ U2 = TName n) + [|split + [generalize in match H4;elim T2 0;simplify;intros;destruct;reflexivity + |generalize in match H5;elim U2 0;simplify;intros;destruct;reflexivity]] + elim Hcut; + rewrite > H6;rewrite > H7;apply NSA_Refl_TVar; + [apply (adeq_WFE2 ? H1);assumption + |rewrite > H3 in H2;rewrite < eq_fv_Nenv_fv_env in H2;assumption] + |intros;cut (T2 = TName n) + [|generalize in match H5;elim T2 0;simplify;intros;destruct;reflexivity] + rewrite > Hcut; + elim (decoder t1 O ? []); + [rewrite > H4 in H1;rewrite > H7 in H1;elim (xxx ? ? ? ? H1);elim H8; + apply NSA_Trans_TVar + [apply a1 + |assumption + |apply H3;autobatch] + |apply (WFT_to_closed l);apply (JS_to_WFT1 ? ? ? H2) + |simplify;reflexivity + |unfold;intros;simplify in H7;elim (not_le_Sn_O ? H7) + |apply not_in_list_nil] + |intros;cut (∃u,u1,u2,u3.T2 = NArrow u u1 ∧ U2 = NArrow u2 u3) + [elim Hcut;elim H8;elim H9;elim H10;elim H11;clear Hcut H8 H9 H10 H11; + rewrite > H12;rewrite > H13;rewrite > H13 in H7;simplify in H7;destruct; + simplify in H6;destruct;apply NSA_Arrow + [apply H2;reflexivity + |apply H4;reflexivity] + |generalize in match H6;elim T2 0;simplify;intros;destruct; + generalize in match H7;elim U2 0;simplify;intros;destruct; + autobatch depth=6 width=2 size=7] + |intros;cut (∃n,u,u1,n1,u2,u3.T2 = NForall n u u1 ∧ U2 = NForall n1 u2 u3) + [elim Hcut;elim H8;elim H9;elim H10;elim H11;elim H12;elim H13; + clear Hcut H8 H9 H10 H11 H12 H13;rewrite > H14;rewrite > H15; + rewrite > H14 in H6;rewrite > H15 in H7;simplify in H6;simplify in H7; + destruct H6;destruct H7;lapply (SA_All ? ? ? ? ? H1 H3);destruct H5; + lapply (JS_to_WFT1 ? ? ? Hletin);lapply (JS_to_WFT2 ? ? ? Hletin); + apply NSA_All + [apply (adeq_WFT2 ? ? Hletin1);reflexivity + |apply (adeq_WFT2 ? ? Hletin2);reflexivity + |apply H2;reflexivity + |intros;apply H4; + [apply Z + |rewrite < eq_fv_Nenv_fv_env;assumption + |simplify;reflexivity + |rewrite < (encode_subst a2 Z a []); + [reflexivity + |2,3:apply not_in_list_nil + |lapply (SA_All ? ? ? ? ? H1 H3);lapply (JS_to_WFT1 ? ? ? Hletin); + intro;elim (decidable_eq_nat Z a) + [assumption + |lapply (fv_WFT ? Z ? Hletin1) + [elim H5;rewrite > eq_fv_Nenv_fv_env;assumption + |simplify;apply in_list_to_in_list_append_r; + apply fv_NTyp_fv_Typ + [assumption + |intro;apply H9;autobatch]]]] + |rewrite < (encode_subst a5 Z a3 []) + [reflexivity + |2,3:apply not_in_list_nil + |intro;elim H7 + [assumption + |elim (H9 H8)]]]] + |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]] +qed. -- 2.39.2