matita/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;autobatch width=5 size=11
  53  |simplify;apply (SA_All ? ? ? ? ? (H2 ? H6 ?? H8 H9))
  54   [assumption
  55   |apply H4
  56    [autobatch depth=4 width=4 size=8
  57    |change in ⊢ (???%) with (flift f 1);autobatch;
  58    |intro;cases n;simplify;intros;autobatch depth=4
  59    |change in ⊢ (???%) with (flift f 1);autobatch]]]
  60 qed.
  61
  62 inverter JS_indinv for JSubtype (%?%).
  63
  64 theorem narrowing:∀G,G1,U,P,M,N.
  65   G1 ⊢ P ⊴ U →
  66   (∀G2,S,T.
  67     G2@G1 ⊢ S ⊴ lift U (length ? G2) O →
  68     G2@G1 ⊢ lift U (length ? G2) O ⊴ T →
  69     G2@G1 ⊢ S ⊴ T) →
  70   G ⊢ M ⊴ N →
  71   ∀l.G=l@(mk_bound true U::G1) → l@(mk_bound true P::G1) ⊢ M ⊴ N.
  72 intros 9;elim H2;destruct;try autobatch depth=4 size=7;
  73 elim (decidable_eq_nat n (length ? l1))
  74 [apply (SA_Trans_TVar ??? P);
  75  [elim l1 in n H7
  76   [rewrite > H7;simplify;autobatch
  77   |rewrite > H8;simplify;apply le_S_S;apply H7;reflexivity]
  78  |elim l1 in n H4 H7
  79   [rewrite > H7;reflexivity
  80   |rewrite > H8;simplify;apply H4
  81    [rewrite > H8 in H7;apply H7
  82    |reflexivity]]
  83  |cut (U = t1)
  84   [change in ⊢ (? (? ? ? %) ? ?) with ([mk_bound true P]@G1);
  85    cut (S n = length ? (l1@[mk_bound true P]))
  86    [rewrite > Hcut1;rewrite < associative_append;apply H1;rewrite < Hcut1;
  87     rewrite > Hcut;rewrite > associative_append;
  88     [do 2 rewrite > lift_perm2;rewrite < Hcut;
  89      apply (JS_weakening ??? H)
  90      [simplify;autobatch
  91      |autobatch
  92      |intros;simplify;change in ⊢ (??(??%)) with (l1@[⊴P]@G1);
  93       rewrite < associative_append;
  94       rewrite > length_append;rewrite < Hcut1;rewrite < sym_plus;
  95       autobatch
  96      |applyS incl_append]
  97     |apply H6;reflexivity]
  98    |elim l1 in n H7
  99     [simplify;rewrite > H7;reflexivity
 100     |simplify;rewrite > H8;rewrite < H7
 101      [simplify;apply refl_eq
 102      |skip
 103      |reflexivity]]]
 104   |elim l1 in n H7 H4;destruct;
 105    [simplify in H4;destruct;reflexivity
 106    |simplify in H7;apply H4
 107     [2:apply H7
 108     |skip
 109     |reflexivity]]]]
 110 |apply (SA_Trans_TVar ??? t1)
 111  [cut (length ? (l1@⊴ P :: G1) = length ? (l1@⊴U::G1))
 112   [rewrite > Hcut;assumption
 113   |elim l1;simplify;autobatch]
 114  |rewrite < H4;elim l1 in n H7 0
 115   [simplify;intro;cases n1;intros
 116    [elim H7;reflexivity
 117    |reflexivity]
 118   |simplify;intros 4;elim n1
 119    [simplify;reflexivity
 120    |simplify;apply H7;intro;elim H9;autobatch]]
 121  |apply H6;reflexivity]]
 122 qed.
 123
 124 lemma JS_trans_prova: ∀T,G,R,U,f.G ⊢ R ⊴ perm T f → G ⊢ perm T f ⊴ U → G ⊢ R ⊴ U.
 125 intro;elim T;
 126   [simplify in H;simplify in H1;elim H using JS_indinv;destruct;autobatch
 127   |simplify in H1;inversion H1; intros; destruct; assumption
 128   |simplify in H2;elim H2 using JS_indinv;intros;destruct;
 129    [autobatch
 130    |simplify in H3;inversion H3;intros;destruct;autobatch depth=4 size=7]
 131   |simplify in H2;elim H2 using JS_indinv;intros;destruct;
 132    [autobatch
 133    |simplify in H3;inversion H3;intros;destruct;
 134     [apply SA_Top;autobatch
 135     |apply SA_All
 136      [apply (H ???? H8 H4);assumption
 137      |apply H1
 138       [2:apply (narrowing (mk_bound true (perm t f)::G) G ???? H8 ? H6 [])
 139        [intros;rewrite > lift_perm2 in H12;rewrite > lift_perm2 in H13;
 140         rewrite > perm_compose in H12; rewrite > perm_compose in H13;
 141         apply H
 142         [2,3:autobatch]
 143        |reflexivity]
 144       |3:assumption]]]]]
 145 qed.
 146
 147 theorem JS_trans : ∀G,T,U,V.G ⊢ T ⊴ U → G ⊢ U ⊴ V → G ⊢ T ⊴ V.
 148 intros 4;rewrite > (perm_id ? 0) in ⊢ (???% → ??%? → ?);
 149 intros;autobatch;
 150 qed.
 151
 152 theorem JS_narrow : ∀G1,G2,P,Q,T,U.
 153                        (G2 @ (mk_bound true Q :: G1)) ⊢ T ⊴ U → G1 ⊢ P ⊴ Q →
 154                        (G2 @ (mk_bound true P :: G1)) ⊢ T ⊴ U.
 155 intros; apply (narrowing ? ? ? ? ? ? H1 ? H) [|autobatch]
 156 intros;autobatch;
 157 qed.