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