- [unfold;intro;apply H7;apply natinG_or_inH_to_natinGH;right;
- assumption
- |unfold;intro;apply H7;apply natinG_or_inH_to_natinGH;left;
- assumption]]
- |apply (H2 H6)]]
-qed.
-
-lemma WFE_consG_to_WFT : \forall G.\forall b,X,T.
- (WFEnv ((mk_bound b X T)::G)) \to (WFType G T).
-intros.
-inversion H
- [intro;reduce in H1;destruct H1
- |intros;lapply (inj_head ? ? ? ? H5);lapply (inj_tail ? ? ? ? ? H5);
- destruct Hletin;rewrite > Hletin1;rewrite > Hcut2;assumption]
-qed.
-
-lemma WFE_consG_WFE_G : \forall G.\forall b.
- (WFEnv (b::G)) \to (WFEnv G).
-intros.
-inversion H
- [intro;reduce in H1;destruct H1
- |intros;lapply (inj_tail ? ? ? ? ? H5);rewrite > Hletin;assumption]
-qed.
-
-lemma WFT_swap : \forall u,v,G,T.(WFType G T) \to
- (WFType (swap_Env u v G) (swap_Typ u v T)).
-intros.elim H
- [simplify;apply WFT_TFree;lapply (natinfv_boundinenv ? ? H1);elim Hletin;
- elim H2;apply boundinenv_natinfv;apply ex_intro
- [apply a
- |apply ex_intro
- [apply (swap_Typ u v a1)
- |apply lookup_swap;assumption]]
- |simplify;apply WFT_Top
- |simplify;apply WFT_Arrow
- [assumption|assumption]
- |simplify;apply WFT_Forall
- [assumption
- |intros;rewrite < (swap_inv u v);
- cut (\lnot (in_list ? (swap u v X) (fv_type t1)))
- [cut (\lnot (in_list ? (swap u v X) (fv_env e)))
- [generalize in match (H4 ? Hcut1 Hcut);simplify;
- rewrite > subst_type_O_swap;intro;assumption
- |lapply (in_dom_swap u v (swap u v X) e);elim Hletin;unfold;
- intros;lapply (H7 H9);rewrite > (swap_inv u v) in Hletin1;
- apply (H5 Hletin1)]
- |generalize in match (in_fv_type_swap u v (swap u v X) t1);intros;
- elim H7;unfold;intro;lapply (H8 H10);
- rewrite > (swap_inv u v) in Hletin;apply (H6 Hletin)]]]
-qed.
-
-lemma WFE_swap : \forall u,v,G.(WFEnv G) \to (WFEnv (swap_Env u v G)).
-intros 3.elim G 0
- [intro;simplify;assumption
- |intros 2;elim s;simplify;constructor 2
- [apply H;apply (WFE_consG_WFE_G ? ? H1)
- |unfold;intro;lapply (in_dom_swap u v n l);elim Hletin;lapply (H4 H2);
- (* FIXME trick *)generalize in match H1;intro;inversion H1
- [intros;absurd ((mk_bound b n t)::l = [])
- [assumption|apply nil_cons]
- |intros;lapply (inj_head ? ? ? ? H10);lapply (inj_tail ? ? ? ? ? H10);
- destruct Hletin2;rewrite < Hcut1 in H8;rewrite < Hletin3 in H8;
- apply (H8 Hletin1)]
- |apply (WFT_swap u v l t);inversion H1
- [intro;absurd ((mk_bound b n t)::l = [])
- [assumption|apply nil_cons]
- |intros;lapply (inj_head ? ? ? ? H6);lapply (inj_tail ? ? ? ? ? H6);
- destruct Hletin;rewrite > Hletin1;rewrite > Hcut2;assumption]]]
-qed.
-
-(*** some exotic inductions and related lemmas ***)
-
-(* TODO : relocate the following 3 lemmas *)
-
-lemma max_case : \forall m,n.(max m n) = match (leb m n) with
- [ false \Rightarrow n
- | true \Rightarrow m ].
-intros;elim m;simplify;reflexivity;
-qed.
-
-lemma not_t_len_lt_SO : \forall T.\lnot (t_len T) < (S O).
-intros;elim T
- [simplify;unfold;intro;unfold in H;elim (not_le_Sn_n ? H)
- |simplify;unfold;intro;unfold in H;elim (not_le_Sn_n ? H)
- |simplify;unfold;intro;unfold in H;elim (not_le_Sn_n ? H)
- |simplify;unfold;rewrite > max_case;elim (leb (t_len t) (t_len t1))
- [simplify in H2;apply H1;apply (trans_lt ? ? ? ? H2);unfold;constructor 1
- |simplify in H2;apply H;apply (trans_lt ? ? ? ? H2);unfold;constructor 1]
- |simplify;unfold;rewrite > max_case;elim (leb (t_len t) (t_len t1))
- [simplify in H2;apply H1;apply (trans_lt ? ? ? ? H2);unfold;constructor 1
- |simplify in H2;apply H;apply (trans_lt ? ? ? ? H2);unfold;constructor 1]]
-qed.
-
-lemma t_len_gt_O : \forall T.(t_len T) > O.
-intro;elim T
- [simplify;unfold;unfold;constructor 1
- |simplify;unfold;unfold;constructor 1
- |simplify;unfold;unfold;constructor 1
- |simplify;lapply (max_case (t_len t) (t_len t1));rewrite > Hletin;
- elim (leb (t_len t) (t_len t1))
- [simplify;unfold;unfold;constructor 2;unfold in H1;unfold in H1;assumption
- |simplify;unfold;unfold;constructor 2;unfold in H;unfold in H;assumption]
- |simplify;lapply (max_case (t_len t) (t_len t1));rewrite > Hletin;
- elim (leb (t_len t) (t_len t1))
- [simplify;unfold;unfold;constructor 2;unfold in H1;unfold in H1;assumption
- |simplify;unfold;unfold;constructor 2;unfold in H;unfold in H;assumption]]
-qed.
-
-lemma Typ_len_ind : \forall P:Typ \to Prop.
- (\forall U.(\forall V.((t_len V) < (t_len U)) \to (P V))
- \to (P U))
- \to \forall T.(P T).
-cut (\forall P:Typ \to Prop.
- (\forall U.(\forall V.((t_len V) < (t_len U)) \to (P V))
- \to (P U))
- \to \forall T,n.(n = (t_len T)) \to (P T))
- [intros;apply (Hcut ? H ? (t_len T));reflexivity
- |intros 4;generalize in match T;apply (nat_elim1 n);intros;
- generalize in match H2;elim t
- [apply H;intros;simplify in H4;elim (not_t_len_lt_SO ? H4)
- |apply H;intros;simplify in H4;elim (not_t_len_lt_SO ? H4)
- |apply H;intros;simplify in H4;elim (not_t_len_lt_SO ? H4)
- |apply H;intros;apply (H1 (t_len V))
- [rewrite > H5;assumption
- |reflexivity]
- |apply H;intros;apply (H1 (t_len V))
- [rewrite > H5;assumption
- |reflexivity]]]
-qed.
-
-lemma t_len_arrow1 : \forall T1,T2.(t_len T1) < (t_len (Arrow T1 T2)).
-intros.simplify.
-(* FIXME!!! BUG?!?! *)
-cut ((max (t_len T1) (t_len T2)) = match (leb (t_len T1) (t_len T2)) with
- [ false \Rightarrow (t_len T2)
- | true \Rightarrow (t_len T1) ])
- [rewrite > Hcut;cut ((leb (t_len T1) (t_len T2)) = false \lor
- (leb (t_len T1) (t_len T2)) = true)
- [lapply (leb_to_Prop (t_len T1) (t_len T2));elim Hcut1
- [rewrite > H;rewrite > H in Hletin;simplify;constructor 1
- |rewrite > H;rewrite > H in Hletin;simplify;simplify in Hletin;
- unfold;apply le_S_S;assumption]
- |elim (leb (t_len T1) (t_len T2));auto]
- |elim T1;simplify;reflexivity]
-qed.
-
-lemma t_len_arrow2 : \forall T1,T2.(t_len T2) < (t_len (Arrow T1 T2)).
-intros.simplify.
-(* FIXME!!! BUG?!?! *)
-cut ((max (t_len T1) (t_len T2)) = match (leb (t_len T1) (t_len T2)) with
- [ false \Rightarrow (t_len T2)
- | true \Rightarrow (t_len T1) ])
- [rewrite > Hcut;cut ((leb (t_len T1) (t_len T2)) = false \lor
- (leb (t_len T1) (t_len T2)) = true)
- [lapply (leb_to_Prop (t_len T1) (t_len T2));elim Hcut1
- [rewrite > H;rewrite > H in Hletin;simplify;simplify in Hletin;
- lapply (not_le_to_lt ? ? Hletin);unfold in Hletin1;unfold;
- constructor 2;assumption
- |rewrite > H;simplify;unfold;constructor 1]
- |elim (leb (t_len T1) (t_len T2));auto]
- |elim T1;simplify;reflexivity]
-qed.
-
-lemma t_len_forall1 : \forall T1,T2.(t_len T1) < (t_len (Forall T1 T2)).
-intros.simplify.
-(* FIXME!!! BUG?!?! *)
-cut ((max (t_len T1) (t_len T2)) = match (leb (t_len T1) (t_len T2)) with
- [ false \Rightarrow (t_len T2)
- | true \Rightarrow (t_len T1) ])
- [rewrite > Hcut;cut ((leb (t_len T1) (t_len T2)) = false \lor
- (leb (t_len T1) (t_len T2)) = true)
- [lapply (leb_to_Prop (t_len T1) (t_len T2));elim Hcut1
- [rewrite > H;rewrite > H in Hletin;simplify;constructor 1
- |rewrite > H;rewrite > H in Hletin;simplify;simplify in Hletin;
- unfold;apply le_S_S;assumption]
- |elim (leb (t_len T1) (t_len T2));auto]
- |elim T1;simplify;reflexivity]
-qed.
-
-lemma t_len_forall2 : \forall T1,T2.(t_len T2) < (t_len (Forall T1 T2)).
-intros.simplify.
-(* FIXME!!! BUG?!?! *)
-cut ((max (t_len T1) (t_len T2)) = match (leb (t_len T1) (t_len T2)) with
- [ false \Rightarrow (t_len T2)
- | true \Rightarrow (t_len T1) ])
- [rewrite > Hcut;cut ((leb (t_len T1) (t_len T2)) = false \lor
- (leb (t_len T1) (t_len T2)) = true)
- [lapply (leb_to_Prop (t_len T1) (t_len T2));elim Hcut1
- [rewrite > H;rewrite > H in Hletin;simplify;simplify in Hletin;
- lapply (not_le_to_lt ? ? Hletin);unfold in Hletin1;unfold;
- constructor 2;assumption
- |rewrite > H;simplify;unfold;constructor 1]
- |elim (leb (t_len T1) (t_len T2));auto]
- |elim T1;simplify;reflexivity]
-qed.
-
-lemma eq_t_len_TFree_subst : \forall T,n,X.(t_len T) =
- (t_len (subst_type_nat T (TFree X) n)).
-intro.elim T
- [simplify;elim (eqb n n1)
- [simplify;reflexivity
- |simplify;reflexivity]
- |simplify;reflexivity
- |simplify;reflexivity
- |simplify;lapply (H n X);lapply (H1 n X);rewrite < Hletin;rewrite < Hletin1;
- reflexivity
- |simplify;lapply (H n X);lapply (H1 (S n) X);rewrite < Hletin;
- rewrite < Hletin1;reflexivity]