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

   1 (*#* #stop file *)
   2
   3 Require Export pr1_defs.
   4 Require Export pr2_defs.
   5
   6       Inductive pr3 [c:C] : T -> T -> Prop :=
   7          | pr3_r : (t:?) (pr3 c t t)
   8          | pr3_u : (t2,t1:?) (pr2 c t1 t2) ->
   9                    (t3:?) (pr3 c t2 t3) -> (pr3 c t1 t3).
  10
  11       Hint pr3: ltlc := Constructors pr3.
  12
  13    Section pr3_props. (******************************************************)
  14
  15       Theorem pr3_pr2 : (c,t1,t2:?) (pr2 c t1 t2) -> (pr3 c t1 t2).
  16       XEAuto.
  17       Qed.
  18
  19       Theorem pr3_t : (t2,t1,c:?) (pr3 c t1 t2) ->
  20                       (t3:?) (pr3 c t2 t3) -> (pr3 c t1 t3).
  21       Intros until 1; XElim H; XEAuto.
  22       Qed.
  23
  24       Theorem pr3_tail_1 : (c:?; u1,u2:?) (pr3 c u1 u2) ->
  25                            (k:?; t:?) (pr3 c (TTail k u1 t) (TTail k u2 t)).
  26       Intros until 1; XElim H; Intros.
  27 (* case 1 : pr3_r *)
  28       XAuto.
  29 (* case 2 : pr3_u *)
  30       EApply pr3_u; [ Apply pr2_tail_1; Apply H | XAuto ].
  31       Qed.
  32
  33       Theorem pr3_tail_2 : (c:?; u,t1,t2:?; k:?) (pr3 (CTail c k u) t1 t2) ->
  34                            (pr3 c (TTail k u t1) (TTail k u t2)).
  35       Intros until 1; XElim H; Intros.
  36 (* case 1 : pr3_r *)
  37       XAuto.
  38 (* case 2 : pr3_u *)
  39       EApply pr3_u; [ Apply pr2_tail_2; Apply H | XAuto ].
  40       Qed.
  41
  42       Hints Resolve pr3_tail_1 pr3_tail_2 : ltlc.
  43
  44       Theorem pr3_tail_21 : (c:?; u1,u2:?) (pr3 c u1 u2) ->
  45                             (k:?; t1,t2:?) (pr3 (CTail c k u1) t1 t2) ->
  46                             (pr3 c (TTail k u1 t1) (TTail k u2 t2)).
  47       Intros.
  48       EApply pr3_t; [ Apply pr3_tail_2 | Apply pr3_tail_1 ]; XAuto.
  49       Qed.
  50
  51       Theorem pr3_tail_12 : (c:?; u1,u2:?) (pr3 c u1 u2) ->
  52                             (k:?; t1,t2:?) (pr3 (CTail c k u2) t1 t2) ->
  53                             (pr3 c (TTail k u1 t1) (TTail k u2 t2)).
  54       Intros.
  55       EApply pr3_t; [ Apply pr3_tail_1 | Apply pr3_tail_2 ]; XAuto.
  56       Qed.
  57
  58       Theorem pr3_shift : (h:?; c,e:?) (drop h (0) c e) ->
  59                           (t1,t2:?) (pr3 c t1 t2) ->
  60                           (pr3 e (app c h t1) (app c h t2)).
  61       Intros until 2; XElim H0; Clear t1 t2; Intros.
  62 (* case 1 : pr3_r *)
  63       XAuto.
  64 (* case 2 : pr3_u *)
  65       XEAuto.
  66       Qed.
  67
  68       Theorem pr3_pr1: (t1,t2:?) (pr1 t1 t2) -> (c:?) (pr3 c t1 t2).
  69       Intros until 1; XElim H; XEAuto.
  70       Qed.
  71
  72    End pr3_props.
  73
  74       Hints Resolve pr3_pr2 pr3_t pr3_pr1
  75                     pr3_tail_12 pr3_tail_21 pr3_shift : ltlc.