| (Arrow T1 T2) \Rightarrow (Arrow (subst_type_nat T1 U i) (subst_type_nat T2 U i))
| (Forall T1 T2) \Rightarrow (Forall (subst_type_nat T1 U i) (subst_type_nat T2 U (S i))) ].
-(*** height of T's syntactic tree ***)
-
-let rec t_len T \def
- match T with
- [(TVar n) \Rightarrow (S O)
- |(TFree X) \Rightarrow (S O)
- |Top \Rightarrow (S O)
- |(Arrow T1 T2) \Rightarrow (S (max (t_len T1) (t_len T2)))
- |(Forall T1 T2) \Rightarrow (S (max (t_len T1) (t_len T2)))].
-
(*** definitions about lists ***)
definition fv_env : (list bound) \to (list nat) \def
interpretation "subst bound var" 'substvar S T n =
(cic:/matita/Fsub/defn/subst_type_nat.con S T n).
-notation "hvbox(|T|)"
- non associative with precedence 30 for @{ 'tlen $T }.
-interpretation "type length" 'tlen T =
- (cic:/matita/Fsub/defn/t_len.con T).
-
notation "hvbox(!X ⊴ T)"
non associative with precedence 60 for @{ 'subtypebound $X $T }.
interpretation "subtyping bound" 'subtypebound X T =
(\exists B,T.(in_list ? (mk_bound B x T) G)) \to
(in_list ? x (fv_env G)).
intros 2;elim G
- [elim H;elim H1;lapply (in_list_nil ? ? H2);elim Hletin
- |elim H1;elim H2;elim (in_cons_case ? ? ? ? H3)
- [rewrite < H4;simplify;apply in_Base
- |simplify;apply in_Skip;apply H;apply (ex_intro ? ? a);
+ [elim H;elim H1;lapply (not_in_list_nil ? ? H2);elim Hletin
+ |elim H1;elim H2;elim (in_list_cons_case ? ? ? ? H3)
+ [rewrite < H4;simplify;apply in_list_head
+ |simplify;apply in_list_cons;apply H;apply (ex_intro ? ? a);
apply (ex_intro ? ? a1);assumption]]
qed.
lemma natinfv_boundinenv : \forall x,G.(in_list ? x (fv_env G)) \to
\exists B,T.(in_list ? (mk_bound B x T) G).
intros 2;elim G 0
- [simplify;intro;lapply (in_list_nil ? ? H);elim Hletin
- |intros 3;elim t;simplify in H1;elim (in_cons_case ? ? ? ? H1)
- [rewrite < H2;apply (ex_intro ? ? b);apply (ex_intro ? ? t1);apply in_Base
+ [simplify;intro;lapply (not_in_list_nil ? ? H);elim Hletin
+ |intros 3;elim t;simplify in H1;elim (in_list_cons_case ? ? ? ? H1)
+ [rewrite < H2;apply (ex_intro ? ? b);apply (ex_intro ? ? t1);apply in_list_head
|elim (H H2);elim H3;apply (ex_intro ? ? a);
- apply (ex_intro ? ? a1);apply in_Skip;assumption]]
+ apply (ex_intro ? ? a1);apply in_list_cons;assumption]]
qed.
lemma incl_bound_fv : \forall l1,l2.(incl ? l1 l2) \to
lemma incl_cons : \forall x,l1,l2.
(incl ? l1 l2) \to (incl nat (x :: l1) (x :: l2)).
-intros.unfold in H.unfold.intros.elim (in_cons_case ? ? ? ? H1)
- [rewrite > H2;apply in_Base|apply in_Skip;apply (H ? H2)]
+intros.unfold in H.unfold.intros.elim (in_list_cons_case ? ? ? ? H1)
+ [rewrite > H2;apply in_list_head|apply in_list_cons;apply (H ? H2)]
qed.
lemma WFT_env_incl : \forall G,T.(WFType G T) \to
(y \neq x) \to
(in_list ? (mk_bound D y V) (H @ ((mk_bound B x T) :: G))).
intros 10;elim H
- [simplify in H1;elim (in_cons_case ? ? ? ? H1)
+ [simplify in H1;elim (in_list_cons_case ? ? ? ? H1)
[destruct H3;elim (H2);reflexivity
- |simplify;apply (in_Skip ? ? ? ? H3);]
- |simplify in H2;simplify;elim (in_cons_case ? ? ? ? H2)
- [rewrite > H4;apply in_Base
- |apply (in_Skip ? ? ? ? (H1 H4 H3))]]
+ |simplify;apply (in_list_cons ? ? ? ? H3);]
+ |simplify in H2;simplify;elim (in_list_cons_case ? ? ? ? H2)
+ [rewrite > H4;apply in_list_head
+ |apply (in_list_cons ? ? ? ? (H1 H4 H3))]]
qed.
lemma in_FV_subst : \forall x,T,U,n.(in_list ? x (fv_type T)) \to
(in_list ? x (fv_type (subst_type_nat T U n))).
intros 3;elim T
- [simplify in H;elim (in_list_nil ? ? H)
+ [simplify in H;elim (not_in_list_nil ? ? H)
|2,3:simplify;simplify in H;assumption
- |*:simplify in H2;simplify;elim (append_to_or_in_list ? ? ? ? H2)
- [1,3:apply in_list_append1;apply (H ? H3)
- |*:apply in_list_append2;apply (H1 ? H3)]]
+ |*:simplify in H2;simplify;elim (in_list_append_to_or_in_list ? ? ? ? H2)
+ [1,3:apply in_list_to_in_list_append_l;apply (H ? H3)
+ |*:apply in_list_to_in_list_append_r;apply (H1 ? H3)]]
qed.
(*** lemma on fresh names ***)
[apply a
|apply H;constructor 1]
|intros;elim l
- [apply (ex_intro ? ? O);intros;unfold;intro;elim (in_list_nil ? ? H1)
+ [apply (ex_intro ? ? O);intros;unfold;intro;elim (not_in_list_nil ? ? H1)
|elim H;
apply (ex_intro ? ? (S (max a t))).
intros.unfold. intro.
- elim (in_cons_case ? ? ? ? H3)
+ elim (in_list_cons_case ? ? ? ? H3)
[rewrite > H4 in H2.autobatch
|elim H4
[apply (H1 m ? H4).apply (trans_le ? (max a t));autobatch
lemma fv_WFT : \forall T,x,G.(WFType G T) \to (in_list ? x (fv_type T)) \to
(in_list ? x (fv_env G)).
intros 4.elim H
- [simplify in H2;elim (in_cons_case ? ? ? ? H2)
- [rewrite > H3;assumption|elim (in_list_nil ? ? H3)]
- |simplify in H1;elim (in_list_nil ? x H1)
- |simplify in H5;elim (append_to_or_in_list ? ? ? ? H5);autobatch
- |simplify in H5;elim (append_to_or_in_list ? ? ? ? H5)
+ [simplify in H2;elim (in_list_cons_case ? ? ? ? H2)
+ [rewrite > H3;assumption|elim (not_in_list_nil ? ? H3)]
+ |simplify in H1;elim (not_in_list_nil ? x H1)
+ |simplify in H5;elim (in_list_append_to_or_in_list ? ? ? ? H5);autobatch
+ |simplify in H5;elim (in_list_append_to_or_in_list ? ? ? ? H5)
[apply (H2 H6)
|elim (fresh_name ((fv_type t1) @ (fv_env l)));
cut (¬ (a ∈ (fv_type t1)) ∧ ¬ (a ∈ (fv_env l)))
[elim Hcut;lapply (H4 ? H9 H8)
[cut (x ≠ a)
- [simplify in Hletin;elim (in_cons_case ? ? ? ? Hletin)
+ [simplify in Hletin;elim (in_list_cons_case ? ? ? ? Hletin)
[elim (Hcut1 H10)
|assumption]
|intro;apply H8;applyS H6]
|apply in_FV_subst;assumption]
|split
- [intro;apply H7;apply in_list_append1;assumption
- |intro;apply H7;apply in_list_append2;assumption]]]]
+ [intro;apply H7;apply in_list_to_in_list_append_l;assumption
+ |intro;apply H7;apply in_list_to_in_list_append_r;assumption]]]]
qed.
(*** lemmata relating subtyping and well-formedness ***)
(in_list ? (mk_bound B x T) G) \to
(in_list ? (mk_bound B x U) G) \to T = U.
intros 6;elim H
- [lapply (in_list_nil ? ? H1);elim Hletin
- |elim (in_cons_case ? ? ? ? H6)
- [destruct H7;destruct;elim (in_cons_case ? ? ? ? H5)
+ [lapply (not_in_list_nil ? ? H1);elim Hletin
+ |elim (in_list_cons_case ? ? ? ? H6)
+ [destruct H7;destruct;elim (in_list_cons_case ? ? ? ? H5)
[destruct H7;reflexivity
|elim H7;elim H3;apply boundinenv_natinfv;apply (ex_intro ? ? B);
apply (ex_intro ? ? T);assumption]
- |elim (in_cons_case ? ? ? ? H5)
+ |elim (in_list_cons_case ? ? ? ? H5)
[destruct H8;elim H3;apply boundinenv_natinfv;apply (ex_intro ? ? B);
apply (ex_intro ? ? U);assumption
|apply (H2 H8 H7)]]]
|destruct H5|*:destruct H6]
qed.
+(*
(* elim vs inversion *)
lemma JS_trans_TFree: ∀G,T,X.G ⊢ T ⊴ (TFree X) →
∀U.G ⊢ (TFree X) ⊴ U → G ⊢ T ⊴ U.
|apply (SA_Trans_TVar ? ? ? ? H1);apply (H3 Y);assumption
|*:destruct H5]]
qed.
+*)
lemma fv_append : ∀G,H.fv_env (G @ H) = (fv_env G @ fv_env H).
intro;elim G;simplify;autobatch paramodulation;
-qed.
\ No newline at end of file
+qed.
projects / helm.git / blobdiff