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

   1 (*#* #stop file *)
   2
   3 Require subst0_subst0.
   4 Require pr0_subst0.
   5 Require cpr0_defs.
   6 Require pr3_defs.
   7 Require pr3_props.
   8 Require pr3_confluence.
   9 Require pc3_defs.
  10
  11    Section pc3_trans. (******************************************************)
  12
  13       Theorem pc3_t: (t2,c,t1:?) (pc3 c t1 t2) ->
  14                      (t3:?) (pc3 c t2 t3) -> (pc3 c t1 t3).
  15       Intros; Repeat Pc3Unfold; Pr3Confluence; XEAuto.
  16       Qed.
  17
  18       Theorem pc3_pr2_u2: (c:?; t0,t1:?) (pr2 c t0 t1) ->
  19                           (t2:?) (pc3 c t0 t2) -> (pc3 c t1 t2).
  20       Intros; Apply (pc3_t t0); XAuto.
  21       Qed.
  22
  23       Theorem pc3_tail_12: (c:?; u1,u2:?) (pc3 c u1 u2) ->
  24                            (k:?; t1,t2:?) (pc3 (CTail c k u2) t1 t2) ->
  25                            (pc3 c (TTail k u1 t1) (TTail k u2 t2)).
  26       Intros.
  27       EApply pc3_t; [ Apply pc3_tail_1 | Apply pc3_tail_2 ]; XAuto.
  28       Qed.
  29
  30       Theorem pc3_tail_21: (c:?; u1,u2:?) (pc3 c u1 u2) ->
  31                            (k:?; t1,t2:?) (pc3 (CTail c k u1) t1 t2) ->
  32                            (pc3 c (TTail k u1 t1) (TTail k u2 t2)).
  33       Intros.
  34       EApply pc3_t; [ Apply pc3_tail_2 | Apply pc3_tail_1 ]; XAuto.
  35       Qed.
  36
  37    End pc3_trans.
  38
  39       Hints Resolve pc3_t pc3_tail_12 pc3_tail_21 : ltlc.
  40
  41       Tactic Definition Pc3T :=
  42          Match Context With
  43             | [ _: (pr3 ?1 ?2 (TTail ?3 ?4 ?5)); _: (pc3 ?1 ?6 ?4) |- ? ] ->
  44                LApply (pc3_t (TTail ?3 ?4 ?5) ?1 ?2); [ Intros H_x | XAuto ];
  45                LApply (H_x (TTail ?3 ?6 ?5)); [ Clear H_x; Intros | Apply pc3_s; XAuto ]
  46             | [ _: (pc3 ?1 ?2 ?3); _: (pr3 ?1 ?3 ?4) |- ? ] ->
  47                LApply (pc3_t ?3 ?1 ?2); [ Intros H_x | XAuto ];
  48                LApply (H_x ?4); [ Clear H_x; Intros | XAuto ]
  49             | [ _: (pc3 ?1 ?2 ?3); _: (pc3 ?1 ?4 ?3) |- ? ] ->
  50                LApply (pc3_t ?3 ?1 ?2); [ Intros H_x | XAuto ];
  51                LApply (H_x ?4); [ Clear H_x; Intros | XAuto ].
  52
  53    Section pc3_context. (****************************************************)
  54
  55       Theorem pc3_pr0_pr2_t: (u1,u2:?) (pr0 u2 u1) ->
  56                              (c:?; t1,t2:?; k:?) (pr2 (CTail c k u2) t1 t2) ->
  57                              (pc3 (CTail c k u1) t1 t2).
  58       Intros.
  59       Inversion H0; Clear H0; [ XAuto | NewInduction i ].
  60 (* case 1: pr2_delta i = 0 *)
  61       DropGenBase; Inversion H0; Clear H0 H4 H5 H6 c k t.
  62       Rewrite H7 in H; Clear H7 u2.
  63       Pr0Subst0; Apply pc3_pr3_t with t0:=x; XEAuto.
  64 (* case 2: pr2_delta i > 0 *)
  65       NewInduction k; DropGenBase; XEAuto.
  66       Qed.
  67
  68       Theorem pc3_pr2_pr2_t: (c:?; u1,u2:?) (pr2 c u2 u1) ->
  69                              (t1,t2:?; k:?) (pr2 (CTail c k u2) t1 t2) ->
  70                              (pc3 (CTail c k u1) t1 t2).
  71       Intros until 1; Inversion H; Clear H; Intros.
  72 (* case 1: pr2_free *)
  73       EApply pc3_pr0_pr2_t; [ Apply H0 | XAuto ].
  74 (* case 2: pr2_delta *)
  75       Inversion H; [ XAuto | NewInduction i0 ].
  76 (* case 2.1: i0 = 0 *)
  77       DropGenBase; Inversion H4; Clear H3 H4 H7 t t4.
  78       Rewrite <- H9; Rewrite H10 in H; Rewrite <- H11 in H6; Clear H9 H10 H11 d0 k u0.
  79       Pr0Subst0; Subst0Subst0; Arith9'In H6 i.
  80       EApply pc3_pr2_u.
  81       EApply pr2_delta; XEAuto.
  82       Apply pc3_pr2_x; EApply pr2_delta; [ Idtac | XEAuto | XEAuto ]; XEAuto.
  83 (* case 2.2: i0 > 0 *)
  84       Clear IHi0; NewInduction k; DropGenBase; XEAuto.
  85       Qed.
  86
  87       Theorem pc3_pr2_pr3_t: (c:?; u2,t1,t2:?; k:?)
  88                              (pr3 (CTail c k u2) t1 t2) ->
  89                              (u1:?) (pr2 c u2 u1) ->
  90                              (pc3 (CTail c k u1) t1 t2).
  91       Intros until 1; XElim H; Intros.
  92 (* case 1: pr3_refl *)
  93       XAuto.
  94 (* case 2: pr3_sing *)
  95       EApply pc3_t.
  96       EApply pc3_pr2_pr2_t; [ Apply H2 | Apply H ].
  97       XAuto.
  98       Qed.
  99
 100       Theorem pc3_pr3_pc3_t: (c:?; u1,u2:?) (pr3 c u2 u1) ->
 101                              (t1,t2:?; k:?) (pc3 (CTail c k u2) t1 t2) ->
 102                              (pc3 (CTail c k u1) t1 t2).
 103       Intros until 1; XElim H; Intros.
 104 (* case 1: pr3_refl *)
 105       XAuto.
 106 (* case 2: pr3_sing *)
 107       Apply H1; Pc3Unfold.
 108       EApply pc3_t; [ Idtac | Apply pc3_s ]; EApply pc3_pr2_pr3_t; XEAuto.
 109       Qed.
 110
 111    End pc3_context.
 112
 113       Tactic Definition Pc3Context :=
 114          Match Context With
 115             | [ H1: (pr0 ?3 ?2); H2: (pr2 (CTail ?1 ?4 ?3) ?5 ?6) |- ? ] ->
 116                LApply (pc3_pr0_pr2_t ?2 ?3); [ Clear H1; Intros H1 | XAuto ];
 117                LApply (H1 ?1 ?5 ?6 ?4); [ Clear H1 H2; Intros | XAuto ]
 118             | [ H1: (pr0 ?3 ?2); H2: (pr3 (CTail ?1 ?4 ?3) ?5 ?6) |- ? ] ->
 119                LApply (pc3_pr2_pr3_t ?1 ?3 ?5 ?6 ?4); [ Clear H2; Intros H2 | XAuto ];
 120                LApply (H2 ?2); [ Clear H1 H2; Intros | XAuto ]
 121             | [ H1: (pr2 ?1 ?3 ?2); H2: (pr2 (CTail ?1 ?4 ?3) ?5 ?6) |- ? ] ->
 122                LApply (pc3_pr2_pr2_t ?1 ?2 ?3); [ Clear H1; Intros H1 | XAuto ];
 123                LApply (H1 ?5 ?6 ?4); [ Clear H1 H2; Intros | XAuto ]
 124             | [ H1: (pr2 ?1 ?3 ?2); H2: (pr3 (CTail ?1 ?4 ?3) ?5 ?6) |- ? ] ->
 125                LApply (pc3_pr2_pr3_t ?1 ?3 ?5 ?6 ?4); [ Clear H2; Intros H2 | XAuto ];
 126                LApply (H2 ?2); [ Clear H1 H2; Intros | XAuto ]
 127             | [ H1: (pr3 ?1 ?3 ?2); H2: (pc3 (CTail ?1 ?4 ?3) ?5 ?6) |- ? ] ->
 128                LApply (pc3_pr3_pc3_t ?1 ?2 ?3); [ Clear H1; Intros H1 | XAuto ];
 129                LApply (H1 ?5 ?6 ?4); [ Clear H1 H2; Intros | XAuto ]
 130             | _ -> Pr3Context.
 131
 132    Section pc3_lift. (*******************************************************)
 133
 134       Theorem pc3_lift: (c,e:?; h,d:?) (drop h d c e) ->
 135                         (t1,t2:?) (pc3 e t1 t2) ->
 136                         (pc3 c (lift h d t1) (lift h d t2)).
 137
 138       Intros.
 139       Pc3Unfold.
 140       EApply pc3_pr3_t; (EApply pr3_lift; [ XEAuto | Apply H1 Orelse Apply H2 ]).
 141       Qed.
 142
 143    End pc3_lift.
 144
 145       Hints Resolve pc3_lift : ltlc.
 146
 147    Section pc3_cpr0. (*******************************************************)
 148
 149       Remark pc3_cpr0_t_aux: (c1,c2:?) (cpr0 c1 c2) ->
 150                              (k:?; u,t1,t2:?) (pr3 (CTail c1 k u) t1 t2) ->
 151                              (pc3 (CTail c2 k u) t1 t2).
 152       Intros; XElim H0; Intros.
 153 (* case 1.1: pr3_refl *)
 154       XAuto.
 155 (* case 1.2: pr3_sing *)
 156       EApply pc3_t; [ Idtac | XEAuto ]. Clear H2 t1 t2.
 157       Inversion_clear H0.
 158 (* case 1.2.1: pr2_free *)
 159       XAuto.
 160 (* case 1.2.2: pr2_delta *)
 161       Cpr0Drop; Pr0Subst0.
 162       EApply pc3_pr2_u; [ EApply pr2_delta; XEAuto | XAuto ].
 163       Qed.
 164
 165       Theorem pc3_cpr0_t: (c1,c2:?) (cpr0 c1 c2) ->
 166                           (t1,t2:?) (pr3 c1 t1 t2) ->
 167                           (pc3 c2 t1 t2).
 168       Intros until 1; XElim H; Intros.
 169 (* case 1: cpr0_refl *)
 170       XAuto.
 171 (* case 2: cpr0_comp *)
 172       Pc3Context; Pc3Unfold.
 173       EApply pc3_t; [ Idtac | Apply pc3_s ]; EApply pc3_cpr0_t_aux; XEAuto.
 174       Qed.
 175
 176       Theorem pc3_cpr0: (c1,c2:?) (cpr0 c1 c2) -> (t1,t2:?) (pc3 c1 t1 t2) ->
 177                         (pc3 c2 t1 t2).
 178       Intros; Pc3Unfold.
 179       EApply pc3_t; [ Idtac | Apply pc3_s ]; EApply pc3_cpr0_t; XEAuto.
 180       Qed.
 181
 182    End pc3_cpr0.
 183
 184       Hints Resolve pc3_cpr0 : ltlc.
 185
 186    Section pc3_ind_left. (***************************************************)
 187
 188       Inductive pc3_left [c:C] : T -> T -> Prop :=
 189          | pc3_left_r : (t:?) (pc3_left c t t)
 190          | pc3_left_ur: (t1,t2:?) (pr2 c t1 t2) -> (t3:?) (pc3_left c t2 t3) ->
 191                         (pc3_left c t1 t3)
 192          | pc3_left_ux: (t1,t2:?) (pr2 c t1 t2) -> (t3:?) (pc3_left c t1 t3) ->
 193                         (pc3_left c t2 t3).
 194
 195       Hint pc3_left: ltlc := Constructors pc3_left.
 196
 197       Remark pc3_left_pr3: (c:?; t1,t2:?) (pr3 c t1 t2) -> (pc3_left c t1 t2).
 198       Intros; XElim H; XEAuto.
 199       Qed.
 200
 201       Remark pc3_left_trans: (c:?; t1,t2:?) (pc3_left c t1 t2) ->
 202                              (t3:?) (pc3_left c t2 t3) -> (pc3_left c t1 t3).
 203       Intros until 1; XElim H; XEAuto.
 204       Qed.
 205
 206       Hints Resolve pc3_left_trans : ltlc.
 207
 208       Remark pc3_left_sym: (c:?; t1,t2:?) (pc3_left c t1 t2) ->
 209                            (pc3_left c t2 t1).
 210       Intros; XElim H; XEAuto.
 211       Qed.
 212
 213       Hints Resolve pc3_left_sym pc3_left_pr3 : ltlc.
 214
 215       Remark pc3_left_pc3: (c:?; t1,t2:?) (pc3 c t1 t2) -> (pc3_left c t1 t2).
 216       Intros; Pc3Unfold; XEAuto.
 217       Qed.
 218
 219       Remark pc3_pc3_left: (c:?; t1,t2:?) (pc3_left c t1 t2) -> (pc3 c t1 t2).
 220       Intros; XElim H; XEAuto.
 221       Qed.
 222
 223       Hints Resolve pc3_left_pc3 pc3_pc3_left : ltlc.
 224
 225       Theorem pc3_ind_left: (c:C; P:(T->T->Prop))
 226                             ((t:T) (P t t)) ->
 227                             ((t1,t2:T) (pr2 c t1 t2) -> (t3:T) (pc3 c t2 t3) -> (P t2 t3) -> (P t1 t3)) ->
 228                             ((t1,t2:T) (pr2 c t1 t2) -> (t3:T) (pc3 c t1 t3) -> (P t1 t3) -> (P t2 t3)) ->
 229                             (t,t0:T) (pc3 c t t0) -> (P t t0).
 230       Intros; ElimType (pc3_left c t t0); XEAuto.
 231       Qed.
 232
 233    End pc3_ind_left.