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

   1 (*#* #stop file *)
   2
   3 Require lift_gen.
   4 Require lift_props.
   5 Require subst0_gen.
   6 Require pr0_defs.
   7 Require pr0_lift.
   8
   9    Section pr0_gen_abbr. (***************************************************)
  10
  11       Theorem pr0_gen_abbr : (u1,t1,x:?) (pr0 (TTail (Bind Abbr) u1 t1) x) ->
  12                              (EX u2 t2 | x = (TTail (Bind Abbr) u2 t2) &
  13                                          (pr0 u1 u2) &
  14                                          (pr0 t1 t2) \/
  15                                          (EX y | (pr0 t1 y) & (subst0 (0) u2 y t2))
  16                              ) \/
  17                              (pr0 t1 (lift (1) (0) x)).
  18       Intros.
  19       Inversion H; Clear H; XDEAuto 6.
  20       Qed.
  21
  22    End pr0_gen_abbr.
  23
  24    Section pr0_gen_void. (***************************************************)
  25
  26       Theorem pr0_gen_void : (u1,t1,x:?) (pr0 (TTail (Bind Void) u1 t1) x) ->
  27                              (EX u2 t2 | x = (TTail (Bind Void) u2 t2) &
  28                                          (pr0 u1 u2) & (pr0 t1 t2)
  29                              ) \/
  30                              (pr0 t1 (lift (1) (0) x)).
  31       Intros.
  32       Inversion H; Clear H; XEAuto.
  33       Qed.
  34
  35    End pr0_gen_void.
  36
  37    Section pr0_gen_lift. (***************************************************)
  38
  39       Tactic Definition IH :=
  40          Match Context With
  41             | [ H: (_:?; _:?) ?0 = (lift ? ? ?) -> ?;
  42                 H0: ?0 = (lift ? ?2 ?3) |- ? ] ->
  43                LApply (H ?3 ?2); [ Clear H H0; Intros H_x | XAuto ];
  44                XElim H_x; Intro; Intros H_x; Intro;
  45                Try Rewrite H_x; Try Rewrite H_x in H3; Clear H_x.
  46
  47 (*#* #caption "generation lemma for lift" *)
  48 (*#* #cap #alpha t1 in U1, t2 in U2, x in T, d in i *)
  49
  50       Theorem pr0_gen_lift : (t1,x:?; h,d:?) (pr0 (lift h d t1) x) ->
  51                              (EX t2 | x = (lift h d t2) & (pr0 t1 t2)).
  52       Intros until 1; InsertEq H '(lift h d t1);
  53       UnIntro H d; UnIntro H t1; XElim H; Clear y x; Intros;
  54       Rename x into t3; Rename x0 into d.
  55 (* case 1 : pr0_r *)
  56       XEAuto.
  57 (* case 2 : pr0_c *)
  58       NewInduction k; LiftGen; Rewrite H3; Clear H3 t0;
  59       IH; IH; XEAuto.
  60 (* case 3 : pr0_beta *)
  61       LiftGen; Rewrite H3; Clear H3 t0.
  62       LiftGen; Rewrite H3; Clear H3 H5 x1 k.
  63       IH; IH; XEAuto.
  64 (* case 4 : pr0_upsilon *)
  65       LiftGen; Rewrite H6; Clear H6 t0.
  66       LiftGen; Rewrite H6; Clear H6 x1.
  67       IH; IH; IH.
  68       Rewrite <- lift_d; [ Simpl | XAuto ].
  69       Rewrite <- lift_flat; XEAuto.
  70 (* case 5 : pr0_delta *)
  71       LiftGen; Rewrite H4; Clear H4 t0.
  72       IH; IH; Arith3In H3 d; Subst0Gen.
  73       Rewrite H3; XEAuto.
  74 (* case 6 : pr0_zeta *)
  75       LiftGen; Rewrite H2; Clear H2 t0.
  76       Arith7In H4 d; LiftGen; Rewrite H2; Clear H2 x1.
  77       IH; XEAuto.
  78 (* case 7 : pr0_zeta *)
  79       LiftGen; Rewrite H1; Clear H1 t0.
  80       IH; XEAuto.
  81       Qed.
  82
  83    End pr0_gen_lift.
  84
  85       Tactic Definition Pr0Gen :=
  86          Match Context With
  87             | [ H: (pr0 (TTail (Bind Abbr) ?1 ?2) ?3) |- ? ] ->
  88                LApply (pr0_gen_abbr ?1 ?2 ?3); [ Clear H; Intros H | XAuto ];
  89                XElim H;
  90                [ Intros H; XElim H; Do 4 Intro; Intros H_x;
  91                  XElim H_x; [ Intros | Intros H_x; XElim H_x; Intros ]
  92                | Intros ]
  93             | [ H: (pr0 (TTail (Bind Void) ?1 ?2) ?3) |- ? ] ->
  94                LApply (pr0_gen_void ?1 ?2 ?3); [ Clear H; Intros H | XAuto ];
  95                XElim H; [ Intros H; XElim H; Intros | Intros ]
  96             | [ H: (pr0 (lift ?0 ?1 ?2) ?3) |- ? ] ->
  97                LApply (pr0_gen_lift ?2 ?3 ?0 ?1); [ Clear H; Intros H | XAuto ];
  98                XElim H; Intros
  99             | _ -> Pr0GenBase.