(**************************************************************************)
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]]]]
+ |elim H1;elim H2;elim (in_cons_case ? ? ? ? H3)
+ [rewrite < H4;simplify;apply in_Base
+ |elim H4;elim t;simplify;apply in_Skip2;apply H;apply (ex_intro ? ? a);
+ apply (ex_intro ? ? a1);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]]]
+ |simplify in H2;elim (in_cons_case ? ? ? ? H2)
+ [right;rewrite > H3;apply in_Base
+ |elim H3;elim (H1 H5) [left;assumption|right;apply in_Skip2;assumption]]]
qed.
lemma natinG_or_inH_to_natinGH : \forall G,H,n.
intros.elim H1
[elim H
[simplify;assumption
- |simplify;apply in_Skip;assumption]
+ |simplify;apply in_Skip2;assumption]
|generalize in match H2;elim H2
[simplify;apply in_Base
|lapply (H4 H3);simplify;apply in_Skip;assumption]]
\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]]]]
+ |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 H2;elim (H H4);elim H5;apply (ex_intro ? ? a);
+ apply (ex_intro ? ? a1);apply in_Skip
+ [assumption
+ |intro;destruct H7;elim (H3 Hcut1)]]]
qed.
theorem varinT_varinT_subst : \forall X,Y,T.
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]
+intros.unfold in H.unfold.intros.elim (in_cons_case ? ? ? ? H1)
+ [rewrite > H2;apply in_Base|elim H2;apply in_Skip2;apply (H ? H4)]
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)]]]
qed.
(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 Hcut1)
+ |simplify;elim H3;apply (in_Skip ? ? ? ? H5);intro;destruct H6;
+ apply (H2 Hcut1)]
+ |simplify in H2;simplify;elim (in_cons_case ? ? ? ? H2)
+ [rewrite > H4;apply in_Base
+ |elim H4;apply (in_Skip ? ? ? ? (H1 H6 H3) H5)]]
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
[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)]]
+ [apply (ex_intro ? ? O);intros;unfold;intro;elim (in_list_nil ? ? H1)
+ |elim H;elim (decidable_eq_nat a t)
+ [apply (ex_intro ? ? (S a));intros;intro;elim (in_cons_case ? ? ? ? H4)
+ [rewrite < H5 in H2;rewrite < H2 in H3;apply (not_le_Sn_n ? H3)
+ |elim H5;elim (H1 m ? H7);apply (le_S_S_to_le ? ? (le_S ? ? H3))]
|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)]]]
+ [apply (ex_intro ? ? (S t));intros;intro;
+ elim (in_cons_case ? ? ? ? H5)
+ [rewrite > H6 in H4;apply (not_le_Sn_n ? H4)
+ |elim H6;elim (H1 m ? H8);apply (trans_le a t m)
+ [lapply (leb_to_Prop a t);rewrite > H3 in Hletin;assumption
+ |apply (le_S_S_to_le t m (le_S (S t) m H4))]]
+ |apply (ex_intro ? ? a);intros;intro;elim (in_cons_case ? ? ? ? H5)
+ [lapply (leb_to_Prop a t);rewrite > H3 in Hletin;
+ simplify in Hletin;lapply (not_le_to_lt ? ? Hletin);
+ unfold in Hletin1;rewrite < H6 in Hletin;apply (Hletin H4)
+ |elim H6;elim (H1 ? H4 H8)]]
|elim (leb a t);autobatch]]]]
qed.
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 H3;elim (in_list_nil ? ? H5)]
+ |simplify in H1;elim (in_list_nil ? x H1)
+ |simplify in H5;elim (nat_in_list_case ? ? ? H5);autobatch
+ |simplify in H5;elim (nat_in_list_case ? ? ? H5)
+ [elim (fresh_name ((fv_type t1) @ (fv_env l)));
+ cut ((¬ (in_list ? a (fv_type t1))) ∧
+ (¬ (in_list ? 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)|elim H10;assumption]
+ |intro;apply H8;rewrite < H10;assumption]
|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]]
+ [intro;apply H7;apply natinG_or_inH_to_natinGH;right;assumption
+ |intro;apply H7;apply natinG_or_inH_to_natinGH;left;assumption]]
|apply (H2 H6)]]
qed.
(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;rewrite < Hcut2 in H6;rewrite < Hcut in H4;
+ rewrite < Hcut in H6;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
+ [rewrite < Hcut in H5;apply (H1 H5 H3)
+ |rewrite < (fv_env_extends ? x B C T U);rewrite > Hcut;rewrite > Hcut2;
+ assumption
+ |rewrite < Hcut3 in H8;rewrite > Hcut1;apply (WFT_env_incl ? ? H8);
+ rewrite < (fv_env_extends ? x B C T U);unfold;intros;
+ rewrite > Hcut;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;subst;elim (in_cons_case ? ? ? ? H5)
+ [destruct H7;assumption
+ |elim H7;elim H3;apply boundinenv_natinfv;apply (ex_intro ? ? b);
+ apply (ex_intro ? ? T);assumption]
+ |elim H7;elim (in_cons_case ? ? ? ? H5)
+ [destruct H10;elim H3;apply boundinenv_natinfv;apply (ex_intro ? ? B);
+ apply (ex_intro ? ? U);rewrite < Hcut1;assumption
+ |elim H10;apply (H2 H12 H9)]]]
qed.
(**************************************************************************)
set "baseuri" "cic:/matita/Fsub/part1a/".
-include "logic/equality.ma".
-include "nat/nat.ma".
-include "datatypes/bool.ma".
-include "nat/compare.ma".
-include "Fsub/util.ma".
include "Fsub/defn.ma".
(*** Lemma A.1 (Reflexivity) ***)
-theorem JS_Refl : \forall T,G.(WFType G T) \to (WFEnv G) \to (JSubtype G T T).
-apply Typ_len_ind;intro;elim U
- [(* FIXME *) generalize in match H1;intro;inversion H1
- [intros;destruct H6
- |intros;destruct H5
- |*:intros;destruct H9]
- |apply (SA_Refl_TVar ? ? H2);(*FIXME*)generalize in match H1;intro;
- inversion H1
- [intros;destruct H6;rewrite > Hcut;assumption
- |intros;destruct H5
- |*:intros;destruct H9]
- |apply (SA_Top ? ? H2 H1)
- |cut ((WFType G t) \land (WFType G t1))
- [elim Hcut;apply SA_Arrow
- [apply H2
- [apply t_len_arrow1
- |*:assumption]
- |apply H2
- [apply t_len_arrow2
- |*:assumption]]
- |(* no shortcut? *)
- (*FIXME*)generalize in match H3;intro;inversion H3
- [intros;destruct H8
- |intros;destruct H7
- |intros;destruct H11;rewrite > Hcut;rewrite > Hcut1;split;assumption
- |intros;destruct H11]]
- |cut (WFType G t)
- [lapply (H2 t ? ? Hcut H4)
- [apply t_len_forall1
- |apply (SA_All ? ? ? ? ? Hletin);intros;apply H2
- [rewrite < eq_t_len_TFree_subst;
- apply t_len_forall2
- |generalize in match H3;intro;inversion H3
- [intros;destruct H9
- |intros;destruct H8
- |intros;destruct H12
- |intros;destruct H12;subst;apply H9
- [assumption
- |unfold;intro;apply H5;
- elim (fresh_name ((fv_env l)@(fv_type t3)));
- cut ((\lnot (in_list ? a (fv_env l))) \land
- (\lnot (in_list ? a (fv_type t3))))
- [elim Hcut1;lapply (H9 ? H13 H14);
- lapply (fv_WFT ? X ? Hletin1)
- [simplify in Hletin2;inversion Hletin2
- [intros;lapply (inj_head_nat ? ? ? ? H16);subst;
- elim (H14 H11)
- |intros;lapply (inj_tail ? ? ? ? ? H18);
- rewrite < Hletin3 in H15;assumption]
- |apply varinT_varinT_subst;
- assumption]
- |split;unfold;intro;apply H12;apply natinG_or_inH_to_natinGH
- [right;assumption
- |left;assumption]]]]
- |apply WFE_cons;assumption]]
- |(*FIXME*)generalize in match H3;intro;inversion H3
- [intros;destruct H8
- |intros;destruct H7
- |intros;destruct H11
- |intros;destruct H11;subst;assumption]]]
+theorem JS_Refl : ∀T,G.WFType G T → WFEnv G → G ⊢ T ⊴ T.
+intros 3;elim H
+ [apply (SA_Refl_TVar l n H2 H1);
+ |apply (SA_Top l Top H1 (WFT_Top l));
+ |apply (SA_Arrow l t t1 t t1 (H2 H5) (H4 H5))
+ |apply (SA_All ? ? ? ? ? (H2 H5));intros;apply (H4 X H6)
+ [intro;apply H6;apply (fv_WFT (Forall t t1) X l)
+ [apply (WFT_Forall ? ? ? H1 H3)
+ |simplify;autobatch]
+ |autobatch]]
qed.
(*
|apply WFE_cons
[1,2:assumption
|apply (JS_to_WFT1 ? ? ? Hletin)]
- |unfold;intros;inversion H9
- [intros;lapply (inj_head ? ? ? ? H11);rewrite > Hletin1;apply in_Base
- |intros;lapply (inj_tail ? ? ? ? ? H13);rewrite < Hletin1 in H10;
- apply in_Skip;apply (H7 ? H10)]]]
+ |unfold;intros;elim (in_cons_case ? ? ? ? H9)
+ [rewrite > H10;apply in_Base
+ |elim H10;apply (in_Skip ? ? ? ? ? H11);apply (H7 ? H12)]]]
+qed.
+
+lemma decidable_eq_Typ : \forall S,T:Typ.(S = T) ∨ (S ≠ T).
+intro;elim S
+ [elim T
+ [elim (decidable_eq_nat n n1)
+ [rewrite > H;left;reflexivity
+ |right;intro;destruct H1;apply (H Hcut)]
+ |2,3:right;intro;destruct H
+ |*:right;intro;destruct H2]
+ |elim T
+ [2:elim (decidable_eq_nat n n1)
+ [rewrite > H;left;reflexivity
+ |right;intro;destruct H1;apply (H Hcut)]
+ |1,3:right;intro;destruct H
+ |*:right;intro;destruct H2]
+ |elim T
+ [3:left;reflexivity
+ |1,2:right;intro;destruct H
+ |*:right;intro;destruct H2]
+ |elim T
+ [1,2,3:right;intro;destruct H2
+ |elim (H t2)
+ [rewrite > H4;elim (H1 t3)
+ [rewrite > H5;left;reflexivity
+ |right;intro;apply H5;destruct H6;assumption]
+ |right;intro;apply H4;destruct H5;assumption]
+ |right;intro;destruct H4]
+ |elim T
+ [1,2,3:right;intro;destruct H2
+ |right;intro;destruct H4
+ |elim (H t2)
+ [rewrite > H4;elim (H1 t3)
+ [rewrite > H5;left;reflexivity
+ |right;intro;apply H5;destruct H6;assumption]
+ |right;intro;apply H4;destruct H5;assumption]]]
qed.
+lemma decidable_eq_bound: ∀b1,b2:bound.(b1 = b2) ∨ (b1 ≠ b2).
+intros;elim b1;elim b2;elim (decidable_eq_nat n n1)
+ [rewrite < H;elim (decidable_eq_Typ t t1)
+ [rewrite < H1;elim (bool_to_decidable_eq b b3)
+ [rewrite > H2;left;reflexivity
+ |right;intro;destruct H3;apply (H2 Hcut)]
+ |right;intro;destruct H2;apply (H1 Hcut1)]
+ |right;intro;destruct H1;apply (H Hcut1)]
+qed.
+
(* Lemma A.3 (Transitivity and Narrowing) *)
lemma JS_trans_narrow : \forall Q.
[apply (SA_Trans_TVar ? ? ? P)
[rewrite < H10;elim l1
[simplify;constructor 1
- |simplify;constructor 2;assumption]
+ |simplify;elim (decidable_eq_bound (mk_bound true X P) t2)
+ [rewrite < H12;apply in_Base
+ |apply (in_Skip ? ? ? ? ? H12);assumption]]
|apply H7
[lapply (H6 ? H7 H8 H9);lapply (JS_to_WFE ? ? ? Hletin);
apply (JS_weakening ? ? ? H3 ? Hletin1);unfold;intros;
- elim l1;simplify;constructor 2;assumption
+ elim l1
+ [simplify;
+ elim (decidable_eq_bound x (mk_bound true X P))
+ [rewrite < H12;apply in_Base
+ |apply (in_Skip ? ? ? ? ? H12);assumption]
+ |simplify;elim (decidable_eq_bound x t2)
+ [rewrite < H13;apply in_Base
+ |apply (in_Skip ? ? ? ? ? H13);assumption]]
|lapply (WFE_bound_bound true n t1 U ? ? H4)
[apply (JS_to_WFE ? ? ? H5)
|rewrite < Hletin;apply (H6 ? H7 H8 H9)
|rewrite > H9;rewrite > H10;elim l1;simplify
[constructor 1
- |constructor 2;assumption]]]]
+ |elim (decidable_eq_bound (mk_bound true n U) t2)
+ [rewrite > H12;apply in_Base
+ |apply (in_Skip ? ? ? ? ? H12);assumption]]]]]
|apply (SA_Trans_TVar ? ? ? t1)
[rewrite > H9 in H4;
apply (lookup_env_extends ? ? ? ? ? ? ? ? ? ? H4);
projects / helm.git / commitdiff