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
|
; Copyright (C) 2022, ForrestHunt, Inc.
; Written by Matt Kaufmann and J Moore
; License: A 3-clause BSD license. See the LICENSE file distributed with ACL2.
; This file contains a series of theorems about loop$ that are easy to prove by the
; correct induction argument. The file is designed to test the :induction rules in
; loop-lemmas.lisp.
(in-package "ACL2")
(include-book "top")
(defthm loop$-induction-challenge-1
(implies (natp i0)
(nat-listp (loop$ for i from i0 to max collect i)))
:rule-classes nil)
(defthm loop$-induction-challenge-2
(implies (and (natp i0)
(natp bump))
(nat-listp (loop$ for i from i0 to max collect (+ i bump))))
:rule-classes nil)
(defthm loop$-induction-challenge-3
(implies (and (natp i0)
(natp j0))
(nat-listp (loop$ for i from i0 to max
as j from j0 to max
collect (+ i j))))
:rule-classes nil)
(defthm loop$-induction-challenge-4a
(implies (and (nat-listp lst1)
(nat-listp lst2))
(nat-listp (loop$ for i in lst1
as j in lst2
collect (+ i j))))
:rule-classes nil)
(defthm loop$-induction-challenge-4b
(implies (and (nat-listp lst1)
(nat-listp lst2))
(nat-listp (loop$ for i in lst1
as l on lst2
collect (+ i (car l)))))
:rule-classes nil)
(defthm loop$-induction-challenge-4c
(implies (nat-listp lst)
(loop$ for i in lst
as j in lst
always (equal i j)))
:rule-classes nil)
(defthm loop$-induction-challenge-4d
(implies (and (symbol-listp lst1)
(nat-listp lst2))
(symbol-alistp
(loop$ for e in lst1
as i in lst2
collect (cons e i))))
:rule-classes nil)
(defthm loop$-induction-challenge-5a
(implies (and (nat-listp lst1)
(natp j0))
(nat-listp (loop$ for i in lst1
as j from j0 to (+ j0 (len lst1) -1)
collect (+ i j))))
:rule-classes nil)
(defthm loop$-induction-challenge-5b
(implies (and (nat-listp lst1)
(natp j0))
(nat-listp (loop$ for j from j0 to (+ j0 (len lst1) -1)
as i in lst1
collect (+ i j))))
:rule-classes nil)
(defthm loop$-induction-challenge-5c
(implies (and (nat-listp lst1)
(natp j0))
(nat-listp (loop$ for j from j0 to (+ j0 (len lst1) -1)
as l on lst1
collect (+ (car l) j))))
:rule-classes nil)
(defthm loop$-induction-challenge-5d
(implies (and (natp i0)
(natp j0))
(nat-listp (loop$ for i from i0 to maxi
as j from j0 to maxj
collect (+ i j))))
:rule-classes nil)
(defthm loop$-induction-challenge-6a
(implies (natp i0)
(equal (loop$ for e in lst as i from i0 to (+ i0 (len lst) -1) always (equal i e))
(loop$ for i from i0 to (+ i0 (len lst) -1) as e in lst always (equal i e))))
:rule-classes nil)
(defthm loop$-induction-challenge-6b
(implies (natp i0)
(equal (loop$ for e in lst as i from i0 to max always (equal i e))
(loop$ for i from i0 to max as e in lst always (equal i e))))
:rule-classes nil)
; The following theorem is not proved automatically:
; (defthm loop$-induction-challenge-7a
; (implies (and (integerp lo1) (integerp hi1)
; (integerp lo2) (integerp hi2))
; (loop$ for i from lo1 to hi1 by 1
; as j from lo2 to hi2 by 1
; always (equal (- i j) (- lo1 lo2))))
; :rule-classes nil)
; But we can prove it this way:
(encapsulate
nil
(local
(defthm lemma
(implies (and (integerp lo1)
(integerp lo2))
(equal (always$+ (LAMBDA$ (LOOP$-GVARS LOOP$-IVARS)
(EQUAL (+ (CAR LOOP$-IVARS)
(- (CADR LOOP$-IVARS)))
(+ (CAR LOOP$-GVARS)
(- (CADR LOOP$-GVARS)))))
(list lo1 lo2)
targets)
(always$+ (LAMBDA$ (LOOP$-GVARS LOOP$-IVARS)
(EQUAL (+ (CAR LOOP$-IVARS)
(- (CADR LOOP$-IVARS)))
(CAR LOOP$-GVARS)))
(list (- lo1 lo2))
targets)))))
(defthm loop$-induction-challenge-7a
(implies (and (integerp lo1) (integerp hi1)
(integerp lo2) (integerp hi2))
(loop$ for i from lo1 to hi1 by 1
as j from lo2 to hi2 by 1
always (equal (- i j) (- lo1 lo2))))
:rule-classes nil))
; We can prove essentially the same theorem, without needing the lemma, by just
; stating it differently, i.e., moving the arithmetic on lo1 and lo2 outside
; the lambda.
(defthm loop$-induction-challenge-7b
(implies (and (integerp lo1) (integerp hi1)
(integerp lo2) (integerp hi2))
(let ((diff (- lo1 lo2)))
(loop$ for i from lo1 to hi1 by 1
as j from lo2 to hi2 by 1
always (equal (- i j) diff))))
:rule-classes nil)
(defthm loop$-induction-challenge-8
(equal (loop$ for a in lst1 as b in lst2
thereis (if (equal x a) b nil))
(loop$ for b in lst2 as a in lst1
thereis (if (equal x a) b nil)))
:rule-classes nil)
(defthm loop$-induction-challenge-9
(equal (loop$ for a in lst1
as b in lst2
when (and (equal a 1)
(equal b -1))
sum (+ a b))
0)
:rule-classes nil)
|
