helm/software/matita/contribs/POPLmark/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 include "Fsub/defn.ma".
  16
  17 (*** Lemma A.1 (Reflexivity) ***)
  18 theorem JS_Refl : ∀T,G.(G ⊢ T) → G ⊢ ♦ → G ⊢ T ⊴  T.
  19 intros 3; elim H;try autobatch;
  20 apply SA_All; [ autobatch | intros;autobatch depth=4 size=10]
  21 qed.
  22
  23 (*
  24  * A slightly more general variant to lemma A.2.2, where weakening isn't
  25  * defined as concatenation of any two disjoint environments, but as
  26  * set inclusion.
  27  *)
  28
  29 lemma JS_weakening : ∀G,T,U.G ⊢ T ⊴ U → ∀H.H ⊢ ♦ → G ⊆ H → H ⊢ T ⊴ U.
  30 intros 4; elim H;try autobatch depth=4 size=7;
  31 apply (SA_All ? ? ? ? ? (H2 ? H6 H7));
  32 intros; autobatch depth=6 width=4 size=13;
  33 qed.
  34
  35 inverter JS_indinv for JSubtype (%?%).
  36
  37 theorem narrowing:∀X,G,G1,U,P,M,N.
  38   G1 ⊢ P ⊴ U → (∀G2,T.G2@G1 ⊢ U ⊴ T → G2@G1 ⊢ P ⊴ T) → G ⊢ M ⊴ N →
  39   ∀l.G=l@ !X ⊴ U::G1 → l@ !X ⊴ P::G1 ⊢ M ⊴ N.
  40 intros 10.elim H2; destruct;
  41  [letin x \def fv_env. letin y ≝incl. autobatch depth=4 size=8.
  42  | autobatch depth=4 size=7;
  43  | elim (decidable_eq_nat X n)
  44     [apply (SA_Trans_TVar ? ? ? P); destruct;
  45       [ autobatch
  46       | lapply (WFE_bound_bound X t1 U ? ? H3); autobatch]
  47     | apply (SA_Trans_TVar ? ? ? t1); autobatch]
  48  | autobatch
  49  | apply SA_All;
  50     [ autobatch
  51     | intros; apply (H6 ? ? (mk_bound true X1 t2::l1)); autobatch]]
  52 qed.
  53
  54 lemma JS_trans_prova: ∀T,G1.(G1 ⊢ T) →
  55       ∀G,R,U.fv_env G1 ⊆ fv_env G → G ⊢ R ⊴ T → G ⊢ T ⊴ U → G ⊢ R ⊴ U.
  56 intros 3;elim H;clear H;
  57   [elim H3 using JS_indinv;destruct;autobatch
  58   |inversion H3; intros; destruct; assumption
  59   |*:elim H6 using JS_indinv;destruct;
  60     [1,3: autobatch
  61     |*: inversion H7; intros; destruct;
  62       [1,2: autobatch depth=4 width=4 size=9
  63       | apply SA_Top
  64          [ assumption
  65          | apply WFT_Forall;intros;autobatch depth=4]
  66       | apply SA_All
  67          [ autobatch
  68          | intros;apply (H4 X);simplify;
  69             [4: apply (narrowing X (mk_bound true X t::G) ? ? ? ? ? H11 ? ? [])
  70                [intros;apply H2;try unfold;intros;autobatch;
  71                |*:autobatch]
  72             |3:apply incl_cons;apply H5
  73             |*:autobatch]]]]]
  74 qed.
  75
  76 theorem JS_trans : ∀G,T,U,V.G ⊢ T ⊴ U → G ⊢ U ⊴ V → G ⊢ T ⊴ V.
  77 intros 5; apply (JS_trans_prova ? G); autobatch depth=2.
  78 qed.
  79
  80 theorem JS_narrow : ∀G1,G2,X,P,Q,T,U.
  81                        G2 @ !X ⊴ Q :: G1 ⊢ T ⊴ U → G1 ⊢ P ⊴ Q →
  82                        G2 @ !X ⊴ P :: G1 ⊢ T ⊴ U.
  83 intros;apply (narrowing ? ? ? ? ? ? ? H1 ? H) [|autobatch]
  84 intros;apply (JS_trans ? ? ? ? ? H2);apply (JS_weakening ? ? ? H1);autobatch.
  85 qed.