helm/software/matita/contribs/POPLmark/Fsub/defndb.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 include "nat/le_arith.ma".
  17 include "nat/lt_arith.ma".
  18
  19 (*** representation of Fsub types ***)
  20 inductive Typ : Set ≝
  21   | TVar : nat → Typ          (* type var *)
  22   | Top : Typ                 (* maximum type *)
  23   | Arrow : Typ → Typ → Typ   (* functions *)
  24   | Forall : Typ → Typ → Typ. (* universal type *)
  25
  26 (* representation of bounds *)
  27
  28 record bound : Set ≝ {
  29                           istype : bool;    (* is subtyping bound? *)
  30                           btype  : Typ      (* type to which the name is bound *)
  31                      }.
  32
  33 (*** Type Well-Formedness judgement ***)
  34
  35 inductive WFType : list bound → Typ → Prop ≝
  36   | WFT_TVar : ∀G,n,T.n < length ? G → (nth ? G (mk_bound true Top) n = mk_bound true T) →
  37                WFType G (TVar n)
  38   | WFT_Top : ∀G.WFType G Top
  39   | WFT_Arrow : ∀G,T,U.WFType G T → WFType G U → WFType G (Arrow T U)
  40   | WFT_Forall : ∀G,T,U.WFType G T → WFType (mk_bound true T::G) U →
  41                  WFType G (Forall T U).
  42
  43 (*** Environment Well-Formedness judgement ***)
  44
  45 inductive WFEnv : list bound → Prop ≝
  46   | WFE_Empty : WFEnv (nil ?)
  47   | WFE_cons : ∀B,T,G.WFEnv G → WFType G T → WFEnv (mk_bound B T :: G).
  48
  49 let rec lift T h k on T ≝
  50 match T with
  51 [ TVar n ⇒ TVar (match (leb k n) with [true ⇒ n + h | false ⇒ n])
  52 | Top ⇒ Top
  53 | Arrow U V ⇒ Arrow (lift U h k) (lift V h k)
  54 | Forall U V ⇒ Forall (lift U h k) (lift V h (S k))].
  55
  56 (*** Subtyping judgement ***)
  57 inductive JSubtype : list bound → Typ → Typ → Prop ≝
  58   | SA_Top : ∀G,T.WFEnv G → WFType G T → JSubtype G T Top
  59   | SA_Refl_TVar : ∀G,n.WFEnv G → WFType G (TVar n) → JSubtype G (TVar n) (TVar n)
  60   | SA_Trans_TVar : ∀G,n,T,U.n < length ? G →
  61                       nth ? G (mk_bound true Top) n = mk_bound true U →
  62                       JSubtype G (lift U (S n) O) T → JSubtype G (TVar n) T
  63   | SA_Arrow : ∀G,S1,S2,T1,T2. JSubtype G T1 S1 → JSubtype G S2 T2 →
  64                JSubtype G (Arrow S1 S2) (Arrow T1 T2)
  65   | SA_All : ∀G,S1,S2,T1,T2.
  66              JSubtype G T1 S1 → JSubtype (mk_bound true T1 :: G) S2 T2 →
  67              JSubtype G (Forall S1 S2) (Forall T1 T2).
  68
  69 notation "hvbox(e ⊢ break ta ⊴  break tb)"
  70   non associative with precedence 30 for @{ 'subjudg $e $ta $tb }.
  71 interpretation "Fsub subtype judgement" 'subjudg e ta tb = (JSubtype e ta tb).
  72
  73 notation > "hvbox(\Forall S.T)"
  74   non associative with precedence 60 for @{ 'forall $S $T}.
  75 notation < "hvbox('All' \sub S. break T)"
  76   non associative with precedence 60 for @{ 'forall $S $T}.
  77 interpretation "universal type" 'forall S T = (Forall S T).
  78
  79 notation "#x" with precedence 79 for @{'tvar $x}.
  80 interpretation "bound tvar" 'tvar x = (TVar x).
  81
  82 notation "⊤" with precedence 90 for @{'toptype}.
  83 interpretation "toptype" 'toptype = Top.
  84
  85 notation "hvbox(s break ⇛ t)"
  86   right associative with precedence 55 for @{ 'arrow $s $t }.
  87 interpretation "arrow type" 'arrow S T = (Arrow S T).
  88
  89 notation "hvbox(⊴ T)"
  90   non associative with precedence 60 for @{ 'subtypebound $T }.
  91 interpretation "subtyping bound" 'subtypebound T = (mk_bound true T).
  92
  93 (****** PROOFS ********)
  94
  95 (*** theorems about lists ***)
  96
  97 let rec flift f k on k ≝ match k with
  98 [ O ⇒ f
  99 | S p ⇒ flift (λn.match n with [ O ⇒ O | S m ⇒ S (f m) ]) p ].
 100
 101 let rec perm T f ≝ match T with
 102 [ TVar m ⇒ TVar (f m)
 103 | Top ⇒ Top
 104 | Arrow U V ⇒ Arrow (perm U f) (perm V f)
 105 | Forall U V ⇒ Forall (perm U f) (perm V (flift f 1))].
 106
 107 definition blift : bound → nat → bound ≝
 108 λB,n.match B with [ mk_bound b t ⇒ mk_bound b (lift t n O) ].
 109
 110 definition bperm : bound → (nat→nat) → bound ≝
 111 λB,f.match B with [ mk_bound b t ⇒ mk_bound b (perm t f) ].
 112
 113 definition incl : list bound → list bound → (nat → nat) → Prop ≝
 114 λG,H,f.injective ?? f → ∀n.n < length ? G →
 115   bperm (blift (nth ? G (mk_bound true Top) n) (S n)) f =
 116   blift (nth ? H (mk_bound true Top) (f n)) (S (f n)).
 117
 118 lemma lift_lift : ∀T,n,m,k.lift (lift T n k) m k = lift T (n+m) k.
 119 intros 3;elim T;simplify;
 120 [apply (leb_elim k n1);intros;simplify;
 121  [apply leb_elim;intros;simplify;
 122   [apply eq_f;rewrite < assoc_plus;reflexivity
 123   |elim H1;autobatch]
 124  |rewrite > lt_to_leb_false
 125   [simplify;reflexivity
 126   |autobatch]]
 127 |*:autobatch]
 128 qed.
 129
 130 lemma lift_O : ∀T,k.lift T O k = T.
 131 intro;elim T;simplify
 132 [cases (leb k n);simplify;autobatch paramodulation
 133 |*:autobatch]
 134 qed.
 135
 136 lemma flift_flift : ∀h,k,f.flift (flift f h) k = flift f (h+k).
 137 intros 2;elim h;simplify
 138 [reflexivity
 139 |rewrite > H;reflexivity]
 140 qed.
 141
 142 lemma eq_f_g_to_eq_fx_gx : ∀A,B:Type.∀f,g:A → B.∀x.f = g → f x = g x.
 143 intros;rewrite > H;reflexivity;
 144 qed.
 145
 146 lemma flift_S : ∀n,m,f.flift f (S n) (S m) = S (flift f n m).
 147 intros 2;elim n
 148 [reflexivity
 149 |cut (flift f (S (S n1)) (S m) = flift (flift f (S n1)) 1 (S m))
 150  [rewrite > Hcut;simplify;reflexivity
 151  |change in match (S (S n1)) with (1 + (S n1));rewrite > sym_plus;
 152   apply eq_f_g_to_eq_fx_gx;symmetry;apply flift_flift]]
 153 qed.
 154
 155 lemma le_flift : ∀k,n.k ≤ n → ∀f.k ≤ flift f k n.
 156 intro;elim k
 157 [autobatch
 158 |cut (∃p.n1 = S p)
 159  [elim Hcut;rewrite > H2;rewrite > flift_S;apply le_S_S;apply H;
 160   rewrite > H2 in H1;autobatch
 161  |elim H1
 162   [exists[apply n]
 163    reflexivity
 164   |elim H3;exists[apply (S a)]
 165    apply eq_f;assumption]]]
 166 qed.
 167
 168 lemma le_flift2 : ∀k,n.n < k → ∀f.flift f k n = n.
 169 intro;elim k
 170 [elim (not_le_Sn_O ? H)
 171 |generalize in match H1;cases n1;intros
 172  [cut (flift f (S n) O = flift (flift f n) 1 O)
 173   [rewrite > Hcut;reflexivity
 174   |apply eq_f_g_to_eq_fx_gx;autobatch paramodulation]
 175  |rewrite > flift_S;apply eq_f;apply H;autobatch]]
 176 qed.
 177
 178 lemma lift_perm : ∀T,n,f,k.perm (lift T (S n) k) (flift f (S k)) = lift (perm (lift T n k) (flift f k)) 1 k.
 179 intros 2;elim T;simplify;
 180 [apply (leb_elim k n1);simplify;intros
 181  [apply eq_f;change in ⊢ (??(?%??)?) with (flift f 1);
 182   cut (flift (flift f 1) k (n1+S n) = flift (flift f k) 1 (n1+S n))
 183   [rewrite > Hcut;rewrite < plus_n_Sm;simplify;
 184    apply (leb_elim k (flift f k (n1+n)));simplify;intros
 185    [rewrite > sym_plus in ⊢ (???%);simplify;reflexivity
 186    |elim H1;elim k in H
 187     [autobatch
 188     |apply le_flift;autobatch]]
 189   |apply eq_f_g_to_eq_fx_gx;autobatch paramodulation]
 190  |apply eq_f;change in ⊢ (??(?%??)?) with (flift f 1);
 191   rewrite > le_flift2 [|autobatch]
 192   apply (leb_elim k (flift f k n1));simplify;intro
 193   [rewrite > le_flift2 in H1 [|autobatch]
 194    elim (H H1)
 195   |symmetry;apply le_flift2;autobatch]]
 196 |reflexivity
 197 |apply eq_f2;change in ⊢ (? ? (? ? (? % ?)) ?) with (flift f 1);
 198   rewrite > flift_flift;simplify in ⊢ (? ? (? ? (? ? %)) ?);autobatch
 199 |apply eq_f2
 200  [change in ⊢ (? ? (? ? (? % ?)) ?) with (flift f 1);
 201   rewrite > flift_flift;simplify in ⊢ (? ? (? ? (? ? %)) ?);autobatch
 202  |change in ⊢ (??(??%)?) with (flift (flift (flift f 1) k) 1);
 203   rewrite > flift_flift in ⊢ (??%?);
 204   rewrite > sym_plus in ⊢ (? ? (? ? (? ? %)) ?);
 205   rewrite > flift_flift;
 206   simplify in ⊢ (? ? (? ? (? ? %)) ?);
 207   rewrite > H1;do 2 apply eq_f_g_to_eq_fx_gx;
 208   apply eq_f;apply eq_f;
 209   change in ⊢ (???%) with (flift (flift f k) 1);
 210   rewrite > flift_flift;rewrite > sym_plus;reflexivity]]
 211 qed.
 212
 213 lemma blift_bperm : ∀B,n,f.bperm (blift B (S n)) (flift f 1) = blift (bperm (blift B n) f) 1.
 214 intros;cases B;simplify;apply eq_f;
 215 change in ⊢ (? ? ? (? (? ? %) ? ?)) with (flift f O);
 216 apply lift_perm;
 217 qed.
 218
 219 definition lifter : nat → nat → nat → nat ≝
 220  λn,k,m.match (leb k m) with
 221  [ true ⇒ m+n
 222  | false ⇒ m ].
 223
 224 lemma extensional_perm : ∀T.∀f,g.(∀x.f x = g x) → perm T f = perm T g.
 225 intro;elim T
 226 [4:whd in ⊢ (??%%);cut (∀x.flift f 1 x = flift g 1 x)
 227  [rewrite > (H f g);
 228   [rewrite > (H1 (flift f 1) (flift g 1));
 229    [reflexivity
 230    |assumption]
 231   |assumption]
 232  |intro;simplify;cases x
 233   [reflexivity
 234   |simplify;rewrite > H2;reflexivity]]
 235 |*:simplify;autobatch]
 236 qed.
 237
 238 lemma flift_lifter : ∀p,n,m,k.flift (lifter n k) p m = lifter n (k+p) m.
 239 intro;elim p
 240 [simplify;autobatch paramodulation
 241 |change in ⊢ (? ? (? ? % ?) ?) with (1+n);
 242  rewrite < plus_n_Sm;whd in ⊢ (???%);
 243  transitivity (flift (flift (lifter n1 k) n) 1 m)
 244  [apply eq_f_g_to_eq_fx_gx;rewrite > sym_plus;autobatch
 245  |unfold lifter;simplify;
 246   change in ⊢ (? ? match ? return ? with [_⇒?|_⇒λ_:?.? (? % ? ?)] ?) with (lifter n1 k);
 247   cases m
 248   [simplify;reflexivity
 249   |simplify;rewrite > H;unfold lifter;cases (leb (k+n) n2);reflexivity]]]
 250 qed.
 251
 252 lemma lift_perm2 : ∀T,n,k.lift T n k = perm T (lifter n k).
 253 intros 2;elim T;simplify
 254 [1,2,3:autobatch
 255 |rewrite < H;change in ⊢ (???(??(??%))) with (flift (lifter n k) 1);
 256  rewrite > H1;
 257  rewrite > (extensional_perm ? (lifter n (S k)) (flift (lifter n k) 1))
 258  [reflexivity
 259  |intro;symmetry;autobatch]]
 260 qed.
 261
 262 lemma incl_cons : ∀G,H,f,T.injective ?? f → incl G H f →
 263                            incl (⊴ T::G) (⊴ perm T f :: H) (flift f 1).
 264 intros;unfold;intros 2;
 265 elim n;
 266 [simplify;change in ⊢ (? ? (? ? (? ? %)) ?) with (flift f 1);
 267  rewrite > lift_perm;rewrite > lift_O;reflexivity
 268 |simplify in H5;lapply (le_S_S_to_le ?? H5);clear H5;
 269  simplify in ⊢ (? ? ? (? % ?));
 270  simplify in ⊢ (? ? (? (? % ?) ?) ?);
 271  unfold in H2;rewrite > (blift_bperm ? ? f);
 272  rewrite > (H2 ?? Hletin);
 273  [cases (nth bound H (mk_bound true Top) (f n1));
 274   simplify;rewrite > lift_lift;rewrite > sym_plus;
 275   reflexivity
 276  |assumption]]
 277 qed.
 278
 279 lemma injective_flift : ∀f,n.injective ?? f → injective ?? (flift f n).
 280 intros;elim n
 281 [simplify;assumption
 282 |change in ⊢ (? ? ? (? ? %)) with (1+n1);rewrite > sym_plus;
 283  rewrite < flift_flift;unfold;intros 2;
 284  cases (decidable_eq_nat x 0)
 285  [rewrite > le_flift2
 286   [cases (decidable_eq_nat y 0)
 287    [intro;autobatch paramodulation
 288    |elim y in H3
 289     [elim H3;reflexivity
 290     |simplify in H5;destruct]]
 291   |rewrite > H2;autobatch]
 292  |generalize in match H2;cases x
 293   [intros;elim H3;reflexivity
 294   |intro;cases y;simplify;intros;destruct;
 295    rewrite > (H1 ?? Hcut);reflexivity]]]
 296 qed.
 297
 298 lemma injective_lifter : ∀n,k.injective ?? (lifter n k).
 299 intros;unfold;intros;unfold lifter in H;
 300 apply (leb_elim k x);intros;
 301 [rewrite > (le_to_leb_true ?? H1) in H;apply (leb_elim k y);intros;
 302  [rewrite > (le_to_leb_true ?? H2) in H;simplify in H;
 303   autobatch
 304  |lapply (not_le_to_lt ?? H2) as H3;rewrite > (lt_to_leb_false ?? H3) in H;
 305   simplify in H;rewrite < H in H2;elim H2;autobatch]
 306 |lapply (not_le_to_lt ?? H1) as H2;rewrite > (lt_to_leb_false ?? H2) in H;
 307  apply (leb_elim k y);intros
 308  [rewrite > (le_to_leb_true ?? H3) in H;simplify in H;rewrite > H in H1;
 309   elim H1;autobatch
 310  |lapply (not_le_to_lt ?? H3) as H4;rewrite > (lt_to_leb_false ?? H4) in H;
 311   simplify in H;assumption]]
 312 qed.
 313
 314 lemma incl_append : ∀G,H. incl G (H@G) (lifter (length ? H) O).
 315 intros;unfold;intros;
 316 cut (nth ? G (⊴ ⊤) n = nth ? (H@G) (⊴ ⊤) (lifter (length ? H) O n))
 317 [rewrite < Hcut;cases (nth bound G (⊴ ⊤) n);simplify;
 318  rewrite < lift_perm2;rewrite > lift_lift;reflexivity
 319 |elim H
 320  [simplify;rewrite < plus_n_O;reflexivity
 321  |simplify;rewrite < plus_n_Sm;apply H3]]
 322 qed.
 323
 324 lemma flift_id : ∀m,n.flift (λx.x) m n = n.
 325 intro;elim m
 326 [reflexivity
 327 |change in ⊢ (??(??%?)?) with (1+n);rewrite > sym_plus;
 328  transitivity (flift (flift (λx.x) n) 1 n1)
 329  [apply eq_f_g_to_eq_fx_gx;autobatch
 330  |simplify;generalize in match H;cases n1;intro
 331   [reflexivity
 332   |simplify;apply eq_f;apply H1]]]
 333 qed.
 334
 335 lemma perm_id : ∀T,n.T = perm T (flift (λx.x) n).
 336 intro;elim T;
 337 [1:simplify;rewrite > flift_id;reflexivity
 338 |4:whd in ⊢ (???%);rewrite > flift_flift;rewrite < H1;rewrite < H;reflexivity
 339 |*:simplify;autobatch]
 340 qed.
 341
 342 lemma perm_compose : ∀T,f,g.perm (perm T f) g = perm T (λx.g (f x)).
 343 intro;elim T
 344 [reflexivity
 345 |reflexivity
 346 |simplify;autobatch
 347 |simplify;rewrite > H;
 348  change in ⊢ (? ? (? ? (? (? ? %) ?)) ?) with (flift f 1);
 349  change in ⊢ (? ? (? ? (? ? %)) ?) with (flift g 1);
 350  rewrite > H1;
 351  change in ⊢ (? ? ? (? ? (? ? %))) with (flift (λx.g (f x)) 1);
 352  rewrite > (extensional_perm ? (λx.flift g 1 (flift f 1 x)) (flift (λx.g (f x)) 1));
 353  [reflexivity
 354  |intros;cases x;simplify;reflexivity]]
 355 qed.
 356
 357 lemma WFT_env_incl : ∀G,T.WFType G T → ∀H,f.injective nat nat f → incl G H f →
 358                           (∀n. n < length ? G → f n < length ? H) →
 359                           WFType H (perm T f).
 360 intros 3;elim H
 361 [simplify;unfold in H5;lapply (H5 H4 n H1);
 362  cut (∃T.nth ? H3 (mk_bound true Top) (f n) = mk_bound true T)
 363  [elim Hcut;apply WFT_TVar
 364   [apply a
 365   |*:autobatch]
 366  |rewrite > H2 in Hletin;simplify in Hletin;
 367   elim (nth bound H3 (mk_bound true Top) (f n)) in Hletin;elim b in H7
 368   [exists[apply t1]
 369    reflexivity
 370   |simplify in H7;destruct]]
 371 |2:simplify;autobatch
 372 |simplify;autobatch width=4 size=9
 373 |simplify;apply WFT_Forall
 374  [autobatch
 375  |apply H4
 376   [change in ⊢ (???%) with (flift f 1);apply injective_flift;assumption
 377   |change in ⊢ (???%) with (flift f 1);apply incl_cons;assumption
 378   |intro;cases n;simplify;intros;autobatch depth=4]]]
 379 qed.
 380
 381 lemma WFT_env_incl2: ∀G,T.WFType G T → ∀H.length ? G = length ? H →
 382 (∀n,U.n < length ? G → nth ? G (mk_bound true Top) n = mk_bound true U →
 383  ∃V.nth ? H (mk_bound true Top) n = mk_bound true V) →
 384  WFType H T.
 385 intros 3;elim H
 386 [elim (H5 n t)
 387  [apply WFT_TVar
 388   [2:applyS H1
 389   |3:apply H6]
 390  |assumption
 391  |assumption]
 392 |autobatch
 393 |apply WFT_Arrow;autobatch
 394 |apply WFT_Forall;try autobatch;
 395  apply H4;
 396  [simplify;autobatch
 397  |intros;elim n in H8 H9
 398   [exists[apply t]
 399    reflexivity
 400   |elim (H7 n1 U ? H10)
 401    [exists[apply a]
 402     assumption
 403    |apply le_S_S_to_le;apply H9]]]]
 404 qed.
 405
 406 lemma WFT_extends : ∀G,H,U,P,T.WFType (G@(mk_bound true U::H)) T → WFType (G@(mk_bound true P::H)) T.
 407 intros;apply (WFT_env_incl2 ?? H1)
 408 [elim G;simplify
 409  [reflexivity
 410  |rewrite > H2;reflexivity]
 411 |intros 3;elim (decidable_eq_nat n (length ? G))
 412  [exists [apply P]
 413   elim G in n H3
 414   [simplify in H4;destruct;reflexivity
 415   |simplify;simplify in H5;rewrite > H5;simplify;apply H3;reflexivity]
 416  |exists [apply U1]
 417   elim G in n H3 H4 0
 418   [simplify;intro;elim n1
 419    [elim H3;reflexivity
 420    |simplify in H5;simplify;assumption]
 421   |simplify;intros 4;elim n1
 422    [simplify in H5;simplify;assumption
 423    |simplify;apply H3
 424     [intro;elim H5;autobatch
 425     |apply H6]]]]]
 426 qed.
 427
 428 lemma WFE_extends : ∀G,H,U,P.WFType H P → WFEnv (G@(mk_bound true U::H)) → WFEnv (G@(mk_bound true P::H)).
 429 intros;cut (WFType H U)
 430 [generalize in match H2;elim G 0;simplify;intros
 431  [inversion H3;intros;destruct;autobatch
 432  |generalize in match H4;cases a;intros;apply WFE_cons
 433   [inversion H4;intros;destruct;autobatch
 434   |inversion H5;intros;destruct;autobatch]]
 435 |elim G in H2 0;simplify;intros;
 436  [inversion H2;intros;destruct;assumption
 437  |apply H2;inversion H3;simplify;intros;destruct;assumption]]
 438 qed.
 439
 440 (*** lemmata relating subtyping and well-formedness ***)
 441
 442 lemma JS_to_WFE : ∀G,T,U.G ⊢ T ⊴ U → WFEnv G.
 443 intros;elim H;assumption.
 444 qed.
 445
 446 lemma JS_to_WFT : ∀G,T,U.G ⊢ T ⊴ U → WFType G T ∧ WFType G U.
 447 intros;elim H
 448   [1,2:autobatch
 449   |elim H4;split;autobatch
 450   |decompose;autobatch size=7
 451   |decompose;split
 452    [apply WFT_Forall;
 453     [assumption
 454     |apply (WFT_env_incl2 ?? H2) [reflexivity]
 455      simplify;intros 3;elim n
 456      [exists[apply t]
 457       reflexivity
 458      |exists[apply U1]
 459       assumption]]
 460    |autobatch]]
 461 qed.
 462
 463 lemma JS_to_WFT1 : ∀G,T,U.G ⊢ T ⊴ U → WFType G T.
 464 intros;elim (JS_to_WFT ? ? ? H);assumption;
 465 qed.
 466
 467 lemma JS_to_WFT2 : ∀G,T,U.G ⊢ T ⊴ U → WFType G U.
 468 intros;elim (JS_to_WFT ? ? ? H);assumption;
 469 qed.