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
|
; (certify-book "equisort")
; Suppose sortfn1 and sortfn2 are two arbitrary unary functions that return
; ordered results that preserve the how-many property for every object e. Then
; they are equal.
; I constrain sortfn1 and sortfn2 and then prove this. Thus, when one
; functionally instantiates sortfn1-is-sortfn2 below, replacing the two generic
; names by specific sorting functions, nice proof obligations are produced:
; each sorting function must return an ordered list that preserves the how-many
; property.
(in-package "ACL2")
(include-book "perm")
(include-book "ordered-perms")
(include-book "convert-perm-to-how-many")
(encapsulate ((sortfn1 (x) t)
(sortfn2 (x) t))
(local (defun sortfn1-insert (e x)
(if (endp x)
(cons e x)
(if (lexorder e (car x))
(cons e x)
(cons (car x)
(sortfn1-insert e (cdr x)))))))
(local (defun sortfn1 (x)
(if (endp x)
nil
(sortfn1-insert (car x)
(sortfn1 (cdr x))))))
(local (defun sortfn2 (x) (sortfn1 x)))
(defthm orderedp-sortfn1
(orderedp (sortfn1 x)))
(defthm true-listp-sortfn1
(implies (true-listp x)
(true-listp (sortfn1 x))))
(defthm orderedp-sortfn2
(orderedp (sortfn2 x)))
(defthm true-listp-sortfn2
(implies (true-listp x)
(true-listp (sortfn2 x))))
(defthm how-many-sortfn1
(equal (how-many e (sortfn1 x))
(how-many e x)))
(defthm how-many-sortfn2
(equal (how-many e (sortfn2 x))
(how-many e x))))
(defthm weak-sortfn1-is-sortfn2
(implies (true-listp x)
(equal (sortfn1 x) (sortfn2 x)))
:hints (("Goal" :use (:instance ordered-perms
(a (sortfn1 x))
(b (sortfn2 x))))))
(encapsulate ((ssortfn1 (x) t)
(ssortfn2 (x) t))
(local (defun ssortfn1-insert (e x)
(if (endp x)
(cons e x)
(if (lexorder e (car x))
(cons e x)
(cons (car x)
(ssortfn1-insert e (cdr x)))))))
(local (defun ssortfn1 (x)
(if (endp x)
nil
(ssortfn1-insert (car x)
(ssortfn1 (cdr x))))))
(local (defun ssortfn2 (x) (ssortfn1 x)))
(defthm orderedp-ssortfn1
(orderedp (ssortfn1 x)))
(defthm true-listp-ssortfn1
(true-listp (ssortfn1 x)))
(defthm orderedp-ssortfn2
(orderedp (ssortfn2 x)))
(defthm true-listp-ssortfn2
(true-listp (ssortfn2 x)))
(defthm how-many-ssortfn1
(equal (how-many e (ssortfn1 x))
(how-many e x)))
(defthm how-many-ssortfn2
(equal (how-many e (ssortfn2 x))
(how-many e x))))
(defthm strong-ssortfn1-is-ssortfn2
(equal (ssortfn1 x) (ssortfn2 x))
:hints (("Goal" :use (:instance ordered-perms
(a (ssortfn1 x))
(b (ssortfn2 x))))))
|
