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 "logic/equality.ma".
  17 include "nat/nat.ma".
  18 include "datatypes/bool.ma".
  19 include "nat/compare.ma".
  20 include "Fsub/util.ma".
  21 include "Fsub/defn.ma".
  22
  23 (*** Lemma A.1 (Reflexivity) ***)
  24
  25 theorem JS_Refl : \forall T,G.(WFType G T) \to (WFEnv G) \to (JSubtype G T T).
  26 apply Typ_len_ind;intro;elim U
  27   [(* FIXME *) generalize in match H1;intro;inversion H1
  28      [intros;destruct H6
  29      |intros;destruct H5
  30      |*:intros;destruct H9]
  31   |apply (SA_Refl_TVar ? ? H2);(*FIXME*)generalize in match H1;intro;
  32    inversion H1
  33      [intros;destruct H6;rewrite > Hcut;assumption
  34      |intros;destruct H5
  35      |*:intros;destruct H9]
  36   |apply (SA_Top ? ? H2 H1)
  37   |cut ((WFType G t) \land (WFType G t1))
  38      [elim Hcut;apply SA_Arrow
  39         [apply H2
  40            [apply t_len_arrow1
  41            |*:assumption]
  42         |apply H2
  43            [apply t_len_arrow2
  44            |*:assumption]]
  45      |(* no shortcut? *)
  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   |cut (WFType G t)
  52      [lapply (H2 t ? ? Hcut H4)
  53         [apply t_len_forall1
  54         |apply (SA_All ? ? ? ? ? Hletin);intros;apply H2
  55            [rewrite > subst_O_nat;rewrite < eq_t_len_TFree_subst;
  56             apply t_len_forall2
  57            |generalize in match H3;intro;inversion H3
  58               [intros;destruct H9
  59               |intros;destruct H8
  60               |intros;destruct H12
  61               |intros;destruct H12;subst;apply H9
  62                  [assumption
  63                  |unfold;intro;apply H5;
  64                   elim (fresh_name ((fv_env e)@(fv_type t3)));
  65                   cut ((\lnot (in_list ? a (fv_env e))) \land
  66                        (\lnot (in_list ? a (fv_type t3))))
  67                     [elim Hcut1;lapply (H9 ? H13 H14);
  68                      lapply (fv_WFT ? X ? Hletin1)
  69                        [simplify in Hletin2;inversion Hletin2
  70                           [intros;lapply (inj_head_nat ? ? ? ? H16);subst;
  71                            elim (H14 H11)
  72                           |intros;lapply (inj_tail ? ? ? ? ? H18);
  73                            rewrite < Hletin3 in H15;assumption]
  74                        |rewrite >subst_O_nat;apply varinT_varinT_subst;
  75                         assumption]
  76                     |split;unfold;intro;apply H12;apply natinG_or_inH_to_natinGH
  77                        [right;assumption
  78                        |left;assumption]]]]
  79            |apply WFE_cons;assumption]]
  80      |(*FIXME*)generalize in match H3;intro;inversion H3
  81         [intros;destruct H8
  82         |intros;destruct H7
  83         |intros;destruct H11
  84         |intros;destruct H11;subst;assumption]]]
  85 qed.
  86
  87 (*
  88  * A slightly more general variant to lemma A.2.2, where weakening isn't
  89  * defined as concatenation of any two disjoint environments, but as
  90  * set inclusion.
  91  *)
  92
  93 lemma JS_weakening : \forall G,T,U.(JSubtype G T U) \to
  94                       \forall H.(WFEnv H) \to (incl ? G H) \to (JSubtype H T U).
  95 intros 4;elim H
  96   [apply (SA_Top ? ? H4);lapply (incl_bound_fv ? ? H5);
  97    apply (WFT_env_incl ? ? H2 ? Hletin)
  98   |apply (SA_Refl_TVar ? ? H4);lapply (incl_bound_fv ? ? H5);
  99    apply (Hletin ? H2)
 100   |lapply (H3 ? H5 H6);lapply (H6 ? H1);
 101    apply (SA_Trans_TVar ? ? ? ? Hletin1 Hletin)
 102   |lapply (H2 ? H6 H7);lapply (H4 ? H6 H7);
 103    apply (SA_Arrow ? ? ? ? ? Hletin Hletin1)
 104   |lapply (H2 ? H6 H7);apply (SA_All ? ? ? ? ? Hletin);intros;apply H4
 105      [unfold;intro;apply H8;lapply (incl_bound_fv ? ? H7);apply (Hletin1 ? H9)
 106      |apply WFE_cons
 107         [1,2:assumption
 108         |apply (JS_to_WFT1 ? ? ? Hletin)]
 109      |unfold;intros;inversion H9
 110         [intros;lapply (inj_head ? ? ? ? H11);rewrite > Hletin1;apply in_Base
 111         |intros;lapply (inj_tail ? ? ? ? ? H13);rewrite < Hletin1 in H10;
 112          apply in_Skip;apply (H7 ? H10)]]]
 113 qed.
 114
 115 (* Lemma A.3 (Transitivity and Narrowing) *)
 116
 117 lemma JS_trans_narrow : \forall Q.
 118   (\forall G,T,U.
 119      (JSubtype G T Q) \to (JSubtype G Q U) \to
 120      (JSubtype G T U)) \land
 121   (\forall G,H,X,P,M,N.
 122      (JSubtype (H @ ((mk_bound true X Q) :: G)) M N) \to
 123      (JSubtype G P Q) \to
 124      (JSubtype (H @ ((mk_bound true X P) :: G)) M N)).
 125 apply Typ_len_ind;intros 2;
 126 cut (\forall G,T,P.
 127            (JSubtype G T U) \to
 128            (JSubtype G U P) \to
 129            (JSubtype G T P))
 130   [split
 131      [assumption
 132      |cut (\forall G,M,N.(JSubtype G M N) \to
 133            \forall G1,X,G2,P.
 134               (G = G2 @ ((mk_bound true X U) :: G1)) \to
 135               (JSubtype G1 P U) \to
 136               (JSubtype (G2 @ ((mk_bound true X P) :: G1)) M N))
 137         [intros;apply (Hcut1 ? ? ? H2 ? ? ? ? ? H3);reflexivity
 138         |intros;cut (incl ? (fv_env (G2 @ ((mk_bound true X U)::G1)))
 139                     (fv_env (G2 @ ((mk_bound true X P)::G1))))
 140            [intros;generalize in match H2;generalize in match Hcut1;
 141             generalize in match Hcut;generalize in match G2;elim H1
 142               [apply SA_Top
 143                  [rewrite > H8 in H4;lapply (JS_to_WFT1 ? ? ? H3);
 144                   apply (WFE_Typ_subst ? ? ? ? ? ? ? H4 Hletin)
 145                  |rewrite > H8 in H5;apply (WFT_env_incl ? ? H5 ? H7)]
 146               |apply SA_Refl_TVar
 147                  [rewrite > H8 in H4;apply (WFE_Typ_subst ? ? ? ? ? ? ? H4);
 148                   apply (JS_to_WFT1 ? ? ? H3)
 149                  |rewrite > H8 in H5;apply (H7 ? H5)]
 150               |elim (decidable_eq_nat X n)
 151                  [apply (SA_Trans_TVar ? ? ? P)
 152                     [rewrite < H10;elim l
 153                       [simplify;constructor 1
 154                       |simplify;constructor 2;assumption]
 155                    |apply H7
 156                       [lapply (H6 ? H7 H8 H9);lapply (JS_to_WFE ? ? ? Hletin);
 157                        apply (JS_weakening ? ? ? H3 ? Hletin1);unfold;intros;
 158                        elim l;simplify;constructor 2;assumption
 159                       |lapply (WFE_bound_bound true n t1 U ? ? H4)
 160                          [apply (JS_to_WFE ? ? ? H5)
 161                          |rewrite < Hletin;apply (H6 ? H7 H8 H9)
 162                          |rewrite > H9;rewrite > H10;elim l;simplify
 163                             [constructor 1
 164                             |constructor 2;assumption]]]]
 165                 |apply (SA_Trans_TVar ? ? ? t1)
 166                    [rewrite > H9 in H4;
 167                     apply (lookup_env_extends ? ? ? ? ? ? ? ? ? ? H4);
 168                     unfold;intro;apply H10;symmetry;assumption
 169                    |apply (H6 ? H7 H8 H9)]]
 170              |apply SA_Arrow
 171                 [apply (H5 ? H8 H9 H10)
 172                 |apply (H7 ? H8 H9 H10)]
 173              |apply SA_All
 174                 [apply (H5 ? H8 H9 H10)
 175                 |intros;apply (H7 ? ? (mk_bound true X1 t2::l) H8)
 176                    [rewrite > H10;cut ((fv_env (l@(mk_bound true X P::G1))) =
 177                                        (fv_env (l@(mk_bound true X U::G1))))
 178                       [unfold;intro;apply H11;unfold;rewrite > Hcut2;assumption
 179                       |elim l
 180                          [simplify;reflexivity
 181                          |elim t4;simplify;rewrite > H12;reflexivity]]
 182                    |simplify;apply (incl_nat_cons ? ? ? H9)
 183                    |simplify;rewrite < H10;reflexivity]]]
 184           |cut ((fv_env (G2@(mk_bound true X U::G1))) =
 185                 (fv_env (G2@(mk_bound true X P::G1))))
 186              [rewrite > Hcut1;unfold;intros;assumption
 187              |elim G2
 188                 [simplify;reflexivity
 189                 |elim t;simplify;rewrite > H4;reflexivity]]]]]
 190   |intros 4;generalize in match H;elim H1
 191      [inversion H5
 192         [intros;rewrite < H8;apply (SA_Top ? ? H2 H3)
 193         |intros;destruct H9
 194         |intros;destruct H10
 195         |*:intros;destruct H11]
 196      |assumption
 197      |apply (SA_Trans_TVar ? ? ? ? H2);apply (H4 H5 H6)
 198      |inversion H7
 199         [intros;apply (SA_Top ? ? H8);rewrite < H10;apply WFT_Arrow
 200            [apply (JS_to_WFT2 ? ? ? H2)
 201            |apply (JS_to_WFT1 ? ? ? H4)]
 202         |intros;destruct H11
 203         |intros;destruct H12
 204         |intros;destruct H13;apply SA_Arrow
 205               [rewrite > H12 in H2;rewrite < Hcut in H8;
 206                lapply (H6 t2)
 207                  [elim Hletin;apply (H15 ? ? ? H8 H2)
 208                  |apply (t_len_arrow1 t2 t3)]
 209               |rewrite > H12 in H4;rewrite < Hcut1 in H10;
 210                lapply (H6 t3)
 211                  [elim Hletin;apply (H15 ? ? ? H4 H10)
 212                  |apply (t_len_arrow2 t2 t3)]]
 213            |intros;destruct H13]
 214      |inversion H7
 215         [intros;apply (SA_Top ? ? H8);rewrite < H10;apply WFT_Forall
 216            [apply (JS_to_WFT2 ? ? ? H2)
 217            |intros;lapply (H4 ? H13);lapply (JS_to_WFT1 ? ? ? Hletin);
 218             apply (WFT_env_incl ? ? Hletin1);simplify;unfold;intros;
 219             assumption]
 220         |intros;destruct H11
 221         |intros;destruct H12
 222         |intros;destruct H13
 223         |intros;destruct H13;subst;apply SA_All
 224            [lapply (H6 t4)
 225               [elim Hletin;apply (H12 ? ? ? H8 H2)
 226               |apply t_len_forall1]
 227            |intros;(*destruct H12;*)subst;
 228             lapply (H6 (subst_type_O t5 (TFree X)))
 229               [elim Hletin;apply H13
 230                  [lapply (H6 t4)
 231                     [elim Hletin1;apply (H16 e1 [] X t6);
 232                        [simplify;apply H4;assumption
 233                        |assumption]
 234                     |apply t_len_forall1]
 235                  |apply (H10 ? H12)]
 236               |rewrite > subst_O_nat;rewrite < eq_t_len_TFree_subst;
 237                apply t_len_forall2]]]]]
 238 qed.
 239
 240 theorem JS_trans : \forall G,T,U,V.(JSubtype G T U) \to
 241                                    (JSubtype G U V) \to
 242                                    (JSubtype G T V).
 243 intros;elim JS_trans_narrow;autobatch;
 244 qed.
 245
 246 theorem JS_narrow : \forall G1,G2,X,P,Q,T,U.
 247                        (JSubtype (G2 @ (mk_bound true X Q :: G1)) T U) \to
 248                        (JSubtype G1 P Q) \to
 249                        (JSubtype (G2 @ (mk_bound true X P :: G1)) T U).
 250 intros;elim JS_trans_narrow;autobatch;
 251 qed.