helm/software/matita/contribs/POPLmark/Fsub/part1adb.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 include "Fsub/defndb.ma".
  16 include "nat/lt_arith.ma".
  17 include "nat/le_arith.ma".
  18
  19 (*** Lemma A.1 (Reflexivity) ***)
  20 theorem JS_Refl : ∀T,G.WFType G T → WFEnv G → G ⊢ T ⊴  T.
  21 intros 3;elim H;autobatch depth=4 size=7;
  22 qed.
  23
  24 (*
  25  * A slightly more general variant to lemma A.2.2, where weakening isn't
  26  * defined as concatenation of any two disjoint environments, but as
  27  * set inclusion.
  28  *)
  29
  30 lemma JS_weakening : ∀G,T,U.G ⊢ T ⊴ U → ∀H.WFEnv H →
  31                      ∀f. injective nat nat f →
  32                      (∀n:ℕ.n<length bound G→f n<length bound H) →
  33                      incl G H f → H ⊢ perm T f ⊴ perm U f.
  34 intros 4; elim H;
  35  [apply SA_Top
  36   [assumption
  37   |apply (WFT_env_incl ?? H2);assumption]
  38  |simplify;apply SA_Refl_TVar
  39   [assumption
  40   |change in ⊢ (? ? %) with (perm (TVar n) f);autobatch width=4]
  41  |simplify;lapply (H4 ? H6 ? H7);
  42   lapply (H9 ? n H1)
  43   [assumption
  44   |rewrite > H2 in Hletin1;simplify in Hletin1;
  45    cut (∃t.nth bound H5 (mk_bound true Top) (f n) = mk_bound true t)
  46    [elim Hcut;rewrite > H10 in Hletin1;simplify in Hletin1;destruct;
  47     rewrite > Hcut1 in Hletin;apply (SA_Trans_TVar ?????? Hletin);autobatch
  48    |elim (nth bound H5 (mk_bound true Top) (f n)) in Hletin1;
  49     elim b in H10;simplify in H10;destruct;exists [apply t2]
  50     reflexivity]
  51   |*:assumption]
  52  |simplify;apply SA_Arrow;autobatch width=4
  53  |simplify;apply (SA_All ? ? ? ? ? (H2 ? H6 ?? H8 H9))
  54   [assumption
  55   |apply H4
  56    [apply WFE_cons
  57     [assumption
  58     |lapply (H2 ? H6 ? H7);autobatch]
  59    |change in ⊢ (???%) with (flift f 1);apply injective_flift;assumption
  60    |intro;cases n;simplify;intros;autobatch depth=4
  61    |change in ⊢ (???%) with (flift f 1);apply incl_cons;assumption]]]
  62 qed.
  63
  64 inverter JS_indinv for JSubtype (%?%).
  65
  66 theorem narrowing:∀G,G1,U,P,M,N.
  67   G1 ⊢ P ⊴ U →
  68   (∀G2,S,T.
  69     G2@G1 ⊢ S ⊴ lift U (length ? G2) O →
  70     G2@G1 ⊢ lift U (length ? G2) O ⊴ T \to
  71     G2@G1 ⊢ S ⊴ T) →
  72   G ⊢ M ⊴ N →
  73   ∀l.G=l@(mk_bound true U::G1) → l@(mk_bound true P::G1) ⊢ M ⊴ N.
  74 intros 9;elim H2;destruct;try autobatch depth=4 size=7;
  75 elim (decidable_eq_nat n (length ? l1))
  76 [apply (SA_Trans_TVar ??? P);
  77  [elim l1 in n H7
  78   [rewrite > H7;simplify;autobatch
  79   |rewrite > H8;simplify;apply le_S_S;apply H7;reflexivity]
  80  |elim l1 in n H4 H7
  81   [rewrite > H7;reflexivity
  82   |rewrite > H8;simplify;apply H4
  83    [rewrite > H8 in H7;apply H7
  84    |reflexivity]]
  85  |cut (U = t1)
  86   [change in ⊢ (? (? ? ? %) ? ?) with ([mk_bound true P]@G1);
  87    cut (S n = length ? (l1@[mk_bound true P]))
  88    [rewrite > Hcut1;rewrite < associative_append;apply H1;rewrite < Hcut1;
  89     rewrite > Hcut;rewrite > associative_append;
  90     [do 2 rewrite > lift_perm2;rewrite < Hcut;
  91      apply (JS_weakening ??? H)
  92      [simplify;autobatch
  93      |autobatch
  94      |intros;simplify;change in ⊢ (??(??%)) with (l1@[⊴P]@G1);
  95       rewrite < associative_append;
  96       rewrite > length_append;rewrite < Hcut1;rewrite < sym_plus;
  97       autobatch
  98      |applyS incl_append]
  99     |apply H6;reflexivity]
 100    |elim l1 in n H7
 101     [simplify;rewrite > H7;reflexivity
 102     |simplify;rewrite > H8;rewrite < H7
 103      [simplify;apply refl_eq
 104      |skip
 105      |reflexivity]]]
 106   |elim l1 in n H7 H4;destruct;
 107    [simplify in H4;destruct;reflexivity
 108    |simplify in H7;apply H4
 109     [2:apply H7
 110     |skip
 111     |reflexivity]]]]
 112 |apply (SA_Trans_TVar ??? t1)
 113  [cut (length ? (l1@⊴ P :: G1) = length ? (l1@⊴U::G1))
 114   [rewrite > Hcut;assumption
 115   |elim l1;simplify;autobatch]
 116  |rewrite < H4;elim l1 in n H7 0
 117   [simplify;intro;cases n1;intros
 118    [elim H7;reflexivity
 119    |reflexivity]
 120   |simplify;intros 4;elim n1
 121    [simplify;reflexivity
 122    |simplify;apply H7;intro;elim H9;autobatch]]
 123  |apply H6;reflexivity]]
 124 qed.
 125
 126 lemma JS_trans_prova: ∀T,G1.WFType G1 T →
 127 ∀G,R,U,f.injective ?? f → length ? G1 ≤ length ? G → G ⊢ R ⊴ perm T f → G ⊢ perm T f ⊴ U → G ⊢ R ⊴ U.
 128 intros 3;elim H;clear H; try autobatch;
 129   [simplify in H5;simplify in H6;elim H5 using JS_indinv;destruct;autobatch
 130   |simplify in H4;inversion H4; intros; destruct; assumption
 131   |simplify in H7;elim H7 using JS_indinv;intros;destruct;
 132    [autobatch
 133    |simplify in H8;inversion H8;intros;destruct;
 134     [apply SA_Top;autobatch;
 135     |apply SA_Arrow
 136      [apply (H2 ?????? H12 H);assumption
 137      |apply (H4 ?????? H10 H14);assumption]]]
 138   |simplify in H7;elim H7 using JS_indinv;intros;destruct;
 139    [autobatch
 140    |simplify in H8;inversion H8;intros;destruct;
 141     [apply SA_Top;autobatch
 142     |apply SA_All
 143      [apply (H2 ?????? H12 H);assumption
 144      |apply H4
 145       [3:simplify;apply le_S_S;assumption
 146       |4:apply (narrowing (mk_bound true (perm t f)::G) G ???? H12 ? H10 [])
 147        [intros;rewrite > lift_perm2 in H16;rewrite > lift_perm2 in H17;
 148         rewrite > perm_compose in H16; rewrite > perm_compose in H17;
 149         apply H2
 150         [3:apply (trans_le ??? H6);rewrite > length_append;autobatch
 151         |4:apply H16
 152         |5:apply H17
 153         |2:apply injective_compose;autobatch]
 154        |reflexivity]
 155       |5:assumption
 156       |2:change in ⊢ (???%) with (flift f 1);autobatch]]]]]
 157 qed.
 158
 159 theorem JS_trans : ∀G,T,U,V.G ⊢ T ⊴ U → G ⊢ U ⊴ V → G ⊢ T ⊴ V.
 160 intros 4;rewrite > (perm_id ? 0) in ⊢ (???% → ??%? → ?);
 161 intros;apply (JS_trans_prova ????????? H H1)
 162 [apply G
 163 |rewrite < perm_id in H;autobatch
 164 |simplify;intros;assumption
 165 |apply le_n]
 166 qed.
 167
 168 theorem JS_narrow : ∀G1,G2,P,Q,T,U.
 169                        (G2 @ (mk_bound true Q :: G1)) ⊢ T ⊴ U → G1 ⊢ P ⊴ Q →
 170                        (G2 @ (mk_bound true P :: G1)) ⊢ T ⊴ U.
 171 intros; apply (narrowing ? ? ? ? ? ? H1 ? H) [|autobatch]
 172 intros;autobatch;
 173 qed.