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