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

   1 (*#* #stop file *)
   2
   3 Require subst0_gen.
   4 Require drop_props.
   5 Require pr0_gen.
   6 Require pr2_defs.
   7
   8    Section pr2_gen. (********************************************************)
   9
  10       Theorem pr2_gen_abbr : (c:?; u1,t1,x:?)
  11                              (pr2 c (TTail (Bind Abbr) u1 t1) x) ->
  12                              (EX u2 t2 | x = (TTail (Bind Abbr) u2 t2) &
  13                                          (pr2 c u1 u2) &
  14                                          ((b:?; u:?) (pr2 (CTail c (Bind b) u) t1 t2)) \/
  15                                          (EX y | (pr0 t1 y) & (subst0 (0) u2 y t2))
  16                              ) \/
  17                              (pr0 t1 (lift (1) (0) x)).
  18       Intros; Inversion H;
  19       Try Pr0Gen; Try Subst0Gen; XDEAuto 8.
  20       Qed.
  21
  22       Theorem pr2_gen_void : (c:?; u1,t1,x:?)
  23                              (pr2 c (TTail (Bind Void) u1 t1) x) ->
  24                              (EX u2 t2 | x = (TTail (Bind Void) u2 t2) &
  25                                          (pr2 c u1 u2) & (b:?; u:?)
  26                                          (pr2 (CTail c (Bind b) u) t1 t2)
  27                              ) \/
  28                              (pr0 t1 (lift (1) (0) x)).
  29       Intros; Inversion H;
  30       Try Pr0Gen; Try Subst0Gen; XDEAuto 7.
  31       Qed.
  32
  33 (*#* #start file *)
  34
  35 (*#* #caption "generation lemma for lift" *)
  36 (*#* #cap #cap c #alpha e in D, t1 in U1, t2 in U2, x in T, d in i *)
  37
  38       Theorem pr2_gen_lift : (c:?; t1,x:?; h,d:?) (pr2 c (lift h d t1) x) ->
  39                              (e:?) (drop h d c e) ->
  40                              (EX t2 | x = (lift h d t2) & (pr2 e t1 t2)).
  41
  42 (*#* #stop file *)
  43
  44       Intros.
  45       Inversion H; Clear H.
  46 (* case 1 : pr2_pr0 *)
  47       Pr0Gen; XEAuto.
  48 (* case 2 : pr2_delta *)
  49       Apply (lt_le_e i d); Intros.
  50 (* case 2.1 : i < d *)
  51       Rewrite (lt_plus_minus i d) in H0; [ Idtac | XAuto ].
  52       Rewrite (lt_plus_minus i d) in H2; [ Idtac | XAuto ].
  53       DropDis; Rewrite H0 in H2; Clear H0 u.
  54       Subst0Gen; Rewrite <- lt_plus_minus in H0; XEAuto.
  55 (* case 2.2 : i >= d *)
  56       Apply (lt_le_e i (plus d h)); Intros.
  57 (* case 2.2.1 : i < d + h *)
  58       EApply subst0_gen_lift_false; [ Apply H | Apply H3 | XEAuto ].
  59 (* case 2.2.2 : i >= d + h *)
  60       DropDis; Subst0Gen; XEAuto.
  61       Qed.
  62
  63    End pr2_gen.
  64
  65       Tactic Definition Pr2Gen :=
  66          Match Context With
  67             | [ H: (pr2 ?1 (TTail (Bind Abbr) ?2 ?3) ?4) |- ? ] ->
  68                LApply (pr2_gen_abbr ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ];
  69                XElim H;
  70                [ Intros H; XElim H; Do 4 Intro; Intros H_x; XElim H_x;
  71                  [ Intros | Intros H_x; XElim H_x; Intros ]
  72                | Intros ]
  73             | [ H: (pr2 ?1 (TTail (Bind Void) ?2 ?3) ?4) |- ? ] ->
  74                LApply (pr2_gen_void ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ];
  75                XElim H; [ Intros H; XElim H; Intros | Intros ]
  76             | [ H0: (pr2 ?1 (lift ?2 ?3 ?4) ?5);
  77                 H1: (drop ?2 ?3 ?1 ?6) |- ? ] ->
  78                LApply (pr2_gen_lift ?1 ?4 ?5 ?2 ?3); [ Clear H0; Intros H0 | XAuto ];
  79                LApply (H0 ?6); [ Clear H0; Intros H0 | XAuto ];
  80                XElim H0; Intros
  81             | _ -> Pr2GenBase.