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