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  [autobatch
 228  |intro;simplify;cases x
 229   [reflexivity
 230   |simplify;rewrite > H2;reflexivity]]
 231 |*:simplify;autobatch]
 232 qed.
 233
 234 lemma flift_lifter : ∀p,n,m,k.flift (lifter n k) p m = lifter n (k+p) m.
 235 intro;elim p
 236 [simplify;autobatch paramodulation
 237 |change in ⊢ (? ? (? ? % ?) ?) with (1+n);
 238  rewrite < plus_n_Sm;whd in ⊢ (???%);
 239  transitivity (flift (flift (lifter n1 k) n) 1 m)
 240  [apply eq_f_g_to_eq_fx_gx;rewrite > sym_plus;autobatch
 241  |unfold lifter;simplify;
 242   change in ⊢ (? ? match ? return ? with [_⇒?|_⇒λ_:?.? (? % ? ?)] ?) with (lifter n1 k);
 243   cases m
 244   [simplify;reflexivity
 245   |simplify;rewrite > H;unfold lifter;cases (leb (k+n) n2);reflexivity]]]
 246 qed.
 247
 248 lemma lift_perm2 : ∀T,n,k.lift T n k = perm T (lifter n k).
 249 intros 2;elim T;simplify
 250 [1,2,3:autobatch
 251 |rewrite < H;change in ⊢ (???(??(??%))) with (flift (lifter n k) 1);
 252  rewrite > H1;
 253  rewrite > (extensional_perm ? (lifter n (S k)) (flift (lifter n k) 1))
 254  [reflexivity
 255  |intro;symmetry;autobatch]]
 256 qed.
 257
 258 lemma incl_cons : ∀G,H,f,T.injective ?? f → incl G H f →
 259                            incl (⊴ T::G) (⊴ perm T f :: H) (flift f 1).
 260 intros;unfold;intros 2;
 261 elim n;
 262 [simplify;change in ⊢ (? ? (? ? (? ? %)) ?) with (flift f 1);
 263  rewrite > lift_perm;rewrite > lift_O;reflexivity
 264 |simplify in H5;lapply (le_S_S_to_le ?? H5);clear H5;
 265  simplify in ⊢ (? ? ? (? % ?));
 266  simplify in ⊢ (? ? (? (? % ?) ?) ?);
 267  unfold in H2;rewrite > (blift_bperm ? ? f);
 268  rewrite > (H2 ?? Hletin);
 269  [cases (nth bound H (mk_bound true Top) (f n1));
 270   simplify;rewrite > lift_lift;rewrite > sym_plus;
 271   reflexivity
 272  |assumption]]
 273 qed.
 274
 275 lemma injective_flift : ∀f,n.injective ?? f → injective ?? (flift f n).
 276 intros;elim n
 277 [simplify;assumption
 278 |change in ⊢ (? ? ? (? ? %)) with (1+n1);rewrite > sym_plus;
 279  rewrite < flift_flift;unfold;intros 2;
 280  cases (decidable_eq_nat x 0)
 281  [rewrite > le_flift2
 282   [cases (decidable_eq_nat y 0)
 283    [intro;autobatch paramodulation
 284    |elim y in H3
 285     [elim H3;reflexivity
 286     |simplify in H5;destruct]]
 287   |rewrite > H2;autobatch]
 288  |generalize in match H2;cases x
 289   [intros;elim H3;reflexivity
 290   |intro;cases y;simplify;intros;destruct;
 291    rewrite > (H1 ?? Hcut);reflexivity]]]
 292 qed.
 293
 294 lemma injective_lifter : ∀n,k.injective ?? (lifter n k).
 295 intros;unfold;intros;unfold lifter in H;
 296 apply (leb_elim k x);intros;
 297 [rewrite > (le_to_leb_true ?? H1) in H;apply (leb_elim k y);intros;
 298  [rewrite > (le_to_leb_true ?? H2) in H;simplify in H;
 299   autobatch
 300  |lapply (not_le_to_lt ?? H2) as H3;rewrite > (lt_to_leb_false ?? H3) in H;
 301   simplify in H;rewrite < H in H2;elim H2;autobatch]
 302 |lapply (not_le_to_lt ?? H1) as H2;rewrite > (lt_to_leb_false ?? H2) in H;
 303  apply (leb_elim k y);intros
 304  [rewrite > (le_to_leb_true ?? H3) in H;simplify in H;rewrite > H in H1;
 305   elim H1;autobatch
 306  |lapply (not_le_to_lt ?? H3) as H4;rewrite > (lt_to_leb_false ?? H4) in H;
 307   simplify in H;assumption]]
 308 qed.
 309
 310 lemma incl_append : ∀G,H. incl G (H@G) (lifter (length ? H) O).
 311 intros;unfold;intros;
 312 cut (nth ? G (⊴ ⊤) n = nth ? (H@G) (⊴ ⊤) (lifter (length ? H) O n))
 313 [rewrite < Hcut;cases (nth bound G (⊴ ⊤) n);simplify;
 314  rewrite < lift_perm2;rewrite > lift_lift;reflexivity
 315 |elim H
 316  [simplify;rewrite < plus_n_O;reflexivity
 317  |simplify;rewrite < plus_n_Sm;apply H3]]
 318 qed.
 319
 320 lemma flift_id : ∀m,n.flift (λx.x) m n = n.
 321 intro;elim m
 322 [reflexivity
 323 |change in ⊢ (??(??%?)?) with (1+n);rewrite > sym_plus;
 324  transitivity (flift (flift (λx.x) n) 1 n1)
 325  [apply eq_f_g_to_eq_fx_gx;autobatch
 326  |simplify;generalize in match H;cases n1;intro
 327   [reflexivity
 328   |simplify;apply eq_f;apply H1]]]
 329 qed.
 330
 331 lemma perm_id : ∀T,n.T = perm T (flift (λx.x) n).
 332 intro;elim T;
 333 [1:simplify;rewrite > flift_id;reflexivity
 334 |4:whd in ⊢ (???%);rewrite > flift_flift;rewrite < H1;rewrite < H;reflexivity
 335 |*:simplify;autobatch]
 336 qed.
 337
 338 lemma perm_compose : ∀T,f,g.perm (perm T f) g = perm T (λx.g (f x)).
 339 intro;elim T
 340 [reflexivity
 341 |reflexivity
 342 |simplify;autobatch
 343 |simplify;rewrite > H;
 344  change in ⊢ (? ? (? ? (? (? ? %) ?)) ?) with (flift f 1);
 345  change in ⊢ (? ? (? ? (? ? %)) ?) with (flift g 1);
 346  rewrite > H1;
 347  change in ⊢ (? ? ? (? ? (? ? %))) with (flift (λx.g (f x)) 1);
 348  rewrite > (extensional_perm ? (λx.flift g 1 (flift f 1 x)) (flift (λx.g (f x)) 1));
 349  [reflexivity
 350  |intros;cases x;simplify;reflexivity]]
 351 qed.
 352
 353 lemma WFT_env_incl : ∀G,T.WFType G T → ∀H,f.injective nat nat f → incl G H f →
 354                           (∀n. n < length ? G → f n < length ? H) →
 355                           WFType H (perm T f).
 356 intros 3;elim H
 357 [simplify;unfold in H5;lapply (H5 H4 n H1);
 358  cut (∃T.nth ? H3 (mk_bound true Top) (f n) = mk_bound true T)
 359  [elim Hcut;apply WFT_TVar
 360   [apply a
 361   |*:autobatch]
 362  |rewrite > H2 in Hletin;simplify in Hletin;
 363   elim (nth bound H3 (mk_bound true Top) (f n)) in Hletin;elim b in H7
 364   [exists[apply t1]
 365    reflexivity
 366   |simplify in H7;destruct]]
 367 |2:simplify;autobatch
 368 |simplify;autobatch width=4 size=9
 369 |simplify;apply WFT_Forall
 370  [autobatch
 371  |apply H4
 372   [change in ⊢ (???%) with (flift f 1);apply injective_flift;assumption
 373   |change in ⊢ (???%) with (flift f 1);apply incl_cons;assumption
 374   |intro;cases n;simplify;intros;autobatch depth=4]]]
 375 qed.
 376
 377 lemma WFT_env_incl2: ∀G,T.WFType G T → ∀H.length ? G = length ? H →
 378 (∀n,U.n < length ? G → nth ? G (mk_bound true Top) n = mk_bound true U →
 379  ∃V.nth ? H (mk_bound true Top) n = mk_bound true V) →
 380  WFType H T.
 381 intros 3;elim H
 382 [elim (H5 n t)
 383  [apply WFT_TVar
 384   [2:applyS H1
 385   |3:apply H6]
 386  |assumption
 387  |assumption]
 388 |autobatch
 389 |apply WFT_Arrow;autobatch
 390 |apply WFT_Forall;try autobatch;
 391  apply H4;
 392  [simplify;autobatch
 393  |intros;elim n in H8 H9
 394   [exists[apply t]
 395    reflexivity
 396   |elim (H7 n1 U ? H10)
 397    [exists[apply a]
 398     assumption
 399    |apply le_S_S_to_le;apply H9]]]]
 400 qed.
 401
 402 lemma WFT_extends : ∀G,H,U,P,T.WFType (G@(mk_bound true U::H)) T → WFType (G@(mk_bound true P::H)) T.
 403 intros;apply (WFT_env_incl2 ?? H1)
 404 [elim G;simplify
 405  [reflexivity
 406  |rewrite > H2;reflexivity]
 407 |intros 3;elim (decidable_eq_nat n (length ? G))
 408  [exists [apply P]
 409   elim G in n H3
 410   [simplify in H4;destruct;reflexivity
 411   |simplify;simplify in H5;rewrite > H5;simplify;apply H3;reflexivity]
 412  |exists [apply U1]
 413   elim G in n H3 H4 0
 414   [simplify;intro;elim n1
 415    [elim H3;reflexivity
 416    |simplify in H5;simplify;assumption]
 417   |simplify;intros 4;elim n1
 418    [simplify in H5;simplify;assumption
 419    |simplify;apply H3
 420     [intro;elim H5;autobatch
 421     |apply H6]]]]]
 422 qed.
 423
 424 lemma WFE_extends : ∀G,H,U,P.WFType H P → WFEnv (G@(mk_bound true U::H)) → WFEnv (G@(mk_bound true P::H)).
 425 intros;cut (WFType H U)
 426 [generalize in match H2;elim G 0;simplify;intros
 427  [inversion H3;intros;destruct;autobatch
 428  |generalize in match H4;cases a;intros;apply WFE_cons
 429   [inversion H4;intros;destruct;autobatch
 430   |inversion H5;intros;destruct;autobatch]]
 431 |elim G in H2 0;simplify;intros;
 432  [inversion H2;intros;destruct;assumption
 433  |apply H2;inversion H3;simplify;intros;destruct;assumption]]
 434 qed.
 435
 436 (*** lemmata relating subtyping and well-formedness ***)
 437
 438 lemma JS_to_WFE : ∀G,T,U.G ⊢ T ⊴ U → WFEnv G.
 439 intros;elim H;assumption.
 440 qed.
 441
 442 lemma JS_to_WFT : ∀G,T,U.G ⊢ T ⊴ U → WFType G T ∧ WFType G U.
 443 intros;elim H
 444   [1,2:autobatch
 445   |elim H4;split;autobatch
 446   |decompose;autobatch size=7
 447   |decompose;split
 448    [apply WFT_Forall;
 449     [assumption
 450     |apply (WFT_env_incl2 ?? H2) [reflexivity]
 451      simplify;intros 3;elim n
 452      [exists[apply t]
 453       reflexivity
 454      |exists[apply U1]
 455       assumption]]
 456    |autobatch]]
 457 qed.
 458
 459 lemma JS_to_WFT1 : ∀G,T,U.G ⊢ T ⊴ U → WFType G T.
 460 intros;elim (JS_to_WFT ? ? ? H);assumption;
 461 qed.
 462
 463 lemma JS_to_WFT2 : ∀G,T,U.G ⊢ T ⊴ U → WFType G U.
 464 intros;elim (JS_to_WFT ? ? ? H);assumption;
 465 qed.