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

   1 (*#* #stop file *)
   2
   3 Require Export drop_defs.
   4 Require Export pr0_defs.
   5
   6       Inductive pr2 [c:C; t1,t2:T] : Prop :=
   7 (* structural rules *)
   8          | pr2_pr0   : (pr0 t1 t2) -> (pr2 c t1 t2)
   9 (* axiom rules *)
  10          | pr2_delta : (d:?; u:?; i:?)
  11                        (drop i (0) c (CTail d (Bind Abbr) u)) ->
  12                        (subst0 i u t1 t2) -> (pr2 c t1 t2).
  13
  14       Hint pr2 : ltlc := Constructors pr2.
  15
  16    Section pr2_gen_base. (***************************************************)
  17
  18       Theorem pr2_gen_sort : (c:?; x:?; n:?) (pr2 c (TSort n) x) ->
  19                              x = (TSort n).
  20       Intros; Inversion H;
  21       Try Subst0GenBase; XEAuto.
  22       Qed.
  23
  24       Theorem pr2_gen_bref : (c:?; x:?; n:?) (pr2 c (TBRef n) x) ->
  25                              x = (TBRef n) \/
  26                              (EX d u | (drop n (0) c (CTail d (Bind Abbr) u)) &
  27                                         x = (lift (S n) (0) u)
  28                              ).
  29       Intros; Inversion H;
  30       Try Subst0GenBase; Try Rewrite <- H1 in H0; XEAuto.
  31       Qed.
  32
  33       Theorem pr2_gen_abst : (c:?; u1,t1,x:?)
  34                              (pr2 c (TTail (Bind Abst) u1 t1) x) ->
  35                              (EX u2 t2 | x = (TTail (Bind Abst) u2 t2) &
  36                                          (pr2 c u1 u2) & (b:?; u:?)
  37                                          (pr2 (CTail c (Bind b) u) t1 t2)
  38                              ).
  39       Intros; Inversion H;
  40       Try Pr0GenBase; Try Subst0GenBase; XDEAuto 6.
  41       Qed.
  42
  43       Theorem pr2_gen_appl : (c:?; u1,t1,x:?)
  44                              (pr2 c (TTail (Flat Appl) u1 t1) x) -> (OR
  45                              (EX u2 t2 | x = (TTail (Flat Appl) u2 t2) &
  46                                          (pr2 c u1 u2) & (pr2 c t1 t2)
  47                              ) |
  48                              (EX y1 z1 u2 t2 | t1 = (TTail (Bind Abst) y1 z1) &
  49                                                x = (TTail (Bind Abbr) u2 t2) &
  50                                                (pr0 u1 u2) & (pr0 z1 t2)
  51                              ) |
  52                              (EX b y1 z1 u2 v2 t2 |
  53                                 ~b=Abst &
  54                                 t1 = (TTail (Bind b) y1 z1) &
  55                                 x = (TTail (Bind b) v2 (TTail (Flat Appl) (lift (1) (0) u2) t2)) &
  56                                 (pr0 u1 u2) & (pr0 y1 v2) & (pr0 z1 t2))
  57                              ).
  58       Intros; Inversion H;
  59       Try Pr0GenBase; Try Subst0GenBase; XEAuto.
  60       Qed.
  61
  62       Theorem pr2_gen_cast : (c:?; u1,t1,x:?)
  63                              (pr2 c (TTail (Flat Cast) u1 t1) x) ->
  64                              (EX u2 t2 | x = (TTail (Flat Cast) u2 t2) &
  65                                          (pr2 c u1 u2) & (pr2 c t1 t2)
  66                              ) \/
  67                             (pr0 t1 x).
  68       Intros; Inversion H;
  69       Try Pr0GenBase; Try Subst0GenBase; XEAuto.
  70       Qed.
  71
  72    End pr2_gen_base.
  73
  74       Tactic Definition Pr2GenBase :=
  75          Match Context With
  76             | [ H: (pr2 ?1 (TTail (Bind Abst) ?2 ?3) ?4) |- ? ] ->
  77                LApply (pr2_gen_abst ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ];
  78                XElim H; Intros.
  79
  80    Section pr2_props. (******************************************************)
  81
  82       Theorem pr2_thin_dx : (c:?; t1,t2:?) (pr2 c t1 t2) ->
  83                             (u:?; f:?) (pr2 c (TTail (Flat f) u t1)
  84                                               (TTail (Flat f) u t2)).
  85       Intros; Inversion H; XEAuto.
  86       Qed.
  87
  88       Theorem pr2_tail_1 : (c:?; u1,u2:?) (pr2 c u1 u2) ->
  89                            (k:?; t:?) (pr2 c (TTail k u1 t) (TTail k u2 t)).
  90       Intros; Inversion H; XEAuto.
  91       Qed.
  92
  93       Theorem pr2_tail_2 : (c:?; u,t1,t2:?; k:?) (pr2 (CTail c k u) t1 t2) ->
  94                            (pr2 c (TTail k u t1) (TTail k u t2)).
  95       XElim k; Intros;
  96       (Inversion H; [ XAuto | Clear H ];
  97       (NewInduction i; DropGenBase; [ Inversion H; XEAuto | XEAuto ])).
  98       Qed.
  99
 100       Hints Resolve pr2_tail_2 : ltlc.
 101
 102       Theorem pr2_shift : (i:?; c,e:?) (drop i (0) c e) ->
 103                           (t1,t2:?) (pr2 c t1 t2) ->
 104                           (pr2 e (app c i t1) (app c i t2)).
 105       XElim i.
 106 (* case 1 : i = 0 *)
 107       Intros.
 108       DropGenBase; Rewrite H in H0.
 109       Repeat Rewrite app_O; XAuto.
 110 (* case 2 : i > 0 *)
 111       XElim c.
 112 (* case 2.1 : CSort *)
 113       Intros; DropGenBase; Rewrite H0; XAuto.
 114 (* case 2.2 : CTail *)
 115       XElim k; Intros; Simpl; DropGenBase; XAuto.
 116       Qed.
 117
 118    End pr2_props.
 119
 120       Hints Resolve pr2_thin_dx pr2_tail_1 pr2_tail_2 pr2_shift : ltlc.