-
Notifications
You must be signed in to change notification settings - Fork 7
/
Copy pathproperties.v
2100 lines (1810 loc) · 68.9 KB
/
properties.v
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
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
(*===========================================================================
Proofs of properties of arithmetic and logical operations on n-bit words
===========================================================================*)
From HB Require Import structures.
Require Import mathcomp.ssreflect.ssreflect.
From mathcomp Require Import ssrfun ssrbool eqtype ssrnat seq fintype tuple zmodp div.
Require Import ssrextra.tuple ssrextra.nat.
Require Import spec spec.properties operations.
Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.
(*---------------------------------------------------------------------------
Casting properties
---------------------------------------------------------------------------*)
Lemma nat_cast_ord:
forall n m (H: n = m) (i: 'I_n), nat_of_ord (cast_ord H i) = i.
Proof.
move=> n m H i.
by case: m / H.
Qed.
Lemma toNat_tcast:
forall n m (bs: BITS n)(H: n = m), toNat (tcast H bs) = toNat bs.
Proof.
move=> n m bs H.
by case: m / H.
Qed.
Lemma getBit_tcast:
forall n m (bs: BITS n)(H: n = m), getBit (tcast H bs) = getBit bs.
Proof.
move=> n m bs H.
by case: m / H.
Qed.
(*---------------------------------------------------------------------------
Properties of bitwise logical operations
---------------------------------------------------------------------------*)
Lemma liftUnOpCons n op b (p: BITS n) :
liftUnOp op (consB b p) = consB (op b) (liftUnOp op p).
Proof. by apply: eq_from_tnth=> i; rewrite !(tnth_nth (op b)). Qed.
Lemma liftBinOpCons n op b1 b2 (p1 p2: BITS n) :
liftBinOp op (consB b1 p1) (consB b2 p2)
= consB (op b1 b2) (liftBinOp op p1 p2).
Proof. by apply: eq_from_tnth=> i; rewrite !(tnth_nth (op b1 b2)). Qed.
Lemma getBit_liftBinOp:
forall n op (bs: BITS n)(bs': BITS n) k, k < n ->
getBit (liftBinOp op bs bs') k = op (getBit bs k) (getBit bs' k).
Proof.
elim=> // n IHn op /tupleP[b bs] /tupleP[b' bs'];
case=> [|k] ?.
+ (* k ~ 0 *)
have ->: getBit (liftBinOp op [tuple of b :: bs] [tuple of b' :: bs']) 0 = op b b'
by compute.
by trivial.
+ (* k ~ k + 1 *)
have ->: getBit [tuple of b :: bs] k.+1 = getBit bs k by compute.
have ->: getBit [tuple of b' :: bs'] k.+1 = getBit bs' k by compute.
have ->: getBit (liftBinOp op [tuple of b :: bs] [tuple of b' :: bs']) k.+1 = getBit (liftBinOp op bs bs') k
by compute.
by apply IHn.
Qed.
Lemma getBit_liftUnOp:
forall n op (bs : BITS n) k, k < n -> getBit (liftUnOp op bs) k = op (getBit bs k).
Proof.
elim=> // n IHn op /tupleP[b bs];
case=> // k le_k.
+ (* k ~ k + 1 *)
rewrite liftUnOpCons.
have ->: getBit [tuple of b :: bs] k.+1 = getBit bs k
by compute.
have ->: getBit (consB (op b) (liftUnOp op bs)) k.+1 = getBit (liftUnOp op bs) k
by compute.
by apply IHn; apply le_k.
Qed.
(** Do something with every hypothesis. *)
Local Ltac do_with_hyp' tac :=
match goal with
| [ H : _ |- _ ] => tac H
end.
(** Revert all hypotheses *)
Local Ltac reverse := repeat do_with_hyp' ltac:(fun H => revert H).
(** We should probably make a general lemma about [liftBinOp] equality... *)
Local Ltac lift_op_t n :=
(** first do induction, and take care of the base case with trivialBits *)
(move => *; induction n; first (by do ?move => ?; apply trivialBits));
(** destruct all of the tuples as we introduce them *)
reverse;
(do ![case/tupleP | case/(@id bool) | move => ?]);
(** unfold the lifting, and rewrite with the relevant lemmas, repeatedly *)
do !rewrite /liftBinOp/liftUnOp/copy/ones/zero ?nseqCons ?zipCons ?mapCons;
(** unfold the lifting, and rewrite with any hypothesis at most once. *)
unfold liftBinOp, liftUnOp in *;
try by do !do_with_hyp' ltac:(fun H => rewrite H; clear H).
Lemma lift_associative op n : associative op -> associative (liftBinOp (n:=n) op).
Proof. by lift_op_t n. Qed.
Lemma lift_left_id n id op : left_id id op ->
left_id (copy n id) (liftBinOp (n:=n) op).
Proof. by lift_op_t n. Qed.
Lemma lift_right_id n : forall id op, right_id id op ->
right_id (copy n id) (liftBinOp (n:=n) op).
Proof. by lift_op_t n. Qed.
Lemma lift_left_zero n zero op : left_zero zero op ->
left_zero (copy n zero) (liftBinOp (n:=n) op).
Proof. by lift_op_t n. Qed.
Lemma lift_right_zero n : forall zero op, right_zero zero op ->
right_zero (copy n zero) (liftBinOp (n:=n) op).
Proof. by lift_op_t n. Qed.
Lemma lift_commutative n : forall op, commutative op -> commutative (liftBinOp (n:=n) op).
Proof. by lift_op_t n. Qed.
Lemma lift_idempotent n : forall op, idempotent op -> idempotent (liftBinOp (n:=n) op).
Proof. by lift_op_t n. Qed.
Lemma xorBC n : commutative (xorB (n:=n)).
Proof. by apply lift_commutative; do !elim. Qed.
Lemma andBC n : commutative (andB (n:=n)).
Proof. by apply lift_commutative; do !elim. Qed.
Lemma andBB n : idempotent (andB (n:=n)).
Proof. by apply lift_idempotent; do !elim. Qed.
Lemma orBC n : commutative (orB (n:=n)).
Proof. by apply lift_commutative; do !elim. Qed.
Lemma orBB n : idempotent (orB (n:=n)).
Proof. by apply lift_idempotent; do !elim. Qed.
Lemma xorBA n : associative (xorB (n:=n)).
Proof. by apply lift_associative; do !elim. Qed.
Lemma andBA n : associative (andB (n:=n)).
Proof. by apply lift_associative; do !elim. Qed.
Lemma and1B n : left_id (ones _) (andB (n:=n)).
Proof. by apply lift_left_id; do !elim. Qed.
Lemma andB1 n : right_id (ones _) (andB (n:=n)).
Proof. by apply lift_right_id; do !elim. Qed.
Lemma orBA n : associative (orB (n:=n)).
Proof. by apply lift_associative; do !elim. Qed.
Lemma or0B n : left_id #0 (orB (n:=n)).
Proof. by rewrite fromNat0; apply lift_left_id; do !elim. Qed.
Lemma orB0 n : right_id #0 (orB (n:=n)).
Proof. by rewrite fromNat0; apply lift_right_id; do !elim. Qed.
Lemma and0B n : left_zero #0 (andB (n:=n)).
Proof. by rewrite fromNat0; apply lift_left_zero; do !elim. Qed.
Lemma andB0 n : right_zero #0 (andB (n:=n)).
Proof. by rewrite fromNat0; apply lift_right_zero; do !elim. Qed.
Lemma xor0B n : left_id #0 (xorB (n:=n)).
Proof. by rewrite fromNat0; apply lift_left_id; do !elim. Qed.
Lemma xorB0 n : right_id #0 (xorB (n:=n)).
Proof. by rewrite fromNat0; apply lift_right_id; do !elim. Qed.
Lemma xorBB n : forall x, xorB (n:=n) x x = #0.
Proof. by rewrite /xorB; lift_op_t n. Qed.
Lemma xorBN : forall n (b : BITS n), xorB b (ones n) = invB b.
Proof. by rewrite /xorB/invB => n; lift_op_t n. Qed.
Lemma invB0 n : invB #0 = ones n.
Proof. by rewrite /invB; lift_op_t n. Qed.
Lemma xorBNaux : forall n (b : BITS n), xorB b (invB b) = ones _.
Proof. move => n b. by rewrite -xorBN xorBA xorBB xor0B. Qed.
Lemma toNat_andB:
forall n (bs: BITS n) bs', toNat (andB bs bs') <= toNat bs'.
Proof.
elim=> [bs bs'|n IH /tupleP[b bs] /tupleP[b' bs']].
+ by rewrite tuple0.
+ rewrite /andB liftBinOpCons -/andB /=.
rewrite /toNat /consB /=.
apply leq_add.
elim: b=> //.
rewrite leq_double.
by apply IH.
Qed.
Lemma orB_invB:
forall n (bs: BITS n),
orB bs (invB bs) = ones n.
Proof.
move=> n bs.
apply allBitsEq=> k le_k.
rewrite getBit_liftBinOp =>//.
rewrite getBit_liftUnOp =>//.
by rewrite orbN /getBit nth_nseq le_k.
Qed.
Lemma andB_invB:
forall n (bs: BITS n),
andB bs (invB bs) = zero n.
Proof.
move=> n bs.
apply allBitsEq.
move=> k le_k.
rewrite getBit_liftBinOp =>//.
rewrite getBit_liftUnOp =>//.
by rewrite andbN -fromNat0 getBit_zero.
Qed.
Lemma leB_andB:
forall n (bs: BITS n) (bs': BITS n), leB (andB bs bs') bs'.
Proof.
elim=> [bs bs'|n IHn /tupleP[b bs] /tupleP[b' bs']].
+ (* n ~ 0 *)
by rewrite !tuple0 [bs']tuple0.
+ (* n ~ n.+1 *)
rewrite /andB liftBinOpCons -/andB /leB /ltB /=
!tuple.beheadCons !tuple.theadCons -/ltB.
case H: (ltB (andB bs bs') bs').
by rewrite /leB in IHn.
have H': (andB bs bs' == bs').
rewrite -[andB _ _ == _]orbF orbC -H.
by apply IHn.
rewrite H'.
move/eqP: H'->.
case: b'=> /=.
+ (* b' = true *)
rewrite !andbT.
by case: b=> /=.
+ (* b' = false *)
by rewrite !andbF orbC orbF //.
Qed.
(*---------------------------------------------------------------------------
Properties of increment and decrement operations
---------------------------------------------------------------------------*)
Lemma ones_decomp n : ones n.+1 = consB true (ones n).
Proof. by apply val_inj. Qed.
Lemma zero_decomp n : zero n.+1 = consB false (zero n).
Proof. by apply val_inj. Qed.
Lemma bitsEq_decomp n b1 b2 (p1 p2: BITS n) :
(consB b1 p1 == consB b2 p2) = (b1 == b2) && (p1 == p2).
Proof. done. Qed.
Lemma andB_mask1:
forall n (bs: BITS n),
andB bs #1 = (if getBit bs 0 then #1 else #0).
Proof.
case=> [bs|n /tupleP [b bs]].
- (* Case: n ~ 0 *)
by rewrite [bs]tuple0 tuple0.
- (* Case: n ~ n.+1 *)
rewrite /andB liftBinOpCons -/andB /= andbT !fromNat0 -/fromNat.
rewrite andB0.
have ->: getBit [tuple of b :: bs] 0 = b by [].
by case: b=> //; rewrite zero_decomp fromNat0.
Qed.
(* First, with respect to conversions *)
Lemma toNat_incB n : forall (p: BITS n), toNat (incB p) = if p == ones _ then 0 else (toNat p).+1.
Proof. induction n.
+ move => p. by rewrite (tuple0 p).
+ case/tupleP => [b p].
rewrite /= theadCons beheadCons toNatCons.
destruct b => //.
rewrite toNat_joinlsb add0n add1n IHn.
case E: (p == ones n).
+ by replace (_ == _) with true.
+ by rewrite ones_decomp/= bitsEq_decomp doubleS E.
Qed.
Lemma toNatMod_incB n (p: BITS n) : toNat (incB p) = (toNat p).+1 %[mod 2^n].
Proof. rewrite toNat_incB.
case E: (p == ones n) => //.
by rewrite (eqP E) toNat_ones_succ modnn mod0n.
Qed.
Lemma toNat_decB_succ n : forall (p: BITS n), (toNat (decB p)).+1 = if p == #0 then 2^n else toNat p.
Proof. induction n.
+ move => p. by rewrite (tuple0 p).
+ case/tupleP => [b p].
rewrite /=theadCons beheadCons toNatCons.
destruct b => //.
rewrite toNat_joinlsb add0n.
specialize (IHn p).
case E: (p == #0) => //.
+ rewrite (eqP E). rewrite (eqP E) eq_refl in IHn. rewrite expnS. rewrite -IHn.
replace (_ == _) with true. by rewrite add1n mul2n doubleS.
rewrite /fromNat-/fromNat/=/joinlsb. simpl. by rewrite eq_refl.
+ replace (_ == _) with false. rewrite E in IHn. rewrite -IHn.
rewrite doubleS. by rewrite add1n.
Qed.
Lemma toNat_decB n (p: BITS n) : toNat (decB p) = (if p == #0 then 2^n else toNat p).-1.
Proof. by rewrite -toNat_decB_succ succnK. Qed.
Lemma nonZeroIsSucc n (p: BITS n) : p != #0 -> exists m, toNat p = m.+1.
Proof. move => H.
case E: (toNat p) => [| n'].
+ rewrite -(toNatK p) in H. by rewrite E fromNat0 eq_refl in H.
+ by exists n'.
Qed.
Lemma toNatMod_decB n (p: BITS n) : toNat (decB p) = (toNat p + (2^n).-1) %[mod 2^n].
Proof. rewrite toNat_decB.
case E: (p == #0) => //.
+ rewrite (eqP E) {E}. by rewrite toNat_fromNat0 add0n.
+ apply negbT in E. destruct (nonZeroIsSucc E) as [m E']. rewrite E'. rewrite succnK.
rewrite -!subn1. rewrite addnBA. rewrite addnC. rewrite -addnBA => //.
rewrite subn1 succnK. by rewrite modnDl.
apply expn_gt0.
Qed.
Lemma fromNatDouble b n : forall m, cons_tuple b (fromNat (n:=n) m) = fromNat (b + m.*2).
Proof. move => m. rewrite /fromNat-/fromNat/=. rewrite oddD odd_double.
destruct b. simpl. by rewrite uphalf_double.
by rewrite add0n half_double.
Qed.
From mathcomp Require Import ssralg.
Import GRing.Theory.
(*---------------------------------------------------------------------------
All operations in BITS n (for n>0) have corresponding operations
in 'Z_(2^n).
---------------------------------------------------------------------------*)
Lemma toZp_incB n (p:BITS n.+1) : toZp (incB p) = (toZp p + 1)%R.
Proof. apply val_inj. rewrite /= Zp_cast; last apply pow2_gt1.
rewrite modnDml modnDmr addn1 toNat_incB.
case E: (p == ones _) => //.
by rewrite (eqP E) toNat_ones_succ modnn mod0n.
Qed.
Lemma toZp_decB n (p:BITS n.+1) : toZp (decB p) = (toZp p - 1)%R.
Proof. apply val_inj.
set N := n.+1.
set D :=decB p.
rewrite /= Zp_cast; last apply pow2_gt1.
rewrite /D {D}.
rewrite toNatMod_decB. replace (1 %% 2^N) with 1.
rewrite (@modn_small (2^N - 1)).
rewrite (@modn_small (toNat p)). by rewrite subn1.
apply toNatBounded.
apply pow2_sub_ltn.
rewrite modn_small => //; last apply pow2_gt1.
Qed.
#[export]
Hint Rewrite toZp_incB toZp_decB : ZpHom.
(*---------------------------------------------------------------------------
We can now prove properties via 'Z_(2^n).
The pattern to these proofs is as follows:
1. Deal with the n=0 case by
destruct n; first apply trivialBits
2. Embed into toZp using
apply toZp_inj
3. Repeatedly apply homomorphisms from BITS n into 'Z_n using equations
with names toZp_X such as toZp_incB or toZp_adcB
4. You're now in the land of 'Z_n and ring theory, so apply lemmas from
ssralg and zmodp.
---------------------------------------------------------------------------*)
Lemma decBK n : cancel (@decB n) incB.
Proof. move => p. destruct n; first apply trivialBits.
apply toZp_inj. autorewrite with ZpHom.
by rewrite -addrA addNr addr0.
Qed.
Lemma incBK n : cancel (@incB n) decB.
Proof. move => p. destruct n; first apply trivialBits.
apply toZp_inj. autorewrite with ZpHom.
by rewrite -addrA addrN addr0.
Qed.
Lemma decB_zero n : decB (zero n) = ones _.
Proof. destruct n; first apply trivialBits.
apply toZp_inj. autorewrite with ZpHom.
by rewrite sub0r.
Qed.
Lemma incB_ones n : incB (ones n) = zero _.
Proof. destruct n; first apply trivialBits.
apply toZp_inj. autorewrite with ZpHom.
by rewrite addNr.
Qed.
Lemma incB_fromNat n m : incB (n:=n) #m = #(m.+1).
Proof. destruct n; first apply trivialBits.
apply toZp_inj. autorewrite with ZpHom.
by rewrite -(addn1 m) natrD.
Qed.
Lemma decB_fromSuccNat n m : decB (n:=n) #(m.+1) = #m.
Proof. destruct n => //.
apply toZp_inj. autorewrite with ZpHom.
rewrite -(addn1 m) GRing.natrD.
by rewrite GRing.addrK.
Qed.
(*---------------------------------------------------------------------------
Properties of inversion (one's complement)
---------------------------------------------------------------------------*)
Lemma invBCons n b (p: BITS n) : invB (cons_tuple b p) = cons_tuple (negb b) (invB p).
Proof. rewrite /invB. by rewrite liftUnOpCons. Qed.
Lemma negB_or_invB_fromNat n : forall m, m < 2^n ->
negB (n:=n) #m = #(2^n - m)
/\ invB (n:=n) #m = #((2^n).-1 - m).
Proof. induction n. split; [done | apply trivialBits].
move => m H.
rewrite expnS mul2n in H. pose H' := half_ltn_double H. elim (IHn _ H') => [IH1 IH2] {IHn}.
split.
+
rewrite /negB.
rewrite /fromNat-/fromNat. rewrite invBCons IH2 /=!theadCons!beheadCons.
rewrite oddB. rewrite odd_power2/=.
case ODD: (odd m).
- rewrite expnS mul2n. rewrite half_sub.
rewrite uphalf_half ODD -subn1 subnDA. done. apply (ltnW H).
- rewrite incB_fromNat.
rewrite expnS mul2n half_sub.
rewrite uphalf_half ODD add0n.
rewrite -subn1. rewrite subnAC. rewrite subn1. rewrite prednK. done.
by rewrite subn_gt0.
apply (ltnW H).
- rewrite expnS mul2n. apply (ltnW H).
rewrite /fromNat-/fromNat invBCons IH2. rewrite oddB/=.
rewrite odd_power2subn1/=. rewrite -!subn1 -!subnDA expnS mul2n.
rewrite half_sub. done. apply H.
rewrite expnS mul2n. apply leq_subn; last done. rewrite -mul2n -expnS. apply expn_gt0.
Qed.
Corollary negB_fromNat n m : m < 2^n -> negB (n:=n) #m = #(2^n - m).
Proof. apply negB_or_invB_fromNat. Qed.
Corollary invB_fromNat n m : m < 2^n -> invB (n:=n) #m = #((2^n).-1 - m).
Proof. apply negB_or_invB_fromNat. Qed.
Lemma toNat_negB_or_invB n : forall (p: BITS n),
(toNat (negB p) = if toNat p == 0 then 0 else 2^n - toNat p)
/\ (toNat (invB p) = (2^n).-1 - toNat p).
Proof. induction n. move => p. by rewrite (tuple0 p)/toNat/=.
case/tupleP => [b p]. rewrite /negB !invBCons!toNatCons/=!theadCons!beheadCons.
elim (IHn p) => [IH1 IH2]. split. case b.
+ simpl. rewrite toNatCons IH2.
rewrite doubleB expnS mul2n. rewrite -subn1 doubleB/=.
rewrite add1n. rewrite -!mul2n. rewrite muln1. rewrite subnAC. rewrite subn2.
rewrite subnDA. rewrite subnAC. rewrite prednK. by rewrite subn1.
assert (B:=toNatBounded p). rewrite !mul2n -doubleB.
rewrite -subn1. rewrite subn_gt0. rewrite -subn_gt0 in B. rewrite -half_gt0.
rewrite doubleK. done.
+ simpl. rewrite toNatCons. rewrite !add0n.
rewrite /negB in IH1. rewrite IH1.
case E: (toNat p) => [| n']. done.
simpl. rewrite doubleB expnS -muln2 mulnC. done.
case b.
+ simpl. rewrite add0n. rewrite IH2. rewrite expnS. rewrite -!subn1 !doubleB.
rewrite -!muln2. rewrite mul1n subnDA. rewrite mulnC. rewrite !subn1 subn2. done.
+ simpl. rewrite add0n. rewrite IH2. rewrite expnS. rewrite -!subn1 !doubleB.
rewrite -!muln2. rewrite mul1n. rewrite add1n. rewrite subnAC. rewrite mulnC.
rewrite subn2.
assert (B:0 < (2*2^n - toNat p * 2).-1).
assert (B':=toNatBounded p). rewrite mul2n muln2. rewrite -doubleB.
rewrite -subn_gt0 in B'. rewrite -subn1 subn_gt0 -half_gt0 doubleK. done.
rewrite (ltn_predK B). rewrite -subn1. by rewrite subnAC.
Qed.
Corollary toNat_invB n (p: BITS n) : toNat (invB p) = (2^n).-1 - toNat p.
Proof. apply toNat_negB_or_invB. Qed.
Corollary toNat_negB n (p: BITS n) : toNat (negB p) =
if toNat p == 0 then 0 else 2^n - toNat p.
Proof. apply toNat_negB_or_invB. Qed.
(* There must be an easier way to prove this! *)
Lemma toZp_invB n (p:BITS n.+1) : toZp (invB p) = (-toZp p - 1)%R.
Proof. apply val_inj.
rewrite /= Zp_cast; last apply pow2_gt1.
rewrite toNat_invB.
rewrite (@modn_small 1); last apply pow2_gt1.
rewrite (@modn_small (toNat p)); last apply toNatBounded.
rewrite (@modn_small (2^n.+1-1)); last apply pow2_sub_ltn.
rewrite modn_small.
case E: (toNat p) => [| p'].
+ rewrite 2!subn0. rewrite modnn add0n.
rewrite modn_small; last apply pow2_sub_ltn. by rewrite subn1.
rewrite -subn1 -subnDA add1n.
rewrite (@modn_small (2^n.+1 - p'.+1)); last apply pow2_sub_ltn.
rewrite addnBA; last apply expn_gt0.
rewrite addnC.
rewrite -addnBA.
rewrite addnC. rewrite modnDr.
rewrite -subnDA. rewrite addn1. rewrite modn_small; last apply pow2_sub_ltn.
done.
have B:= toNatBounded p.
rewrite -E.
by rewrite subn_gt0.
rewrite -subn1. rewrite -subnDA. rewrite add1n. apply pow2_sub_ltn.
Qed.
(*
Corollary invB_fromNatAux n m : m < 2^n -> invB (n:=n) #m = #((2^n).-1 - m).
Proof. move => H. destruct n; first apply trivialBits.
apply toZp_inj. rewrite toZp_invB 2!toZp_fromNat.
rewrite -subn1. rewrite natr_sub.
rewrite natr_sub; last apply expn_gt0. rewrite addrAC.
done. rewrite oppr_sub. subrCA. rewrite modZp. done. simpl. . done. => //. rewrite subrr. _sub. rewrite -Zp_opp. rewrapply apply negB_or_invB_fromNat. Qed.
*)
(*---------------------------------------------------------------------------
Properties of negation (two's complement)
---------------------------------------------------------------------------*)
Lemma toZp_negB n (p:BITS n.+1) : toZp (negB p) = (-toZp p)%R.
Proof. apply val_inj. rewrite /= Zp_cast; last apply pow2_gt1.
rewrite toNat_negB.
case E: (toNat p) => [| n'].
+ simpl. rewrite modn_small. by rewrite subn0 modnn.
apply expn_gt0.
+ simpl. rewrite modn_small.
rewrite (@modn_small (n'.+1)).
rewrite modn_small. done.
apply pow2_sub_ltn.
rewrite -E. apply toNatBounded.
apply pow2_sub_ltn.
Qed.
#[export]
Hint Rewrite toZp_negB : ZpHom.
Lemma negBK n : involutive (@negB n).
Proof. move => p. destruct n; first apply trivialBits.
apply toZp_inj. autorewrite with ZpHom.
by rewrite opprK.
Qed.
Lemma negB_zero n : negB (zero n) = zero _.
Proof. destruct n; first apply trivialBits.
apply toZp_inj. autorewrite with ZpHom.
by rewrite oppr0.
Qed.
Corollary negB0 n : @negB n #0 = #0.
Proof. destruct n; first apply trivialBits.
apply toZp_inj. autorewrite with ZpHom.
by rewrite oppr0.
Qed.
(*---------------------------------------------------------------------------
Properties of addition
---------------------------------------------------------------------------*)
Lemma fullAdderTT c : fullAdder c true true = (true,c).
Proof. by destruct c. Qed.
Lemma adcBmain_nat n : forall b (p1 p2: BITS n), adcBmain b p1 p2 = #(b + toNat p1 + toNat p2).
Proof.
induction n.
+ move => b p1 p2. rewrite 2!toNatNil. by destruct b.
+ move => b. case/tupleP => [b1 p1]. case/tupleP => [b2 p2].
rewrite /fromNat-/fromNat/=.
rewrite !theadCons !beheadCons !toNatCons !oddD !odd_double /=.
case e: (fullAdder b b1 b2) => [carry' b0].
specialize (IHn carry' p1 p2). rewrite IHn /= addnA.
assert (b0 = odd b (+) (odd b1 (+) false) (+) (odd b2 (+) false)).
rewrite /fullAdder in e. destruct b; destruct b1; destruct b2; inversion e; subst; done.
rewrite -H.
assert (carry' + toNat p1 + toNat p2 =
(b + (b1 + (toNat p1).*2) + b2 + (toNat p2).*2)./2).
rewrite addnA (addnC _ b2) -!addnA -doubleD !addnA.
rewrite /fullAdder in e. destruct b; destruct b1; destruct b2; inversion e; subst; simpl;
by (try rewrite uphalf_double; try rewrite half_double).
rewrite H0. by apply val_inj.
Qed.
Lemma adcB_bounded n (b:bool) (p1 p2: BITS n) : b + toNat p1 + toNat p2 < 2^n.+1.
Proof.
have B1 := toNatBounded p1.
have B2 := toNatBounded p2.
rewrite expnS mul2n -addnn.
have B :=leq_add B1 B2.
destruct b.
+ rewrite addnC add1n -addn1 addnC addnA add1n. apply leq_add; done.
+ rewrite add0n -addn1 addnC addnA add1n. apply leq_add; first done. by rewrite ltnW.
Qed.
Corollary toNat_adcBmain n b (p1 p2: BITS n) : toNat (adcBmain b p1 p2) = b + toNat p1 + toNat p2.
Proof.
rewrite adcBmain_nat. rewrite toNat_fromNatBounded => //.
apply adcB_bounded.
Qed.
Lemma toZp_adcB n b (p1 p2:BITS n) :
toZp (adcBmain b p1 p2) = (bool_inZp _ b + toZpAux p1 + toZpAux p2)%R.
Proof.
apply val_inj. rewrite /= Zp_cast; last apply pow2_gt1.
rewrite toNat_adcBmain.
have BOUND:= adcB_bounded b p1 p2.
rewrite modn_small => //.
rewrite (@modn_small b).
rewrite (@modn_small (toNat p1)).
rewrite (@modn_small (toNat p2)).
rewrite (@modn_small (b + toNat p1)).
rewrite modn_small => //.
apply: leq_ltn_trans BOUND. apply leq_addr.
apply: leq_ltn_trans BOUND. rewrite addnC. apply leq_addr.
apply: leq_ltn_trans BOUND. rewrite -addnAC. apply leq_addl.
apply: leq_ltn_trans BOUND. rewrite -addnA. apply leq_addr.
Qed.
Corollary toNat_addB n (p1 p2: BITS n) : toNat (addB p1 p2) = (toNat p1 + toNat p2) %% 2^n.
Proof. by rewrite toNat_dropmsb toNat_adcBmain add0n. Qed.
Corollary toZp_addB n (p1 p2: BITS n.+1) : toZp (addB p1 p2) = (toZp p1 + toZp p2)%R.
Proof. apply val_inj. rewrite /toZp. rewrite toNat_addB.
rewrite /= Zp_cast; last apply pow2_gt1.
rewrite (@modn_small (toNat p1)); last apply toNatBounded.
rewrite (@modn_small (toNat p2)); last apply toNatBounded.
by rewrite modn_mod.
Qed.
#[export]
Hint Rewrite toZp_adcB toZp_addB : ZpHom.
Lemma addBC n : commutative (@addB n).
Proof. move => x y. destruct n; first apply trivialBits.
apply toZp_inj. autorewrite with ZpHom.
by rewrite addrC.
Qed.
(*=addBA *)
Lemma addBA n : associative (@addB n).
Proof. move => x y z. destruct n; first apply trivialBits.
apply toZp_inj. autorewrite with ZpHom.
by rewrite addrA. Qed.
(*=End *)
Lemma adcBC n c : commutative (@adcBmain n c).
Proof. move => x y. apply toZp_inj.
autorewrite with ZpHom.
by rewrite addrAC.
Qed.
Lemma adc0B n (p : BITS n) : adcBmain false #0 p = joinmsb0 p.
Proof.
apply toZp_inj. rewrite fromNat0. autorewrite with ZpHom.
rewrite /bool_inZp -Zp_nat.
by rewrite 2!add0r.
Qed.
Lemma adcB0 n (p : BITS n) : adcBmain false p #0 = joinmsb0 p.
Proof.
apply toZp_inj. rewrite fromNat0. autorewrite with ZpHom.
by rewrite /bool_inZp addr0 -!Zp_nat add0r.
Qed.
Lemma add0B n : left_id #0 (@addB n).
Proof. move => x. destruct n; first apply trivialBits.
apply toZp_inj. autorewrite with ZpHom.
by rewrite add0r.
Qed.
Lemma addB0 n : right_id #0 (@addB n).
Proof. move => x. destruct n; first apply trivialBits.
apply toZp_inj. autorewrite with ZpHom.
by rewrite addr0.
Qed.
Lemma fromNat_addBn n m1 m2 : #m1 +# m2 = fromNat (n:=n) (m1 + m2).
Proof. apply toNat_inj. rewrite toNat_addB !toNat_fromNat. by rewrite modnDm. Qed.
Lemma addB_addn n (p:BITS n) m1 m2 : p +# (m1+m2) = p +# m1 +# m2.
Proof. destruct n; first apply trivialBits.
apply toZp_inj. autorewrite with ZpHom.
by rewrite natrD addrA.
Qed.
Lemma addB1 n (p: BITS n) : p +# 1 = incB p.
Proof. destruct n; first apply trivialBits.
apply toZp_inj. autorewrite with ZpHom.
done.
Qed.
Lemma addB_negBn n (p: BITS n) m : addB (p +# m) (negB #m) = p.
Proof. destruct n; first apply trivialBits.
apply toZp_inj. autorewrite with ZpHom.
by rewrite -addrA addrN addr0.
Qed.
Lemma addB_decB_incB n (c a: BITS n) : addB (decB c) (incB a) = addB c a.
Proof. destruct n; first apply trivialBits.
apply toZp_inj. autorewrite with ZpHom.
by rewrite addrAC -2!addrA addrN addr0.
Qed.
Lemma addBN n (p: BITS n) : addB (negB p) p = #0.
Proof. destruct n; first apply trivialBits.
apply toZp_inj. autorewrite with ZpHom.
by rewrite addNr.
Qed.
Lemma addNB n (p: BITS n) : addB p (negB p) = #0.
Proof. by rewrite addBC addBN. Qed.
Lemma adcIsInc n c (p:BITS n) : dropmsb (adcBmain c p #0) = if c then incB p else p.
Proof. rewrite adcBmain_nat dropmsb_fromNat fromNat0 toNat_zero addn0. destruct c.
+ by rewrite -incB_fromNat toNatK.
+ by rewrite add0n toNatK.
Qed.
(* Add is iterated increment *)
(* Proof seems a bit contorted! *)
Lemma adcIsIterInc n m : forall c (p:BITS n),
dropmsb (adcBmain c p #m) = iter m incB (if c then incB p else p).
Proof.
induction m => c p.
+ by rewrite /= adcIsInc.
+ rewrite /= -IHm. clear IHm. rewrite 2!adcBmain_nat. rewrite !dropmsb_fromNat.
set D := c + toNat p.
rewrite incB_fromNat.
rewrite -(addn1 (D + toNat #m)) -addnA.
apply fromNat_addn. rewrite toNatK addn1. apply fromNat_succn. by rewrite toNatK.
Qed.
Transparent sbbB adcB.
Corollary addIsIterInc n (p:BITS n) m : p +# m = iter m incB p.
Proof. by apply: adcIsIterInc. Qed.
(*---------------------------------------------------------------------------
Properties of subtraction
---------------------------------------------------------------------------*)
Lemma subB_is_dropmsb_adcB_invB n (p q: BITS n) : subB p q = dropmsb (adcBmain true p (invB q)).
Proof. by []. Qed.
Lemma toZp_subB n (p q: BITS n.+1) : toZp (subB p q) = (toZp p - toZp q)%R.
Proof. rewrite subB_is_dropmsb_adcB_invB.
apply val_inj. rewrite toZp_dropmsb /toZpAux.
rewrite toNat_adcBmain toNat_invB. rewrite add1n.
rewrite /inZp/= Zp_cast; last apply pow2_gt1.
rewrite (@modn_small (toNat p)); last apply toNatBounded.
rewrite (@modn_small (toNat q)); last apply toNatBounded.
rewrite -addn1.
rewrite -subn1. rewrite -subnDA. rewrite addnAC. rewrite -addnA. rewrite addn1 add1n. rewrite -subSn; last apply toNatBounded.
case E: (toNat q) => [| n'].
rewrite !subn0 modnn addn0. rewrite subn1. rewrite succnK. by rewrite modnDr.
rewrite (@modn_small (2^n.+1 - n'.+1)); last apply pow2_sub_ltn.
done.
Qed.
#[export]
Hint Rewrite toZp_subB : ZpHom.
Lemma subB_equiv_addB_negB n (p q: BITS n): subB p q = addB p (negB q).
Proof. destruct n; first apply trivialBits.
apply toZp_inj. by autorewrite with ZpHom.
Qed.
(* This is absurdly complicated! *)
Lemma sbb0B_carry n (p: BITS n.+1) : fst (sbbB false #0 p) = (p != #0).
Proof. rewrite /sbbB. simpl (~~false). rewrite /adcB.
elim E: (splitmsb (adcBmain true #0 (invB p))) => [carry res].
rewrite -(toNatK (adcBmain true #0 (invB p))) in E.
rewrite splitmsb_fromNat in E.
rewrite toNat_adcBmain toNat_fromNat0 addn0 toNat_invB in E.
inversion E.
clear E H0 H1.
rewrite add1n.
case E: (p == #0).
+ rewrite (eqP E). rewrite toNat_fromNat0.
rewrite subn0. rewrite prednK; last apply expn_gt0.
by rewrite divnn expn_gt0.
+ apply negbT in E. have [m H] := (nonZeroIsSucc E).
rewrite H.
rewrite divn_small => //.
rewrite -subSn. rewrite prednK; last apply expn_gt0.
apply pow2_sub_ltn.
have B:= toNatBounded p.
rewrite H in B.
have HH := @ltn_sub2r 1 m.+1 (2^n.+1).
rewrite subn1 in HH.
rewrite prednK in HH => //.
rewrite subn1 in HH.
apply HH.
apply pow2_gt1.
apply B.
Qed.
Lemma subB0 n (p: BITS n) : subB p #0 = p.
Proof. destruct n; first apply trivialBits.
apply toZp_inj. autorewrite with ZpHom.
by rewrite subr0.
Qed.
Lemma sub0B n (p: BITS n) : subB #0 p = negB p.
Proof. destruct n; first apply trivialBits.
apply toZp_inj. autorewrite with ZpHom.
by rewrite sub0r.
Qed.
Lemma subBB n (p: BITS n) : subB p p = #0.
Proof. destruct n; first apply trivialBits.
apply toZp_inj. autorewrite with ZpHom.
by rewrite subrr.
Qed.
Lemma toNat_addBn n : forall (p: BITS n) m, toNat (p +# m) = (toNat p + m) %% 2^n.
Proof. move => p m.
rewrite /adcB adcBmain_nat add0n. rewrite splitmsb_fromNat.
rewrite !toNat_fromNat.
by rewrite modnDmr.
Qed.
Corollary inZp_addBn n (p:BITS n.+1) m : toZp (p +# m) = inZp (toNat p + m).
Proof. apply val_inj. rewrite /inZp/toZp.
rewrite toNat_addBn.
rewrite /= Zp_cast; last apply pow2_gt1.
apply modn_mod.
Qed.
Lemma toNat_addBn_wrap n : forall (p: BITS n) m,
m<2^n -> toNat p + m >= 2^n -> toNat (p +# m) + 2^n = toNat p + m.
Proof.
move => p m BOUND H.
rewrite /adcB adcBmain_nat splitmsb_fromNat add0n.
rewrite toNat_fromNat. rewrite toNat_fromNat.
rewrite modnDmr. apply modn_sub.
+ apply expn_gt0. + apply toNatBounded. + done. + done.
Qed.
Lemma neqB_modn n (p q: BITS n) : p <> q <-> toNat p <> toNat q %[mod 2^n].
Proof. split => H. move => H'.
rewrite (@modn_small (toNat p)) in H'.
rewrite (@modn_small (toNat q)) in H'.
apply toNat_inj in H'. by subst. apply toNatBounded. apply toNatBounded.
move => H'. by subst.
Qed.
Lemma addBn_distinct n m : forall (p: BITS n), m.+1 < 2^n -> p <> p +#(m.+1).
Proof. move => p LT.
rewrite neqB_modn.
rewrite toNat_addB toNat_fromNat. rewrite (@modn_small (m.+1)) => //. rewrite modn_mod.
move/eqP. rewrite -{1}(addn0 (toNat p)).
rewrite eqn_modDl.
rewrite modn_small; last by apply expn_gt0.
by rewrite modn_small; last by assumption.
Qed.
Corollary addBn_ne n m : forall (p: BITS n), m.+1 < 2^n -> p != p +#(m.+1).
Proof. move => p LT. apply/eqP. by apply addBn_distinct. Qed.
(* @todo: prove these as corollaries of addBn_distinct *)
Lemma incBDistinct n : forall (p: BITS n.+1), incB p <> p.
Proof. case/tupleP => b p'. by elim b. Qed.
Lemma incBincBDistinct n : forall (p: BITS n.+2), incB (incB p) <> p.
Proof. case/tupleP => b p'. case/tupleP: p' => b' p'. elim b; by elim b'. Qed.
Lemma incBincBincBDistinct n : forall (p: BITS n.+2), incB (incB (incB p)) <> p.
Proof. case/tupleP => b p'. case/tupleP: p' => b' p'. elim b; by elim b'. Qed.
Lemma incBneq n : forall (p: BITS n.+1), incB p != p.
Proof. move => p. apply (introN eqP). apply: incBDistinct. Qed.
Lemma incBincBneq n : forall (p: BITS n.+2), incB (incB p) != p.
Proof. move => p. apply (introN eqP). apply: incBincBDistinct. Qed.
Lemma incBincBincBneq n : forall (p: BITS n.+2), incB (incB (incB p)) != p.
Proof. move => p. apply (introN eqP). apply: incBincBincBDistinct. Qed.
(*
Lemma bitsEqInc n : forall (p: BITS n.+1), bitsEq (incB p) p = false.
Proof. move => p. replace (bitsEq (incB p) p) with (incB p == p) by done.
apply negbTE. apply incBneq. Qed.
Lemma bitsEqIncInc n : forall (p: BITS n.+2), bitsEq (incB (incB p)) p = false.
Proof. move => p. replace (bitsEq _ p) with (incB (incB p) == p) by done.
apply negbTE. apply incBincBneq. Qed.
Lemma bitsEqIncIncInc n : forall (p: BITS n.+2), bitsEq (incB (incB (incB p))) p = false.
Proof. move => p. replace (bitsEq _ p) with (incB (incB (incB p)) == p) by done.
apply negbTE. apply incBincBincBneq. Qed.
*)
Lemma addBsubBn n (p: BITS n) m1 m2 : m2 <= m1 -> p +# (m1-m2) = p +# m1 -# m2.
Proof. move => H. destruct n; first apply trivialBits.
apply toZp_inj. autorewrite with ZpHom.
rewrite natrB => //.
by rewrite addrA.
Qed.
Lemma subB_def n (p q: BITS n.+1) : subB p q = fromZp (toZp p - toZp q)%R.
Proof. apply toZp_inj. by autorewrite with ZpHom. Qed.
Lemma addB_def n (p q: BITS n.+1) : addB p q = fromZp (toZp p + toZp q)%R.
Proof. apply toZp_inj. by autorewrite with ZpHom. Qed.
Lemma addB0_inv n (p: BITS n) m : m < 2^n -> p == p +# m -> m = 0.
Proof. move => BOUND EQ.
destruct n. by destruct m.
have: toNat p == toNat (p +# m). by rewrite {1}(eqP EQ).
rewrite toNat_addB.
rewrite toNat_fromNat. rewrite (@modn_small m); last done.
rewrite -{1}(@modn_small (toNat p) (2^n.+1)).
rewrite -{1}(addn0 (toNat p)).
rewrite eqn_modDl. rewrite modn_small.
rewrite modn_small; last done.
by move/eqP ->.
apply expn_gt0. apply toNatBounded.
Qed.
Lemma subB_eq n (x y z: BITS n) : (subB x z == y) = (x == addB y z).
Proof. destruct n. by rewrite (tuple0 x) (tuple0 y) (tuple0 z).
rewrite 2!toZp_eq. autorewrite with ZpHom.
by rewrite subr_eq.
Qed.
Lemma subB_eq0 n (x y: BITS n) : (subB x y == #0) = (x == y).
Proof. destruct n. by rewrite (tuple0 x) (tuple0 y).
rewrite 2!toZp_eq. autorewrite with ZpHom.
by rewrite subr_eq0.
Qed.
Lemma subB1 n (p: BITS n) : p -# 1 = decB p.
Proof. destruct n; first apply trivialBits.
apply toZp_inj. by autorewrite with ZpHom.
Qed.
Lemma subB_addn n (p:BITS n) m1 m2 : p -# (m1+m2) = p -# m1 -# m2.
Proof. destruct n; first apply trivialBits.
apply toZp_inj. autorewrite with ZpHom.
by rewrite natrD opprD addrA.
Qed.
Lemma subB_addB n (p: BITS n) m1 m2 :
p -# m1 +# m2 = if m1<m2 then p +# (m2-m1) else p -# (m1-m2).
Proof. destruct n; first apply trivialBits.
case E: (m1 < m2).
apply toZp_inj. autorewrite with ZpHom.
rewrite natrB. rewrite addrAC. by rewrite addrA. by apply ltnW.
apply toZp_inj. autorewrite with ZpHom.
rewrite natrB. rewrite addrAC. rewrite opprB. by rewrite addrA.
rewrite leqNgt. by rewrite E.
Qed.
Lemma addB_subBK n (p: BITS n) q : addB p (subB q p) = q.
Proof. destruct n; first apply trivialBits.
apply toZp_inj.
rewrite toZp_addB toZp_subB.
by rewrite addrCA addrN addr0.
Qed.
(*---------------------------------------------------------------------------
Properties of unsigned comparison
---------------------------------------------------------------------------*)
Lemma ltB_nat n : forall p1 p2: BITS n, ltB p1 p2 = (toNat p1 < toNat p2).
Proof.
induction n. move => p1 p2. by rewrite (tuple0 p1) (tuple0 p2).
move => p1 p2. case/tupleP: p1 => [b1 q1]. case/tupleP: p2 => [b2 q2].
rewrite 2!toNatCons /= !beheadCons !theadCons IHn.
case E: (toNat q1 < toNat q2). simpl.
case b1; case b2; simpl.
+ by rewrite ltn_add2l ltn_double.
+ by rewrite add0n addnC addn1 ltn_Sdouble.