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

   1 Require lift_gen.
   2 Require drop_defs.
   3
   4 (*#* #caption "main properties of drop" #clauses *)
   5
   6    Section confluence. (*****************************************************)
   7
   8 (*#* #stop macro *)
   9
  10       Tactic Definition IH :=
  11          Match Context With
  12             [ H1: (drop ?1 ?2 c ?3); H2: (drop ?1 ?2 c ?4) |- ? ] ->
  13                LApply (H ?4 ?2 ?1); [ Clear H H2; Intros H | XAuto ];
  14                LApply (H ?3); [ Clear H H1; Intros | XAuto ].
  15
  16 (*#* #start macro *)
  17
  18 (*#* #caption "confluence, first case" *)
  19 (*#* #cap #alpha c in C, x1 in C1, x2 in C2, d in i *)
  20
  21       Theorem drop_mono : (c,x1:?; d,h:?) (drop h d c x1) ->
  22                           (x2:?) (drop h d c x2) -> x1 = x2.
  23
  24 (*#* #stop proof *)
  25
  26       XElim c.
  27 (* case 1: CSort *)
  28       Intros; Repeat DropGenBase; Rewrite H0; XAuto.
  29 (* case 2: CTail k *)
  30       XElim d.
  31 (* case 2.1: d = 0 *)
  32       XElim h; Intros; Repeat DropGenBase; Try Rewrite <- H0; XEAuto.
  33 (* case 2.2: d > 0 *)
  34       Intros; Repeat DropGenBase; Rewrite H1; Rewrite H2; Rewrite H5 in H3;
  35       LiftGen; IH; XAuto.
  36       Qed.
  37
  38 (*#* #start proof *)
  39
  40 (*#* #caption "confluence, second case" *)
  41 (*#* #cap #alpha c in C1, c0 in E1, e in C2, e0 in E2, u in V1, v in V2, i in k, d in i *)
  42
  43       Theorem drop_conf_lt: (b:?; i:?; u:?; c0,c:?)
  44                             (drop i (0) c (CTail c0 (Bind b) u)) ->
  45                             (e:?; h,d:?) (drop h (S (plus i d)) c e) ->
  46                             (EX v e0 | u = (lift h d v) &
  47                                        (drop i (0) e (CTail e0 (Bind b) v)) &
  48                                        (drop h d c0 e0)
  49                             ).
  50
  51 (*#* #stop proof *)
  52
  53       XElim i.
  54 (* case 1 : i = 0 *)
  55       Intros until 1.
  56       DropGenBase.
  57       Rewrite H in H0; Clear H.
  58       Inversion H0; XEAuto.
  59 (* case 2 : i > 0 *)
  60       Intros i; XElim c.
  61 (* case 2.1 : CSort *)
  62       Intros; Inversion H0.
  63 (* case 2.2 : CTail k *)
  64       XElim k; Intros; Repeat DropGenBase; Rewrite H2; Clear H2 H3 e t.
  65 (* case 2.2.1 : Bind *)
  66       LApply (H u c0 c); [ Clear H H0 H1; Intros H | XAuto ].
  67       LApply (H x0 h d); [ Clear H H9; Intros H | XAuto ].
  68       XElim H; XEAuto.
  69 (* case 2.2.2 : Flat *)
  70       LApply H0; [ Clear H H0 H1; Intros H | XAuto ].
  71       LApply (H x0 h d); [ Clear H H9; Intros H | XAuto ].
  72       XElim H; XEAuto.
  73       Qed.
  74
  75 (*#* #start proof *)
  76
  77 (*#* #caption "confluence, third case" *)
  78 (*#* #cap #alpha c in C, a in C1, e in C2, i in k, d in i *)
  79
  80       Theorem drop_conf_ge: (i:?; a,c:?) (drop i (0) c a) ->
  81                             (e:?; h,d:?) (drop h d c e) -> (le (plus d h) i) ->
  82                             (drop (minus i h) (0) e a).
  83
  84 (*#* #stop proof *)
  85
  86       XElim i.
  87 (* case 1 : i = 0 *)
  88       Intros until 1.
  89       DropGenBase; Rewrite H in H0; Clear H c.
  90       Inversion H1; Rewrite H2; Simpl; Clear H1.
  91       PlusO; Rewrite H in H0; Rewrite H1 in H0; Clear H H1 d h.
  92       DropGenBase; Rewrite <- H; XAuto.
  93 (* case 2 : i > 0 *)
  94       Intros i; XElim c.
  95 (* case 2.1 : CSort *)
  96       Intros; Repeat DropGenBase; Rewrite H1; Rewrite H0; XAuto.
  97 (* case 2.2 : CTail k *)
  98       XElim k; Intros; DropGenBase;
  99       ( NewInduction d;
 100       [ NewInduction h; DropGenBase;
 101         [ Rewrite <- H2; Simpl; XAuto | Clear IHh ]
 102       | DropGenBase; Rewrite H2; Clear IHd H2 H4 e t ] ).
 103 (* case 2.2.1 : Bind, d = 0, h > 0 *)
 104       LApply (H a c); [ Clear H H0 H1; Intros H | XAuto ].
 105       LApply (H e h (0)); XAuto.
 106 (* case 2.2.2 : Bind, d > 0 *)
 107       LApply (H a c); [ Clear H H0 H1; Intros H | XAuto ].
 108       LApply (H x0 h d); [ Clear H H4; Intros H | XAuto ].
 109       LApply H; [ Clear H; Simpl in H3; Intros H | XAuto ].
 110       Rewrite <- minus_Sn_m; XEAuto.
 111 (* case 2.2.3 : Flat, d = 0, h > 0 *)
 112       LApply H0; [ Clear H H0 H1; Intros H | XAuto ].
 113       LApply (H e (S h) (0)); XAuto.
 114 (* case 2.2.4 : Flat, d > 0 *)
 115       LApply H0; [ Clear H H0 H1; Intros H | XAuto ].
 116       LApply (H x0 h (S d)); [ Clear H H4; Intros H | XAuto ].
 117       LApply H; [ Clear H; Simpl in H3; Intros H | XAuto ].
 118       Rewrite <- minus_Sn_m in H; [ Idtac | XEAuto ].
 119       Rewrite <- minus_Sn_m; XEAuto.
 120       Qed.
 121
 122 (*#* #start proof *)
 123
 124    End confluence.
 125
 126    Section transitivity. (***************************************************)
 127
 128 (*#* #caption "transitivity, first case" *)
 129 (*#* #cap #alpha c1 in C1, c2 in C2, e1 in D1, e2 in D2, d in i, i in k *)
 130
 131       Theorem drop_trans_le : (i,d:?) (le i d) ->
 132                               (c1,c2:?; h:?) (drop h d c1 c2) ->
 133                               (e2:?) (drop i (0) c2 e2) ->
 134                               (EX e1 | (drop i (0) c1 e1) & (drop h (minus d i) e1 e2)).
 135
 136 (*#* #stop proof *)
 137
 138       XElim i.
 139 (* case 1 : i = 0 *)
 140       Intros.
 141       DropGenBase; Rewrite H1 in H0.
 142       Rewrite <- minus_n_O; XEAuto.
 143 (* case 2 : i > 0 *)
 144       Intros i IHi; XElim d.
 145 (* case 2.1 : d = 0 *)
 146       Intros; Inversion H.
 147 (* case 2.2 : d > 0 *)
 148       Intros d IHd; XElim c1.
 149 (* case 2.2.1 : CSort *)
 150       Intros.
 151       DropGenBase; Rewrite H0 in H1.
 152       DropGenBase; Rewrite H1; XEAuto.
 153 (* case 2.2.2 : CTail k *)
 154       Intros c1 IHc; XElim k; Intros;
 155       DropGenBase; Rewrite H0 in H1; Rewrite H2; Clear IHd H0 H2 c2 t;
 156       DropGenBase.
 157 (* case 2.2.2.1 : Bind *)
 158       LApply (IHi d); [ Clear IHi; Intros IHi | XAuto ].
 159       LApply (IHi c1 x0 h); [ Clear IHi H8; Intros IHi | XAuto ].
 160       LApply (IHi e2); [ Clear IHi H0; Intros IHi | XAuto ].
 161       XElim IHi; XEAuto.
 162 (* case 2.2.2.2 : Flat *)
 163       LApply (IHc x0 h); [ Clear IHc H8; Intros IHc | XAuto ].
 164       LApply (IHc e2); [ Clear IHc H0; Intros IHc | XAuto ].
 165       XElim IHc; XEAuto.
 166       Qed.
 167
 168 (*#* #start proof *)
 169
 170 (*#* #caption "transitivity, second case" *)
 171 (*#* #cap #alpha c1 in C1, c2 in C, e2 in C2, d in i, i in k *)
 172
 173       Theorem drop_trans_ge : (i:?; c1,c2:?; d,h:?) (drop h d c1 c2) ->
 174                               (e2:?) (drop i (0) c2 e2) -> (le d i) ->
 175                               (drop (plus i h) (0) c1 e2).
 176
 177 (*#* #stop proof *)
 178
 179       XElim i.
 180 (* case 1: i = 0 *)
 181       Intros.
 182       DropGenBase; Rewrite <- H0.
 183       Inversion H1; Rewrite H2 in H; XAuto.
 184 (* case 2 : i > 0 *)
 185       Intros i IHi; XElim c1; Simpl.
 186 (* case 2.1: CSort *)
 187       Intros.
 188       DropGenBase; Rewrite H in H0.
 189       DropGenBase; Rewrite H0; XAuto.
 190 (* case 2.2: CTail *)
 191       Intros c1 IHc; XElim d.
 192 (* case 2.2.1: d = 0 *)
 193       XElim h; Intros.
 194 (* case 2.2.1.1: h = 0 *)
 195       DropGenBase; Rewrite <- H in H0;
 196       DropGenBase; Rewrite <- plus_n_O; XAuto.
 197 (* case 2.2.1.2: h > 0 *)
 198       DropGenBase; Rewrite <- plus_n_Sm.
 199       Apply drop_drop; RRw; XEAuto. (**) (* explicit constructor *)
 200 (* case 2.2.2: d > 0 *)
 201       Intros d IHd; Intros.
 202       DropGenBase; Rewrite H in IHd; Rewrite H in H0; Rewrite H2 in IHd; Rewrite H2; Clear IHd H H2 c2 t;
 203       DropGenBase; Apply drop_drop; NewInduction k; Simpl; XEAuto. (**) (* explicit constructor *)
 204       Qed.
 205
 206 (*#* #start proof *)
 207
 208    End transitivity.
 209
 210 (*#* #stop macro *)
 211
 212       Tactic Definition DropDis :=
 213          Match Context With
 214             [ H1: (drop ?1 ?2 ?3 ?4); H2: (drop ?1 ?2 ?3 ?5) |- ? ] ->
 215                LApply (drop_mono ?3 ?5 ?2 ?1); [ Intros H_x | XAuto ];
 216                LApply (H_x ?4); [ Clear H_x H1; Intros H1; Rewrite H1 in H2 | XAuto ]
 217             | [ H1: (drop ?0 (0) ?1 (CTail ?2 (Bind ?3) ?4));
 218                 H2: (drop ?5 (S (plus ?0 ?6)) ?1 ?7) |- ? ] ->
 219                LApply (drop_conf_lt ?3 ?0 ?4 ?2 ?1); [ Clear H1; Intros H1 | XAuto ];
 220                LApply (H1 ?7 ?5 ?6); [ Clear H1 H2; Intros H1 | XAuto ];
 221                XElim H1; Intros
 222             | [ _: (drop ?0 (0) ?1 ?2); _: (drop ?5 (0) ?1 ?7);
 223                 _: (lt ?5 ?0) |- ? ] ->
 224                LApply (drop_conf_ge ?0 ?2 ?1); [ Intros H_x | XAuto ];
 225                LApply (H_x ?7 ?5 (0)); [ Clear H_x; Intros H_x | XAuto ];
 226                Simpl in H_x; LApply H_x; [ Clear H_x; Intros | XAuto ]
 227             | [ _: (drop ?1 (0) ?2 (CTail ?3 (Bind ?) ?));
 228                 _: (drop (1) ?1 ?2 ?4) |- ? ] ->
 229                LApply (drop_conf_ge (S ?1) ?3 ?2); [ Intros H_x | XEAuto ];
 230                LApply (H_x ?4 (1) ?1); [ Clear H_x; Intros H_x | XAuto ];
 231                LApply H_x; [ Clear H_x; Intros | Rewrite plus_sym; XAuto ]; (
 232                Match Context With
 233                   [ H: (drop (minus (S ?1) (1)) (0) ?4 ?3) |- ? ] ->
 234                     Simpl in H; Rewrite <- minus_n_O in H )
 235             | [ H0: (drop ?0 (0) ?1 ?2); H2: (lt ?6 ?0);
 236                 H1: (drop (1) ?6 ?1 ?7) |- ? ] ->
 237                LApply (drop_conf_ge ?0 ?2 ?1); [ Intros H_x | XAuto ];
 238                LApply (H_x ?7 (1) ?6); [ Clear H_x; Intros H_x | XAuto ];
 239                LApply H_x; [ Clear H_x; Intros | Rewrite plus_sym; XAuto ]
 240             | [ H0: (drop ?0 (0) ?1 ?2);
 241                 H1: (drop ?5 ?6 ?1 ?7) |- ? ] ->
 242                LApply (drop_conf_ge ?0 ?2 ?1); [ Intros H_x | XAuto ];
 243                LApply (H_x ?7 ?5 ?6); [ Clear H_x; Intros H_x | XAuto ];
 244                LApply H_x; [ Clear H_x; Intros | XAuto ]
 245             | [ H0: (lt ?1 ?2);
 246                 H1: (drop ?3 ?2 ?4 ?5); H2: (drop ?1 (0) ?5 ?6) |- ? ] ->
 247                LApply (drop_trans_le ?1 ?2); [ Intros H_x | XAuto ];
 248                LApply (H_x ?4 ?5 ?3); [ Clear H_x H1; Intros H_x | XAuto ];
 249                LApply (H_x ?6); [ Clear H_x H2; Intros H_x | XAuto ];
 250                XElim H_x; Intros
 251             | [ H0: (le ?1 ?2);
 252                 H1: (drop ?3 ?1 ?4 ?5); H2: (drop ?2 (0) ?5 ?6) |- ? ] ->
 253                LApply (drop_trans_ge ?2 ?4 ?5 ?1 ?3); [ Clear H1; Intros H1 | XAuto ];
 254                LApply (H1 ?6); [ Clear H1 H2; Intros H1 | XAuto ];
 255                LApply H1; [ Clear H1; Intros | XAuto ].
 256
 257 (*#* #start macro *)
 258
 259 (*#* #single *)