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