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