forked from acl2/acl2
-
Notifications
You must be signed in to change notification settings - Fork 0
/
rewrite.lisp
17874 lines (15605 loc) · 792 KB
/
rewrite.lisp
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
; ACL2 Version 8.1 -- A Computational Logic for Applicative Common Lisp
; Copyright (C) 2018, Regents of the University of Texas
; This version of ACL2 is a descendent of ACL2 Version 1.9, Copyright
; (C) 1997 Computational Logic, Inc. See the documentation topic NOTE-2-0.
; This program is free software; you can redistribute it and/or modify
; it under the terms of the LICENSE file distributed with ACL2.
; This program is distributed in the hope that it will be useful,
; but WITHOUT ANY WARRANTY; without even the implied warranty of
; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
; LICENSE for more details.
; Written by: Matt Kaufmann and J Strother Moore
; email: [email protected] and [email protected]
; Department of Computer Science
; University of Texas at Austin
; Austin, TX 78712 U.S.A.
(in-package "ACL2")
; We start our development of the rewriter by coding one-way-unify and the
; substitution fns.
; Essay on Equivalence, Refinements, and Congruence-based Rewriting
; (Note: At the moment, the fact that fn is an equivalence relation is encoded
; merely by existence of a non-nil 'coarsenings property. No :equivalence rune
; explaining why fn is an equivalence relation is to be found there -- though
; such a rune does exist and is indeed found among the 'congruences of fn
; itself. We do not track the use of equivalence relations, we just use them
; anonymously. It would be good to track them and report them. When we do
; that, read the Note on Tracking Equivalence Runes in subst-type-alist1.)
; (Note: Some of the parenthetical remarks in this code are extremely trite
; observations -- to the ACL2 aficionado -- added when I sent this commented
; code off to friends to read.)
; We will allow the user to introduce new equivalence relations. At the
; moment, they must be functions of two arguments only. Parameterized
; equivalence relations, e.g., x == y (mod n), are interesting and may
; eventually be implemented. But in the spirit of getting something done right
; and working, we start simple.
; An equivalence relation here is any two argument function that has been
; proved to be Boolean, symmetric, reflexive, and transitive. The rule-class
; :EQUIVALENCE indicates that a given theorem establishes that equiv is an
; equivalence relation. (In the tradition of Nqthm, the ACL2 user tells the
; system how to use a theorem when the theorem is submitted by the user. These
; instructions are called "rule classes". A typical "event" might therefore
; be:
; (defthm set-equal-is-an-equivalence-rel
; (and (booleanp (set-equal x y))
; (set-equal x x)
; (implies (set-equal x y) (set-equal y x))
; (implies (and (set-equal x y)
; (set-equal y z))
; (set-equal x z)))
; :rule-classes :EQUIVALENCE)
; The rule class :EQUIVALENCE just alerts the system that this formula states
; that something is an equivalence relation. If the formula is proved, the
; system identifies set-equal as the relation and adds to the database certain
; information that enables the processing described here.)
; The Boolean requirement is imposed for coding convenience. In
; assume-true-false, for example, when we assume (equiv x y) true, we simply
; give it the type-set *ts-t*, rather than something complicated like its full
; type-set take away *ts-nil*. In addition, the Boolean requirement means that
; (equiv x y) is equal to (equiv y x) (not just propositionally) and hence we
; can commute it at will. The other three requirements are the classic ones
; for an equivalence relation. All three are exploited. Symmetry is used to
; justify commutativity, which currently shows up in assume-true-false when we
; put either (equiv x y) or (equiv y x) on the type-alist -- depending on
; term-order -- and rely on it to assign the value of either. Reflexivity is
; used to eliminate (equiv x term) as a hypothesis when x does not occur in
; term or elsewhere in the clause. Transitivity is used throughout the
; rewriting process. These are not guaranteed to be all the places these
; properties are used!
; Note: Some thought has been given to the idea of generalizing our work to
; non-symmetric reflexive and transitive relations. We have seen occasional
; utility for the idea of rewriting with such a monotonic relation, replacing a
; term by a stronger or more defined one. But to implement that we feel it
; should be done in a completely independent second pass in which monotonic
; relations are considered. Equivalence relations are of such importance that
; we did not want to risk doing them weakly just to allow this esoteric
; variant.
; Note: We explicitly check that an equivalence relation has no guard because
; we never otherwise consider their guards. (The "guard" on an ACL2 function
; can be thought of as a "precondition" or a characterization of the domain of
; the function definition. In Common Lisp many functions, e.g., car and cdr,
; are not defined everywhere and guards are our way of taking note of this.
; Equivalence relations have "no" guard, meaning their guard is t, i.e., they
; are defined everywhere.)
; The motivation behind equivalence relations is to allow their use as :REWRITE
; rules. For example, after set-equal has been proved to be an equivalence
; relation and union-eq, say, has been proved to be commutative (wrt
; set-equal),
; (implies (and (symbol-listp a)
; (true-listp a)
; (symbol-listp b)
; (true-listp b))
; (set-equal (union-eq a b) (union-eq b a)))
; then we would like to be able to use the above rule as a rewrite rule to
; commute union-eq expressions. Of course, this is only allowed in situations
; in which it is sufficient to maintain set-equality as we rewrite. Implicit
; in this remark is the idea that the rewriter is given an equivalence relation
; to maintain as it rewrites. This is a generalization of id/iff flag in
; Nqthm's rewriter; that flag indicates whether the rewriter is maintaining
; identity or propositional equivalence. :CONGRUENCE lemmas, discussed later,
; inform the rewriter of the appropriate relations to maintain as it steps from
; (fn a1 ... an) to the ai. But given a relation to maintain and a term to
; rewrite, the rewriter looks at all the :REWRITE rules available and applies
; those that maintain the given relation.
; For example, suppose the rewriter is working on (memb x (union-eq b a)),
; where memb is a function that returns t or nil according to whether its first
; argument is an element of its second. Suppose the rewriter is to maintain
; identity during this rewrite, i.e., it is to maintain the equivalence
; relation equal. Suppose a :CONGRUENCE rule informs us that equal can be
; preserved on memb expressions by maintaining set-equal on the second
; argument. Then when rewriting the second argument to the memb, rewrite
; shifts from maintaining equal to maintaining set-equal. This enables it to
; use the above theorem as a rewrite rule, replacing (union-eq b a) by
; (union-eq a b), just as Nqthm would had the connecting relation been equal
; instead of set-equal.
; This raises the problem of refinements. For example, we may have some rules
; about union-eq that are expressed with equal rather than set-equal. For
; example, the definition of union-eq is an equality! It is clear that a rule
; may be tried if its connecting equivalence relation is a refinement of the
; one we wish to maintain. By ``equiv1 is a refinement of equiv2'' we mean
; (implies (equiv1 x y) (equiv2 x y)).
; Such rules are called :REFINEMENT rules and are a distinguished rule-class,
; named :REFINEMENT. Every equivalence relation is a refinement of itself.
; Equal is a refinement of every equivalence relation and no other relation is
; a refinement of equal.
; Every equivalence relation, fn, has a non-nil value for the property
; 'coarsenings. The value of the property is a list of all equivalence
; relations (including fn itself) known to admit fn as a refinement. This list
; is always closed under the transitivity of refinement. That is, if e1 is a
; refinement of e2 and e2 is a refinement of e3, then the 'coarsenings for e1
; includes e1 (itself), e2 (of course), and e3 (surprise!). This makes it
; easier to answer quickly the question of who is a refinement of whom.
; Equivalence relations are the only symbols with non-nil 'coarsenings
; properties, thus this is the way they are recognized. Furthermore, the
; 'coarsenings property of 'equal will always list all known equivalence
; relations.
; When we are rewriting to maintain equiv we use any rule that is a known
; refinement of equiv. Thus, while rewriting to maintain set-equal we can use
; both set-equal rules and equal rules.
; Now we move on to the heart of the matter: knowing what relation to maintain
; at each step. This is where :CONGRUENCE rules come in.
; To understand the key idea in congruence-based rewriting, consider lemmas of
; the form
; (implies (equiv1 x y)
; (equiv2 (fn a1 ... x ... an)
; (fn a1 ... y ... an))),
; where equiv1 and equiv2 are equivalence relations, the ai, x, and y are
; distinct variables and x and y occur in the kth argument position of the
; n-ary function fn. These lemmas can be used to rewrite fn-expressions,
; maintaining equiv2, by rewriting the kth argument position maintaining
; equiv1. In the separate Essay on Patterned Congruences and Equivalences we
; generalize to what we call "patterned congruence rules", but in this Essay we
; focus only on lemmas of the form above.
; We call such a lemma a ``congruence lemma'' and say that it establishes that
; ``equiv2 is maintained by equiv1 in the kth argument of fn.'' The rule-class
; :CONGRUENCE indicates when a lemma is to be so used.
; An example :CONGRUENCE lemma is
; (implies (set-equal a b) (iff (member x a) (member x b))).
; (In my previous example I used memb. Here I use member, the Common Lisp
; function. When member succeeds, it returns the tail of its second arg that
; starts with its first. Thus, (member x a) is not necessary equal to (member
; x b), even when a and b are set-equal. But they are propositionally
; equivalent, i.e., mutually nil or non-nil. Iff is just another equivalence
; relation.)
; That is, iff is maintained by set-equal in the second argument of member.
; Thus, when rewriting a member expression while trying to maintain iff it is
; sufficient merely to maintain set-equivalence on the second argument of
; member. In general we will sweep across the arguments of a function
; maintaining an appropriate equivalence relation for each argument as a
; function of the relation we wish to maintain outside.
; A literal interpretation of the lemma above suggests that one must maintain
; identity on the first argument of member in order to rely on the lemma in the
; second argument. What then justifies our independent use of :CONGRUENCE
; lemmas in distinct argument positions?
; Congruence Theorem 1. :CONGRUENCE lemmas for different argument positions of
; the same function can be used independently. In particular, suppose equiv is
; maintained by e1 in the kth argument of fn and equiv is maintained by e2 in
; the jth argument of fn, where j is not k. Suppose a is e1 to a' and b is e2
; to b'. Then (fn ...a...b...) is equiv to (fn ...a'...b'...), where a and b
; occur in the kth and jth arguments, respectively.
; Proof. By the :CONGRUENCE lemma for equiv and e1 we know that (fn
; ...a...b...) is equiv (fn ...a'...b...). By the :CONGRUENCE lemma for equiv
; and e2 we know that (fn ...a'...b...) is equiv to (fn ...a'...b'...). The
; desired result is then obtained via the transitivity of equiv. Q.E.D.
; Again, we are not considering patterned congruences in the present Essay.
; For the proof above it is important that in the :CONGRUENCE lemma, each
; argument of a call of fn is a distinct variable.
; While we require the user to formulate (non-patterned) :CONGRUENCE lemmas as
; shown above we actually store them in a data structure, called the
; 'congruences property of fn, in which lemmas for different slots have been
; combined. Indeed, we ``generalize'' still further and allow for more than
; one way to rewrite a given argument position. If fn has arity n, then the
; 'congruences property of fn is a list of tuples, each of which is of the form
; (equiv slot1 slot2 ... slotn), where equiv is some equivalence relation and
; each slotk summarizes our knowledge of what is allowed in each argument slot
; of fn while maintaining equiv. The entire n+1 tuple is assembled from many
; different :CONGRUENCE lemmas. Indeed, it is modified each time a new
; :CONGRUENCE lemma is proved about fn and equiv. Without discussing yet the
; structure of slotk, such a tuple means:
; (implies (and (or (equiv1.1 x1 y1)
; ...
; (equiv1.i x1 y1))
; ...
; (or (equivn.1 xn yn)
; ...
; (equivn.j xn yn)))
; (equiv (fn x1 ... xn)
; (fn y1 ... yn))).
; Thus, to rewrite (fn x1 ... xn) maintaining equiv we sweep across the
; arguments rewriting each in turn, maintaining any one of the corresponding
; equivk.l's, which are encoded in the structure of slotk.
; Note that each equivk,l above is attributable to one and only one :CONGRUENCE
; lemma. Since the ors cause searching, we allow the user to control the
; search by disabling :CONGRUENCE lemmas. We only pursue paths introduced by
; enabled lemmas.
; The structure of slotk is a list of ``congruence-rules'', which are instances
; of the following record.
(defrec congruence-rule (nume equiv . rune) t)
; The :equiv field is the function symbol of an equivalence relation which, if
; maintained in argument k, is sufficient to maintain equiv for the
; fn-expression; :rune (it stands for "rule name") is the name of the
; :CONGRUENCE lemma that established this link between equiv, :equiv, fn, and
; k; and :nume is the nume of the rune (a "nume" is a unique natural number
; corresponding to a rune, used only to speed up the answer to the question:
; "is the named rule enabled -- i.e., among those the user permits us to apply
; automatically?"), allowing us to query the enabled structure directly.
; Because we allow more than one :CONGRUENCE rule per argument, we have a
; problem. If we are trying to maintain equiv for fn and are rewriting an
; argument whose slot contains (equivk.1 ... equivk.l), what equivalence
; relation do we try to maintain while rewriting the argument? We could
; iteratively try them each, rewriting the argument l times. This suffers
; because some rules would be tried many times due to our use of refinements.
; For example, all of the equality rules would be tried for each equivk.i
; tried.
; It is desirable to eliminate the need for more than one pass through rewrite.
; We would like to rewrite once. But if we pass the whole set in, with the
; understanding that any refinement of any of them can be used, we are not
; assured that the result of rewrite is equivalent in any of those senses to
; the input. The reason is that rewrite may recursively rewrite its
; intermediate answer. (If our rewriter simplifies a to a' it may then rewrite
; a' to a''.) Thus, a may rewrite to a' maintaining equivk.1 and then a' may
; rewrite to a'' maintaining equivk.2 and it may be that a is not equivalent to
; a'' in either the equivk.1 or equivk.2 sense. However, note that there
; exists an equivalence relation of which equivk.1 and equivk.2 are
; refinements, and that is the relation being maintained. Call that the
; ``generated relation.'' Numerous questions arise. Is the generated relation
; definable in the logic, for if so, perhaps we could allow only one
; equivalence relation per slot per fn and equiv and force the user to invent
; the necessary generalization of the several relations he wants to use.
; Furthermore, if both equivk.1 and equivk.2 maintain equiv in the kth slot of
; fn, does their generated relation maintain it? We need to know that the
; answer is ``yes'' if we are going to replace a by a'' (which are equivalent
; only in the generated sense) and still maintain the goal relation.
; We have taken the tack of allowing more than one :CONGRUENCE rule per slot by
; automatically (indeed, implicitly) dealing with the generated equivalence
; relations. To justify our code, we need a variety of theorems about
; generated relations. We state and prove those now.
; Let e1 and e2 be two binary relations. We define the relation s ``generated
; by e1 and e2,'' denoted {e1 e2}, as follows. Because order is unimportant
; below, our set notation {e1 e2} is acceptable.
; (s x y) iff there exists a finite sequence x1, x2, ..., xn such that x = x1,
; y = xn, and for all i, ((e1 xi xi+1) or (e2 xi xi+1)). We read this as
; saying ``(s x y) iff there is a chain connecting x to y composed entirely of
; e1 and/or e2 links.''
; Congruence Theorem 2. If e1 and e2 are equivalence relations, so is {e1 e2}.
; Proof. Let s be {e1 e2}. Then s is reflexive, symmetric, and transitive, as
; shown below.
; Reflexive. To show that (s x x) holds we must exhibit a sequence linking x
; to x via e1 and/or e2. The sequence x,x suffices.
; Symmetric. If (s x y) holds, then there exists a sequence linking x to y via
; e1 and/or e2 steps. Let that sequence be x, x2, ..., xk, y. By definition,
; either e1 or e2 links each pair. Since e1 is symmetric, if a pair, xi, xj,
; is linked by e1 then the pair xj, xi is also linked by e1. Similarly for e2.
; Thus, the sequence obtained by reversing that above, y, xk, ..., x2, x, has
; the desired property: each pair is linked by e1 or e2. Therefore, (s y x).
; Transitive. If (s x y) holds, then there exists a sequence linking x to y,
; say x, x2, ..., xk, y. If (s y z) holds, there exists a sequence linking y
; to z, say, y, y1, ..., yk, z. Consider the concatenation of those two
; sequences, x, x2, ..., xk, y, y, y1, ..., yk, z. It links x and z and every
; pair is linked by either e1 or e2. Thus, (s x z).
; Q.E.D.
; Thus, the relation generated by two equivalence relations is an equivalence
; relation.
; Congruence Theorem 3. If e1 and e2 are equivalence relations, they are both
; refinements of {e1 e2}.
; Proof. Let s be {e1 e2}. We wish to prove (implies (e1 x y) (s x y)) and
; (implies (e2 x y) (s x y)). We consider the first goal only. The second is
; symmetric. But clearly, if x is linked to y by e1 then (s x y) holds, as
; witnessed by the sequence x,y. Q.E.D.
; Congruence Theorem 4. Let equiv, e1 and e2 be equivalence relations.
; Suppose equiv is preserved by e1 in the kth argument of fn. Suppose equiv is
; also preserved by e2 in the kth argument of fn. Then equiv is preserved by
; {e1 e2} in the kth argument of fn.
; Proof. Let s be {e1 e2}. Without loss of generality we restrict our
; attention to a function, fn, of one argument. We have
; (implies (e1 x y) (equiv (fn x) (fn y)))
; and
; (implies (e2 x y) (equiv (fn x) (fn y)))
; We wish to prove
; (implies (s x y) (equiv (fn x) (fn y)))
; The hypothesis (s x y) establishes that there is a chain linking x to y via
; e1 and/or e2. Let that chain be x, x2, ..., xk, y. Since each adjacent pair
; is linked via e1 or e2, and both preserve equiv, we get that (equiv (fn x)
; (fn x2)), (equiv (fn x2) (fn x3)), ... (equiv (fn xk) (fn y)). By the
; transitivity of equiv, therefore, (equiv (fn x) (fn y)). Q.E.D.
; Lemma. If e1 is preserved by e in the kth argument of fn then so is {e1 e2},
; for any relation e2.
; Proof. We have that (e a b) implies (e1 (f ...a...) (f ...b...)). Let s be
; {e1 e2}. We wish to prove that (e a b) implies (s (f ...a...) (f ...b...)).
; But by Congruence Theorem 3 above, e1 is a refinement of s. Hence, (e1 (f
; ...a...) (f ...b...)) implies (s (f ...a...) (f ...b...)). Q.E.D.
; Congruence Theorem 5. Let e1, ..., e4 be equivalence relations. Then if e2
; is preserved by e1 in the kth argument of fn and e4 is preserved by e3 in the
; kth argument of fn, then {e2 e4} is preserved by {e1 e3} in the kth argument
; of fn.
; Proof. By the above lemma, we know {e2 e4} is preserved by e1 in the kth
; argument of fn. Similarly, {e2 e4} is preserved by e3 in the kth argument of
; fn. Thus, the hypotheses of Theorem 4 are satisfied and we have that {e2 e4}
; is preserved by {e1 e3} in the kth argument of fn. Q.E.D.
; We generalize the notion of the relation generated by two relations to that
; generated by n relations, {e1, e2, ..., en}. By the above results, {e1, ...,
; en} is an equivalence relation if each ei is, each ei is a refinement of it,
; and it supports any congruence that all ei support. We adopt the convention
; that the relation generated by {} is EQUAL and the relation denoted by {e1}
; is e1.
; In our code, generated equivalence relations are represented by lists of
; congruence-rules. Thus, if cr1 and cr2 are two instances of the
; congruence-rule record having :equivs e1 and e2 respectively, then {e1 e2}
; can be represented by '(cr1 cr2).
; The equivalence relation to be maintained by rewrite is always represented as
; a generated equivalence relation. In our code we follow the convention of
; always using a variant of the name ``geneqv'' for such an equivalence
; relation. When a variable contains (or is expected to contain) the name of
; an equivalence relation rather than a :CONGRUENCE rule or geneqv, we use a
; variant of the name ``equiv'' or even ``fn''.
; The geneqv denoting EQUAL is nil. The geneqv denoting IFF is:
(defconst *geneqv-iff*
(list (make congruence-rule
:rune *fake-rune-for-anonymous-enabled-rule*
:nume nil
:equiv 'iff)))
; This completes our general essay on the subject. The theorems proved above
; are mentioned by name elsewhere in our code. In addition, various details
; are discussed elsewhere. For a simple example of how all of this works
; together, see the function subst-equiv-expr which implements substitution of
; new for old in term to produce term', where it is given that new is equiv1
; old and term is to be equiv2 term'.
; We now turn to the most primitive functions for manipulating equivalences and
; generated equivalences. We deal with refinements first and then with the
; question of congruences.
(defun refinementp (equiv1 equiv2 wrld)
; Note: Keep this function in sync with refinementp1.
; (ACL2 is an applicative subset of Common Lisp. When this
; function, refinementp, is called, its third argument, wrld, will be
; the current "property list world" which is just an association
; list binding symbols and property names to values. The lookup of
; a symbol's property in wrld is via the ACL2 function getprop.
; Getprop is coded in a clever way so that in the case that the
; world is in fact that implicit in the global property list
; structure of Common Lisp, then getprop is just Common Lisp's
; non-applicative get. In our code, wrld is always that world,
; but the code works correctly -- if somewhat more slowly -- if
; called on a different world.)
; Both equiv1 and equiv2 are function symbols. We determine whether
; equiv1 is a known refinement of equiv2, given wrld. If we return t
; we must be correct. Nil means ``maybe not.'' For an explanation of
; why our database contains the 'coarsenings property instead of the
; inverse 'refinements property, see the discussion of
; geneqv-refinements below.
(cond ((eq equiv1 'equal)
; Equal is a refinement of all equivalence relations.
t)
((eq equiv2 'equal)
; No other relation is a refinement of equal.
nil)
((eq equiv1 equiv2)
; Every equivalence relation is a refinement of itself.
t)
(t
; Otherwise, look for equiv2 among the known coarsenings of equiv1.
; The database must be kept so that the transitive property of
; refinement is manifested explicitly. This function is called very
; often and we do not want to go searching through the transitive
; closure of refinementhood or coarseninghood. So if e1 is a known
; refinement of e2 and e2 is a known refinement of e3, then the
; 'coarsenings property of e1 must include not just e2 but also e3.
; We know the first element in the 'coarsenings of equiv1 is equiv1
; -- which isn't equiv2 -- so we skip it.
(member-eq equiv2
(cdr (getpropc equiv1 'coarsenings nil wrld))))))
; The above function determines if one equivalence symbol is a
; refinement of another. More often we want to know whether a symbol
; is a refinement of a generated equivalence relation. That is, is e1
; a refinement of {e2 e3}? The most common occurrence of this
; question is when we are maintaining {e2 e3} and want to know if we
; can apply a :REWRITE rule about e1.
(defun geneqv-refinementp1 (coarsenings geneqv)
; We determine whether any name in coarsenings is the :equiv of any
; :CONGRUENCE rule in geneqv. If so, we return the :rune of the rule
; found.
(cond ((null geneqv) nil)
((member-eq (access congruence-rule (car geneqv) :equiv)
coarsenings)
(access congruence-rule (car geneqv) :rune))
(t (geneqv-refinementp1 coarsenings (cdr geneqv)))))
(defun geneqv-refinementp (equiv geneqv wrld)
; We determine whether the equivalence relation symbol equiv is a
; known refinement of the generated relation geneqv. If so, we return
; the rune of the :CONGRUENCE rule in geneqv used, or
; *fake-rune-for-anonymous-enabled-rule* if equality was used.
; Otherwise we return nil.
; This function is used both as a function and a predicate. Its
; primary use is as a predicate, typically to determine whether it is
; permitted to use a :REWRITE rule whose top-level equivalence is
; equiv. If the function reports success and the rewrite in fact
; succeeds, the caller will typically use the value of the function as
; the rune of the :CONGRUENCE rule used, adding it into the tag-tree of
; the term being rewritten.
; Note: If the database contained only a 'refinements property for e2
; and e3, we would have to access both of them to determine whether e1
; was among the known refinements. But if the database contains a
; 'coarsenings property for e1 we can access just that and then look
; for e2 or e3 in it. This saves us doing unnecessary getprops.
; Historical Note: Once we passed around geneqvs that contained
; possibly disabled :CONGRUENCE rules and this function got, as an
; additional argument, the current enabled structure and had the job
; of ignoring those :CONGRUENCE rules. This proved cumbersome and we
; adopted the idea of passing around geneqvs that are fully enabled.
; It means, of course, filtering out the disabled components when we
; form new geneqvs from those in the database. In any case, this
; function does not get the enabled structure and takes no note of the
; status of any rule.
(cond ((eq equiv 'equal) *fake-rune-for-anonymous-enabled-rule*)
((null geneqv) nil)
(t (geneqv-refinementp1 (getpropc equiv 'coarsenings nil wrld)
geneqv))))
; We now define the function which constructs the list of generated
; equivalences to be maintained across the arguments of fn, as a
; function of the generated equivalence to be maintained overall and
; the current enabled structure. Our main concern, technically, here
; is to avoid consing. Most often, we expect that the list of geneqvs
; stored a given fn will be the list we are to return, because we will
; be trying to maintain just one primitive equivalence and we will
; know at most one way to do it for each arg, and none of the
; :CONGRUENCE rules are disabled. So we start with the function that
; filters out of the geneqv stored in slot k all of the disabled
; congruences -- and we code it so as to first check to see whether
; anything needs to be removed. Then we move up to the corresponding
; operation on a stored list of geneqvs. Finally, we consider the
; problem of unioning together the slot k's for all of the primitive
; equivalences to be maintained.
(defun some-congruence-rule-disabledp (geneqv ens)
(cond ((null geneqv) nil)
((enabled-numep (access congruence-rule (car geneqv) :nume) ens)
(some-congruence-rule-disabledp (cdr geneqv) ens))
(t t)))
(defun filter-geneqv1 (geneqv ens)
(cond ((null geneqv) nil)
((enabled-numep (access congruence-rule (car geneqv) :nume) ens)
(cons (car geneqv) (filter-geneqv1 (cdr geneqv) ens)))
(t (filter-geneqv1 (cdr geneqv) ens))))
(defun filter-geneqv (geneqv ens)
; Geneqv is a set (list) of :CONGRUENCE rules, generally retrieved from
; slot k of some equiv entry on some function's 'congruences. We
; return the subset consisting of the enabled ones. We avoid consing
; if they are all enabled.
(cond ((some-congruence-rule-disabledp geneqv ens)
(filter-geneqv1 geneqv ens))
(t geneqv)))
; Now we repeat this exercise one level higher, where we are dealing with
; a list of geneqvs.
(defun some-geneqv-disabledp (lst ens)
(cond ((null lst) nil)
((some-congruence-rule-disabledp (car lst) ens) t)
(t (some-geneqv-disabledp (cdr lst) ens))))
(defun filter-geneqv-lst1 (lst ens)
(cond ((null lst) nil)
(t (cons (filter-geneqv (car lst) ens)
(filter-geneqv-lst1 (cdr lst) ens)))))
(defun filter-geneqv-lst (lst ens)
; It is handy to allow ens to be nil, indicating that nothing is disabled.
(cond ((null ens)
lst)
((some-geneqv-disabledp lst ens)
(filter-geneqv-lst1 lst ens))
(t lst)))
; Next we must union together two lists of :CONGRUENCE rules. To keep
; the lists from getting large we will eliminate refinements. That
; is, if we have {e1 e2} U {e3 e4}, and e1 is a refinement of e3, but
; there is no refinement relation between e2, e3 and e4, then the
; answer will be {e2 e3 e4}. In general, we will assume the two lists
; are free of internal refinement relations and we will generate such
; a list. It is a little messy because e3 may be a refinement of e2,
; say. In which case the answer is {e2 e4}.
(defun refinementp1 (equiv1 coarsenings1 equiv2)
; Note: Keep this function in sync with refinementp.
; Both equiv1 and equiv2 are function symbols and coarsenings1 is the
; cdr of the 'coarsenings property of equiv1 (the car of that property
; is equiv1 itself). We determine whether equiv1 is a known
; refinement of equiv2. This function should be kept in sync with the
; more general refinementp.
(cond ((eq equiv1 'equal) t)
((eq equiv2 'equal) nil)
((eq equiv1 equiv2) t)
(t (member-eq equiv2 coarsenings1))))
(defun pair-congruence-rules-with-coarsenings (geneqv wrld)
; We pair each congruence rule in geneqv with non-id coarsenings,
; i.e., the cdr of the 'coarsenings property of its :equiv.
(cond
((null geneqv) nil)
(t (cons (cons (car geneqv)
(cdr (getpropc (access congruence-rule (car geneqv) :equiv)
'coarsenings nil wrld)))
(pair-congruence-rules-with-coarsenings (cdr geneqv) wrld)))))
(defun add-to-cr-and-coarsenings
(new-cr new-cr-coarsenings old-crs-and-coarsenings both-tests-flg)
; New-cr is a congruence rule and new-cr-coarsenings is the
; 'coarsenings property of its :equiv. Note that the car of
; new-cr-coarsenings is thus the :equiv name. Old-crs-and-coarsenings
; is a list of pairs of the form (congruence-rule . non-id-coarsenings).
; We assume no member of the old list refines any other member.
; We ``add'' the new pair (new-cr . non-id-new-cr-coarsenings) to the old
; list. However, if new-cr is a refinement of any equiv in the old
; list, we do nothing. Furthermore, if any member of the old list is
; a refinement of new-cr, we delete that member.
(cond
((null old-crs-and-coarsenings)
; Add the new-cr and its non-id coarsenings to the list.
(list (cons new-cr (cdr new-cr-coarsenings))))
((and both-tests-flg
(refinementp1
(car new-cr-coarsenings) ; new-equiv
(cdr new-cr-coarsenings) ; new-equiv's non-id coarsenings
(access congruence-rule ; first old-equiv
(car (car old-crs-and-coarsenings))
:equiv)))
; The new equiv is a refinement of the first old one. Nothing to do.
old-crs-and-coarsenings)
((refinementp1
(access congruence-rule ; first old-equiv
(car (car old-crs-and-coarsenings))
:equiv)
(cdr (car old-crs-and-coarsenings)) ; first old-equiv's non-id coarsenings
(car new-cr-coarsenings)) ; new-equiv
; The first old equiv is a refinement of the new one. Delete the old
; one. Continue inserting the new one -- it may cause other
; refinements to be deleted. But there is no possibility that it will
; be dropped because any old cr which it refines would have been
; refined by the one we just dropped. So we can henceforth only test for
; this case.
(add-to-cr-and-coarsenings new-cr new-cr-coarsenings
(cdr old-crs-and-coarsenings)
nil))
(t (cons (car old-crs-and-coarsenings)
(add-to-cr-and-coarsenings new-cr new-cr-coarsenings
(cdr old-crs-and-coarsenings)
both-tests-flg)))))
(defun union-geneqv1 (geneqv1 old-crs-and-coarsenings wrld)
; Geneqv1 is a geneqv and old-crs-and-coarsenings is a list of pairs
; of the form (congruence-rule . coarsenings), where the coarsenings
; are the non-id coarsenings of the :equiv of the corresponding
; congruence-rule. This data structure makes it possible to answer
; refinement questions without going back to the world. We scan down
; geneqv1 and augment old-crs-and-coarsenings, adding a new
; (congruence-rule . non-id-coarsenings) pair for each congruence rule in
; geneqv1 that is not a refinement of any rule already in the old set.
; In addition, if we find an old rule that is a refinement of some new
; one, we drop it from the old set, replacing it with the new one.
(cond
((null geneqv1) old-crs-and-coarsenings)
(t (union-geneqv1 (cdr geneqv1)
(add-to-cr-and-coarsenings (car geneqv1)
(getpropc
(access congruence-rule
(car geneqv1)
:equiv)
'coarsenings nil wrld)
old-crs-and-coarsenings
t)
wrld))))
(defun union-geneqv (geneqv1 geneqv2 wrld)
; We union together the congruence rules in the two geneqv's, forming
; a set with the property that no element in it is a refinement of any
; other. Roughly speaking we simply add the equivs of geneqv1 into
; those of geneqv2, not adding any that is a refinement and deleting
; any that is refined by a new one. To make this process faster we
; first annotate geneqv2 by pairing each congruence rule in it with
; the non-id 'coarsenings property of its :equiv. Union-geneqv1 does the
; work and returns such an annotated list of congruence rules. We
; convert that back into a geneqv by stripping out the annotations.
(strip-cars
(union-geneqv1
geneqv1
(pair-congruence-rules-with-coarsenings geneqv2 wrld)
wrld)))
; And now we do slotwise union.
(defun pairwise-union-geneqv (lst1 lst2 wrld)
; Lst1 and lst2 are lists of geneqvs that are in 1:1 correspondence.
; We pairwise union their elements.
(cond ((null lst1) nil)
(t (cons (union-geneqv (car lst1) (car lst2) wrld)
(pairwise-union-geneqv (cdr lst1) (cdr lst2) wrld)))))
; That brings us to the main function we've been wanting: the one that
; determines what generated equivalence relations must be maintained
; across the the arguments of fn in order to maintain a given
; generated equivalence relation for the fn-expression itself. Because
; we form new geneqvs from stored ones in the database, we have to
; have the enabled structure so we filter out disabled congruence
; rules.
(defun geneqv-lst1 (congruences geneqv ens wrld)
; Congruences is the list of congruences of a certain function, fn.
; Geneqv is a list of congruence-rules whose :equiv relations we are
; trying to maintain as we sweep across the args of fn. For each
; element of congruences, (equiv slot1 ... slotn), such that equiv is
; an element of geneqv we filter disabled rules out of each slot and
; then union together corresponding slots.
; In coding this, the following question arose. ``Should we include
; those equiv that are refinements of elements of geneqv or just those
; that are literally elements of geneqv?'' Our answer is ``include
; refinements.'' Suppose geneqv is {set-equal}. Suppose list-equal
; is a known refinement of set-equal. Suppose that for the fn in
; question we know a :CONGRUENCE rule that preserves list-equal but we
; know no rules that preserve set-equal. Then if we do not include
; refinements we will be fooled into thinking that the only way to
; preserve set-equal for the fn is to preserve equal across the args.
; But if we do include refinements we will know that we can admit
; whatever relations are known to maintain list-equal across the args.
(cond ((null congruences)
; This is a little subtle. We return nil where we ought to return a
; list of n nils. But it is ok. An optimization below (in which we
; avoid pairwise-union-geneqv when the second arg is nil) makes it
; clearly ok. But even without the optimization it is ok because
; pairwise-union-geneqv is controlled by its first arg!
nil)
(t (let ((ans (geneqv-lst1 (cdr congruences) geneqv ens wrld)))
(cond
((geneqv-refinementp (caar congruences) geneqv wrld)
(cond
((null ans)
(filter-geneqv-lst (cdar congruences) ens))
(t (pairwise-union-geneqv
(filter-geneqv-lst (cdar congruences) ens)
ans
wrld))))
(t ans))))))
; On the Optimization of Geneqv-lst
; Once upon a time we suspected that geneqv-lst might be causing a significant
; slowdown of ACL2 compared to Nqthm. So we tried the following experiment.
; First we ran the code on the Nqthm package and learned that geneqv-lst is
; called a total of 876843 times. The entire series of proofs took 1654
; seconds (on Rana, a Sparc 2). Then we recoded the function so that it saved
; every input and output and reran it on the proof of the Nqthm package to
; collect all io pairs. Analyzing the io pairs showed that we could reproduce
; the behavior of geneqv-lst on that series of proofs with the following code.
; Note that this does does not look at the property lists nor at the enabled
; structure. Nor does it do any consing.
; (defun geneqv-lst (fn geneqv ens wrld)
; (declare (ignore ens wrld))
; ; (setq geneqv-cnt (1+ geneqv-cnt))
; (cond
; ((and (eq fn 'IFF)
; (equal geneqv *geneqv-iff*))
; '(((NIL IFF :FAKE-RUNE-FOR-ANONYMOUS-ENABLED-RULE NIL))
; ((NIL IFF :FAKE-RUNE-FOR-ANONYMOUS-ENABLED-RULE NIL))))
; ((and (eq fn 'IMPLIES)
; (equal geneqv *geneqv-iff*))
; '(((NIL IFF :FAKE-RUNE-FOR-ANONYMOUS-ENABLED-RULE NIL))
; ((NIL IFF :FAKE-RUNE-FOR-ANONYMOUS-ENABLED-RULE NIL))))
; ((eq fn 'IF)
; (cond
; ((null geneqv)
; '(((NIL IFF :FAKE-RUNE-FOR-ANONYMOUS-ENABLED-RULE NIL))
; nil nil))
; ((equal geneqv *geneqv-iff*)
; '(((NIL IFF :FAKE-RUNE-FOR-ANONYMOUS-ENABLED-RULE NIL))
; ((NIL IFF :FAKE-RUNE-FOR-ANONYMOUS-ENABLED-RULE NIL))
; ((NIL IFF :FAKE-RUNE-FOR-ANONYMOUS-ENABLED-RULE NIL))))
; (t nil)))
; ((and (eq fn 'NOT)
; (equal geneqv *geneqv-iff*))
; '(((NIL IFF :FAKE-RUNE-FOR-ANONYMOUS-ENABLED-RULE NIL))))
; (t nil)))
; (Note: ((NIL IFF :FAKE-RUNE-FOR-ANONYMOUS-ENABLED-RULE NIL)) is just
; *geneqv-iff*.)
; Then we recompiled the entire ACL2 system with this definition in place (to
; ensure that the calls were all fast) and reran the Nqthm package proofs. The
; result was that it took 1668 seconds!
; Not wanting to believe these results (it seems so obvious that this function
; is inefficient!) we tried redefining geneqv-lst so that always returned nil.
; This is not the same behavior as the geneqv-lst below, but at least it is
; fast. The resulting proofs took 1780 seconds but investigation showed that
; some proofs followed different paths, so this experiment was discounted.
; Next, we simply remembered the complete sequence of answers generated by the
; code below (all 876843 of them) and then redefined the function to feed back
; those very answers in the same sequence. The answers were pushed into a
; stack during one run, the stack was reversed, and the answers were popped off
; during the second run. The code for geneqv-lst was simply (pop
; geneqv-stack). We cannot imagine a faster implementation. The second
; run took 1685 seconds.
; The conclusion of these experiments is that geneqv-lst is not likely to be
; optimized!
(defun geneqv-lst (fn geneqv ens wrld)
; Suppose we are attempting to rewrite a term whose function is fn while
; maintaining the generated equivalence relation geneqv. Fn may be a lambda
; expression. We return the list of generated equivalence relations to be
; maintained at each argument position. See the essay above for some
; experiments on the optimization of this function.
; For example, while rewriting a MEMBER expression, (MEMBER x s) to
; maintain IFF we should rewrite x maintaining EQUAL and rewrite s
; maintaining SET-EQUAL. That is, given MEMBER and IFF (for fn and
; geneqv) we wish to return (EQUAL SET-EQUAL), a list in 1:1
; correspondence with the formals of fn giving the equivalence
; relations that must be maintained for the arguments in order to
; maintain geneqv. However, rather than (EQUAL SET-EQUAL) we return a
; list of two geneqvs, namely '(nil (cr)), where cr is the congruence
; rule which establishes that IFF is maintained by SET-EQUAL in the
; 2nd arg of MEMBER.
; The fact that nil denotes the equivalence generated by 'EQUAL,
; combined with the facts that the car and cdr of nil are nil, allows
; us to return nil to denote a list of a suitable number of generated
; equalities. Thus, the answer nil is always correct and is in fact
; the answer returned for all those functions for which we know no
; :CONGRUENCE rules.
; If fn is a lambda-expression, we return nil. Otherwise, the
; 'congruences property of the symbol fn is an alist. The entries of
; the alist are of the form (equiv geneqv1 ... geneqvn). Consider the
; entry for each refinement of some :equiv in the goal geneqv, after
; filtering out the disabled rules from each:
; (equiv1 geneqv1,1 ... geneqv1,n)
; (equiv2 geneqv2,1 ... geneqv2,n)
; ...
; (equivk geneqvk,1 ... geneqvk,n)
; The union down the first column is geneqv. Let the union down
; subsequent columns be geneqv1, ... geneqvn. Then by Congruence
; Theorem 5, we have that geneqv is maintained by geneqvi in the ith
; argument of fn. Thus, we return (geneqv1 ... geneqvn).
; Observe that if some equivj in geneqv is not mentioned in the
; known congruences then we have, implicitly, the entry
; (equivj {} ... {}) and so its contribution to the union is
; justifiably ignored.
; Observe that if we throw away a disabled rule from a geneqvi,j we
; are just strengthening the equivalence relation to be maintained
; in that slot. Thus, our heuristic use of ens is sound.
; We allow ens to be nil, to signify that all rules are to be considered as
; enabled.
(cond ((flambdap fn) nil)
((eq fn 'if)
; IF is an unusual function symbol vis-a-vis congruence. We know that
; equality is preserved by iff in the 1st argument of IF. But more
; significantly, for every equivalence relation, equiv, we have that
; equiv is preserved by equiv in the 2nd and 3rd arguments of if.
; Thus, we could store a lot of congruences under IF, one for each
; equivalence relation: (equiv iff equiv equiv). Instead, we just
; manufacture it when we are asked. This is inefficient in that we
; may cons up the same structure repeatedly. But we do not suffer
; as much as one might think because the really heavy-duty users of
; geneqv-lst, e.g., rewrite, build in their handling of IF anyway and
; never call geneqv-lst on 'IF.
(list *geneqv-iff* geneqv geneqv))
(t (let ((congruences (getpropc fn 'congruences nil wrld)))
(cond
((null congruences) nil)
((null geneqv)
; This is a special case. If we are trying to maintain equality
; then the likelihood is that we have to maintain equality across
; the args, i.e., return nil. But it is possible that the congruences
; for fn lists 'equal explicitly. If so, we use those. Otherwise nil.
; But we have to filter for disabled rules.
(filter-geneqv-lst (cdr (assoc-eq 'equal congruences)) ens))
(t
; This is the general case in which the function has some known congruence
; relations and the equivalence relation we are trying to maintain is not just
; equality. In this case, we are prepared to to do some consing.
(geneqv-lst1 congruences geneqv ens wrld)))))))
; As an exercise in the use of the equivalence and congruence stuff, we
; now code the function that substitutes one term for another maintaining
; a given generated equivalence. We begin with elementary substitution
; because it illustrates the fundamental notion of substitution.
; Elementary Expression Substitution (``Equals for Equals'')
; Students of our code might find it helpful to look at subst-var
; before looking at the following.
; We show how to substitute one term, new, for another term, old,
; in a term. The presumption is that new and old are known to be
; equal. This might be used, for example, to substitute
; A for (CAR (CONS A B)) in (FOO (CAR (CONS A B))) to produce
; (FOO A).
(mutual-recursion
(defun subst-expr1 (new old term)
(declare (xargs :guard (and (pseudo-termp new)
(pseudo-termp old)
(pseudo-termp term))))
(cond ((equal term old) new)
((variablep term) term)
((fquotep term) term)
(t (cons-term (ffn-symb term)
(subst-expr1-lst new old (fargs term))))))
(defun subst-expr1-lst (new old args)
(declare (xargs :guard (and (pseudo-termp new)
(pseudo-termp old)
(pseudo-term-listp args))))
(cond ((endp args) nil)
(t (cons (subst-expr1 new old (car args))
(subst-expr1-lst new old (cdr args))))))
)
(defun subst-expr-error (const)
(declare (xargs :guard nil))
(er hard 'subst-expr-error
"An attempt was made to substitute for the explicit value ~x0. ~
The substitution functions were optimized to disallow this."
const))
(defun subst-expr (new old term)
(declare (xargs :guard (and (pseudo-termp new)
(pseudo-termp old)
(not (quotep old))
(pseudo-termp term))))
(cond ((variablep old) (subst-var new old term))
((fquotep old) (subst-expr-error old))
(t (subst-expr1 new old term))))
; Congruence-Based Substitution: