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
[ 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
| 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) →
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).
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.
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.
[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;
|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
|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]]]]
|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.
[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]]]]]]
[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
[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
[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)
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)
|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;
[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)
[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)))
|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]]]
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)
|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.
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)
[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;
[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
|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);
|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
[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]]]
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)]
[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
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
[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);
|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 []).
[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
[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;
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.
[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
[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]]
[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
|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)
[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
|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]
[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]]
[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.
projects / helm.git / commitdiff