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

   1 (*#* #stop file *)
   2
   3 Require lift_gen.
   4 Require pr3_props.
   5 Require pr3_gen.
   6 Require pc3_defs.
   7 Require pc3_props.
   8
   9    Section pc3_gen. (********************************************************)
  10
  11       Theorem pc3_gen_abst : (c:?; u1,u2,t1,t2:?)
  12                              (pc3 c (TTail (Bind Abst) u1 t1)
  13                                     (TTail (Bind Abst) u2 t2)
  14                              ) ->
  15                              (pc3 c u1 u2) /\
  16                              (b:?; u:?) (pc3 (CTail c (Bind b) u) t1 t2).
  17       Intros.
  18       Pc3Confluence; Pr3Gen; Pr3Gen; Rewrite H0 in H; Clear H0 x.
  19       Inversion H; Rewrite H5 in H1; Rewrite H6 in H2.
  20       Split; XEAuto.
  21       Qed.
  22
  23       Theorem pc3_gen_lift: (c:?; t1,t2:?; h,d:?)
  24                             (pc3 c (lift h d t1) (lift h d t2)) ->
  25                             (e:?) (drop h d c e) ->
  26                             (pc3 e t1 t2).
  27       Intros.
  28       Pc3Confluence; Pr3Gen; Pr3Gen; Rewrite H1 in H; Clear H1 x.
  29       LiftGen; Rewrite H in H2; XEAuto.
  30       Qed.
  31
  32       Theorem pc3_gen_not_abst : (b:?) ~b=Abst -> (c:?; t1,t2,u1,u2:?)
  33                                  (pc3 c (TTail (Bind b) u1 t1)
  34                                         (TTail (Bind Abst) u2 t2)
  35                                  ) ->
  36                                  (pc3 (CTail c (Bind b) u1) t1
  37                                       (lift (1) (0) (TTail (Bind Abst) u2 t2))
  38                                  )
  39              .
  40       Intros b; XElim b; Intros;
  41       Try EqFalse; Pc3Confluence; Pr3Gen; Pr3Gen;
  42       Try (Rewrite H1 in H0; Inversion H0);
  43       Rewrite H1 in H4; Pr3Context;
  44       EApply pc3_pr3_t; XEAuto.
  45       Qed.
  46
  47       Theorem pc3_gen_lift_abst : (c:?; t,t2,u2:?; h,d:?)
  48                                   (pc3 c (lift h d t)
  49                                          (TTail (Bind Abst) u2 t2)
  50                                   ) ->
  51                                   (e:?) (drop h d c e) ->
  52                                   (EX u1 t1 | (pr3 e t (TTail (Bind Abst) u1 t1)) &
  53                                               (pr3 c u2 (lift h d u1)) &
  54                                               (b:B; u:T)(pr3 (CTail c (Bind b) u) t2 (lift h (S d) t1))
  55                                   ).
  56       Intros.
  57       Pc3Confluence; Pr3Gen; Pr3Gen; Rewrite H1 in H; Clear H1 x.
  58       LiftGenBase; Rewrite H in H4; Rewrite H1 in H2; Rewrite H5 in H3; XEAuto.
  59       Qed.
  60
  61    End pc3_gen.
  62
  63       Tactic Definition Pc3Gen :=
  64          Match Context With
  65             | [ _: (pc3 ?1 (lift ?2 ?3 ?4) (lift ?2 ?3 ?5));
  66                 _: (drop ?2 ?3 ?1 ?6) |- ? ] ->
  67                LApply (pc3_gen_lift ?1 ?4 ?5 ?2 ?3); [ Intros H_x | XAuto ];
  68                LApply (H_x ?6); [ Clear H_x; Intros | XAuto ]
  69             | [ H: (pc3 ?1 (TTail (Bind Abst) ?2 ?3) (TTail (Bind Abst) ?4 ?5)) |- ? ] ->
  70                LApply (pc3_gen_abst ?1 ?2 ?4 ?3 ?5);[ Clear H; Intros H | XAuto ];
  71                XElim H; Intros
  72             | [ H: (pc3 ?1 (TTail (Bind ?2) ?3 ?4) (TTail (Bind Abst) ?5 ?6));
  73                 _: ~ ?2 = Abst |- ? ] ->
  74                LApply (pc3_gen_not_abst ?2); [ Intros H_x | XAuto ];
  75                LApply (H_x ?1 ?4 ?6 ?3 ?5); [ Clear H H_x; Intros | XAuto ]
  76             | [ _: (pc3 ?1 (lift ?2 ?3 ?4) (TTail (Bind Abst) ?5 ?6));
  77                 _: (drop ?2 ?3 ?1 ?7) |- ? ] ->
  78                LApply (pc3_gen_lift_abst ?1 ?4 ?6 ?5 ?2 ?3); [ Intros H_x | XAuto ];
  79                LApply (H_x ?7); [ Clear H_x; Intros H_x | XAuto ];
  80                XElim H_x; Intros.