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

   1 Require subst0_subst0.
   2 Require pr0_subst0.
   3 Require pr2_lift.
   4 Require pr3_defs.
   5
   6 (*#* #caption "main properties of predicate \\texttt{pr3}" *)
   7 (*#* #clauses *)
   8
   9 (*#* #stop file *)
  10
  11    Section pr3_context. (****************************************************)
  12
  13       Theorem pr3_pr0_pr2_t : (u1,u2:?) (pr0 u1 u2) ->
  14                               (c:?; t1,t2:?; k:?) (pr2 (CTail c k u2) t1 t2) ->
  15                               (pr3 (CTail c k u1) t1 t2).
  16       Intros.
  17       Inversion H0; Clear H0; XAuto.
  18       NewInduction i.
  19 (* case 1 : pr2_delta i = 0 *)
  20       DropGenBase; Inversion H0; Clear H0 H3 H4 c k.
  21       Rewrite H5 in H; Clear H5 u2.
  22       Pr0Subst0; XEAuto.
  23 (* case 2 : pr2_delta i > 0 *)
  24       NewInduction k; DropGenBase; XEAuto.
  25       Qed.
  26
  27       Theorem pr3_pr2_pr2_t : (c:?; u1,u2:?) (pr2 c u1 u2) ->
  28                               (t1,t2:?; k:?) (pr2 (CTail c k u2) t1 t2) ->
  29                               (pr3 (CTail c k u1) t1 t2).
  30       Intros until 1; Inversion H; Clear H; Intros.
  31 (* case 1 : pr2_pr0 *)
  32       EApply pr3_pr0_pr2_t; [ Apply H0 | XAuto ].
  33 (* case 2 : pr2_delta *)
  34       Inversion H; [ XAuto | NewInduction i0 ].
  35 (* case 2.1 : i0 = 0 *)
  36       DropGenBase; Inversion H2; Clear H2.
  37       Rewrite <- H5; Rewrite H6 in H; Rewrite <- H7 in H3; Clear H5 H6 H7 d0 k u0.
  38       Subst0Subst0; Arith9'In H4 i; XDEAuto 7.
  39 (* case 2.2 : i0 > 0 *)
  40       Clear IHi0; NewInduction k; DropGenBase; XEAuto.
  41       Qed.
  42
  43       Theorem pr3_pr2_pr3_t : (c:?; u2,t1,t2:?; k:?)
  44                               (pr3 (CTail c k u2) t1 t2) ->
  45                               (u1:?) (pr2 c u1 u2) ->
  46                               (pr3 (CTail c k u1) t1 t2).
  47       Intros until 1; XElim H; Intros.
  48 (* case 1 : pr3_r *)
  49       XAuto.
  50 (* case 2 : pr3_u *)
  51       EApply pr3_t.
  52       EApply pr3_pr2_pr2_t; [ Apply H2 | Apply H ].
  53       XAuto.
  54       Qed.
  55
  56 (*#* #start file *)
  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
  65 (*#* #stop file *)
  66
  67       Intros until 1; XElim H; Intros.
  68 (* case 1 : pr3_r *)
  69       XAuto.
  70 (* case 2 : pr3_u *)
  71       EApply pr3_pr2_pr3_t; [ Apply H1; XAuto | XAuto ].
  72       Qed.
  73
  74    End pr3_context.
  75
  76       Tactic Definition Pr3Context :=
  77          Match Context With
  78             | [ H1: (pr0 ?2 ?3); H2: (pr2 (CTail ?1 ?4 ?3) ?5 ?6) |- ? ] ->
  79                LApply (pr3_pr0_pr2_t ?2 ?3); [ Clear H1; Intros H1 | XAuto ];
  80                LApply (H1 ?1 ?5 ?6 ?4); [ Clear H1 H2; Intros | XAuto ]
  81             | [ H1: (pr0 ?2 ?3); H2: (pr3 (CTail ?1 ?4 ?3) ?5 ?6) |- ? ] ->
  82                LApply (pr3_pr2_pr3_t ?1 ?3 ?5 ?6 ?4); [ Clear H2; Intros H2 | XAuto ];
  83                LApply (H2 ?2); [ Clear H1 H2; Intros | XAuto ]
  84             | [ H1: (pr2 ?1 ?2 ?3); H2: (pr2 (CTail ?1 ?4 ?3) ?5 ?6) |- ? ] ->
  85                LApply (pr3_pr2_pr2_t ?1 ?2 ?3); [ Clear H1; Intros H1 | XAuto ];
  86                LApply (H1 ?5 ?6 ?4); [ Clear H1 H2; Intros | XAuto ]
  87             | [ H1: (pr2 ?1 ?2 ?3); H2: (pr3 (CTail ?1 ?4 ?3) ?5 ?6) |- ? ] ->
  88                LApply (pr3_pr2_pr3_t ?1 ?3 ?5 ?6 ?4); [ Clear H2; Intros H2 | XAuto ];
  89                LApply (H2 ?2); [ Clear H1 H2; Intros | XAuto ]
  90             | [ H1: (pr3 ?1 ?2 ?3); H2: (pr3 (CTail ?1 ?4 ?3) ?5 ?6) |- ? ] ->
  91                LApply (pr3_pr3_pr3_t ?1 ?2 ?3); [ Clear H1; Intros H1 | XAuto ];
  92                LApply (H1 ?5 ?6 ?4); [ Clear H1 H2; Intros | XAuto ].
  93
  94    Section pr3_lift. (*******************************************************)
  95
  96 (*#* #start file *)
  97
  98 (*#* #caption "conguence with lift" *)
  99 (*#* #cap #cap c, t1, t2 #alpha e in D, d in i *)
 100
 101       Theorem pr3_lift : (c,e:?; h,d:?) (drop h d c e) ->
 102                          (t1,t2:?) (pr3 e t1 t2) ->
 103                          (pr3 c (lift h d t1) (lift h d t2)).
 104
 105 (*#* #stop file *)
 106
 107       Intros until 2; XElim H0; Intros; XEAuto.
 108       Qed.
 109
 110    End pr3_lift.
 111
 112       Hints Resolve pr3_lift : ltlc.
 113