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

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