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

   1 (*#* #stop file *)
   2
   3 Require Export contexts_defs.
   4 Require Export subst0_defs.
   5 Require Export drop_defs.
   6
   7       Inductive csubst0 : nat -> T -> C -> C -> Prop :=
   8          | csubst0_fst  : (k:?; i:?; u,v,w:?) (subst0 (r k i) v u w) -> (c:?)
   9                           (csubst0 (S i) v (CTail c k u) (CTail c k w))
  10          | csubst0_snd  : (k:?; i:?; c1,c2:?; v:?) (csubst0 (r k i) v c1 c2) ->
  11                           (u:?) (csubst0 (S i) v (CTail c1 k u) (CTail c2 k u))
  12          | csubst0_both : (k:?; i:?; u,v,w:?) (subst0 (r k i) v u w) ->
  13                           (c1,c2:?) (csubst0 (r k i) v c1 c2) ->
  14                           (csubst0 (S i) v (CTail c1 k u) (CTail c2 k w)).
  15
  16       Hint csubst0 : ltlc := Constructors csubst0.
  17
  18       Inductive fsubst0 [i:nat; v:T; c1:C; t1:T] : C -> T -> Prop :=
  19          | fsubst0_t : (t2:?) (subst0 i v t1 t2) -> (fsubst0 i v c1 t1 c1 t2)
  20          | fsubst0_c : (c2:?) (csubst0 i v c1 c2) -> (fsubst0 i v c1 t1 c2 t1)
  21          | fsubst0_b : (t2:?) (subst0 i v t1 t2) ->
  22                        (c2:?) (csubst0 i v c1 c2) -> (fsubst0 i v c1 t1 c2 t2).
  23
  24       Hint fsubst0 : ltlc := Constructors fsubst0.
  25
  26    Section csubst0_gen_base. (***********************************************)
  27
  28       Theorem csubst0_gen_tail: (k:?; c1,x:?; u1,v:?; i:?)
  29                                 (csubst0 (S i) v (CTail c1 k u1) x) -> (OR
  30                                 (EX u2 | x = (CTail c1 k u2) &
  31                                          (subst0 (r k i) v u1 u2)
  32                                 ) |
  33                                 (EX c2 | x = (CTail c2 k u1) &
  34                                          (csubst0 (r k i) v c1 c2)
  35                                 ) |
  36                                 (EX u2 c2 | x = (CTail c2 k u2) &
  37                                             (subst0 (r k i) v u1 u2) &
  38                                             (csubst0 (r k i) v c1 c2)
  39                                 )).
  40       Intros until 1; InsertEq H '(S i); InsertEq H '(CTail c1 k u1).
  41       XCase H; Clear x v y y0; Intros; Inversion H1.
  42 (* case 1: csubst0_fst *)
  43       Inversion H0; Rewrite H3 in H; Rewrite H5 in H; Rewrite H6 in H; XEAuto.
  44 (* case 2: csubst0_snd *)
  45       Inversion H0; Rewrite H3 in H; Rewrite H4 in H; Rewrite H5 in H; XEAuto.
  46 (* case 2: csubst0_both *)
  47       Inversion H2; Rewrite H5 in H; Rewrite H6 in H; Rewrite H7 in H;
  48       Rewrite H4 in H0; Rewrite H5 in H0; Rewrite H7 in H0; XEAuto.
  49       Qed.
  50
  51    End csubst0_gen_base.
  52
  53       Tactic Definition CSubst0GenBase :=
  54          Match Context With
  55             | [ H: (csubst0 (S ?1) ?2 (CTail ?3 ?4 ?5) ?6) |- ? ] ->
  56                LApply (csubst0_gen_tail ?4 ?3 ?6 ?5 ?2 ?1); [ Clear H; Intros H | XAuto ];
  57                XElim H; Intros H; XElim H; Intros.
  58
  59    Section csubst0_drop. (***************************************************)
  60
  61       Theorem csubst0_drop_ge : (i,n:?) (le i n) ->
  62                                 (c1,c2:?; v:?) (csubst0 i v c1 c2) ->
  63                                 (e:?) (drop n (0) c1 e) ->
  64                                 (drop n (0) c2 e).
  65       XElim i.
  66 (* case 1: i = 0 *)
  67       Intros; Inversion H0.
  68 (* case 2: i > 0 *)
  69       Intros i; XElim n.
  70 (* case 2.1: n = 0 *)
  71       Intros; Inversion H0.
  72 (* case 2.2: n > 0 *)
  73       Intros until 3; Clear H0; InsertEq H2 '(S i); XElim H0; Intros.
  74       DropGenBase.
  75 (* case 2.2.1: csubst0_fst *)
  76       XAuto.
  77 (* case 2.2.2: csubst0_snd *)
  78       XReplaceIn H0 i0 i; DropGenBase; NewInduction k; XEAuto.
  79 (* case 2.2.3: csubst0_both *)
  80       XReplaceIn H0 i0 i; XReplaceIn H2 i0 i.
  81       DropGenBase; NewInduction k; XEAuto.
  82       Qed.
  83
  84       Tactic Definition IH :=
  85          Match Context With
  86             | [ H0: (n:?) (lt n ?1) -> (c1,c2:?; v:?) (csubst0 ?1 v c1 c2) -> (e:C) (drop n (0) c1 e) -> ?;
  87                 H1: (csubst0 ?1 ?2 ?3 ?4); H2: (drop ?5 (0) ?3 ?6) |- ? ] ->
  88                LApply (H0 ?5); [ Clear H0; Intros H0 | XAuto ];
  89                LApply (H0 ?3 ?4 ?2); [ Clear H0 H1; Intros H0 | XAuto ];
  90                LApply (H0 ?6); [ Clear H0 H2; Intros H0 | XAuto ];
  91                XElim H0; Intros H0; [ Idtac | XElim H0 | XElim H0 | XElim H0 ]; Intros
  92             | [ H0: (r ? ?1) = (S ?1) -> (e:?) (drop (S ?2) (0) ?3 e) -> ?;
  93                 H1: (drop (S ?2) (0) ?3 ?4) |- ? ] ->
  94                LApply H0; [ Clear H0; Intros H0 | XAuto ];
  95                LApply (H0 ?4); [ Clear H0 H1; Intros H0 | XAuto ];
  96                XElim H0; Intros H0; [ Idtac | XElim H0 | XElim H0 | XElim H0 ]; Intros.
  97
  98       Theorem csubst0_drop_lt : (i,n:?) (lt n i) ->
  99                                 (c1,c2:?; v:?) (csubst0 i v c1 c2) ->
 100                                 (e:?) (drop n (0) c1 e) -> (OR
 101                                 (drop n (0) c2 e) |
 102                                 (EX k e0 u w | e = (CTail e0 k u) &
 103                                                (drop n (0) c2 (CTail e0 k w)) &
 104                                                (subst0 (minus (r k i) (S n)) v u w)
 105                                 ) |
 106                                 (EX k e1 e2 u | e = (CTail e1 k u) &
 107                                                 (drop n (0) c2 (CTail e2 k u)) &
 108                                                 (csubst0 (minus (r k i) (S n)) v e1 e2)
 109                                 ) |
 110                                 (EX k e1 e2 u w | e = (CTail e1 k u) &
 111                                                  (drop n (0) c2 (CTail e2 k w)) &
 112                                                  (subst0 (minus (r k i) (S n)) v u w) &
 113                                                  (csubst0 (minus (r k i) (S n)) v e1 e2)
 114                                 )).
 115       XElim i.
 116 (* case 1: i = 0 *)
 117       Intros; Inversion H.
 118 (* case 2: i > 0 *)
 119       Intros i; XElim n.
 120 (* case 2.1: n = 0 *)
 121       Intros H0; Clear H0; Intros until 1; InsertEq H0 '(S i); XElim H0;
 122       Clear H c1 c2 v y; Intros; DropGenBase; XRewrite e;
 123       Rewrite <- r_arith0 in H; Try Rewrite <- r_arith0 in H0; Replace i with i0; XEAuto.
 124 (* case 2.2: n > 0 *)
 125       Intros until 3; Clear H0; InsertEq H2 '(S i); XElim H0; Clear c1 c2 v y;
 126       Intros; DropGenBase.
 127 (* case 2.2.1: csubst0_fst *)
 128       XEAuto.
 129 (* case 2.2.2: csubst0_snd *)
 130       Replace i0 with i; XAuto; XReplaceIn H0 i0 i; XReplaceIn H2 i0 i; Clear H3 i0.
 131       Apply (r_dis k); Intros; Rewrite (H3 i) in H0; Rewrite (H3 n) in H4.
 132 (* case 2.2.2.1: bind *)
 133       IH; XRewrite e; Try Rewrite <- (H3 n) in H; Try Rewrite <- (H3 n) in H0;
 134       Try Rewrite <- r_arith1 in H4; Try Rewrite <- r_arith1 in H5; XEAuto.
 135 (* case 2.2.2.2: flat *)
 136       IH; XRewrite e; Try Rewrite <- (H3 n) in H2; Try Rewrite <- (H3 n) in H4; XEAuto.
 137 (* case 2.2.3: csubst0_both *)
 138       Replace i0 with i; XAuto; XReplaceIn H0 i0 i; XReplaceIn H2 i0 i; XReplaceIn H3 i0 i; Clear H4 i0.
 139       Apply (r_dis k); Intros; Rewrite (H4 i) in H2; Rewrite (H4 n) in H5.
 140 (* case 2.2.2.1: bind *)
 141       IH; XRewrite e; Try Rewrite <- (H4 n) in H; Try Rewrite <- (H4 n) in H2;
 142       Try Rewrite <- r_arith1 in H5; Try Rewrite <- r_arith1 in H6; XEAuto.
 143 (* case 2.2.3.2: flat *)
 144       IH; XRewrite e; Try Rewrite <- (H4 n) in H3; Try Rewrite <- (H4 n) in H5; XEAuto.
 145       Qed.
 146
 147       Theorem csubst0_drop_ge_back : (i,n:?) (le i n) ->
 148                                      (c1,c2:?; v:?) (csubst0 i v c1 c2) ->
 149                                      (e:?) (drop n (0) c2 e) ->
 150                                      (drop n (0) c1 e).
 151       XElim i.
 152 (* case 1 : i = 0 *)
 153       Intros; Inversion H0.
 154 (* case 2 : i > 0 *)
 155       Intros i; XElim n.
 156 (* case 2.1 : n = 0 *)
 157       Intros; Inversion H0.
 158 (* case 2.2 : n > 0 *)
 159       Intros until 3; Clear H0; InsertEq H2 '(S i); XElim H0; Intros;
 160       DropGenBase.
 161 (* case 2.2.1 : csubst0_fst *)
 162       XAuto.
 163 (* case 2.2.2 : csubst0_snd *)
 164       XReplaceIn H0 i0 i; NewInduction k; XEAuto.
 165 (* case 2.2.3 : csubst0_both *)
 166       XReplaceIn H0 i0 i; XReplaceIn H2 i0 i; NewInduction k; XEAuto.
 167       Qed.
 168
 169    End csubst0_drop.
 170
 171       Tactic Definition CSubst0Drop :=
 172          Match Context With
 173             | [ H1: (lt ?2 ?1);
 174                 H2: (csubst0 ?1 ?3 ?4 ?5); H3: (drop ?2 (0) ?4 ?6) |- ? ] ->
 175                LApply (csubst0_drop_lt ?1 ?2); [ Intros H_x | XAuto ];
 176                LApply (H_x ?4 ?5 ?3); [ Clear H_x; Intros H_x | XAuto ];
 177                LApply (H_x ?6); [ Clear H_x H3; Intros H3 | XAuto ];
 178                XElim H3;
 179                [ Intros | Intros H3; XElim H3; Intros
 180                | Intros H3; XElim H3; Intros | Intros H3; XElim H3; Intros ]
 181             | [ H1: (le ?1 ?2);
 182                 H2: (csubst0 ?1 ?3 ?4 ?5); H3: (drop ?2 (0) ?4 ?6) |- ? ] ->
 183                LApply (csubst0_drop_ge ?1 ?2); [ Intros H_x | XAuto ];
 184                LApply (H_x ?4 ?5 ?3); [ Clear H_x; Intros H_x | XAuto ];
 185                LApply (H_x ?6); [ Clear H_x H3; Intros | XAuto ]
 186             | [H2: (csubst0 ?1 ?3 ?4 ?5); H3: (drop ?1 (0) ?4 ?6) |- ? ] ->
 187                LApply (csubst0_drop_ge ?1 ?1); [ Intros H_x | XAuto ];
 188                LApply (H_x ?4 ?5 ?3); [ Clear H_x H2; Intros H2 | XAuto ];
 189                LApply (H2 ?6); [ Clear H2 H3; Intros | XAuto ]
 190             | [H2: (csubst0 ?1 ?3 ?4 ?5); H3: (drop ?1 (0) ?5 ?6) |- ? ] ->
 191                LApply (csubst0_drop_ge_back ?1 ?1); [ Intros H_x | XAuto ];
 192                LApply (H_x ?4 ?5 ?3); [ Clear H_x; Intros H_x | XAuto ];
 193                LApply (H_x ?6); [ Clear H_x H3; Intros | XAuto ]
 194             | [H2: (csubst0 ?1 ?3 ?4 ?5); H3: (drop ?2 (0) ?5 ?6) |- ? ] ->
 195                LApply (csubst0_drop_ge_back ?1 ?2); [ Intros H_x | XAuto ];
 196                LApply (H_x ?4 ?5 ?3); [ Clear H_x; Intros H_x | XAuto ];
 197                LApply (H_x ?6); [ Clear H_x H3; Intros | XAuto ].
 198