helm/software/matita/contribs/POPLmark/Fsub/defn.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/util.ma".
  16
  17 (*** representation of Fsub types ***)
  18 inductive Typ : Set ≝
  19   | TVar : nat → Typ            (* type var *)
  20   | TFree: nat → Typ            (* free type name *)
  21   | Top : Typ                     (* maximum type *)
  22   | Arrow : Typ → Typ → Typ   (* functions *)
  23   | Forall : Typ → Typ → Typ. (* universal type *)
  24
  25 (* representation of bounds *)
  26
  27 record bound : Set ≝ {
  28                           istype : bool;    (* is subtyping bound? *)
  29                           name   : nat ;    (* name *)
  30                           btype  : Typ      (* type to which the name is bound *)
  31                         }.
  32
  33 (*** Various kinds of substitution, not all will be used probably ***)
  34
  35 (* substitutes i-th dangling index in type T with type U *)
  36 let rec subst_type_nat T U i ≝
  37     match T with
  38     [ TVar n ⇒ match eqb n i with
  39       [ true ⇒ U
  40       | false ⇒ T]
  41     | TFree X ⇒ T
  42     | Top ⇒ T
  43     | Arrow T1 T2 ⇒ Arrow (subst_type_nat T1 U i) (subst_type_nat T2 U i)
  44     | Forall T1 T2 ⇒ Forall (subst_type_nat T1 U i) (subst_type_nat T2 U (S i)) ].
  45
  46 (*** definitions about lists ***)
  47
  48 definition filter_types : list bound → list bound ≝
  49   λG.(filter ? G (λB.match B with [mk_bound B X T ⇒ B])).
  50
  51 definition fv_env : list bound → list nat ≝
  52   λG.(map ? ? (λb.match b with [mk_bound B X T ⇒ X]) (filter_types G)).
  53
  54 let rec fv_type T ≝
  55   match T with
  56     [TVar n ⇒ []
  57     |TFree x ⇒ [x]
  58     |Top ⇒ []
  59     |Arrow U V ⇒ fv_type U @ fv_type V
  60     |Forall U V ⇒ fv_type U @ fv_type V].
  61
  62 (*** Type Well-Formedness judgement ***)
  63
  64 inductive WFType : list bound → Typ → Prop ≝
  65   | WFT_TFree : ∀X,G.in_list ? X (fv_env G) → WFType G (TFree X)
  66   | WFT_Top : ∀G.WFType G Top
  67   | WFT_Arrow : ∀G,T,U.WFType G T → WFType G U → WFType G (Arrow T U)
  68   | WFT_Forall : ∀G,T,U.WFType G T →
  69                    (∀X:nat.
  70                     (¬ (in_list ? X (fv_env G))) →
  71                     (¬ (in_list ? X (fv_type U))) →
  72                     (WFType ((mk_bound true X T) :: G)
  73                      (subst_type_nat U (TFree X) O))) →
  74                  (WFType G (Forall T U)).
  75
  76 (*** Environment Well-Formedness judgement ***)
  77
  78 inductive WFEnv : list bound → Prop ≝
  79   | WFE_Empty : WFEnv (nil ?)
  80   | WFE_cons : ∀B,X,T,G.WFEnv G → ¬ (in_list ? X (fv_env G)) →
  81                   WFType G T → WFEnv ((mk_bound B X T) :: G).
  82
  83 (*** Subtyping judgement ***)
  84 inductive JSubtype : list bound → Typ → Typ → Prop ≝
  85   | SA_Top : ∀G,T.WFEnv G → WFType G T → JSubtype G T Top
  86   | SA_Refl_TVar : ∀G,X.WFEnv G → in_list ? X (fv_env G)
  87                    → JSubtype G (TFree X) (TFree X)
  88   | SA_Trans_TVar : ∀G,X,T,U.in_list ? (mk_bound true X U) G →
  89                     JSubtype G U T → JSubtype G (TFree X) T
  90   | SA_Arrow : ∀G,S1,S2,T1,T2. JSubtype G T1 S1 → JSubtype G S2 T2 →
  91                JSubtype G (Arrow S1 S2) (Arrow T1 T2)
  92   | SA_All : ∀G,S1,S2,T1,T2. JSubtype G T1 S1 →
  93              (∀X.¬ (in_list ? X (fv_env G)) →
  94                JSubtype ((mk_bound true X T1) :: G)
  95                 (subst_type_nat S2 (TFree X) O) (subst_type_nat T2 (TFree X) O)) →
  96              JSubtype G (Forall S1 S2) (Forall T1 T2).
  97
  98 notation "mstyle color #007f00 (hvbox(e ⊢ break ta ⊴ break tb))"
  99   non associative with precedence 30 for @{ 'subjudg $e $ta $tb }.
 100 interpretation "Fsub subtype judgement" 'subjudg e ta tb = (JSubtype e ta tb).
 101
 102 notation "mstyle color #007f00 (hvbox(e ⊢ ♦))"
 103   non associative with precedence 30 for @{ 'wfejudg $e }.
 104 interpretation "Fsub WF env judgement" 'wfejudg e = (WFEnv e).
 105
 106 notation "mstyle color #007f00 (hvbox(e ⊢ break t))"
 107   non associative with precedence 30 for @{ 'wftjudg $e $t }.
 108 interpretation "Fsub WF type judgement" 'wftjudg e t = (WFType e t).
 109
 110 notation > "\Forall S.T"
 111   non associative with precedence 60 for @{ 'forall $S $T}.
 112 notation < "hvbox(⊓ \sub S. break T)"
 113   non associative with precedence 60 for @{ 'forall $S $T}.
 114 interpretation "universal type" 'forall S T = (Forall S T).
 115
 116 notation "#x" with precedence 79 for @{'tvar $x}.
 117 interpretation "bound tvar" 'tvar x = (TVar x).
 118
 119 notation "!x" with precedence 79 for @{'tname $x}.
 120 interpretation "bound tname" 'tname x = (TFree x).
 121
 122 notation "⊤" with precedence 90 for @{'toptype}.
 123 interpretation "toptype" 'toptype = Top.
 124
 125 notation "hvbox(s break ⇛ t)"
 126   right associative with precedence 55 for @{ 'arrow $s $t }.
 127 interpretation "arrow type" 'arrow S T = (Arrow S T).
 128
 129 notation "hvbox(S [#n ↦ T])"
 130   non associative with precedence 80 for @{ 'substvar $S $T $n }.
 131 interpretation "subst bound var" 'substvar S T n = (subst_type_nat S T n).
 132
 133 notation "hvbox(!X ⊴ T)"
 134   non associative with precedence 60 for @{ 'subtypebound $X $T }.
 135 interpretation "subtyping bound" 'subtypebound X T = (mk_bound true X T).
 136
 137 (****** PROOFS ********)
 138
 139 (*** theorems about lists ***)
 140
 141 lemma boundinenv_natinfv : ∀x,G.(∃T.!x ⊴ T ∈ G) → x ∈ (fv_env G).
 142 intros 2;elim G;decompose
 143   [elim (not_in_list_nil ? ? H1)
 144   |elim (in_list_cons_case ? ? ? ? H2)
 145      [rewrite < H1;simplify;apply in_list_head
 146      |elim a;apply (bool_elim ? b);intro;simplify;try apply in_list_cons;
 147       apply H;autobatch]]
 148 qed.
 149
 150 lemma natinfv_boundinenv : ∀x,G.x ∈ (fv_env G) → ∃T.!x ⊴ T ∈ G.
 151 intros 2;elim G 0
 152   [simplify;intro;lapply (not_in_list_nil ? ? H);elim Hletin
 153   |intros 3;
 154    elim a;simplify in H1;elim b in H1;simplify in H1
 155    [elim (in_list_cons_case ? ? ? ? H1)
 156      [rewrite < H2;autobatch
 157      |elim (H H2);autobatch]
 158    |elim (H H1);autobatch]]
 159 qed.
 160
 161 lemma incl_bound_fv : ∀l1,l2.l1 ⊆ l2 → (fv_env l1) ⊆ (fv_env l2).
 162 intros;unfold in H;unfold;intros;apply boundinenv_natinfv;
 163 lapply (natinfv_boundinenv ? ? H1);decompose;autobatch depth=4;
 164 qed.
 165
 166 lemma WFT_env_incl : ∀G,T.(G ⊢ T) → ∀H.fv_env G ⊆ fv_env H → (H ⊢ T).
 167 intros 3.elim H
 168   [apply WFT_TFree;unfold in H3;apply (H3 ? H1)
 169   |apply WFT_Top
 170   |apply WFT_Arrow;autobatch
 171   |apply WFT_Forall
 172      [apply (H2 ? H6)
 173      |intros;apply (H4 ? ? H8)
 174         [unfold;intro;autobatch
 175         |simplify;apply (incl_cons ???? H6)]]]
 176 qed.
 177
 178 lemma fv_env_extends : ∀H,x,T,U,G,B.
 179                          fv_env (H @ mk_bound B x T :: G) =
 180                          fv_env (H @ mk_bound B x U :: G).
 181 intros 5;elim H;elim B
 182   [1,2:reflexivity
 183   |*:elim a;elim b;simplify;lapply (H1 true);lapply (H1 false);
 184    try rewrite > Hletin;try rewrite > Hletin1;reflexivity]
 185 qed.
 186
 187 lemma lookup_env_extends : ∀G,H,B,C,D,T,U,V,x,y.
 188             mk_bound D y V ∈ H @ mk_bound C x U :: G → y ≠ x →
 189             mk_bound D y V ∈ H @ mk_bound B x T :: G.
 190 intros 10;elim H
 191   [simplify in H1;elim (in_list_cons_case ? ? ? ? H1)
 192      [destruct H3;elim H2;reflexivity
 193      |simplify;apply (in_list_cons ? ? ? ? H3);]
 194   |simplify in H2;simplify;elim (in_list_cons_case ? ? ? ? H2)
 195      [rewrite > H4;apply in_list_head
 196      |apply (in_list_cons ? ? ? ? (H1 H4 H3))]]
 197 qed.
 198
 199 lemma in_FV_subst : ∀x,T,U,n.x ∈ fv_type T → x ∈ fv_type (subst_type_nat T U n).
 200 intros 3;elim T
 201   [simplify in H;elim (not_in_list_nil ? ? H)
 202   |2,3:simplify;simplify in H;assumption
 203   |*:simplify in H2;simplify;elim (in_list_append_to_or_in_list ? ? ? ? H2);
 204      autobatch]
 205 qed.
 206
 207 (*** lemma on fresh names ***)
 208
 209 lemma fresh_name : ∀l:list nat.∃n.n ∉ l.
 210 cut (∀l:list nat.∃n.∀m.n ≤ m → ¬ in_list ? m l);intros
 211   [lapply (Hcut l);elim Hletin;apply ex_intro;autobatch
 212   |elim l
 213     [apply ex_intro[apply O];intros;unfold;intro;elim (not_in_list_nil ? ? H1)
 214     |elim H;apply ex_intro[apply (S (max a1 a))];
 215      intros;unfold;intro;
 216      elim (in_list_cons_case ? ? ? ? H3)
 217       [rewrite > H4 in H2;autobatch
 218       |elim H4
 219          [apply (H1 m ? H4);autobatch
 220          |assumption]]]]
 221 qed.
 222
 223 (*** lemmata on well-formedness ***)
 224
 225 lemma fv_WFT : ∀T,x,G.(G ⊢ T) → x ∈ fv_type T → x ∈ fv_env G.
 226 intros 4.elim H
 227   [simplify in H2;elim (in_list_cons_case ? ? ? ? H2)
 228      [applyS H1|elim (not_in_list_nil ? ? H3)]
 229   |simplify in H1;elim (not_in_list_nil ? x H1)
 230   |simplify in H5;elim (in_list_append_to_or_in_list ? ? ? ? H5);autobatch
 231   |simplify in H5;elim (in_list_append_to_or_in_list ? ? ? ? H5)
 232      [apply (H2 H6)
 233      |elim (fresh_name (fv_type t1 @ fv_env l));
 234       cut (¬ in_list ? a (fv_type t1) ∧ ¬ in_list ? a (fv_env l))
 235         [elim Hcut;lapply (H4 ? H9 H8)
 236            [cut (x ≠ a)
 237               [simplify in Hletin;elim (in_list_cons_case ? ? ? ? Hletin)
 238                  [elim (Hcut1 H10)
 239                  |assumption]
 240               |intro;apply H8;applyS H6]
 241            |autobatch]
 242         |split;intro;apply H7;autobatch]]]
 243 qed.
 244
 245 (*** lemmata relating subtyping and well-formedness ***)
 246
 247 lemma JS_to_WFE : ∀G,T,U.G ⊢ T ⊴ U → G ⊢ ♦.
 248 intros;elim H;assumption.
 249 qed.
 250
 251 lemma JS_to_WFT : ∀G,T,U.G ⊢ T ⊴ U → (G ⊢ T) ∧ (G ⊢ U).
 252 intros;elim H
 253   [1,2:autobatch
 254   |split
 255     [apply WFT_TFree;(* FIXME! qui bastava autobatch, ma si e` rotto *) apply boundinenv_natinfv;autobatch
 256     |elim H3;assumption]
 257   |decompose;autobatch size=7
 258   |elim H2;split
 259      [apply (WFT_Forall ? ? ? H6);intros;elim (H4 X H7);
 260       apply (WFT_env_incl ? ? H9);simplify;unfold;intros;assumption
 261      |apply (WFT_Forall ? ? ? H5);intros;elim (H4 X H7);
 262       apply (WFT_env_incl ? ? H10);simplify;unfold;intros;assumption]]
 263 qed.
 264
 265 lemma JS_to_WFT1 : ∀G,T,U.G ⊢ T ⊴ U → G ⊢ T.
 266 intros;elim (JS_to_WFT ? ? ? H);assumption;
 267 qed.
 268
 269 lemma JS_to_WFT2 : ∀G,T,U.G ⊢ T ⊴ U → G ⊢ U.
 270 intros;elim (JS_to_WFT ? ? ? H);assumption;
 271 qed.
 272
 273 lemma WFE_Typ_subst : ∀H,x,B,T,U,G.
 274                       H @ mk_bound B x T :: G ⊢ ♦ → (G ⊢ U) →
 275                       H @ mk_bound B x U :: G ⊢ ♦.
 276 intros 6;elim H 0
 277   [simplify;intros;inversion H1;intros
 278      [elim (nil_cons ? G (mk_bound B x T) H3)
 279      |destruct H7;autobatch]
 280   |intros;simplify;generalize in match H2;elim a;simplify in H4;
 281    inversion H4;intros
 282      [destruct H5
 283      |destruct H9;apply WFE_cons
 284         [apply (H1 H5 H3)
 285         |rewrite < (fv_env_extends ? x T U); assumption
 286         |apply (WFT_env_incl ? ? H8);
 287          rewrite < (fv_env_extends ? x T U);unfold;intros;
 288          assumption]]]
 289 qed.
 290
 291 lemma WFE_bound_bound : ∀x,T,U,G.G ⊢ ♦ → !x ⊴  T ∈ G → !x ⊴ U ∈ G → T = U.
 292 intros 5;elim H
 293   [lapply (not_in_list_nil ? ? H1);elim Hletin
 294   |elim (in_list_cons_case ? ? ? ? H6)
 295      [destruct H7;destruct;elim (in_list_cons_case ? ? ? ? H5)
 296         [destruct H7;reflexivity
 297         |elim H7;elim H3;apply boundinenv_natinfv;autobatch]
 298      |elim (in_list_cons_case ? ? ? ? H5)
 299         [destruct H8;elim H3;apply boundinenv_natinfv;autobatch
 300         |apply (H2 H8 H7)]]]
 301 qed.
 302
 303 lemma WFT_to_incl: ∀G,T,U.(∀X.X ∉ fv_env G → X ∉ fv_type U →
 304     (mk_bound true X T::G ⊢ (subst_type_nat U (TFree X) O))) →
 305     fv_type U ⊆ fv_env G.
 306 intros;elim (fresh_name (fv_type U@fv_env G));lapply(H a)
 307   [unfold;intros;lapply (fv_WFT ? x ? Hletin)
 308      [simplify in Hletin1;inversion Hletin1;intros
 309         [destruct H4;elim H1;autobatch
 310         |destruct H6;assumption]
 311      |apply in_FV_subst;assumption]
 312   |*:intro;apply H1;autobatch]
 313 qed.
 314
 315 lemma incl_fv_env: ∀X,G,G1,U,P.
 316       fv_env (G1@ !X ⊴ U::G) ⊆ fv_env (G1@ !X ⊴ P::G).
 317 intros.rewrite < fv_env_extends.apply incl_A_A.
 318 qed.
 319
 320 lemma fv_append : ∀G,H.fv_env (G @ H) = fv_env G @ fv_env H.
 321 intro;elim G;simplify;
 322 [reflexivity
 323 |elim a;simplify;elim b;simplify;lapply (H H1);rewrite > Hletin;reflexivity]
 324 qed.