matita/library/Fsub/part1a.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 set "baseuri" "cic:/matita/Fsub/part1a/".
  16 include "library/logic/equality.ma".
  17 include "library/nat/nat.ma".
  18 include "library/datatypes/bool.ma".
  19 include "library/nat/compare.ma".
  20 include "Fsub/defn.ma".
  21
  22 theorem JS_Refl : \forall T,G.(WFType G T) \to (WFEnv G) \to (JSubtype G T T).
  23 apply Typ_len_ind;intro;elim U
  24   [(* FIXME *) generalize in match H1;intro;inversion H1
  25      [intros;destruct H6
  26      |intros;destruct H5
  27      |intros;destruct H9
  28      |intros;destruct H9]
  29   |apply (SA_Refl_TVar ? ? H2);(*FIXME*)generalize in match H1;intro;
  30    inversion H1
  31      [intros;destruct H6;rewrite > Hcut;assumption
  32      |intros;destruct H5
  33      |intros;destruct H9
  34      |intros;destruct H9]
  35   |apply (SA_Top ? ? H2 H1)
  36   |cut ((WFType G t) \land (WFType G t1))
  37      [elim Hcut;apply SA_Arrow
  38         [apply H2
  39            [apply t_len_arrow1
  40            |assumption
  41            |assumption]
  42         |apply H2
  43            [apply t_len_arrow2
  44            |assumption
  45            |assumption]]
  46      |(*FIXME*)generalize in match H3;intro;inversion H3
  47         [intros;destruct H8
  48         |intros;destruct H7
  49         |intros;destruct H11;rewrite > Hcut;rewrite > Hcut1;split;assumption
  50         |intros;destruct H11]]
  51   |elim (fresh_name ((fv_type t1) @ (fv_env G)));
  52    cut ((\lnot (in_list ? a (fv_type t1))) \land
  53         (\lnot (in_list ? a (fv_env G))))
  54      [elim Hcut;cut (WFType G t)
  55         [apply (SA_All2 ? ? ? ? ? a ? H7 H6 H6)
  56            [apply H2
  57               [apply t_len_forall1
  58               |assumption
  59               |assumption]
  60            |apply H2
  61               [rewrite > subst_O_nat;rewrite < eq_t_len_TFree_subst;
  62                apply t_len_forall2
  63               |(*FIXME*)generalize in match H3;intro;inversion H3
  64                  [intros;destruct H11
  65                  |intros;destruct H10
  66                  |intros;destruct H14
  67                  |intros;destruct H14;rewrite < Hcut2 in H11;
  68                   rewrite < Hcut3 in H11;rewrite < H13;rewrite < H13 in H11;
  69                   apply (H11 ? H7 H6)]
  70               |apply WFE_cons;assumption]]
  71         |(*FIXME*)generalize in match H3;intro;inversion H3
  72            [intros;destruct H11
  73            |intros;destruct H10
  74            |intros;destruct H14
  75            |intros;destruct H14;rewrite > Hcut1;assumption]]
  76      |split;unfold;intro;apply H5;apply natinG_or_inH_to_natinGH;auto]]
  77 qed.
  78
  79 lemma env_append_weaken : \forall G,H.(WFEnv (H @ G)) \to
  80                              (incl ? G (H @ G)).
  81 intros 2;elim H
  82   [simplify;unfold;intros;assumption
  83   |simplify in H2;simplify;unfold;intros;apply in_Skip;apply H1
  84      [apply (WFE_consG_WFE_G ? ? H2)
  85      |assumption]]
  86 qed.
  87
  88 lemma JS_weakening : \forall G,T,U.(JSubtype G T U) \to
  89                       \forall H.(WFEnv H) \to (incl ? G H) \to (JSubtype H T U).
  90 intros 4;elim H
  91   [apply (SA_Top ? ? H4);lapply (incl_bound_fv ? ? H5);
  92    apply (WFT_env_incl ? ? H2 ? Hletin)
  93   |apply (SA_Refl_TVar ? ? H4);lapply (incl_bound_fv ? ? H5);
  94    apply (Hletin ? H2)
  95   |lapply (H3 ? H5 H6);lapply (H6 ? H1);
  96    apply (SA_Trans_TVar ? ? ? ? Hletin1 Hletin)
  97   |lapply (H2 ? H6 H7);lapply (H4 ? H6 H7);
  98    apply (SA_Arrow ? ? ? ? ? Hletin Hletin1)
  99   |lapply (H2 ? H6 H7);apply (SA_All ? ? ? ? ? Hletin);intros;apply H4
 100      [unfold;intro;apply H8;lapply (incl_bound_fv ? ? H7);apply (Hletin1 ? H9)
 101      |apply WFE_cons
 102         [assumption
 103         |assumption
 104         |lapply (incl_bound_fv ? ? H7);apply (WFT_env_incl ? ? ? ? Hletin1);
 105          apply (JS_to_WFT1 ? ? ? H1)]
 106      |unfold;intros;inversion H9
 107         [intros;lapply (inj_head ? ? ? ? H11);rewrite > Hletin1;apply in_Base
 108         |intros;lapply (inj_tail ? ? ? ? ? H13);rewrite < Hletin1 in H10;
 109          apply in_Skip;apply (H7 ? H10)]]]
 110 qed.
 111
 112 lemma fv_env_extends : \forall H,x,B,C,T,U,G.
 113                           (fv_env (H @ ((mk_bound B x T) :: G))) =
 114                           (fv_env (H @ ((mk_bound C x U) :: G))).
 115 intros;elim H
 116   [simplify;reflexivity
 117   |elim s;simplify;rewrite > H1;reflexivity]
 118 qed.
 119
 120 lemma WFE_Typ_subst : \forall H,x,B,C,T,U,G.
 121                       (WFEnv (H @ ((mk_bound B x T) :: G))) \to (WFType G U) \to
 122                       (WFEnv (H @ ((mk_bound C x U) :: G))).
 123 intros 7;elim H 0
 124   [simplify;intros;(*FIXME*)generalize in match H1;intro;inversion H1
 125      [intros;lapply (nil_cons ? G (mk_bound B x T));lapply (Hletin H4);
 126       elim Hletin1
 127      |intros;lapply (inj_tail ? ? ? ? ? H8);lapply (inj_head ? ? ? ? H8);
 128       destruct Hletin1;rewrite < Hletin in H6;rewrite < Hletin in H4;
 129       rewrite < Hcut1 in H6;apply (WFE_cons ? ? ? ? H4 H6 H2)]
 130   |intros;simplify;generalize in match H2;elim s;simplify in H4;
 131    inversion H4
 132      [intros;absurd (mk_bound b n t::l@(mk_bound B x T::G)=Empty)
 133         [assumption
 134         |apply nil_cons]
 135      |intros;lapply (inj_tail ? ? ? ? ? H9);lapply (inj_head ? ? ? ? H9);
 136       destruct Hletin1;apply WFE_cons
 137         [apply H1
 138            [rewrite > Hletin;assumption
 139            |assumption]
 140         |rewrite > Hcut1;generalize in match H7;rewrite < Hletin;
 141          rewrite > (fv_env_extends ? x B C T U);intro;assumption
 142         |rewrite < Hletin in H8;rewrite > Hcut2;
 143          apply (WFT_env_incl ? ? H8);rewrite > (fv_env_extends ? x B C T U);
 144          unfold;intros;assumption]]]
 145 qed.
 146
 147 lemma lookup_env_extends : \forall G,H,B,C,D,T,U,V,x,y.
 148             (in_list ? (mk_bound D y V) (H @ ((mk_bound C x U) :: G))) \to
 149             (y \neq x) \to
 150             (in_list ? (mk_bound D y V) (H @ ((mk_bound B x T) :: G))).
 151 intros 10;elim H
 152   [simplify in H1;(*FIXME*)generalize in match H1;intro;inversion H1
 153      [intros;lapply (inj_head ? ? ? ? H5);rewrite < H4 in Hletin;
 154       destruct Hletin;absurd (y = x) [symmetry;assumption|assumption]
 155      |intros;simplify;lapply (inj_tail ? ? ? ? ? H7);rewrite > Hletin;
 156       apply in_Skip;assumption]
 157   |(*FIXME*)generalize in match H2;intro;inversion H2
 158      [intros;simplify in H6;lapply (inj_head ? ? ? ? H6);rewrite > Hletin;
 159       simplify;apply in_Base
 160      |simplify;intros;lapply (inj_tail ? ? ? ? ? H8);rewrite > Hletin in H1;
 161       rewrite > H7 in H1;apply in_Skip;apply (H1 H5 H3)]]
 162 qed.
 163
 164 lemma t_len_pred: \forall T,m.(S (t_len T)) \leq m \to (t_len T) \leq (pred m).
 165 intros 2;elim m
 166   [elim (not_le_Sn_O ? H)
 167   |simplify;apply (le_S_S_to_le ? ? H1)]
 168 qed.
 169
 170 lemma pred_m_lt_m : \forall m,T.(t_len T) \leq m \to (pred m) < m.
 171 intros 2;elim m 0
 172   [elim T
 173      [simplify in H;elim (not_le_Sn_n ? H)
 174      |simplify in H;elim (not_le_Sn_n ? H)
 175      |simplify in H;elim (not_le_Sn_n ? H)
 176      |simplify in H2;elim (not_le_Sn_O ? H2)
 177      |simplify in H2;elim (not_le_Sn_O ? H2)]
 178   |intros;simplify;unfold;constructor 1]
 179 qed.
 180
 181 lemma WFE_bound_bound : \forall B,x,T,U,G. (WFEnv G) \to
 182                                   (in_list ? (mk_bound B x T) G) \to
 183                                   (in_list ? (mk_bound B x U) G) \to T = U.
 184 intros 6;elim H
 185   [lapply (in_list_nil ? ? H1);elim Hletin
 186   |inversion H6
 187      [intros;rewrite < H7 in H8;lapply (inj_head ? ? ? ? H8);
 188       rewrite > Hletin in H5;inversion H5
 189         [intros;rewrite < H9 in H10;lapply (inj_head ? ? ? ? H10);
 190          destruct Hletin1;symmetry;assumption
 191         |intros;lapply (inj_tail ? ? ? ? ? H12);rewrite < Hletin1 in H9;
 192          rewrite < H11 in H9;lapply (boundinenv_natinfv x e)
 193            [destruct Hletin;rewrite < Hcut1 in Hletin2;lapply (H3 Hletin2);
 194             elim Hletin3
 195            |apply ex_intro
 196               [apply B|apply ex_intro [apply T|assumption]]]]
 197      |intros;lapply (inj_tail ? ? ? ? ? H10);rewrite < H9 in H7;
 198       rewrite < Hletin in H7;(*FIXME*)generalize in match H5;intro;inversion H5
 199         [intros;rewrite < H12 in H13;lapply (inj_head ? ? ? ? H13);
 200          destruct Hletin1;rewrite < Hcut1 in H7;
 201          lapply (boundinenv_natinfv n e)
 202            [lapply (H3 Hletin2);elim Hletin3
 203            |apply ex_intro
 204               [apply B|apply ex_intro [apply U|assumption]]]
 205         |intros;apply (H2 ? H7);rewrite > H14;lapply (inj_tail ? ? ? ? ? H15);
 206          rewrite > Hletin1;assumption]]]
 207 qed.
 208
 209 lemma JS_trans_narrow : \forall n.
 210   (\forall G,T,Q,U.
 211      (t_len Q) \leq n \to (JSubtype G T Q) \to (JSubtype G Q U) \to
 212      (JSubtype G T U)) \land
 213   (\forall G,H,X,P,Q,M,N.
 214      (t_len Q) \leq n \to
 215      (JSubtype (H @ ((mk_bound true X Q) :: G)) M N) \to
 216      (JSubtype G P Q) \to
 217      (JSubtype (H @ ((mk_bound true X P) :: G)) M N)).
 218 intro;apply (nat_elim1 n);intros 2;
 219 cut (\forall G,T,Q.(JSubtype G T Q) \to
 220         \forall U.(t_len Q \leq m) \to (JSubtype G Q U) \to (JSubtype G T U))
 221   [cut (\forall G,M,N.(JSubtype G M N) \to
 222            \forall G1,X,Q,G2,P.
 223               (G = G2 @ ((mk_bound true X Q) :: G1)) \to (t_len Q) \leq m \to
 224               (JSubtype G1 P Q) \to
 225               (JSubtype (G2 @ ((mk_bound true X P) :: G1)) M N))
 226      [split
 227         [intros;apply (Hcut ? ? ? H2 ? H1 H3)
 228         |intros;apply (Hcut1 ? ? ? H3 ? ? ? ? ? ? H2 H4);reflexivity]
 229      |intros 9;cut (incl ? (fv_env (G2 @ ((mk_bound true X Q)::G1)))
 230                    (fv_env (G2 @ ((mk_bound true X P)::G1))))
 231         [intros;
 232 (*                 [rewrite > H6 in H2;lapply (JS_to_WFT1 ? ? ? H8);
 233                   apply (WFE_Typ_subst ? ? ? ? ? ? ? H2 Hletin) *)
 234          generalize in match Hcut1;generalize in match H2;
 235          generalize in match H1;generalize in match H4;
 236          generalize in match G1;generalize in match G2;elim H1
 237            [apply SA_Top
 238               [rewrite > H9 in H5;lapply (JS_to_WFT1 ? ? ? H7);
 239                apply (WFE_Typ_subst ? ? ? ? ? ? ? H5 Hletin)
 240               |rewrite > H9 in H6;apply (WFT_env_incl ? ? H6);elim l
 241                  [simplify;unfold;intros;assumption
 242                  |simplify;apply (incl_nat_cons ? ? ? H11)]]
 243            |apply SA_Refl_TVar
 244               [rewrite > H9 in H5;lapply (JS_to_WFT1 ? ? ? H7);
 245                apply (WFE_Typ_subst ? ? ? ? ? ? ? H5 Hletin)
 246               |apply H10;rewrite < H9;assumption]
 247            |elim (decidable_eq_nat X n1)
 248               [apply (SA_Trans_TVar ? ? ? P)
 249                  [rewrite < H12;elim l
 250                     [simplify;apply in_Base
 251                     |simplify;apply in_Skip;assumption]
 252                  |lapply (JS_to_WFE ? ? ? H9);rewrite > H10 in Hletin;
 253                   rewrite > H10 in H5;
 254                   lapply (WFE_bound_bound ? ? ? Q ? Hletin H5)
 255                     [lapply (H7 ? ? H8 H6 H10 H11);rewrite > Hletin1 in Hletin2;
 256                      apply (Hcut ? ? ? ? ? H3 Hletin2);
 257                      lapply (JS_to_WFE ? ? ? Hletin2);
 258                      apply (JS_weakening ? ? ? H8 ? Hletin3);unfold;intros;
 259                      elim l;simplify;apply in_Skip;assumption
 260                     |rewrite > H12;elim l
 261                        [simplify;apply in_Base
 262                        |simplify;apply in_Skip;assumption]]]
 263               |rewrite > H10 in H5;apply (SA_Trans_TVar ? ? ? t1)
 264                  [apply (lookup_env_extends ? ? ? ? ? ? ? ? ? ? H5);unfold;
 265                   intro;apply H12;symmetry;assumption
 266                  |apply (H7 ? ? H8 H6 H10 H11)]]
 267            |apply SA_Arrow
 268               [apply (H6 ? ? H9 H5 H11 H12)
 269               |apply (H8 ? ? H9 H7 H11 H12)]
 270            |apply SA_All
 271               [apply (H6 ? ? H9 H5 H11 H12)
 272               |intros;apply (H8 ? ? (mk_bound true X1 t2::l) l1)
 273                  [unfold;intro;apply H13;rewrite > H11 in H14;apply (H12 ? H14)
 274                  |assumption
 275                  |apply H7;rewrite > H11;unfold;intro;apply H13;apply (H12 ? H14)
 276                  |simplify;rewrite < H11;reflexivity
 277                  |simplify;apply incl_nat_cons;assumption]]]
 278         |elim G2 0
 279            [simplify;unfold;intros;assumption
 280            |intro;elim s 0;simplify;intros;apply incl_nat_cons;assumption]]]
 281   |intros 4;(*generalize in match H1;*)elim H1
 282      [inversion H5
 283         [intros;rewrite < H8;apply (SA_Top ? ? H2 H3)
 284         |intros;destruct H9
 285         |intros;destruct H10
 286         |intros;destruct H11
 287         |intros;destruct H11]
 288      |assumption
 289      |apply (SA_Trans_TVar ? ? ? ? H2);apply (H4 ? H5 H6)
 290      |inversion H7
 291         [intros;apply (SA_Top ? ? H8);rewrite < H10;apply WFT_Arrow
 292            [apply (JS_to_WFT2 ? ? ? H2)
 293            |apply (JS_to_WFT1 ? ? ? H4)]
 294         |intros;destruct H11
 295         |intros;destruct H12
 296         |intros;destruct H13;elim (H (pred m))
 297            [apply SA_Arrow
 298               [rewrite > H12 in H2;rewrite < Hcut in H8;
 299                apply (H15 ? ? ? ? ? H8 H2);lapply (t_len_arrow1 t2 t3);
 300                unfold in Hletin;lapply (trans_le ? ? ? Hletin H6);
 301                apply (t_len_pred ? ? Hletin1)
 302               |rewrite > H12 in H4;rewrite < Hcut1 in H10;
 303                apply (H15 ? ? ? ? ? H4 H10);lapply (t_len_arrow2 t2 t3);
 304                unfold in Hletin;lapply (trans_le ? ? ? Hletin H6);
 305                apply (t_len_pred ? ? Hletin1)]
 306            |apply (pred_m_lt_m ? ? H6)]
 307         |intros;destruct H13]
 308      |inversion H7
 309         [intros;apply (SA_Top ? ? H8);rewrite < H10;apply WFT_Forall
 310            [apply (JS_to_WFT2 ? ? ? H2)
 311            |intros;lapply (H4 ? H13);lapply (JS_to_WFT1 ? ? ? Hletin);
 312             apply (WFT_env_incl ? ? Hletin1);simplify;unfold;intros;
 313             assumption]
 314         |intros;destruct H11
 315         |intros;destruct H12
 316         |intros;destruct H13
 317         |intros;destruct H13;elim (H (pred m))
 318            [elim (fresh_name ((fv_env e1) @ (fv_type t1) @ (fv_type t7)));
 319             cut ((\lnot (in_list ? a (fv_env e1))) \land
 320                  (\lnot (in_list ? a (fv_type t1))) \land
 321                  (\lnot (in_list ? a (fv_type t7))))
 322               [elim Hcut2;elim H18;clear Hcut2 H18;apply (SA_All2 ? ? ? ? ? a)
 323                  [rewrite < Hcut in H8;rewrite > H12 in H2;
 324                   apply (H15 ? ? ? ? ? H8 H2);lapply (t_len_forall1 t2 t3);
 325                   unfold in Hletin;lapply (trans_le ? ? ? Hletin H6);
 326                   apply (t_len_pred ? ? Hletin1)
 327                  |assumption
 328                  |assumption
 329                  |assumption
 330                  |lapply (H10 ? H20);rewrite > H12 in H5;
 331                   lapply (H5 ? H20 (subst_type_O t5 (TFree a)))
 332                     [apply (H15 ? ? ? ? ? ? Hletin)
 333                        [rewrite < Hcut1;rewrite > subst_O_nat;
 334                         rewrite < eq_t_len_TFree_subst;
 335                         lapply (t_len_forall2 t2 t3);unfold in Hletin2;
 336                         lapply (trans_le ? ? ? Hletin2 H6);
 337                         apply (t_len_pred ? ? Hletin3)
 338                        |rewrite < Hcut in H8;
 339                         apply (H16 e1 (nil ?) a t6 t2 ? ? ? Hletin1 H8);
 340                         lapply (t_len_forall1 t2 t3);unfold in Hletin2;
 341                         lapply (trans_le ? ? ? Hletin2 H6);
 342                         apply (t_len_pred ? ? Hletin3)]
 343                     |rewrite > subst_O_nat;rewrite < eq_t_len_TFree_subst;
 344                      lapply (t_len_forall2 t2 t3);unfold in Hletin1;
 345                      lapply (trans_le ? ? ? Hletin1 H6);
 346                      apply (trans_le ? ? ? ? Hletin2);constructor 2;
 347                      constructor 1
 348                     |rewrite > Hcut1;rewrite > H12 in H4;
 349                      lapply (H4 ? H20);rewrite < Hcut1;apply JS_Refl
 350                        [apply (JS_to_WFT2 ? ? ? Hletin1)
 351                        |apply (JS_to_WFE ? ? ? Hletin1)]]]
 352               |split
 353                  [split
 354                     [unfold;intro;apply H17;
 355                      apply (natinG_or_inH_to_natinGH ? (fv_env e1));right;
 356                      assumption
 357                     |unfold;intro;apply H17;
 358                      apply (natinG_or_inH_to_natinGH
 359                                ((fv_type t1) @ (fv_type t7)));left;
 360                      apply natinG_or_inH_to_natinGH;right;assumption]
 361                  |unfold;intro;apply H17;
 362                   apply (natinG_or_inH_to_natinGH
 363                             ((fv_type t1) @ (fv_type t7)));left;
 364                   apply natinG_or_inH_to_natinGH;left;assumption]]
 365            |apply (pred_m_lt_m ? ? H6)]]]]
 366 qed.
 367
 368 theorem JS_trans : \forall G,T,U,V.(JSubtype G T U) \to
 369                                    (JSubtype G U V) \to
 370                                    (JSubtype G T V).
 371 intros;elim (JS_trans_narrow (t_len U));apply (H2 ? ? ? ? ? H H1);constructor 1;
 372 qed.
 373
 374 theorem JS_narrow : \forall G1,G2,X,P,Q,T,U.
 375                        (JSubtype (G2 @ (mk_bound true X Q :: G1)) T U) \to
 376                        (JSubtype G1 P Q) \to
 377                        (JSubtype (G2 @ (mk_bound true X P :: G1)) T U).
 378 intros;elim (JS_trans_narrow (t_len Q));apply (H3 ? ? ? ? ? ? ? ? H H1);
 379 constructor 1;
 380 qed.