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

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