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

   1 Require Export pr2_defs.
   2 Require Export pr3_defs.
   3 Require Export pc1_defs.
   4
   5 (*#* #caption "the relation $\\PcT{}{}{}$" *)
   6 (*#* #cap #cap c, t, t1, t2 *)
   7
   8       Definition pc3 := [c:?; t1,t2:?] (EX t | (pr3 c t1 t) & (pr3 c t2 t)).
   9
  10 (*#* #stop file *)
  11
  12       Hints Unfold pc3 : ltlc.
  13
  14       Tactic Definition Pc3Unfold :=
  15          Match Context With
  16             [ H: (pc3 ?1 ?2 ?3) |- ? ] -> Unfold pc3 in H; XDecompose H.
  17
  18    Section pc3_props. (******************************************************)
  19
  20       Theorem pc3_pr2_r: (c,t1,t2:?) (pr2 c t1 t2) -> (pc3 c t1 t2).
  21       XEAuto.
  22       Qed.
  23
  24       Theorem pc3_pr2_x: (c,t1,t2:?) (pr2 c t2 t1) -> (pc3 c t1 t2).
  25       XEAuto.
  26       Qed.
  27
  28       Theorem pc3_pr3_r: (c:?; t1,t2) (pr3 c t1 t2) -> (pc3 c t1 t2).
  29       XEAuto.
  30       Qed.
  31
  32       Theorem pc3_pr3_x: (c:?; t1,t2) (pr3 c t2 t1) -> (pc3 c t1 t2).
  33       XEAuto.
  34       Qed.
  35
  36       Theorem pc3_pr3_t: (c:?; t1,t0:?) (pr3 c t1 t0) ->
  37                          (t2:?) (pr3 c t2 t0) -> (pc3 c t1 t2).
  38       XEAuto.
  39       Qed.
  40
  41       Theorem pc3_pr2_u: (c:?; t2,t1:?) (pr2 c t1 t2) ->
  42                          (t3:?) (pc3 c t2 t3) -> (pc3 c t1 t3).
  43       Intros; Pc3Unfold; XEAuto.
  44       Qed.
  45
  46       Theorem pc3_refl: (c:?; t:?) (pc3 c t t).
  47       XEAuto.
  48       Qed.
  49
  50       Theorem pc3_s: (c,t2,t1:?) (pc3 c t1 t2) -> (pc3 c t2 t1).
  51       Intros; Pc3Unfold; XEAuto.
  52       Qed.
  53
  54       Theorem pc3_thin_dx: (c:? ;t1,t2:?) (pc3 c t1 t2) ->
  55                            (u:?; f:?) (pc3 c (TTail (Flat f) u t1)
  56                                              (TTail (Flat f) u t2)).
  57       Intros; Pc3Unfold; XEAuto.
  58       Qed.
  59
  60       Theorem pc3_tail_1: (c:?; u1,u2:?) (pc3 c u1 u2) ->
  61                           (k:?; t:?) (pc3 c (TTail k u1 t) (TTail k u2 t)).
  62       Intros; Pc3Unfold; XEAuto.
  63       Qed.
  64
  65       Theorem pc3_tail_2: (c:?; u,t1,t2:?; k:?) (pc3 (CTail c k u) t1 t2) ->
  66                           (pc3 c (TTail k u t1) (TTail k u t2)).
  67       Intros; Pc3Unfold; XEAuto.
  68       Qed.
  69
  70       Theorem pc3_shift: (h:?; c,e:?) (drop h (0) c e) ->
  71                          (t1,t2:?) (pc3 c t1 t2) ->
  72                          (pc3 e (app c h t1) (app c h t2)).
  73       Intros; Pc3Unfold; XEAuto.
  74       Qed.
  75
  76       Theorem pc3_pc1: (t1,t2:?) (pc1 t1 t2) -> (c:?) (pc3 c t1 t2).
  77       Intros; Pc1Unfold; XEAuto.
  78       Qed.
  79
  80    End pc3_props.
  81
  82       Hints Resolve pc3_refl pc3_pr2_r pc3_pr2_x pc3_pr3_r pc3_pr3_x
  83                     pc3_s pc3_pr3_t pc3_thin_dx pc3_tail_1 pc3_tail_2
  84                     pc3_pr2_u pc3_shift pc3_pc1 : ltlc.