| 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)).
(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)).
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
[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 →
[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]))
|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.
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).
|*: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 ≝
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
|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]]
projects / helm.git / blobdiff