helm/coq-contribs/LAMBDA-TYPES/ty0_subst0.v

   1 Require drop_props.
   2 Require csubst0_defs.
   3 Require fsubst0_defs.
   4 Require pc3_props.
   5 Require pc3_subst0.
   6 Require ty0_defs.
   7 Require ty0_lift.
   8 Require ty0_props.
   9
  10    Section ty0_fsubst0. (****************************************************)
  11
  12 (*#* #stop macro *)
  13
  14       Tactic Definition IH H0 v1 v2 v3 v4 v5 :=
  15          LApply (H0 v1 v2 v3 v4); [ Intros H_x | XEAuto ];
  16          LApply H_x; [ Clear H_x; Intros H_x | XEAuto ];
  17          LApply (H_x v5); [ Clear H_x; Intros | XEAuto ].
  18
  19       Tactic Definition IHT :=
  20          Match Context With
  21             [ H: (i:nat; u0:T; c2:C; t2:T) (fsubst0 i u0 ?1 ?2 c2 t2) ->
  22                  (wf0 ?3 c2) ->
  23                  (e:C) (drop i (0) ?1 (CTail e (Bind Abbr) u0)) -> ?;
  24               _: (subst0 ?4 ?5 ?2 ?6);
  25               _: (drop ?4 (0) ?1 (CTail ?9 (Bind Abbr) ?5)) |- ? ] ->
  26                IH H ?4 ?5 ?1 ?6 ?9.
  27
  28       Tactic Definition IHTb1 :=
  29          Match Context With
  30             [ H: (i:nat; u0:T; c2:C; t2:T) (fsubst0 i u0 (CTail ?1 (Bind ?11) ?10) ?2 c2 t2) ->
  31                  (wf0 ?3 c2) ->
  32                  (e:C) (drop i (0) (CTail ?1 (Bind ?11) ?10) (CTail e (Bind Abbr) u0)) -> ?;
  33               _: (subst0 ?4 ?5 ?10 ?6);
  34               _: (drop ?4 (0) ?1 (CTail ?9 (Bind Abbr) ?5)) |- ? ] ->
  35                IH H '(S ?4) ?5 '(CTail ?1 (Bind ?11) ?6) ?2 ?9.
  36
  37       Tactic Definition IHTb2 :=
  38          Match Context With
  39             [ H: (i:nat; u0:T; c2:C; t2:T) (fsubst0 i u0 (CTail ?1 (Bind ?11) ?10) ?2 c2 t2) ->
  40                  (wf0 ?3 c2) ->
  41                  (e:C) (drop i (0) (CTail ?1 (Bind ?11) ?10) (CTail e (Bind Abbr) u0)) -> ?;
  42               _: (subst0 (s (Bind ?11) ?4) ?5 ?2 ?6);
  43               _: (drop ?4 (0) ?1 (CTail ?9 (Bind Abbr) ?5)) |- ? ] ->
  44                IH H '(S ?4) ?5 '(CTail ?1 (Bind ?11) ?10) ?6 ?9.
  45
  46       Tactic Definition IHC :=
  47          Match Context With
  48             [ H: (i:nat; u0:T; c2:C; t2:T) (fsubst0 i u0 ?1 ?2 c2 t2) ->
  49                  (wf0 ?3 c2) ->
  50                  (e:C) (drop i (0) ?1 (CTail e (Bind Abbr) u0)) -> ?;
  51               _: (csubst0 ?4 ?5 ?1 ?6);
  52               _: (drop ?4 (0) ?1 (CTail ?9 (Bind Abbr) ?5)) |- ? ] ->
  53                IH H ?4 ?5 ?6 ?2 ?9.
  54
  55       Tactic Definition IHCb :=
  56          Match Context With
  57             [ H: (i:nat; u0:T; c2:C; t2:T) (fsubst0 i u0 (CTail ?1 (Bind ?11) ?10) ?2 c2 t2) ->
  58                  (wf0 ?3 c2) ->
  59                  (e:C) (drop i (0) (CTail ?1 (Bind ?11) ?10) (CTail e (Bind Abbr) u0)) -> ?;
  60               _: (csubst0 ?4 ?5 ?1 ?6);
  61               _: (drop ?4 (0) ?1 (CTail ?9 (Bind Abbr) ?5)) |- ? ] ->
  62                IH H '(S ?4) ?5 '(CTail ?6 (Bind ?11) ?10) ?2 ?9.
  63
  64       Tactic Definition IHTTb :=
  65          Match Context With
  66             [ H: (i:nat; u0:T; c2:C; t2:T) (fsubst0 i u0 (CTail ?1 (Bind ?11) ?10) ?2 c2 t2) ->
  67                  (wf0 ?3 c2) ->
  68                  (e:C) (drop i (0) (CTail ?1 (Bind ?11) ?10) (CTail e (Bind Abbr) u0)) -> ?;
  69               _: (subst0 ?4 ?5 ?10 ?6);
  70               _: (subst0 (s (Bind ?11) ?4) ?5 ?2 ?7);
  71               _: (drop ?4 (0) ?1 (CTail ?9 (Bind Abbr) ?5)) |- ? ] ->
  72                IH H '(S ?4) ?5 '(CTail ?1 (Bind ?11) ?6) ?7 ?9.
  73
  74       Tactic Definition IHCT :=
  75          Match Context With
  76             [ H: (i:nat; u0:T; c2:C; t2:T) (fsubst0 i u0 ?1 ?2 c2 t2) ->
  77                  (wf0 ?3 c2) ->
  78                  (e:C) (drop i (0) ?1 (CTail e (Bind Abbr) u0)) -> ?;
  79               _: (csubst0 ?4 ?5 ?1 ?6);
  80               _: (subst0 ?4 ?5 ?2 ?7);
  81               _: (drop ?4 (0) ?1 (CTail ?9 (Bind Abbr) ?5)) |- ? ] ->
  82                IH H ?4 ?5 ?6 ?7 ?9.
  83
  84       Tactic Definition IHCTb1 :=
  85          Match Context With
  86             [ H: (i:nat; u0:T; c2:C; t2:T) (fsubst0 i u0 (CTail ?1 (Bind ?11) ?10) ?2 c2 t2) ->
  87                  (wf0 ?3 c2) ->
  88                  (e:C) (drop i (0) (CTail ?1 (Bind ?11) ?10) (CTail e (Bind Abbr) u0)) -> ?;
  89               _: (csubst0 ?4 ?5 ?1 ?6);
  90               _: (subst0 ?4 ?5 ?10 ?7);
  91               _: (drop ?4 (0) ?1 (CTail ?9 (Bind Abbr) ?5)) |- ? ] ->
  92                IH H '(S ?4) ?5 '(CTail ?6 (Bind ?11) ?7) ?2 ?9.
  93
  94       Tactic Definition IHCTb2 :=
  95          Match Context With
  96             [ H: (i:nat; u0:T; c2:C; t2:T) (fsubst0 i u0 (CTail ?1 (Bind ?11) ?10) ?2 c2 t2) ->
  97                  (wf0 ?3 c2) ->
  98                  (e:C) (drop i (0) (CTail ?1 (Bind ?11) ?10) (CTail e (Bind Abbr) u0)) -> ?;
  99               _: (csubst0 ?4 ?5 ?1 ?6);
 100               _: (subst0 (s (Bind ?11) ?4) ?5 ?2 ?7);
 101               _: (drop ?4 (0) ?1 (CTail ?9 (Bind Abbr) ?5)) |- ? ] ->
 102                IH H '(S ?4) ?5 '(CTail ?6 (Bind ?11) ?10) ?7 ?9.
 103
 104       Tactic Definition IHCTTb :=
 105          Match Context With
 106             [ H: (i:nat; u0:T; c2:C; t2:T) (fsubst0 i u0 (CTail ?1 (Bind ?11) ?10) ?2 c2 t2) ->
 107                  (wf0 ?3 c2) ->
 108                  (e:C) (drop i (0) (CTail ?1 (Bind ?11) ?10) (CTail e (Bind Abbr) u0)) -> ?;
 109               _: (csubst0 ?4 ?5 ?1 ?6);
 110               _: (subst0 ?4 ?5 ?10 ?7);
 111               _: (subst0 (s (Bind ?11) ?4) ?5 ?2 ?8);
 112               _: (drop ?4 (0) ?1 (CTail ?9 (Bind Abbr) ?5)) |- ? ] ->
 113                IH H '(S ?4) ?5 '(CTail ?6 (Bind ?11) ?7) ?8 ?9.
 114
 115 (*#* #start macro *)
 116
 117 (*#* #caption "substitution preserves types" *)
 118 (*#* #cap #cap c1, c2, e, t1, t2, t #alpha u in V *)
 119
 120 (* NOTE: This breaks the mutual recursion between ty0_subst0 and ty0_csubst0 *)
 121       Theorem ty0_fsubst0: (g:?; c1:?; t1,t:?) (ty0 g c1 t1 t) ->
 122                            (i:?; u,c2,t2:?) (fsubst0 i u c1 t1 c2 t2) ->
 123                            (wf0 g c2) ->
 124                            (e:?) (drop i (0) c1 (CTail e (Bind Abbr) u)) ->
 125                            (ty0 g c2 t2 t).
 126
 127 (*#* #stop file *)
 128
 129       Intros until 1; XElim H.
 130 (* case 1: ty0_conv *)
 131       Intros until 6; XElim H4; Intros.
 132 (* case 1.1: fsubst0_snd *)
 133       IHT; EApply ty0_conv; XEAuto.
 134 (* case 1.2: fsubst0_fst *)
 135       IHC; EApply ty0_conv; Try EApply pc3_fsubst0; XEAuto.
 136 (* case 1.3: fsubst0_both *)
 137       IHCT; IHCT; EApply ty0_conv; Try EApply pc3_fsubst0; XEAuto.
 138 (* case 2: ty0_sort *)
 139       Intros until 2; XElim H0; Intros.
 140 (* case 2.1: fsubst0_snd *)
 141       Subst0GenBase.
 142 (* case 2.2: fsubst0_fst *)
 143       XAuto.
 144 (* case 2.3: fsubst0_both *)
 145       Subst0GenBase.
 146 (* case 3: ty0_abbr *)
 147       Intros until 5; XElim H3; Intros; Clear c1 c2 t t1 t2.
 148 (* case 3.1: fsubst0_snd *)
 149       Subst0GenBase; Rewrite H6; Rewrite <- H3 in H5; Clear H3 H6 i t3.
 150       DropDis; Inversion H5; Rewrite <- H6 in H0; Rewrite H7 in H1; XEAuto.
 151 (* case 3.2: fsubst0_fst *)
 152       Apply (lt_le_e n i); Intros; CSubst0Drop.
 153 (* case 3.2.1: n < i, none *)
 154       EApply ty0_abbr; XEAuto.
 155 (* case 3.2.2: n < i, csubst0_snd *)
 156       Inversion H0; CSubst0Drop.
 157       Rewrite <- H10 in H7; Rewrite <- H11 in H7; Rewrite <- H11 in H8; Rewrite <- H12 in H8;
 158       Clear H0 H10 H11 H12 x0 x1 x2.
 159       DropDis; Rewrite minus_x_Sy in H0; [ DropGenBase | XAuto ].
 160       IHT; EApply ty0_abbr; XEAuto.
 161 (* case 3.2.3: n < i, csubst0_fst *)
 162       Inversion H0; CSubst0Drop.
 163       Rewrite <- H10 in H8; Rewrite <- H11 in H7; Rewrite <- H11 in H8; Rewrite <- H12 in H7;
 164       Clear H0 H10 H11 H12 x0 x1 x3.
 165       DropDis; Rewrite minus_x_Sy in H0; [ DropGenBase; CSubst0Drop | XAuto ].
 166       IHC; EApply ty0_abbr; XEAuto.
 167 (* case 3.2.4: n < i, csubst0_both *)
 168       Inversion H0; CSubst0Drop.
 169       Rewrite <- H11 in H9; Rewrite <- H12 in H7; Rewrite <- H12 in H8; Rewrite <- H12 in H9; Rewrite <- H13 in H8;
 170       Clear H0 H11 H12 H13 x0 x1 x3.
 171       DropDis; Rewrite minus_x_Sy in H0; [ DropGenBase; CSubst0Drop | XAuto ].
 172       IHCT; EApply ty0_abbr; XEAuto.
 173 (* case 3.2.5: n >= i *)
 174       EApply ty0_abbr; XEAuto.
 175 (* case 3.3: fsubst0_both *)
 176       Subst0GenBase; Rewrite H7; Rewrite <- H3 in H4; Rewrite <- H3 in H6; Clear H3 H7 i t3.
 177       DropDis; Inversion H6; Rewrite <- H7 in H0; Rewrite H8 in H1.
 178       CSubst0Drop; XEAuto.
 179 (* case 4: ty0_abst *)
 180       Intros until 5; XElim H3; Intros; Clear c1 c2 t t1 t2.
 181 (* case 4.1: fsubst0_snd *)
 182       Subst0GenBase; Rewrite H3 in H0; DropDis; Inversion H0.
 183 (* case 4.2: fsubst0_fst *)
 184       Apply (lt_le_e n i); Intros; CSubst0Drop.
 185 (* case 4.2.1: n < i, none *)
 186       EApply ty0_abst; XEAuto.
 187 (* case 4.2.2: n < i, csubst0_snd *)
 188       Inversion H0; CSubst0Drop.
 189       Rewrite <- H10 in H7; Rewrite <- H11 in H7; Rewrite <- H11 in H8; Rewrite <- H12 in H8; Rewrite <- H12;
 190       Clear H0 H10 H11 H12 x0 x1 x2.
 191       DropDis; Rewrite minus_x_Sy in H0; [ DropGenBase | XAuto ].
 192       IHT; EApply ty0_conv;
 193       [ EApply ty0_lift | EApply ty0_abst | EApply pc3_lift ]; XEAuto.
 194 (* case 4.2.3: n < i, csubst0_fst *)
 195       Inversion H0; CSubst0Drop.
 196       Rewrite <- H10 in H8; Rewrite <- H11 in H7; Rewrite <- H11 in H8; Rewrite <- H12 in H7; Rewrite <- H12;
 197       Clear H0 H10 H11 H12 x0 x1 x3.
 198       DropDis; Rewrite minus_x_Sy in H0; [ DropGenBase; CSubst0Drop | XAuto ].
 199       IHC; EApply ty0_abst; XEAuto.
 200 (* case 4.2.4: n < i, csubst0_both *)
 201       Inversion H0; CSubst0Drop.
 202       Rewrite <- H11 in H9; Rewrite <- H12 in H7; Rewrite <- H12 in H8; Rewrite <- H12 in H9; Rewrite <- H13 in H8; Rewrite <- H13;
 203       Clear H0 H11 H12 H13 x0 x1 x3.
 204       DropDis; Rewrite minus_x_Sy in H0; [ DropGenBase; CSubst0Drop | XAuto ].
 205       IHCT; IHC; EApply ty0_conv;
 206       [ EApply ty0_lift | EApply ty0_abst
 207       | EApply pc3_lift; Try EApply pc3_fsubst0; Try Apply H0
 208       ]; XEAuto.
 209 (* case 4.2.4: n >= i *)
 210       EApply ty0_abst; XEAuto.
 211 (* case 4.3: fsubst0_both *)
 212       Subst0GenBase; Rewrite H3 in H0; DropDis; Inversion H0.
 213 (* case 5: ty0_bind *)
 214       Intros until 7; XElim H5; Intros; Clear H4.
 215 (* case 5.1: fsubst0_snd *)
 216       Subst0GenBase; Rewrite H4; Clear H4 t6.
 217 (* case 5.1.1: subst0 on left argument *)
 218       Ty0Correct; IHT; IHTb1; Ty0Correct.
 219       EApply ty0_conv;
 220       [ EApply ty0_bind | EApply ty0_bind | EApply pc3_fsubst0 ]; XEAuto.
 221 (* case 5.1.2: subst0 on right argument *)
 222       IHTb2; Ty0Correct; EApply ty0_bind; XEAuto.
 223 (* case 5.1.3: subst0 on both arguments *)
 224       Ty0Correct; IHT; IHTb1; IHTTb; Ty0Correct.
 225       EApply ty0_conv;
 226       [ EApply ty0_bind | EApply ty0_bind | EApply pc3_fsubst0 ]; XEAuto.
 227 (* case 5.2: fsubst0_fst *)
 228       IHC; IHCb; Ty0Correct; EApply ty0_bind; XEAuto.
 229 (* case 5.3: fsubst0_both *)
 230       Subst0GenBase; Rewrite H4; Clear H4 t6.
 231 (* case 5.3.1: subst0 on left argument *)
 232       IHC; IHCb; Ty0Correct; Ty0Correct; IHCT; IHCTb1; Ty0Correct.
 233       EApply ty0_conv;
 234       [ EApply ty0_bind | EApply ty0_bind
 235       | EApply pc3_fsubst0; [ Idtac | Idtac | XEAuto ] ]; XEAuto.
 236 (* case 5.3.2: subst0 on right argument *)
 237       IHC; IHCTb2; Ty0Correct; EApply ty0_bind; XEAuto.
 238 (* case 5.3.3: subst0 on both arguments *)
 239       IHC; IHCb; Ty0Correct; Ty0Correct; IHCT; IHCTTb; Ty0Correct.
 240       EApply ty0_conv;
 241       [ EApply ty0_bind | EApply ty0_bind
 242       | EApply pc3_fsubst0; [ Idtac | Idtac | XEAuto ] ]; XEAuto.
 243 (* case 6: ty0_appl *)
 244       Intros until 5; XElim H3; Intros.
 245 (* case 6.1: fsubst0_snd *)
 246       Subst0GenBase; Rewrite H3; Clear H3 c1 c2 t t1 t2 t3.
 247 (* case 6.1.1: subst0 on left argument *)
 248       Ty0Correct; Ty0GenBase; IHT; Ty0Correct.
 249       EApply ty0_conv;
 250       [ EApply ty0_appl | EApply ty0_appl | EApply pc3_fsubst0 ]; XEAuto.
 251 (* case 6.1.2: subst0 on right argument *)
 252       IHT; EApply ty0_appl; XEAuto.
 253 (* case 6.1.3: subst0 on both arguments *)
 254       Ty0Correct; Ty0GenBase; Move H after H10; Ty0Correct; IHT; Clear H2; IHT.
 255       EApply ty0_conv;
 256       [ EApply ty0_appl | EApply ty0_appl | EApply pc3_fsubst0 ]; XEAuto.
 257 (* case 6.2: fsubst0_fst *)
 258       IHC; Clear H2; IHC; EApply ty0_appl; XEAuto.
 259 (* case 6.3: fsubst0_both *)
 260       Subst0GenBase; Rewrite H3; Clear H3 c1 c2 t t1 t2 t3.
 261 (* case 6.3.1: subst0 on left argument *)
 262       IHC; Ty0Correct; Ty0GenBase; Clear H2; IHC; IHCT.
 263       EApply ty0_conv;
 264       [ EApply ty0_appl | EApply ty0_appl
 265       | EApply pc3_fsubst0; [ Idtac | Idtac | XEAuto ] ]; XEAuto.
 266 (* case 6.3.2: subst0 on right argument *)
 267       IHCT; Clear H2; IHC; EApply ty0_appl; XEAuto.
 268 (* case 6.3.3: subst0 on both arguments *)
 269       IHC; Ty0Correct; Ty0GenBase; IHCT; Clear H2; IHC; Ty0Correct; IHCT.
 270       EApply ty0_conv;
 271       [ EApply ty0_appl | EApply ty0_appl
 272       | EApply pc3_fsubst0; [ Idtac | Idtac | XEAuto ] ]; XEAuto.
 273 (* case 7: ty0_cast *)
 274       Clear c1 t t1; Intros until 5; XElim H3; Intros; Clear c2 t3.
 275 (* case 7.1: fsubst0_snd *)
 276       Subst0GenBase; Rewrite H3; Clear H3 t4.
 277 (* case 7.1.1: subst0 on left argument *)
 278       IHT; EApply ty0_conv;
 279       [ Idtac
 280       | EApply ty0_cast;
 281         [ EApply ty0_conv; [ Idtac | Idtac | Apply pc3_s; EApply pc3_fsubst0 ]
 282         | Idtac ]
 283       | EApply pc3_fsubst0 ]; XEAuto.
 284 (* case 7.1.2: subst0 on right argument *)
 285       IHT; EApply ty0_cast; XEAuto.
 286 (* case 7.1.3: subst0 on both arguments *)
 287       IHT; Clear H2; IHT.
 288       EApply ty0_conv;
 289       [ Idtac
 290       | EApply ty0_cast;
 291         [ EApply ty0_conv; [ Idtac | Idtac | Apply pc3_s; EApply pc3_fsubst0 ]
 292         | Idtac ]
 293       | EApply pc3_fsubst0 ]; XEAuto.
 294 (* case 7.2: fsubst0_fst *)
 295       IHC; Clear H2; IHC; EApply ty0_cast; XEAuto.
 296 (* case 6.3: fsubst0_both *)
 297       Subst0GenBase; Rewrite H3; Clear H3 t4.
 298 (* case 7.3.1: subst0 on left argument *)
 299       IHC; IHCT; Clear H2; IHC.
 300       EApply ty0_conv;
 301       [ Idtac
 302       | EApply ty0_cast;
 303         [ EApply ty0_conv; [ Idtac | Idtac | Apply pc3_s; EApply pc3_fsubst0; [ Idtac | Idtac | XEAuto ] ]
 304         | Idtac ]
 305       | EApply pc3_fsubst0; [ Idtac | Idtac | XEAuto ] ]; XEAuto.
 306 (* case 7.3.2: subst0 on right argument *)
 307       IHCT; IHC; EApply ty0_cast; XEAuto.
 308 (* case 7.3.3: subst0 on both arguments *)
 309       IHC; IHCT; Clear H2; IHCT.
 310       EApply ty0_conv;
 311       [ Idtac
 312       | EApply ty0_cast;
 313         [ EApply ty0_conv; [ Idtac | Idtac | Apply pc3_s; EApply pc3_fsubst0; [ Idtac | Idtac | XEAuto ] ]
 314         | Idtac ]
 315       | EApply pc3_fsubst0; [ Idtac | Idtac | XEAuto ] ]; XEAuto.
 316       Qed.
 317
 318       Theorem ty0_csubst0: (g:?; c1:?; t1,t2:?) (ty0 g c1 t1 t2) ->
 319                            (e:?; u:?; i:?) (drop i (0) c1 (CTail e (Bind Abbr) u)) ->
 320                            (c2:?) (wf0 g c2) -> (csubst0 i u c1 c2) ->
 321                            (ty0 g c2 t1 t2).
 322       Intros; EApply ty0_fsubst0; XEAuto.
 323       Qed.
 324
 325       Theorem ty0_subst0: (g:?; c:?; t1,t:?) (ty0 g c t1 t) ->
 326                           (e:?; u:?; i:?) (drop i (0) c (CTail e (Bind Abbr) u)) ->
 327                           (t2:?) (subst0 i u t1 t2) -> (ty0 g c t2 t).
 328       Intros; EApply ty0_fsubst0; XEAuto.
 329       Qed.
 330
 331    End ty0_fsubst0.
 332
 333       Hints Resolve ty0_subst0 : ltlc.