(**************************************************************************)
set "baseuri" "cic:/matita/Fsub/defn".
-include "logic/equality.ma".
-include "nat/nat.ma".
-include "datatypes/bool.ma".
-include "nat/compare.ma".
-include "list/list.ma".
include "Fsub/util.ma".
(*** representation of Fsub types ***)
| Top : Typ (* maximum type *)
| Arrow : Typ \to Typ \to Typ (* functions *)
| Forall : Typ \to Typ \to Typ. (* universal type *)
-
-(*** representation of Fsub terms ***)
-inductive Term : Set \def
- | Var : nat \to Term (* variable *)
- | Free : nat \to Term (* free name *)
- | Abs : Typ \to Term \to Term (* abstraction *)
- | App : Term \to Term \to Term (* function application *)
- | TAbs : Typ \to Term \to Term (* type abstraction *)
- | TApp : Term \to Typ \to Term. (* type application *)
-
+
(* representation of bounds *)
record bound : Set \def {
btype : Typ (* type to which the name is bound *)
}.
-(* representation of Fsub typing environments *)
-(*definition Env \def (list bound).
-definition Empty \def (nil bound).
-definition Cons \def \lambda G,X,T.((mk_bound false X T) :: G).
-definition TCons \def \lambda G,X,T.((mk_bound true X T) :: G).
-
-definition env_append : Env \to Env \to Env \def \lambda G,H.(H @ G). *)
-
(*** Various kinds of substitution, not all will be used probably ***)
(* substitutes i-th dangling index in type T with type U *)
| (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))) ].
-(* substitutes 0-th dangling index in type T with type U *)
-(*let rec subst_type_O T U \def subst_type_nat T U O.*)
-
-(* substitutes 0-th dangling index in term t with term u *)
-(*let rec subst_term_O t u \def
- let rec aux t0 i \def
- match t0 with
- [ (Var n) \Rightarrow match (eqb n i) with
- [ true \Rightarrow u
- | false \Rightarrow t0]
- | (Free X) \Rightarrow t0
- | (Abs T1 t1) \Rightarrow (Abs T1 (aux t1 (S i)))
- | (App t1 t2) \Rightarrow (App (aux t1 i) (aux t2 i))
- | (TAbs T1 t1) \Rightarrow (TAbs T1 (aux t1 (S i)))
- | (TApp t1 T1) \Rightarrow (TApp (aux t1 i) T1) ]
- in aux t O.
-
-(* substitutes 0-th dangling index in term T, which shall be a TVar,
- with type U *)
-let rec subst_term_tO t T \def
- let rec aux t0 i \def
- match t0 with
- [ (Var n) \Rightarrow t0
- | (Free X) \Rightarrow t0
- | (Abs T1 t1) \Rightarrow (Abs (subst_type_nat T1 T i) (aux t1 (S i)))
- | (App t1 t2) \Rightarrow (App (aux t1 i) (aux t2 i))
- | (TAbs T1 t1) \Rightarrow (TAbs (subst_type_nat T1 T i) (aux t1 (S i)))
- | (TApp t1 T1) \Rightarrow (TApp (aux t1 i) (subst_type_nat T1 T i)) ]
- in aux t O.
-
-(* substitutes (TFree X) in type T with type U *)
-let rec subst_type_tfree_type T X U on T \def
- match T with
- [ (TVar n) \Rightarrow T
- | (TFree Y) \Rightarrow match (eqb X Y) with
- [ true \Rightarrow U
- | false \Rightarrow T ]
- | Top \Rightarrow T
- | (Arrow T1 T2) \Rightarrow (Arrow (subst_type_tfree_type T1 X U)
- (subst_type_tfree_type T2 X U))
- | (Forall T1 T2) \Rightarrow (Forall (subst_type_tfree_type T1 X U)
- (subst_type_tfree_type T2 X U)) ].*)
-
(*** height of T's syntactic tree ***)
let rec t_len T \def
|(Arrow T1 T2) \Rightarrow (S (max (t_len T1) (t_len T2)))
|(Forall T1 T2) \Rightarrow (S (max (t_len T1) (t_len T2)))].
-definition head \def
- \lambda G:(list bound).match G with
- [ nil \Rightarrow (mk_bound false O Top)
- | (cons b H) \Rightarrow b].
-
-definition head_nat \def
- \lambda G:(list nat).match G with
- [ nil \Rightarrow O
- | (cons n H) \Rightarrow n].
-
(*** definitions about lists ***)
-(*(* var binding is in env judgement *)
-definition var_bind_in_env : bound \to (list bound) \to Prop \def
- \lambda b,G.(in_list bound b G).*)
-
definition fv_env : (list bound) \to (list nat) \def
\lambda G.(map ? ? (\lambda b.match b with
[(mk_bound B X T) \Rightarrow X]) G).
-(*(* variable is in env judgement *)
-definition var_in_env : nat \to (list bound) \to Prop \def
- \lambda x,G.(in_list nat x (fv_env G)).
-
-definition var_type_in_env : nat \to (list bound) \to Prop \def
- \lambda x,G.\exists T.(var_bind_in_env (mk_bound true x T) G).*)
-
let rec fv_type T \def
match T with
[(TVar n) \Rightarrow []
interpretation "type length" 'tlen T =
(cic:/matita/Fsub/defn/t_len.con T).
-notation > "hvbox(x ∈ l)"
- non associative with precedence 30 for @{ 'inlist $x $l }.
-notation < "hvbox(x \nbsp ∈ \nbsp l)"
- non associative with precedence 30 for @{ 'inlist $x $l }.
-interpretation "item in list" 'inlist x l =
- (cic:/matita/Fsub/util/in_list.ind#xpointer(1/1) _ x l).
-
notation "hvbox(!X ⊴ T)"
non associative with precedence 60 for @{ 'subtypebound $X $T }.
interpretation "subtyping bound" 'subtypebound X T =
(cic:/matita/Fsub/defn/bound.ind#xpointer(1/1/1) true X T).
-(*notation < "hvbox(e break ⊢ ta \nbsp 'V' \nbsp tb (= \above \alpha))"
- non associative with precedence 30 for @{ 'subjudg $e $ta $tb }.
-notation > "hvbox(e break ⊢ ta 'Fall' break tb)"
- non associative with precedence 30 for @{ 'subjudg $e $ta $tb }.
-notation "hvbox(e break ⊢ ta \lessdot break tb)"
- non associative with precedence 30 for @{ 'subjudg $e $ta $tb }.*)
-
(****** PROOFS ********)
-(*lemma subst_O_nat : \forall T,U.((subst_type_O T U) = T[#O↦U]).
-intros;elim T;simplify;reflexivity;
-qed.*)
-
(*** theorems about lists ***)
-(* FIXME: these definitions shouldn't be part of the poplmark challenge
- - use destruct instead, when hopefully it will get fixed... *)
-
-lemma inj_head : \forall h1,h2:bound.\forall t1,t2:(list bound).
- (h1::t1 = h2::t2) \to h1 = h2.
-intros.
-lapply (eq_f ? ? head ? ? H).simplify in Hletin.assumption.
-qed.
-
-lemma inj_head_nat : \forall h1,h2:nat.\forall t1,t2:(list nat).
- (h1::t1 = h2::t2) \to (h1 = h2).
-intros.
-lapply (eq_f ? ? head_nat ? ? H).simplify in Hletin.assumption.
-qed.
-
-lemma inj_tail : \forall A.\forall h1,h2:A.\forall t1,t2:(list A).
- ((h1::t1) = (h2::t2)) \to (t1 = t2).
-intros.lapply (eq_f ? ? (tail ?) ? ? H).simplify in Hletin.assumption.
-qed.
-
-(* end of fixme *)
-
lemma boundinenv_natinfv : \forall x,G.
(\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;inversion H3
- [intros;rewrite < H4;simplify;apply in_Base
- |intros;elim a3;simplify;apply in_Skip;
- lapply (inj_tail ? ? ? ? ? H7);rewrite > Hletin in H;apply H;
- apply ex_intro
- [apply a
- |apply ex_intro
- [apply a1
- |rewrite > H6;assumption]]]]
-qed.
-
-lemma nat_in_list_case : \forall G,H,n.(in_list nat n (H @ G)) \to
- (in_list nat n G) \lor (in_list nat n H).
-intros 3.elim H
- [simplify in H1;left;assumption
- |simplify in H2;inversion H2
- [intros;lapply (inj_head_nat ? ? ? ? H4);rewrite > Hletin;
- right;apply in_Base
- |intros;lapply (inj_tail ? ? ? ? ? H6);rewrite < Hletin in H3;
- rewrite > H5 in H1;lapply (H1 H3);elim Hletin1
- [left;assumption|right;apply in_Skip;assumption]]]
-qed.
-
-lemma natinG_or_inH_to_natinGH : \forall G,H,n.
- (in_list nat n G) \lor (in_list nat n H) \to
- (in_list nat n (H @ G)).
-intros.elim H1
- [elim H
- [simplify;assumption
- |simplify;apply in_Skip;assumption]
- |generalize in match H2;elim H2
- [simplify;apply in_Base
- |lapply (H4 H3);simplify;apply in_Skip;assumption]]
+ |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);
+ 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;inversion H1
- [intros;rewrite < H2;simplify;apply ex_intro
- [apply b
- |apply ex_intro
- [apply t1
- |lapply (inj_head_nat ? ? ? ? H3);rewrite > H2;rewrite < Hletin;
- apply in_Base]]
- |intros;lapply (inj_tail ? ? ? ? ? H5);rewrite < Hletin in H2;
- rewrite < H4 in H2;lapply (H H2);elim Hletin1;elim H6;apply ex_intro
- [apply a2
- |apply ex_intro
- [apply a3
- |apply in_Skip;rewrite < H4;assumption]]]]
-qed.
-
-theorem varinT_varinT_subst : \forall X,Y,T.
- (in_list ? X (fv_type T)) \to \forall n.
- (in_list ? X (fv_type (subst_type_nat T (TFree Y) n))).
-intros 3;elim T
- [simplify in H;elim (in_list_nil ? ? H)
- |simplify in H;simplify;assumption
- |simplify in H;elim (in_list_nil ? ? H)
- |simplify in H2;simplify;elim (nat_in_list_case ? ? ? H2);
- apply natinG_or_inH_to_natinGH;
- [left;apply (H1 H3)
- |right;apply (H H3)]
- |simplify in H2;simplify;elim (nat_in_list_case ? ? ? H2);
- apply natinG_or_inH_to_natinGH;
- [left;apply (H1 H3);
- |right;apply (H H3)]]
+ |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
+ |elim (H H2);elim H3;apply (ex_intro ? ? a);
+ apply (ex_intro ? ? a1);apply in_Skip;assumption]]
qed.
lemma incl_bound_fv : \forall l1,l2.(incl ? l1 l2) \to
|apply (H ? H3)]]
qed.
-lemma incl_nat_cons : \forall x,l1,l2.
- (incl nat l1 l2) \to (incl nat (x :: l1) (x :: l2)).
-intros.unfold in H.unfold.intros.inversion H1
- [intros;lapply (inj_head_nat ? ? ? ? H3);rewrite > Hletin;apply in_Base
- |intros;apply in_Skip;apply H;lapply (inj_tail ? ? ? ? ? H5);rewrite > Hletin;
- assumption]
+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)]
qed.
lemma WFT_env_incl : \forall G,T.(WFType G T) \to
|apply WFT_Arrow [apply (H2 ? H6)|apply (H4 ? H6)]
|apply WFT_Forall
[apply (H2 ? H6)
- |intros;apply H4
+ |intros;apply (H4 ? ? H8)
[unfold;intro;apply H7;apply(H6 ? H9)
- |assumption
- |simplify;apply (incl_nat_cons ? ? ? H6)]]]
+ |simplify;apply (incl_cons ? ? ? H6)]]]
qed.
lemma fv_env_extends : \forall H,x,B,C,T,U,G.
(fv_env (H @ ((mk_bound B x T) :: G))) =
(fv_env (H @ ((mk_bound C x U) :: G))).
intros;elim H
- [simplify;reflexivity
- |elim t;simplify;rewrite > H1;reflexivity]
+ [simplify;reflexivity|elim t;simplify;rewrite > H1;reflexivity]
qed.
lemma lookup_env_extends : \forall G,H,B,C,D,T,U,V,x,y.
(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;(*FIXME*)generalize in match H1;intro;inversion H1
- [intros;lapply (inj_head ? ? ? ? H5);rewrite < H4 in Hletin;
- destruct Hletin;absurd (y = x) [symmetry;assumption|assumption]
- |intros;simplify;lapply (inj_tail ? ? ? ? ? H7);rewrite > Hletin;
- apply in_Skip;assumption]
- |(*FIXME*)generalize in match H2;intro;inversion H2
- [intros;simplify in H6;lapply (inj_head ? ? ? ? H6);rewrite > Hletin;
- simplify;apply in_Base
- |simplify;intros;lapply (inj_tail ? ? ? ? ? H8);rewrite > Hletin in H1;
- rewrite > H7 in H1;apply in_Skip;apply (H1 H5 H3)]]
+ [simplify in H1;elim (in_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))]]
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;inversion H
- [intros;lapply (sym_eq ? ? ? H2);absurd (a::l = [])
- [assumption|apply nil_cons]
- |intros;lapply (sym_eq ? ? ? H4);absurd (a1::l = [])
- [assumption|apply nil_cons]]
+ [simplify in H;elim (in_list_nil ? ? H)
|2,3:simplify;simplify in H;assumption
- |*:simplify in H2;simplify;apply natinG_or_inH_to_natinGH;
- lapply (nat_in_list_case ? ? ? H2);elim Hletin
- [1,3:left;apply (H1 ? H3)
- |*:right;apply (H ? H3)]]
+ |*: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)]]
qed.
(*** lemma on fresh names ***)
[apply a
|apply H;constructor 1]
|intros;elim l
- [apply ex_intro
- [apply O
- |intros;unfold;intro;inversion H1
- [intros;lapply (sym_eq ? ? ? H3);absurd (a::l1 = [])
- [assumption|apply nil_cons]
- |intros;lapply (sym_eq ? ? ? H5);absurd (a1::l1 = [])
- [assumption|apply nil_cons]]]
- |elim H;lapply (decidable_eq_nat a t);elim Hletin
- [apply ex_intro
- [apply (S a)
- |intros;unfold;intro;inversion H4
- [intros;lapply (inj_head_nat ? ? ? ? H6);rewrite < Hletin1 in H5;
- rewrite < H2 in H5;rewrite > H5 in H3;
- apply (not_le_Sn_n ? H3)
- |intros;lapply (inj_tail ? ? ? ? ? H8);rewrite < Hletin1 in H5;
- rewrite < H7 in H5;
- apply (H1 m ? H5);lapply (le_S ? ? H3);
- apply (le_S_S_to_le ? ? Hletin2)]]
- |cut ((leb a t) = true \lor (leb a t) = false)
- [elim Hcut
- [apply ex_intro
- [apply (S t)
- |intros;unfold;intro;inversion H5
- [intros;lapply (inj_head_nat ? ? ? ? H7);rewrite > H6 in H4;
- rewrite < Hletin1 in H4;apply (not_le_Sn_n ? H4)
- |intros;lapply (inj_tail ? ? ? ? ? H9);
- rewrite < Hletin1 in H6;lapply (H1 a1)
- [apply (Hletin2 H6)
- |lapply (leb_to_Prop a t);rewrite > H3 in Hletin2;
- simplify in Hletin2;rewrite < H8;
- apply (trans_le ? ? ? Hletin2);
- apply (trans_le ? ? ? ? H4);constructor 2;constructor 1]]]
- |apply ex_intro
- [apply a
- |intros;lapply (leb_to_Prop a t);rewrite > H3 in Hletin1;
- simplify in Hletin1;lapply (not_le_to_lt ? ? Hletin1);
- unfold in Hletin2;unfold;intro;inversion H5
- [intros;lapply (inj_head_nat ? ? ? ? H7);
- rewrite < Hletin3 in H6;rewrite > H6 in H4;
- apply (Hletin1 H4)
- |intros;lapply (inj_tail ? ? ? ? ? H9);
- rewrite < Hletin3 in H6;rewrite < H8 in H6;
- apply (H1 ? H4 H6)]]]
- |elim (leb a t);autobatch]]]]
+ [apply (ex_intro ? ? O);intros;unfold;intro;elim (in_list_nil ? ? H1)
+ |elim H;
+ apply (ex_intro ? ? (S (max a t))).
+ intros.unfold. intro.
+ elim (in_cons_case ? ? ? ? H3)
+ [rewrite > H4 in H2.autobatch
+ |elim H4
+ [apply (H1 m ? H4).apply (trans_le ? (max a t));autobatch
+ |assumption]]]]
qed.
(*** lemmata on well-formedness ***)
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;inversion H2
- [intros;lapply (inj_head_nat ? ? ? ? H4);rewrite < Hletin;assumption
- |intros;lapply (inj_tail ? ? ? ? ? H6);rewrite < Hletin in H3;
- inversion H3
- [intros;lapply (sym_eq ? ? ? H8);absurd (a2 :: l2 = [])
- [assumption|apply nil_cons]
- |intros;lapply (sym_eq ? ? ? H10);
- absurd (a3 :: l2 = []) [assumption|apply nil_cons]]]
- |simplify in H1;lapply (in_list_nil ? x H1);elim Hletin
- |simplify in H5;lapply (nat_in_list_case ? ? ? H5);elim Hletin
- [apply (H4 H6)
- |apply (H2 H6)]
- |simplify in H5;lapply (nat_in_list_case ? ? ? H5);elim Hletin
- [lapply (fresh_name ((fv_type t1) @ (fv_env l)));elim Hletin1;
- cut ((\lnot (in_list ? a (fv_type t1))) \land
- (\lnot (in_list ? a (fv_env l))))
+ [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)
+ [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 \neq a)
- [simplify in Hletin2;
- (* FIXME trick *);generalize in match Hletin2;intro;
- inversion Hletin2
- [intros;lapply (inj_head_nat ? ? ? ? H12);
- rewrite < Hletin3 in H11;lapply (Hcut1 H11);elim Hletin4
- |intros;lapply (inj_tail ? ? ? ? ? H14);rewrite > Hletin3;
- assumption]
- |unfold;intro;apply H8;rewrite < H10;assumption]
+ [cut (x ≠ a)
+ [simplify in Hletin;elim (in_cons_case ? ? ? ? Hletin)
+ [elim (Hcut1 H10)
+ |assumption]
+ |intro;apply H8;applyS H6]
|apply in_FV_subst;assumption]
|split
- [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.
-
-(*** some exotic inductions and related lemmas ***)
-
-lemma not_t_len_lt_SO : \forall T.\lnot (t_len T) < (S O).
-intros;elim T
- [1,2,3: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))
- [1,3: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 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
- [1,2,3:apply H;intros;simplify in H4;elim (not_t_len_lt_SO ? H4)
- |*:apply H;intros;apply (H1 (t_len V))
- [1,3: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 ⇒ (t_len T2)
- | true ⇒ (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));autobatch]
- |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));autobatch]
- |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));autobatch]
- |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));autobatch]
- |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
- |2,3: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]
+ [intro;apply H7;apply in_list_append1;assumption
+ |intro;apply H7;apply in_list_append2;assumption]]]]
qed.
(*** lemmata relating subtyping and well-formedness ***)
(WFEnv (H @ ((mk_bound B x T) :: G))) \to (WFType G U) \to
(WFEnv (H @ ((mk_bound C x U) :: G))).
intros 7;elim H 0
- [simplify;intros;(*FIXME*)generalize in match H1;intro;inversion H1
- [intros;lapply (nil_cons ? G (mk_bound B x T));lapply (Hletin H4);
- elim Hletin1
- |intros;lapply (inj_tail ? ? ? ? ? H8);lapply (inj_head ? ? ? ? H8);
- destruct Hletin1;rewrite < Hletin in H6;rewrite < Hletin in H4;
- rewrite < Hcut1 in H6;apply (WFE_cons ? ? ? ? H4 H6 H2)]
+ [simplify;intros;(*FIXME*)generalize in match H1;intro;inversion H1;intros
+ [lapply (nil_cons ? G (mk_bound B x T));elim (Hletin H4)
+ |destruct H8;apply (WFE_cons ? ? ? ? H4 H6 H2)]
|intros;simplify;generalize in match H2;elim t;simplify in H4;
- inversion H4
- [intros;absurd (mk_bound b n t1::l@(mk_bound B x T::G)=[])
- [assumption
- |apply nil_cons]
- |intros;lapply (inj_tail ? ? ? ? ? H9);lapply (inj_head ? ? ? ? H9);
- destruct Hletin1;apply WFE_cons
- [apply H1
- [rewrite > Hletin;assumption
- |assumption]
- |rewrite > Hcut1;generalize in match H7;rewrite < Hletin;
- rewrite > (fv_env_extends ? x B C T U);intro;assumption
- |rewrite < Hletin in H8;rewrite > Hcut2;
- apply (WFT_env_incl ? ? H8);rewrite > (fv_env_extends ? x B C T U);
- unfold;intros;assumption]]]
+ inversion H4;intros
+ [destruct H5
+ |destruct H9;apply WFE_cons
+ [apply (H1 H5 H3)
+ |rewrite < (fv_env_extends ? x B C T U); assumption
+ |apply (WFT_env_incl ? ? H8);
+ rewrite < (fv_env_extends ? x B C T U);unfold;intros;
+ assumption]]]
qed.
lemma WFE_bound_bound : \forall B,x,T,U,G. (WFEnv G) \to
(in_list ? (mk_bound B x U) G) \to T = U.
intros 6;elim H
[lapply (in_list_nil ? ? H1);elim Hletin
- |inversion H6
- [intros;rewrite < H7 in H8;lapply (inj_head ? ? ? ? H8);
- rewrite > Hletin in H5;inversion H5
- [intros;rewrite < H9 in H10;lapply (inj_head ? ? ? ? H10);
- destruct Hletin1;symmetry;assumption
- |intros;lapply (inj_tail ? ? ? ? ? H12);rewrite < Hletin1 in H9;
- rewrite < H11 in H9;lapply (boundinenv_natinfv x l)
- [destruct Hletin;rewrite < Hcut1 in Hletin2;lapply (H3 Hletin2);
- elim Hletin3
- |apply ex_intro
- [apply B|apply ex_intro [apply T|assumption]]]]
- |intros;lapply (inj_tail ? ? ? ? ? H10);rewrite < H9 in H7;
- rewrite < Hletin in H7;(*FIXME*)generalize in match H5;intro;inversion H5
- [intros;rewrite < H12 in H13;lapply (inj_head ? ? ? ? H13);
- destruct Hletin1;rewrite < Hcut1 in H7;
- lapply (boundinenv_natinfv n l)
- [lapply (H3 Hletin2);elim Hletin3
- |apply ex_intro
- [apply B|apply ex_intro [apply U|assumption]]]
- |intros;apply (H2 ? H7);rewrite > H14;lapply (inj_tail ? ? ? ? ? H15);
- rewrite > Hletin1;assumption]]]
+ |elim (in_cons_case ? ? ? ? H6)
+ [destruct H7;destruct;elim (in_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)
+ [destruct H8;elim H3;apply boundinenv_natinfv;apply (ex_intro ? ? B);
+ apply (ex_intro ? ? U);assumption
+ |apply (H2 H8 H7)]]]
+qed.
+
+lemma WFT_to_incl: ∀G,T,U.
+ (∀X.(¬(X ∈ fv_env G)) → (¬(X ∈ fv_type U)) →
+ (WFType (mk_bound true X T::G) (subst_type_nat U (TFree X) O)))
+ → incl ? (fv_type U) (fv_env G).
+intros.elim (fresh_name ((fv_type U)@(fv_env G))).lapply(H a)
+ [unfold;intros;lapply (fv_WFT ? x ? Hletin)
+ [simplify in Hletin1;inversion Hletin1;intros
+ [destruct H4;elim H1;autobatch
+ |destruct H6;assumption]
+ |apply in_FV_subst;assumption]
+ |*:intro;apply H1;autobatch]
qed.
+
+lemma incl_fv_env: ∀X,G,G1,U,P.
+ incl ? (fv_env (G1@(mk_bound true X U::G)))
+ (fv_env (G1@(mk_bound true X P::G))).
+intros.rewrite < fv_env_extends.apply incl_A_A.
+qed.
+
+lemma JSubtype_Top: ∀G,P.G ⊢ ⊤ ⊴ P → P = ⊤.
+intros.inversion H;intros
+ [assumption|reflexivity
+ |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.
+intros 4.cut (∀Y.TFree Y = TFree X → ∀U.G ⊢ (TFree Y) ⊴ U → G ⊢ T ⊴ U)
+ [apply Hcut;reflexivity
+ |elim H;intros
+ [rewrite > H3 in H4;rewrite > (JSubtype_Top ? ? H4);apply SA_Top;assumption
+ |rewrite < H3;assumption
+ |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
projects / helm.git / blobdiff