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

   1 (*#* #stop file *)
   2
   3 Require Export pr0_defs.
   4 Require Export pr1_defs.
   5
   6       Definition pc1 := [t1,t2:?] (EX t | (pr1 t1 t) & (pr1 t2 t)).
   7
   8       Hints Unfold pc1 : ltlc.
   9
  10       Tactic Definition Pc1Unfold :=
  11          Match Context With
  12             [ H: (pc1 ?2 ?3) |- ? ] -> Unfold pc1 in H; XDecompose H.
  13
  14    Section pc1_props. (******************************************************)
  15
  16       Theorem pc1_pr0_r: (t1,t2:?) (pr0 t1 t2) -> (pc1 t1 t2).
  17       XEAuto.
  18       Qed.
  19
  20       Theorem pc1_pr0_x: (t1,t2:?) (pr0 t2 t1) -> (pc1 t1 t2).
  21       XEAuto.
  22       Qed.
  23
  24       Theorem pc1_pr0_u: (t2,t1:?) (pr0 t1 t2) ->
  25                          (t3:?) (pc1 t2 t3) -> (pc1 t1 t3).
  26       Intros; Pc1Unfold; XEAuto.
  27       Qed.
  28
  29       Theorem pc1_refl: (t:?) (pc1 t t).
  30       XEAuto.
  31       Qed.
  32
  33       Theorem pc1_s: (t2,t1:?) (pc1 t1 t2) -> (pc1 t2 t1).
  34       Intros; Pc1Unfold; XEAuto.
  35       Qed.
  36
  37       Theorem pc1_tail_1: (u1,u2:?) (pc1 u1 u2) ->
  38                           (t:?; k:?) (pc1 (TTail k u1 t) (TTail k u2 t)).
  39       Intros; Pc1Unfold; XEAuto.
  40       Qed.
  41
  42       Theorem pc1_tail_2: (t1,t2:?) (pc1 t1 t2) ->
  43                           (u:?; k:?) (pc1 (TTail k u t1) (TTail k u t2)).
  44       Intros; Pc1Unfold; XEAuto.
  45       Qed.
  46
  47    End pc1_props.
  48
  49       Hints Resolve pc1_refl pc1_pr0_u pc1_pr0_r pc1_pr0_x pc1_s
  50                     pc1_tail_1 pc1_tail_2 : ltlc.