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

   1 Require subst0_subst0.
   2 Require pr0_subst0.
   3 Require cpr0_defs.
   4 Require pr2_lift.
   5 Require pr2_gen.
   6 Require pr3_defs.
   7
   8 (*#* #caption "main properties of the relation $\\PrT{}{}{}$" *)
   9 (*#* #clauses *)
  10
  11 (*#* #stop file *)
  12
  13    Section pr3_context. (****************************************************)
  14
  15       Theorem pr3_pr0_pr2_t: (u1,u2:?) (pr0 u1 u2) ->
  16                              (c:?; t1,t2:?; k:?) (pr2 (CTail c k u2) t1 t2) ->
  17                              (pr3 (CTail c k u1) t1 t2).
  18       Intros; Inversion H0; Clear H0; XAuto.
  19       NewInduction i.
  20 (* case 1 : pr2_delta i = 0 *)
  21       DropGenBase; Inversion H0; Clear H0 H4 H5 H6 c k t.
  22       Rewrite H7 in H; Clear H7 u2.
  23       Pr0Subst0; XEAuto.
  24 (* case 2 : pr2_delta i > 0 *)
  25       NewInduction k; DropGenBase; XEAuto.
  26       Qed.
  27
  28       Theorem pr3_pr2_pr2_t: (c:?; u1,u2:?) (pr2 c u1 u2) ->
  29                              (t1,t2:?; k:?) (pr2 (CTail c k u2) t1 t2) ->
  30                              (pr3 (CTail c k u1) t1 t2).
  31       Intros until 1; Inversion H; Clear H; Intros.
  32 (* case 1 : pr2_free *)
  33       EApply pr3_pr0_pr2_t; [ Apply H0 | XAuto ].
  34 (* case 2 : pr2_delta *)
  35       Inversion H; [ XAuto | NewInduction i0 ].
  36 (* case 2.1 : i0 = 0 *)
  37       DropGenBase; Inversion H4; Clear H3 H4 H7 t t4.
  38       Rewrite <- H9; Rewrite H10 in H; Rewrite <- H11 in H6; Clear H9 H10 H11 d0 k u0.
  39       Subst0Subst0; Arith9'In H4 i; Clear H2 H H6 u2.
  40       Pr0Subst0; Apply pr3_sing with t2:=x0; XEAuto.
  41 (* case 2.2 : i0 > 0 *)
  42       Clear IHi0; NewInduction k; DropGenBase; XEAuto.
  43       Qed.
  44
  45       Theorem pr3_pr2_pr3_t: (c:?; u2,t1,t2:?; k:?)
  46                              (pr3 (CTail c k u2) t1 t2) ->
  47                              (u1:?) (pr2 c u1 u2) ->
  48                              (pr3 (CTail c k u1) t1 t2).
  49       Intros until 1; XElim H; Intros.
  50 (* case 1 : pr3_refl *)
  51       XAuto.
  52 (* case 2 : pr3_sing *)
  53       EApply pr3_t.
  54       EApply pr3_pr2_pr2_t; [ Apply H2 | Apply H ].
  55       XAuto.
  56       Qed.
  57
  58 (*#* #caption "reduction inside context items" *)
  59 (*#* #cap #cap t1, t2 #alpha c in E, u1 in V1, u2 in V2, k in z *)
  60
  61       Theorem pr3_pr3_pr3_t: (c:?; u1,u2:?) (pr3 c u1 u2) ->
  62                              (t1,t2:?; k:?) (pr3 (CTail c k u2) t1 t2) ->
  63                              (pr3 (CTail c k u1) t1 t2).
  64       Intros until 1; XElim H; Intros.
  65 (* case 1 : pr3_refl *)
  66       XAuto.
  67 (* case 2 : pr3_sing *)
  68       EApply pr3_pr2_pr3_t; [ Apply H1; XAuto | XAuto ].
  69       Qed.
  70
  71    End pr3_context.
  72
  73       Tactic Definition Pr3Context :=
  74          Match Context With
  75             | [ H1: (pr0 ?2 ?3); H2: (pr2 (CTail ?1 ?4 ?3) ?5 ?6) |- ? ] ->
  76                LApply (pr3_pr0_pr2_t ?2 ?3); [ Intros H_x | XAuto ];
  77                LApply (H_x ?1 ?5 ?6 ?4); [ Clear H_x H2; Intros | XAuto ]
  78             | [ H1: (pr0 ?2 ?3); H2: (pr3 (CTail ?1 ?4 ?3) ?5 ?6) |- ? ] ->
  79                LApply (pr3_pr2_pr3_t ?1 ?3 ?5 ?6 ?4); [ Clear H2; Intros H2 | XAuto ];
  80                LApply (H2 ?2); [ Clear H2; Intros | XAuto ]
  81             | [ H1: (pr2 ?1 ?2 ?3); H2: (pr2 (CTail ?1 ?4 ?3) ?5 ?6) |- ? ] ->
  82                LApply (pr3_pr2_pr2_t ?1 ?2 ?3); [ Intros H_x | XAuto ];
  83                LApply (H_x ?5 ?6 ?4); [ Clear H_x H2; Intros | XAuto ]
  84             | [ H1: (pr2 ?1 ?2 ?3); H2: (pr3 (CTail ?1 ?4 ?3) ?5 ?6) |- ? ] ->
  85                LApply (pr3_pr2_pr3_t ?1 ?3 ?5 ?6 ?4); [ Clear H2; Intros H2 | XAuto ];
  86                LApply (H2 ?2); [ Clear H2; Intros | XAuto ]
  87             | [ H1: (pr3 ?1 ?2 ?3); H2: (pr3 (CTail ?1 ?4 ?3) ?5 ?6) |- ? ] ->
  88                LApply (pr3_pr3_pr3_t ?1 ?2 ?3); [ Intros H_x | XAuto ];
  89                LApply (H_x ?5 ?6 ?4); [ Clear H_x H2; Intros | XAuto ].
  90
  91    Section pr3_lift. (*******************************************************)
  92
  93 (*#* #caption "conguence with lift" *)
  94 (*#* #cap #cap c, t1, t2 #alpha e in D, d in i *)
  95
  96       Theorem pr3_lift: (c,e:?; h,d:?) (drop h d c e) ->
  97                         (t1,t2:?) (pr3 e t1 t2) ->
  98                         (pr3 c (lift h d t1) (lift h d t2)).
  99       Intros until 2; XElim H0; Intros; XEAuto.
 100       Qed.
 101
 102    End pr3_lift.
 103
 104       Hints Resolve pr3_lift : ltlc.
 105
 106    Section pr3_cpr0. (*******************************************************)
 107
 108       Theorem pr3_cpr0_t: (c1,c2:?) (cpr0 c2 c1) -> (t1,t2:?) (pr3 c1 t1 t2) ->
 109                           (pr3 c2 t1 t2).
 110       Intros until 1; XElim H; Intros.
 111 (* case 1 : cpr0_refl *)
 112       XAuto.
 113 (* case 2 : cpr0_comp *)
 114       Pr3Context; Clear H1.
 115       XElim H2; Intros.
 116 (* case 2.1 : pr3_refl *)
 117       XAuto.
 118 (* case 2.2 : pr3_sing *)
 119       EApply pr3_t; [ Idtac | XEAuto ]. Clear H2 H3 c1 c2 t1 t2 t4 u2.
 120       Inversion_clear H1.
 121 (* case 2.2.1 : pr2_free *)
 122       XAuto.
 123 (* case 2.2.1 : pr2_delta *)
 124       Cpr0Drop; Pr0Subst0; Apply pr3_sing with t2:=x; XEAuto.
 125       Qed.
 126
 127    End pr3_cpr0.