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