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 (*#* #stop file *)
   6
   7       Inductive pc2 [c:C; t1,t2:T] : Prop :=
   8          | pc2_r : (pr2 c t1 t2) -> (pc2 c t1 t2)
   9          | pc2_x : (pr2 c t2 t1) -> (pc2 c t1 t2).
  10
  11       Hint pc2 : ltlc := Constructors pc2.
  12
  13 (*#* #start file *)
  14
  15 (*#* #caption "axioms for the relation $\\PcT{}{}{}$",
  16    "reflexivity", "single step transitivity"
  17 *)
  18 (*#* #cap #cap c, t, t1, t2, t3 *)
  19
  20       Inductive pc3 [c:C] : T -> T -> Prop :=
  21          | pc3_r : (t:?) (pc3 c t t)
  22          | pc3_u : (t2,t1:?) (pc2 c t1 t2) ->
  23                    (t3:?) (pc3 c t2 t3) -> (pc3 c t1 t3).
  24
  25 (*#* #stop file *)
  26
  27       Hint pc3 : ltlc := Constructors pc3.
  28
  29    Section pc2_props. (******************************************************)
  30
  31       Theorem pc2_s : (c,t2,t1:?) (pc2 c t1 t2) -> (pc2 c t2 t1).
  32       Intros.
  33       Inversion H; XAuto.
  34       Qed.
  35
  36       Theorem pc2_shift : (h:?; c,e:?) (drop h (0) c e) ->
  37                           (t1,t2:?) (pc2 c t1 t2) ->
  38                           (pc2 e (app c h t1) (app c h t2)).
  39       Intros until 2; XElim H0; Intros.
  40 (* case 1 : pc2_r *)
  41       XAuto.
  42 (* case 2 : pc2_x *)
  43       XEAuto.
  44       Qed.
  45
  46    End pc2_props.
  47
  48       Hints Resolve pc2_s pc2_shift : ltlc.
  49
  50    Section pc3_props. (******************************************************)
  51
  52       Theorem pc3_pr2_r : (c,t1,t2:?) (pr2 c t1 t2) -> (pc3 c t1 t2).
  53       XEAuto.
  54       Qed.
  55
  56       Theorem pc3_pr2_x : (c,t1,t2:?) (pr2 c t2 t1) -> (pc3 c t1 t2).
  57       XEAuto.
  58       Qed.
  59
  60       Theorem pc3_pc2 : (c,t1,t2:?) (pc2 c t1 t2) -> (pc3 c t1 t2).
  61       XEAuto.
  62       Qed.
  63
  64       Theorem pc3_t : (t2,c,t1:?) (pc3 c t1 t2) ->
  65                       (t3:?) (pc3 c t2 t3) -> (pc3 c t1 t3).
  66       Intros t2 c t1 H; XElim H; XEAuto.
  67       Qed.
  68
  69       Hints Resolve pc3_t : ltlc.
  70
  71       Theorem pc3_s : (c,t2,t1:?) (pc3 c t1 t2) -> (pc3 c t2 t1).
  72       Intros; XElim H; [ XAuto | XEAuto ].
  73       Qed.
  74
  75       Hints Resolve pc3_s : ltlc.
  76
  77       Theorem pc3_pr3_r : (c:?; t1,t2) (pr3 c t1 t2) -> (pc3 c t1 t2).
  78       Intros; XElim H; XEAuto.
  79       Qed.
  80
  81       Theorem pc3_pr3_x : (c:?; t1,t2) (pr3 c t2 t1) -> (pc3 c t1 t2).
  82       Intros; XElim H; XEAuto.
  83       Qed.
  84
  85       Hints Resolve pc3_pr3_r pc3_pr3_x : ltlc.
  86
  87       Theorem pc3_pr3_t : (c:?; t1,t0:?) (pr3 c t1 t0) ->
  88                           (t2:?) (pr3 c t2 t0) -> (pc3 c t1 t2).
  89       Intros; Apply (pc3_t t0); XAuto.
  90       Qed.
  91
  92       Theorem pc3_thin_dx : (c:? ;t1,t2:?) (pc3 c t1 t2) ->
  93                             (u:?; f:?) (pc3 c (TTail (Flat f) u t1)
  94                                               (TTail (Flat f) u t2)).
  95       Intros; XElim H; [XAuto | Intros ].
  96       EApply pc3_u; [ Inversion H | Apply H1 ]; XAuto.
  97       Qed.
  98
  99       Theorem pc3_tail_1 : (c:?; u1,u2:?) (pc3 c u1 u2) ->
 100                            (k:?; t:?) (pc3 c (TTail k u1 t) (TTail k u2 t)).
 101       Intros until 1; XElim H; Intros.
 102 (* case 1 : pc3_r *)
 103       XAuto.
 104 (* case 2 : pc3_u *)
 105       EApply pc3_u; [ Inversion H | Apply H1 ]; XAuto.
 106       Qed.
 107
 108       Theorem pc3_tail_2 : (c:?; u,t1,t2:?; k:?) (pc3 (CTail c k u) t1 t2) ->
 109                            (pc3 c (TTail k u t1) (TTail k u t2)).
 110       Intros.
 111       XElim H; [ Idtac | Intros; Inversion H ]; XEAuto.
 112       Qed.
 113
 114       Theorem pc3_tail_12 : (c:?; u1,u2:?) (pc3 c u1 u2) ->
 115                             (k:?; t1,t2:?) (pc3 (CTail c k u2) t1 t2) ->
 116                             (pc3 c (TTail k u1 t1) (TTail k u2 t2)).
 117       Intros.
 118       EApply pc3_t; [ Apply pc3_tail_1 | Apply pc3_tail_2 ]; XAuto.
 119       Qed.
 120
 121       Theorem pc3_tail_21 : (c:?; u1,u2:?) (pc3 c u1 u2) ->
 122                             (k:?; t1,t2:?) (pc3 (CTail c k u1) t1 t2) ->
 123                             (pc3 c (TTail k u1 t1) (TTail k u2 t2)).
 124       Intros.
 125       EApply pc3_t; [ Apply pc3_tail_2 | Apply pc3_tail_1 ]; XAuto.
 126       Qed.
 127
 128       Theorem pc3_pr3_u : (c:?; t2,t1:?) (pr2 c t1 t2) ->
 129                           (t3:?) (pc3 c t2 t3) -> (pc3 c t1 t3).
 130       XEAuto.
 131       Qed.
 132
 133       Theorem pc3_pr3_u2 : (c:?; t0,t1:?) (pr2 c t0 t1) ->
 134                            (t2:?) (pc3 c t0 t2) -> (pc3 c t1 t2).
 135       Intros; Apply (pc3_t t0); XAuto.
 136       Qed.
 137
 138       Theorem pc3_shift : (h:?; c,e:?) (drop h (0) c e) ->
 139                           (t1,t2:?) (pc3 c t1 t2) ->
 140                           (pc3 e (app c h t1) (app c h t2)).
 141       Intros until 2; XElim H0; Clear t1 t2; Intros.
 142 (* case 1 : pc3_r *)
 143       XAuto.
 144 (* case 2 : pc3_u *)
 145       XEAuto.
 146       Qed.
 147
 148       Theorem pc3_pc1: (t1,t2:?) (pc1 t1 t2) -> (c:?) (pc3 c t1 t2).
 149       Intros; XElim H; Intros.
 150 (* case 1: pc1_r *)
 151       XAuto.
 152 (* case 2 : pc1_u *)
 153       XElim H; XEAuto.
 154       Qed.
 155
 156    End pc3_props.
 157
 158       Hints Resolve pc3_pr2_r pc3_pr2_x pc3_pc2 pc3_pr3_r pc3_pr3_x
 159                     pc3_t pc3_s pc3_pr3_t pc3_thin_dx pc3_tail_1 pc3_tail_2
 160                     pc3_tail_12 pc3_tail_21 pc3_pr3_u pc3_shift pc3_pc1 : ltlc.
 161
 162       Tactic Definition Pc3T :=
 163          Match Context With
 164             | [ _: (pr3 ?1 ?2 (TTail ?3 ?4 ?5)); _: (pc3 ?1 ?6 ?4) |- ? ] ->
 165                LApply (pc3_t (TTail ?3 ?4 ?5) ?1 ?2); [ Intros H_x | XAuto ];
 166                LApply (H_x (TTail ?3 ?6 ?5)); [ Clear H_x; Intros | Apply pc3_s; XAuto ]
 167             | [ _: (pc3 ?1 ?2 ?3); _: (pr3 ?1 ?3 ?4) |- ? ] ->
 168                LApply (pc3_t ?3 ?1 ?2); [ Intros H_x | XAuto ];
 169                LApply (H_x ?4); [ Clear H_x; Intros | XAuto ]
 170             | [ _: (pc3 ?1 ?2 ?3); _: (pc3 ?1 ?4 ?3) |- ? ] ->
 171                LApply (pc3_t ?3 ?1 ?2); [ Intros H_x | XAuto ];
 172                LApply (H_x ?4); [ Clear H_x; Intros | XAuto ].