-
Notifications
You must be signed in to change notification settings - Fork 0
/
rewrite.lisp
19269 lines (16849 loc) · 856 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.3 -- A Computational Logic for Applicative Common Lisp
; Copyright (C) 2020, 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 introduce ev-fncall+ early in this file to support its use in the
; definition of scons-term.
; Essay on Evaluation of Apply$ and Loop$ Calls During Proofs
; (Note: This essay also applies similarly to badge, even though we do not
; discuss badge in it.)
; A goal from the earliest days of ACL2 has been efficient evaluation, not only
; for forms submitted at the top-level loop, but also during proofs. The
; earliest implementations of apply$, badge, and loop$ limited their evaluation
; during proofs, essentially disallowing apply$ or badge for user-defined
; functions. This is not particularly unreasonable since attachments are
; disallowed during proofs, which is completely appropriate.
; This situation has been remedied starting in March, 2019, by expanding the
; use in the rewriter of doppelganger-apply$-userfn and
; doppelganger-badge-userfn, for calls of apply$-userfn and badge-userfn on
; concrete arguments, where the first argument has a warrant. If the warrant
; is not known to be true in the current context, then it is forced (unless it
; is known to be false). See community book
; books/system/tests/apply-in-proofs.lisp for examples.
; The key idea is that the truth of the warrant for fn justifies replacement of
; (apply$ 'fn '(arg1 ... argk)) by (fn arg1 ... argk); let's call this a
; "warranted replacement". A version of ev-fncall, ev-fncall+, records the
; warrants that are required to be true in order to make those warranted
; replacements during evaluation. Ev-fncall+ is actually a small wrapper for
; ev-fncall+-w, which in turn has a raw Lisp implementation that relies on a
; Lisp global, *warrant-reqs*. The definition of *warrant-reqs* has a comment
; explaining its legal values, and a search of the sources for *warrant-reqs*
; should make reasonably clear how this variable is used; but here is a
; summary. When *warrant-reqs* has its global value of nil, no special
; behavior occurs: ev-fncall+[-w] essentially reduces to ev-fncall[-w].
; Otherwise, *warrant-reqs* can be initialized to t to represent the empty
; list, and this "list" is extended by maybe-extend-warrant-reqs each time a
; new function requires a true warrant because of a warranted replacement (as
; described above). Upon completion of a ground evaluation using ev-fncall+,
; this list of functions is returned as the third value of ev-fncall+. The
; function push-warrants then processes this list of functions as follows: for
; the warrant of each function in that list, either the warrant is known to be
; true or it is forced (except that if it the warrant is known to be false, the
; evaluation is considered to have failed).
; Note that *aokp* must be true for the apply$-lambda and loop$ shortcuts. So
; for the rewriter as described above, where *aokp* is nil but *warrant-reqs*
; is non-nil, evaluation involving apply$ or loop$ always reduces to evaluation
; of apply$-userfn, which is handled with warranted replacements as described
; above. At one time we considered allowing these shortcuts for lambdas and
; loop$ forms, and we could reconsider if we want more efficiency. But the
; current implementation seems to provide sufficient efficiency (until someone
; complains, at least), and has the following advantage: the function symbols
; stored in *warrant-reqs* are exactly those for which warranted replacement is
; used; but if we allow shortcuts for lambdas and loop$ forms, then we will
; need to include all user-defined functions occurring in the lambda body or
; loop$ body even when lying on an IF branch that was not taken during a given
; evaluation.
; We considered handling evaluation in expand-abbreviations as described above
; for the rewriter. However, there is no type-alist readily available in
; expand-abbreviations for determining which warrants are known to be true.
; Moreover, the rules justifying warranted replacements (with names like
; apply$-fn) are conditional rewrite rules, which we traditionally ignore
; during preprocess-clause (and hence during expand-abbreviations) in favor of
; considering only "simple" rules. However, we do use ev-fncall+ in
; expand-abbreviations, so that we can avoid wrapping HIDE around the ground
; function application when the evaluation aborted rather than doing a
; warranted replacement. This case is represented by the case that the third
; value of ev-fncall+[-w] is a function symbol. Special handling is important
; for this case, to avoid wrapping the call in HIDE, since that would prevent
; the rewriter from later performing a successful evaluation using warranted
; replacements. Note that we initialize *warrant-reqs* to :nil! in this case
; instead of t, which causes evaluation to abort immediately the first time
; that a warranted replacement is called for. For very long loops this
; obviously can be important for efficiency!
; We considered also using ev-fncall+ for eval-ground-subexpressions, but that
; seemed to introduce more complexity than it's worth; this could change based
; on user demand. Since eval-ground-subexpressions does not introduce HIDE, we
; don't have the need for ev-fncall+ that is described above for
; expand-abbreviations.
; Note that our scheme works nicely with the executable-counterpart of apply$
; disabled. Specifically, all warranted replacements are justified by warrants
; -- actually by rules with names like apply$-fn -- rather than by the
; execution of apply$ calls.
; Next we develop the logical and raw Lisp definitions of ev-fncall+.
(defun badged-fns-of-world (wrld)
; We return the list of all warranted functions in wrld, but in a way that can
; be guard-verified and can be proved to return a list of function symbols.
; Historical Note: The name ``badged-fns-of-world'' is somewhat of a misnomer.
; There are badged functions, like CAR, not in this list. To be precise, this
; function returns the names of all the functions in the
; :badge-userfn-structure of the badge-table. Those symbols are put there by
; defwarrant and every symbol in the returned list has a warrant. Every
; function having a warrant is in the alist, and the alist associates the
; function name with its badge, which sort of explains why ``badge'' is part of
; the name of :badge-userfn-structure. But it ought, perhaps be named
; :badges-of-all-warranted-functions since there are functions not in the list
; that have badges, i.e., the 800+ apply$ primitives! Strictly speaking, even
; the use of the term ``userfn'' in the name is a misnomer! The list contains
; many symbols that are not, strictly speaking, user-defined but are in fact
; built-in, like the loop$ scions, COLLECT$ and COLLECT$+ and other loop$
; supporters like FROM-TO-BY. All uses of ``userfn'' in discussions related to
; apply$ ought to be changed to ``warranted-fns'' or something! The messiness
; of our nomenclature is in part due to the facts that initially apply$ was
; truly introduced after the fact in a book rather than as a system primitive,
; and that even after it was a system primitive there were badged functions
; that were not primitives but weren't warranted, i.e., multi-valued functions
; to which defwarrant could assign a badge (so they could be used in tame
; functions) but which were not given warrants (because at the time apply$ was
; not axiomatized to handle multiple values). It was only after the
; accommodation of multi-valued functions that we achieved the goal that the
; functions known to apply$ could be partitioned into three classes: the 800+
; apply$ primitives, the apply$ boot functions (like badge and apply$), and
; warranted functions. The first two sets all have badges but not warrants,
; all in the last set have badges and warrants.
(declare (xargs :mode :logic :guard (plist-worldp wrld)))
(and (alistp (table-alist 'badge-table wrld))
(let ((badge-alist
(cdr (assoc-eq :badge-userfn-structure
(table-alist 'badge-table wrld)))))
(and (alistp badge-alist)
(let ((syms (strip-cars badge-alist)))
(and (all-function-symbolps syms wrld)
syms))))))
(partial-encapsulate
; See the Essay on Evaluation of Apply$ and Loop$ Calls During Proofs.
; We think of (ev-fncall+-fns fn args wrld big-n safe-mode gc-off nil) as the
; list of badged functions supplied to apply$-userfn or badge-userfn during
; evaluation of the call of fn on args in wrld using the given
; user-stobj-alist, big-n, safe-mode, and gc-off. But if the last argument,
; strictp, is non-nil, then we think of the result as the first function symbol
; encountered during evaluation, if any, for which a true warrant was required
; to complete that call of fn.
; The constraint below can almost surely be explicitly strengthened, but we see
; no need at this point.
; Also see ev-fncall+-w.
(((ev-fncall+-fns * * * * * * *) => *))
nil
(logic)
(local (defun ev-fncall+-fns (fn args wrld big-n safe-mode gc-off strictp)
(declare (ignore fn args big-n safe-mode gc-off))
(and (not strictp)
(badged-fns-of-world wrld))))
(defthm all-function-symbolps-ev-fncall+-fns
(let ((fns (ev-fncall+-fns fn args wrld big-n safe-mode gc-off nil)))
(all-function-symbolps fns wrld)))
(defthm ev-fncall+-fns-is-subset-of-badged-fns-of-world
(subsetp (ev-fncall+-fns fn args wrld big-n safe-mode gc-off nil)
(badged-fns-of-world wrld)))
(defthm function-symbolp-ev-fncall+-fns-strictp
(let ((fn (ev-fncall+-fns fn args wrld big-n safe-mode gc-off t)))
(and (symbolp fn)
(or (null fn)
(function-symbolp fn wrld))))))
#+acl2-loop-only
(defun ev-fncall+-w (fn args w safe-mode gc-off strictp)
; See the Essay on Evaluation of Apply$ and Loop$ Calls During Proofs.
; This function allows apply$-userfn and badge-userfn to execute on warranted
; functions even when *aokp* is nil. It returns an error triple whose
; non-erroneous value is a list of the functions that need warrants in order to
; trust the result. However, in the case of an error when strictp is true, the
; value is a function symbol responsible for the error when a warrant is
; required so that evaluation is aborted, else nil. Its implementation is in
; the #-acl2-loop-only definition of this function; the present logical
; definition is incomplete in the sense that ev-fncall+-fns is partially
; constrained.
; This logical definition actually permits a list, computed by constrained
; function ev-fncall+-fns, that properly includes the intended list as a
; subset. But the under-the-hood implementation of ev-fncall+-w produces
; exactly the set of functions given to apply$-userfn or badge-userfn.
(let* ((big-n (big-n))
(fns (ev-fncall+-fns fn args w big-n safe-mode gc-off strictp)))
(mv-let (erp val latches)
(ev-fncall-rec-logical fn args
nil ; irrelevant arg-exprs (as latches is nil)
w
nil ; user-stobj-alist
big-n safe-mode gc-off
nil ; latches
t ; hard-error-returns-nilp
nil ; aokp
(and (not strictp) fns))
(declare (ignore latches))
(mv erp val fns))))
#-acl2-loop-only
(defvar *warrant-reqs*
; See the Essay on Evaluation of Apply$ and Loop$ Calls During Proofs.
; Legal values of this variable are as follows.
; nil - Always the global value, and always the value when *aokp* is non-nil
; t - Represents the empty list, enabling accumulation of function symbols
; whose (true) warrants support evaluation
; lst - A non-empty, duplicate-free list, which represents a set of warranted
; function symbols whose (true) warrants support evaluation
; :nil! - Like nil, but causes evaluation to stop if a warrant is ever required
; fn - A function symbol for which evaluation is aborted because its warrant
; is required (because *warrant-reqs* is :nil!)
nil)
; The third result of ev-fncall+ is LOGICALLY constrained (in the
; partial-encapsulate in rewrite.lisp before the logic definition of
; ev-fncall+-w) to always be a subset of the functions named in the
; :badge-userfn-structure of the badge-table. Thus, every function named in
; that third result has a warrant because :badge-userfn-structure is updated
; only by successful defwarrants. But the COMPUTED value of the third result
; is accumulated in raw Lisp as the value of the special *warrant-reqs*. This
; comment explains how we know *warrant-reqs* satisfies the constraint.
; The function maybe-extend-warrant-reqs is the only way we add a new element
; to *warrant-reqs*. That function is called in doppelganger-badge-userfn and
; doppelganger-apply$-userfn. In both contexts, maybe-extend-warrant-reqs is
; used to extend *warrant-reqs* with a function, fn, that has passed
; query-badge-userfn-structure, which does just what its name suggests: it
; inspects the :badge-userfn-structure.
#-acl2-loop-only
(defun ev-fncall+-w (fn args w safe-mode gc-off strictp)
; See comments in the logic definition of this function.
(let ((*warrant-reqs*
; See comments in the definition of *warrant-reqs* for a discussion of the
; :nil! and t values of this global.
(if strictp :nil! t)))
(declare (special *warrant-reqs*)) ; just to be safe
(mv-let (erp val latches)
(ev-fncall-w fn args w
nil ; user-stobj-alist
safe-mode gc-off
t ; hard-error-returns-nilp
nil) ; aok
(declare (ignore latches))
(mv erp
val
(if (member-eq *warrant-reqs* '(t nil :nil!))
nil
*warrant-reqs*)))))
(defun ev-fncall+ (fn args strictp state)
; See the Essay on Evaluation of Apply$ and Loop$ Calls During Proofs.
; Also see comments in the logic definition of ev-fncall+-w.
(ev-fncall+-w fn args
(w state)
(f-get-global 'safe-mode state)
(gc-off state)
strictp))
; 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)))