aboutsummaryrefslogtreecommitdiff
path: root/src/BaseSystemProofs.v
blob: 1c2fe0fbe088ce06896ab0abfd9c6813751e81ef (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
Require Import Coq.Lists.List Coq.micromega.Psatz.
Require Import Crypto.Util.ListUtil Crypto.Util.CaseUtil Crypto.Util.ZUtil.
Require Import Coq.ZArith.ZArith Coq.ZArith.Zdiv.
Require Import Coq.omega.Omega Coq.Numbers.Natural.Peano.NPeano Coq.Arith.Arith.
Require Import Crypto.BaseSystem.
Require Import Crypto.Util.Notations.
Import Morphisms.
Local Open Scope Z.

Local Infix ".+" := add.

Local Hint Extern 1 (@eq Z _ _) => ring.

Section BaseSystemProofs.
  Context `(base_vector : BaseVector).

  Lemma decode'_truncate : forall bs us, decode' bs us = decode' bs (firstn (length bs) us).
  Proof.
    unfold decode'; intros; f_equal; apply combine_truncate_l.
  Qed.

  Lemma decode'_splice : forall xs ys bs,
    decode' bs (xs ++ ys) =
    decode' (firstn (length xs) bs) xs + decode'  (skipn (length xs) bs) ys.
  Proof.
    unfold decode'.
    induction xs; destruct ys, bs; boring.
    + rewrite combine_truncate_r.
      do 2 rewrite Z.add_0_r; auto.
    + unfold accumulate.
      apply Z.add_assoc.
  Qed.

  Lemma add_rep : forall bs us vs, decode' bs (add us vs) = decode' bs us + decode' bs vs.
  Proof.
    unfold decode', accumulate; induction bs; destruct us, vs; boring; ring.
  Qed.

  Lemma decode_nil : forall bs, decode' bs nil = 0.
    auto.
  Qed.
  Hint Rewrite decode_nil.

  Lemma decode_base_nil : forall us, decode' nil us = 0.
  Proof.
    intros; rewrite decode'_truncate; auto.
  Qed.

  Hint Rewrite decode_base_nil.

  Lemma mul_each_rep : forall bs u vs,
    decode' bs (mul_each u vs) = u * decode' bs vs.
  Proof.
    unfold decode', accumulate; induction bs; destruct vs; boring; ring.
  Qed.

  Lemma base_eq_1cons: base = 1 :: skipn 1 base.
  Proof.
    pose proof (b0_1 0) as H.
    destruct base; compute in H; try discriminate; boring.
  Qed.

  Lemma decode'_cons : forall x1 x2 xs1 xs2,
    decode' (x1 :: xs1) (x2 :: xs2) = x1 * x2 + decode' xs1 xs2.
  Proof.
    unfold decode', accumulate; boring; ring.
  Qed.
  Hint Rewrite decode'_cons.

  Lemma decode_cons : forall x us,
    decode base (x :: us) = x + decode base (0 :: us).
  Proof.
    unfold decode; intros.
    rewrite base_eq_1cons.
    autorewrite with core; ring_simplify; auto.
  Qed.

  Lemma decode'_map_mul : forall v xs bs,
    decode' (map (Z.mul v) bs) xs =
    Z.mul v (decode' bs xs).
  Proof.
    unfold decode'.
    induction xs; destruct bs; boring.
    unfold accumulate; simpl; nia.
  Qed.

  Lemma decode_map_mul : forall v xs,
    decode (map (Z.mul v) base) xs =
    Z.mul v (decode base xs).
  Proof.
    unfold decode; intros; apply decode'_map_mul.
  Qed.

  Lemma sub_rep : forall bs us vs, decode' bs (sub us vs) = decode' bs us - decode' bs vs.
  Proof.
    induction bs; destruct us; destruct vs; boring; ring.
  Qed.

  Lemma nth_default_base_nonzero : forall d, d <> 0 ->
    forall i, nth_default d base i <> 0.
  Proof.
    intros.
    rewrite nth_default_eq.
    destruct (nth_in_or_default i base d).
    + auto using Z.positive_is_nonzero, base_positive.
    + congruence.
  Qed.

  Lemma nth_default_base_pos : forall d, 0 < d ->
    forall i,  0 < nth_default d base i.
  Proof.
    intros.
    rewrite nth_default_eq.
    destruct (nth_in_or_default i base d).
    + apply Z.gt_lt; auto using base_positive.
    + congruence.
  Qed.

  Lemma mul_each_base : forall us bs c,
      decode' bs (mul_each c us) = decode' (mul_each c bs) us.
  Proof.
    induction us; destruct bs; boring; ring.
  Qed.

  Hint Rewrite (@nth_default_nil Z).
  Hint Rewrite (@firstn_nil Z).
  Hint Rewrite (@skipn_nil Z).

  Lemma base_app : forall us low high,
      decode' (low ++ high) us = decode' low (firstn (length low) us) + decode' high (skipn (length low) us).
  Proof.
    induction us; destruct low; boring.
  Qed.

  Lemma base_mul_app : forall low c us,
      decode' (low ++ mul_each c low) us = decode' low (firstn (length low) us) +
      c * decode' low (skipn (length low) us).
  Proof.
    intros.
    rewrite base_app; f_equal.
    rewrite <- mul_each_rep.
    rewrite mul_each_base.
    reflexivity.
  Qed.

  Lemma zeros_rep : forall bs n, decode' bs (zeros n) = 0.
    induction bs; destruct n; boring.
  Qed.
  Lemma length_zeros : forall n, length (zeros n) = n.
    induction n; boring.
  Qed.
  Hint Rewrite length_zeros.

  Lemma app_zeros_zeros : forall n m, zeros n ++ zeros m = zeros (n + m)%nat.
  Proof.
    induction n; boring.
  Qed.
  Hint Rewrite app_zeros_zeros.

  Lemma zeros_app0 : forall m, zeros m ++ 0 :: nil = zeros (S m).
  Proof.
    induction m; boring.
  Qed.
  Hint Rewrite zeros_app0.

  Lemma nth_default_zeros : forall n i, nth_default 0 (BaseSystem.zeros n) i = 0.
  Proof.
    induction n; intros; [ cbv [BaseSystem.zeros]; apply nth_default_nil | ].
    rewrite <-zeros_app0, nth_default_app.
    rewrite length_zeros.
    destruct (lt_dec i n); auto.
    destruct (eq_nat_dec i n); subst.
    + rewrite Nat.sub_diag; apply nth_default_cons.
    + apply nth_default_out_of_bounds.
      cbv [length]; omega.
  Qed.

  Lemma rev_zeros : forall n, rev (zeros n) = zeros n.
  Proof.
    induction n; boring.
  Qed.
  Hint Rewrite rev_zeros.

  Hint Unfold nth_default.

  Lemma decode_single : forall n bs x,
    decode' bs (zeros n ++ x :: nil) = nth_default 0 bs n * x.
  Proof.
    induction n; destruct bs; boring.
  Qed.
  Hint Rewrite decode_single.

  Lemma peel_decode : forall xs ys x y, decode' (x::xs) (y::ys) = x*y + decode' xs ys.
  Proof.
    boring.
  Qed.
  Hint Rewrite zeros_rep peel_decode.

  Lemma decode_Proper : Proper (Logic.eq ==> (Forall2 Logic.eq) ==> Logic.eq) decode'.
  Proof.
    repeat intro; subst.
    revert y y0 H0; induction x0; intros.
    + inversion H0. rewrite !decode_nil.
      reflexivity.
    + inversion H0; subst.
      destruct y as [|y0 y]; [rewrite !decode_base_nil; reflexivity | ].
      specialize (IHx0 y _ H4).
      rewrite !peel_decode.
      f_equal; auto.
  Qed.

  Lemma decode_highzeros : forall xs bs n, decode' bs (xs ++ zeros n) = decode' bs xs.
  Proof.
    induction xs; destruct bs; boring.
  Qed.

  Lemma mul_bi'_zeros : forall n m, mul_bi' base n (zeros m) = zeros m.
    induction m; boring.
  Qed.
  Hint Rewrite mul_bi'_zeros.

  Lemma nth_error_base_nonzero : forall n x,
    nth_error base n = Some x -> x <> 0.
  Proof.
    eauto using (@nth_error_value_In Z), Z.gt0_neq0, base_positive.
  Qed.

  Hint Rewrite plus_0_r.

  Lemma mul_bi_single : forall m n x,
    (n + m < length base)%nat ->
    decode base (mul_bi base n (zeros m ++ x :: nil)) = nth_default 0 base m * x * nth_default 0 base n.
  Proof.
    unfold mul_bi, decode.
    destruct m; simpl; simpl_list; simpl; intros. {
      pose proof nth_error_base_nonzero as nth_nonzero.
      case_eq base; [intros; boring | intros z l base_eq].
      specialize (b0_1 0); intro b0_1'.
      rewrite base_eq in *.
      rewrite nth_default_cons in b0_1'.
      rewrite b0_1' in *.
      unfold crosscoef.
      autounfold; autorewrite with core.
      unfold nth_default.
      nth_tac.
      rewrite Z.mul_1_r.
      rewrite Z_div_same_full.
      destruct x; ring.
      eapply nth_nonzero; eauto.
    } {
      ssimpl_list.
      autorewrite with core.
      rewrite app_assoc.
      autorewrite with core.
      unfold crosscoef; simpl; ring_simplify.
      rewrite Nat.add_1_r.
      rewrite base_good by auto.
      rewrite Z_div_mult by (apply base_positive; rewrite nth_default_eq; apply nth_In; auto).
      rewrite <- Z.mul_assoc.
      rewrite <- Z.mul_comm.
      rewrite <- Z.mul_assoc.
      rewrite <- Z.mul_assoc.
      destruct (Z.eq_dec x 0); subst; try ring.
      rewrite Z.mul_cancel_l by auto.
      rewrite <- base_good by auto.
      ring.
      }
  Qed.

  Lemma set_higher' : forall vs x, vs++x::nil = vs .+ (zeros (length vs) ++ x :: nil).
    induction vs; boring; f_equal; ring.
  Qed.

  Lemma set_higher : forall bs vs x,
    decode' bs (vs++x::nil) = decode' bs vs + nth_default 0 bs (length vs) * x.
  Proof.
    intros.
    rewrite set_higher'.
    rewrite add_rep.
    f_equal.
    apply decode_single.
  Qed.

  Lemma zeros_plus_zeros : forall n, zeros n = zeros n .+ zeros n.
    induction n; auto.
    simpl; f_equal; auto.
  Qed.

  Lemma mul_bi'_n_nil : forall n, mul_bi' base n nil = nil.
  Proof.
    unfold mul_bi; auto.
  Qed.
  Hint Rewrite mul_bi'_n_nil.

  Lemma add_nil_l : forall us, nil .+ us = us.
    induction us; auto.
  Qed.
  Hint Rewrite add_nil_l.

  Lemma add_nil_r : forall us, us .+ nil = us.
    induction us; auto.
  Qed.
  Hint Rewrite add_nil_r.

  Lemma add_first_terms : forall us vs a b,
    (a :: us) .+ (b :: vs) = (a + b) :: (us .+ vs).
    auto.
  Qed.
  Hint Rewrite add_first_terms.

  Lemma mul_bi'_cons : forall n x us,
    mul_bi' base n (x :: us) = x * crosscoef base n (length us) :: mul_bi' base n us.
  Proof.
    unfold mul_bi'; auto.
  Qed.

  Lemma add_same_length : forall us vs l, (length us = l) -> (length vs = l) ->
    length (us .+ vs) = l.
  Proof.
    induction us, vs; boring.
    erewrite (IHus vs (pred l)); boring.
  Qed.

  Hint Rewrite app_nil_l.
  Hint Rewrite app_nil_r.

  Lemma add_snoc_same_length : forall l us vs a b,
    (length us = l) -> (length vs = l) ->
    (us ++ a :: nil) .+ (vs ++ b :: nil) = (us .+ vs) ++ (a + b) :: nil.
  Proof.
    induction l, us, vs; boring; discriminate.
  Qed.

  Lemma mul_bi'_add : forall us n vs l
    (Hlus: length us = l)
    (Hlvs: length vs = l),
    mul_bi' base n (rev (us .+ vs)) =
    mul_bi' base n (rev us) .+ mul_bi' base n (rev vs).
  Proof.
    (* TODO(adamc): please help prettify this *)
    induction us using rev_ind;
      try solve [destruct vs; boring; congruence].
    destruct vs using rev_ind; boring; clear IHvs; simpl_list.
    erewrite (add_snoc_same_length (pred l) us vs _ _); simpl_list.
    repeat rewrite mul_bi'_cons; rewrite add_first_terms; simpl_list.
    rewrite (IHus n vs (pred l)).
    replace (length us) with (pred l).
    replace (length vs) with (pred l).
    rewrite (add_same_length us vs (pred l)).
    f_equal; ring.

    erewrite length_snoc; eauto.
    erewrite length_snoc; eauto.
    erewrite length_snoc; eauto.
    erewrite length_snoc; eauto.
    erewrite length_snoc; eauto.
    erewrite length_snoc; eauto.
    erewrite length_snoc; eauto.
    erewrite length_snoc; eauto.
   Qed.

  Lemma zeros_cons0 : forall n, 0 :: zeros n = zeros (S n).
    auto.
  Qed.

  Lemma add_leading_zeros : forall n us vs,
    (zeros n ++ us) .+ (zeros n ++ vs) = zeros n ++ (us .+ vs).
  Proof.
    induction n; boring.
  Qed.

  Lemma rev_add_rev : forall us vs l, (length us = l) -> (length vs = l) ->
    (rev us) .+ (rev vs) = rev (us .+ vs).
  Proof.
    induction us, vs; boring; try solve [subst; discriminate].
    rewrite (add_snoc_same_length (pred l) _ _ _ _) by (subst; simpl_list; omega).
    rewrite (IHus vs (pred l)) by omega; auto.
  Qed.
  Hint Rewrite rev_add_rev.

  Lemma mul_bi'_length : forall us n, length (mul_bi' base n us) = length us.
  Proof.
    induction us, n; boring.
  Qed.
  Hint Rewrite mul_bi'_length.

  Lemma add_comm : forall us vs, us .+ vs = vs .+ us.
  Proof.
    induction us, vs; boring; f_equal; auto.
  Qed.

  Hint Rewrite rev_length.

  Lemma mul_bi_add_same_length : forall n us vs l,
    (length us = l) -> (length vs = l) ->
    mul_bi base n (us .+ vs) = mul_bi base n us .+ mul_bi base n vs.
  Proof.
    unfold mul_bi; boring.
    rewrite add_leading_zeros.
    erewrite mul_bi'_add; boring.
    erewrite rev_add_rev; boring.
  Qed.

  Lemma add_zeros_same_length : forall us, us .+ (zeros (length us)) = us.
  Proof.
    induction us; boring; f_equal; omega.
  Qed.

  Hint Rewrite add_zeros_same_length.
  Hint Rewrite minus_diag.

  Lemma add_trailing_zeros : forall us vs, (length us >= length vs)%nat ->
    us .+ vs = us .+ (vs ++ (zeros (length us - length vs)%nat)).
  Proof.
    induction us, vs; boring; f_equal; boring.
  Qed.

  Lemma length_add_ge : forall us vs, (length us >= length vs)%nat ->
    (length (us .+ vs) <= length us)%nat.
  Proof.
    intros.
    rewrite add_trailing_zeros by trivial.
    erewrite add_same_length by (pose proof app_length; boring); omega.
  Qed.

  Lemma add_length_le_max : forall us vs,
      (length (us .+ vs) <= max (length us) (length vs))%nat.
  Proof.
    intros; case_max; (rewrite add_comm; apply length_add_ge; omega) ||
                                        (apply length_add_ge; omega) .
  Qed.

  Lemma sub_nil_length: forall us : digits, length (sub nil us) = length us.
  Proof.
     induction us; boring.
  Qed.

  Lemma sub_length : forall us vs,
      (length (sub us vs) = max (length us) (length vs))%nat.
  Proof.
    induction us, vs; boring.
    rewrite sub_nil_length; auto.
  Qed.

  Lemma mul_bi_length : forall us n, length (mul_bi base n us) = (length us + n)%nat.
  Proof.
    pose proof mul_bi'_length; unfold mul_bi.
    destruct us; repeat progress (simpl_list; boring).
  Qed.
  Hint Rewrite mul_bi_length.

  Lemma mul_bi_trailing_zeros : forall m n us,
    mul_bi base n us ++ zeros m = mul_bi base n (us ++ zeros m).
  Proof.
    unfold mul_bi.
    induction m; intros; try solve [boring].
    rewrite <- zeros_app0.
    rewrite app_assoc.
    repeat progress (boring; rewrite rev_app_distr).
  Qed.

  Lemma mul_bi_add_longer : forall n us vs,
    (length us >= length vs)%nat ->
    mul_bi base n (us .+ vs) = mul_bi base n us .+ mul_bi base n vs.
  Proof.
    boring.
    rewrite add_trailing_zeros by auto.
    rewrite (add_trailing_zeros (mul_bi base n us) (mul_bi base n vs))
      by (repeat (rewrite mul_bi_length); omega).
    erewrite mul_bi_add_same_length by
      (eauto; simpl_list; rewrite length_zeros; omega).
    rewrite mul_bi_trailing_zeros.
    repeat (f_equal; boring).
  Qed.

  Lemma mul_bi_add : forall n us vs,
    mul_bi base n (us .+ vs) = (mul_bi base n  us) .+ (mul_bi base n vs).
  Proof.
    intros; pose proof mul_bi_add_longer.
    destruct (le_ge_dec (length us) (length vs)). {
      rewrite add_comm.
      rewrite (add_comm (mul_bi base n us)).
      boring.
    } {
      boring.
    }
  Qed.

  Lemma mul_bi_rep : forall i vs,
    (i + length vs < length base)%nat ->
    decode base (mul_bi base i vs) = decode base vs * nth_default 0 base i.
  Proof.
    unfold decode.
    induction vs using rev_ind; intros; try solve [unfold mul_bi; boring].
    assert (i + length vs < length base)%nat by
      (rewrite app_length in *; boring).

    rewrite set_higher.
    ring_simplify.
    rewrite <- IHvs by auto; clear IHvs.
    rewrite <- mul_bi_single by auto.
    rewrite <- add_rep.
    rewrite <- mul_bi_add.
    rewrite set_higher'.
    auto.
  Qed.

  Local Notation mul' := (mul' base).
  Local Notation mul := (mul base).

  Lemma mul'_rep : forall us vs,
    (length us + length vs <= length base)%nat ->
    decode base (mul' (rev us) vs) = decode base us * decode base vs.
  Proof.
    unfold decode.
    induction us using rev_ind; boring.

    assert (length us + length vs < length base)%nat by
      (rewrite app_length in *; boring).

    ssimpl_list.
    rewrite add_rep.
    boring.
    rewrite set_higher.
    rewrite mul_each_rep.
    rewrite mul_bi_rep by auto.
    unfold decode; ring.
  Qed.

  Lemma mul_rep : forall us vs,
    (length us + length vs <= length base)%nat ->
    decode base (mul us vs) = decode base us * decode base vs.
  Proof.
    exact mul'_rep.
  Qed.

  Lemma mul'_length: forall us vs,
      (length (mul' us vs) <= length us + length vs)%nat.
  Proof.
    pose proof add_length_le_max.
    induction us; boring.
    unfold mul_each.
    simpl_list; case_max; boring; omega.
  Qed.

  Lemma mul_length: forall us vs,
      (length (mul us vs) <= length us + length vs)%nat.
  Proof.
    intros; unfold BaseSystem.mul.
    rewrite mul'_length.
    rewrite rev_length; omega.
  Qed.

  Lemma add_length_exact : forall us vs,
      length (us .+ vs) = max (length us) (length vs).
  Proof.
    induction us; destruct vs; boring.
  Qed.

  Hint Rewrite add_length_exact : distr_length.

  Lemma mul'_length_exact_full: forall us vs,
      (length (mul' us vs) = match length us with
                             | 0 => 0%nat
                             | _ => pred (length us + length vs)
                             end)%nat.
  Proof.
    induction us; intros; try solve [boring].
    unfold BaseSystem.mul'; fold mul'.
    unfold mul_each.
    rewrite add_length_exact, map_length, mul_bi_length, length_cons.
    destruct us.
    + rewrite Max.max_0_r. simpl; omega.
    + rewrite Max.max_l; [ omega | ].
      rewrite IHus by ( congruence || simpl in *; omega).
      simpl; omega.
  Qed.

  Hint Rewrite mul'_length_exact_full : distr_length.

  (* TODO(@jadephilipoom, from jgross): one of these conditions isn't
  needed.  Should it be dropped, or was there a reason to keep it? *)
  Lemma mul'_length_exact: forall us vs,
      (length us <= length vs)%nat -> us <> nil ->
      (length (mul' us vs) = pred (length us + length vs))%nat.
  Proof.
    intros; rewrite mul'_length_exact_full; destruct us; simpl; congruence.
  Qed.

  Lemma mul_length_exact_full: forall us vs,
      (length (mul us vs) = match length us with
                            | 0 => 0
                            | _ => pred (length us + length vs)
                            end)%nat.
  Proof.
    intros; unfold BaseSystem.mul; autorewrite with distr_length; reflexivity.
  Qed.

  Hint Rewrite mul_length_exact_full : distr_length.

  (* TODO(@jadephilipoom, from jgross): one of these conditions isn't
  needed.  Should it be dropped, or was there a reason to keep it? *)
  Lemma mul_length_exact: forall us vs,
      (length us <= length vs)%nat -> us <> nil ->
      (length (mul us vs) = pred (length us + length vs))%nat.
  Proof.
    intros; unfold BaseSystem.mul.
    rewrite mul'_length_exact; rewrite ?rev_length; try omega.
    intro rev_nil.
    match goal with H : us <> nil |- _ => apply H end.
    apply length0_nil; rewrite <-rev_length, rev_nil.
    reflexivity.
  Qed.
  Definition encode'_zero z max  : encode' base z max 0%nat = nil := eq_refl.
  Definition encode'_succ z max i : encode' base z max (S i) =
    encode' base z max i ++ ((z mod (nth_default max base (S i))) / (nth_default max base i)) :: nil := eq_refl.
  Opaque encode'.
  Hint Resolve encode'_zero encode'_succ.

  Lemma encode'_length : forall z max i, length (encode' base z max i) = i.
  Proof.
    induction i; auto.
    rewrite encode'_succ, app_length, IHi.
    cbv [length].
    omega.
  Qed.

  (* States that each element of the base is a positive integer multiple of the previous
     element, and that max is a positive integer multiple of the last element. Ideally this
     would have a better name. *)
  Definition base_max_succ_divide max := forall i, (S i <= length base)%nat ->
    Z.divide (nth_default max base i) (nth_default max base (S i)).

  Lemma encode'_spec : forall z max, 0 < max ->
    base_max_succ_divide max -> forall i, (i <= length base)%nat ->
    decode' base (encode' base z max i) = z mod (nth_default max base i).
  Proof.
    induction i; intros.
    + rewrite encode'_zero, b0_1, Z.mod_1_r.
      apply decode_nil.
    + rewrite encode'_succ, set_higher.
      rewrite IHi by omega.
      rewrite encode'_length, (Z.add_comm (z mod nth_default max base i)).
      replace (nth_default 0 base i) with (nth_default max base i) by
        (rewrite !nth_default_eq; apply nth_indep; omega).
      match goal with H1 : base_max_succ_divide _, H2 : (S i <= length base)%nat, H3 : 0 < max |- _ =>
        specialize (H1 i H2);
        rewrite (Znumtheory.Zmod_div_mod _ _ _ (nth_default_base_pos _ H _)
                                               (nth_default_base_pos _ H _) H0) end.
      rewrite <-Z.div_mod by (apply Z.positive_is_nonzero, Z.lt_gt; auto using nth_default_base_pos).
      reflexivity.
  Qed.

  Lemma encode_rep : forall z max, 0 <= z < max ->
    base_max_succ_divide max -> decode base (encode base z max) = z.
  Proof.
    unfold encode; intros.
    rewrite encode'_spec, nth_default_out_of_bounds by (omega || auto).
    apply Z.mod_small; omega.
  Qed.

End BaseSystemProofs.

Hint Rewrite @add_length_exact @mul'_length_exact_full @mul_length_exact_full @encode'_length @sub_length : distr_length.

Section MultiBaseSystemProofs.
  Context base0 (base_vector0 : @BaseVector base0) base1 (base_vector1 : @BaseVector base1).

  Lemma decode_short_initial : forall (us : digits),
      (firstn (length us) base0 = firstn (length us) base1)
      -> decode base0 us = decode base1 us.
  Proof.
    intros us H.
    unfold decode, decode'.
    rewrite (combine_truncate_r us base0), (combine_truncate_r us base1), H.
    reflexivity.
  Qed.

  Lemma mul_rep_two_base : forall (us vs : digits),
      (length us + length vs <= length base1)%nat
      -> firstn (length us) base0 = firstn (length us) base1
      -> firstn (length vs) base0 = firstn (length vs) base1
      -> (decode base0 us) * (decode base0 vs) = decode base1 (mul base1 us vs).
  Proof.
      intros.
      rewrite mul_rep by trivial.
      apply f_equal2; apply decode_short_initial; assumption.
  Qed.

End MultiBaseSystemProofs.