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