-
(**************************************************************************)
(* ___ *)
(* ||M|| *)
nbtype : NTyp
}.
-inductive option (A:Type) : Set \def
-| Some : A \to option A
-| None : option A.
-
-definition swap : nat → nat → nat → nat ≝
- λu,v,x.match (eqb x u) with
- [true ⇒ v
- |false ⇒ match (eqb x v) with
- [true ⇒ u
- |false ⇒ x]].
-
-lemma swap_left : ∀x,y.(swap x y x) = y.
-intros;unfold swap;rewrite > eqb_n_n;simplify;reflexivity;
-qed.
-
-lemma swap_right : ∀x,y.(swap x y y) = x.
-intros;unfold swap;rewrite > eqb_n_n;apply (eqb_elim y x);intro;autobatch;
-qed.
-
-lemma swap_other : \forall x,y,z.(z \neq x) \to (z \neq y) \to (swap x y z) = z.
-intros;unfold swap;apply (eqb_elim z x);intro;simplify
- [elim H;assumption
- |rewrite > not_eq_to_eqb_false;autobatch]
-qed.
-
-lemma swap_inv : \forall u,v,x.(swap u v (swap u v x)) = x.
-intros;unfold in match (swap u v x);apply (eqb_elim x u);intro;simplify
- [autobatch paramodulation
- |apply (eqb_elim x v);intro;simplify
- [autobatch paramodulation
- |apply swap_other;assumption]]
-qed.
-
-lemma swap_inj : ∀u,v,x,y.swap u v x = swap u v y → x = y.
-intros 4;unfold swap;apply (eqb_elim x u);simplify;intro
- [apply (eqb_elim y u);simplify;intro
- [intro;autobatch paramodulation
- |apply (eqb_elim y v);simplify;intros
- [autobatch paramodulation
- |elim H2;symmetry;assumption]]
- |apply (eqb_elim y u);simplify;intro
- [apply (eqb_elim x v);simplify;intros;
- [autobatch paramodulation
- |elim H2;assumption]
- |apply (eqb_elim x v);simplify;intro
- [apply (eqb_elim y v);simplify;intros
- [autobatch paramodulation
- |elim H1;symmetry;assumption]
- |apply (eqb_elim y v);simplify;intros
- [elim H;assumption
- |assumption]]]]
-qed.
+let rec encodetype T vars on T ≝
+ match T with
+ [ (TName n) ⇒ match (lookup n vars) with
+ [ true ⇒ (TVar (posn vars n))
+ | false ⇒ (TFree n)]
+ | NTop ⇒ Top
+ | (NArrow T1 T2) ⇒ Arrow (encodetype T1 vars) (encodetype T2 vars)
+ | (NForall n2 T1 T2) ⇒ Forall (encodetype T1 vars)
+ (encodetype T2 (n2::vars))].
let rec swap_NTyp u v T on T ≝
match T with
|(Arrow T1 T2) ⇒ (Arrow (swap_Typ u v T1) (swap_Typ u v T2))
|(Forall T1 T2) ⇒ (Forall (swap_Typ u v T1) (swap_Typ u v T2))].
-definition swap_list : nat \to nat \to (list nat) \to (list nat) ≝
- \lambda u,v,l.(map ? ? (swap u v) l).
-
let rec var_NTyp (T:NTyp):list nat\def
match T with
[TName x ⇒ [x]
|NArrow U V ⇒ (var_NTyp U)@(var_NTyp V)
|NForall X U V ⇒ X::(var_NTyp U)@(var_NTyp V)].
-inductive alpha_eq : NTyp \to NTyp \to Prop \def
-| A_refl : \forall T.(alpha_eq T T)
-| A_arrow : \forall T1,T2,U1,U2.(alpha_eq T1 U1) \to (alpha_eq T2 U2) \to
- (alpha_eq (NArrow T1 T2) (NArrow U1 U2))
-| A_forall : \forall T1,T2,U1,U2,X,Y.
- (alpha_eq T1 U1) \to
- (\forall Z.
- \lnot (in_list nat Z (X::Y::((var_NTyp T2)@(var_NTyp U2))))
- \to (alpha_eq (swap_NTyp Z X T2) (swap_NTyp Z Y U2))) \to
- (alpha_eq (NForall X T1 T2) (NForall Y U1 U2)).
-
-let rec posn l x on l ≝
- match l with
- [ nil ⇒ O
- | (cons (y:nat) l2) ⇒
- match (eqb x y) with
- [ true ⇒ O
- | false ⇒ S (posn l2 x)]].
-
-let rec length A l on l ≝
- match l with
- [ nil ⇒ O
- | (cons (y:A) l2) ⇒ S (length A l2)].
-
-let rec lookup n l on l ≝
- match l with
- [ nil ⇒ false
- | cons (x:nat) l1 ⇒ match (eqb n x) with
- [true ⇒ true
- |false ⇒ (lookup n l1)]].
-
-let rec encodetype T vars on T ≝
- match T with
- [ (TName n) ⇒ match (lookup n vars) with
- [ true ⇒ (TVar (posn vars n))
- | false ⇒ (TFree n)]
- | NTop ⇒ Top
- | (NArrow T1 T2) ⇒ Arrow (encodetype T1 vars) (encodetype T2 vars)
- | (NForall n2 T1 T2) ⇒ Forall (encodetype T1 vars)
- (encodetype T2 (n2::vars))].
-
-let rec head (A:Type) l on l ≝
- match l with
- [ nil ⇒ None A
- | (cons (x:A) l2) ⇒ Some A x].
-
-let rec nth n l on n ≝
- match n with
- [ O ⇒ match l with
- [ nil ⇒ O
- | (cons x l2) ⇒ x]
- | (S n2) ⇒ (nth n2 (tail ? l))].
-
-definition max_list : (list nat) \to nat \def
- \lambda l.let rec aux l0 m on l0 \def
- match l0 with
- [ nil ⇒ m
- | (cons n l2) ⇒ (aux l2 (max m n))]
- in aux l O.
-
-let rec decodetype T vars C on T \def
- match T with
- [ TVar n ⇒ TName (nth n vars)
- | TFree x ⇒ TName x
- | Top ⇒ NTop
- | Arrow T1 T2 ⇒ NArrow (decodetype T1 vars C) (decodetype T2 vars C)
- | Forall T1 T2 ⇒ NForall (S (max_list (vars@C))) (decodetype T1 vars C)
- (decodetype T2 ((S (max_list (vars@C)))::vars) C)].
-
-definition sublist: \forall A:Type.(list A) \to (list A) \to Prop \def
- \lambda A,l1,l2.\forall x.(in_list ? x l1) \to (in_list ? x l2).
-
-let rec remove_nat (x:nat) (l:list nat) on l \def
- match l with
- [ nil ⇒ (nil nat)
- | (cons y l2) ⇒ match (eqb x y) with
- [ true ⇒ (remove_nat x l2)
- | false ⇒ (y :: (remove_nat x l2)) ]].
let rec fv_NTyp (T:NTyp):list nat\def
match T with
| false ⇒ (NForall Z (subst_NTyp_var U X Y)
(subst_NTyp_var V X Y))]].
+definition filter_ntypes : list nbound → list nbound ≝
+ λG.(filter ? G (λB.match B with [mk_nbound B X T ⇒ B])).
+
definition fv_Nenv : list nbound → list nat ≝
- map nbound nat
+ λG.map nbound nat
(λb.match b with
- [mk_nbound (B:bool) (X:nat) (T:NTyp) ⇒ X]).
+ [mk_nbound (B:bool) (X:nat) (T:NTyp) ⇒ X]) (filter_ntypes G).
inductive NWFType : (list nbound) → NTyp → Prop ≝
- | NWFT_TName : ∀X,G.(in_list ? X (fv_Nenv G))
+ | NWFT_TName : ∀X,G.(X ∈ (fv_Nenv G))
→ (NWFType G (TName X))
| NWFT_Top : ∀G.(NWFType G NTop)
| 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.¬(in_list ? Y (fv_Nenv G)) →
- (Y = X ∨ ¬(in_list ? 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)).
inductive NWFEnv : (list nbound) → Prop ≝
| NWFE_Empty : (NWFEnv (nil ?))
| NWFE_cons : ∀B,X,T,G.(NWFEnv G) →
- ¬(in_list ? X (fv_Nenv G)) →
+ X ∉ (fv_Nenv G) →
(NWFType G T) → (NWFEnv ((mk_nbound B X T) :: G)).
inductive NJSubtype : (list nbound) → NTyp → NTyp → Prop ≝
| NSA_Top : ∀G,T.(NWFEnv G) → (NWFType G T) → (NJSubtype G T NTop)
| NSA_Refl_TVar : ∀G,X.(NWFEnv G)
- → (in_list ? X (fv_Nenv G))
+ → X ∈ (fv_Nenv G)
→ (NJSubtype G (TName X) (TName X))
| NSA_Trans_TVar : ∀G,X,T,U.
- (in_list ? (mk_nbound true X U) G) →
+ (mk_nbound true X U) ∈ G →
(NJSubtype G U T) → (NJSubtype G (TName X) T)
| 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,Y,S1,S2,T1,T2.
- (NWFType G (NForall X S1 S2)) \to
- (NWFType G (NForall Y T1 T2)) \to
(NJSubtype G T1 S1) →
- (∀Z.¬(in_list ? 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
+ (∀Z.Z ∉ (fv_Nenv G) →
+ (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))
- | NSA_alpha : ∀G,T1,T2,U1,U2.(NJSubtype G T1 U1) →
- (alpha_eq T1 T2) →
- (alpha_eq U1 U2) →
- (NJSubtype G T2 U2).
+ (NJSubtype G (NForall X S1 S2) (NForall Y T1 T2)).
-let rec nt_len T \def
+let rec nt_len T ≝
match T with
[ TName X ⇒ O
| NTop ⇒ O
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
- |rewrite < H;elim a;simplify;reflexivity]
+ |elim a;elim b;simplify;rewrite < H;reflexivity]
qed.
lemma decidable_eq_Typ : ∀T,U:Typ.decidable (T = U).
|right;intro;destruct H1;elim H;reflexivity]
qed.
-lemma in_Nenv_to_in_env: ∀l,n,n2.in_list ? (mk_nbound true n n2) l →
- in_list ? (mk_bound true n (encodetype n2 [])) (encodeenv l).
+lemma in_Nenv_to_in_env: ∀l,n,n2.(mk_nbound true n n2) ∈ l →
+ (mk_bound true n (encodetype n2 [])) ∈ (encodeenv l).
intros 3;elim l
[elim (not_in_list_nil ? ? H)
|inversion H1;intros;destruct;
|elim a;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;elim H;simplify
- [rewrite > eqb_n_n;reflexivity
- |rewrite > H2;elim (eqb a a1);reflexivity]
-qed.
-
-lemma lookup_in : \forall x,l.(lookup x l = true) \to (in_list ? x l).
-intros 2;elim l
- [simplify in H;destruct H
- |generalize in match H1;simplify;elim (decidable_eq_nat x a)
- [applyS in_list_head
- |apply in_list_cons;apply H;
- rewrite > (not_eq_to_eqb_false ? ? H2) in H3;simplify in H3;assumption]]
-qed.
-
-lemma posn_length : \forall x,vars.(in_list ? x vars) \to
- (posn vars x) < (length ? vars).
-intros 2;elim vars
- [elim (not_in_list_nil ? ? H)
- |inversion H1;intros;destruct;simplify
- [rewrite > eqb_n_n;simplify;
- apply lt_O_S
- |elim (eqb x a);simplify
- [apply lt_O_S
- |apply le_S_S;apply H;assumption]]]
-qed.
-
-lemma in_remove : \forall a,b,l.(a \neq b) \to (in_list ? a l) \to
- (in_list ? a (remove_nat b l)).
-intros 4;elim l
- [elim (not_in_list_nil ? ? H1)
- |inversion H2;intros;destruct;simplify
- [rewrite > not_eq_to_eqb_false
- [simplify;apply in_list_head
- |intro;apply H;symmetry;assumption]
- |elim (eqb b a1);simplify
- [apply H1;assumption
- |apply in_list_cons;apply H1;assumption]]]
-qed.
-
lemma NTyp_len_ind : \forall P:NTyp \to Prop.
(\forall U.(\forall V.((nt_len V) < (nt_len U)) \to (P V))
\to (P U))
|*:autobatch paramodulation]
qed.
-lemma swap_same : \forall x,y.swap x x y = y.
-intros;elim (decidable_eq_nat y x)
- [autobatch paramodulation
- |rewrite > swap_other;autobatch]
-qed.
-
-lemma not_nat_in_to_lookup_false : ∀l,X.¬(in_list ? X l) → lookup X l = false.
-intros 2;elim l;simplify
- [reflexivity
- |elim (decidable_eq_nat X a)
- [elim H1;rewrite > H2;apply in_list_head
- |rewrite > (not_eq_to_eqb_false ? ? H2);simplify;apply H;intro;apply H1;
- apply (in_list_cons ? ? ? ? H3);]]
-qed.
-
lemma fv_encode : ∀T,l1,l2.
- (∀x.(in_list ? x (fv_NTyp T)) →
+ (∀x.x ∈ (fv_NTyp T) →
(lookup x l1 = lookup x l2 ∧
(lookup x l1 = true → posn l1 x = posn l2 x))) →
(encodetype T l1 = encodetype T l2).
intro;elim T
[simplify in H;elim (H n)
- [simplify;rewrite < H1;generalize in match H2;elim (lookup n l1);simplify
- [rewrite > H3;autobatch
+ [simplify;rewrite < H1;elim (lookup n l1) in H2;simplify
+ [rewrite > H2;autobatch
|reflexivity]
|apply in_list_head]
|simplify;reflexivity
|intros;apply H2;simplify;apply in_list_to_in_list_append_l;autobatch]]
qed.
-lemma lookup_swap : ∀a,b,x,vars.
- lookup (swap a b x) (swap_list a b vars) =
- lookup x vars.
-intros 4;elim vars;simplify
- [reflexivity
- |elim (decidable_eq_nat x a1)
- [rewrite > H1;rewrite > eqb_n_n;rewrite > eqb_n_n;simplify;reflexivity
- |rewrite > (not_eq_to_eqb_false ? ? H1);elim (decidable_eq_nat x a)
- [rewrite > H;rewrite > H2;rewrite > swap_left;
- elim (decidable_eq_nat b a1)
- [rewrite < H3;rewrite > swap_right;
- rewrite > (not_eq_to_eqb_false b a)
- [reflexivity
- |intro;autobatch]
- |rewrite > (swap_other a b a1)
- [rewrite > (not_eq_to_eqb_false ? ? H3);simplify;reflexivity
- |*:intro;autobatch]]
- |elim (decidable_eq_nat x b)
- [rewrite > H;rewrite > H3;rewrite > swap_right;
- elim (decidable_eq_nat a1 a)
- [rewrite > H4;rewrite > swap_left;
- rewrite > (not_eq_to_eqb_false a b)
- [reflexivity
- |intro;autobatch]
- |rewrite > (swap_other a b a1)
- [rewrite > (not_eq_to_eqb_false a a1)
- [reflexivity
- |intro;autobatch]
- |assumption
- |intro;autobatch]]
- |rewrite > H;rewrite > (swap_other a b x)
- [elim (decidable_eq_nat a a1)
- [rewrite > H4;rewrite > swap_left;
- rewrite > (not_eq_to_eqb_false ? ? H3);reflexivity
- |elim (decidable_eq_nat b a1)
- [rewrite > H5;rewrite > swap_right;
- rewrite > (not_eq_to_eqb_false ? ? H2);reflexivity
- |rewrite > (swap_other a b a1)
- [rewrite > (not_eq_to_eqb_false ? ? H1);reflexivity
- |*:intro;autobatch]]]
- |*:assumption]]]]]
-qed.
-
-lemma posn_swap : ∀a,b,x,vars.
- posn vars x = posn (swap_list a b vars) (swap a b x).
-intros 4;elim vars;simplify
- [reflexivity
- |rewrite < H;elim (decidable_eq_nat x a1)
- [rewrite > H1;do 2 rewrite > eqb_n_n;reflexivity
- |elim (decidable_eq_nat (swap a b x) (swap a b a1))
- [elim H1;autobatch
- |rewrite > (not_eq_to_eqb_false ? ? H1);
- rewrite > (not_eq_to_eqb_false ? ? H2);reflexivity]]]
-qed.
-
theorem encode_swap : ∀a,x,T,vars.
- ((in_list ? a (fv_NTyp T)) → (in_list ? a vars)) →
- (in_list ? x vars) →
+ (a ∈ (fv_NTyp T) → a ∈ vars) →
+ x ∈ vars →
encodetype T vars =
encodetype (swap_NTyp a x T) (swap_list a x vars).
intros 3;elim T
qed.
lemma encode_swap2 : ∀a:nat.∀x:nat.∀T:NTyp.
- ¬(in_list ? a (fv_NTyp T)) →
- ∀vars.in_list ? x vars
- →encodetype T vars=encodetype (swap_NTyp a x T) (swap_list a x vars).
+ a ∉ (fv_NTyp T) →
+ ∀vars.x ∈ vars
+ → encodetype T vars=encodetype (swap_NTyp a x T) (swap_list a x vars).
intros;apply (encode_swap ? ? ? ? ? H1);intro;elim (H H2);
qed.
-lemma remove_inlist : \forall x,y,l.(in_list ? x (remove_nat y l)) \to
- (in_list ? x l) \land x \neq y.
-intros 3;elim l 0;simplify;intro
- [elim (not_in_list_nil ? ? H)
- |elim (decidable_eq_nat y a)
- [rewrite > H in H2;rewrite > eqb_n_n in H2;simplify in H2;
- rewrite > H in H1;elim (H1 H2);rewrite > H;split
- [apply in_list_cons;assumption
- |assumption]
- |rewrite > (not_eq_to_eqb_false ? ? H) in H2;simplify in H2;
- inversion H2;intros;destruct;
- [split;autobatch
- |elim (H1 H3);split;autobatch]]]
-qed.
-
-lemma inlist_remove : ∀x,y,l.(in_list ? x l → x \neq y →
- (in_list ? x (remove_nat y l))).
-intros 3;elim l
- [elim (not_in_list_nil ? ? H);
- |simplify;elim (decidable_eq_nat y a)
- [rewrite > (eq_to_eqb_true ? ? H3);simplify;apply H
- [inversion H1;intros;destruct;
- [elim H2;reflexivity
- |assumption]
- |assumption]
- |rewrite > (not_eq_to_eqb_false ? ? H3);simplify;
- inversion H1;intros;destruct;autobatch]]
-qed.
-
-lemma incl_fv_var : \forall T.(incl ? (fv_NTyp T) (var_NTyp T)).
+lemma incl_fv_var : \forall T.(fv_NTyp T) ⊆ (var_NTyp T).
intro;elim T;simplify;unfold;intros
[1,2:assumption
|elim (in_list_append_to_or_in_list ? ? ? ? H2);autobatch
qed.
lemma fv_encode2 : ∀T,l1,l2.
- (∀x.(in_list ? x (fv_NTyp T)) →
+ (∀x.x ∈ (fv_NTyp T) →
(lookup x l1 = lookup x l2 ∧
posn l1 x = posn l2 x)) →
(encodetype T l1 = encodetype T l2).
[assumption|intro;assumption]
qed.
-lemma alpha_sym : \forall S,T.(alpha_eq S T) \to (alpha_eq T S).
-intros;elim H
- [apply A_refl
- |apply A_arrow;assumption
- |apply A_forall
- [assumption
- |intros;apply H4;intro;apply H5;elim (decidable_eq_nat Z n5)
- [rewrite > H7;apply in_list_head
- |apply in_list_cons;inversion H6;intros;destruct;
- [apply in_list_head
- |apply in_list_cons;inversion H8;intros;destruct;
- [elim H7;reflexivity
- |elim (in_list_append_to_or_in_list ? ? ? ? H10);autobatch]]]]]
-qed.
-
-(*legacy*)
-lemma nat_in_list_case :∀G,H,n.in_list nat n (H@G) →
- in_list nat n G ∨ in_list nat n H.
-intros;elim (in_list_append_to_or_in_list ???? H1)
-[right;assumption
-|left;assumption]
-qed.
-
lemma inlist_fv_swap : ∀x,y,b,T.
- (¬ in_list ? b (y::var_NTyp T)) →
- in_list ? x (fv_NTyp (swap_NTyp b y T)) →
- x ≠ y ∧ (x = b ∨ (in_list ? x (fv_NTyp T))).
+ b ∉ (y::var_NTyp T) →
+ x ∈ (fv_NTyp (swap_NTyp b y T)) →
+ x ≠ y ∧ (x = b ∨ x ∈ (fv_NTyp T)).
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;
|elim H6
[left;assumption
|right;apply in_list_to_in_list_append_r;assumption]]
- |intro;apply H2;elim (nat_in_list_case (var_NTyp n1) [y] ? H5)
- [apply (in_list_to_in_list_append_r ? ? (y::var_NTyp n) (var_NTyp n1));
- assumption
- |inversion H6;intros;destruct;
- [apply in_list_head
- |elim (not_in_list_nil ? ? H7)]]
+ |intro;apply H2;elim (in_list_append_to_or_in_list ?? [y] (var_NTyp n1) H5)
+ [lapply (in_list_singleton_to_eq ??? H6);applyS in_list_head
+ |autobatch]
|assumption]]
|simplify;simplify in H3;simplify in H2;elim (in_list_append_to_or_in_list ? ? ? ? H3)
[elim H
qed.
lemma inlist_fv_swap_r : ∀x,y,b,T.
- (¬(in_list ? b (y::var_NTyp T))) →
- ((x = b ∧ (in_list ? y (fv_NTyp T))) ∨
- (x \neq y ∧ (in_list ? x (fv_NTyp T)))) →
- (in_list ? x (fv_NTyp (swap_NTyp b y T))).
+ (b ∉ (y::var_NTyp T)) →
+ ((x = b ∧ y ∈ (fv_NTyp T)) ∨
+ (x ≠ y ∧ x ∈ (fv_NTyp T))) →
+ x ∈ (fv_NTyp (swap_NTyp b y T)).
intros 4;elim T
[simplify;simplify in H;simplify in H1;cut (b ≠ n)
[elim H1
|change in ⊢ (???%) with ((y::n::var_NTyp n1)@var_NTyp n2);autobatch]]
|intro;apply H2;inversion H4;simplify;intros;destruct;autobatch depth=4]]
qed.
-
-lemma fv_alpha : ∀S,T.alpha_eq S T → incl ? (fv_NTyp S) (fv_NTyp T).
-intros;elim H;simplify;unfold;intros
- [assumption
- |elim (in_list_append_to_or_in_list ? ? ? ? H5);autobatch
- |elim (in_list_append_to_or_in_list ? ? ? ? H5)
- [autobatch
- |elim (fresh_name (n4::n5::var_NTyp n1@var_NTyp n3));
- apply in_list_to_in_list_append_r;
- lapply (H4 ? H7);
- elim (remove_inlist ? ? ? H6);apply inlist_remove
- [lapply (inlist_fv_swap_r x n4 a n1)
- [elim (inlist_fv_swap x n5 a n3)
- [elim H11
- [rewrite < H12 in H7;elim H7;autobatch depth=5;
- |assumption]
- |intro;apply H7;inversion H10;intros;destruct;autobatch depth=4
- |autobatch]
- |intro;apply H7;inversion H10;intros;destruct;autobatch depth=4
- |right;split;assumption]
- |intros;intro;lapply (inlist_fv_swap_r x n4 a n1)
- [lapply (Hletin ? Hletin1);elim (inlist_fv_swap x n5 a n3 ? Hletin2)
- [apply (H11 H10)
- |intro;apply H7;elim (decidable_eq_nat a n4)
- [rewrite > H12;apply in_list_head
- |apply in_list_cons;inversion H11;intros;destruct;autobatch]]
- |intro;apply H7;inversion H11;intros;destruct;autobatch depth=4
- |right;split;assumption]]]]
-qed.
-
-theorem alpha_to_encode : ∀S,T.alpha_eq S T →
- ∀vars.encodetype S vars = encodetype T vars.
-intros 3;elim H
-[reflexivity
-|simplify;rewrite > H2;rewrite > H4;reflexivity
-|simplify;rewrite > H2;
- cut (encodetype n1 (n4::vars) = encodetype n3 (n5::vars))
- [rewrite > Hcut;reflexivity
- |elim (fresh_name (n4::n5::var_NTyp n1@var_NTyp n3));
- lapply (encode_swap2 a n4 n1 ? (n4::vars))
- [intro;apply H5;autobatch depth=5
- |lapply (encode_swap2 a n5 n3 ? (n5::vars))
- [intro;autobatch depth=5
- |rewrite > Hletin;rewrite > Hletin1;simplify;rewrite > swap_right;
- rewrite > swap_right;rewrite > (H4 a H5 (a::swap_list a n4 vars));
- rewrite > (fv_encode2 ? ? (a::swap_list a n5 vars))
- [reflexivity
- |intros;elim (decidable_eq_nat n4 n5)
- [autobatch
- |cut ((x ≠ n4) ∧ (x ≠ n5))
- [elim Hcut;elim (decidable_eq_nat x a);simplify
- [rewrite > (eq_to_eqb_true ? ? H10);simplify;autobatch
- |rewrite > (not_eq_to_eqb_false ? ? H10);simplify;elim vars;simplify
- [autobatch
- |elim H11;rewrite < H12;rewrite > H13;elim (decidable_eq_nat a a1)
- [rewrite > H14;do 2 rewrite > swap_left;
- rewrite > (not_eq_to_eqb_false ? ? H8);
- rewrite > (not_eq_to_eqb_false ? ? H9);simplify;autobatch
- |elim (decidable_eq_nat n4 a1)
- [rewrite > H15;rewrite > swap_right;rewrite > (swap_other a n5 a1)
- [rewrite > (not_eq_to_eqb_false ? ? H10);rewrite < H15;
- rewrite > (not_eq_to_eqb_false ? ? H8);autobatch
- |intro;autobatch
- |intro;autobatch]
- |rewrite > (swap_other a n4 a1);elim (decidable_eq_nat n5 a1)
- [rewrite < H16;rewrite > swap_right;
- rewrite > (not_eq_to_eqb_false ? ? H9);
- rewrite > (not_eq_to_eqb_false ? ? H10);autobatch
- |rewrite > (swap_other a n5 a1);try intro;autobatch
- |*:intro;autobatch]]]]]
- |split
- [lapply (H3 ? H5);lapply (alpha_sym ? ? Hletin2);
- lapply (fv_alpha ? ? Hletin3);lapply (Hletin4 ? H6);
- elim (inlist_fv_swap ? ? ? ? ? Hletin5)
- [assumption
- |intro;apply H5;inversion H8;intros;destruct;autobatch depth=4]
- |elim (inlist_fv_swap ? ? ? ? ? H6)
- [assumption
- |intro;apply H5;elim (decidable_eq_nat a n4)
- [applyS in_list_head
- |apply in_list_cons;inversion H8;intros;destruct;autobatch]]]]]]
- |apply in_list_head]
- |apply in_list_head]]]
-qed.
lemma encode_append : ∀T,U,n,l.length ? l ≤ n →
subst_type_nat (encodetype T l) U n = encodetype T l.
|intro;rewrite > H2 in Hletin1;unfold in Hletin1;autobatch]
|cut (lookup n l = false)
[rewrite > Hcut;reflexivity
- |generalize in match H1;elim (lookup n l);
- [elim H2;reflexivity|reflexivity]]]
+ |elim (lookup n l) in H1;
+ [elim H1;reflexivity|reflexivity]]]
|reflexivity
|autobatch
|rewrite > (H ? ? H2);rewrite > H1;
encodetype T l = subst_type_nat (encodetype T (l@[X])) (TFree X) (length ? l).
intros 2;elim T;simplify
[cut (lookup n l = true → posn l n = posn (l@[X]) n)
- [generalize in match Hcut;elim (bool_to_decidable_eq (lookup n l) true)
+ [elim (bool_to_decidable_eq (lookup n l) true) in Hcut
[cut (lookup n (l@[X]) = true)
- [rewrite > H;rewrite > Hcut1;simplify;
+ [rewrite > H;rewrite > Hcut;simplify;
cut (eqb (posn (l@[X]) n) (length nat l) = false)
- [rewrite > Hcut2;simplify;rewrite < (H1 H);reflexivity
- |generalize in match H;elim l 0
- [simplify;intro;destruct H2
+ [rewrite > Hcut1;simplify;rewrite < (H1 H);reflexivity
+ |elim l in H 0
+ [simplify;intro;destruct
|intros 2;simplify;elim (eqb n a);simplify
[reflexivity
- |simplify in H3;apply (H2 H3)]]]
- |generalize in match H;elim l
- [simplify in H2;destruct H2
- |generalize in match H3;simplify;elim (eqb n a) 0;simplify;intro
+ |simplify in H3;apply (H H2)]]]
+ |elim l in H
+ [simplify in H;destruct
+ |generalize in match H2;simplify;elim (eqb n a) 0;simplify;intro
[reflexivity
- |apply (H2 H4)]]]
+ |apply (H H3)]]]
|cut (lookup n l = false)
[elim (decidable_eq_nat n X)
- [rewrite > Hcut1;rewrite > H2;cut (lookup X (l@[X]) = true)
- [rewrite > Hcut2;simplify;cut (eqb (posn (l@[X]) X) (length nat l) = true)
- [rewrite > Hcut3;simplify;reflexivity
- |generalize in match Hcut1;elim l 0
+ [rewrite > Hcut;rewrite > H2;cut (lookup X (l@[X]) = true)
+ [rewrite > Hcut1;simplify;cut (eqb (posn (l@[X]) X) (length nat l) = true)
+ [rewrite > Hcut2;simplify;reflexivity
+ |elim l in Hcut 0
[intros;simplify;rewrite > eqb_n_n;simplify;reflexivity
|simplify;intros 2;rewrite > H2;elim (eqb X a);simplify in H4
- [destruct H4
+ [destruct
|apply (H3 H4)]]]
|elim l;simplify
[rewrite > eqb_n_n;reflexivity
[reflexivity
|assumption]]]
|cut (lookup n l = lookup n (l@[X]))
- [rewrite < Hcut2;rewrite > Hcut1;simplify;reflexivity
+ [rewrite < Hcut1;rewrite > Hcut;simplify;reflexivity
|elim l;simplify
[rewrite > (not_eq_to_eqb_false ? ? H2);simplify;reflexivity
|elim (eqb n a);simplify
[reflexivity
|assumption]]]]
- |generalize in match H;elim (lookup n l);
- [elim H2;reflexivity|reflexivity]]]
+ |elim (lookup n l) in H
+ [elim H;reflexivity|reflexivity]]]
|elim l 0
- [intro;simplify in H;destruct H
+ [intro;simplify in H;destruct
|simplify;intros 2;elim (eqb n a);simplify
[reflexivity
|simplify in H1;rewrite < (H H1);reflexivity]]]
rewrite < (H1 ([n]@l));reflexivity]
qed.
-lemma encode_subst : ∀T,X,Y,l.¬(in_list ? X l) → ¬(in_list ? Y l) →
- (in_list ? X (fv_NTyp T) → X = Y) →
+lemma encode_subst : ∀T,X,Y,l.X ∉ l → Y ∉ l →
+ (X ∈ (fv_NTyp T) → X = Y) →
encodetype (swap_NTyp X Y T) l =
subst_type_nat (encodetype T (l@[Y])) (TFree X) (length ? l).
apply NTyp_len_ind;intro;elim U
[simplify;rewrite > Hcut;rewrite > (not_nat_in_to_lookup_false ? ? H2);
simplify;cut (posn (l@[Y]) Y = length ? l)
[rewrite > Hcut1;rewrite > eqb_n_n;reflexivity
- |generalize in match H2;elim l;simplify
+ |elim l in H2;simplify
[rewrite > eqb_n_n;reflexivity
|elim (decidable_eq_nat Y a)
- [elim H6;rewrite > H7;apply in_list_head
- |rewrite > (not_eq_to_eqb_false ? ? H7);simplify;rewrite < H5
+ [elim H5;rewrite > H6;apply in_list_head
+ |rewrite > (not_eq_to_eqb_false ? ? H6);simplify;rewrite < H2
[reflexivity
|intro;autobatch]]]]
|elim l;simplify
cut (lookup Y (l@[Y]) = true)
[rewrite > Hcut;simplify;cut (posn (l@[Y]) Y = length ? l)
[rewrite > Hcut1;rewrite > eqb_n_n;reflexivity
- |generalize in match H2;elim l;simplify
+ |elim l in H2;simplify
[rewrite > eqb_n_n;reflexivity
|elim (decidable_eq_nat Y a)
- [elim H7;rewrite > H8;apply in_list_head
- |rewrite > (not_eq_to_eqb_false ? ? H8);simplify;rewrite < H6
+ [elim H6;applyS in_list_head
+ |rewrite > (not_eq_to_eqb_false ? ? H7);simplify;rewrite < H2
[reflexivity
|intro;autobatch]]]]
|elim l;simplify
|simplify;rewrite > (swap_other X Y n)
[cut (lookup n l = lookup n (l@[Y]) ∧
(lookup n l = true → posn l n = posn (l@[Y]) n))
- [elim Hcut;rewrite > H6;generalize in match H7;
- generalize in match H6;elim (lookup n (l@[Y]));simplify;
- [rewrite < H9;generalize in match H8;elim l
- [simplify in H10;destruct H10;
+ [elim Hcut;rewrite > H6;elim (lookup n (l@[Y])) in H7 H6;simplify;
+ [rewrite < H7;elim l in H6
+ [simplify in H6;destruct
|elim (decidable_eq_nat n a);simplify
- [rewrite > (eq_to_eqb_true ? ? H12);reflexivity
- |rewrite > (not_eq_to_eqb_false ? ? H12);
- simplify;generalize in match H10;elim (eqb (posn l1 n) (length nat l1))
- [simplify in H13;simplify in H11;
- rewrite > (not_eq_to_eqb_false ? ? H12) in H11;
- simplify in H11;lapply (H13 H11);destruct Hletin
+ [rewrite > (eq_to_eqb_true ? ? H9);reflexivity
+ |rewrite > (not_eq_to_eqb_false ? ? H9);
+ simplify;elim (eqb (posn l1 n) (length nat l1)) in H6
+ [simplify in H8;simplify in H6;
+ rewrite > (not_eq_to_eqb_false ? ? H9) in H8;
+ simplify in H8;lapply (H6 H8);destruct
|reflexivity]]
|*:assumption]
|reflexivity]
|intro;apply H5;simplify;autobatch]
|simplify;rewrite < (H2 n1 ? ? ? ? H3 H4)
[cut (l = swap_list X Y l)
- [|generalize in match H3;generalize in match H4;elim l;simplify
+ [|elim l in H3 H4;simplify
[reflexivity
|elim (decidable_eq_nat a X)
- [elim H8;rewrite > H9;apply in_list_head
+ [elim H4;applyS in_list_head
|elim (decidable_eq_nat a Y)
- [elim H7;rewrite > H10;apply in_list_head
+ [elim H6;applyS in_list_head
|rewrite > (swap_other X Y a)
- [rewrite < H6
+ [rewrite < H3
[reflexivity
|*:intro;autobatch]
|*:assumption]]]]]
|intro;apply H5;simplify;autobatch]]
qed.
-lemma swap_case: ∀u,v,x.(swap u v x) = u ∨ (swap u v x) = v ∨ (swap u v x = x).
-intros;unfold in match swap;simplify;elim (eqb x u);simplify
- [autobatch
- |elim (eqb x v);simplify;autobatch]
-qed.
-
-lemma in_fvNTyp_in_fvNenv : ∀G,T.(NWFType G T) → (incl ? (fv_NTyp T) (fv_Nenv G)).
+lemma in_fvNTyp_in_fvNenv : ∀G,T.(NWFType G T) → (fv_NTyp T) ⊆ (fv_Nenv G).
intros;elim H;simplify;unfold;intros;
[inversion H2;intros;destruct;
[assumption
autobatch depth=5
|apply (in_remove ? ? ? H15 H16)]]
|simplify;simplify in H13;elim (remove_inlist ? ? ? H13);
- elim (nat_in_list_case ? ? ? H14);
- [apply in_list_to_in_list_append_r;apply in_remove;
+ elim (in_list_append_to_or_in_list ???? H14)
+ [apply in_list_to_in_list_append_l;apply H10;
+ [rewrite < (associative_append ? [x] (fv_Nenv l) (var_NTyp n4));
+ intro;apply H12;simplify;
+ rewrite < (associative_append ? [x] (fv_Nenv l) (n3::var_NTyp n4@var_NTyp n5));
+ elim (in_list_append_to_or_in_list ???? H17);autobatch depth=4
+ |autobatch]
+ |apply in_list_to_in_list_append_r;apply in_remove;
[elim (remove_inlist ? ? ? H16);intro;apply H18;
elim (swap_case a n n3)
[elim H20
[rewrite < (associative_append ? [x] (fv_Nenv l) (var_NTyp n5));
intro;apply H12;simplify;
rewrite < (associative_append ? [x] (fv_Nenv l) (n3::var_NTyp n4 @ var_NTyp n5));
- elim (nat_in_list_case ? ? ? H17);autobatch depth=4
- |elim (remove_inlist ? ? ? H16);autobatch]]
- |apply in_list_to_in_list_append_l;apply H10;
- [rewrite < (associative_append ? [x] (fv_Nenv l) (var_NTyp n4));
- intro;apply H12;simplify;
- rewrite < (associative_append ? [x] (fv_Nenv l) (n3::var_NTyp n4@var_NTyp n5));
- elim (nat_in_list_case ? ? ? H17);autobatch depth=4
- |autobatch]]]]
+ elim (in_list_append_to_or_in_list ???? H17);autobatch depth=4
+ |elim (remove_inlist ? ? ? H16);autobatch]]]]]
|split
[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.(in_list ? X (fv_NTyp T)) → ¬(in_list ? X l) →
- (in_list ? X (fv_type (encodetype T l))).
+lemma fv_NTyp_fv_Typ : ∀T,X,l.X ∈ (fv_NTyp T) → X ∉ l →
+ X ∈ (fv_type (encodetype T l)).
intros 2;elim T;simplify
[simplify in H;cut (X = n)
[rewrite < Hcut;generalize in match (lookup_in X l);elim (lookup 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]))
|*:apply not_in_list_nil]]]
qed.
-lemma not_in_list_encodetype : \forall T,l,x.in_list ? x l \to
- \lnot (in_list ? x (fv_type (encodetype T l))).
+lemma not_in_list_encodetype : \forall T,l,x.x ∈ l \to
+ \lnot x ∈ (fv_type (encodetype T l)).
intro;elim T;simplify
[apply (bool_elim ? (lookup n l));intro;simplify
[apply not_in_list_nil
[rewrite > (in_lookup ? ? H) in H1;destruct H1
|apply (not_in_list_nil ? ? H3)]]
|apply not_in_list_nil
- |intro;elim (nat_in_list_case ? ? ? H3);autobatch
- |intro;elim (nat_in_list_case ? ? ? H3);
- [apply (H1 (n::l) x ? H4);apply in_list_cons;assumption
- |autobatch]]
+ |intro;elim (in_list_append_to_or_in_list ???? H3);autobatch
+ |intro;elim (in_list_append_to_or_in_list ???? H3);
+ [autobatch
+ |apply (H1 (n::l) x ? H4);apply in_list_cons;assumption]]
qed.
-lemma incl_fv_encode_fv : \forall T,l.incl ? (fv_type (encodetype T l)) (fv_NTyp T).
+lemma incl_fv_encode_fv : \forall T,l.(fv_type (encodetype T l)) ⊆ (fv_NTyp T).
intro;elim T;simplify;unfold;
[intro;elim (lookup n l);simplify in H
[elim (not_in_list_nil ? ? H)
|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).
intros;elim H;simplify;autobatch;
qed.
-lemma NWFT_env_incl : ∀G,T.NWFType G T → ∀H.incl ? (fv_Nenv G) (fv_Nenv H)
+lemma NWFT_env_incl : ∀G,T.NWFType G T → ∀H.(fv_Nenv G) ⊆ (fv_Nenv H)
→ NWFType H T.
intros 3;elim H
[4:apply NWFT_Forall
|intros;apply (H4 ? ? H8);
[intro;apply H7;apply (H6 ? H9)
|unfold;intros;simplify;simplify in H9;inversion H9;intros;
- destruct;autobatch]]
+ destruct;simplify;
+ [autobatch
+ |apply in_list_cons;apply H6;apply H10]]]
|*: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;autobatch]]
- |assumption]
- |elim H2;elim H4;split;autobatch
- |split;assumption
- |elim H2;split
- [lapply (adeq_WFT ? ? H5);autobatch;
- |lapply (adeq_WFT ? ? H6);autobatch]]
+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;lapply (in_remove ? ? ? H10 H11);elim H7;
- autobatch]
+ [assumption
+ |elim H5;autobatch depth=5]
|elim (decidable_eq_nat X n1)
- [left;assumption
- |right;intro;lapply (in_remove ? ? ? H10 H11);elim H7;
- autobatch]]
- |2,3:apply not_in_list_nil
- |intro;elim (NJSubtype_to_NWFT ? ? ? Hletin);
- lapply (in_fvNTyp_in_fvNenv ? ? H10);simplify in Hletin1;
+ [assumption
+ |elim H5;autobatch depth=5]]
+ |2,3:autobatch
+ |intro;elim (NJS_fv_to_fvNenv ? ? ? Hletin);
+ simplify in H8;
elim (decidable_eq_nat X n1)
[assumption
- |lapply (in_remove ? ? ? H11 H8);elim H7;autobatch]]
+ |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
- |lapply (in_remove ? ? ? H11 H8);elim H7;autobatch]]]
- |rewrite < (alpha_to_encode ? ? H3);rewrite < (alpha_to_encode ? ? H4);
- assumption]
+ |elim H5;autobatch depth=4]]]]
qed.
let rec closed_type T n ≝
| 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 ? (a::l1) O (S n1) ≠ nth ? (a::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; *)
- apply H4
- |simplify;autobatch
- |intro;elim (not_eq_O_S n1);symmetry;assumption]]]]
-qed.
-
-lemma nth_in_list : ∀l,n. n < length ? l → in_list ? (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
- |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
- |elim (eqb (nth nat l1 O n1) a);simplify;
- [reflexivity
- |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
+ (\forall x. x ∈ (fv_type T) \to x ∉ l) \to
∃U.T = encodetype U l.
intro;elim T
[simplify in H;apply (ex_intro ? ? (TName (nth ? l O n)));simplify;
|elim a in H6;simplify in H6;destruct H6;apply NWFE_cons;autobatch]]
qed.
-lemma xxx : \forall b,X,T,l.
+lemma in_list_encodeenv : \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.
+ (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 a 0;simplify;intros;destruct;
qed.
lemma eq_swap_NTyp_to_case :
- \forall X,Y,Z,T.\lnot in_list ? Y (X::var_NTyp T) \to
+ \forall X,Y,Z,T. 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).
+ Z = X \lor 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)
|rewrite > H3 in H2;rewrite < eq_fv_Nenv_fv_env in H2;assumption]
|intros;cut (T2 = TName n)
[|elim T2 in H5 0;simplify;intros;destruct;reflexivity]
- rewrite > Hcut;
- elim (decoder t1 O ? []);
- [rewrite > H4 in H1;rewrite > H7 in H1;elim (xxx ? ? ? ? H1);elim H8;
- autobatch
+ rewrite > Hcut;elim (decoder t1 O ? []);
+ [rewrite > H4 in H1;rewrite > H7 in H1;elim (in_list_encodeenv ???? H1);
+ elim H8;autobatch
|4:unfold;intros;simplify in H7;elim (not_le_Sn_O ? H7)
|*:autobatch]
|intros;cut (∃u,u1,u2,u3.T2 = NArrow u u1 ∧ U2 = NArrow u2 u3)
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