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_sort: (c:?; m,n:?) (pc3 c (TSort m) (TSort n)) -> m = n.
  12       Intros; Pc3Unfold; Repeat Pr3GenBase.
  13       Rewrite H0 in H; Clear H0 x c.
  14       TGenBase; XAuto.
  15       Qed.
  16
  17       Theorem pc3_gen_abst: (c:?; u1,u2,t1,t2:?)
  18                             (pc3 c (TTail (Bind Abst) u1 t1)
  19                                    (TTail (Bind Abst) u2 t2)
  20                             ) ->
  21                             (pc3 c u1 u2) /\
  22                             (b:?; u:?) (pc3 (CTail c (Bind b) u) t1 t2).
  23       Intros.
  24       Pc3Unfold; Repeat Pr3GenBase; Rewrite H1 in H; Clear H1 x.
  25       TGenBase; Rewrite H1 in H4; Rewrite H6 in H5.
  26       XEAuto.
  27       Qed.
  28
  29       Theorem pc3_gen_lift: (c:?; t1,t2:?; h,d:?)
  30                             (pc3 c (lift h d t1) (lift h d t2)) ->
  31                             (e:?) (drop h d c e) ->
  32                             (pc3 e t1 t2).
  33       Intros.
  34       Pc3Unfold; Repeat Pr3Gen; Rewrite H2 in H; Clear H2 x.
  35       LiftGen; Rewrite H in H4; XEAuto.
  36       Qed.
  37
  38       Theorem pc3_gen_not_abst: (b:?) ~b=Abst -> (c:?; t1,t2,u1,u2:?)
  39                                 (pc3 c (TTail (Bind b) u1 t1)
  40                                        (TTail (Bind Abst) u2 t2)
  41                                 ) ->
  42                                 (pc3 (CTail c (Bind b) u1) t1
  43                                      (lift (1) (0) (TTail (Bind Abst) u2 t2))
  44                                 ).
  45       XElim b; Intros;
  46       Try EqFalse; Pc3Unfold; Repeat Pr3Gen;
  47       Try (Rewrite H0 in H3; TGenBase);
  48       Rewrite H1 in H0; Clear H H1 x;
  49       EApply pc3_pr3_t; XEAuto.
  50       Qed.
  51
  52       Theorem pc3_gen_lift_abst: (c:?; t,t2,u2:?; h,d:?)
  53                                  (pc3 c (lift h d t)
  54                                         (TTail (Bind Abst) u2 t2)
  55                                  ) ->
  56                                  (e:?) (drop h d c e) ->
  57                                  (EX u1 t1 | (pr3 e t (TTail (Bind Abst) u1 t1)) &
  58                                              (pr3 c u2 (lift h d u1)) &
  59                                              (b:B; u:T)(pr3 (CTail c (Bind b) u) t2 (lift h (S d) t1))
  60                                  ).
  61       Intros.
  62       Pc3Unfold; Repeat Pr3Gen; Rewrite H1 in H; Clear H1 x.
  63       LiftGenBase; Rewrite H in H3; Rewrite H1 in H4; Rewrite H2 in H5; XEAuto.
  64       Qed.
  65
  66    End pc3_gen.
  67
  68       Tactic Definition Pc3Gen :=
  69          Match Context With
  70             | [H: (pc3 ?1 (TSort ?2) (TSort ?3)) |- ? ] ->
  71                LApply (pc3_gen_sort ?1 ?2 ?3); [ Clear H; Intros | XAuto ]
  72             | [ _: (pc3 ?1 (lift ?2 ?3 ?4) (lift ?2 ?3 ?5));
  73                 _: (drop ?2 ?3 ?1 ?6) |- ? ] ->
  74                LApply (pc3_gen_lift ?1 ?4 ?5 ?2 ?3); [ Intros H_x | XAuto ];
  75                LApply (H_x ?6); [ Clear H_x; Intros | XAuto ]
  76             | [ H: (pc3 ?1 (TTail (Bind Abst) ?2 ?3) (TTail (Bind Abst) ?4 ?5)) |- ? ] ->
  77                LApply (pc3_gen_abst ?1 ?2 ?4 ?3 ?5);[ Clear H; Intros H | XAuto ];
  78                XElim H; Intros
  79             | [ H: (pc3 ?1 (TTail (Bind ?2) ?3 ?4) (TTail (Bind Abst) ?5 ?6));
  80                 _: ~ ?2 = Abst |- ? ] ->
  81                LApply (pc3_gen_not_abst ?2); [ Intros H_x | XAuto ];
  82                LApply (H_x ?1 ?4 ?6 ?3 ?5); [ Clear H H_x; Intros | XAuto ]
  83             | [ _: (pc3 ?1 (lift ?2 ?3 ?4) (TTail (Bind Abst) ?5 ?6));
  84                 _: (drop ?2 ?3 ?1 ?7) |- ? ] ->
  85                LApply (pc3_gen_lift_abst ?1 ?4 ?6 ?5 ?2 ?3); [ Intros H_x | XAuto ];
  86                LApply (H_x ?7); [ Clear H_x; Intros H_x | XAuto ];
  87                XElim H_x; Intros
  88             | _ -> Pr3Gen.