-(*** definitions and theorems about swaps ***)
-
-definition swap : nat \to nat \to nat \to nat \def
- \lambda u,v,x.match (eqb x u) with
- [true \Rightarrow v
- |false \Rightarrow match (eqb x v) with
- [true \Rightarrow u
- |false \Rightarrow x]].
-
-lemma swap_left : \forall x,y.(swap x y x) = y.
-intros;unfold swap;rewrite > eqb_n_n;simplify;reflexivity;
-qed.
-
-lemma swap_right : \forall x,y.(swap x y y) = x.
-intros;unfold swap;elim (eq_eqb_case y x)
- [elim H;rewrite > H2;simplify;rewrite > H1;reflexivity
- |elim H;rewrite > H2;simplify;rewrite > eqb_n_n;simplify;reflexivity]
-qed.
-
-lemma swap_other : \forall x,y,z.(z \neq x) \to (z \neq y) \to (swap x y z) = z.
-intros;unfold swap;elim (eq_eqb_case z x)
- [elim H2;lapply (H H3);elim Hletin
- |elim H2;rewrite > H4;simplify;elim (eq_eqb_case z y)
- [elim H5;lapply (H1 H6);elim Hletin
- |elim H5;rewrite > H7;simplify;reflexivity]]
-qed.
-
-lemma swap_inv : \forall u,v,x.(swap u v (swap u v x)) = x.
-intros;unfold in match (swap u v x);elim (eq_eqb_case x u)
- [elim H;rewrite > H2;simplify;rewrite > H1;apply swap_right
- |elim H;rewrite > H2;simplify;elim (eq_eqb_case x v)
- [elim H3;rewrite > H5;simplify;rewrite > H4;apply swap_left
- |elim H3;rewrite > H5;simplify;apply (swap_other ? ? ? H1 H4)]]
-qed.
-
-lemma swap_inj : \forall u,v,x,y.(swap u v x) = (swap u v y) \to x = y.
-intros;unfold swap in H;elim (eq_eqb_case x u)
- [elim H1;elim (eq_eqb_case y u)
- [elim H4;rewrite > H5;assumption
- |elim H4;rewrite > H3 in H;rewrite > H6 in H;simplify in H;
- elim (eq_eqb_case y v)
- [elim H7;rewrite > H9 in H;simplify in H;rewrite > H in H8;
- lapply (H5 H8);elim Hletin
- |elim H7;rewrite > H9 in H;simplify in H;elim H8;symmetry;assumption]]
- |elim H1;elim (eq_eqb_case y u)
- [elim H4;rewrite > H3 in H;rewrite > H6 in H;simplify in H;
- elim (eq_eqb_case x v)
- [elim H7;rewrite > H9 in H;simplify in H;rewrite < H in H8;
- elim H2;assumption
- |elim H7;rewrite > H9 in H;simplify in H;elim H8;assumption]
- |elim H4;rewrite > H3 in H;rewrite > H6 in H;simplify in H;
- elim (eq_eqb_case x v)
- [elim H7;rewrite > H9 in H;elim (eq_eqb_case y v)
- [elim H10;rewrite > H11;assumption
- |elim H10;rewrite > H12 in H;simplify in H;elim H5;symmetry;
- assumption]
- |elim H7;rewrite > H9 in H;elim (eq_eqb_case y v)
- [elim H10;rewrite > H12 in H;simplify in H;elim H2;assumption
- |elim H10;rewrite > H12 in H;simplify in H;assumption]]]]
-qed.
-
-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)
- |simplify;intros;assumption
- |simplify;intros;assumption
- |intros;simplify in H2;elim (nat_in_list_case ? ? ? H2)
- [simplify;apply natinG_or_inH_to_natinGH;left;apply (H1 ? H3)
- |simplify;apply natinG_or_inH_to_natinGH;right;apply (H ? H3)]
- |intros;simplify in H2;elim (nat_in_list_case ? ? ? H2)
- [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.
-
-let rec swap_Typ u v T on T \def
- match T with
- [(TVar n) \Rightarrow (TVar n)
- |(TFree X) \Rightarrow (TFree (swap u v X))
- |Top \Rightarrow Top
- |(Arrow T1 T2) \Rightarrow (Arrow (swap_Typ u v T1) (swap_Typ u v T2))
- |(Forall T1 T2) \Rightarrow (Forall (swap_Typ u v T1) (swap_Typ u v T2))].
-
-lemma swap_Typ_inv : \forall u,v,T.(swap_Typ u v (swap_Typ u v T)) = T.
-intros;elim T
- [simplify;reflexivity
- |simplify;rewrite > swap_inv;reflexivity
- |simplify;reflexivity
- |simplify;rewrite > H;rewrite > H1;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
- [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;reflexivity
- |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))))
- [elim Hcut;elim H4;elim H5;clear Hcut H4 H5;rewrite > (H H6 H8);
- rewrite > (H1 H7 H9);reflexivity
- |split
- [split;unfold;intro;apply H2;apply natinG_or_inH_to_natinGH;auto
- |split;unfold;intro;apply H3;apply natinG_or_inH_to_natinGH;auto]]
- |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))))
- [elim Hcut;elim H4;elim H5;clear Hcut H4 H5;rewrite > (H H6 H8);
- rewrite > (H1 H7 H9);reflexivity
- |split
- [split;unfold;intro;apply H2;apply natinG_or_inH_to_natinGH;auto
- |split;unfold;intro;apply H3;apply natinG_or_inH_to_natinGH;auto]]]
-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
- |simplify;reflexivity
- |simplify;reflexivity
- |simplify;rewrite > H;rewrite > H1;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
- [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;intro;elim (in_list_nil ? ? H)
- |simplify;intros;elim (nat_in_list_case ? ? ? H2)
- [apply natinG_or_inH_to_natinGH;left;apply (H1 H3)
- |apply natinG_or_inH_to_natinGH;right;apply (H H3)]
- |simplify;intros;elim (nat_in_list_case ? ? ? H2)
- [apply natinG_or_inH_to_natinGH;left;apply (H1 H3)
- |apply natinG_or_inH_to_natinGH;right;apply (H H3)]]
- |elim T 0
- [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;intro;elim (in_list_nil ? ? H)
- |simplify;intros;elim (nat_in_list_case ? ? ? H2)
- [apply natinG_or_inH_to_natinGH;left;apply (H1 H3)
- |apply natinG_or_inH_to_natinGH;right;apply (H H3)]
- |simplify;intros;elim (nat_in_list_case ? ? ? H2)
- [apply natinG_or_inH_to_natinGH;left;apply (H1 H3)
- |apply natinG_or_inH_to_natinGH;right;apply (H H3)]]]