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

   1 (*#* #stop file *)
   2
   3 Require Export pr0_defs.
   4
   5       Inductive pc0 [t1,t2:T] : Prop :=
   6          | pc0_r : (pr0 t1 t2) -> (pc0 t1 t2)
   7          | pc0_x : (pr0 t2 t1) -> (pc0 t1 t2).
   8
   9       Hint pc0 : ltlc := Constructors pc0.
  10
  11       Inductive pc1 : T -> T -> Prop :=
  12          | pc1_r : (t:?) (pc1 t t)
  13          | pc1_u : (t2,t1:?) (pc0 t1 t2) -> (t3:?) (pc1 t2 t3) -> (pc1 t1 t3).
  14
  15       Hint pc1 : ltlc := Constructors pc1.
  16
  17    Section pc0_props. (******************************************************)
  18
  19       Theorem pc0_s : (t2,t1:?) (pc0 t1 t2) -> (pc0 t2 t1).
  20       Intros.
  21       Inversion H; XAuto.
  22       Qed.
  23
  24    End pc0_props.
  25
  26       Hints Resolve pc0_s : ltlc.
  27
  28    Section pc1_props. (******************************************************)
  29
  30       Theorem pc1_pr0_r : (t1,t2:?) (pr0 t1 t2) -> (pc1 t1 t2).
  31       XEAuto.
  32       Qed.
  33
  34       Theorem pc1_pr0_x : (t1,t2:?) (pr0 t2 t1) -> (pc1 t1 t2).
  35       XEAuto.
  36       Qed.
  37
  38       Theorem pc1_pc0 : (t1,t2:?) (pc0 t1 t2) -> (pc1 t1 t2).
  39       XEAuto.
  40       Qed.
  41
  42       Theorem pc1_t : (t2,t1:?) (pc1 t1 t2) ->
  43                       (t3:?) (pc1 t2 t3) -> (pc1 t1 t3).
  44       Intros t2 t1 H; XElim H; XEAuto.
  45       Qed.
  46
  47       Hints Resolve pc1_t : ltlc.
  48
  49       Theorem pc1_s : (t2,t1:?) (pc1 t1 t2) -> (pc1 t2 t1).
  50       Intros; XElim H; XEAuto.
  51       Qed.
  52
  53       Theorem pc1_tail_1: (u1,u2:?) (pc1 u1 u2) ->
  54                           (t:?; k:?) (pc1 (TTail k u1 t) (TTail k u2 t)).
  55       Intros; XElim H; Intros.
  56 (* case 1: pc1_r *)
  57       XAuto.
  58 (* case 2: pc1_u *)
  59       XElim H; Intros; XEAuto.
  60       Qed.
  61
  62       Theorem pc1_tail_2: (t1,t2:?) (pc1 t1 t2) ->
  63                           (u:?; k:?) (pc1 (TTail k u t1) (TTail k u t2)).
  64       Intros; XElim H; Intros.
  65 (* case 1: pc1_r *)
  66       XAuto.
  67 (* case 2: pc1_u *)
  68       XElim H; Intros; XEAuto.
  69       Qed.
  70
  71       Theorem pc1_tail: (u1,u2:?) (pc1 u1 u2) -> (t1,t2:?) (pc1 t1 t2) ->
  72                         (k:?) (pc1 (TTail k u1 t1) (TTail k u2 t2)).
  73       Intros; EApply pc1_t; [ EApply pc1_tail_1 | EApply pc1_tail_2 ]; XAuto.
  74       Qed.
  75
  76    End pc1_props.
  77
  78       Hints Resolve pc1_pr0_r pc1_pr0_x pc1_pc0 pc1_t pc1_s
  79                     pc1_tail_1 pc1_tail_2 pc1_tail : ltlc.