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

   1 Require lift_gen.
   2 Require subst1_gen.
   3 Require csubst1_defs.
   4 Require pr0_lift.
   5 Require pr0_subst1.
   6 Require cpr0_defs.
   7 Require pc1_props.
   8 Require pc3_props.
   9 Require pc3_gen.
  10 Require ty0_defs.
  11 Require ty0_gen.
  12 Require ty0_lift.
  13 Require ty0_props.
  14 Require ty0_subst0.
  15 Require ty0_gen_context.
  16 Require csub0_defs.
  17 Require csub0_props.
  18
  19 (*#* #caption "subject reduction" #clauses *)
  20
  21 (*#* #stop file *)
  22
  23    Section ty0_sred_cpr0_pr0. (**********************************************)
  24
  25       Tactic Definition IH H c2 t2 :=
  26          LApply (H c2); [ Intros H_x | XEAuto ];
  27          LApply H_x; [ Clear H_x; Intros H_x | XAuto ];
  28          LApply (H_x t2); [ Clear H_x; Intros | XEAuto ].
  29
  30       Tactic Definition IH0 :=
  31          Match Context With
  32             [ H1: (c2:C) (wf0 ?1 c2)->(cpr0 ?2 c2)->(t2:T)(pr0 ?3 t2)->(ty0 ?1 c2 t2 ?4);
  33               H2: (cpr0 ?2 ?5); H3: (ty0 ?1 ?2 ?3 ?4) |- ? ] ->
  34                IH H1 ?5 ?3.
  35
  36       Tactic Definition IH0c :=
  37          Match Context With
  38             [ H1: (c2:C) (wf0 ?1 c2)->(cpr0 ?2 c2)->(t2:T)(pr0 ?3 t2)->(ty0 ?1 c2 t2 ?4);
  39               H2: (cpr0 ?2 ?5); H3: (ty0 ?1 ?2 ?3 ?4) |- ? ] ->
  40                IH H1 ?5 ?3; Clear H1.
  41
  42       Tactic Definition IH0B :=
  43          Match Context With
  44             [ H1: (c2:C) (wf0 ?1 c2)->(cpr0 (CTail ?2 (Bind ?6) ?7) c2)->(t2:T)(pr0 ?3 t2)->(ty0 ?1 c2 t2 ?4);
  45               H2: (cpr0 ?2 ?5); H3: (ty0 ?1 (CTail ?2 (Bind ?6) ?7) ?3 ?4) |- ? ] ->
  46                IH H1 '(CTail ?5 (Bind ?6) ?7) ?3.
  47
  48       Tactic Definition IH0Bc :=
  49          Match Context With
  50             [ H1: (c2:C) (wf0 ?1 c2)->(cpr0 (CTail ?2 (Bind ?6) ?7) c2)->(t2:T)(pr0 ?3 t2)->(ty0 ?1 c2 t2 ?4);
  51               H2: (cpr0 ?2 ?5); H3: (ty0 ?1 (CTail ?2 (Bind ?6) ?7) ?3 ?4) |- ? ] ->
  52                IH H1 '(CTail ?5 (Bind ?6) ?7) ?3; Clear H1.
  53
  54       Tactic Definition IH1 :=
  55          Match Context With
  56             [ H1: (c2:C) (wf0 ?1 c2)->(cpr0 ?2 c2)->(t2:T)(pr0 ?3 t2)->(ty0 ?1 c2 t2 ?4);
  57               H2: (cpr0 ?2 ?5); H3: (pr0 ?3 ?6) |- ? ] ->
  58             IH H1 ?5 ?6.
  59
  60       Tactic Definition IH1c :=
  61          Match Context With
  62             [ H1: (c2:C) (wf0 ?1 c2)->(cpr0 ?2 c2)->(t2:T)(pr0 ?3 t2)->(ty0 ?1 c2 t2 ?4);
  63               H2: (cpr0 ?2 ?5); H3: (pr0 ?3 ?6) |- ? ] ->
  64             IH H1 ?5 ?6; Clear H1.
  65
  66       Tactic Definition IH1Bc :=
  67          Match Context With
  68             [ H1: (c2:C) (wf0 ?1 c2)->(cpr0 (CTail ?2 (Bind ?7) ?8) c2)->(t2:T)(pr0 ?3 t2)->(ty0 ?1 c2 t2 ?4);
  69               H2: (cpr0 ?2 ?5); H3: (pr0 ?3 ?6) |- ? ] ->
  70             IH H1 '(CTail ?5 (Bind ?7) ?8) ?6; Clear H1.
  71
  72       Tactic Definition IH1BLc :=
  73          Match Context With
  74             [ H1: (c2:C) (wf0 ?1 c2)->(cpr0 (CTail ?2 (Bind ?7) ?8) c2)->(t2:T)(pr0 (lift ?10 ?11 ?3) t2)->(ty0 ?1 c2 t2 ?4);
  75               H2: (cpr0 ?2 ?5); H3: (pr0 ?3 ?6) |- ? ] ->
  76             IH H1 '(CTail ?5 (Bind ?7) ?8) '(lift ?10 ?11 ?6); Clear H1.
  77
  78       Tactic Definition IH1T :=
  79          Match Context With
  80             [ H1: (c2:C) (wf0 ?1 c2)->(cpr0 ?2 c2)->(t2:T)(pr0 (TTail ?7 ?8 ?3) t2)->(ty0 ?1 c2 t2 ?4);
  81               H2: (cpr0 ?2 ?5); H3: (pr0 ?3 ?6) |- ? ] ->
  82             IH H1 ?5 '(TTail ?7 ?8 ?6).
  83
  84       Tactic Definition IH1T2c :=
  85          Match Context With
  86             [ H1: (c2:C) (wf0 ?1 c2)->(cpr0 ?2 c2)->(t2:T)(pr0 (TTail ?7 ?8 ?3) t2)->(ty0 ?1 c2 t2 ?4);
  87               H2: (cpr0 ?2 ?5); H3: (pr0 ?3 ?6); H4: (pr0 ?8 ?9) |- ? ] ->
  88             IH H1 ?5 '(TTail ?7 ?9 ?6); Clear H1.
  89
  90       Tactic Definition IH3B :=
  91          Match Context With
  92             [ H1: (c2:C) (wf0 ?1 c2)->(cpr0 (CTail ?2 (Bind ?7) ?8) c2)->(t2:T)(pr0 ?3 t2)->(ty0 ?1 c2 t2 ?4);
  93               H2: (cpr0 ?2 ?5); H3: (pr0 ?3 ?6); H4: (pr0 ?8 ?9) |- ? ] ->
  94             IH H1 '(CTail ?5 (Bind ?7) ?9) ?6.
  95
  96 (*#* #start file *)
  97
  98 (*#* #caption "base case" *)
  99 (*#* #cap #cap c1, c2 #alpha t1 in T, t2 in T1, t in T2 *)
 100
 101       Theorem ty0_sred_cpr0_pr0: (g:?; c1:?; t1,t:?) (ty0 g c1 t1 t) ->
 102                                  (c2:?) (wf0 g c2) -> (cpr0 c1 c2) ->
 103                                  (t2:?) (pr0 t1 t2) -> (ty0 g c2 t2 t).
 104
 105 (*#* #stop file *)
 106
 107       Intros until 1; XElim H; Intros.
 108 (* case 1: ty0_conv *)
 109       IH1c; IH0c; EApply ty0_conv; XEAuto.
 110 (* case 2: ty0_sort *)
 111       Inversion H2; XAuto.
 112 (* case 3: ty0_abbr *)
 113       Inversion H5; Cpr0Drop; IH1c; XEAuto.
 114 (* case 4: ty0_abst *)
 115       Intros; Inversion H5; Cpr0Drop; IH0; IH1.
 116       EApply ty0_conv;
 117       [ EApply ty0_lift; [ Idtac | XAuto | XEAuto ]
 118       | EApply ty0_abst
 119       | EApply pc3_lift ]; XEAuto.
 120 (* case 5: ty0_bind *)
 121       Intros; Inversion H7; Clear H7.
 122 (* case 5.1: pr0_refl *)
 123       IH0c; IH0Bc; IH0Bc.
 124       EApply ty0_bind; XEAuto.
 125 (* case 5.2: pr0_cont *)
 126       IH0; IH0B; Ty0Correct; IH3B; Ty0Correct.
 127       EApply ty0_conv; [ EApply ty0_bind | EApply ty0_bind | Idtac ]; XEAuto.
 128 (* case 5.3: pr0_delta *)
 129       Rewrite <- H8 in H1; Rewrite <- H8 in H2;
 130       Rewrite <- H8 in H3; Rewrite <- H8 in H4; Clear H8 b.
 131       IH0; IH0B; Ty0Correct; IH3B; Ty0Correct.
 132       EApply ty0_conv; [ EApply ty0_bind | EApply ty0_bind | Idtac ]; XEAuto.
 133 (* case 5.4: pr0_zeta *)
 134       Rewrite <- H11 in H1; Rewrite <- H11 in H2; Clear H8 H9 H10 H11 b0 t2 t7 u0.
 135       IH0; IH1BLc; Move H3 after H8; IH0Bc; Ty0Correct; Move H8 after H4; Clear H H0 H1 H3 H6 c c1 t t1;
 136       NewInduction b.
 137 (* case 5.4.1: Abbr *)
 138       Ty0GenContext; Subst1Gen; LiftGen; Rewrite H in H1; Clear H x0.
 139       EApply ty0_conv;
 140       [ EApply ty0_bind; XEAuto | XEAuto
 141       | EApply pc3_pr3_x;
 142         EApply (pr3_t (TTail (Bind Abbr) u (lift (1) (0) x1))); XEAuto ].
 143 (* case 5.4.2: Abst *)
 144       EqFalse.
 145 (* case 5.4.3: Void *)
 146       Ty0GenContext; Rewrite H0; Rewrite H0 in H2; Clear H0 t3.
 147       LiftGen; Rewrite <- H in H1; Clear H x0.
 148       EApply ty0_conv; [ EApply ty0_bind; XEAuto | XEAuto | XAuto ].
 149 (* case 6: ty0_appl *)
 150       Intros; Inversion H5; Clear H5.
 151 (* case 6.1: pr0_refl *)
 152       IH0c; IH0c; EApply ty0_appl; XEAuto.
 153 (* case 6.2: pr0_cont *)
 154       Clear H6 H7 H8 H9 c1 k t t1 t2 t3 u1.
 155       IH0; Ty0Correct; Ty0GenBase; IH1c; IH0; IH1c.
 156       EApply ty0_conv;
 157       [ EApply ty0_appl; [ XEAuto | EApply ty0_bind; XEAuto ]
 158       | EApply ty0_appl; XEAuto
 159       | XEAuto ].
 160 (* case 6.3: pr0_beta *)
 161       Rewrite <- H7 in H1; Rewrite <- H7 in H2; Clear H6 H7 H9 c1 t t1 t2 v v1.
 162       IH1T; IH0c; Ty0Correct; Ty0GenBase; IH0; IH1c.
 163       Move H5 after H13; Ty0GenBase; Pc3Gen; Repeat CSub0Ty0.
 164       EApply ty0_conv;
 165       [ Apply ty0_appl; [ Idtac | EApply ty0_bind ]
 166       | EApply ty0_bind
 167       | Apply (pc3_t (TTail (Bind Abbr) v2 t0))
 168       ]; XEAuto.
 169 (* case 6.4: pr0_delta *)
 170       Rewrite <- H7 in H1; Rewrite <- H7 in H2; Clear H6 H7 H11 c1 t t1 t2 v v1.
 171       IH1T2c; Clear H1; Ty0Correct; NonLinear; Ty0GenBase; IH1; IH0c.
 172       Move H5 after H1; Ty0GenBase; Pc3Gen; Rewrite lift_bind in H0.
 173       Move H1 after H0; Ty0Lift b u2; Rewrite lift_bind in H17.
 174       Ty0GenBase.
 175       EApply ty0_conv;
 176       [ Apply ty0_appl; [ Idtac | EApply ty0_bind ]; XEAuto
 177       | EApply ty0_bind;
 178         [ Idtac
 179         | EApply ty0_appl; [ EApply ty0_lift | EApply ty0_conv ]
 180         | EApply ty0_appl; [ EApply ty0_lift | EApply ty0_bind ]
 181         ]; XEAuto
 182       | Idtac ].
 183       Rewrite <- lift_bind; Apply pc3_pc1;
 184       Apply (pc1_pr0_u2 (TTail (Flat Appl) v2 (TTail (Bind b) u2 (lift (1) (0) (TTail (Bind Abst) u t0))))); XAuto.
 185 (* case 7: ty0_cast *)
 186       Intros; Inversion H5; Clear H5.
 187 (* case 7.1: pr0_refl *)
 188       IH0c; IH0c; EApply ty0_cast; XEAuto.
 189 (* case 7.2: pr0_cont *)
 190       Clear H6 H7 H8 H9 c1 k u1 t t1 t4 t5.
 191       IH0; IH1c; IH1c.
 192       EApply ty0_conv;
 193       [ XEAuto
 194       | EApply ty0_cast; [ EApply ty0_conv; XEAuto | XEAuto ]
 195       | XAuto ].
 196 (* case 7.3: pr0_epsilon *)
 197       XAuto.
 198       Qed.
 199
 200    End ty0_sred_cpr0_pr0.
 201
 202    Section ty0_sred_pr3. (**********************************************)
 203
 204       Theorem ty0_sred_pr1: (c:?; t1,t2:?) (pr1 t1 t2) ->
 205                             (g:?; t:?) (ty0 g c t1 t) ->
 206                             (ty0 g c t2 t).
 207       Intros until 1; XElim H; Intros.
 208 (* case 1: pr1_r *)
 209       XAuto.
 210 (* case 2: pr1_u *)
 211       EApply H1; EApply ty0_sred_cpr0_pr0; XEAuto.
 212       Qed.
 213
 214       Theorem ty0_sred_pr2: (c:?; t1,t2:?) (pr2 c t1 t2) ->
 215                             (g:?; t:?) (ty0 g c t1 t) ->
 216                             (ty0 g c t2 t).
 217       Intros until 1; XElim H; Intros.
 218 (* case 1: pr2_free *)
 219       EApply ty0_sred_cpr0_pr0; XEAuto.
 220 (* case 2: pr2_u *)
 221       EApply ty0_subst0; Try EApply ty0_sred_cpr0_pr0; XEAuto.
 222       Qed.
 223
 224 (*#* #start file *)
 225
 226 (*#* #caption "general case without the reduction in the context" *)
 227 (*#* #cap #cap c #alpha t1 in T, t2 in T1, t in T2 *)
 228
 229       Theorem ty0_sred_pr3: (c:?; t1,t2:?) (pr3 c t1 t2) ->
 230                             (g:?; t:?) (ty0 g c t1 t) ->
 231                             (ty0 g c t2 t).
 232
 233 (*#* #stop file *)
 234
 235       Intros until 1; XElim H; Intros.
 236 (* case 1: pr3_refl *)
 237       XAuto.
 238 (* case 2: pr3_sing *)
 239       EApply H1; EApply ty0_sred_pr2; XEAuto.
 240       Qed.
 241
 242    End ty0_sred_pr3.
 243
 244       Tactic Definition Ty0SRed :=
 245          Match Context With
 246             | [ H1: (pr3 ?1 ?2 ?3); H2: (ty0 ?4 ?1 ?2 ?5) |- ? ] ->
 247                LApply (ty0_sred_pr3 ?1 ?2 ?3); [ Intros H_x | XAuto ];
 248                LApply (H_x ?4 ?5); [ Clear H2 H_x; Intros | XAuto ].
 249
 250 (*#* #start file *)
 251
 252 (*#* #single *)