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

   1 (*#* #stop file *)
   2
   3 Require subst0_subst0.
   4 Require fsubst0_defs.
   5 Require pr0_subst0.
   6 Require pc3_defs.
   7
   8    Section pc3_fsubst0. (****************************************************)
   9
  10       Theorem pc3_pr2_fsubst0: (c1:?; t1,t:?) (pr2 c1 t1 t) ->
  11                                (i:?; u,c2,t2:?) (fsubst0 i u c1 t1 c2 t2) ->
  12                                (e:?) (drop i (0) c1 (CTail e (Bind Abbr) u)) ->
  13                                (pc3 c2 t2 t).
  14       Intros until 1; XElim H.
  15 (* case 1: pr2_free *)
  16       Intros until 2; XElim H0; Intros.
  17 (* case 1.1: fsubst0_snd *)
  18       Pr0Subst0; [ XAuto | Apply (pc3_pr3_u c1 x); XEAuto ].
  19 (* case 1.2: fsubst0_fst *)
  20       XAuto.
  21 (* case 1.3: fsubst0_both *)
  22       Pr0Subst0; CSubst0Drop; [ XAuto | Apply (pc3_pr3_u c0 x); XEAuto ].
  23 (* case 2 : pr2_delta *)
  24       Intros until 4; XElim H2; Intros.
  25 (* case 2.1: fsubst0_snd. *)
  26       Apply (pc3_t t1); [ Apply pc3_s; XEAuto | XEAuto ].
  27 (* case 2.2: fsubst0_fst. *)
  28       Apply (lt_le_e i i0); Intros; CSubst0Drop.
  29 (* case 2.2.1: i < i0, none *)
  30       XEAuto.
  31 (* case 2.2.2: i < i0, csubst0_snd *)
  32       CGenBase; Rewrite <- H8 in H5; Rewrite <- H9 in H5; Rewrite <- H9 in H6; Rewrite <- H10 in H6; Clear H8 H9 H10 c2 t3 x0 x1 x2.
  33       Subst0Subst0; Rewrite <- lt_plus_minus_r in H7; [ CSubst0Drop | XAuto ].
  34       Apply (pc3_pr3_u c0 x); XEAuto.
  35 (* case 2.2.3: i < i0, csubst0_fst *)
  36       CGenBase; Rewrite <- H8 in H6; Rewrite <- H9 in H5; Rewrite <- H9 in H6; Rewrite <- H10 in H5; Clear H8 H9 H10 c2 t3 x0 x1 x3.
  37       Apply pc3_pr2_r; XEAuto.
  38 (* case 2.2.4: i < i0, csubst0_both *)
  39       CGenBase; Rewrite <- H9 in H7; Rewrite <- H10 in H5; Rewrite <- H10 in H6; Rewrite <- H10 in H7; Rewrite <- H11 in H6; Clear H9 H10 H11 c2 t3 x0 x1 x3.
  40       Subst0Subst0; Rewrite <- lt_plus_minus_r in H8; [ CSubst0Drop | XAuto ].
  41       Apply (pc3_pr3_u c0 x); XEAuto.
  42 (* case 2.2.5: i >= i0 *)
  43       XEAuto.
  44 (* case 2.3: fsubst0_both *)
  45       Apply (lt_le_e i i0); Intros; CSubst0Drop.
  46 (* case 2.3.1 : i < i0, none *)
  47       CSubst0Drop; Apply pc3_pr3_u2 with t0 := t1; XEAuto.
  48 (* case 2.3.2 : i < i0, csubst0_snd *)
  49       CGenBase; Rewrite <- H9 in H6; Rewrite <- H10 in H6; Rewrite <- H10 in H7; Rewrite <- H11 in H7; Clear H9 H10 H11 c2 t3 x0 x1 x2.
  50       Subst0Subst0; Rewrite <- lt_plus_minus_r in H8; [ CSubst0Drop | XAuto ].
  51       Apply (pc3_pr3_u2 c0 t1); [ Idtac | Apply (pc3_pr3_u c0 x) ]; XEAuto.
  52 (* case 2.3.3: i < i0, csubst0_fst *)
  53       CGenBase; Rewrite <- H9 in H7; Rewrite <- H10 in H6; Rewrite <- H10 in H7; Rewrite <- H11 in H6; Clear H9 H10 H11 c2 t3 x0 x1 x3.
  54       CSubst0Drop; Apply (pc3_pr3_u2 c0 t1); [ Idtac | Apply pc3_pr2_r ]; XEAuto.
  55 (* case 2.3.4: i < i0, csubst0_both *)
  56       CGenBase; Rewrite <- H10 in H8; Rewrite <- H11 in H6; Rewrite <- H11 in H7; Rewrite <- H11 in H8; Rewrite <- H12 in H7; Clear H10 H11 H12 c2 t3 x0 x1 x3.
  57       Subst0Subst0; Rewrite <- lt_plus_minus_r in H9; [ CSubst0Drop | XAuto ].
  58       Apply (pc3_pr3_u2 c0 t1); [ Idtac | Apply (pc3_pr3_u c0 x) ]; XEAuto.
  59 (* case 2.3.5: i >= i0 *)
  60       CSubst0Drop; Apply (pc3_pr3_u2 c0 t1); XEAuto.
  61       Qed.
  62
  63       Theorem pc3_pr2_fsubst0_back: (c1:?; t,t1:?) (pr2 c1 t t1) ->
  64                                     (i:?; u,c2,t2:?) (fsubst0 i u c1 t1 c2 t2) ->
  65                                     (e:?) (drop i (0) c1 (CTail e (Bind Abbr) u)) ->
  66                                     (pc3 c2 t t2).
  67       Intros until 1; XElim H.
  68 (* case 1: pr2_free *)
  69       Intros until 2; XElim H0; Intros.
  70 (* case 1.1: fsubst0_snd. *)
  71       Apply (pc3_pr3_u c1 t2); XEAuto.
  72 (* case 1.2: fsubst0_fst. *)
  73       XAuto.
  74 (* case 1.3: fsubst0_both. *)
  75       CSubst0Drop; Apply (pc3_pr3_u c0 t2); XEAuto.
  76 (* case 2: pr2_delta *)
  77       Intros until 4; XElim H2; Intros.
  78 (* case 2.1: fsubst0_snd. *)
  79       Apply (pc3_t t2); Apply pc3_pr3_r; XEAuto.
  80 (* case 2.2: fsubst0_fst. *)
  81       Apply (lt_le_e i i0); Intros; CSubst0Drop.
  82 (* case 2.2.1: i < i0, none *)
  83       XEAuto.
  84 (* case 2.2.2: i < i0, csubst0_bind *)
  85       CGenBase; Rewrite <- H8 in H5; Rewrite <- H9 in H5; Rewrite <- H9 in H6; Rewrite <- H10 in H6; Clear H8 H9 H10 c2 t3 x0 x1 x2.
  86       Subst0Subst0; Rewrite <- lt_plus_minus_r in H7; [ CSubst0Drop | XAuto ].
  87       Apply (pc3_pr3_u c0 x); XEAuto.
  88 (* case 2.2.3: i < i0, csubst0_fst *)
  89       CGenBase; Rewrite <- H8 in H6; Rewrite <- H9 in H5; Rewrite <- H9 in H6; Rewrite <- H10 in H5; Clear H8 H9 H10 c2 t3 x0 x1 x3.
  90       Apply pc3_pr2_r; XEAuto.
  91 (* case 2.2.4: i < i0, csubst0_both *)
  92       CGenBase; Rewrite <- H9 in H7; Rewrite <- H10 in H5; Rewrite <- H10 in H6; Rewrite <- H10 in H7; Rewrite <- H11 in H6; Clear H9 H10 H11 c2 t3 x0 x1 x3.
  93       Subst0Subst0; Rewrite <- lt_plus_minus_r in H8; [ CSubst0Drop | XAuto ].
  94       Apply (pc3_pr3_u c0 x); XEAuto.
  95 (* case 2.2.5: i >= i0 *)
  96       XEAuto.
  97 (* case 2.3: fsubst0_both *)
  98       Apply (lt_le_e i i0); Intros; CSubst0Drop.
  99 (* case 2.3.1 : i < i0, none *)
 100       CSubst0Drop; Apply pc3_pr3_u with t2:=t2; Try Apply pc3_pr3_r; XEAuto.
 101 (* case 2.3.2 : i < i0, csubst0_snd *)
 102       CGenBase; Rewrite <- H9 in H6; Rewrite <- H10 in H6; Rewrite <- H10 in H7; Rewrite <- H11 in H7; Clear H9 H10 H11 c2 t3 x0 x1 x2.
 103       Subst0Subst0; Rewrite <- lt_plus_minus_r in H8; [ CSubst0Drop | XAuto ].
 104       Apply (pc3_pr3_u c0 x); [ Idtac | Apply (pc3_pr3_u2 c0 t0) ]; XEAuto.
 105 (* case 2.3.3: i < i0, csubst0_fst *)
 106       CGenBase; Rewrite <- H9 in H7; Rewrite <- H10 in H6; Rewrite <- H10 in H7; Rewrite <- H11 in H6; Clear H9 H10 H11 c2 t3 x0 x1 x3.
 107       CSubst0Drop; Apply (pc3_pr3_u c0 t0); [ Idtac | Apply pc3_pr2_r ]; XEAuto.
 108 (* case 2.3.4: i < i0, csubst0_both *)
 109       CGenBase; Rewrite <- H10 in H8; Rewrite <- H11 in H6; Rewrite <- H11 in H7; Rewrite <- H11 in H8; Rewrite <- H12 in H7; Clear H10 H11 H12 c2 t3 x0 x1 x3.
 110       Subst0Subst0; Rewrite <- lt_plus_minus_r in H9; [ CSubst0Drop | XAuto ].
 111       Apply (pc3_pr3_u c0 x); [ Idtac | Apply (pc3_pr3_u2 c0 t0) ]; XEAuto.
 112 (* case 2.3.5: i >= i0 *)
 113       CSubst0Drop; Apply (pc3_pr3_u c0 t0); XEAuto.
 114       Qed.
 115
 116       Theorem pc3_pc2_fsubst0: (c1:?; t1,t:?) (pc2 c1 t1 t) ->
 117                                (i:?; u,c2,t2:?) (fsubst0 i u c1 t1 c2 t2) ->
 118                                (e:?) (drop i (0) c1 (CTail e (Bind Abbr) u)) ->
 119                                (pc3 c2 t2 t).
 120       Intros until 1; XElim H; Intros.
 121 (* case 1: pc2_r *)
 122       EApply pc3_pr2_fsubst0; XEAuto.
 123 (* case 2: pc2_x *)
 124       Apply pc3_s; EApply pc3_pr2_fsubst0_back; XEAuto.
 125       Qed.
 126
 127       Theorem pc3_fsubst0: (c1:?; t1,t:?) (pc3 c1 t1 t) ->
 128                            (i:?; u,c2,t2:?) (fsubst0 i u c1 t1 c2 t2) ->
 129                            (e:?) (drop i (0) c1 (CTail e (Bind Abbr) u)) ->
 130                            (pc3 c2 t2 t).
 131       Intros until 1; XElim H.
 132 (* case 1: pc3_r *)
 133       Intros until 1; XElim H; Intros; Try CSubst0Drop; XEAuto.
 134 (* case 2: pc3_u *)
 135       Intros until 4; XElim H2; Intros;
 136       (Apply (pc3_t t2); [ EApply pc3_pc2_fsubst0; XEAuto | XEAuto ]).
 137       Qed.
 138
 139    End pc3_fsubst0.
 140
 141       Hints Resolve pc3_fsubst0.