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

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