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

   1 (*#* #stop file *)
   2
   3 Require lift_gen.
   4 Require lift_props.
   5 Require subst1_defs.
   6 Require subst1_lift.
   7 Require subst1_confluence.
   8 Require drop_props.
   9 Require csubst1_defs.
  10 Require pc3_gen.
  11 Require pc3_gen_context.
  12 Require ty0_defs.
  13 Require ty0_lift.
  14
  15 (* NOTE: these break the recursion between ty0_sred_cpr0_pr0 and ty0_gen_lift *)
  16
  17    Section ty0_gen_cabbr. (**************************************************)
  18
  19       Tactic Definition IH d a0 a :=
  20          Match Context With
  21             [ H: (e:?; u:?; d:?) ? -> (a0:?) ? -> (a:?) ? -> ? -> ? |- ? ] ->
  22                LApply (H e u0 d); [ Clear H; Intros H | XAuto ];
  23                LApply (H a0); [ Clear H; Intros H | XAuto ];
  24                LApply (H a); [ Clear H; Intros H | XEAuto ];
  25                LApply H; [ Clear H; Intros H | XAuto ];
  26                XElim H; Intros.
  27
  28 (* NOTE: This can be generalized removing the last three premises *)
  29       Theorem ty0_gen_cabbr: (g:?; c:?; t1,t2:?) (ty0 g c t1 t2) ->
  30                              (e:?; u:?; d:?) (drop d (0) c (CTail e (Bind Abbr) u)) ->
  31                              (a0:?) (csubst1 d u c a0) ->
  32                              (a:?) (wf0 g a) -> (drop (1) d a0 a) ->
  33                              (EX y1 y2 | (subst1 d u t1 (lift (1) d y1)) &
  34                                          (subst1 d u t2 (lift (1) d y2)) &
  35                                          (ty0 g a y1 y2)
  36                              ).
  37       Intros until 1; XElim H; Intros.
  38 (* case 1: ty0_conv *)
  39       Repeat IH d a0 a; EApply ex3_2_intro;
  40       [ XEAuto | XEAuto | EApply ty0_conv; Try EApply pc3_gen_cabbr; XEAuto ].
  41 (* case 2: ty0_sort *)
  42       EApply ex3_2_intro; Try Rewrite lift_sort; XAuto.
  43 (* case 3: ty0_abbr *)
  44       Apply (lt_eq_gt_e n d0); Intros; Clear c t1 t2.
  45 (* case 3.1: n < d0 *)
  46       Clear H1; DropDis; Rewrite minus_x_Sy in H1; [ DropGenBase | XAuto ].
  47       CSubst1Drop; Rewrite minus_x_Sy in H0; [ Idtac | XAuto ].
  48       CSubst1GenBase; Rewrite H0 in H8; Clear H0 x; Simpl in H9.
  49       Rewrite (lt_plus_minus n d0) in H6; [ Idtac | XAuto ].
  50       DropDis; Rewrite H0 in H9; Clear H0 x0.
  51       IH '(minus d0 (S n)) x1 x3.
  52       Subst1Confluence; Rewrite H0 in H11; Clear H0 x0.
  53       Pattern 3 d0; Rewrite (le_plus_minus_sym (S n) d0); [ Idtac | XAuto ].
  54       Pattern 4 d0; Rewrite (le_plus_minus (S n) d0); [ Idtac | XAuto ].
  55       EApply ex3_2_intro;
  56       [ Rewrite lift_lref_lt | Rewrite lift_d | EApply ty0_abbr ]; XEAuto.
  57 (* case 3.2: n = d0 *)
  58       Rewrite H7; Rewrite H7 in H0; Clear H2 H7 n.
  59       DropDis; Inversion H0; Rewrite H8 in H4; Clear H0 H7 H8 e u0.
  60       CSubst1Drop; DropDis.
  61       EApply ex3_2_intro;
  62       [ EApply subst1_single; Rewrite lift_free; Simpl; XEAuto
  63       | Rewrite lift_free; Simpl; XEAuto
  64       | XEAuto ].
  65 (* case 3.3: n > d0 *)
  66       Clear H2 H3 e; CSubst1Drop; DropDis.
  67       Pattern 1 n; Rewrite (lt_plus_minus (0) n); [ Idtac | XEAuto ].
  68       Arith4c '(0) '(minus n (1)).
  69       EApply ex3_2_intro;
  70       [ Rewrite lift_lref_ge
  71       | Rewrite lift_free; Simpl
  72       | Pattern 2 n; Rewrite (minus_x_SO n)
  73       ]; XEAuto.
  74 (* case 4: ty0_abst *)
  75       Apply (lt_eq_gt_e n d0); Intros; Clear c t1 t2.
  76 (* case 4.1: n < d0 *)
  77       Clear H1; DropDis; Rewrite minus_x_Sy in H1; [ DropGenBase | XAuto ].
  78       CSubst1Drop; Rewrite minus_x_Sy in H0; [ Idtac | XAuto ].
  79       CSubst1GenBase; Rewrite H0 in H8; Clear H0 x; Simpl in H9.
  80       Rewrite (lt_plus_minus n d0) in H6; [ Idtac | XAuto ].
  81       DropDis; Rewrite H0 in H9; Clear H0 x0.
  82       IH '(minus d0 (S n)) x1 x3.
  83       Subst1Confluence; Rewrite H0 in H11; Clear H0 x0.
  84       Pattern 3 d0; Rewrite (le_plus_minus_sym (S n) d0); [ Idtac | XAuto ].
  85       Pattern 4 d0; Rewrite (le_plus_minus (S n) d0); [ Idtac | XAuto ].
  86       EApply ex3_2_intro;
  87       [ Rewrite lift_lref_lt | Rewrite lift_d | EApply ty0_abst ]; XEAuto.
  88 (* case 4.2: n = d0 *)
  89       Rewrite H7; Rewrite H7 in H0; DropDis; Inversion H0.
  90 (* case 4.3: n > d0 *)
  91       Clear H2 H3 e; CSubst1Drop; DropDis.
  92       Pattern 1 n; Rewrite (lt_plus_minus (0) n); [ Idtac | XEAuto ].
  93       Arith4c '(0) '(minus n (1)).
  94       EApply ex3_2_intro;
  95       [ Rewrite lift_lref_ge
  96       | Rewrite lift_free; Simpl
  97       | Pattern 2 n; Rewrite (minus_x_SO n)
  98       ]; XEAuto.
  99 (* case 5: ty0_bind *)
 100       IH d a0 a; Clear H H1 H3 c t1 t2.
 101       IH '(S d) '(CTail a0 (Bind b) (lift (1) d x0)) '(CTail a (Bind b) x0).
 102       IH '(S d) '(CTail a0 (Bind b) (lift (1) d x0)) '(CTail a (Bind b) x0).
 103       Subst1Confluence; Rewrite H4 in H11; Clear H4 x5.
 104       EApply ex3_2_intro; Try Rewrite lift_bind; XEAuto.
 105 (* case 6: ty0_appl *)
 106       Repeat IH d a0 a; Clear H H1 c t1 t2.
 107       Subst1GenBase; SymEqual; LiftGenBase; Rewrite H in H8; Rewrite H11 in H1; Rewrite H12 in H7; Clear H H11 H12 x1 x4 x5.
 108       Subst1Confluence; Rewrite H in H8; Clear H x6.
 109       EApply ex3_2_intro; Try Rewrite lift_flat;
 110       [ Idtac | EApply subst1_tail; [ Idtac | Rewrite lift_bind ] | Idtac ]; XEAuto.
 111 (* case 7: ty0_cast *)
 112       Rename u into u0; Repeat IH d a0 a; Clear H H1 c t1 t2.
 113       Subst1Confluence; Rewrite H in H10; Clear H x3.
 114       EApply ex3_2_intro; [ Rewrite lift_flat | Idtac | Idtac ]; XEAuto.
 115       Qed.
 116
 117    End ty0_gen_cabbr.
 118
 119    Section ty0_gen_cvoid. (**************************************************)
 120
 121       Tactic Definition IH d a :=
 122          Match Context With
 123             [ H: (e:?; u:?; d:?) ? -> (a:?) ? -> ? -> ? |- ? ] ->
 124                LApply (H e u0 d); [ Clear H; Intros H | XAuto ];
 125                LApply (H a); [ Clear H; Intros H | XEAuto ];
 126                LApply H; [ Clear H; Intros H | XAuto ];
 127                XElim H; Intros.
 128
 129 (* NOTE: This can be generalized removing the last two premises *)
 130       Theorem ty0_gen_cvoid: (g:?; c:?; t1,t2:?) (ty0 g c t1 t2) ->
 131                              (e:?; u:?; d:?) (drop d (0) c (CTail e (Bind Void) u)) ->
 132                              (a:?) (wf0 g a) -> (drop (1) d c a) ->
 133                              (EX y1 y2 | t1 = (lift (1) d y1) &
 134                                          t2 = (lift (1) d y2) &
 135                                          (ty0 g a y1 y2)
 136                              ).
 137       Intros until 1; XElim H; Intros.
 138 (* case 1: ty0_conv *)
 139       Repeat IH d a; Rewrite H0 in H3; Rewrite H7 in H3; Pc3Gen; XEAuto.
 140 (* case 2: ty0_sort *)
 141       EApply ex3_2_intro; Try Rewrite lift_sort; XEAuto.
 142 (* case 3: ty0_abbr *)
 143       Apply (lt_eq_gt_e n d0); Intros.
 144 (* case 3.1: n < d0 *)
 145       DropDis; Rewrite minus_x_Sy in H7; [ DropGenBase | XAuto ].
 146       Rewrite (lt_plus_minus n d0) in H5; [ Idtac | XAuto ].
 147       DropDis; Rewrite H0 in H2; Clear H0 H1 u.
 148       IH '(minus d0 (S n)) x1; Rewrite H1; Clear H1 t.
 149       LiftGen; Rewrite <- H0 in H2; Clear H0 x2.
 150       Rewrite <- lift_d; [ Idtac | XAuto ].
 151       Rewrite <- le_plus_minus; [ Idtac | XAuto ].
 152       EApply ex3_2_intro; [ Rewrite lift_lref_lt | Idtac | EApply ty0_abbr ]; XEAuto.
 153 (* case 3.2: n = d0 *)
 154       Rewrite H6 in H0; DropDis; Inversion H0.
 155 (* case 3.3: n > d0 *)
 156       Clear H2 H3 c e t1 t2 u0; DropDis.
 157       Pattern 1 n; Rewrite (lt_plus_minus (0) n); [ Idtac | XEAuto ].
 158       Arith4c '(0) '(minus n (1)).
 159       EApply ex3_2_intro;
 160       [ Rewrite lift_lref_ge
 161       | Rewrite lift_free; Simpl
 162       | Pattern 2 n; Rewrite (minus_x_SO n)
 163       ]; XEAuto.
 164 (* case 4: ty0_abst *)
 165       Apply (lt_eq_gt_e n d0); Intros.
 166 (* case 4.1: n < d0 *)
 167       DropDis; Rewrite minus_x_Sy in H7; [ DropGenBase | XAuto ].
 168       Rewrite (lt_plus_minus n d0) in H5; [ Idtac | XAuto ].
 169       DropDis; Rewrite H0; Rewrite H0 in H2; Clear H0 H1 u.
 170       IH '(minus d0 (S n)) x1; Clear H1 t.
 171       LiftGen; Rewrite <- H0 in H2; Clear H0 x2.
 172       Rewrite <- lift_d; [ Idtac | XAuto ].
 173       Rewrite <- le_plus_minus; [ Idtac | XAuto ].
 174       EApply ex3_2_intro; [ Rewrite lift_lref_lt | Idtac | EApply ty0_abst ]; XEAuto.
 175 (* case 4.2: n = d0 *)
 176       Rewrite H6 in H0; DropDis; Inversion H0.
 177 (* case 4.3: n > d0 *)
 178       Clear H2 H3 c e t1 t2 u0; DropDis.
 179       Pattern 1 n; Rewrite (lt_plus_minus (0) n); [ Idtac | XEAuto ].
 180       Arith4c '(0) '(minus n (1)).
 181       EApply ex3_2_intro;
 182       [ Rewrite lift_lref_ge
 183       | Rewrite lift_free; [ Simpl | Simpl | Idtac ]
 184       | Pattern 2 n; Rewrite (minus_x_SO n)
 185       ]; XEAuto.
 186 (* case 5: ty0_bind *)
 187       IH d a; Rewrite H0; Rewrite H0 in H2; Rewrite H0 in H4; Clear H H0 H1 H3 H8 u t.
 188       IH '(S d) '(CTail a (Bind b) x0); Rewrite H; Rewrite H in H2; Clear H H0 t3 t4.
 189       IH '(S d) '(CTail a (Bind b) x0); Rewrite H; Clear H t0.
 190       LiftGen; Rewrite <- H in H2; Clear H x5.
 191       LiftTailRwBack; XEAuto.
 192 (* case 6: ty0_appl *)
 193       IH d a; Rewrite H2; Clear H H1 H2 v.
 194       LiftGenBase; Rewrite H in H7; Rewrite H1; Rewrite H1 in H0; Rewrite H2; Clear H H1 H2 u t x1.
 195       IH d a; Rewrite H; Clear H w.
 196       LiftGen; Rewrite <- H in H1; Clear H x4.
 197       LiftTailRwBack; XEAuto.
 198 (* case 7: ty0_cast *)
 199       Rename u into u0.
 200       IH d a; Rewrite H2 in H0; Rewrite H2; Clear H H1 H2 H6 t3 t4.
 201       IH d a; Rewrite H; Clear H t0.
 202       LiftGen; Rewrite <- H in H1; Clear H x3.
 203       LiftTailRwBack; XEAuto.
 204       Qed.
 205
 206    End ty0_gen_cvoid.
 207
 208       Tactic Definition Ty0GenContext :=
 209          Match Context With
 210             | [ H: (ty0 ?1 (CTail ?2 (Bind Abbr) ?3) ?4 ?5) |- ? ] ->
 211                LApply (ty0_gen_cabbr ?1 (CTail ?2 (Bind Abbr) ?3) ?4 ?5); [ Clear H; Intros H | XAuto ];
 212                LApply (H ?2 ?3 (0)); [ Clear H; Intros H | XAuto ];
 213                LApply (H (CTail ?2 (Bind Abbr) ?3)); [ Clear H; Intros H | XAuto ];
 214                LApply (H ?2); [ Clear H; Intros H | XAuto ];
 215                LApply H; [ Clear H; Intros H | XAuto ];
 216                XElim H; Intros
 217             | [ H: (ty0 ?1 (CTail ?2 (Bind Void) ?3) ?4 ?5) |- ? ] ->
 218                LApply (ty0_gen_cvoid ?1 (CTail ?2 (Bind Void) ?3) ?4 ?5); [ Clear H; Intros H | XAuto ];
 219                LApply (H ?2 ?3 (0)); [ Clear H; Intros H | XAuto ];
 220                LApply (H ?2); [ Clear H; Intros H | XAuto ];
 221                LApply H; [ Clear H; Intros H | XAuto ];
 222                XElim H; Intros
 223             | _ -> Ty0GenBase.
 224
 225 (*#* #start file *)
 226
 227 (*#* #single *)