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

   1 (*#* #stop file *)
   2
   3 Require drop_props.
   4 Require subst1_gen.
   5 Require subst1_subst1.
   6 Require subst1_confluence.
   7 Require csubst1_defs.
   8 Require pr0_gen.
   9 Require pr0_subst1.
  10 Require pr2_defs.
  11 Require pr2_subst1.
  12
  13    Section pr2_gen_context. (************************************************)
  14
  15       Theorem pr2_gen_cabbr: (c:?; t1,t2:?) (pr2 c t1 t2) -> (e:?; u:?; d:?)
  16                              (drop d (0) c (CTail e (Bind Abbr) u)) ->
  17                              (a0:?) (csubst1 d u c a0) ->
  18                              (a:?) (drop (1) d a0 a) ->
  19                              (x1:?) (subst1 d u t1 (lift (1) d x1)) ->
  20                              (EX x2 | (subst1 d u t2 (lift (1) d x2)) &
  21                                       (pr2 a x1 x2)
  22                              ).
  23       Intros until 1; XElim H; Intros.
  24 (* case 1: pr2_pr0 *)
  25       Pr0Subst1; Pr0Gen; Rewrite H in H3; Clear H x; XEAuto.
  26 (* case 2: pr2_delta *)
  27       Apply (lt_eq_gt_e i d0); Intros.
  28 (* case 2.1: i < d0 *)
  29       Subst1Confluence; CSubst1Drop.
  30       Rewrite minus_x_Sy in H; [ Idtac | XAuto ].
  31       CSubst1GenBase; Rewrite H in H6; Clear H x0.
  32       Rewrite (lt_plus_minus i d0) in H3; [ Idtac | XAuto ].
  33       DropDis; Rewrite H in H7; Clear H x2.
  34       Subst1Subst1; Pattern 2 d0 in H; Rewrite (lt_plus_minus i d0) in H; [ Idtac | XAuto ].
  35       Subst1Gen; Rewrite H in H9; Simpl in H9; Clear H x2.
  36       Rewrite <- lt_plus_minus in H9; [ Idtac | XAuto ].
  37       Rewrite <- lt_plus_minus_r in H9; XEAuto.
  38 (* case 2.2: i = d0 *)
  39       Rewrite H5 in H; Rewrite H5 in H0; Clear H5 i.
  40       DropDis; Inversion H; Rewrite <- H7 in H0; Rewrite <- H7 in H1; Rewrite <- H7; Clear H H6 H7 e u.
  41       Subst1Confluence; Subst1Gen; Rewrite H0 in H; Clear H0 x; XEAuto.
  42 (* case 2.3: i > d0 *)
  43       Subst1Confluence; Subst1Gen; Rewrite H4 in H0; Clear H1 H4 x.
  44       CSubst1Drop; DropDis; XEAuto.
  45       Qed.
  46
  47    End pr2_gen_context.
  48
  49       Tactic Definition Pr2GenContext :=
  50          Match Context With
  51             | [ H0: (pr2 ?1 ?2 ?3); H1: (drop ?4 (0) ?1 (CTail ?5 (Bind Abbr) ?6));
  52                 H2: (csubst1 ?4 ?6 ?1 ?7); H3: (drop (1) ?4 ?7 ?8);
  53                 H4: (subst1 ?4 ?6 ?2 (lift (1) ?4 ?9)) |- ? ] ->
  54                LApply (pr2_gen_cabbr ?1 ?2 ?3); [ Clear H0; Intros H0 | XAuto ];
  55                LApply (H0 ?5 ?6 ?4); [ Clear H0; Intros H0 | XAuto ];
  56                LApply (H0 ?7); [ Clear H0; Intros H0 | XAuto ];
  57                LApply (H0 ?8); [ Clear H0; Intros H0 | XAuto ];
  58                LApply (H0 ?9); [ Clear H0 H4; Intros H0 | XAuto ];
  59                XElim H0; Intros.