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

   1 (*#* #stop file *)
   2
   3 Require pr0_subst0.
   4 Require pr3_defs.
   5 Require pr3_props.
   6 Require cpr0_defs.
   7
   8    Section cpr0_drop. (******************************************************)
   9
  10       Theorem cpr0_drop : (c1,c2:?) (cpr0 c1 c2) -> (h:?; e1:?; u1:?; k:?)
  11                           (drop h (0) c1 (CTail e1 k u1)) ->
  12                           (EX e2 u2 | (drop h (0) c2 (CTail e2 k u2)) &
  13                                       (cpr0 e1 e2) & (pr0 u1 u2)
  14                           ).
  15       Intros until 1; XElim H.
  16 (* case 1 : cpr0_refl *)
  17       XEAuto.
  18 (* case 2 : cpr0_cont *)
  19       XElim h.
  20 (* case 2.1 : h = 0 *)
  21       Intros; DropGenBase.
  22       Inversion H2; Rewrite H6 in H1; Rewrite H4 in H; XEAuto.
  23 (* case 2.2 : h > 0 *)
  24       XElim k; Intros; DropGenBase.
  25 (* case 2.2.1 : Bind *)
  26       LApply (H0 n e1 u0 k); [ Clear H0 H3; Intros H0 | XAuto ].
  27       XElim H0; XEAuto.
  28 (* case 2.2.2 : Flat *)
  29       LApply (H0 (S n) e1 u0 k); [ Clear H0 H3; Intros H0 | XAuto ].
  30       XElim H0; XEAuto.
  31       Qed.
  32
  33       Theorem cpr0_drop_back : (c1,c2:?) (cpr0 c2 c1) -> (h:?; e1:?; u1:?; k:?)
  34                                (drop h (0) c1 (CTail e1 k u1)) ->
  35                                (EX e2 u2 | (drop h (0) c2 (CTail e2 k u2)) &
  36                                            (cpr0 e2 e1) & (pr0 u2 u1)
  37                                ).
  38       Intros until 1; XElim H.
  39 (* case 1 : cpr0_refl *)
  40       XEAuto.
  41 (* case 2 : cpr0_cont *)
  42       XElim h.
  43 (* case 2.1 : h = 0 *)
  44       Intros; DropGenBase.
  45       Inversion H2; Rewrite H6 in H1; Rewrite H4 in H; XEAuto.
  46 (* case 2.2 : h > 0 *)
  47       XElim k; Intros; DropGenBase.
  48 (* case 2.2.1 : Bind *)
  49       LApply (H0 n e1 u0 k); [ Clear H0 H3; Intros H0 | XAuto ].
  50       XElim H0; XEAuto.
  51 (* case 2.2.2 : Flat *)
  52       LApply (H0 (S n) e1 u0 k); [ Clear H0 H3; Intros H0 | XAuto ].
  53       XElim H0; XEAuto.
  54       Qed.
  55
  56    End cpr0_drop.
  57
  58       Tactic Definition Cpr0Drop :=
  59          Match Context With
  60             | [ _: (drop ?1 (0) ?2 (CTail ?3 ?4 ?5));
  61                 _: (cpr0 ?2 ?6) |- ? ] ->
  62                LApply (cpr0_drop ?2 ?6); [ Intros H_x | XAuto ];
  63                LApply (H_x ?1 ?3 ?5 ?4); [ Clear H_x; Intros H_x | XAuto ];
  64                XElim H_x; Intros
  65             | [ _: (drop ?1 (0) ?2 (CTail ?3 ?4 ?5));
  66                 _: (cpr0 ?6 ?2) |- ? ] ->
  67                LApply (cpr0_drop_back ?2 ?6); [ Intros H_x | XAuto ];
  68                LApply (H_x ?1 ?3 ?5 ?4); [ Clear H_x; Intros H_x | XAuto ];
  69                XElim H_x; Intros
  70             | [ _: (drop ?1 (0) (CTail ?2 ?7 ?8) (CTail ?3 ?4 ?5));
  71                 _: (cpr0 ?2 ?6) |- ? ] ->
  72                LApply (cpr0_drop (CTail ?2 ?7 ?8) (CTail ?6 ?7 ?8)); [ Intros H_x | XAuto ];
  73                LApply (H_x ?1 ?3 ?5 ?4); [ Clear H_x; Intros H_x | XAuto ];
  74                XElim H_x; Intros
  75             | [ _: (drop ?1 (0) (CTail ?2 ?7 ?8) (CTail ?3 ?4 ?5));
  76                 _: (cpr0 ?6 ?2) |- ? ] ->
  77                LApply (cpr0_drop_back (CTail ?2 ?7 ?8) (CTail ?6 ?7 ?8)); [ Intros H_x | XAuto ];
  78                LApply (H_x ?1 ?3 ?5 ?4); [ Clear H_x; Intros H_x | XAuto ];
  79                XElim H_x; Intros.
  80
  81    Section cpr0_pr3. (*******************************************************)
  82
  83       Theorem cpr0_pr3_t : (c1,c2:?) (cpr0 c2 c1) -> (t1,t2:?) (pr3 c1 t1 t2) ->
  84                            (pr3 c2 t1 t2).
  85       Intros until 1; XElim H; Intros.
  86 (* case 1 : cpr0_refl *)
  87       XAuto.
  88 (* case 2 : cpr0_cont *)
  89       Pr3Context.
  90       XElim H1; Intros.
  91 (* case 2.1 : pr3_r *)
  92       XAuto.
  93 (* case 2.2 : pr3_u *)
  94       EApply pr3_t; [ Idtac | XEAuto ]. Clear H2 H3 c1 c2 t1 t2 t4 u2.
  95       Inversion_clear H1.
  96 (* case 2.2.1 : pr2_pr0 *)
  97       XAuto.
  98 (* case 2.2.1 : pr2_delta *)
  99       Cpr0Drop; Pr0Subst0.
 100       EApply pr3_u; [ EApply pr2_delta; XEAuto | XAuto ].
 101       Qed.
 102
 103    End cpr0_pr3.