-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathstdlib.bus
More file actions
8443 lines (6393 loc) · 245 KB
/
Copy pathstdlib.bus
File metadata and controls
8443 lines (6393 loc) · 245 KB
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
/*
Language built-ins:
atom IMPLIES;
syntax (a b) = a b, precedence 10000, associativity left;
*/
syntax (a -> b) = IMPLIES a b, precedence 100, associativity right;
assume proofsyntax
ARGS : (
( (first:IDENT) (rest:ARGS) ),
( ),
),
(
define (funcname:IDENT) (args:ARGS) = (expr) ;
(innerproof)
) = (
atom ((funcname));
syntaxassume _def_((funcname))_ltr proves ((make_forany args)) ((funcname)) ((args)) -> ( ((expr)) );
syntaxassume _def_((funcname))_rtl proves ((make_forany args)) ( ((expr)) ) -> ((funcname)) ((args));
((innerproof))
),
make_forany_3 (args:ARGS.0) = ( , ((args.first)) ((make_forany_3 args.rest)) ),
make_forany_3 (args:ARGS.1) = ( ),
make_forany_2 (args:ARGS.0) = ( ((args.first)) ((make_forany_3 args.rest)) ),
make_forany_2 (args:ARGS.1) = ( ),
make_forany (args:ARGS.0) = ( forany ((make_forany_2 args)) : ),
make_forany (args:ARGS.1) = ( ),
;
proofsyntax
(
unwrap (funcname:IDENT) (innerproof)
) = (
_def_((funcname))_ltr < ( ((innerproof)) )
),
;
proofsyntax
(
wrap (funcname:IDENT) (innerproof)
) = (
_def_((funcname))_rtl < ( ((innerproof)) )
),
;
assume todo proves forany a: a;
define FALSE = forany a: a;
syntax (!a) = a -> FALSE, precedence 20000, associativity right;
require false_proves_anything proves forany a: FALSE -> a by ( assume f proves FALSE; unwrap FALSE f );
assume not_not_impl proves forany a: ((a -> FALSE) -> FALSE) -> a;
atom AND;
syntax (a && b) = AND a b, precedence 150, associativity left;
assume and_left proves forany a,b: (a && b) -> a;
assume and_right proves forany a,b: (a && b) -> b;
assume impl_impl_and proves forany a,b: a -> b -> (a && b);
define eq x y = (x -> y) && (y -> x);
syntax (a == b) = eq a b, precedence 160, associativity noassoc;
syntax (a != b) = !(a == b), precedence 160, associativity noassoc;
assume func_eq proves forany f,g: (f == g) == (forany x,y: x == y -> f x == g y);
define or a b = !(!a && !b);
syntax (a || b) = or a b, precedence 150, associativity left;
define xor a b = (a || b) && !(a && b);
syntax (a ^^ b) = xor a b, precedence 150, associativity left;
atom HAS_MEMBER;
syntax (a : b) = HAS_MEMBER b a, precedence 200, associativity noassoc;
assume proofsyntax
(
enum (enumname:IDENT) {
(vallist:VAL_LIST)
};
(innerproof)
) = (
atom ((enumname));
((make_atoms vallist))
((make_has_members enumname vallist))
((make_is_one_of enumname vallist))
((make_inequalities enumname vallist))
((innerproof))
),
CONDITION : (
( | (condition) ),
( ),
),
VAL_ITEM_ARGS : (
( (first:IDENT) (rest:VAL_ITEM_ARGS) ),
( ),
),
VAL_LIST : (
( (first_name:IDENT) (first_args:VAL_ITEM_ARGS) (first_condition:CONDITION) , (rest:VAL_LIST) ),
( ),
( , ),
),
make_atoms (vallist:VAL_LIST.0) = (
atom ((vallist.first_name));
((make_atoms vallist.rest))
),
make_atoms (vallist:VAL_LIST.1) = ( ),
make_atoms (vallist:VAL_LIST.2) = ( ),
make_inequality__arg_list enumname name (args:VAL_ITEM_ARGS.0) = (
_((enumname))_((name))_((args.first))
((make_inequality__arg_list enumname name args.rest))
),
make_inequality__arg_list enumname name (args:VAL_ITEM_ARGS.1) = ( ),
make_inequality__forany_3 enumname first_name (first_args:VAL_ITEM_ARGS.1) second_name (second_args:VAL_ITEM_ARGS.1) = ( ),
make_inequality__forany_3 enumname first_name (first_args:VAL_ITEM_ARGS.1) second_name (second_args:VAL_ITEM_ARGS.0) = (
, _((enumname))_((second_name))_((second_args.first))
((make_inequality__forany_3 enumname first_name first_args second_name second_args.rest))
),
make_inequality__forany_3 enumname first_name (first_args:VAL_ITEM_ARGS.0) second_name (second_args:VAL_ITEM_ARGS) = (
, _((enumname))_((first_name))_((first_args.first))
((make_inequality__forany_3 enumname first_name first_args.rest second_name second_args))
),
make_inequality__forany enumname first_name (first_args:VAL_ITEM_ARGS.1) second_name (second_args:VAL_ITEM_ARGS.1) = ( ),
make_inequality__forany enumname first_name (first_args:VAL_ITEM_ARGS.0) second_name second_args = (
forany _((enumname))_((first_name))_((first_args.first))
((make_inequality__forany_3 enumname first_name first_args.rest second_name second_args))
:
),
make_inequality__forany enumname first_name first_args second_name (second_args:VAL_ITEM_ARGS.0) = (
forany _((enumname))_((second_name))_((second_args.first))
((make_inequality__forany_3 enumname first_name first_args second_name second_args.rest))
:
),
make_inequality enumname first_name first_args first_condition second_name second_args second_condition = (
syntaxassume _neq_((enumname))_((first_name))_((second_name))
proves
((make_inequality__forany enumname first_name first_args second_name second_args))
((make_inequality_condition first_condition enumname first_name first_args))
((make_inequality_condition second_condition enumname second_name second_args))
((first_name))
((make_inequality__arg_list enumname first_name first_args))
!=
((second_name))
((make_inequality__arg_list enumname second_name second_args))
;
),
make_inequalities_2 enumname first_name first_args first_condition (vallist:VAL_LIST.0) = (
((make_inequality enumname first_name first_args first_condition vallist.first_name vallist.first_args vallist.first_condition))
((make_inequalities_2 enumname first_name first_args first_condition vallist.rest))
),
make_inequalities_2 enumname first_name first_args first_condition (vallist:VAL_LIST.1) = ( ),
make_inequalities_2 enumname first_name first_args first_condition (vallist:VAL_LIST.2) = ( ),
make_inequalities enumname (vallist:VAL_LIST.0) = (
((make_inequalities_2 enumname vallist.first_name vallist.first_args vallist.first_condition vallist.rest))
),
make_inequalities enumname (vallist:VAL_LIST.1) = ( ),
make_inequalities enumname (vallist:VAL_LIST.2) = ( ),
replace_arg_names input enumname name (args:VAL_ITEM_ARGS.0) = ( ((replace_ident args.first (concat "_" enumname "_" name "_" args.first) (replace_arg_names input enumname name args.rest))) ),
replace_arg_names input enumname name (args:VAL_ITEM_ARGS.1) = ( ((input)) ),
make_inequality_condition (condition:CONDITION.0) enumname name args = ( ( ((replace_arg_names condition.condition enumname name args)) ) -> ),
make_inequality_condition (condition:CONDITION.1) enumname name args = ( ),
make_forany_2 (args:VAL_ITEM_ARGS.0) = ( , ((args.first)) ((make_forany_2 args.rest)) ),
make_forany_2 (args:VAL_ITEM_ARGS.1) = ( ),
make_forany (args:VAL_ITEM_ARGS.0) = (
forany ((args.first)) ((make_forany_2 args.rest)) :
),
make_forany (args:VAL_ITEM_ARGS.1) = ( ),
make_has_member_maybe_condition (condition:CONDITION.0) = ( ( ((condition.condition)) ) -> ),
make_has_member_maybe_condition (condition:CONDITION.1) = ( ),
make_has_members enumname (vallist:VAL_LIST.0) = (
syntaxassume _((enumname))_has_member_((vallist.first_name)) proves ((make_forany vallist.first_args)) ((make_has_member_maybe_condition vallist.first_condition)) HAS_MEMBER ((enumname)) ( ((vallist.first_name)) ((vallist.first_args)) );
((make_has_members enumname vallist.rest))
),
make_has_members enumname (vallist:VAL_LIST.1) = ( ),
make_is_one_of__maybe_condition (condition:CONDITION.0) = ( ( ((condition.condition)) ) && ),
make_is_one_of__maybe_condition (condition:CONDITION.1) = ( ),
make_is_one_of_4 (vallist:VAL_LIST.0) = (
( ( ((make_forany vallist.first_args)) ( ((make_is_one_of__maybe_condition vallist.first_condition)) xxx == ((vallist.first_name)) ((vallist.first_args)) ) -> FALSE ) -> FALSE )
),
make_is_one_of_3 (vallist:VAL_LIST.0) = ( || ((make_is_one_of_4 vallist)) ((make_is_one_of_3 vallist.rest)) ),
make_is_one_of_3 (vallist:VAL_LIST.1) = ( ),
make_is_one_of_2 (vallist:VAL_LIST.0) = (
((make_is_one_of_4 vallist)) ((make_is_one_of_3 vallist.rest))
),
make_is_one_of enumname (vallist:VAL_LIST.0) = (
syntaxassume _((enumname))_is_one_of proves forany xxx: (HAS_MEMBER UINT xxx) -> ( ((make_is_one_of_2 vallist)) ) ;
),
;
assume proofsyntax
(
define (funcname:IDENT) {
(branch_list:BRANCH_LIST) ;
(inequality_proofs:INEQUALITY_PROOFS) ;
(self_inequality_proofs:INEQUALITY_PROOFS) ;
};
(innerproof)
) = (
atom ((funcname));
((make_equalities funcname branch_list "x"))
scope (
((make_requirements funcname branch_list inequality_proofs "x"))
((make_self_requirements funcname branch_list self_inequality_proofs "x"))
);
((innerproof))
),
INEQUALITY_PROOFS : (
( (proof) , (rest:INEQUALITY_PROOFS) ),
( (proof) ),
),
CONDITION : (
( | (condition) ),
( ),
),
BRANCH_LIST : (
( (branch:BRANCH) , (rest:BRANCH_LIST) ),
( (branch:BRANCH) ),
),
BRANCH : (
( (vars:BRANCH_VARS) : (lhs_args_maybe:LHS_ARGS_MAYBE) (condition:CONDITION) = (rhs) ),
( (lhs_args_maybe:LHS_ARGS_MAYBE) (condition:CONDITION) = (rhs) ),
),
BRANCH_VARS : (
( (first:IDENT) , (rest:BRANCH_VARS) ),
( (first:IDENT) ),
),
LHS_ARG : (
( (ident:IDENT) ),
( (paren:PAREN) ),
),
LHS_ARGS_MAYBE : (
( (lhs_args:LHS_ARGS) ),
( ),
),
LHS_ARGS : (
( (arg:LHS_ARG) (rest:LHS_ARGS) ),
( (arg:LHS_ARG) ),
),
make_equalities funcname (branch_list:BRANCH_LIST.0) counter = (
((make_equality funcname branch_list.branch counter))
((make_equalities funcname branch_list.rest (concat counter "x")))
),
make_equalities funcname (branch_list:BRANCH_LIST.1) counter = (
((make_equality funcname branch_list.branch counter))
),
make_condition (condition:CONDITION.0) = ( ( ((condition.condition)) ) -> ),
make_condition (condition:CONDITION.1) = ( ),
make_equality funcname (branch:BRANCH.0) counter = (
syntaxassume _def_((funcname))_((counter)) proves forany ((branch.vars)) : ((make_condition branch.condition)) ((funcname)) ((branch.lhs_args_maybe)) == ( ((branch.rhs)) );
),
make_equality funcname (branch:BRANCH.1) counter = (
syntaxassume _def_((funcname))_((counter)) proves ((make_condition branch.condition)) ((funcname)) ((branch.lhs_args_maybe)) == ( ((branch.rhs)) );
),
make_requirements_3 funcname (branch_list_1:BRANCH_LIST.0) (branch_list_2:BRANCH_LIST.0) inequality_proofs counter = (
((make_requirement funcname branch_list_1.branch branch_list_2.branch inequality_proofs.proof counter))
((make_requirements_3 funcname branch_list_1 branch_list_2.rest inequality_proofs.rest (concat counter "x")))
),
make_requirements_3 funcname (branch_list_1:BRANCH_LIST.0) (branch_list_2:BRANCH_LIST.1) (inequality_proofs:INEQUALITY_PROOFS.0) counter = (
((make_requirement funcname branch_list_1.branch branch_list_2.branch inequality_proofs.proof counter))
((make_requirements funcname branch_list_1.rest inequality_proofs.rest (concat counter "x")))
),
make_requirements_3 funcname (branch_list_1:BRANCH_LIST.0) (branch_list_2:BRANCH_LIST.1) (inequality_proofs:INEQUALITY_PROOFS.1) counter = (
((make_requirement funcname branch_list_1.branch branch_list_2.branch inequality_proofs.proof counter))
),
// TODO error when there are too many proofs
make_requirements funcname (branch_list_1:BRANCH_LIST.1) inequality_proofs counter = ( ),
make_requirements funcname (branch_list_1:BRANCH_LIST.0) inequality_proofs counter = (
((make_requirements_3 funcname branch_list_1 branch_list_1.rest inequality_proofs counter))
),
make_requirements_3 funcname (branch_list_1:BRANCH_LIST.1) branch_list_2 inequality_proofs = ( ),
make_requirement_forany_2 (vars:BRANCH_VARS.0) suffix = ( ((vars.first))((suffix)) , ((make_requirement_forany_2 vars.rest suffix)) ),
make_requirement_forany_2 (vars:BRANCH_VARS.1) suffix = ( ((vars.first))((suffix)) ),
make_requirement_forany (first:BRANCH.0) (second:BRANCH.0) = (
forany ((make_requirement_forany_2 first.vars "_1")) , ((make_requirement_forany_2 second.vars "_2")) :
),
make_requirement_forany (first:BRANCH.0) (second:BRANCH.1) = (
forany ((make_requirement_forany_2 first.vars "_1")) :
),
make_requirement_forany (first:BRANCH.1) (second:BRANCH.0) = (
forany ((make_requirement_forany_2 second.vars "_2")) :
),
make_requirement_forany (first:BRANCH.1) (second:BRANCH.1) = ( ),
make_requirement funcname (first:BRANCH) (second:BRANCH) inequality_proof counter = (
require _def_((funcname))_((counter)) proves ((make_requirement_forany first second)) ((make_inequality_condition first "_1")) ((make_inequality_condition second "_2")) ((make_inequalities first second first.lhs_args_maybe.lhs_args second.lhs_args_maybe.lhs_args))
by ((inequality_proof)) ;
),
make_forany_var_replacements (a:BRANCH_VARS.0) suffix expr
= ( ((replace_ident a.first (concat a.first suffix) (make_forany_var_replacements a.rest suffix expr))) ),
make_forany_var_replacements (a:BRANCH_VARS.1) suffix expr
= ( ((replace_ident a.first (concat a.first suffix) expr)) ),
make_inequality_condition_without_vars (condition:CONDITION.0) = ( ( ((condition.condition)) ) -> ),
make_inequality_condition_without_vars (condition:CONDITION.1) = ( ),
make_inequality_condition_with_vars (vars:BRANCH_VARS) suffix (condition:CONDITION.0) = ( ( ((make_forany_var_replacements vars suffix condition.condition)) ) -> ),
make_inequality_condition_with_vars (vars:BRANCH_VARS) suffix (condition:CONDITION.1) = ( ),
make_inequality_condition (branch:BRANCH.0) suffix = ( ((make_inequality_condition_with_vars branch.vars suffix branch.condition)) ),
make_inequality_condition (branch:BRANCH.1) suffix = ( ((make_inequality_condition_without_vars branch.condition)) ),
arg_with_var_replacements (branch:BRANCH.0) suffix (arg:LHS_ARG) = ( ( ((make_forany_var_replacements branch.vars suffix arg)) ) ),
arg_with_var_replacements (branch:BRANCH.1) suffix (arg:LHS_ARG) = ( ( ((arg)) ) ),
make_inequality (a:BRANCH) (b:BRANCH) (first_arg:LHS_ARG) (second_arg:LHS_ARG) = (
((arg_with_var_replacements a "_1" first_arg)) != ((arg_with_var_replacements b "_2" second_arg))
),
make_inequalities (a:BRANCH) (b:BRANCH) (first_args:LHS_ARGS.0) (second_args:LHS_ARGS.0) = (
((make_inequality a b first_args.arg second_args.arg)) || ((make_inequalities a b first_args.rest second_args.rest))
),
make_inequalities (a:BRANCH) (b:BRANCH) (first_args:LHS_ARGS.1) (second_args:LHS_ARGS.1) = (
((make_inequality a b first_args.arg second_args.arg))
),
make_inequalities (a:BRANCH) (b:BRANCH) (first_args:LHS_ARGS.1) (second_args:LHS_ARGS.0) = ( ((error "Define branches must have same amount of arguments")) ),
make_inequalities (a:BRANCH) (b:BRANCH) (first_args:LHS_ARGS.0) (second_args:LHS_ARGS.1) = ( ((error "Define branches must have same amount of arguments")) ),
make_self_requirement_forany_3 (vars:BRANCH_VARS.0) = ( ((vars.first))_1 != ((vars.first))_2 -> ((make_self_requirement_forany_3 vars.rest)) ),
make_self_requirement_forany_3 (vars:BRANCH_VARS.1) = ( ((vars.first))_1 != ((vars.first))_2 -> ),
make_self_requirement_forany_2 (vars:BRANCH_VARS.0) suffix = ( ((vars.first))((suffix)) , ((make_self_requirement_forany_2 vars.rest suffix)) ),
make_self_requirement_forany_2 (vars:BRANCH_VARS.1) suffix = ( ((vars.first))((suffix)) ),
make_self_requirement_forany (branch:BRANCH.0) = ( forany ((make_self_requirement_forany_2 branch.vars "_1")) , ((make_self_requirement_forany_2 branch.vars "_2")) : ((make_self_requirement_forany_3 branch.vars)) ),
make_self_requirement_2 (lhs_args:LHS_ARGS.0) (vars:BRANCH_VARS) = ( ((make_forany_var_replacements vars "_1" lhs_args.arg)) != ((make_forany_var_replacements vars "_2" lhs_args.arg)) || ((make_self_requirement_2 lhs_args.rest vars)) ),
make_self_requirement_2 (lhs_args:LHS_ARGS.1) (vars:BRANCH_VARS) = ( ((make_forany_var_replacements vars "_1" lhs_args.arg)) != ((make_forany_var_replacements vars "_2" lhs_args.arg)) ),
make_self_requirement_conditions (condition:CONDITION.0) (vars:BRANCH_VARS) = (
( ((make_forany_var_replacements vars "_1" condition.condition)) ) -> ( ((make_forany_var_replacements vars "_2" condition.condition)) ) ->
),
make_self_requirement_conditions (condition:CONDITION.1) (vars:BRANCH_VARS) = ( ),
make_self_requirement funcname (branch:BRANCH.0) proof counter = (
require _def_((funcname))_self_((counter)) proves ((make_self_requirement_forany branch)) ((make_self_requirement_conditions branch.condition branch.vars)) ((make_self_requirement_2 branch.lhs_args_maybe.lhs_args branch.vars)) by ((proof));
),
make_self_requirements_2 funcname (branch:BRANCH.0) (branch_list:BRANCH_LIST) (self_inequality_proofs:INEQUALITY_PROOFS.0) counter = (
((make_self_requirement funcname branch self_inequality_proofs.proof counter))
((make_self_requirements funcname branch_list self_inequality_proofs.rest (concat counter "x")))
),
make_self_requirements_2 funcname (branch:BRANCH.0) (branch_list:BRANCH_LIST) (self_inequality_proofs:INEQUALITY_PROOFS.1) counter = (
((error "Too few self-inequality proofs"))
),
make_self_requirements_2 funcname (branch:BRANCH.1) (branch_list:BRANCH_LIST) (self_inequality_proofs:INEQUALITY_PROOFS) counter = (
((make_self_requirements funcname branch_list self_inequality_proofs counter))
),
make_self_requirements funcname (branch_list:BRANCH_LIST.0) (self_inequality_proofs:INEQUALITY_PROOFS) counter = (
((make_self_requirements_2 funcname branch_list.branch branch_list.rest self_inequality_proofs counter))
),
make_self_requirements funcname (branch_list:BRANCH_LIST.1) (self_inequality_proofs:INEQUALITY_PROOFS.1) counter = (
((make_self_requirement funcname branch_list.branch self_inequality_proofs.proof counter))
),
make_self_requirements funcname (branch_list:BRANCH_LIST.1) (self_inequality_proofs:INEQUALITY_PROOFS.0) counter = (
((error "Too many self-inequality proofs"))
),
;
proofsyntax
( unwrap2 (funcname:IDENT).(counter:IDENT) (innerproof) ) =
( ( _def_((funcname))_((counter)) > eq_ltr ) < ( ((innerproof)) ) );
proofsyntax
( wrap2 (funcname:IDENT).(counter:IDENT) (innerproof) ) =
( ( _def_((funcname))_((counter)) > eq_rtl) < ( ((innerproof)) ) );
proofsyntax
( defeq2 (funcname:IDENT).(counter:IDENT) ) =
( _def_((funcname))_((counter)) );
enum UINT {
UINT_ZERO,
UINT_SUCC prev | prev : UINT,
};
require impl_same proves forany a: a -> a
by (
forany a:
assume A proves a;
A
);
require impl_reverse proves forany a,b: (a -> b) -> (!b -> !a)
by (
forany a,b:
assume AB proves a -> b;
assume BF proves b -> FALSE; // !b
assume A proves a;
(A > AB) > BF
);
require impl_not_not proves forany a: a -> !!a
by (
forany a:
assume A proves a;
assume NA proves (a -> FALSE);
A > NA
);
require not_not_eq proves forany a: ((a -> FALSE) -> FALSE) == a
by (
wrap eq (impl_impl_and < not_not_impl < impl_not_not)
);
require left_impl_not_right__not_and proves forany a,b: (a -> !b) -> !(a && b)
by (
forany a,b:
assume a_nb proves a -> !b;
assume a_and_b proves a && b;
a_nb < (a_and_b > and_left) < (a_and_b > and_right)
);
require right_impl_not_left__not_and proves forany a,b: (b -> !a) -> !(a && b)
by (
forany a,b:
assume b_na proves b -> !a;
assume a_and_b proves a && b;
b_na < (a_and_b > and_right) < (a_and_b > and_left)
);
require yay_or_nay proves forany a: a || !a
by (
forany aa:
require temp proves !(!aa && !!aa)
by (substitute a=!aa in impl_not_not) > left_impl_not_right__not_and;
wrap or temp
);
require or__not_left__right proves forany a,b: a || b -> !a -> b
by (
forany a,b:
assume A_OR_B proves a || b;
assume NA proves !a;
require A_OR_B_ proves !(!a && !b)
by unwrap or A_OR_B;
not_not_impl < (
// Goal:
// !!b
assume NB proves !b;
A_OR_B_ < (NB > NA > impl_impl_and)
)
);
require or__not_right__left proves forany a,b: a || b -> !b -> a
by (
forany a,b:
assume A_OR_B proves a || b;
assume NB proves !b;
require A_OR_B_ proves !(!a && !b)
by unwrap or A_OR_B;
not_not_impl < (
// Goal:
// !!a
assume NA proves !a;
A_OR_B_ < (NB > NA > impl_impl_and)
)
);
require impl_weaken proves forany a,b: a -> (b -> a)
by (
forany a,b:
assume A proves a;
assume _ proves b;
A
);
require impl_trans proves forany a,b,c: (a -> b) -> (b -> c) -> (a -> c)
by (
forany a,b,c:
assume AB proves a -> b;
assume BC proves b -> c;
assume A proves a;
(A > AB) > BC
);
require impl_impl_impl__and_impl proves forany a,b,c: (a -> b -> c) -> (a && b -> c)
by (
forany a,b,c:
assume abc proves a -> b -> c;
assume ab proves a && b;
(ab > and_right) > (ab > and_left) > abc
);
require impl_reverse_back proves forany a,b: (!b -> !a) -> (a -> b)
by (
forany a,b:
assume NB_NA proves !b -> !a;
assume A proves a;
((A > impl_not_not) > (NB_NA > impl_reverse)) > not_not_impl
);
require or_cases proves forany a,b,c: a || b -> (a -> c) -> (b -> c) -> c
by (
forany a,b,c:
assume ab proves a || b;
assume a_c proves a -> c;
assume b_c proves b -> c;
require nc_na proves !c -> !a by a_c > impl_reverse;
require nc_nb proves !c -> !b by b_c > impl_reverse;
not_not_impl < (
// Goal:
// !!c
assume nc proves !c;
// Goal:
// FALSE
(unwrap or ab) < (
// Goal:
// !a && !b
impl_impl_and < (nc > nc_na) < (nc > nc_nb)
)
)
);
require by_contradiction proves forany a: (a -> !a) -> !a
by (
forany a:
assume A_NA proves a -> !a;
assume A proves a;
A > (A > A_NA)
);
require by_contradiction_2 proves forany a: (!a -> a) -> a
by (
forany a:
assume NA_A proves !a -> a;
NA_A > impl_same > yay_or_nay > or_cases
);
require eq_same proves forany a: a == a
by (
wrap eq (impl_same > impl_same > impl_impl_and)
);
require wrap_in_func_impl proves forany f,a,b: a == b -> (f a) == (f b)
by (
forany f,a,b:
assume AB proves eq a b;
AB > eq_same > ((unwrap eq func_eq) > and_left)
);
require lhs_rhs_eq proves forany f,g,a,b: f == g -> a == b -> (f a) == (g b)
by (
(unwrap eq func_eq) > and_left
);
require bin_sub_left_impl proves forany f,a,b,x: a == b -> f a x -> f b x
by (
forany f,a,b,x:
assume AB proves eq a b;
assume FAX proves f a x;
require FA_FB proves eq (f a) (f b) by AB > eq_same > lhs_rhs_eq;
FAX > ((unwrap eq (eq_same > FA_FB > lhs_rhs_eq)) > and_left)
);
require bin_sub_left_eq proves forany f,a,b,x: a == b -> (f a x) == (f b x)
by (
forany f,a,b,x:
assume AB proves eq a b;
eq_same > (AB > (substitute f=f in wrap_in_func_impl)) > lhs_rhs_eq
);
require bin_sub_right_impl proves forany f,a,b,x: a == b -> f x a -> f x b
by (
forany f,a,b,x:
assume AB proves eq a b;
assume FXA proves f x a;
FXA > (unwrap eq (AB > eq_same > lhs_rhs_eq) > and_left)
);
require bin_sub_right_eq proves forany f,a,b,x: a == b -> (f x a) == (f x b)
by (
forany f,x,a,b:
assume AB proves eq a b;
AB > (substitute a=(f x) in eq_same) > lhs_rhs_eq
);
require un_sub_arg proves forany f,a,b: a == b -> (f a) == (f b)
by wrap_in_func_impl;
require wrap_in_bin_func_lhs proves forany f,a,b,c: a == b -> (f a c) == (f b c)
by (
forany f,a,b,c:
assume ab proves eq a b;
(substitute a=(f a c) in eq_same) > (ab > bin_sub_left_eq) > bin_sub_right_impl
);
require wrap_in_bin_func_rhs proves forany f,a,b,c: a == b -> (f c a) == (f c b)
by (
forany f,a,b,c:
assume ab proves eq a b;
(substitute a=(f c a) in eq_same) > (ab > bin_sub_right_eq) > bin_sub_right_impl
);
require and_comm_impl proves forany a,b: a && b -> b && a
by (
forany a,b:
assume AB proves AND a b;
(AB > and_left) > ((AB > and_right) > impl_impl_and)
);
require and_comm_eq proves forany a,b: (a && b) == (b && a)
by wrap eq ( impl_impl_and < and_comm_impl < and_comm_impl );
require not_left__not_and proves forany a,b: !a -> !(a && b)
by (
forany a,b:
assume NA proves a -> FALSE;
assume AB proves AND a b;
(AB > and_left) > NA
);
require not_right__not_and proves forany a,b: !b -> !(a && b)
by (
forany a,b:
assume NB proves b -> FALSE;
assume AB proves AND a b;
(AB > and_right) > NB
);
require and_same proves forany a: (a && a) == a
by (
forany a:
require ltr proves (AND a a) -> a by and_left;
require rtl proves a -> (AND a a) by (
assume A proves a;
A > A > impl_impl_and
);
wrap eq (rtl > ltr > impl_impl_and)
);
require not_and__left_impl_not_right proves forany a,b: !(a && b) -> a -> !b
by (
forany a,b:
assume not_ab proves !(a && b);
assume A proves a;
assume B proves b;
not_ab < (impl_impl_and < A < B)
);
require not_and__right_impl_not_left proves forany a,b: !(a && b) -> b -> !a
by (
forany a,b:
assume not_ab proves !(a && b);
assume B proves b;
assume A proves a;
not_ab < (impl_impl_and < A < B)
);
require eq_ltr proves forany a,b: a == b -> (a -> b)
by (
forany a,b:
assume AeqB proves a == b;
(unwrap eq AeqB) > and_left
);
require eq_rtl proves forany a,b: a == b -> (b -> a)
by (
forany a,b:
assume AeqB proves a == b;
(unwrap eq AeqB) > and_right
);
require eq_comm proves forany a,b: a == b -> b == a
by (
forany a,b:
assume A_eq_B proves a == b;
wrap eq ((unwrap eq A_eq_B) > and_comm_impl)
);
require eq_comm_eq proves forany a,b: (a == b) == (b == a)
by (
forany a,b:
wrap eq (impl_impl_and < eq_comm < eq_comm)
);
require eq_trans proves forany a,b,c: a == b -> b == c -> a == c
by (
forany a,b,c:
assume A_eq_B proves eq a b;
assume B_eq_C proves eq b c;
A_eq_B > B_eq_C > bin_sub_right_impl
);
require neq_comm proves forany a,b: a != b -> b != a
by (
forany a,b:
assume ab proves a != b;
assume ba proves b == a;
ab < (ba > eq_comm)
);
require neq_same proves forany a: !(a != a)
by eq_same > impl_not_not;
require not_impl__or proves forany a,b: (!a -> b) -> a || b
by (
forany a,b:
assume NA_B proves !a -> b;
wrap or (
assume NA_AND_NB proves !a && !b;
(NA_AND_NB > and_left) > ((NA_AND_NB > and_right) > (NA_B > impl_reverse))
)
);
require or_left proves forany a,b: a -> a || b
by (
forany a,b:
assume A proves a;
wrap or (
assume NA_and_NB proves !a && !b;
A > (NA_and_NB > and_left)
)
);
require or_right proves forany a,b: b -> a || b
by (
forany a,b:
assume B proves b;
wrap or (
assume NA_and_NB proves !a && !b;
B > (NA_and_NB > and_right)
)
);
require or_impl_left proves forany a,b,c: ((a || b) -> c) -> (a -> c)
by (
forany a,b,c:
assume OR_AB_C proves (a || b) -> c;
assume A proves a;
((A > or_left) > OR_AB_C)
);
require or_impl_right proves forany a,b,c: ((a || b) -> c) -> (b -> c)
by (
forany a,b,c:
assume OR_AB_C proves (a || b) -> c;
assume B proves b;
((B > or_right) > OR_AB_C)
);
require or_comm_impl proves forany a,b: a || b -> b || a
by (
forany a,b:
assume A_OR_B proves a || b;
require A_IMPL_B_OR_A proves a -> b || a by or_right;
require B_IMPL_B_OR_A proves b -> b || a by or_left;
B_IMPL_B_OR_A > A_IMPL_B_OR_A > A_OR_B > or_cases
);
require or_comm_eq proves forany a,b: eq (or a b) (or b a)
by wrap eq ( impl_impl_and < or_comm_impl < or_comm_impl );
require false_false__not_or proves forany a,b: !a -> !b -> !(a || b)
by (
forany a,b:
assume NA proves !a;
assume NB proves !b;
assume OR_AB proves or a b;
require OR_AB_ proves (AND !a !b) -> FALSE
by unwrap or OR_AB;
(NB > NA > impl_impl_and) > OR_AB_
);
syntax (a++) = UINT_SUCC a, precedence 20000, associativity left;
print _UINT_has_member_UINT_ZERO;
print _UINT_has_member_UINT_SUCC;
require zero_is_uint proves UINT_ZERO : UINT by _UINT_has_member_UINT_ZERO;
require succ_uint_is_uint proves forany a: (a : UINT) -> HAS_MEMBER UINT (UINT_SUCC a) by
(forany a: assume auint proves a : UINT; _UINT_has_member_UINT_SUCC < auint);
require succ_not_zero proves forany a: a : UINT -> (UINT_SUCC a) != UINT_ZERO
by (
forany a:
assume auint proves a : UINT;
(_neq_UINT_UINT_ZERO_UINT_SUCC < auint) > neq_comm
);
require uint_is_zero_or_succ_new proves forany a: a : UINT -> or (eq a UINT_ZERO) ((forany b: (HAS_MEMBER UINT b && (eq a (UINT_SUCC b)) -> FALSE)) -> FALSE) by (
forany a:
assume auint proves a : UINT;
(auint > _UINT_is_one_of) > (not_not_eq > bin_sub_left_impl)
);
require uint_is_zero_or_succ proves forany a: a : UINT -> or (eq a UINT_ZERO) ((forany b: (HAS_MEMBER UINT b -> (eq a (UINT_SUCC b)) -> FALSE)) -> FALSE) by (
forany a:
assume auint proves a : UINT;
or_cases < (uint_is_zero_or_succ_new < auint) < (
assume ass proves eq a UINT_ZERO;
ass > or_left
) < (
assume ass proves (forany b: (HAS_MEMBER UINT b && (eq a (UINT_SUCC b)) -> FALSE)) -> FALSE;
or_right < (
// Goal:
// (forany b: (HAS_MEMBER UINT b -> (eq a (UINT_SUCC b)) -> FALSE)) -> FALSE
assume ass2 proves forany b: HAS_MEMBER UINT b -> (eq a (UINT_SUCC b)) -> FALSE;
// Goal: FALSE
ass < (
// Goal:
// forany b: HAS_MEMBER UINT b && (eq a (UINT_SUCC b)) -> FALSE
forany b:
assume ass3 proves HAS_MEMBER UINT b && (eq a (UINT_SUCC b));
// Goal: FALSE
ass2 < (
ass3 > and_left
) < (
// Goal:
// (eq a (UINT_SUCC b))
ass3 > and_right
)
)
)
)
);
assume uint_inductive proves forany a,P: P UINT_ZERO -> (forany b: (b : UINT) -> P b -> P (UINT_SUCC b)) -> (a : UINT) -> P a;
assume uint_succ_injective proves forany a,b: a : UINT -> b : UINT -> a++ == b++ -> a == b;
define UINT_ONE = UINT_SUCC UINT_ZERO;
define UINT_TWO = UINT_SUCC UINT_ONE;
define UINT_PRED {
a: (UINT_SUCC a) | a : UINT = a;
;
(
forany a1, a2:
assume a1_not_a2 proves a1 != a2;
assume a1uint proves a1 : UINT;
assume a2uint proves a2 : UINT;
((uint_succ_injective < a1uint < a2uint) > impl_reverse) < a1_not_a2
);
};
require uint_pred proves forany a: (a : UINT) -> eq (UINT_PRED (UINT_SUCC a)) a by (
forany a:
assume auint proves a : UINT;
eq_same > (defeq2 UINT_PRED.x < auint) > bin_sub_right_impl
);
define UINT_ADD {
a : a UINT_ZERO | a : UINT = a,
a,b: a (UINT_SUCC b) | (a : UINT) && (b : UINT) = UINT_SUCC (UINT_ADD a b);
(
forany a1,a2,b2:
assume condition_1 proves a1 : UINT;
assume condition_2 proves (a2 : UINT) && (b2 : UINT);
(_neq_UINT_UINT_ZERO_UINT_SUCC < (condition_2 > and_right)) > or_right
);
(
forany a1, a2:
assume a1_not_a2 proves a1 != a2;
assume a1uint proves a1 : UINT;
assume a2uint proves a2 : UINT;
or_left < a1_not_a2
), (
forany a1, b1, a2, b2:
assume a1_not_a2 proves a1 != a2;
assume b1_not_b2 proves b1 != b2;
assume a1b1uint proves (a1 : UINT) && (b1 : UINT);
assume a2b2uint proves (a2 : UINT) && (b2 : UINT);
or_left < a1_not_a2
);
};
syntax (a + b) = UINT_ADD a b, precedence 200, associativity left;
define UINT_MUL {
a: a UINT_ZERO | a : UINT = UINT_ZERO,
a,b: a (UINT_SUCC b) | (a : UINT) && (b : UINT) = (UINT_ADD (UINT_MUL a b) a);
(
forany a1,a2,b2:
assume condition_1 proves a1 : UINT;
assume condition_2 proves (a2 : UINT) && (b2 : UINT);
(_neq_UINT_UINT_ZERO_UINT_SUCC < (condition_2 > and_right)) > or_right
);
(
forany a1, a2:
assume a1_not_a2 proves a1 != a2;
assume a1uint proves a1 : UINT;
assume a2uint proves a2 : UINT;
or_left < a1_not_a2
), (
forany a1, b1, a2, b2:
assume a1_not_a2 proves a1 != a2;
assume b1_not_b2 proves b1 != b2;
assume a1b1uint proves (a1 : UINT) && (b1 : UINT);
assume a2b2uint proves (a2 : UINT) && (b2 : UINT);
or_left < a1_not_a2
);
};
syntax (a * b) = UINT_MUL a b, precedence 210, associativity left;
define UINT_POW {
a: a UINT_ZERO | a : UINT = UINT_ONE,
a,b: a (UINT_SUCC b) | (a : UINT) && (b : UINT) = (UINT_MUL (UINT_POW a b) a);
(
forany a1,a2,b2:
assume condition_1 proves a1 : UINT;
assume condition_2 proves (a2 : UINT) && (b2 : UINT);
(_neq_UINT_UINT_ZERO_UINT_SUCC < (condition_2 > and_right)) > or_right
);
(