← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/workshops/1999/calculus/solutions/mesh-make-partition.lisp

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/workshops/1999/calculus/solutions/mesh-make-partition.lisp
 
1
(in-package "ACL2")
 
2
 
 
3
; Solution to Exercise 6.6.
 
4
 
 
5
; This solution is just barely simple enough that we do not create lemma books
 
6
; underneath it.
 
7
 
 
8
(include-book "partition-defuns")
 
9
 
 
10
; If one submits mesh-make-partition or thinks first about how the proof might
 
11
; go, one is led quickly to the decision to prove an appropriate fact about the
 
12
; mesh of (make-partition-rec a delta n), namely, mesh-make-partition-rec
 
13
; below.  When that theorem is submitted to ACL2, the following term is printed
 
14
; in a goal that does not simplify further:
 
15
 
 
16
#|
 
17
                    (CAR (MAKE-PARTITION-REC (+ A DELTA)
 
18
                                             DELTA (+ -1 N)))
 
19
|#
 
20
 
 
21
; But the first element of the result returned by make-partition-rec is clearly
 
22
; its first argument, a fact brought to the prover's attention with the first
 
23
; lemma below.
 
24
 
 
25
(encapsulate
 
26
 ()
 
27
 
 
28
 (local
 
29
  (defthm car-make-partition-rec
 
30
    (equal (car (make-partition-rec a delta n))
 
31
           a)))
 
32
 
 
33
 (defthm mesh-make-partition-rec
 
34
   (implies (and (rationalp delta)
 
35
                 (<= 0 delta)
 
36
                 (integerp n)
 
37
                 (< 0 n))
 
38
            (equal (mesh (make-partition-rec a delta n))
 
39
                   delta))
 
40
   :hints (("Goal" :expand ((make-partition-rec a delta 1))))))
 
41
 
 
42
; We need to disable the nonrecursive function symbol mesh in order for the
 
43
; rewrite rule mesh-make-partition-rec to apply when we are trying to prove
 
44
; mesh-make-partition.
 
45
(in-theory (disable mesh))
 
46
 
 
47
; The theorem mesh-make-partition now goes through automatically if we include
 
48
; an appropriate arithmetic book, e.g.,
 
49
; (include-book "/projects/acl2/v2-5/books/arithmetic/top").  However, below we
 
50
; show how one can get the theorem proved without such help.
 
51
 
 
52
; An attempt to prove mesh-make-partition causes an induction to be tried,
 
53
; which is perhaps surprising given the rewrite rule mesh-make-partition-rec,
 
54
; and is followed by failure to prove the thoerem.  Why is that?  The problem
 
55
; is that the prover cannot show that the particular delta fed to
 
56
; make-partition-rec by make-partition satisfies the nonnegativity hypothesis
 
57
; of rule mesh-make-partition-rec.  If it is not clear that this is indeed the
 
58
; issue, then see file mesh-make-partition_info.txt for an annotated transcript
 
59
; of a proof-checker session that leads us to this fact.
 
60
 
 
61
; Lemma hack2 below states that the delta in question is indeed nonnegative.
 
62
; We have to work a bit in order to prove hack2.  It seems clear if the
 
63
; distributivity law is applied in reverse, so our approach is to obtain hack2
 
64
; from a lemma hack1 that is the result of applying factoring to hack2 (and
 
65
; then simplifying and generalizing a bit).  An attempt to prove hack1, in
 
66
; turn, leads the prover to get stuck attempting to prove
 
67
; (<= 0 (* X (+ (- A) B)))
 
68
; under relevant hypotheses, which leads us to prove the lemma
 
69
; product-nonnegative below.
 
70
 
 
71
(local
 
72
 (encapsulate
 
73
  ()
 
74
 
 
75
  (local
 
76
   (defthm product-nonnegative
 
77
     (implies (and (rationalp x) (rationalp y))
 
78
              ;; If we use equal instead of iff, ACL2's linear arithmetic
 
79
              ;; doesn't happen to work.
 
80
              (iff (< (* x y) 0);; (not (<= 0 (* x y)))
 
81
                   (or (and (< 0 x) (< y 0))
 
82
                       (and (< x 0) (< 0 y)))))))
 
83
 
 
84
  (local
 
85
   (defthm hack1
 
86
     (implies (and (rationalp x) (rationalp a) (rationalp b)
 
87
                   (<= 0 x)
 
88
                   (<= a b))
 
89
              (<= 0 (* x (- b a))))
 
90
     :hints (("Goal" :in-theory (disable distributivity)))
 
91
     :rule-classes nil))
 
92
 
 
93
  (defthm hack2
 
94
    (implies (and (rationalp n)
 
95
                  (< 0 n)
 
96
                  (rationalp a)
 
97
                  (rationalp b)
 
98
                  (<= a b))
 
99
             (<= 0 (+ (* b (/ n)) (* (/ n) (- a)))))
 
100
    :hints (("Goal" :use ((:instance hack1 (x (/ n)))))))))
 
101
 
 
102
(defthm mesh-make-partition
 
103
  (implies (and (rationalp a)
 
104
                (rationalp b)
 
105
                (< a b)
 
106
                (integerp n)
 
107
                (< 0 n))
 
108
           (equal (mesh (make-partition a b n))
 
109
                  (/ (- b a) n))))