-
-(*** theorems about swaps ***)
-
-lemma fv_subst_type_nat : \forall x,T,y,n.(in_list ? x (fv_type T)) \to
- (in_list ? x (fv_type (subst_type_nat T (TFree y) n))).
-intros 3;elim T 0
- [intros;simplify in H;elim (in_list_nil ? ? H)
- |2,3:simplify;intros;assumption
- |*:intros;simplify in H2;elim (nat_in_list_case ? ? ? H2)
- [1,3:simplify;apply natinG_or_inH_to_natinGH;left;apply (H1 ? H3)
- |*:simplify;apply natinG_or_inH_to_natinGH;right;apply (H ? H3)]]
-qed.
-
-lemma fv_subst_type_O : \forall x,T,y.(in_list ? x (fv_type T)) \to
- (in_list ? x (fv_type (subst_type_O T (TFree y)))).
-intros;rewrite > subst_O_nat;apply (fv_subst_type_nat ? ? ? ? H);
-qed.
-
-lemma swap_Typ_inv : \forall u,v,T.(swap_Typ u v (swap_Typ u v T)) = T.
-intros;elim T
- [1,3:simplify;reflexivity
- |simplify;rewrite > swap_inv;reflexivity
- |*:simplify;rewrite > H;rewrite > H1;reflexivity]
-qed.
-
-lemma swap_Typ_not_free : \forall u,v,T.\lnot (in_list ? u (fv_type T)) \to
- \lnot (in_list ? v (fv_type T)) \to (swap_Typ u v T) = T.
-intros 3;elim T 0
- [1,3:intros;simplify;reflexivity
- |simplify;intros;cut (n \neq u \land n \neq v)
- [elim Hcut;rewrite > (swap_other ? ? ? H2 H3);reflexivity
- |split
- [unfold;intro;apply H;rewrite > H2;apply in_Base
- |unfold;intro;apply H1;rewrite > H2;apply in_Base]]
- |*:simplify;intros;cut ((\lnot (in_list ? u (fv_type t)) \land
- \lnot (in_list ? u (fv_type t1))) \land
- (\lnot (in_list ? v (fv_type t)) \land
- \lnot (in_list ? v (fv_type t1))))
- [1,3:elim Hcut;elim H4;elim H5;clear Hcut H4 H5;rewrite > (H H6 H8);
- rewrite > (H1 H7 H9);reflexivity
- |*:split
- [1,3:split;unfold;intro;apply H2;apply natinG_or_inH_to_natinGH;autobatch
- |*:split;unfold;intro;apply H3;apply natinG_or_inH_to_natinGH;autobatch]]]
-qed.
-
-lemma subst_type_nat_swap : \forall u,v,T,X,m.
- (swap_Typ u v (subst_type_nat T (TFree X) m)) =
- (subst_type_nat (swap_Typ u v T) (TFree (swap u v X)) m).
-intros 4;elim T
- [simplify;elim (eqb_case n m);rewrite > H;simplify;reflexivity
- |2,3:simplify;reflexivity
- |*:simplify;rewrite > H;rewrite > H1;reflexivity]
-qed.
-
-lemma subst_type_O_swap : \forall u,v,T,X.
- (swap_Typ u v (subst_type_O T (TFree X))) =
- (subst_type_O (swap_Typ u v T) (TFree (swap u v X))).
-intros 4;rewrite > (subst_O_nat (swap_Typ u v T));rewrite > (subst_O_nat T);
-apply subst_type_nat_swap;
-qed.
-
-lemma in_fv_type_swap : \forall u,v,x,T.((in_list ? x (fv_type T)) \to
- (in_list ? (swap u v x) (fv_type (swap_Typ u v T)))) \land
- ((in_list ? (swap u v x) (fv_type (swap_Typ u v T))) \to
- (in_list ? x (fv_type T))).
-intros;split
- [elim T 0
- [1,3:simplify;intros;elim (in_list_nil ? ? H)
- |simplify;intros;cut (x = n)
- [rewrite > Hcut;apply in_Base
- |inversion H
- [intros;lapply (inj_head_nat ? ? ? ? H2);rewrite > Hletin;
- reflexivity
- |intros;lapply (inj_tail ? ? ? ? ? H4);rewrite < Hletin in H1;
- elim (in_list_nil ? ? H1)]]
- |*:simplify;intros;elim (nat_in_list_case ? ? ? H2)
- [1,3:apply natinG_or_inH_to_natinGH;left;apply (H1 H3)
- |*:apply natinG_or_inH_to_natinGH;right;apply (H H3)]]
- |elim T 0
- [1,3:simplify;intros;elim (in_list_nil ? ? H)
- |simplify;intros;cut ((swap u v x) = (swap u v n))
- [lapply (swap_inj ? ? ? ? Hcut);rewrite > Hletin;apply in_Base
- |inversion H
- [intros;lapply (inj_head_nat ? ? ? ? H2);rewrite > Hletin;
- reflexivity
- |intros;lapply (inj_tail ? ? ? ? ? H4);rewrite < Hletin in H1;
- elim (in_list_nil ? ? H1)]]
- |*:simplify;intros;elim (nat_in_list_case ? ? ? H2)
- [1,3:apply natinG_or_inH_to_natinGH;left;apply (H1 H3)
- |*:apply natinG_or_inH_to_natinGH;right;apply (H H3)]]]
-qed.
-
-lemma lookup_swap : \forall x,u,v,T,B,G.(in_list ? (mk_bound B x T) G) \to
- (in_list ? (mk_bound B (swap u v x) (swap_Typ u v T)) (swap_Env u v G)).
-intros 6;elim G 0
- [intros;elim (in_list_nil ? ? H)
- |intro;elim t;simplify;inversion H1
- [intros;lapply (inj_head ? ? ? ? H3);rewrite < H2 in Hletin;
- destruct Hletin;rewrite > Hcut;rewrite > Hcut1;rewrite > Hcut2;
- apply in_Base
- |intros;lapply (inj_tail ? ? ? ? ? H5);rewrite < Hletin in H2;
- rewrite < H4 in H2;apply in_Skip;apply (H H2)]]
-qed.
-