include "Fsub/util.ma".
(*** representation of Fsub types ***)
-inductive Typ : Set \def
+inductive Typ : Type \def
| TVar : nat \to Typ (* type var *)
| TFree: nat \to Typ (* free type name *)
| Top : Typ (* maximum type *)
| Forall : Typ \to Typ \to Typ. (* universal type *)
(*** representation of Fsub terms ***)
-inductive Term : Set \def
+inductive Term : Type \def
| Var : nat \to Term (* variable *)
| Free : nat \to Term (* free name *)
| Abs : Typ \to Term \to Term (* abstraction *)
(* representation of bounds *)
-record bound : Set \def {
+record bound : Type \def {
istype : bool; (* is subtyping bound? *)
name : nat ; (* name *)
btype : Typ (* type to which the name is bound *)
\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 s;simplify in H1;inversion H1
+ |intros 3;elim t;simplify in H1;inversion H1
[intros;rewrite < H2;simplify;apply ex_intro
[apply b
|apply ex_intro
- [apply t
+ [apply t1
|lapply (inj_head_nat ? ? ? ? H3);rewrite > H2;rewrite < Hletin;
apply in_Base]]
|intros;lapply (inj_tail ? ? ? ? ? H5);rewrite < Hletin in H2;
(var_in_env x G) \lor (var_in_env x H).
intros 3.elim H 0
[simplify;intro;left;assumption
- |intros 2;elim s;simplify in H2;inversion H2
+ |intros 2;elim t;simplify in H2;inversion H2
[intros;lapply (inj_head_nat ? ? ? ? H4);rewrite > Hletin;right;
simplify;constructor 1
|intros;lapply (inj_tail ? ? ? ? ? H6);
intros.elim H1 0
[elim H
[simplify;assumption
- |elim s;simplify;constructor 2;apply (H2 H3)]
+ |elim t;simplify;constructor 2;apply (H2 H3)]
|elim H 0
[simplify;intro;lapply (in_list_nil nat x H2);elim Hletin
- |intros 2;elim s;simplify in H3;inversion H3
+ |intros 2;elim t;simplify in H3;inversion H3
[intros;lapply (inj_head_nat ? ? ? ? H5);rewrite > Hletin;simplify;
constructor 1
|intros;simplify;constructor 2;rewrite < H6;apply H2;
(fv_env (H @ ((mk_bound C x U) :: G))).
intros;elim H
[simplify;reflexivity
- |elim s;simplify;rewrite > H1;reflexivity]
+ |elim t;simplify;rewrite > H1;reflexivity]
qed.
lemma lookup_env_extends : \forall G,H,B,C,D,T,U,V,x,y.
[1,3:elim Hcut;elim H4;elim H5;clear Hcut H4 H5;rewrite > (H H6 H8);
rewrite > (H1 H7 H9);reflexivity
|*:split
- [1,3:split;unfold;intro;apply H2;apply natinG_or_inH_to_natinGH;auto
- |*:split;unfold;intro;apply H3;apply natinG_or_inH_to_natinGH;auto]]]
+ [1,3:split;unfold;intro;apply H2;apply natinG_or_inH_to_natinGH;autobatch
+ |*:split;unfold;intro;apply H3;apply natinG_or_inH_to_natinGH;autobatch]]]
qed.
lemma subst_type_nat_swap : \forall u,v,T,X,m.
(in_list ? (mk_bound B (swap u v x) (swap_Typ u v T)) (swap_Env u v G)).
intros 6;elim G 0
[intros;elim (in_list_nil ? ? H)
- |intro;elim s;simplify;inversion H1
+ |intro;elim t;simplify;inversion H1
[intros;lapply (inj_head ? ? ? ? H3);rewrite < H2 in Hletin;
destruct Hletin;rewrite > Hcut;rewrite > Hcut1;rewrite > Hcut2;
apply in_Base
intros;split
[elim G 0
[simplify;intro;elim (in_list_nil ? ? H)
- |intro;elim s 0;simplify;intros;inversion H1
+ |intro;elim t 0;simplify;intros;inversion H1
[intros;lapply (inj_head_nat ? ? ? ? H3);rewrite > Hletin;apply in_Base
|intros;lapply (inj_tail ? ? ? ? ? H5);rewrite < Hletin in H2;
rewrite > H4 in H;apply in_Skip;apply (H H2)]]
|elim G 0
[simplify;intro;elim (in_list_nil ? ? H)
- |intro;elim s 0;simplify;intros;inversion H1
+ |intro;elim t 0;simplify;intros;inversion H1
[intros;lapply (inj_head_nat ? ? ? ? H3);rewrite < H2 in Hletin;
lapply (swap_inj ? ? ? ? Hletin);rewrite > Hletin1;apply in_Base
|intros;lapply (inj_tail ? ? ? ? ? H5);rewrite < Hletin in H2;
[assumption|apply nil_cons]
|intros;lapply (sym_eq ? ? ? H5);absurd (a1::l1 = [])
[assumption|apply nil_cons]]]
- |elim H;lapply (decidable_eq_nat a s);elim Hletin
+ |elim H;lapply (decidable_eq_nat a t);elim Hletin
[apply ex_intro
[apply (S a)
|intros;unfold;intro;inversion H4
rewrite < H7 in H5;
apply (H1 m ? H5);lapply (le_S ? ? H3);
apply (le_S_S_to_le ? ? Hletin2)]]
- |cut ((leb a s) = true \lor (leb a s) = false)
+ |cut ((leb a t) = true \lor (leb a t) = false)
[elim Hcut
[apply ex_intro
- [apply (S s)
+ [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 s);rewrite > H3 in Hletin2;
+ |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 s);rewrite > H3 in Hletin1;
+ |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);
|intros;lapply (inj_tail ? ? ? ? ? H9);
rewrite < Hletin3 in H6;rewrite < H8 in H6;
apply (H1 ? H4 H6)]]]
- |elim (leb a s);auto]]]]
+ |elim (leb a t);autobatch]]]]
qed.
(*** lemmas on well-formedness ***)
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
+ |intros 2;elim t;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 = [])
+ [intros;absurd ((mk_bound b n t1)::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 = [])
+ |apply (WFT_swap u v l t1);inversion H1
+ [intro;absurd ((mk_bound b n t1)::l = [])
[assumption|apply nil_cons]
|intros;lapply (inj_head ? ? ? ? H6);lapply (inj_tail ? ? ? ? ? H6);
destruct Hletin;rewrite > Hletin1;rewrite > Hcut2;assumption]]]
[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 (leb (t_len T1) (t_len T2));autobatch]
|elim T1;simplify;reflexivity]
qed.
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 (leb (t_len T1) (t_len T2));autobatch]
|elim T1;simplify;reflexivity]
qed.
[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 (leb (t_len T1) (t_len T2));autobatch]
|elim T1;simplify;reflexivity]
qed.
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 (leb (t_len T1) (t_len T2));autobatch]
|elim T1;simplify;reflexivity]
qed.
(swap_Env u v G) = G.
intros 3.elim G 0
[simplify;intros;reflexivity
- |intros 2;elim s 0;simplify;intros;lapply (notin_cons ? ? ? ? H2);
+ |intros 2;elim t 0;simplify;intros;lapply (notin_cons ? ? ? ? H2);
lapply (notin_cons ? ? ? ? H3);elim Hletin;elim Hletin1;
lapply (swap_other ? ? ? H4 H6);lapply (WFE_consG_to_WFT ? ? ? ? H1);
- cut (\lnot (in_list ? u (fv_type t)))
- [cut (\lnot (in_list ? v (fv_type t)))
+ cut (\lnot (in_list ? u (fv_type t1)))
+ [cut (\lnot (in_list ? v (fv_type t1)))
[lapply (swap_Typ_not_free ? ? ? Hcut Hcut1);
lapply (WFE_consG_WFE_G ? ? H1);
lapply (H Hletin5 H5 H7);
|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)]
- |intros;simplify;generalize in match H2;elim s;simplify in H4;
+ |intros;simplify;generalize in match H2;elim t;simplify in H4;
inversion H4
- [intros;absurd (mk_bound b n t::l@(mk_bound B x T::G)=Empty)
+ [intros;absurd (mk_bound b n t1::l@(mk_bound B x T::G)=Empty)
[assumption
|apply nil_cons]
|intros;lapply (inj_tail ? ? ? ? ? H9);lapply (inj_head ? ? ? ? H9);