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

   1 (*#* #stop file *)
   2
   3 Require subst0_subst0.
   4 Require pr0_subst0.
   5 Require pr3_defs.
   6 Require pr3_props.
   7 Require pr3_confluence.
   8 Require cpr0_defs.
   9 Require cpr0_props.
  10 Require pc3_defs.
  11
  12    Section pc3_confluence. (*************************************************)
  13
  14       Theorem pc3_confluence : (c:?; t1,t2:?) (pc3 c t1 t2) ->
  15                                (EX t0 | (pr3 c t1 t0) & (pr3 c t2 t0)).
  16       Intros; XElim H; Intros.
  17 (* case 1 : pc3_r *)
  18       XEAuto.
  19 (* case 2 : pc3_u *)
  20       Clear H0; XElim H1; Intros.
  21       Inversion_clear H; [ XEAuto | Pr3Confluence; XEAuto ].
  22       Qed.
  23
  24    End pc3_confluence.
  25
  26       Tactic Definition Pc3Confluence :=
  27          Match Context With
  28             [ H: (pc3 ?1 ?2 ?3) |- ? ] ->
  29                LApply (pc3_confluence ?1 ?2 ?3); [ Clear H; Intros H | XAuto ];
  30                XElim H; Intros.
  31
  32    Section pc3_context. (****************************************************)
  33
  34       Theorem pc3_pr0_pr2_t : (u1,u2:?) (pr0 u2 u1) ->
  35                               (c:?; t1,t2:?; k:?) (pr2 (CTail c k u2) t1 t2) ->
  36                               (pc3 (CTail c k u1) t1 t2).
  37       Intros.
  38       Inversion H0; Clear H0; [ XAuto | NewInduction i ].
  39 (* case 1 : pr2_delta i = 0 *)
  40       DropGenBase; Inversion H0; Clear H0 H3 H4 c k.
  41       Rewrite H5 in H; Clear H5 u2.
  42       Pr0Subst0; XEAuto.
  43 (* case 2 : pr2_delta i > 0 *)
  44       NewInduction k; DropGenBase; XEAuto.
  45       Qed.
  46
  47       Theorem pc3_pr2_pr2_t : (c:?; u1,u2:?) (pr2 c u2 u1) ->
  48                               (t1,t2:?; k:?) (pr2 (CTail c k u2) t1 t2) ->
  49                               (pc3 (CTail c k u1) t1 t2).
  50       Intros until 1; Inversion H; Clear H; Intros.
  51 (* case 1 : pr2_pr0 *)
  52       EApply pc3_pr0_pr2_t; [ Apply H0 | XAuto ].
  53 (* case 2 : pr2_delta *)
  54       Inversion H; [ XAuto | NewInduction i0 ].
  55 (* case 2.1 : i0 = 0 *)
  56       DropGenBase; Inversion H2; Clear H2.
  57       Rewrite <- H5; Rewrite H6 in H; Rewrite <- H7 in H3; Clear H5 H6 H7 d0 k u0.
  58       Subst0Subst0; Arith9'In H4 i.
  59       EApply pc3_pr3_u.
  60       EApply pr2_delta; XEAuto.
  61       Apply pc3_pr2_x; EApply pr2_delta; [ Idtac | XEAuto ]; XEAuto.
  62 (* case 2.2 : i0 > 0 *)
  63       Clear IHi0; NewInduction k; DropGenBase; XEAuto.
  64       Qed.
  65
  66       Theorem pc3_pr2_pr3_t : (c:?; u2,t1,t2:?; k:?)
  67                               (pr3 (CTail c k u2) t1 t2) ->
  68                               (u1:?) (pr2 c u2 u1) ->
  69                               (pc3 (CTail c k u1) t1 t2).
  70       Intros until 1; XElim H; Intros.
  71 (* case 1 : pr3_r *)
  72       XAuto.
  73 (* case 2 : pr3_u *)
  74       EApply pc3_t.
  75       EApply pc3_pr2_pr2_t; [ Apply H2 | Apply H ].
  76       XAuto.
  77       Qed.
  78
  79       Theorem pc3_pr3_pc3_t : (c:?; u1,u2:?) (pr3 c u2 u1) ->
  80                               (t1,t2:?; k:?) (pc3 (CTail c k u2) t1 t2) ->
  81                               (pc3 (CTail c k u1) t1 t2).
  82       Intros until 1; XElim H; Intros.
  83 (* case 1 : pr3_r *)
  84       XAuto.
  85 (* case 2 : pr3_u *)
  86       Apply H1; Pc3Confluence.
  87       EApply pc3_t; [ Idtac | Apply pc3_s ]; EApply pc3_pr2_pr3_t; XEAuto.
  88       Qed.
  89
  90    End pc3_context.
  91
  92       Tactic Definition Pc3Context :=
  93          Match Context With
  94             | [ H1: (pr0 ?3 ?2); H2: (pr2 (CTail ?1 ?4 ?3) ?5 ?6) |- ? ] ->
  95                LApply (pc3_pr0_pr2_t ?2 ?3); [ Clear H1; Intros H1 | XAuto ];
  96                LApply (H1 ?1 ?5 ?6 ?4); [ Clear H1 H2; Intros | XAuto ]
  97             | [ H1: (pr0 ?3 ?2); H2: (pr3 (CTail ?1 ?4 ?3) ?5 ?6) |- ? ] ->
  98                LApply (pc3_pr2_pr3_t ?1 ?3 ?5 ?6 ?4); [ Clear H2; Intros H2 | XAuto ];
  99                LApply (H2 ?2); [ Clear H1 H2; Intros | XAuto ]
 100             | [ H1: (pr2 ?1 ?3 ?2); H2: (pr2 (CTail ?1 ?4 ?3) ?5 ?6) |- ? ] ->
 101                LApply (pc3_pr2_pr2_t ?1 ?2 ?3); [ Clear H1; Intros H1 | XAuto ];
 102                LApply (H1 ?5 ?6 ?4); [ Clear H1 H2; Intros | XAuto ]
 103             | [ H1: (pr2 ?1 ?3 ?2); H2: (pr3 (CTail ?1 ?4 ?3) ?5 ?6) |- ? ] ->
 104                LApply (pc3_pr2_pr3_t ?1 ?3 ?5 ?6 ?4); [ Clear H2; Intros H2 | XAuto ];
 105                LApply (H2 ?2); [ Clear H1 H2; Intros | XAuto ]
 106             | [ H1: (pr3 ?1 ?3 ?2); H2: (pc3 (CTail ?1 ?4 ?3) ?5 ?6) |- ? ] ->
 107                LApply (pc3_pr3_pc3_t ?1 ?2 ?3); [ Clear H1; Intros H1 | XAuto ];
 108                LApply (H1 ?5 ?6 ?4); [ Clear H1 H2; Intros | XAuto ]
 109             | _ -> Pr3Context.
 110
 111    Section pc3_lift. (*******************************************************)
 112
 113       Theorem pc3_lift : (c,e:?; h,d:?) (drop h d c e) ->
 114                          (t1,t2:?) (pc3 e t1 t2) ->
 115                          (pc3 c (lift h d t1) (lift h d t2)).
 116
 117       Intros.
 118       Pc3Confluence.
 119       EApply pc3_pr3_t; (EApply pr3_lift; [ XEAuto | Apply H0 Orelse Apply H1 ]).
 120       Qed.
 121
 122    End pc3_lift.
 123
 124       Hints Resolve pc3_lift : ltlc.
 125
 126    Section pc3_cpr0. (*******************************************************)
 127
 128       Remark pc3_cpr0_t_aux : (c1,c2:?) (cpr0 c1 c2) ->
 129                               (k:?; u,t1,t2:?) (pr3 (CTail c1 k u) t1 t2) ->
 130                               (pc3 (CTail c2 k u) t1 t2).
 131       Intros; XElim H0; Intros.
 132 (* case 1.1 : pr3_r *)
 133       XAuto.
 134 (* case 1.2 : pr3_u *)
 135       EApply pc3_t; [ Idtac | XEAuto ]. Clear H2 t1 t2.
 136       Inversion_clear H0.
 137 (* case 1.2.1 : pr2_pr0 *)
 138       XAuto.
 139 (* case 1.2.2 : pr2_delta *)
 140       Cpr0Drop; Pr0Subst0.
 141       EApply pc3_pr3_u; [ EApply pr2_delta; XEAuto | XAuto ].
 142       Qed.
 143
 144       Theorem pc3_cpr0_t : (c1,c2:?) (cpr0 c1 c2) ->
 145                            (t1,t2:?) (pr3 c1 t1 t2) ->
 146                            (pc3 c2 t1 t2).
 147       Intros until 1; XElim H; Intros.
 148 (* case 1 : cpr0_refl *)
 149       XAuto.
 150 (* case 2 : cpr0_cont *)
 151       Pc3Context; Pc3Confluence.
 152       EApply pc3_t; [ Idtac | Apply pc3_s ]; EApply pc3_cpr0_t_aux; XEAuto.
 153       Qed.
 154
 155       Theorem pc3_cpr0 : (c1,c2:?) (cpr0 c1 c2) -> (t1,t2:?) (pc3 c1 t1 t2) ->
 156                          (pc3 c2 t1 t2).
 157       Intros; Pc3Confluence.
 158       EApply pc3_t; [ Idtac | Apply pc3_s ]; EApply pc3_cpr0_t; XEAuto.
 159       Qed.
 160
 161    End pc3_cpr0.
 162
 163       Hints Resolve pc3_cpr0 : ltlc.