helm/coq-contribs/SUBSETS/st_arith.v

   1 Require Export st_nat.
   2
   3 Section Arith_Functions.
   4
   5    Section head_tail_append.
   6
   7       Variable S:Set.
   8 (*
   9 Definition hd: (List S) -> (List S) := (listrec S [_](List S) (empty ?) [_;_](fr ? (empty ?))).
  10 *)
  11       Definition hde: S -> (List S) -> S := [a](listrec S [_]S a [_;_;a]a).
  12
  13       Definition tl: (List S) -> (List S) := (listrec S [_](List S) (empty ?) [v;_;_]v).
  14
  15       Definition app: (List S) -> (List S) -> (List S) := [v](listrec S [_](List S) v [_;p;a](fr S p a)).
  16
  17       Definition app_three: (List S) -> (List S) -> (List S) -> (List S) := [v,w](app (app v w)).
  18 (*
  19 Definition bs_app: (ListS S) -> N -> (List S) := (bs_iter (List S) (empty S) app).
  20
  21 Definition rbs_app: (ListS S)->N->(List S) := (rbs_iter (List S) (empty S) app).
  22 *)
  23       Definition LIn: S -> (List S) -> Set := [a;l](LEx (List S) [v](LEx (List S) [w](Id (List S) (app (fr S v a) w) l))).
  24
  25    End head_tail_append.
  26
  27    Section slicing.
  28
  29       Variable S:Set; n:N; v:(List S).
  30
  31       Definition lskip: N -> (List S) -> (List S) := (natrec [_](List S)->(List S) [w]w [_;p;w](p (tl ? w))).
  32 (*
  33 Definition lfirst: N -> (List S) -> (List S) := (natrec [_](List S)->(List S) [_](empty S) [_;p;w](app ? (p (tl ? w)) (hd ? w))).
  34
  35 Definition lslice: N -> N -> (List S) -> (List S) := [m;n;v](lfirst n (lskip m v)).
  36
  37 Definition lix: N -> (List S) -> (List S) := [n;v](hd S (lskip n v)).
  38
  39 Definition lixe: S -> N -> (List S) -> S := [a;n;v](hde S a (lskip n v)).
  40
  41 Definition llen: (List S) -> N := (listrec S [_]N zero [_;p;_](succ p)).
  42 *)
  43    End slicing.
  44
  45    Section arithmetic.
  46
  47       Definition pred: N -> N := (tl One).
  48
  49       Definition add: N -> N -> N := (app One).
  50
  51       Definition add_three: N -> N -> N -> N := (app_three One).
  52 (*
  53 Definition bs_add: NS -> N -> N := (bs_app One).
  54
  55 Definition rbs_add:NS->N->N := (rbs_app One).
  56 *)
  57       Definition sub: N -> N -> N := [m;n](lskip One n m).
  58 (*
  59 Definition sub_t: N -> N -> N -> N := [m,n](sub (sub m n)).
  60
  61 Definition absv: N -> N -> N := [m;n](plus (minus m n) (minus n m)).
  62 *)
  63    End arithmetic.
  64
  65 End Arith_Functions.
  66
  67 Section Arith_Hints.
  68
  69    Section arith_fold.
  70 (*
  71 Theorem bs_app_fold: (n:N; S:Set; ls:(ListS S); P:(List S)->Set) (P (bs_app S ls n)) -> (P (bs_iter (List S) (empty S) (app S) ls n)).
  72 Intros.
  73 Assumption.
  74 Qed.
  75 *)
  76       Theorem pred_fold: (n:N; P:N->Set) (P (pred n)) -> (P (tl One n)).
  77       Intros.
  78       Assumption.
  79       Qed.
  80 (*
  81 Theorem add_fold: (m,n:N; P:N->Set) (P (add m n)) -> (P (app One m n)).
  82 Intros.
  83 Apply (id_repl N (app One m n) (add m n)).
  84 Apply id_r.
  85 Assumption.
  86 Qed.
  87
  88 Theorem bs_add_fold: (n:N; ns:NS; P:N->Set) (P (bs_add ns n)) -> (P (bs_app One ns n)).
  89 Intros.
  90 Assumption.
  91 Qed.
  92 *)
  93    End arith_fold.
  94
  95 End Arith_Hints.
  96
  97 Section Arith_Results.
  98
  99    Section head_tail_results.
 100
 101       Theorem fr_ini1: (S:Set; a,b:S; v,w:(List S)) (Id (List S) (fr S v a) (fr S w b)) -> (Id (List S) v w).
 102       Intros.
 103       MApply '(id_repl (List S) v (tl S (fr S v a))).
 104       MApply '(id_repl (List S) w (tl S (fr S w b))).
 105       MApply '(id_comp (List S)).
 106       Qed.
 107
 108       Theorem fr_ini2: (S:Set; v,w:(List S); a,b:S) (Id (List S) (fr S v a) (fr S w b)) -> (Id S a b).
 109       Intros.
 110       MApply '(id_repl S a (hde S a (fr S v a))).
 111       MApply '(id_repl S b (hde S a (fr S w b))).
 112       MApply '(id_comp (List S)).
 113       Qed.
 114 (*
 115 Theorem hd_hde_id: (S:Set; a:S; v:(List S)) (GT (llen S v) zero) -> (Id (List S) (hd S v) (fr S (empty S) (hde S a v))).
 116 Intros S a v.
 117 MElim 'v 'listrec.
 118 MApply '(gt_false zero).
 119 Qed.
 120
 121 Theorem tl_len: (S:Set; v:(List S)) (Id N (llen S (tl S v)) (pred (llen S v))).
 122 Intros.
 123 MElim 'v 'listrec.
 124 Qed.
 125 *)
 126       Theorem app_empty: (S:Set; v:(List S)) (Id (List S) (app S (empty S) v) v).
 127       Intros.
 128       MElim 'v 'listrec.
 129       MApply '(id_comp (List S) (List S) [v:?](fr S v s)).
 130       Qed.
 131 (*
 132 Theorem app_ass: (S:Set; u,v,w:(List S)) (Id (List S) (app S (app S u v) w) (app S u (app S v w))).
 133 Intros.
 134 MElim 'w 'listrec.
 135 MApply '(id_comp (List S) (List S) [v:?](fr S v y)).
 136 Qed.
 137 *)
 138       Theorem lin_i: (S:Set; v,w,l:(List S); a:S) (Id (List S) (app S (fr S v a) w) l) -> (LIn S a l).
 139       Intros.
 140       Unfold LIn.
 141       MApply '(lex_i (List S) v).
 142       MApply '(lex_i (List S) w).
 143       Qed.
 144
 145       Theorem lin_e: (S:Set; a:S; l:(List S); P:Set) (LIn S a l) -> ((v,w:(List S)) (Id (List S) (app S (fr S v a) w) l) -> P) -> P.
 146       Intros.
 147       MElim 'H 'lex_e.
 148       MElim 'y 'lex_e.
 149       MApply '(H0 a0 a1).
 150       Qed.
 151
 152       Theorem lin_fr_i: (S:Set; a,b:S; l:(List S)) (LOr (LIn S a l) (Id S a b)) -> (LIn S a (fr S l b)).
 153       Intros.
 154       MElim 'H '(when (LIn S a l) (Id S a b)).
 155       MApply '(lin_e S a l).
 156       MApply '(id_repl (List S) l (app S (fr S v a) w)).
 157       MApply '(lin_i S v (fr S w b)).
 158       MApply '(id_repl S b a).
 159       MApply '(lin_i S l (empty S)).
 160       Qed.
 161
 162    End head_tail_results.
 163 (*
 164 Section slicing_results.
 165
 166 Theorem lskip_empty: (S:Set; n:N) (Id (List S) (lskip S n (empty S)) (empty S)).
 167 Intros.
 168 MElim 'n 'natrec.
 169 Qed.
 170
 171 Theorem lskip_tl: (S:Set; n:N; v:(List S)) (Id (List S) (lskip S n (tl S v)) (tl S (lskip S n v))).
 172 Intros S n.
 173 MElim 'n 'natrec.
 174 MElim 'v 'listrec.
 175 (MApply '(id_repl ? (lskip S n0 (empty S)) (empty S)); MApply 'id_comm).
 176 MApply 'lskip_empty.
 177 MApply '(H l).
 178 Qed.
 179
 180 Theorem lixe_empty: (n:N; S:Set; a:S) (Id S (lixe S a n (empty S)) a).
 181 Intros.
 182 MElim 'n 'natrec.
 183 Qed.
 184
 185 Theorem lixe_app_v: (S:Set; a,b:S; w,v:(List S); n:N) (GT (llen S v) n) -> (Id S (lixe S a n (app S w v)) (lixe S b n v)).
 186 Intros S a b w v.
 187 (Elim v using listrec; MSimpl).
 188 Intros.
 189 MApply '(gt_false n).
 190 Intros l H y n.
 191 MElim 'n 'natrec.
 192 (Unfold lixe; Simpl).
 193 Fold (lixe S a n0 (app S w l)) (lixe S b n0 l). (**)
 194 MApply '(H n0).
 195 Qed.
 196
 197 Theorem lixe_le: (S:Set; a:S; v:(List S); n:N) (LE (llen S v) n) -> (Id S (lixe S a n v) a).
 198 Intros S a v.
 199 (Elim v using listrec; Simpl).
 200 Intros n.
 201 MElim 'n 'natrec.
 202 MApply 'lixe_empty.
 203 Intros l H y n.
 204 MElim 'n 'natrec.
 205 MApply '(le_false (succ (llen S l))).
 206 (Unfold lixe; Simpl).
 207 Fold (lixe S a n0 l). (**)
 208 MApply '(H n0).
 209 Qed.
 210
 211 Theorem lslice_lix: (S:Set; k:N; v:(List S)) (Id (List S) (lslice S k one v) (lix S k v)).
 212 Intros.
 213 Unfold lslice lfirst.
 214 MSimpl.
 215 MApply 'app_empty.
 216 Qed.
 217
 218 End slicing_results.
 219 *)
 220    Section arithmetics_results.
 221
 222       Theorem succ_ini: (m,n:N) (Id N (succ m) (succ n)) -> (Id N m n).
 223       Intros.
 224       MApply '(fr_ini1 One tt tt).
 225       Qed.
 226
 227       Theorem sub_succ: (m,n:N) (LE m n) ->
 228                         (Id N (sub (succ n) m) (succ (sub n m))).
 229       Intros m.
 230       Elim m using natrec.
 231       Intros.
 232       MSimpl.
 233       Intros m' H n.
 234       MElim 'n 'natrec.
 235       MApply '(le_false m').
 236       MApply '(H n0).
 237       Qed.
 238 (*
 239 Theorem succ_pred: (n:N) (GT n zero) -> (Id N (succ (pred n)) n).
 240 Intros n.
 241 MElim 'n 'natrec.
 242 MApply '(gt_false zero).
 243 Qed.
 244 *)
 245       Theorem add_zero: (n:N) (Id N (add zero n) n).
 246       Intros.
 247       Unfold N add zero.
 248       MApply 'app_empty.
 249       Qed.
 250 (*
 251 Theorem add_ass: (l,m,n:N) (Id N (add (add l m) n) (add l (add m n))).
 252 Intros.
 253 Unfold N add.
 254 MApply 'app_ass.
 255 Qed.
 256 *)
 257       Theorem add_succ: (m,n:N) (Id N (add (succ m) n) (succ (add m n))).
 258       Intros.
 259       (MElim 'n 'natrec; Apply succ_fold). (**)
 260       MApply '(id_comp N).
 261       Qed.
 262
 263       Theorem add_comm: (m,n:N) (Id N (add m n) (add n m)).
 264       Intros m.
 265       MElim 'm 'natrec.
 266       MApply 'add_zero.
 267       MApply '(id_trans ? (succ (add n n0))).
 268       MApply 'add_succ.
 269       Apply succ_fold. (**)
 270       MApply '(id_comp N).
 271       MApply '(H n0).
 272       Qed.
 273 (*
 274 Theorem add_pred: (n,m:N) (GT n zero) -> (Id N (succ (add (pred n) m)) (add n m)).
 275 Intros n m.
 276 MElim 'm 'natrec.
 277 MApply 'succ_pred.
 278 (Apply succ_fold; Apply succ_fold). (**)
 279 MApply '(id_comp N).
 280 MApply 'H.
 281 Qed.
 282 *)
 283       Theorem le_comp_pred: (m,n:N) (LE m n) -> (LE (pred m) (pred n)).
 284       Intros m.
 285       Elim m using natrec.
 286       Intros.
 287       MApply 'le_wf.
 288       Intros m' H n.
 289       MElim 'n 'natrec.
 290       MApply '(le_false m').
 291       Qed.
 292
 293       Theorem le_add: (m,n:N) (LE m (add m n)).
 294       Intros.
 295       MElim 'n 'natrec.
 296       MApply 'le_r.
 297       MApply '(le_trans (add m n0)).
 298       Apply succ_fold. (**)
 299       MApply 'le_succ.
 300       Qed.
 301
 302       Theorem le_comp_add: (m1,m2,n:N) (LE m1 m2) -> (LE (add m1 n) (add m2 n)).
 303       Intros m1 m2 n.
 304       MElim 'n 'natrec.
 305       (Apply succ_fold; Apply succ_fold). (**)
 306       MApply 'le_comp_succ.
 307       MApply 'H.
 308       Qed.
 309
 310       Theorem le_comp_add2: (m,n1,n2:N) (LE n1 n2) -> (LE (add m n1) (add m n2)).
 311       Intros.
 312       MApply '(id_repl N (add m n1) (add n1 m)).
 313       MApply 'add_comm.
 314       MApply '(id_repl N (add m n2) (add n2 m)).
 315       MApply 'add_comm.
 316       MApply 'le_comp_add.
 317       Qed.
 318
 319       Theorem gt_comp_add2: (m,n1,n2:N) (GT n1 n2) -> (GT (add m n1) (add m n2)).
 320       Intros.
 321       MApply 'le_gt.
 322       MApply '(id_repl N (succ (add m n2)) (add m (succ n2))).
 323       MApply 'le_comp_add2.
 324       MApply 'gt_le.
 325       Qed.
 326
 327       Theorem le_comp_sub: (n,m1,m2:N) (LE m1 m2) -> (LE (sub m1 n) (sub m2 n)).
 328       Intros n.
 329       MElim 'n 'natrec.
 330       MApply '(H (pred m1) (pred m2)).
 331       MApply 'le_comp_pred.
 332       Qed.
 333
 334       Theorem gt_comp_sub: (m1,m2,n:N) (LE n m2) -> (GT m1 m2) -> (GT (sub m1 n) (sub m2 n)).
 335       Intros.
 336       MApply 'le_gt.
 337       MApply '(id_repl N (succ (sub m2 n)) (sub (succ m2) n)).
 338       MApply 'sub_succ.
 339       MApply 'le_comp_sub.
 340       MApply gt_le.
 341       Qed.
 342 (*
 343 Theorem le_zero_add: (m,n:N) (LE (add n m) zero) -> (Id N n zero).
 344 Intros.
 345 MApply 'le_zero.
 346 MApply '(le_trans (add n m)).
 347 MApply 'le_add.
 348 Qed.
 349
 350 Theorem sub_pred_l: (n,m:N) (Id N (sub (pred m) n) (pred (sub m n))).
 351 Intros.
 352 Unfold N sub pred.
 353 MApply 'lskip_tl.
 354 Qed.
 355 *)
 356       Theorem sub_zero: (n,m:N) (LE m n) -> (Id N (sub m n) zero).
 357       Intros n.
 358       Elim n using natrec.
 359       Intros.
 360       MSimpl.
 361       MApply 'le_zero.
 362       Intros n' H m.
 363       Elim m using natrec.
 364       Intros.
 365       MSimpl.
 366       MApply '(H zero).
 367       Intros m' H1 H2.
 368       MSimpl.
 369       MApply '(H m').
 370       Qed.
 371
 372       Theorem succ_pred_e: (m,n:N) (Id N m (succ n)) -> (Id N (pred m) n).
 373       Intros m.
 374       Elim m using natrec.
 375       Intros.
 376       MApply '(n_false n).
 377       Intros m' H n H2.
 378       MSimpl.
 379       MApply 'succ_ini.
 380       Qed.
 381
 382       Theorem add_sub_e: (n,m2,m1:N) (Id N m1 (add m2 n)) -> (Id N (sub m1 m2) n).
 383       Intros n.
 384       Elim n using natrec.
 385       MSimpl.
 386       Intros.
 387       MApply 'sub_zero.
 388       MApply '(id_repl N m2 m1).
 389       MApply 'le_r.
 390       Intros n' H m2.
 391       Elim m2 using natrec.
 392       Intros.
 393       MSimpl.
 394       MApply '(id_repl N (succ n') (add zero (succ n'))).
 395       MApply 'add_zero.
 396       Intros m2' H1 m1 H2.
 397       MSimpl.
 398       MApply 'pred_fold. (**)
 399       MApply '(H1 (pred m1)).
 400       Simpl in H2.
 401       Fold (succ (add (succ m2') n')) in H2. (**)
 402       MApply '(id_repl N (add m2' (succ n')) (add (succ m2') n')).
 403       MApply '(add_succ m2' n').
 404       MApply 'succ_pred_e.
 405       Qed.
 406
 407       Theorem sub_add: (m,n:N) (Id N (sub (add m n) n) m).
 408       Intros.
 409       MApply 'add_sub_e.
 410       MApply 'add_comm.
 411       Qed.
 412
 413       Theorem gt_add_di: (a,m,n:N) (GT (add m n) a) ->
 414                          (LOr (GT m a) (GT n (sub a m))).
 415       Intros.
 416       MApply '(lor_e (LE m a) (GT m a)).
 417       MCut '(GT n (sub a m)).
 418       MApply '(id_repl N n (sub (add n m) m)).
 419       MApply 'sub_add.
 420       MApply 'gt_comp_sub.
 421       MApply '(id_repl N (add n m) (add m n)).
 422       MApply 'add_comm.
 423       MApply 'in_r.
 424       MApply 'in_l.
 425       MApply 'le_di.
 426       Qed.
 427 (*
 428 Theorem app_llen: (S:Set; w,v:(List S)) (Id N (llen S (app S w v)) (add (llen S w) (llen S v))).
 429 Intros.
 430 MElim 'v 'listrec.
 431 Apply succ_fold. (**)
 432 MApply '(id_comp N).
 433 Qed.
 434
 435 Theorem bsapp_llen: (S:Set; vs:N->(List S); n:N) (Id N (llen S (bs_app S vs n)) (bs_add [n](llen S (vs n)) n)).
 436 Intros.
 437 MElim 'n 'natrec.
 438 MApply '(id_repl ? (bs_add [n:N](llen S (vs n)) n0) (llen S (bs_app S vs n0))).
 439 MApply 'app_llen.
 440 Qed.
 441
 442 Theorem rbsapp_llen: (S:Set; vs:N->(List S); n:N) (Id N (llen S (rbs_app S vs n)) (rbs_add [n](llen S (vs n)) n)).
 443 Intros.
 444 Unfold rbs_add rbs_app rbs_iter.
 445 Apply bs_app_fold.
 446 Apply bs_app_fold.
 447 Apply bs_add_fold. (**)
 448 MApply 'bsapp_llen.
 449 Qed.
 450
 451 Theorem lskip_llen: (S:Set; v:(List S); n:N) (Id N (llen S (lskip S n v)) (sub (llen S v) n)).
 452 Intros.
 453 MElim 'n 'natrec.
 454 Fold (pred (llen S v)). (**)
 455 MApply '(id_trans ? (pred (llen S (lskip S n0 v)))).
 456 MApply '(id_repl ? (lskip S n0 (tl S v)) (tl S (lskip S n0 v))).
 457 (MApply 'id_comm; MApply 'lskip_tl).
 458 MApply 'tl_len.
 459 MApply '(id_trans ? (pred (sub (llen S v) n0))).
 460 MApply '(id_comp N).
 461 (MApply 'id_comm; MApply 'sub_pred_l).
 462 Qed.
 463
 464 Theorem lskip_le: (S:Set; v:(List S); n:N) (LE (llen S v) n) -> (Id N (llen S (lskip S n v)) zero).
 465 Intros.
 466 MApply '(id_trans ? (sub (llen S v) n)).
 467 MApply 'lskip_llen.
 468 MApply 'sub_zero.
 469 Qed.
 470
 471 Theorem lslice_succ_r: (S:Set; v:(List S); k,n:N) (Id (List S) (lslice S k (succ n) v) (app S (lslice S (succ k) n v) (lix S k v))).
 472 Intros.
 473 (Unfold lslice lix; MSimpl).
 474 MApply '(id_repl ? (tl S (lskip S k v)) (lskip S k (tl S v))).
 475 MApply 'lskip_tl.
 476 Qed.
 477
 478 Theorem lslice_succ_l: (S:Set; v:(List S); n,k:N) (Id (List S) (lslice S k (succ n) v) (app S (lix S (add k n) v) (lslice S k n v))).
 479 Intros S v n.
 480 MElim 'n 'natrec.
 481 MApply 'lslice_lix.
 482 MApply '(id_repl ? (succ (add k n0)) (add (succ k) n0)).
 483 MApply 'add_succ.
 484 MApply '(id_repl ? (lslice S k (succ n0) v) (app S (lslice S (succ k) n0 v) (lix S k v))).
 485 (MApply 'id_comm; MApply 'lslice_succ_r).
 486 MApply '(id_repl ? (lslice S k (succ (succ n0)) v) (app S (lslice S (succ k) (succ n0) v) (lix S k v))).
 487 (MApply 'id_comm; MApply 'lslice_succ_r).
 488 MApply '(id_trans (List S) (app S (app S (lix S (add (succ k) n0) v) (lslice S (succ k) n0 v)) (lix S k v))).
 489 MApply '(id_comp (List S) (List S) [u:?](app S u (lix S k v))).
 490 MApply '(H (succ k)).
 491 Apply succ_fold. (**)
 492 MApply '(id_repl N (succ (add k n0)) (add (succ k) n0)).
 493 MApply 'add_succ.
 494 MApply 'app_ass.
 495 Qed.
 496
 497 Theorem lslice_add: (S:Set; v:(List S); k,m,n:N) (Id (List S) (lslice S k (add m n) v) (app S (lslice S (add k m) n v) (lslice S k m v))).
 498 Intros.
 499 MElim 'n 'natrec.
 500 MApply '(id_repl ? (lslice S (add k m) zero v) (empty S)).
 501 (MApply 'id_comm; MApply 'app_empty).
 502 MApply '(id_trans ? (app S (lix S (add k (add m n0)) v) (lslice S k (add m n0) v))).
 503 Apply succ_fold. (**)
 504 MApply 'lslice_succ_l.
 505 MApply '(id_repl ? (lslice S (add k m) (succ n0) v) (app S (lix S (add (add k m) n0) v) (lslice S (add k m) n0 v))).
 506 (MApply 'id_comm; MApply 'lslice_succ_l).
 507 MApply '(id_trans ? (app S (lix S (add (add k m) n0) v) (app S (lslice S (add k m) n0 v) (lslice S k m v)))).
 508 MApply '(id_repl ? (add k (add m n0)) (add (add k m) n0)).
 509 MApply 'add_ass.
 510 MApply '(id_comp (List S) (List S) [w](app S (lix S (add (add k m) n0) v) w)).
 511 (MApply 'id_comm; MApply 'app_ass).
 512 Qed.
 513
 514 Theorem lslice_bsadd: (S:Set; v:(List S); k:N; ms:NS; n:N) (Id (List S) (lslice S k (bs_add ms n) v) (bs_app S [m](lslice S (add k (bs_add ms m)) (ms m) v) n)).
 515 Intros.
 516 (MElim 'n 'natrec; Fold (add (ms n0) (bs_add ms n0))).
 517 MApply '(id_repl ? (bs_app S [m:N](lslice S (add k (bs_add ms m)) (ms m) v) n0) (lslice S k (bs_add ms n0) v)).
 518 MApply '(id_repl ? (add (ms n0) (bs_add ms n0)) (add (bs_add ms n0) (ms n0))).
 519 MApply 'add_comm.
 520 MApply 'lslice_add.
 521 Qed.
 522
 523 Theorem lslice_rbsadd: (S:Set; v:(List S); k:N; ms:NS; n:N) (Id (List S) (lslice S k (rbs_add ms n) v) (rbs_app S [m](lslice S (add k (bs_add ms m)) (ms m) v) n)).
 524 Intros.
 525 Unfold rbs_add rbs_app rbs_iter.
 526 Apply bs_app_fold.
 527 Apply bs_app_fold.
 528 Apply bs_add_fold. (**)
 529 MApply 'lslice_bsadd.
 530 Qed.
 531 *)
 532 End arithmetics_results.
 533
 534 End Arith_Results.