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

   1 (*#* #stop file *)
   2
   3 Require csubst1_defs.
   4 Require pr2_gen_context.
   5 Require pr3_defs.
   6
   7    Section pr3_gen_context. (************************************************)
   8
   9       Theorem pr3_gen_cabbr: (c:?; t1,t2:?) (pr3 c t1 t2) -> (e:?; u:?; d:?)
  10                              (drop d (0) c (CTail e (Bind Abbr) u)) ->
  11                              (a0:?) (csubst1 d u c a0) ->
  12                              (a:?) (drop (1) d a0 a) ->
  13                              (x1:?) (subst1 d u t1 (lift (1) d x1)) ->
  14                              (EX x2 | (subst1 d u t2 (lift (1) d x2)) &
  15                                       (pr3 a x1 x2)
  16                              ).
  17       Intros until 1; XElim H; Intros.
  18 (* case 1: pr3_refl *)
  19       XEAuto.
  20 (* case 1: pr3_refl *)
  21       Pr2GenContext.
  22       LApply (H1 e u d); [ Clear H1; Intros H1 | XAuto ].
  23       LApply (H1 a0); [ Clear H1; Intros H1 | XAuto ].
  24       LApply (H1 a); [ Clear H1; Intros H1 | XAuto ].
  25       LApply (H1 x); [ Clear H1; Intros H1 | XAuto ].
  26       XElim H1; XEAuto.
  27       Qed.
  28
  29    End pr3_gen_context.
  30
  31       Tactic Definition Pr3GenContext :=
  32          Match Context With
  33             | [ H0: (pr3 ?1 ?2 ?3); H1: (drop ?4 (0) ?1 (CTail ?5 (Bind Abbr) ?6));
  34                 H2: (csubst1 ?4 ?6 ?1 ?7); H3: (drop (1) ?4 ?7 ?8);
  35                 H4: (subst1 ?4 ?6 ?2 (lift (1) ?4 ?9)) |- ? ] ->
  36                LApply (pr3_gen_cabbr ?1 ?2 ?3); [ Clear H0; Intros H0 | XAuto ];
  37                LApply (H0 ?5 ?6 ?4); [ Clear H0; Intros H0 | XAuto ];
  38                LApply (H0 ?7); [ Clear H0; Intros H0 | XAuto ];
  39                LApply (H0 ?8); [ Clear H0; Intros H0 | XAuto ];
  40                LApply (H0 ?9); [ Clear H0 H4; Intros H0 | XAuto ];
  41                XElim H0; Intros
  42             | _ -> Pr2GenContext.