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
|
; Copyright (C) 2017, Regents of the University of Texas
; Written by Matt Kaufmann, May 2017
; License: A 3-clause BSD license. See the LICENSE file distributed with ACL2.
; Challenge problem
; Matt Kaufmann, May 2017
; The challenge is to prove sort-by-car<-preserves-assoc below. That theorem
; states that for an alist with rational keys, with no duplicate keys, assoc is
; preserved by sorting the alist by key. More specifically, the challenge is
; to create and certify a book sort-by-car-support.lisp that allows the present
; book, sort-by-car.lisp, to certify. To start, copy sort-by-car.lisp to
; sort-by-car-support.lisp and remove the form below, (local (include-book
; "sort-by-car-support")), from sort-by-car-support.lisp.
; NOTE: The solution in sort-by-car-support.lisp could probably be improved.
; It can be challenging (at least, for me) to carry out an ACL2 proof in a
; manner that exhibits the thought process when complete. It probably would
; have been better for me to include more encapsulate events, with some of the
; lemmas in that book occurring only locally in such encapsulates. I'll leave
; that as a challenge for someone else to clean up, if desired.
; Portcullis command:
#||
(defpkg "SORT-BY-CAR"
(union$
*acl2-exports*
*common-lisp-symbols-from-main-lisp-package*
:test 'eq))
||#
(in-package "SORT-BY-CAR")
(local (include-book "sort-by-car-support"))
(set-enforce-redundancy t)
(include-book "defsort/defsort" :dir :system)
(encapsulate
( ((valp *) => *) )
(local (defun valp (x) (consp x)))
(defthm booleanp-valp
(booleanp (valp x))
:rule-classes :type-prescription))
(encapsulate
( ((indexp *) => *) )
(local (defun indexp (x) (rationalp x)))
(defthm indexp-implies-rationalp
(implies (indexp x)
(rationalp x))
:rule-classes :compound-recognizer))
(defun indexed-pair-p (x)
(declare (xargs :guard t))
(and (consp x)
(indexp (car x))
(valp (cdr x))))
(defun car< (x y)
(declare (xargs :guard (and (indexed-pair-p x)
(indexed-pair-p y))))
(< (car x) (car y)))
(acl2::defsort sort-by-car<
:compare< car<
:comparablep indexed-pair-p
:true-listp t
:weak t)
(defthm sort-by-car<-preserves-assoc
(implies (and (alistp alist)
(no-duplicatesp (strip-cars alist)))
(equal (assoc index (sort-by-car< alist))
(assoc index alist))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Example application to specific defsort:
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(set-enforce-redundancy nil)
(local
(progn
(defun my-valp (x)
(declare (xargs :guard t))
(symbol-listp x))
(defun my-indexed-pair-p (x)
(declare (xargs :guard t))
(and (consp x)
(posp (car x))
(my-valp (cdr x))))
(defun my-car< (x y)
(declare (xargs :guard (and (my-indexed-pair-p x)
(my-indexed-pair-p y))))
(< (car x) (car y)))
(acl2::defsort sort-by-my-car<
:compare< my-car<
:comparablep my-indexed-pair-p
:true-listp t
:weak t)
(defthm sort-by-my-car<-preserves-assoc
(implies (and (alistp alist)
(no-duplicatesp (strip-cars alist)))
(equal (assoc index (sort-by-my-car< alist))
(assoc index alist)))
:otf-flg t
:hints (("Goal"
:in-theory (enable sort-by-car<-merge-tr
sort-by-car<-merge
sort-by-my-car<-merge
sort-by-my-car<)
:do-not-induct t
:by (:functional-instance
sort-by-car<-preserves-assoc
(valp my-valp)
(indexp posp)
(indexed-pair-p my-indexed-pair-p)
(car< my-car<)
(sort-by-car< sort-by-my-car<)
(sort-by-car<-merge sort-by-my-car<-merge)
(sort-by-car<-list-p sort-by-my-car<-list-p)
(sort-by-car<-ordered-p sort-by-my-car<-ordered-p)))))))
|
