forked from acl2/acl2
-
Notifications
You must be signed in to change notification settings - Fork 0
/
prove.lisp
9542 lines (8378 loc) · 416 KB
/
prove.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: Kaufmann@cs.utexas.edu and Moore@cs.utexas.edu
; Department of Computer Science
; University of Texas at Austin
; Austin, TX 78712 U.S.A.
(in-package "ACL2")
; Section: PREPROCESS-CLAUSE
; The preprocessor is the first clause processor in the waterfall when
; we enter from prove. It contains a simple term rewriter that expands
; certain "abbreviations" and a gentle clausifier.
; We first develop the simple rewriter, called expand-abbreviations.
; Rockwell Addition: We are now concerned with lambdas, where we
; didn't used to treat them differently. This extra argument will
; show up in several places during a compare-windows.
(mutual-recursion
(defun abbreviationp1 (lambda-flg vars term2)
; This function returns t if term2 is not an abbreviation of term1
; (where vars is the bag of vars in term1). Otherwise, it returns the
; excess vars of vars. If lambda-flg is t we look out for lambdas and
; do not consider something an abbreviation if we see a lambda in it.
; If lambda-flg is nil, we treat lambdas as though they were function
; symbols.
(cond ((variablep term2)
(cond ((null vars) t) (t (cdr vars))))
((fquotep term2) vars)
((and lambda-flg
(flambda-applicationp term2))
t)
((member-eq (ffn-symb term2) '(if not implies)) t)
(t (abbreviationp1-lst lambda-flg vars (fargs term2)))))
(defun abbreviationp1-lst (lambda-flg vars lst)
(cond ((null lst) vars)
(t (let ((vars1 (abbreviationp1 lambda-flg vars (car lst))))
(cond ((eq vars1 t) t)
(t (abbreviationp1-lst lambda-flg vars1 (cdr lst))))))))
)
(defun abbreviationp (lambda-flg vars term2)
; Consider the :REWRITE rule generated from (equal term1 term2). We
; say such a rule is an "abbreviation" if term2 contains no more
; variable occurrences than term1 and term2 does not call the
; functions IF, NOT or IMPLIES or (if lambda-flg is t) any LAMBDA.
; Vars, above, is the bag of vars from term1. We return non-nil iff
; (equal term1 term2) is an abbreviation.
(not (eq (abbreviationp1 lambda-flg vars term2) t)))
(mutual-recursion
(defun all-vars-bag (term ans)
(cond ((variablep term) (cons term ans))
((fquotep term) ans)
(t (all-vars-bag-lst (fargs term) ans))))
(defun all-vars-bag-lst (lst ans)
(cond ((null lst) ans)
(t (all-vars-bag-lst (cdr lst)
(all-vars-bag (car lst) ans)))))
)
(defun find-abbreviation-lemma (term geneqv lemmas ens wrld)
; Term is a function application, geneqv is a generated equivalence
; relation and lemmas is the 'lemmas property of the function symbol
; of term. We find the first (enabled) abbreviation lemma that
; rewrites term maintaining geneqv. A lemma is an abbreviation if it
; is not a meta-lemma, has no hypotheses, has no loop-stopper, and has
; an abbreviationp for the conclusion.
; If we win we return t, the rune of the :CONGRUENCE rule used, the
; lemma, and the unify-subst. Otherwise we return four nils.
(cond ((null lemmas) (mv nil nil nil nil))
((and (enabled-numep (access rewrite-rule (car lemmas) :nume) ens)
(eq (access rewrite-rule (car lemmas) :subclass) 'abbreviation)
(geneqv-refinementp (access rewrite-rule (car lemmas) :equiv)
geneqv
wrld))
(mv-let
(wonp unify-subst)
(one-way-unify (access rewrite-rule (car lemmas) :lhs) term)
(cond (wonp (mv t
(geneqv-refinementp
(access rewrite-rule (car lemmas) :equiv)
geneqv
wrld)
(car lemmas)
unify-subst))
(t (find-abbreviation-lemma term geneqv (cdr lemmas)
ens wrld)))))
(t (find-abbreviation-lemma term geneqv (cdr lemmas)
ens wrld))))
(mutual-recursion
(defun expand-abbreviations-with-lemma (term geneqv pequiv-info
fns-to-be-ignored-by-rewrite
rdepth step-limit ens wrld state
ttree)
(mv-let
(wonp cr-rune lemma unify-subst)
(find-abbreviation-lemma term geneqv
(getpropc (ffn-symb term) 'lemmas nil wrld)
ens
wrld)
(cond
(wonp
(with-accumulated-persistence
(access rewrite-rule lemma :rune)
((the (signed-byte 30) step-limit) term ttree)
t
(expand-abbreviations
(access rewrite-rule lemma :rhs)
unify-subst
geneqv
pequiv-info
fns-to-be-ignored-by-rewrite
(adjust-rdepth rdepth) step-limit ens wrld state
(push-lemma cr-rune
(push-lemma (access rewrite-rule lemma :rune)
ttree)))))
(t (mv step-limit term ttree)))))
(defun expand-abbreviations (term alist geneqv pequiv-info
fns-to-be-ignored-by-rewrite
rdepth step-limit ens wrld state ttree)
; This function is essentially like rewrite but is more restrictive in its use
; of rules. We rewrite term/alist maintaining geneqv and pequiv-info, avoiding
; the expansion or application of lemmas to terms whose fns are in
; fns-to-be-ignored-by-rewrite. We return a new term and a ttree (accumulated
; onto our argument) describing the rewrite. We only apply "abbreviations"
; which means we expand lambda applications and non-rec fns provided they do
; not duplicate arguments or introduce IFs, etc. (see abbreviationp), and we
; apply those unconditional :REWRITE rules with the same property.
; It used to be written:
; Note: In a break with Nqthm and the first four versions of ACL2, in
; Version 1.5 we also expand IMPLIES terms here. In fact, we expand
; several members of *expandable-boot-strap-non-rec-fns* here, and
; IFF. The impetus for this decision was the forcing of impossible
; goals by simplify-clause. As of this writing, we have just added
; the idea of forcing rounds and the concomitant notion that forced
; hypotheses are proved under the type-alist extant at the time of the
; force. But if the simplifier sees IMPLIES terms and rewrites their
; arguments, it does not augment the context, e.g., in (IMPLIES hyps
; concl) concl is rewritten without assuming hyps and thus assumptions
; forced in concl are context free and often impossible to prove. Now
; while the user might hide propositional structure in other functions
; and thus still suffer this failure mode, IMPLIES is the most common
; one and by opening it now we make our context clearer. See the note
; below for the reason we expand other
; *expandable-boot-strap-non-rec-fns*.
; This is no longer true. We now expand the IMPLIES from the original theorem
; in preprocess-clause before expand-abbreviations is called, and do not expand
; any others here. These changes in the handling of IMPLIES (as well as
; several others) are caused by the introduction of assume-true-false-if. See
; the mini-essay at assume-true-false-if.
(cond
((zero-depthp rdepth)
(rdepth-error
(mv step-limit term ttree)
t))
((time-limit5-reached-p ; nil, or throws
"Out of time in preprocess (expand-abbreviations).")
(mv step-limit nil nil))
(t
(let ((step-limit (decrement-step-limit step-limit)))
(cond
((variablep term)
(let ((temp (assoc-eq term alist)))
(cond (temp (mv step-limit (cdr temp) ttree))
(t (mv step-limit term ttree)))))
((fquotep term) (mv step-limit term ttree))
((and (eq (ffn-symb term) 'return-last)
; We avoid special treatment for return-last when the first argument is progn,
; since the user may have intended the first argument to be rewritten in that
; case; for example, the user might want to see a message printed when the term
; (prog2$ (cw ...) ...) is encountered. But it is useful in the other cases,
; in particular for calls of return-last generated by calls of mbe, to avoid
; spending time simplifying the next-to-last argument.
(not (equal (fargn term 1) ''progn)))
(expand-abbreviations (fargn term 3)
alist geneqv pequiv-info
fns-to-be-ignored-by-rewrite rdepth
step-limit ens wrld state
(push-lemma
(fn-rune-nume 'return-last nil nil wrld)
ttree)))
((eq (ffn-symb term) 'hide)
(mv step-limit
(sublis-var alist term)
ttree))
(t
(mv-let
(deep-pequiv-lst shallow-pequiv-lst)
(pequivs-for-rewrite-args (ffn-symb term) geneqv pequiv-info wrld ens)
(sl-let
(expanded-args ttree)
(expand-abbreviations-lst (fargs term)
alist
1 nil deep-pequiv-lst shallow-pequiv-lst
geneqv (ffn-symb term)
(geneqv-lst (ffn-symb term) geneqv ens wrld)
fns-to-be-ignored-by-rewrite
(adjust-rdepth rdepth) step-limit
ens wrld state ttree)
(let* ((fn (ffn-symb term))
(term (cons-term fn expanded-args)))
; If term does not collapse to a constant, fn is still its ffn-symb.
(cond
((fquotep term)
; Term collapsed to a constant. But it wasn't a constant before, and so
; it collapsed because cons-term executed fn on constants. So we record
; a use of the executable-counterpart.
(mv step-limit
term
(push-lemma (fn-rune-nume fn nil t wrld) ttree)))
((member-equal fn fns-to-be-ignored-by-rewrite)
(mv step-limit (cons-term fn expanded-args) ttree))
((and (all-quoteps expanded-args)
(enabled-xfnp fn ens wrld)
(or (flambda-applicationp term)
(not (getpropc fn 'constrainedp nil wrld))))
(cond ((flambda-applicationp term)
(expand-abbreviations
(lambda-body fn)
(pairlis$ (lambda-formals fn) expanded-args)
geneqv pequiv-info
fns-to-be-ignored-by-rewrite
(adjust-rdepth rdepth) step-limit ens wrld state ttree))
((programp fn wrld)
; We formerly thought this case was possible during admission of recursive
; definitions. Best if it's not! So we cause an error; if we ever hit this
; case, we can think about whether allowing :program mode functions into the
; prover processes is problematic. Our concern about :program mode functions
; in proofs has led us in May 2016 to change the application of meta functions
; and clause-processors to insist that the result is free of :program mode
; function symbols.
(mv step-limit
; (cons-term fn expanded-args)
(er hard! 'expand-abbreviations
"Implementation error: encountered :program mode ~
function symbol, ~x0"
fn)
ttree))
(t
(mv-let
(erp val latches)
(pstk
(ev-fncall fn (strip-cadrs expanded-args) state nil t
nil))
(declare (ignore latches))
(cond
(erp
; We following a suggestion from Matt Wilding and attempt to simplify the term
; before applying HIDE.
(let ((new-term1 (cons-term fn expanded-args)))
(sl-let (new-term2 ttree)
(expand-abbreviations-with-lemma
new-term1 geneqv pequiv-info
fns-to-be-ignored-by-rewrite
rdepth step-limit ens wrld state ttree)
(cond
((equal new-term2 new-term1)
(mv step-limit
(mcons-term* 'hide new-term1)
(push-lemma (fn-rune-nume 'hide nil nil wrld)
ttree)))
(t (mv step-limit new-term2 ttree))))))
(t (mv step-limit
(kwote val)
(push-lemma (fn-rune-nume fn nil t wrld)
ttree))))))))
((flambdap fn)
(cond ((abbreviationp nil
(lambda-formals fn)
(lambda-body fn))
(expand-abbreviations
(lambda-body fn)
(pairlis$ (lambda-formals fn) expanded-args)
geneqv pequiv-info
fns-to-be-ignored-by-rewrite
(adjust-rdepth rdepth) step-limit ens wrld state ttree))
(t
; Once upon a time (well into v1-9) we just returned (mv term ttree)
; here. But then Jun Sawada pointed out some problems with his proofs
; of some theorems of the form (let (...) (implies (and ...) ...)).
; The problem was that the implies was not getting expanded (because
; the let turns into a lambda and the implication in the body is not
; an abbreviationp, as checked above). So we decided that, in such
; cases, we would actually expand the abbreviations in the body
; without expanding the lambda itself, as we do below. This in turn
; often allows the lambda to expand via the following mechanism.
; Preprocess-clause calls expand-abbreviations and it expands the
; implies into IFs in the body without opening the lambda. But then
; preprocess-clause calls clausify-input which does another
; expand-abbreviations and this time the expansion is allowed. We do
; not imagine that this change will adversely affect proofs, but if
; so, well, the old code is shown on the first line of this comment.
(sl-let (body ttree)
(expand-abbreviations
(lambda-body fn)
nil
geneqv
nil ; pequiv-info
fns-to-be-ignored-by-rewrite
(adjust-rdepth rdepth) step-limit ens wrld state
ttree)
; Rockwell Addition:
; Once upon another time (through v2-5) we returned the fcons-term
; shown in the t clause below. But Rockwell proofs indicate that it
; is better to eagerly expand this lambda if the new body would make
; it an abbreviation.
(cond
((abbreviationp nil
(lambda-formals fn)
body)
(expand-abbreviations
body
(pairlis$ (lambda-formals fn) expanded-args)
geneqv pequiv-info
fns-to-be-ignored-by-rewrite
(adjust-rdepth rdepth) step-limit ens wrld state
ttree))
(t
(mv step-limit
(mcons-term (list 'lambda (lambda-formals fn)
body)
expanded-args)
ttree)))))))
((member-eq fn '(iff synp mv-list cons-with-hint return-last
wormhole-eval force case-split
double-rewrite))
; The list above is an arbitrary subset of *expandable-boot-strap-non-rec-fns*.
; Once upon a time we used the entire list here, but Bishop Brock complained
; that he did not want EQL opened. So we have limited the list to just the
; propositional function IFF and the no-ops.
; Note: Once upon a time we did not expand any propositional functions
; here. Indeed, one might wonder why we do now? The only place
; expand-abbreviations was called was from within preprocess-clause.
; And there, its output was run through clausify-input and then
; remove-trivial-clauses. The latter called tautologyp on each clause
; and that, in turn, expanded all the functions above (but discarded
; the expansion except for purposes of determining tautologyhood).
; Thus, there is no real case to make against expanding these guys.
; For sanity, one might wish to keep the list above in sync with
; that in tautologyp, where we say about it: "The list is in fact
; *expandable-boot-strap-non-rec-fns* with NOT deleted and IFF added.
; The main idea here is to include non-rec functions that users
; typically put into the elegant statements of theorems." But now we
; have deleted IMPLIES from this list, to support the assume-true-false-if
; idea, but we still keep IMPLIES in the list for tautologyp because
; if we can decide it's a tautology by expanding, all the better.
(with-accumulated-persistence
(fn-rune-nume fn nil nil wrld)
((the (signed-byte 30) step-limit) term ttree)
t
(expand-abbreviations (bbody fn)
(pairlis$ (formals fn wrld) expanded-args)
geneqv pequiv-info
fns-to-be-ignored-by-rewrite
(adjust-rdepth rdepth)
step-limit ens wrld state
(push-lemma (fn-rune-nume fn nil nil wrld)
ttree))))
; Rockwell Addition: We are expanding abbreviations. This is new treatment
; of IF, which didn't used to receive any special notice.
((eq fn 'if)
; There are no abbreviation (or rewrite) rules hung on IF, so coming out
; here is ok.
(let ((a (car expanded-args))
(b (cadr expanded-args))
(c (caddr expanded-args)))
(cond
((equal b c) (mv step-limit b ttree))
((quotep a)
(mv step-limit
(if (eq (cadr a) nil) c b)
ttree))
((and (equal geneqv *geneqv-iff*)
(equal b *t*)
(or (equal c *nil*)
(ffn-symb-p c 'HARD-ERROR)))
; Some users keep HARD-ERROR disabled so that they can figure out
; which guard proof case they are in. HARD-ERROR is identically nil
; and we would really like to eliminate the IF here. So we use our
; knowledge that HARD-ERROR is nil even if it is disabled. We don't
; even put it in the ttree, because for all the user knows this is
; primitive type inference.
(mv step-limit a ttree))
(t (mv step-limit
(mcons-term 'if expanded-args)
ttree)))))
; Rockwell Addition: New treatment of equal.
((and (eq fn 'equal)
(equal (car expanded-args) (cadr expanded-args)))
(mv step-limit *t* ttree))
(t
(expand-abbreviations-with-lemma
term geneqv pequiv-info
fns-to-be-ignored-by-rewrite rdepth step-limit ens
wrld state ttree))))))))))))
(defun expand-abbreviations-lst (lst alist bkptr rewritten-args-rev
deep-pequiv-lst shallow-pequiv-lst
parent-geneqv parent-fn geneqv-lst
fns-to-be-ignored-by-rewrite rdepth
step-limit ens wrld state ttree)
(cond
((null lst) (mv step-limit (reverse rewritten-args-rev) ttree))
(t (mv-let
(child-geneqv child-pequiv-info)
(geneqv-and-pequiv-info-for-rewrite
parent-fn bkptr rewritten-args-rev lst alist
parent-geneqv
(car geneqv-lst)
deep-pequiv-lst
shallow-pequiv-lst
wrld)
(sl-let (term1 new-ttree)
(expand-abbreviations (car lst) alist
child-geneqv child-pequiv-info
fns-to-be-ignored-by-rewrite
rdepth step-limit ens wrld state ttree)
(expand-abbreviations-lst (cdr lst) alist
(1+ bkptr)
(cons term1 rewritten-args-rev)
deep-pequiv-lst shallow-pequiv-lst
parent-geneqv parent-fn
(cdr geneqv-lst)
fns-to-be-ignored-by-rewrite
rdepth step-limit ens wrld
state new-ttree))))))
)
(defun and-orp (term bool lambda-okp)
; We return t or nil according to whether term is a disjunction (if bool is t)
; or conjunction (if bool is nil).
; After v8-0 we made a change to preserve lambdas on right-hand sides of
; rewrite rules. At that time we added the clause for lambdas below, to
; preserve the old behavior of find-and-or-lemma. However, in general it seems
; a good idea to open up lambdas slowly, so we keep the old behavior of and-orp
; -- not diving into lambda bodies -- in other places, which also helps with
; backward compatibility (one example is the proof of lemma
; aignet-marked-copies-in-bounds-of-empty-bitarr in community book
; books/centaur/aignet/rewrite.lisp). Parameter lambda-okp is true when we
; allow exploration of lambda bodies, else nil. When we tried on 8/14/2018
; calling and-orp with lambda-okp = t in the case (flambda-applicationp term)
; of expand-and-or -- that is, to dive into lambda-bodies of lambda-bodies --
; we got 19 failures when trying an "everything" regression, which (of course)
; almost surely undercounts failures, since certification wasn't attempted for
; books depending on failed books.
(case-match term
(('if & c2 c3)
(if bool
(or (equal c2 *t*) (equal c3 *t*))
(or (equal c2 *nil*) (equal c3 *nil*))))
((('lambda & body) . &)
(and lambda-okp
(and-orp body bool lambda-okp)))))
(defun find-and-or-lemma (term bool lemmas ens wrld)
; Term is a function application and lemmas is the 'lemmas property of
; the function symbol of term. We find the first enabled and-or
; (wrt bool) lemma that rewrites term maintaining iff.
; If we win we return t, the :CONGRUENCE rule name, the lemma, and the
; unify-subst. Otherwise we return four nils.
(cond ((null lemmas) (mv nil nil nil nil))
((and (enabled-numep (access rewrite-rule (car lemmas) :nume) ens)
(or (eq (access rewrite-rule (car lemmas) :subclass) 'backchain)
(eq (access rewrite-rule (car lemmas) :subclass) 'abbreviation))
(null (access rewrite-rule (car lemmas) :hyps))
(null (access rewrite-rule (car lemmas) :heuristic-info))
(geneqv-refinementp (access rewrite-rule (car lemmas) :equiv)
*geneqv-iff*
wrld)
(and-orp (access rewrite-rule (car lemmas) :rhs) bool t))
(mv-let
(wonp unify-subst)
(one-way-unify (access rewrite-rule (car lemmas) :lhs) term)
(cond (wonp (mv t
(geneqv-refinementp
(access rewrite-rule (car lemmas) :equiv)
*geneqv-iff*
wrld)
(car lemmas)
unify-subst))
(t (find-and-or-lemma term bool (cdr lemmas) ens wrld)))))
(t (find-and-or-lemma term bool (cdr lemmas) ens wrld))))
(defun expand-and-or (term bool fns-to-be-ignored-by-rewrite ens wrld state
ttree step-limit)
; We expand the top-level fn symbol of term provided the expansion produces a
; conjunction -- when bool is nil -- or a disjunction -- when bool is t. We
; return four values: the new step-limit, wonp, the new term, and a new ttree.
; This fn is a No-Change Loser.
; Note that preprocess-clause calls expand-abbreviations; but also
; preprocess-clause calls clausify-input, which calls expand-and-or, which
; calls expand-abbreviations. But this is not redundant, as expand-and-or
; calls expand-abbreviations after expanding function definitions and using
; rewrite rules when the result is a conjunction or disjunction (depending on
; bool) -- even when the rule being applied is not an abbreviation rule. Below
; are event sequences that illustrate this extra work being done. In both
; cases, evaluation of (getpropc 'foo 'lemmas) shows that we are expanding with
; a rewrite-rule structure that is not of subclass 'abbreviation.
; (defstub bar (x) t)
; (defun foo (x) (and (bar (car x)) (bar (cdr x))))
; (trace$ expand-and-or expand-abbreviations clausify-input preprocess-clause)
; (thm (foo x) :hints (("Goal" :do-not-induct :otf)))
; (defstub bar (x) t)
; (defstub foo (x) t)
; (defaxiom foo-open (equal (foo x) (and (bar (car x)) (bar (cdr x)))))
; (trace$ expand-and-or expand-abbreviations clausify-input preprocess-clause)
; (thm (foo x) :hints (("Goal" :do-not-induct :otf)))
(cond ((variablep term) (mv step-limit nil term ttree))
((fquotep term) (mv step-limit nil term ttree))
((member-equal (ffn-symb term) fns-to-be-ignored-by-rewrite)
(mv step-limit nil term ttree))
((flambda-applicationp term)
(cond ((and-orp (lambda-body (ffn-symb term)) bool nil)
(sl-let
(term ttree)
(expand-abbreviations
(subcor-var (lambda-formals (ffn-symb term))
(fargs term)
(lambda-body (ffn-symb term)))
nil
*geneqv-iff*
nil
fns-to-be-ignored-by-rewrite
(rewrite-stack-limit wrld) step-limit ens wrld state ttree)
(mv step-limit t term ttree)))
(t (mv step-limit nil term ttree))))
(t
(let ((def-body (def-body (ffn-symb term) wrld)))
(cond
((and def-body
(null (access def-body def-body :recursivep))
(null (access def-body def-body :hyp))
(member-eq (access def-body def-body :equiv)
'(equal iff))
(enabled-numep (access def-body def-body :nume)
ens)
(and-orp (access def-body def-body :concl) bool nil))
(sl-let
(term ttree)
(with-accumulated-persistence
(access def-body def-body :rune)
((the (signed-byte 30) step-limit) term ttree)
t
(expand-abbreviations
(subcor-var (access def-body def-body
:formals)
(fargs term)
(access def-body def-body :concl))
nil
*geneqv-iff*
nil
fns-to-be-ignored-by-rewrite
(rewrite-stack-limit wrld)
step-limit ens wrld state
(push-lemma? (access def-body def-body :rune)
ttree)))
(mv step-limit t term ttree)))
(t (mv-let
(wonp cr-rune lemma unify-subst)
(find-and-or-lemma
term bool
(getpropc (ffn-symb term) 'lemmas nil wrld)
ens wrld)
(cond
(wonp
(sl-let
(term ttree)
(with-accumulated-persistence
(access rewrite-rule lemma :rune)
((the (signed-byte 30) step-limit) term ttree)
t
(expand-abbreviations
(sublis-var unify-subst
(access rewrite-rule lemma :rhs))
nil
*geneqv-iff*
nil
fns-to-be-ignored-by-rewrite
(rewrite-stack-limit wrld)
step-limit ens wrld state
(push-lemma cr-rune
(push-lemma (access rewrite-rule lemma
:rune)
ttree))))
(mv step-limit t term ttree)))
(t (mv step-limit nil term ttree))))))))))
(defun clausify-input1 (term bool fns-to-be-ignored-by-rewrite ens wrld state
ttree step-limit)
; We return three things: a new step-limit, a clause, and a ttree. If bool is
; t, the (disjunction of the literals in the) clause is equivalent to term. If
; bool is nil, the clause is equivalent to the negation of term. This function
; opens up some nonrec fns and applies some rewrite rules. The final ttree
; contains the symbols and rules used.
(cond
((equal term (if bool *nil* *t*)) (mv step-limit nil ttree))
((ffn-symb-p term 'if)
(let ((t1 (fargn term 1))
(t2 (fargn term 2))
(t3 (fargn term 3)))
(cond
(bool
(cond
((equal t3 *t*)
(sl-let (cl1 ttree)
(clausify-input1 t1 nil
fns-to-be-ignored-by-rewrite
ens wrld state ttree step-limit)
(sl-let (cl2 ttree)
(clausify-input1 t2 t
fns-to-be-ignored-by-rewrite
ens wrld state ttree step-limit)
(mv step-limit (disjoin-clauses cl1 cl2) ttree))))
((equal t2 *t*)
(sl-let (cl1 ttree)
(clausify-input1 t1 t
fns-to-be-ignored-by-rewrite
ens wrld state ttree step-limit)
(sl-let (cl2 ttree)
(clausify-input1 t3 t
fns-to-be-ignored-by-rewrite
ens wrld state ttree step-limit)
(mv step-limit (disjoin-clauses cl1 cl2) ttree))))
(t (mv step-limit (list term) ttree))))
((equal t3 *nil*)
(sl-let (cl1 ttree)
(clausify-input1 t1 nil
fns-to-be-ignored-by-rewrite
ens wrld state ttree step-limit)
(sl-let (cl2 ttree)
(clausify-input1 t2 nil
fns-to-be-ignored-by-rewrite
ens wrld state ttree step-limit)
(mv step-limit (disjoin-clauses cl1 cl2) ttree))))
((equal t2 *nil*)
(sl-let (cl1 ttree)
(clausify-input1 t1 t
fns-to-be-ignored-by-rewrite
ens wrld state ttree step-limit)
(sl-let (cl2 ttree)
(clausify-input1 t3 nil
fns-to-be-ignored-by-rewrite
ens wrld state ttree step-limit)
(mv step-limit (disjoin-clauses cl1 cl2) ttree))))
(t (mv step-limit (list (dumb-negate-lit term)) ttree)))))
(t (sl-let (wonp term ttree)
(expand-and-or term bool fns-to-be-ignored-by-rewrite
ens wrld state ttree step-limit)
(cond (wonp
(clausify-input1 term bool fns-to-be-ignored-by-rewrite
ens wrld state ttree step-limit))
(bool (mv step-limit (list term) ttree))
(t (mv step-limit
(list (dumb-negate-lit term))
ttree)))))))
(defun clausify-input1-lst (lst fns-to-be-ignored-by-rewrite ens wrld state
ttree step-limit)
; This function is really a subroutine of clausify-input. It just
; applies clausify-input1 to every element of lst, accumulating the ttrees.
; It uses bool=t.
(cond ((null lst) (mv step-limit nil ttree))
(t (sl-let (clause ttree)
(clausify-input1 (car lst) t fns-to-be-ignored-by-rewrite
ens wrld state ttree step-limit)
(sl-let (clauses ttree)
(clausify-input1-lst (cdr lst)
fns-to-be-ignored-by-rewrite
ens wrld state ttree
step-limit)
(mv step-limit
(conjoin-clause-to-clause-set clause clauses)
ttree))))))
(defun clausify-input (term fns-to-be-ignored-by-rewrite ens wrld state ttree
step-limit)
; This function converts term to a set of clauses, expanding some non-rec
; functions when they produce results of the desired parity (i.e., we expand
; AND-like functions in the hypotheses and OR-like functions in the
; conclusion.) AND and OR themselves are, of course, already expanded into
; IFs, but we will expand other functions when they generate the desired IF
; structure. We also apply :REWRITE rules deemed appropriate. We return three
; results: a new step-limit, the set of clauses, and a ttree documenting the
; expansions.
(sl-let (neg-clause ttree)
(clausify-input1 term nil fns-to-be-ignored-by-rewrite ens
wrld state ttree step-limit)
; Neg-clause is a clause that is equivalent to the negation of term. That is,
; if the literals of neg-clause are lit1, ..., litn, then (or lit1 ... litn)
; <-> (not term). Therefore, term is the negation of the clause, i.e., (and
; (not lit1) ... (not litn)). We will form a clause from each (not lit1) and
; return the set of clauses, implicitly conjoined.
(clausify-input1-lst (dumb-negate-lit-lst neg-clause)
fns-to-be-ignored-by-rewrite
ens wrld state ttree step-limit)))
(defun expand-some-non-rec-fns-in-clauses (fns clauses wrld)
; Warning: fns should be a subset of functions that
; This function expands the non-rec fns listed in fns in each of the clauses
; in clauses. It then throws out of the set any trivial clause, i.e.,
; tautologies. It does not normalize the expanded terms but just leaves
; the expanded bodies in situ. See the comment in preprocess-clause.
(cond
((null clauses) nil)
(t (let ((cl (expand-some-non-rec-fns-lst fns (car clauses) wrld)))
(cond
((trivial-clause-p cl wrld)
(expand-some-non-rec-fns-in-clauses fns (cdr clauses) wrld))
(t (cons cl
(expand-some-non-rec-fns-in-clauses fns (cdr clauses)
wrld))))))))
(defun no-op-histp (hist)
; We say a history, hist, is a "no-op history" if it is empty or its most
; recent entry is a to-be-hidden preprocess-clause or apply-top-hints-clause
; (possibly followed by a settled-down-clause).
(or (null hist)
(and hist
(member-eq (access history-entry (car hist) :processor)
'(apply-top-hints-clause preprocess-clause))
(tag-tree-occur 'hidden-clause
t
(access history-entry (car hist) :ttree)))
(and hist
(eq (access history-entry (car hist) :processor)
'settled-down-clause)
(cdr hist)
(member-eq (access history-entry (cadr hist) :processor)
'(apply-top-hints-clause preprocess-clause))
(tag-tree-occur 'hidden-clause
t
(access history-entry (cadr hist) :ttree)))))
(mutual-recursion
; This pair of functions is copied from expand-abbreviations and
; heavily modified. The idea implemented by the caller of this
; function is to expand all the IMPLIES terms in the final literal of
; the goal clause. This pair of functions actually implements that
; expansion. One might think to use expand-some-non-rec-fns with
; first argument '(IMPLIES). But this function is different in two
; respects. First, it respects HIDE. Second, it expands the IMPLIES
; inside of lambda bodies. The basic idea is to mimic what
; expand-abbreviations used to do, before we added the
; assume-true-false-if idea.
(defun expand-any-final-implies1 (term wrld)
(cond
((variablep term)
term)
((fquotep term)
term)
((eq (ffn-symb term) 'hide)
term)
(t
(let ((expanded-args (expand-any-final-implies1-lst (fargs term)
wrld)))
(let* ((fn (ffn-symb term))
(term (cons-term fn expanded-args)))
(cond ((flambdap fn)
(let ((body (expand-any-final-implies1 (lambda-body fn)
wrld)))
; Note: We could use a make-lambda-application here, but if the
; original lambda used all of its variables then so does the new one,
; because IMPLIES uses all of its variables and we're not doing any
; simplification. This remark is not soundness related; there is no
; danger of introducing new variables, only the inefficiency of
; keeping a big actual which is actually not used.
(fcons-term (make-lambda (lambda-formals fn) body)
expanded-args)))
((eq fn 'IMPLIES)
(subcor-var (formals 'implies wrld)
expanded-args
(bbody 'implies)))
(t term)))))))
(defun expand-any-final-implies1-lst (term-lst wrld)
(cond ((null term-lst)
nil)
(t
(cons (expand-any-final-implies1 (car term-lst) wrld)
(expand-any-final-implies1-lst (cdr term-lst) wrld)))))
)
(defun expand-any-final-implies (cl wrld)
; Cl is a clause (a list of ACL2 terms representing a goal) about to
; enter preprocessing. If the final term contains an 'IMPLIES, we
; expand those IMPLIES here. This change in the handling of IMPLIES
; (as well as several others) is caused by the introduction of
; assume-true-false-if. See the mini-essay at assume-true-false-if.
; Note that we fail to report the fact that we used the definition
; of IMPLIES.
; Note also that we do not use expand-some-non-rec-fns here. We want
; to preserve the meaning of 'HIDE and expand an 'IMPLIES inside of
; a lambda.
(cond ((null cl) ; This should not happen.
nil)
((null (cdr cl))
(list (expand-any-final-implies1 (car cl) wrld)))
(t
(cons (car cl)
(expand-any-final-implies (cdr cl) wrld)))))
(defun rw-cache-state (wrld)
(let ((pair (assoc-eq t (table-alist 'rw-cache-state-table wrld))))
(cond (pair (cdr pair))
(t *default-rw-cache-state*))))
(defmacro make-rcnst (ens wrld state &rest args)
; (Make-rcnst ens w state) will make a rewrite-constant that is the result of
; filling in *empty-rewrite-constant* with a few obviously necessary values,
; such as the global-enabled-structure as the :current-enabled-structure. Then
; it additionally loads user supplied values specified by alternating
; keyword/value pairs to override what is otherwise created. E.g.,
; (make-rcnst ens w state :expand-lst lst)
; will make a rewrite-constant that is like the default one except that it will
; have lst as the :expand-lst.
; Note: Wrld and ens are used in the "default" setting of certain fields.
; Warning: wrld could be evaluated several times. So it should be an
; inexpensive expression, such as a variable or (w state).
`(change rewrite-constant
(change rewrite-constant
*empty-rewrite-constant*
:current-enabled-structure ,ens
:oncep-override (match-free-override ,wrld)
:case-split-limitations (case-split-limitations ,wrld)
:forbidden-fns (forbidden-fns ,wrld ,state)
:nonlinearp (non-linearp ,wrld)
:backchain-limit-rw (backchain-limit ,wrld :rewrite)
:rw-cache-state (rw-cache-state ,wrld))
,@args))
; We now finish the development of tau-clause... To recap our story so far: In
; the file tau.lisp we defined everything we need to implement tau-clause
; except for its connection to type-alist and the linear pot-lst. Now we can
; define tau-clause.
(defun cheap-type-alist-and-pot-lst (cl ens wrld state)
; Given a clause cl, we build a type-alist and linear pot-lst with all of the
; literals in cl assumed false. The pot-lst is built with the cheap-linearp
; flag on, which means we do not rewrite terms before turning them into polys
; and we add no linear lemmas. We insure that the type-alist has no
; assumptions or forced hypotheses. FYI: Just to be doubly sure that we are
; not ignoring assumptions and forced hypotheses, you will note that in
; relieve-dependent-hyps, after calling type-set, we check that no such entries
; are in the returned ttree. We return (mv contradictionp type-alist pot-lst)
(mv-let (contradictionp type-alist ttree)
(type-alist-clause cl nil nil nil ens wrld nil nil)
(cond
((or (tagged-objectsp 'assumption ttree)
(tagged-objectsp 'fc-derivation ttree))
(mv (er hard 'cheap-type-alist-and-pot-lst
"Assumptions and/or fc-derivations were found in the ~
ttree constructed by CHEAP-TYPE-ALIST-AND-POT-LST. This ~
is supposedly impossible!")
nil nil))
(contradictionp
(mv t nil nil))
(t (mv-let (new-step-limit provedp pot-lst)
(setup-simplify-clause-pot-lst1
cl nil type-alist
(make-rcnst ens wrld state
:force-info 'weak
:cheap-linearp t)
wrld state *default-step-limit*)
(declare (ignore new-step-limit))
(cond
(provedp
(mv t nil nil))
(t (mv nil type-alist pot-lst))))))))
(defconst *tau-ttree*
(add-to-tag-tree 'lemma
'(:executable-counterpart tau-system)
nil))
(defun tau-clausep (clause ens wrld state calist)
; This function returns (mv flg ttree), where if flg is t then clause is true.
; The ttree, when non-nil, is just the *tau-ttree*.
; If the executable-counterpart of tau is disabled, this function is a no-op.
(cond
((enabled-numep *tau-system-xnume* ens)
(mv-let
(contradictionp type-alist pot-lst)
(cheap-type-alist-and-pot-lst clause ens wrld state)
(cond
(contradictionp
(mv t *tau-ttree* calist))
(t
(let ((triples (merge-sort-car-<
(annotate-clause-with-key-numbers clause
(len clause)
0 wrld))))
(mv-let