#|
Copyright (C) 1994 by Computational Logic, Inc. All Rights Reserved.
You may copy and distribute verbatim copies of this Nqthm-1992 event script as
you receive it, in any medium, including embedding it verbatim in derivative
works, provided that you conspicuously and appropriately publish on each copy
a valid copyright notice "Copyright (C) 1994 by Computational Logic, Inc. All
Rights Reserved."
NO WARRANTY
Computational Logic, Inc. PROVIDES ABSOLUTELY NO WARRANTY. THE EVENT SCRIPT
IS PROVIDED "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESS OR IMPLIED,
INCLUDING, BUT NOT LIMITED TO, ANY IMPLIED WARRANTIES OF MERCHANTABILITY AND
FITNESS FOR A PARTICULAR PURPOSE. THE ENTIRE RISK AS TO THE QUALITY AND
PERFORMANCE OF THE SCRIPT IS WITH YOU. SHOULD THE SCRIPT PROVE DEFECTIVE, YOU
ASSUME THE COST OF ALL NECESSARY SERVICING, REPAIR OR CORRECTION.
IN NO EVENT WILL Computational Logic, Inc. BE LIABLE TO YOU FOR ANY DAMAGES,
ANY LOST PROFITS, LOST MONIES, OR OTHER SPECIAL, INCIDENTAL OR CONSEQUENTIAL
DAMAGES ARISING OUT OF THE USE OR INABILITY TO USE THIS SCRIPT (INCLUDING BUT
NOT LIMITED TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES
SUSTAINED BY THIRD PARTIES), EVEN IF YOU HAVE ADVISED US OF THE POSSIBILITY OF
SUCH DAMAGES, OR FOR ANY CLAIM BY ANY OTHER PARTY.
A Formal Model of Asynchronous Communication
and
Its Use in Mechanically Verifying a Biphase Mark Protocol
J Strother Moore
Technical Report 68
August, 1991
Abstract (of CLI Tech Report 68):
In this paper we present a formal model of asynchronous
communication as a function in the Boyer-Moore logic. The
function transforms the signal stream generated by one
processor into the signal stream consumed by an independently
clocked processor. This transformation ``blurs'' edges and
``dilates'' time due to differences in the phases and rates of
the two clocks and the communications delay. The model can be
used quantitatively to derive concrete performance bounds on
asynchronous communications at ISO protocol level 1 (physical
level). We develop part of the reusable formal theory that
permits the convenient application of the model. We use the
theory to show that a biphase mark protocol can be used to send
messages of arbitrary length between two asynchronous
processors. We study two versions of the protocol, a
conventional one which uses cells of size 32 cycles and an
unconventional one which uses cells of size 18. Our proof of
the former protocol requires the ratio of the clock rates of
the two processors to be within 3% of unity. The
unconventional biphase mark protocol permits the ratio to vary
by 5%. At nominal clock rates of 20MHz, the unconventional
protocol allows transmissions at a burst rate of slightly over
1MHz. These claims are formally stated in terms of our model
of asynchrony; the proofs of the claims have been mechanically
checked with the Boyer-Moore theorem prover, NQTHM. We
conjecture that the protocol can be proved to work under our
model for smaller cell sizes and more divergent clock rates but
the proofs would be harder. Known inadequacies of our model
include that (a) distortion due to the presence of an edge is
limited to the time span of the cycle during which the edge was
written, (b) both clocks are assumed to be linear functions of
time (i.e., the rate of a given clock is unwavering) and (c)
reading ``on an edge'' produces a nondeterministically defined
value rather than an indeterminate value. We discuss these
problems.
This event file contains all of the definitions and theorems mentioned
in CLI Tech Report 68. In addition, it contains our proof that
``deterministic fuzzy edge detection is impossible,'' which is
mentioned in a footnote of the report. However, the theorem BMP18 of
the paper is here called TOP and BMP18-LEMMA is here LOOP. In
addition, the functions lst' and ts' of the paper are here named LST+
and TS+.
This proof deals with the case of an 18-bit cell divided into
subcells of size 5 and 13. The following numeric constants, which
occur in this file, are related to this particular choice of cell
configuration. It is possible to obtain proofs of different
configurations by consistently replacing these constants and replaying
the script. The proof could be lifted to a much more general one,
but I just didn't feel like doing it.
5 = mark-size
13 = code-size
18 = cell-size = (mark-size + code-size)
17 = cell-size-1
19 = cell-size+1
10 = sampling distance = mark-size+(code-size/2)-1
4 = mark-size-1
12 = code-size-1
|#
; -------------------------------------------------------------------------
; Arithmetic
(boot-strap nqthm)
(defn rate-proximity (w r)
(and (not (lessp (times 18 w) (times 17 r)))
(not (lessp (times 19 r) (times 18 w)))))
(PROVE-LEMMA PLUS-ADD1
(REWRITE)
(EQUAL (PLUS X (ADD1 Y))
(ADD1 (PLUS X Y))))
(PROVE-LEMMA PLUS-COMMUTES1
(REWRITE)
(EQUAL (PLUS X Y) (PLUS Y X)))
(PROVE-LEMMA PLUS-COMMUTES2
(REWRITE)
(EQUAL (PLUS X Y Z) (PLUS Y X Z)))
(PROVE-LEMMA PLUS-ASSOCIATES
(REWRITE)
(EQUAL (PLUS (PLUS X Y) Z)
(PLUS X Y Z)))
(PROVE-LEMMA TIMES-0
(REWRITE)
(EQUAL (TIMES X 0) 0))
(PROVE-LEMMA TIMES-NON-NUMBERP
(REWRITE)
(IMPLIES (NOT (NUMBERP Z))
(EQUAL (TIMES X Z) 0)))
(PROVE-LEMMA TIMES-ADD1
(REWRITE)
(EQUAL (TIMES X (ADD1 Y))
(PLUS X (TIMES X Y))))
(PROVE-LEMMA TIMES-DISTRIBUTES1
(REWRITE)
(EQUAL (TIMES X (PLUS Y Z))
(PLUS (TIMES X Y) (TIMES X Z))))
(PROVE-LEMMA TIMES-COMMUTES1
(REWRITE)
(EQUAL (TIMES X Y) (TIMES Y X)))
(PROVE-LEMMA TIMES-COMMUTES2
(REWRITE)
(EQUAL (TIMES X Y Z) (TIMES Y X Z)))
(PROVE-LEMMA TIMES-ASSOCIATES
(REWRITE)
(EQUAL (TIMES (TIMES X Y) Z)
(TIMES X Y Z)))
(PROVE-LEMMA TIMES-DISTRIBUTES2
(REWRITE)
(EQUAL (TIMES (PLUS X Y) Z)
(PLUS (TIMES X Z) (TIMES Y Z))))
(PROVE-LEMMA DIFFERENCE-IS-0
(REWRITE)
(IMPLIES (NOT (LESSP Y X))
(EQUAL (DIFFERENCE X Y) 0)))
(PROVE-LEMMA DIFFERENCE-PLUS-CANCELLATION1
(REWRITE)
(EQUAL (DIFFERENCE (PLUS I X) I)
(FIX X)))
(PROVE-LEMMA DIFFERENCE-PLUS-CANCELLATION2
(REWRITE)
(EQUAL (DIFFERENCE (PLUS I X) (PLUS I Y))
(DIFFERENCE X Y)))
(PROVE-LEMMA DIFFERENCE-PLUS-CANCELLATION3
(REWRITE)
(EQUAL (DIFFERENCE (PLUS I J X) J)
(PLUS I X)))
(PROVE-LEMMA LESSP-REMAINDER
(GENERALIZE)
(EQUAL (LESSP (REMAINDER X Y) Y)
(NOT (ZEROP Y))))
(PROVE-LEMMA REMAINDER-QUOTIENT-ELIM
(ELIM REWRITE)
(IMPLIES (NUMBERP X)
(EQUAL (PLUS (REMAINDER X Y)
(TIMES Y (QUOTIENT X Y)))
X)))
(PROVE-LEMMA QUOTIENT-PLUS-TIMES
(REWRITE)
(IMPLIES (NOT (ZEROP W))
(EQUAL (QUOTIENT (PLUS V (TIMES W I)) W)
(PLUS I (QUOTIENT V W))))
((INDUCT (TIMES I W))))
(defn len (x)
(if (nlistp x) 0 (add1 (len (cdr x)))))
(PROVE-LEMMA EQUAL-LEN-0
(REWRITE)
(EQUAL (EQUAL (LEN X) 0)
(NLISTP X)))
(defn app (x y)
(if (nlistp x)
y
(cons (car x) (app (cdr x) y))))
(PROVE-LEMMA APP-CANCELLATION
(REWRITE)
(EQUAL (EQUAL (APP A B) (APP A C))
(EQUAL B C)))
(prove-lemma app-assoc (rewrite)
(equal (app (app a b) c) (app a (app b c))))
(prove-lemma len-app (rewrite)
(equal (len (app a b)) (plus (len a) (len b))))
(PROVE-LEMMA QUOTIENT-X-X
(REWRITE)
(IMPLIES (NOT (ZEROP X))
(EQUAL (QUOTIENT X X) 1)))
(PROVE-LEMMA NOT-LESSP-TIMES-QUOTIENT
(REWRITE)
(NOT (LESSP N (TIMES W (QUOTIENT N W)))))
(PROVE-LEMMA TIMES-MONOTONIC
(REWRITE)
(IMPLIES (AND (NOT (ZEROP W)) (LESSP A B))
(LESSP (TIMES W A) (TIMES W B))))
(PROVE-LEMMA DIFFERENCE-PLUS
(REWRITE)
(EQUAL (DIFFERENCE (PLUS X Y) Y)
(FIX X)))
(PROVE-LEMMA NSIG*-ALG-LEMMA-HACK1
(REWRITE)
(IMPLIES (AND (LESSP N (QUOTIENT (PLUS R X) W))
(NUMBERP W)
(NOT (EQUAL W 0)))
(EQUAL (LESSP (PLUS TS (TIMES N W))
(PLUS R TS X))
T))
((DISABLE TIMES-MONOTONIC)
(USE (TIMES-MONOTONIC (A N)
(B (QUOTIENT (PLUS R X) W))))))
(PROVE-LEMMA DIFFERENCE-PLUS-CANCELLATION-4
(REWRITE)
(EQUAL (DIFFERENCE (PLUS R TS X) (PLUS TS Y))
(DIFFERENCE (PLUS R X) Y)))
(PROVE-LEMMA NTS*-ALG-LEMMA2-HACK1
(REWRITE)
(IMPLIES
(AND (LESSP N (QUOTIENT (PLUS R X) W))
(NUMBERP X)
(NOT (EQUAL R 0))
(NUMBERP R)
(NOT (LESSP (TIMES N W) (PLUS R X)))
(NUMBERP N)
(NOT (EQUAL W 0))
(NUMBERP W)
(LESSP X W))
(EQUAL (EQUAL (QUOTIENT (PLUS R X) W)
(QUOTIENT (PLUS X
(TIMES R
(QUOTIENT (DIFFERENCE (TIMES N W) X)
R)))
W))
T))
((DISABLE TIMES-MONOTONIC)
(USE (TIMES-MONOTONIC (A N)
(B (QUOTIENT (PLUS R X) W))
(W W)))))
(PROVE-LEMMA TIMES-CANCELLATION1
(REWRITE)
(IMPLIES (NOT (ZEROP I))
(EQUAL (EQUAL (TIMES I J) (TIMES I K))
(EQUAL (FIX J) (FIX K))))
((INDUCT (LESSP J K))))
(PROVE-LEMMA TIMES-CANCELLATION2
(REWRITE)
(IMPLIES (NOT (ZEROP W))
(EQUAL (EQUAL (PLUS (TIMES W X) (TIMES W Y))
(TIMES W Z))
(EQUAL (PLUS X Y) (FIX Z))))
((DISABLE TIMES-CANCELLATION1)
(USE (TIMES-CANCELLATION1 (I W)
(J (PLUS X Y))
(K Z)))))
(PROVE-LEMMA DIFFERENCE-DIFFERENCE
(REWRITE)
(IMPLIES (NOT (LESSP B C))
(EQUAL (DIFFERENCE A (DIFFERENCE B C))
(DIFFERENCE (PLUS A C) B))))
(PROVE-LEMMA DIFFERENCE-DIFFERENCE-OTHER
(REWRITE)
(EQUAL (DIFFERENCE (DIFFERENCE A B) C)
(DIFFERENCE A (PLUS B C))))
(PROVE-LEMMA QUOTIENT-PLUS-TIMES2
(REWRITE)
(IMPLIES (NOT (ZEROP W))
(EQUAL (QUOTIENT (PLUS V (TIMES I W) (TIMES W J))
W)
(PLUS I J (QUOTIENT V W))))
((DISABLE QUOTIENT-PLUS-TIMES)
(USE (QUOTIENT-PLUS-TIMES (I (PLUS I J))))))
(prove-lemma difference-elim (elim)
(implies (and (numberp i)
(not (lessp i j)))
(equal (plus j (difference i j)) i)))
(PROVE-LEMMA QUOTIENT-DIFFERENCE
(REWRITE)
(IMPLIES (AND (NOT (ZEROP W))
(NOT (LESSP A (TIMES W B))))
(EQUAL (QUOTIENT (DIFFERENCE A (TIMES W B))
W)
(DIFFERENCE (QUOTIENT A W) B))))
(PROVE-LEMMA QUOTIENT-MONOTONIC-LEMMA
(REWRITE)
(IMPLIES (AND (LESSP Z1 Y)
(LESSP Z2 Y)
(NOT (EQUAL Y 0))
(NUMBERP Y)
(LESSP X V))
(EQUAL (LESSP (PLUS Z1 (TIMES Y X))
(PLUS Z2 (TIMES V Y)))
T))
((INDUCT (LESSP X V))))
(PROVE-LEMMA NTR*-ALG-LEMMA2-HACK1
(REWRITE)
(IMPLIES (AND (LESSP N (QUOTIENT (PLUS R X) W))
(NUMBERP X)
(NOT (EQUAL R 0))
(NUMBERP R)
(NOT (LESSP (PLUS TS (TIMES N W))
(PLUS R TS X)))
(NUMBERP N)
(NUMBERP TS)
(NOT (EQUAL W 0))
(NUMBERP W)
(NOT (LESSP (PLUS TS X) TS))
(LESSP (PLUS TS X) (PLUS TS W)))
(EQUAL (EQUAL (PLUS R TS X)
(PLUS TS X
(TIMES R
(QUOTIENT (DIFFERENCE (TIMES N W) X)
R))))
T))
((DISABLE TIMES-MONOTONIC)
(USE (TIMES-MONOTONIC (A N)
(B (QUOTIENT (PLUS R X) W))
(W W)))))
(PROVE-LEMMA NOT-LESSP-TIMES-QUOTIENT-OTHER
(REWRITE)
(IMPLIES (NOT (LESSP X R))
(NOT (LESSP (TIMES R (QUOTIENT X R)) R))))
(PROVE-LEMMA QUOTIENT-MONOTONIC
(REWRITE)
(IMPLIES (AND (NOT (ZEROP W))
(NOT (LESSP A B)))
(EQUAL (LESSP (QUOTIENT A W) (QUOTIENT B W))
F)))
(PROVE-LEMMA NLST*-ALG-LEMMA2-HACK1
(REWRITE)
(IMPLIES
(AND (NUMBERP X)
(NOT (EQUAL R 0))
(NUMBERP R)
(NOT (LESSP (PLUS TS (TIMES N W))
(PLUS R TS X)))
(NUMBERP N)
(NUMBERP TS)
(NOT (EQUAL W 0))
(NUMBERP W)
(NOT (LESSP (PLUS TS X) TS))
(LESSP (PLUS TS X) (PLUS TS W)))
(EQUAL
(PLUS
(QUOTIENT (PLUS R X) W)
(QUOTIENT (DIFFERENCE (PLUS X
(TIMES R
(QUOTIENT (DIFFERENCE (TIMES N W) X)
R)))
(TIMES W (QUOTIENT (PLUS R X) W)))
W))
(QUOTIENT (PLUS X
(TIMES R
(QUOTIENT (DIFFERENCE (TIMES N W) X)
R)))
W)))
((DISABLE QUOTIENT-DIFFERENCE)
(USE
(QUOTIENT-DIFFERENCE (W W)
(A (PLUS X
(TIMES R
(QUOTIENT (DIFFERENCE (TIMES N W) X)
R))))
(B (QUOTIENT (PLUS R X) W))))))
(PROVE-LEMMA NSIG*-UPPER-BOUND-LEMMA1
(REWRITE)
(IMPLIES (NOT (ZEROP R))
(NOT (LESSP (QUOTIENT (TIMES N W) R)
(QUOTIENT (DIFFERENCE (TIMES N W)
(DIFFERENCE TR TS))
R)))))
(PROVE-LEMMA QUOTIENT-TIMES
(REWRITE)
(IMPLIES (NOT (ZEROP R))
(EQUAL (QUOTIENT (TIMES N R) R)
(FIX N)))
((DISABLE QUOTIENT-PLUS-TIMES)
(USE (QUOTIENT-PLUS-TIMES (W R)
(V 0)
(I N)))))
(PROVE-LEMMA MULTIPLY-BOTH-SIDES-OF-LESSP
(REWRITE)
(IMPLIES (NOT (ZEROP R))
(EQUAL (LESSP (TIMES A R) (TIMES B R))
(LESSP A B))))
(PROVE-LEMMA LESSP-QUOTIENT-TO-LESSP-TIMES-LEMMA1 NIL
(IMPLIES (AND (NOT (ZEROP R))
(NOT (LESSP (QUOTIENT X R) N)))
(NOT (LESSP X (TIMES N R))))
((DISABLE MULTIPLY-BOTH-SIDES-OF-LESSP)
(USE (MULTIPLY-BOTH-SIDES-OF-LESSP (A (QUOTIENT X R))
(B N)))))
(PROVE-LEMMA LESSP-QUOTIENT-TO-LESSP-TIMES-LEMMA2 NIL
(IMPLIES (AND (NOT (ZEROP R))
(NOT (LESSP X (TIMES N R))))
(NOT (LESSP (QUOTIENT X R) N)))
((DISABLE QUOTIENT-MONOTONIC)
(USE (QUOTIENT-MONOTONIC (A X)
(B (TIMES N R))
(W R)))))
(PROVE-LEMMA LESSP-QUOTIENT-TO-LESSP-TIMES
(REWRITE)
(IMPLIES (NOT (ZEROP R))
(EQUAL (LESSP (QUOTIENT X R) N)
(LESSP X (TIMES N R))))
((USE (LESSP-QUOTIENT-TO-LESSP-TIMES-LEMMA1)
(LESSP-QUOTIENT-TO-LESSP-TIMES-LEMMA2))))
(PROVE-LEMMA QUOTIENT-PLUS-TIMES1
(REWRITE)
(IMPLIES (NOT (ZEROP R))
(EQUAL (QUOTIENT (PLUS (TIMES N R) Z) R)
(PLUS N (QUOTIENT Z R))))
((DISABLE QUOTIENT-PLUS-TIMES)
(USE (QUOTIENT-PLUS-TIMES (V Z)
(I N)
(W R)))))
(PROVE-LEMMA EQUAL-TIMES-0
(REWRITE)
(EQUAL (EQUAL (TIMES I J) 0)
(OR (ZEROP I) (ZEROP J))))
(PROVE-LEMMA NSIG*-UPPER-BOUND-HACK1
(REWRITE)
(IMPLIES (AND (NOT (ZEROP R))
(NOT (LESSP R (TIMES 18 DELTA)))
(LESSP N 18))
(EQUAL (LESSP (TIMES N DELTA) R) T)))
(PROVE-LEMMA NSIG*-UPPER-BOUND-HACK2
(REWRITE)
(IMPLIES (AND (NOT (LESSP (PLUS R R (TIMES 17 R))
(PLUS W (TIMES 17 W))))
(NOT (LESSP (PLUS W (TIMES 17 W))
(TIMES 17 R)))
(NOT (ZEROP W))
(NOT (ZEROP R))
(NOT (ZEROP N))
(LESSP N 18)
(LESSP W R))
(EQUAL (PLUS W (TIMES W (SUB1 N)))
(PLUS (TIMES (SUB1 N) (DIFFERENCE R W))
(DIFFERENCE W
(TIMES (SUB1 N) (DIFFERENCE R W)))
(TIMES W (SUB1 N))))))
(PROVE-LEMMA QUOTIENT-PLUS-TIMES3
(REWRITE)
(IMPLIES (NOT (ZEROP (PLUS X Z (TIMES X N))))
(EQUAL (QUOTIENT (PLUS Z
(TIMES X N)
(TIMES Z N)
(TIMES X N N))
(PLUS X Z (TIMES X N)))
(PLUS N
(QUOTIENT Z (PLUS X Z (TIMES N X))))))
((DISABLE QUOTIENT-PLUS-TIMES)
(USE (QUOTIENT-PLUS-TIMES (V Z)
(W (PLUS X Z (TIMES X N)))
(I N)))))
(PROVE-LEMMA NSIG*-UPPER-BOUND-HACK3
(REWRITE)
(IMPLIES (LESSP (PLUS Z (TIMES X (SUB1 N)))
(PLUS X Z (TIMES X (SUB1 N))))
(EQUAL (LESSP Z
(PLUS X Z (TIMES X (SUB1 N))))
T)))
(PROVE-LEMMA INTRO-DELTA NIL
(IMPLIES (AND (NUMBERP W) (NOT (LESSP W R)))
(EQUAL W (PLUS R (DIFFERENCE W R)))))
(PROVE-LEMMA NSIG*-UPPER-BOUND-LEMMA2-1 NIL
(IMPLIES (AND (NUMBERP N)
(NOT (ZEROP W))
(NOT (ZEROP R))
(RATE-PROXIMITY W R)
(LESSP N 18)
(NOT (LESSP W R)))
(EQUAL (QUOTIENT (TIMES N W) R) N))
((USE (INTRO-DELTA))))
(PROVE-LEMMA NSIG*-UPPER-BOUND-LEMMA2-2 NIL
(IMPLIES (AND (NUMBERP N)
(NOT (ZEROP W))
(NOT (ZEROP R))
(RATE-PROXIMITY W R)
(LESSP N 18)
(LESSP W R))
(EQUAL (QUOTIENT (TIMES N W) R)
(SUB1 N)))
((EXPAND (TIMES N W))))
(PROVE-LEMMA NSIG*-UPPER-BOUND-LEMMA2-EQUALITY
(REWRITE)
(IMPLIES (AND (NUMBERP N)
(NOT (ZEROP W))
(NOT (ZEROP R))
(RATE-PROXIMITY W R)
(LESSP N 18))
(EQUAL (QUOTIENT (TIMES N W) R)
(IF (LESSP W R) (SUB1 N) N)))
((DISABLE TIMES)
(USE (NSIG*-UPPER-BOUND-LEMMA2-1)
(NSIG*-UPPER-BOUND-LEMMA2-2))))
(PROVE-LEMMA NSIG*-UPPER-BOUND-LEMMA2
(REWRITE)
(IMPLIES (AND (NUMBERP N)
(NOT (ZEROP W))
(NOT (ZEROP R))
(RATE-PROXIMITY W R)
(LESSP N 18))
(NOT (LESSP N (QUOTIENT (TIMES N W) R)))))
(PROVE-LEMMA NSIG*-LOWER-BOUND-LEMMA1
(REWRITE)
(IMPLIES (AND (NOT (ZEROP R))
(NOT (LESSP W TR-TS)))
(NOT (LESSP (QUOTIENT (DIFFERENCE (TIMES N W) TR-TS)
R)
(QUOTIENT (TIMES (SUB1 N) W) R)))))
(PROVE-LEMMA LESSP-TIMES
(REWRITE)
(IMPLIES (NOT (ZEROP N))
(NOT (LESSP (TIMES N W) W))))
(PROVE-LEMMA PLUS-CANCELLATION
(REWRITE)
(EQUAL (EQUAL (PLUS I J) (PLUS I K))
(EQUAL (FIX J) (FIX K))))
(defn boolp (x)
(or (equal x t) (equal x f)))
(disable boolp)
(PROVE-LEMMA BOOLP-T
(REWRITE)
(IMPLIES (AND (BOOLP X) X)
(EQUAL (EQUAL T X) T))
((ENABLE BOOLP)))
(defn b-not (x) (not x))
(disable b-not)
(defn b-xor (x y)
(if x (not y) (if y t f)))
(disable b-xor)
(prove-lemma b-xor-b-not (rewrite)
(and (b-xor x (b-not x))
(b-xor (b-not x) x))
((enable b-xor b-not)))
(defn smooth (prev-val lst)
(if (nlistp lst)
nil
(if (b-xor prev-val (car lst))
(cons 'q (smooth (car lst) (cdr lst)))
(cons (car lst) (smooth (car lst) (cdr lst))))))
(defn reconcile-signals (a b)
(if (equal a b) a 'q))
(defn sig (lst ts tr w)
(if (nlistp lst)
'q
(if (lessp (plus ts w) tr)
(reconcile-signals (car lst)
(sig (cdr lst) (plus ts w) tr w))
(car lst))))
(defn endp (lst ts tr w)
(if (nlistp lst)
t
(if (lessp (plus ts w) tr)
(endp (cdr lst) (plus ts w) tr w)
f)))
(defn lst+ (lst ts nxtr w)
(if (nlistp lst)
lst
(if (lessp nxtr (plus ts w))
lst
(lst+ (cdr lst) (plus ts w) nxtr w))))
(defn ts+ (lst ts nxtr w)
(if (nlistp lst)
ts
(if (lessp nxtr (plus ts w))
ts
(ts+ (cdr lst) (plus ts w) nxtr w))))
(prove-lemma lst+-weakly-shortens-lst (rewrite)
(not (lessp (count lst)
(count (lst+ lst ts tr w)))))
(prove-lemma ts+-increases-tr (rewrite)
(implies (and (not (endp lst ts (plus r tr) w))
(not (zerop r))
(equal (count lst)
(count (lst+ lst ts (plus r tr) w))))
(equal
(lessp (difference (plus w (ts+ lst ts (plus r tr) w))
(plus r tr))
(difference (plus ts w)
tr))
t))
((expand (lst+ lst ts (plus r tr) w)
(ts+ lst ts (plus r tr) w))))
(defn warp (lst ts tr w r)
(if (or (zerop r)
(endp lst ts (plus tr r) w))
nil
(cons (sig lst ts (plus tr r) w)
(warp (lst+ lst ts (plus tr r) w)
(ts+ lst ts (plus tr r) w)
(plus tr r)
w r)))
((ord-lessp (cons (cons (add1 (count lst)) 0)
(difference (plus ts w) tr)))))
(defn det (lst oracle)
(if (nlistp lst)
lst
(if (equal (car lst) 'q)
(cons (if (car oracle) t f) (det (cdr lst) (cdr oracle)))
(cons (car lst) (det (cdr lst) oracle)))))
(defn async (lst ts tr w r oracle)
(det (warp (smooth t lst) ts tr w r)
oracle))
(defn listn (n value)
(if (zerop n)
nil
(cons value
(listn (sub1 n) value))))
(defn csig (prev-signal bit)
; CSIG stands for "contents signal"
(if bit prev-signal (b-not prev-signal)))
(defn cell (prev-signal n1 n2 bit)
(app (listn n1 (b-not prev-signal))
(listn n2 (csig prev-signal bit))))
(defn cells (prev-signal n1 n2 msg)
(if (nlistp msg)
nil
(app (cell prev-signal n1 n2 (car msg))
(cells (csig prev-signal (car msg)) n1 n2 (cdr msg)))))
(defn send (msg pad1 n1 n2 pad2)
(app (listn pad1 t)
(app (cells t n1 n2 msg)
(listn pad2 t))))
(defn scan (prev-signal lst)
(if (nlistp lst)
nil
(if (b-xor prev-signal (car lst))
lst
(scan prev-signal (cdr lst)))))
(defn cdrn (n lst)
(if (zerop n) lst (cdrn (sub1 n) (cdr lst))))
(defn nth (n lst)
(car (cdrn n lst)))
(defn recv-bit (k lst)
(if (b-xor (car lst) (nth k lst)) t f))
(defn recv (i flg k lst)
(if (zerop i)
nil
(cons (recv-bit k (scan flg lst))
(recv (sub1 i)
(nth k (scan flg lst))
k
(cdrn k (scan flg lst))))))
(defn bvp (x)
(if (nlistp x)
(equal x nil)
(and (boolp (car x))
(bvp (cdr x)))))
#|
We can now state the top level theorem without proof.
(prove-lemma top nil
(implies (and (bvp msg)
(numberp ts)
(numberp tr)
(not (zerop w))
(not (zerop r))
(not (lessp tr ts))
(lessp tr (plus ts w))
(rate-proximity w r)
(numberp p1))
(equal (recv (len msg)
t
10
(async (send msg p1 5 13 p2)
ts tr w r oracle))
msg)))
We will prove this by first massaging it into a different form,
suitable for induction. The inductive form shall be called loop
instead of top.
|#
(disable listn)
(disable *1*listn)
(disable cell)
(disable *1*cell)
(disable csig)
(disable *1*csig)
(disable boolp)
(disable smooth)
(disable warp)
(disable det)
(disable recv-bit)
(disable scan)
(disable send)
(prove-lemma b-xor-x-x (rewrite)
(not (b-xor x x))
((enable b-xor)))
; Our first goal will be to transform the recv-async-send theorem
; into the form we will prove inductively. This is done by moving
; the initial header out through the smooth, warp, det, and recv, milking
; a 'q out of the smooth and easing it through the warp to nestle a
; cdrn around the smooth and leaving the det hanging on a q string.
; Because the warping is harder than the smoothing, we'll do it first.
(defn lst* (lst ts tr w r)
(if (or (zerop r)
(endp lst ts (plus tr r) w))
lst
(lst* (lst+ lst ts (plus tr r) w)
(ts+ lst ts (plus tr r) w)
(plus tr r)
w r))
((ord-lessp (cons (cons (add1 (count lst)) 0)
(difference (plus ts w) tr)))))
(defn ts* (lst ts tr w r)
(if (or (zerop r)
(endp lst ts (plus tr r) w))
ts
(ts* (lst+ lst ts (plus tr r) w)
(ts+ lst ts (plus tr r) w)
(plus tr r)
w r))
((ord-lessp (cons (cons (add1 (count lst)) 0)
(difference (plus ts w) tr)))))
(defn tr* (lst ts tr w r)
(if (or (zerop r)
(endp lst ts (plus tr r) w))
tr
(tr* (lst+ lst ts (plus tr r) w)
(ts+ lst ts (plus tr r) w)
(plus tr r)
w r))
((ord-lessp (cons (cons (add1 (count lst)) 0)
(difference (plus ts w) tr)))))
(prove-lemma not-lessp-ts+ (rewrite)
(implies (and (not (lessp tr ts))
(not (zerop w)))
(not (lessp tr (ts+ lst ts tr w)))))
(prove-lemma lessp-ts+ (rewrite)
(implies (and (not (endp lst ts tr w))
(not (lessp tr ts))
(not (zerop w)))
(lessp tr (plus w (ts+ lst ts tr w)))))
(prove-lemma lst+-app (rewrite)
(implies (and (not (endp lst1 ts tr+ w))
(not (zerop w)))
(equal (lst+ (app lst1 lst2) ts tr+ w)
(app (lst+ lst1 ts tr+ w) lst2))))
(prove-lemma ts+-app (rewrite)
(implies (and (not (endp lst1 ts tr+ w))
(not (zerop w)))
(equal (ts+ (app lst1 lst2) ts tr+ w)
(ts+ lst1 ts tr+ w))))
(prove-lemma sig-app (rewrite)
(implies (and (not (endp lst1 ts tr+ w))
(not (zerop w)))
(equal (sig (app lst1 lst2) ts tr+ w)
(sig lst1 ts tr+ w))))
(prove-lemma endp-app (rewrite)
(implies (and (not (endp lst1 ts tr+ w))
(not (zerop w)))
(not (endp (app lst1 lst2) ts tr+ w))))
(defn target (x) x)
(disable target)
(prove-lemma warp-app (rewrite)
(implies (and (numberp ts)
(numberp tr)
(not (lessp tr ts))
(lessp tr (plus ts w))
(not (zerop w))
(not (zerop r)))
(equal (target (warp (app lst1 lst2) ts tr w r))
(app (warp lst1 ts tr w r)
(warp (app (lst* lst1 ts tr w r) lst2)
(ts* lst1 ts tr w r)
(tr* lst1 ts tr w r)
w r))))
((enable target warp)))
; The above lemma, when applied, will generate (warp (listn p1 t) ...)
; and (lst* (listn p1 t) ...) which we now simplify.
(defn nlst+ (n ts tr w)
(if (zerop n)
n
(if (lessp tr (plus ts w))
n
(nlst+ (sub1 n) (plus ts w) tr w))))
(prove-lemma len-lst+ (rewrite)
(equal (len (lst+ lst ts tr w))
(nlst+ (len lst) ts tr w)))
(defn nts+ (n ts tr w)
(if (zerop n)
ts
(if (lessp tr (plus ts w))
ts
(nts+ (sub1 n) (plus ts w) tr w))))
(prove-lemma len-ts+ (rewrite)
(equal (ts+ lst ts tr w)
(nts+ (len lst) ts tr w)))
(defn nendp (n ts tr w)
(if (zerop n)
t
(if (lessp (plus ts w) tr)
(nendp (sub1 n) (plus ts w) tr w)
f)))
(prove-lemma len-endp (rewrite)
(equal (endp lst ts tr w)
(nendp (len lst) ts tr w)))
(prove-lemma lessp-nlst+ (rewrite)
(not (lessp n (nlst+ n ts tr w))))
(prove-lemma nlst+-equal-n (rewrite)
(equal (equal (nlst+ n ts (plus r tr) w) n)
(or (zerop n) (lessp (plus r tr) (plus ts w)))))
(defn nlst* (n ts tr w r)
(if (or (zerop r)
(nendp n ts (plus tr r) w))
n
(nlst* (nlst+ n ts (plus tr r) w)
(nts+ n ts (plus tr r) w)
(plus tr r)
w r))
((ord-lessp (cons (cons (add1 n) 0)
(difference (plus ts w) tr)))))
(prove-lemma len-lst* (rewrite)
(equal (len (lst* lst ts tr w r))
(nlst* (len lst) ts tr w r)))
(defn nts* (n ts tr w r)
(if (or (zerop r)
(nendp n ts (plus tr r) w))
ts
(nts* (nlst+ n ts (plus tr r) w)
(nts+ n ts (plus tr r) w)
(plus tr r)
w r))
((ord-lessp (cons (cons (add1 n) 0)
(difference (plus ts w) tr)))))
(prove-lemma len-ts* (rewrite)
(equal (ts* lst ts tr w r)
(nts* (len lst) ts tr w r)))
(defn ntr* (n ts tr w r)
(if (or (zerop r)
(nendp n ts (plus tr r) w))
tr
(ntr* (nlst+ n ts (plus tr r) w)
(nts+ n ts (plus tr r) w)
(plus tr r)
w r))
((ord-lessp (cons (cons (add1 n) 0)
(difference (plus ts w) tr)))))
(prove-lemma len-tr* (rewrite)
(equal (tr* lst ts tr w r)
(ntr* (len lst) ts tr w r)))
(prove-lemma len-listn (rewrite)
(equal (len (listn n flg)) (fix n))
((enable listn)))
(defn lastn (n lst)
(if (equal n (len lst))
lst
(if (nlistp lst)
lst
(lastn n (cdr lst)))))
(defn tailp (x lst)
(if (equal x lst)
t
(if (nlistp lst)
f
(tailp x (cdr lst)))))
(prove-lemma tailp-transitive (rewrite)
(implies (and (tailp x y) (tailp y z)) (tailp x z)))
(prove-lemma tailp-lst+ (rewrite)
(tailp (lst+ lst ts tr w) lst))
(prove-lemma tailp-lst* (rewrite)
(tailp (lst* lst ts tr w r) lst))
(prove-lemma len-lastn (rewrite)
(equal (len (lastn n lst))
(if (lessp (len lst) n)
0
(fix n))))
(prove-lemma tailp-implies-lastn-len (rewrite)
(implies (tailp x y)
(equal (lastn (len x) y) x)))
(prove-lemma lst*-is-lastn nil
(equal (lastn (len (lst* lst ts tr w r)) lst)
(lst* lst ts tr w r))
((disable len-lst*)))
(defn properp (x)
(if (nlistp x)
(equal x nil)
(properp (cdr x))))
(prove-lemma lastn-nil (rewrite)
(implies (and (properp lst)
(lessp (len lst) n))
(equal (lastn n lst) nil)))
(prove-lemma properp-listn (rewrite)
(properp (listn n flg))
((enable listn)))
(prove-lemma lastn-listn (rewrite)
(implies (and (numberp n)
(numberp k)
(not (lessp k n)))
(equal (lastn n (listn k flg))
(listn n flg)))
((enable listn)
(induct (listn k flg))))
(prove-lemma lessp-nlst* (rewrite)
(not (lessp n (nlst* n ts tr w r))))
(prove-lemma lst*-listn (rewrite)
(implies (numberp n)
(equal (lst* (listn n flg) ts tr w r)
(listn (nlst* n ts tr w r) flg)))
((use (lst*-is-lastn (lst (listn n flg))))))
(defn n* (n ts tr w r)
(if (or (zerop r)
(nendp n ts (plus tr r) w))
0
(add1 (n* (nlst+ n ts (plus tr r) w)
(nts+ n ts (plus tr r) w)
(plus tr r)
w r)))
((ord-lessp (cons (cons (add1 n) 0)
(difference (plus ts w) tr)))))
(prove-lemma not-lessp-nts+ (rewrite)
(implies (and (not (lessp tr ts))
(not (zerop w)))
(not (lessp tr (nts+ n ts tr w)))))
(prove-lemma lessp-nts+ (rewrite)
(implies (and (not (nendp n ts tr w))
(not (lessp tr ts))
(not (zerop w)))
(lessp tr
(plus w (nts+ n ts tr w)))))
(prove-lemma lst+-listn (rewrite)
(implies (and (numberp n)
(not (nendp n ts tr+ w))
(not (zerop w)))
(equal (lst+ (listn n flg) ts tr+ w)
(listn (nlst+ n ts tr+ w) flg)))
((enable listn)))
(prove-lemma sig-listn (rewrite)
(implies (and (not (equal r 0))
(numberp r)
(not (nendp n ts (plus r tr) w))
(numberp n)
(numberp ts)
(numberp tr)
(not (lessp tr ts))
(lessp tr (plus ts w))
(not (equal w 0))
(numberp w))
(equal (sig (listn n flg)
ts
(plus r tr)
w)
flg))
((enable listn)))
(prove-lemma warp-listn (rewrite)
(implies (and (numberp n)
(numberp ts)
(numberp tr)
(not (lessp tr ts))
(lessp tr (plus ts w))
(not (zerop w))
(not (zerop r)))
(equal (warp (listn n flg) ts tr w r)
(listn (n* n ts tr w r) flg)))
((induct (n* n ts tr w r))
(enable listn)
(expand (warp (listn n flg) ts tr w r))))
(prove-lemma lst+-app-gap (rewrite)
(implies (and (numberp ts)
(numberp tr+)
(nendp (len pad) ts tr+ w))
(equal (lst+ (app pad lst)
ts tr+ w)
(lst+ lst
(plus ts (times (len pad) w))
tr+ w)))
((induct (endp pad ts tr+ w))))
(prove-lemma nts+-app-gap (rewrite)
(implies (and (numberp ts)
(numberp tr+)
(numberp k)
(nendp k ts tr+ w))
(equal (nts+ (plus n k) ts tr+ w)
(nts+ n (plus ts (times k w)) tr+ w))))
(prove-lemma warp-app-gap (rewrite)
(implies (and (numberp ts)
(not (zerop r))
(nendp (len pad) ts (plus r tr) w))
(equal (warp (app pad lst)
ts tr w r)
(if (nendp (plus (len pad) (len lst))
ts
(plus r tr)
w)
nil
(cons (sig (app pad lst)
ts
(plus r tr)
w)
(warp (lst+ lst
(plus ts (times (len pad) w))
(plus r tr)
w)
(nts+ (len lst)
(plus ts (times (len pad) w))
(plus r tr)
w)
(plus r tr)
w r)))))
((expand (warp (app pad lst) ts tr w r))))
(prove-lemma nendp-nlst* (rewrite)
(implies (and (numberp ts)
(numberp tr)
(not (zerop r))
(not (zerop w))
(not (lessp tr ts))
(lessp tr (plus ts w)))
(nendp (nlst* k ts tr w r)
(nts* k ts tr w r)
(plus r (ntr* k ts tr w r))
w)))
(defn nqg (k ts tr w r)
; Suppose we are at the front of a gap of len k, consisting of identical
; signals. I.e., (nendp k ts (plus r tr) w) holds and the next k signals
; are all the same. Suppose the k+1st signal is a 'q and that is followed
; by as many more signals as we wish. How many q's do we spit out till we
; get past the q we see? We assume the clock periods are within a factor
; of 2.
(if (lessp (plus r tr)
(plus w ts (times w k)))
(if (lessp (plus r r tr)
(plus w ts (times w k)))
3 ; case c
2) ; case d
1)) ; case e
#|
(defn dwg (k ts tr w r)
; I have gotten this function wrong more times than I care to admit.
; I won't even try to explain the "logic" behind this defn.
(let ((ts1 (plus ts (times k w)))
(ts2 (plus ts w (times k w)))
(ts3 (plus ts w w (times k w)))
(tr1 (plus r tr))
(tr2 (plus r r tr)))
(cond ((lessp tr1 ts2)
(if (lessp tr2 ts3) 0 1))
((equal tr1 ts2) 0)
((and (lessp ts2 tr1) (lessp tr1 ts3)) 0)
((lessp tr1 ts3) 0)
(t 1))))
|#
(defn dwg (k ts tr w r)
; I have gotten this function wrong more times than I care to admit.
; I won't even try to explain the "logic" behind this defn.
(if (lessp (plus r tr)
(plus ts w (times k w)))
(if (lessp (plus r r tr) (plus ts w w (times k w)))
0
1)
(if (equal (plus r tr) (plus ts w (times k w)))
0
(if (and (lessp (plus ts w (times k w)) (plus r tr))
(lessp (plus r tr) (plus ts w w (times k w))))
0
(if (lessp (plus r tr) (plus ts w w (times k w)))
0
1)))))
(defn tsg (k ts tr w r)
; The value of ts after processing the gap described in nqg.
(plus ts ; the header in n1
(times w k) ; the gap of k
w ; the q
(times w (dwg k ts tr w r)))) ; the eaten element of n2
(defn trg (k ts tr w r)
; The tr value after processing the gap.
(plus tr ; the header in k
(times r (nqg k ts tr w r)))) ; the qs
(prove-lemma not-lessp-ntr*-nts* (rewrite)
(implies (and (numberp ts)
(numberp tr)
(not (lessp tr ts))
(lessp tr (plus ts w))
(not (zerop w)))
(not (lessp (ntr* k ts tr w r) (nts* k ts tr w r)))))
(prove-lemma lessp-ntr*-nts* (rewrite)
(implies (and (numberp ts)
(numberp tr)
(not (lessp tr ts))
(lessp tr (plus ts w))
(not (zerop w)))
(lessp (ntr* k ts tr w r) (plus w (nts* k ts tr w r)))))
(prove-lemma nendp-is-usually-f
(rewrite)
(implies (and (numberp ts)
(numberp tr)
(not (equal w 0))
(numberp w)
(not (equal r 0))
(numberp r)
(lessp tr (plus ts w))
(lessp w (times 2 r))
(lessp r (times 2 w))
(lessp 2 k))
(not (nendp k ts (plus r tr) w)))
((expand (nendp k ts (plus r tr) w)
(nendp (sub1 k)
(plus ts w)
(plus r tr)
w)
(nendp (sub1 (sub1 k))
(plus ts w w)
(plus r tr)
w))))
; Note: The following is the nts+ analogue of ts+-app. However the
; rule is a little strange because one naturally would have written
; (nts+ (plus k rest) ...) since k is here the len of the initial
; portion of the list being scanned. But in my actual application,
; the plus has been commuted so I commute it here.
(prove-lemma lessp-plus-nts*-times-w-nlst*-plus-r-ntr*-lemma (rewrite)
(implies (and (nendp k ts (plus r tr) w)
(numberp ts)
(numberp tr)
(not (equal w 0))
(numberp w)
(not (equal r 0))
(numberp r)
(not (lessp (plus r tr) ts))
(lessp tr (plus ts w)))
(not (lessp (plus r tr)
(plus ts (times k w))))))
(prove-lemma not-lessp-plus-r-ntr*-plus-nts*-times-w-nlst* (rewrite)
(implies (and (numberp ts)
(numberp tr)
(not (zerop w))
(not (zerop r))
(not (lessp tr ts))
(lessp tr (plus ts w)))
(not (lessp (plus r (ntr* k ts tr w r))
(plus (nts* k ts tr w r)
(times w (nlst* k ts tr w r)))))))
; That takes care of ts'<=tr'. Now I'll get tr' < ts'+w. In our case,
; ts' is (nts+ m ts'' tr' w r). Now nts+ is going to push ts'' to within
; w or tr' unless m runs out. So we have to make an argument that
; m is big enough. It turns out that we know m is at least 18
; (because it is the encoding of a listp msg) and so if we assume w and r
; are within a factor of 2 of eachother, we can manage.
; These helper lemmas are generated mechanically by just grabbing
; the unproved goals generated in the next real theorem and forcing
; the expansion of the relevant terms. Chances are there are some
; irrelevant hypotheses. Some helper's subsumed others or changed the
; course of the proof so as to make others irrelevant. Thus, their
; numbering is not consecutive.
(prove-lemma helper1 (rewrite)
(implies (and (numberp ts)
(numberp tr)
(not (equal w 0))
(numberp w)
(not (equal r 0))
(numberp r)
(not (lessp tr ts))
(lessp tr (plus ts w))
(lessp w (times 2 r))
(lessp r (times 2 w))
(listp rest)
(lessp (plus ts w w) (plus r tr))
(lessp (plus ts w) (plus r tr))
(not (lessp (plus r tr) (plus ts w w))))
(equal (warp (lst+ rest
(plus ts w w)
(plus r tr)
w)
(nts+ (len rest)
(plus ts w w)
(plus r tr)
w)
(plus r tr)
w r)
(warp rest
(plus ts w w)
(plus r tr)
w r)))
((expand (lst+ rest
(plus ts w w)
(plus r tr)
w)
(nts+ (len rest)
(plus ts w w)
(plus r tr)
w))))
(prove-lemma helper5 (rewrite)
(implies (and (numberp ts)
(numberp tr)
(numberp k)
(not (equal w 0))
(numberp w)
(not (equal r 0))
(numberp r)
(not (lessp tr ts))
(lessp tr (plus ts w))
(lessp w (times 2 r))
(lessp r (times 2 w))
(listp rest)
(listp (cdr rest))
(equal (sub1 (sub1 k)) 0)
(lessp (plus ts w w) (plus r tr))
(lessp (plus ts w) (plus r tr))
(lessp (plus r tr)
(plus ts w (times k w)))
(not (lessp (plus r r tr)
(plus ts w (times k w))))
(lessp (plus r r tr)
(plus ts w w (times k w))))
(equal (warp (cons 'q rest)
(plus ts (times k w))
(plus r tr)
w r)
(cons 'q
(warp rest
(plus ts w (times k w))
(plus tr (times 2 r))
w r))))
((expand (warp (cons 'q rest)
(plus ts w (times w (sub1 k)))
(plus r tr)
w r)
(times 2 r))))
(prove-lemma helper7 (rewrite)
(implies (and (numberp ts)
(numberp tr)
(not (equal w 0))
(numberp w)
(not (equal r 0))
(numberp r)
(not (lessp tr ts))
(lessp tr (plus ts w))
(lessp w (times 2 r))
(lessp r (times 2 w))
(listp rest)
(listp (cdr rest))
(lessp (plus ts w) (plus r tr))
(not (lessp (plus r tr) (plus ts w w)))
(lessp (plus r tr) (plus ts w w w)))
(equal (warp (cons flg1 (cons 'q rest))
ts tr w r)
(cons 'q
(warp rest
(plus ts w w)
(plus r tr)
w r))))
((expand (warp (cons flg1 (cons 'q rest))
ts tr w r))))
(prove-lemma helper8 (rewrite)
(implies (and (numberp ts)
(numberp tr)
(not (equal w 0))
(numberp w)
(not (equal r 0))
(numberp r)
(not (lessp tr ts))
(lessp tr (plus ts w))
(lessp w (times 2 r))
(lessp r (times 2 w))
(listp rest)
(listp (cdr rest))
(lessp (plus ts w) (plus r tr))
(not (lessp (plus r tr) (plus ts w)))
(not (equal (plus r tr) (plus ts w)))
(not (lessp (plus r tr) (plus ts w w))))
(equal (warp (cons 'q rest) ts tr w r)
(cons 'q
(warp (cdr rest)
(plus ts w w)
(plus r tr)
w r))))
((expand (warp (cons 'q rest) ts tr w r)
(lst+ (cdr rest)
(plus ts w w)
(plus r tr)
w)
(nts+ (len (cdr rest))
(plus ts w w)
(plus r tr)
w)
(lst+ rest
(plus ts w)
(plus r tr)
w)
(nts+ (add1 (len (cdr rest)))
(plus ts w)
(plus r tr)
w))))
(prove-lemma helper9 (rewrite)
(implies (and (numberp ts)
(numberp tr)
(not (equal w 0))
(numberp w)
(not (equal r 0))
(numberp r)
(not (lessp tr ts))
(lessp tr (plus ts w))
(lessp w (plus r r))
(lessp r (times 2 w))
(listp rest)
(listp (cdr rest))
(lessp (plus ts w) (plus r tr))
(lessp (plus r tr) (plus ts w w))
(not (lessp (plus r r tr) (plus ts w w)))
(not (lessp (plus r r tr)
(plus ts w w w))))
(equal (warp (cons flg1 (cons 'q rest))
ts tr w r)
(cons 'q
(cons 'q
(warp (cdr rest)
(plus ts w w w)
(plus r r tr)
w r)))))
((expand (warp (cons flg1 (cons 'q rest))
ts tr w r))))
(prove-lemma helper10 (rewrite)
(implies (and (numberp ts)
(numberp tr)
(not (equal w 0))
(numberp w)
(not (equal r 0))
(numberp r)
(not (lessp tr ts))
(lessp tr (plus ts w))
(lessp w (plus r r))
(lessp r (times 2 w))
(listp rest)
(listp (cdr rest))
(lessp (plus ts w) (plus r tr))
(lessp (plus r tr) (plus ts w w))
(not (lessp (plus r r tr) (plus ts w w)))
(lessp (plus r r tr) (plus ts w w w)))
(equal (warp (cons flg1 (cons 'q rest))
ts tr w r)
(cons 'q
(cons 'q
(warp rest
(plus ts w w)
(plus r r tr)
w r)))))
((expand (warp (cons flg1 (cons 'q rest))
ts tr w r)
(warp (cons 'q rest)
(plus ts w)
(plus r tr)
w r))))
(prove-lemma helper11 (rewrite)
(implies (and (numberp ts)
(numberp tr)
(not (equal w 0))
(numberp w)
(not (equal r 0))
(numberp r)
(not (lessp tr ts))
(lessp tr (plus ts w))
(lessp w (plus r r))
(lessp r (times 2 w))
(listp rest)
(listp (cdr rest))
(lessp (plus ts w) (plus r tr))
(lessp (plus r tr) (plus ts w w))
(lessp (plus r r tr) (plus ts w w))
(lessp (plus r r tr) (plus ts w w w)))
(equal (warp (cons flg1 (cons 'q rest))
ts tr w r)
(cons 'q
(cons 'q
(cons 'q
(warp rest
(plus ts w w)
(plus tr (times 3 r))
w r))))))
((expand (warp (cons flg1 (cons 'q rest))
ts tr w r)
(warp (cons 'q rest)
(plus ts w)
(plus r r tr)
w r)
(warp (cons 'q rest)
(plus ts w)
(plus r tr)
w r)
(times 2 r)
(times 3 r))))
(prove-lemma lessp-times-18 (rewrite)
(implies (listp msg)
(not (lessp (times 18 (len msg)) 18))))
(prove-lemma listn-add1 (rewrite)
(equal (listn (add1 n) flg)
(cons flg (listn n flg)))
((enable listn)))
(prove-lemma helper14 (rewrite)
(IMPLIES (AND (NUMBERP TS)
(NUMBERP TR)
(NOT (EQUAL W 0))
(NUMBERP W)
(NOT (EQUAL R 0))
(NUMBERP R)
(NOT (LESSP TR TS))
(LESSP TR (PLUS TS W))
(LESSP W (PLUS R R))
(LESSP R (TIMES 2 W))
(LISTP REST)
(LISTP (CDR REST))
(NOT (LESSP (PLUS R TR) (PLUS TS W)))
(LESSP (PLUS R TR) (PLUS TS W W)))
(EQUAL (WARP (CONS 'Q REST) TS TR W R)
(CONS 'Q
(WARP REST
(PLUS TS W)
(PLUS R TR)
W R))))
((expand (WARP (CONS 'Q REST) TS TR W R))))
(prove-lemma helper15 (rewrite)
(IMPLIES (AND (NUMBERP TS)
(NUMBERP TR)
(NOT (EQUAL W 0))
(NUMBERP W)
(NOT (EQUAL R 0))
(NUMBERP R)
(NOT (LESSP TR TS))
(LESSP TR (PLUS TS W))
(LESSP W (PLUS R R))
(LESSP R (TIMES 2 W))
(LISTP REST)
(LISTP (CDR REST))
(LESSP (PLUS R TR) (PLUS TS W))
(NOT (LESSP (PLUS R R TR) (PLUS TS W)))
(LESSP (PLUS R R TR) (PLUS TS W W)))
(EQUAL (WARP (CONS 'Q REST) TS TR W R)
(CONS 'Q
(CONS 'Q
(WARP REST
(PLUS TS W)
(PLUS R R TR)
W R)))))
((expand (WARP (CONS 'Q REST) TS TR W R))))
(prove-lemma warp-app-across-gap (rewrite)
(implies (and (numberp ts)
(numberp tr)
(numberp k)
(not (zerop w))
(not (zerop r))
(not (lessp tr ts))
(lessp tr (plus ts w))
(lessp w (times 2 r))
(lessp r (times 2 w))
(listp rest)
(listp (cdr rest))
(nendp k ts (plus r tr) w))
(equal (warp (app (listn k flg1)
(cons 'q rest))
ts tr w r)
(app (listn (nqg k ts tr w r) 'q)
(warp (cdrn (dwg k ts tr w r) rest)
(tsg k ts tr w r)
(trg k ts tr w r)
w r))))
((do-not-induct t)
(enable listn)
(expand (nendp k ts (plus r tr) w)
(nendp (sub1 k)
(plus ts w)
(plus r tr)
w)
(nendp (sub1 (sub1 k))
(plus ts w w)
(plus r tr)
w)
(times 2 r))))
(disable helper1)
(disable helper5)
(disable helper7)
(disable helper8)
(disable helper9)
(disable helper10)
(disable helper11)
(disable helper14)
(disable helper15)
(disable nqg)
(disable dwg)
(disable tsg)
(disable trg)
(defn nq (n ts tr w r)
(nqg (nlst* n ts tr w r)
(nts* n ts tr w r)
(ntr* n ts tr w r)
w r))
(defn dw (n ts tr w r)
(dwg (nlst* n ts tr w r)
(nts* n ts tr w r)
(ntr* n ts tr w r)
w r))
(defn ts (n ts tr w r)
(tsg (nlst* n ts tr w r)
(nts* n ts tr w r)
(ntr* n ts tr w r)
w r))
(defn tr (n ts tr w r)
(trg (nlst* n ts tr w r)
(nts* n ts tr w r)
(ntr* n ts tr w r)
w r))
(prove-lemma lessp-2-len-implies-listps nil
(implies (lessp 2 (len x))
(and (listp x) (listp (cdr x)))))
(prove-lemma warp-app-listn-q1 nil
(implies (and (numberp ts)
(numberp tr)
(not (zerop w))
(not (zerop r))
(not (lessp tr ts))
(lessp tr (plus ts w))
(lessp w (times 2 r))
(lessp r (times 2 w))
(numberp n1)
(lessp 2 (len rest)))
(equal (target (warp (app (listn n1 flg1) (cons 'q rest))
ts tr w r))
(app (listn (n* n1 ts tr w r) flg1)
(app (listn (nq n1 ts tr w r) 'q)
(warp (cdrn (dw n1 ts tr w r) rest)
(ts n1 ts tr w r)
(tr n1 ts tr w r)
w r)))))
((use (lessp-2-len-implies-listps (x rest)))
(disable warp-app-gap)))
(prove-lemma warp-app-listn-q (rewrite)
(implies (and (numberp ts)
(numberp tr)
(not (zerop w))
(not (zerop r))
(not (lessp tr ts))
(lessp tr (plus ts w))
(lessp w (times 2 r))
(lessp r (times 2 w))
(numberp n1)
(lessp 2 (len rest)))
(equal (warp (app (listn n1 flg1) (cons 'q rest))
ts tr w r)
(app (listn (n* n1 ts tr w r) flg1)
(app (listn (nq n1 ts tr w r) 'q)
(warp (cdrn (dw n1 ts tr w r) rest)
(ts n1 ts tr w r)
(tr n1 ts tr w r)
w r)))))
((use (warp-app-listn-q1))
(enable target)))
(disable listn-add1)
(disable WARP-APP-ACROSS-GAP)
(disable WARP-APP-GAP)
(disable WARP-LISTN)
(disable warp-app)
; Now there are two applications we must think about: the proof of top and
; the proof of loop. We will deal with top first. To explore I want to
; do the smoothing and det part of top now and then come back to warp.
; Now we do the smoothing.
(prove-lemma smooth-congruence (rewrite)
(implies (not (b-xor flg1 flg2))
(equal (equal (smooth flg2 rest)
(smooth flg1 rest))
t))
((enable b-xor smooth)))
(prove-lemma smooth-flg-app-listn-flg (rewrite)
(implies (not (b-xor flg1 flg2))
(equal (smooth flg1 (app (listn p1 flg2) rest))
(app (listn p1 flg2) (smooth flg1 rest))))
((induct (listn p1 flg2))
(enable smooth listn)))
(prove-lemma listp-app-listn (rewrite)
(equal (listp (app (listn n flg) rest))
(or (not (zerop n))
(listp rest)))
((enable listn)))
(prove-lemma listp-cells (rewrite)
(equal (listp (cells flg 5 13 msg)) (listp msg))
((enable cells cell)))
(disable listp-app-listn)
(prove-lemma car-app (rewrite)
(equal (car (app a b))
(if (listp a) (car a) (car b))))
(prove-lemma listp-listn (rewrite)
(equal (listp (listn n flg))
(not (zerop n)))
((enable listn)))
(prove-lemma car-cells (rewrite)
(implies (listp msg)
(equal (car (cells flg 5 13 msg))
(b-not flg)))
((expand (cells flg 5 13 msg)
(listn 5 (b-not flg)))
(enable cell listn)))
(disable car-app)
(prove-lemma top-smooth-step (rewrite)
(implies (listp msg)
(equal (smooth t (app (listn p1 t) (app (cells t 5 13 msg) (listn p2 t))))
(app (listn p1 t)
(cons 'q (smooth f (app (cdr (cells t 5 13 msg))
(listn p2 t)))))))
((enable cells smooth)))
(disable smooth-flg-app-listn-flg)
(disable car-cells)
(disable listp-cells)
; Now past the det
(defn oracle* (lst oracle)
(if (nlistp lst)
oracle
(if (equal (car lst) 'q)
(oracle* (cdr lst) (cdr oracle))
(oracle* (cdr lst) oracle))))
(disable oracle*)
(prove-lemma det-app (rewrite)
(equal (det (app lst1 lst2) oracle)
(app (det lst1 oracle)
(det lst2 (oracle* lst1 oracle))))
((enable det oracle*)))
(prove-lemma det-listn (rewrite)
(implies (not (equal flg 'q))
(equal (det (listn n flg) oracle)
(listn n flg)))
((enable det listn)))
(prove-lemma oracle*-listn (rewrite)
(implies (not (equal flg 'q))
(equal (oracle* (listn n flg) oracle)
oracle))
((enable oracle* listn)))
; So now we combine all these.
(prove-lemma len-smooth (rewrite)
(equal (len (smooth flg lst)) (len lst))
((enable smooth)))
(prove-lemma cdr-app (rewrite)
(equal (cdr (app a b))
(if (listp a) (app (cdr a) b) (cdr b))))
(prove-lemma top-async-send-lemma1 (rewrite)
(implies (listp msg)
(LESSP 2 (len (cdr (cells t 5 13 msg)))))
((expand (cells t 5 13 msg))
(enable cell)))
(disable cdr-app)
(prove-lemma top-async-send (rewrite)
(implies (and (bvp msg)
(listp msg)
(numberp ts)
(numberp tr)
(not (zerop w))
(not (zerop r))
(not (lessp tr ts))
(lessp tr (plus ts w))
(rate-proximity w r)
(numberp p1))
(equal (async (send msg p1 5 13 p2) ts tr w r oracle)
(app (listn (n* p1 ts tr w r) t)
(app (det (listn (nqg (nlst* p1 ts tr w r)
(nts* p1 ts tr w r)
(ntr* p1 ts tr w r)
w r)
'q)
oracle)
(det (warp (cdrn (dwg (nlst* p1 ts tr w r)
(nts* p1 ts tr w r)
(ntr* p1 ts tr w r)
w r)
(smooth f
(app (cdr (cells t 5 13 msg))
(listn p2 t))))
(tsg (nlst* p1 ts tr w r)
(nts* p1 ts tr w r)
(ntr* p1 ts tr w r)
w r)
(trg (nlst* p1 ts tr w r)
(nts* p1 ts tr w r)
(ntr* p1 ts tr w r)
w r)
w r)
(oracle* (listn (nqg (nlst* p1 ts tr w r)
(nts* p1 ts tr w r)
(ntr* p1 ts tr w r)
w r)
'q)
oracle))))))
((disable app)
(enable async send)))
(disable top-async-send-lemma1)
(disable top-smooth-step)
; Now we get recv to eat the header.
(prove-lemma scan-app-listn (rewrite)
(equal (scan flg (app (listn n flg) rest))
(scan flg rest))
((enable scan listn)))
(prove-lemma top-recv-step (rewrite)
(equal (recv n t k (app (listn p1 t) rest))
(recv n t k rest))
((enable recv)))
#| At this point our top level goal looks like this
(equal (recv (len msg)
t 10
(app (det (listn (nqg (nlst* p1 ts tr w r)
(nts* p1 ts tr w r)
(ntr* p1 ts tr w r)
w r)
'q)
oracle)
(det (warp (cdrn (dwg (nlst* p1 ts tr w r)
(nts* p1 ts tr w r)
(ntr* p1 ts tr w r)
w r)
(smooth f
(app (cdr (cells t 5 13 msg))
(listn p2 t))))
(tsg (nlst* p1 ts tr w r)
(nts* p1 ts tr w r)
(ntr* p1 ts tr w r)
w r)
(trg (nlst* p1 ts tr w r)
(nts* p1 ts tr w r)
(ntr* p1 ts tr w r)
w r)
w r)
(oracle* (listn (nqg (nlst* p1 ts tr w r)
(nts* p1 ts tr w r)
(ntr* p1 ts tr w r)
w r)
'q)
oracle))))
msg)
and we will generalize it to
(equal (recv (len msg)
t 10
(app (det (listn nq 'q) oracle1)
(det (warp (cdrn dw
(smooth f
(app (cdr (cells t 5 13 msg))
(listn p2 t))))
ts tr w r)
oracle2)))
msg)
where we have the usual bounds on nq, dw, ts and tr.
To justify this generalization we must prove the theorems that the
expressions generalized satisfy the usual bounds. We do that now.
|#
(prove-lemma nqg-bounds (rewrite)
(and (lessp 0 (nqg n ts tr w r))
(not (lessp 3 (nqg n ts tr w r))))
((enable nqg)))
(prove-lemma dwg-bounds (rewrite)
(not (lessp 1 (dwg n ts tr w r)))
((enable dwg)))
; Typically trg and tsg will be instantiated as below. We package up
; the required backchaining here. It is my impression that the
; generalized form in which the * terms do not appear is not a
; theorem. The proof of this relies upon
; NOT-LESSP-PLUS-R-NTR*-PLUS-NTS*-TIMES-W-NLST*.
(prove-lemma not-lessp-trg*-tsg* (rewrite)
(implies (and (numberp ts)
(numberp tr)
(numberp n)
(not (zerop w))
(not (zerop r))
(not (lessp tr ts))
(lessp tr (plus ts w))
(lessp w (times 2 r))
(lessp r (times 2 w)))
(not (lessp (trg (nlst* n ts tr w r)
(nts* n ts tr w r)
(ntr* n ts tr w r)
w r)
(tsg (nlst* n ts tr w r)
(nts* n ts tr w r)
(ntr* n ts tr w r)
w r))))
((enable trg tsg nqg dwg)))
(prove-lemma lessp-trg*-plus-w-tsg* (rewrite)
(implies (and (numberp ts)
(numberp tr)
(numberp n)
(not (zerop w))
(not (zerop r))
(not (lessp tr ts))
(lessp tr (plus ts w))
(lessp w (times 2 r))
(lessp r (times 2 w)))
(lessp (trg (nlst* n ts tr w r)
(nts* n ts tr w r)
(ntr* n ts tr w r)
w r)
(plus w (tsg (nlst* n ts tr w r)
(nts* n ts tr w r)
(ntr* n ts tr w r)
w r))))
((enable trg tsg nqg dwg)))
#|
Consider the lhs of the concl of loop:
(recv (len msg)
flg1
10
(app (det (listn nq 'q) oracle1)
(det (warp (cdrn dw
(smooth flg2
(app (cdr (cells flg1 5 13 msg))
(listn p2 t))))
ts tr w r)
oracle2)))
We will derive a killer rewrite rule that expands this, under the
conditions governing our induction, into (cons (car msg) ...) where
... is an instance of the lhs above. I.e., the rule will step the
lhs of the ind concl into the induction hypothesis. The derivation of
this rule will be documented by showing the successive steps. The
actual discovery of the form of the lhs above and the steps was
made by proving the "killer rule" over and over again, each time
making some transformation.
The first step is to open (cells flg1 5 13 msg), drive the cdr around
the first cell and absorb it into the cell size, and associate the apps,
|#
(prove-lemma cdr-app-cell-cells (rewrite)
(implies (not (zerop n1))
(equal (cdr (app (cell flg1 n1 n2 bit) (cells flg2 n1 n2 msg)))
(app (cell flg1 (sub1 n1) n2 bit) (cells flg2 n1 n2 msg))))
((enable cdr-app cell listn)))
#|
So lhs becomes:
(recv (len msg)
flg1
10
(app (det (listn nq 'q) oracle1)
(det (warp (cdrn dw
(smooth flg2
(app (cell flg1 4 13 (car msg))
(app (cells (csig flg1 (car msg)) 5 13 (cdr msg))
(listn p2 t)))))
ts tr w r)
oracle2)))
Our next goal is to drive the smooth through the app.
|#
(prove-lemma smooth-flg-listn-flg (rewrite)
(implies (not (b-xor flg1 flg2))
(equal (smooth flg1 (listn n flg2)) (listn n flg2)))
((enable smooth listn)))
(prove-lemma not-b-xor-b-not (rewrite)
(implies (b-xor flg1 flg2)
(and (not (b-xor flg1 (b-not flg2)))
(not (b-xor (b-not flg2) flg1))))
((enable b-xor b-not)))
(prove-lemma smooth-flg-app-listn-not-flg (rewrite)
(implies (and (not (zerop n))
(b-xor flg1 flg2))
(equal (smooth flg1 (app (listn n flg2) rest))
(app (smooth flg1 (listn n flg2))
(smooth flg2 rest))))
((induct (listn n flg2))
(enable smooth listn)))
(prove-lemma smooth-app-cell-app-cells (rewrite)
(implies (and (not (zerop n1))
(b-xor flg1 flg2))
(equal (smooth flg1
(app (cell flg2 m1 n1 bit)
(app (cells (csig flg2 bit) m n msg)
(listn p2 t))))
(app (smooth flg1 (cell flg2 m1 n1 bit))
(smooth (csig flg2 bit)
(app (cells (csig flg2 bit) m n msg)
(listn p2 t))))))
((enable smooth listn cell csig smooth-flg-app-listn-flg)))
(disable smooth-flg-listn-flg)
(disable smooth-flg-app-listn-not-flg)
; If we had loop-stoppers on iff rules we could use an iff and be more efficient.
(prove-lemma b-xor-commutes (rewrite)
(implies (b-xor x y) (b-xor y x))
((enable b-xor)))
#|
So lhs is now:
(recv (len msg)
flg1
10
(app (det (listn nq 'q) oracle1)
(det (warp (cdrn dw
(app (smooth flg2 (cell flg1 4 13 (car msg)))
(smooth (csig flg1 (car msg))
(app (cells (csig flg1 (car msg)) 5 13 (cdr msg))
(listn p2 t)))))
ts tr w r)
oracle2)))
Now drive the cdrn into the app and the smooth and absorb it in the
cell size.
|#
(prove-lemma listp-smooth-cell (rewrite)
(implies (not (zerop m))
(listp (smooth flg1 (cell flg2 m n bit))))
((enable cell smooth)
(expand (listn m (b-not flg2)))))
(prove-lemma cdrn-dw-app-smooth-cell (rewrite)
(implies (and (not (zerop m))
(numberp dw)
(not (lessp 1 dw)))
(equal (cdrn dw (app (smooth flg1 (cell flg2 m n bit)) rest))
(app (cdrn dw (smooth flg1 (cell flg2 m n bit)))
rest)))
((enable cdr-app)
(expand (cdrn dw (app (smooth flg1 (cell flg2 m n bit)) rest))
(cdrn 1 (smooth flg1 (cell flg2 m n bit))))))
(prove-lemma car-listn (rewrite)
(equal (car (listn n flg)) (if (zerop n) 0 flg))
((enable listn)))
(prove-lemma cdrn-dw-smooth-cell (rewrite)
(implies (and (not (zerop m))
(numberp dw)
(not (lessp 1 dw))
(b-xor flg1 flg2))
(equal (cdrn dw (smooth flg2 (cell flg1 m n (car msg))))
(smooth flg2 (cell flg1 (difference m dw) n (car msg)))))
((enable cdr-app cell listn-add1 smooth)
(expand (listn m (b-not flg1))
(cdrn dw
(cons (b-not flg1)
(smooth (b-not flg1)
(app (listn (sub1 m) (b-not flg1))
(listn n (csig flg1 (car msg)))))))
(plus 1 x))
(do-not-induct t)))
(disable car-listn)
#|
So lhs is
(recv (len msg)
flg1
10
(app (det (listn nq 'q) oracle1)
(det (warp (app (smooth flg2 (cell flg1 (difference 4 dw) 13 (car msg)))
(smooth (csig flg1 (car msg))
(app (cells (csig flg1 (car msg)) 5 13 (cdr msg))
(listn p2 t))))
ts tr w r)
oracle2)))
Next we drive the warp through the app. We do that by putting a TARGET around
the warp and enabling warp-app. To simplify the resulting len expressions we
use:
|#
(prove-lemma len-cell (rewrite)
(equal (len (cell flg m n bit))
(plus m n))
((enable cell)))
(prove-lemma add1-plus-12-difference-4-dw (rewrite)
(implies (not (lessp 1 dw))
(equal (ADD1 (PLUS 12 (DIFFERENCE 4 DW)))
(difference 17 dw))))
#|
Det-app also applies to drive the det through the app.
So now lhs is
(recv
(len msg)
flg1 10
(app (det (listn nq 'q) oracle1)
(app (det (warp (smooth flg2
(cell flg1
(difference 4 dw)
13
(car msg)))
ts tr w r)
oracle2)
(det (warp (app (lst* (smooth flg2
(cell flg1
(difference 4 dw)
13
(car msg)))
ts tr w r)
(smooth (csig flg1 (car msg))
(app (cells (csig flg1 (car msg)) 5
13
(cdr msg))
(listn p2 t))))
(nts* (difference 17 dw) ts tr w r)
(ntr* (difference 17 dw) ts tr w r)
w r)
(oracle* (app (lst* (smooth flg2
(cell flg1
(difference 4 dw)
13
(car msg)))
ts tr w r)
(smooth (csig flg1 (car msg))
(app (cells (csig flg1 (car msg)) 5
13
(cdr msg))
(listn p2 t))))
oracle2)))))
Consider the second warp expression, the one applied to (app (lst* ...)...).
We want to apply warp-app-listn-q to this, which expects
(app (listn n1 flg1) (cons 'q rest))
So now we focus on causing that to happen. The lst* produces a listn.
Our induction will make a base case out of the one-bit msg. So we know
the current cell is followed by another and hence by an edge.
So our 'q comes from there.
We have this induction in mind but we don't yet know the ... parts. The
variables are listed in order of appearance.
(defn loop-ind-hint (nq oracle1 dw flg2 flg1 msg ts tr w r oracle2)
(cond ((nlistp msg) t)
((nlistp (cdr msg)) t)
(t (loop-ind-hint ... (cdr msg) ...))))
|#
; "The lst* produces a listn."
(prove-lemma lst*-is-lastn-nlst* (rewrite)
(equal (lst* lst ts tr w r)
(lastn (nlst* (len lst) ts tr w r) lst))
((use (lst*-is-lastn))))
(prove-lemma lastn-app (rewrite)
(implies (not (lessp (len b) n))
(equal (lastn n (app a b))
(lastn n b))))
(prove-lemma not-lessp-2-nlst* (rewrite)
(implies (and (numberp ts)
(numberp tr)
(not (zerop w))
(not (zerop r))
(not (lessp tr ts))
(lessp tr (plus ts w))
(lessp w (times 2 r))
(lessp r (times 2 w)))
(not (lessp 2 (nlst* n ts tr w r)))))
(prove-lemma smooth-flg-listn-not-flg (rewrite)
(implies (and (not (zerop n))
(b-xor flg1 flg2))
(equal (smooth flg1 (listn n flg2))
(cons 'q (listn (sub1 n) flg2))))
((enable smooth listn)))
(disable smooth-flg-listn-not-flg)
(prove-lemma lst*-smooth-cell (rewrite)
(implies (and (numberp ts)
(numberp tr)
(not (zerop w))
(not (zerop r))
(not (lessp tr ts))
(lessp tr (plus ts w))
(lessp w (times 2 r))
(lessp r (times 2 w))
(not (zerop m))
(numberp n)
(lessp 2 n)
(b-xor flg1 flg2))
(equal (lst* (smooth flg2 (cell flg1 m n bit)) ts tr w r)
(listn (nlst* (plus m n) ts tr w r)
(csig flg1 bit))))
((enable csig cell smooth-flg-app-listn-flg smooth-flg-app-listn-not-flg
smooth-flg-listn-flg smooth-flg-listn-not-flg)))
(disable lst*-is-lastn-nlst*)
#|
So lhs is
(recv
(len msg)
flg1 10
(app (det (listn nq 'q) oracle1)
(app (det (warp (smooth flg2
(cell flg1
(difference 4 dw)
13
(car msg)))
ts tr w r)
oracle2)
(det (warp (app (listn (nlst* (difference 17 dw) ts tr w r)
(csig flg1 (car msg)))
(smooth (csig flg1 (car msg))
(app (cells (csig flg1 (car msg)) 5
13
(cdr msg))
(listn p2 t))))
(nts* (difference 17 dw) ts tr w r)
(ntr* (difference 17 dw) ts tr w r)
w r)
(oracle* (warp (smooth flg2
(cell flg1
(difference 4 dw)
13
(car msg)))
ts tr w r)
oracle2)))))
And we're going to milk a 'q out of the smoothing of the cells term.
|#
; "So our 'q comes from there."
(prove-lemma cdr-listn (rewrite)
(equal (cdr (listn n flg))
(if (zerop n) 0 (listn (sub1 n) flg)))
((expand (listn n flg))))
(disable cdr-listn)
(prove-lemma smooth-app-cells (rewrite)
(implies (and (listp msg)
(not (zerop m)))
(equal (smooth flg
(app (cells flg m n msg)
(listn p2 t)))
(cons 'q (smooth (b-not flg)
(app (cdr (cells flg m n msg))
(listn p2 t))))))
((expand (cells flg m n msg))
(enable cell smooth-flg-app-listn-not-flg smooth-flg-listn-not-flg cdr-app
cdr-listn smooth-flg-app-listn-flg)))
#|
So lhs is
(recv
(len msg)
flg1 10
(app (det (listn nq 'q) oracle1)
(app (det (warp (smooth flg2
(cell flg1
(difference 4 dw)
13
(car msg)))
ts tr w r)
oracle2)
(det (warp (app (listn (nlst* (difference 17 dw) ts tr w r)
(csig flg1 (car msg)))
(cons 'q
(smooth (b-not (csig flg1 (car msg)))
(app (cdr (cells (csig flg1 (car msg)) 5
13
(cdr msg)))
(listn p2 t)))))
(nts* (difference 17 dw) ts tr w r)
(ntr* (difference 17 dw) ts tr w r)
w r)
(oracle* (warp (smooth flg2
(cell flg1
(difference 4 dw)
13
(car msg)))
ts tr w r)
oracle2)))))
Observe that warp-app-listn-q is now applicable if we can relieve the hypotheses.
The only nonobvious one is relieved by:
|#
(prove-lemma lessp-2-len-cdr-cells (rewrite)
(implies (listp msg)
(lessp 2 (len (cdr (cells flg 5 13 msg)))))
((expand (cells flg 5 13 msg))))
; So warp-app-listn-q will push the warp through the two apps and let
; det-app push the det through. Note that while warp-app-listn-q normally
; kicks out some t's or f's before the 'qs the initial string here is
; empty because we're starting with only nlst* of them. Of course, we
; have to know
(prove-lemma app-listn-0 (rewrite)
(equal (app (listn 0 flg) rest) rest)
((enable listn)))
; We include the app because in the proof of our killer rule, app will be
; disabled.
; We are now ready to solidfy our gains as the first step of our killer
; rule. We use the name loop-killer-1a because it has a TARGET on our
; warp. Loop-killer-1, next, doesn't.
(prove-lemma loop-killer-1a nil
(implies (and (bvp msg)
(listp msg)
(listp (cdr msg))
(numberp ts)
(numberp tr)
(not (zerop w))
(not (zerop r))
(not (lessp tr ts))
(lessp tr (plus ts w))
(rate-proximity w r)
(numberp nq)
(not (lessp 3 nq))
(numberp dw)
(not (lessp 1 dw))
(b-xor flg1 flg2))
(equal (recv (len msg)
flg1
10
(app (det (listn nq 'q) oracle1)
(det (target (warp (cdrn dw
(smooth flg2
(app (cdr (cells flg1 5 13 msg))
(listn p2 t))))
ts tr w r))
oracle2)))
(recv
(len msg)
flg1 10
(app (det (listn nq 'q) oracle1)
(app (det (warp (smooth flg2
(cell flg1
(difference 4 dw)
13
(car msg)))
ts tr w r)
oracle2)
(app (det (listn (nqg (nlst* (difference 17 dw) ts tr w r)
(nts* (difference 17 dw) ts tr w r)
(ntr* (difference 17 dw) ts tr w r)
w r)
'q)
(oracle* (warp (smooth flg2
(cell flg1
(difference 4 dw)
13
(car msg)))
ts tr w r)
oracle2))
(det (warp (cdrn (dwg (nlst* (difference 17 dw) ts tr w r)
(nts* (difference 17 dw) ts tr w r)
(ntr* (difference 17 dw) ts tr w r)
w r)
(smooth (b-not (csig flg1 (car msg)))
(app (cdr (cells (csig flg1 (car msg)) 5
13
(cdr msg)))
(listn p2 t))))
(tsg (nlst* (difference 17 dw) ts tr w r)
(nts* (difference 17 dw) ts tr w r)
(ntr* (difference 17 dw) ts tr w r)
w r)
(trg (nlst* (difference 17 dw) ts tr w r)
(nts* (difference 17 dw) ts tr w r)
(ntr* (difference 17 dw) ts tr w r)
w r)
w r)
(oracle* (listn (nqg (nlst* (difference 17 dw) ts tr w r)
(nts* (difference 17 dw) ts tr w r)
(ntr* (difference 17 dw) ts tr w r)
w r)
'q)
(oracle* (warp (smooth flg2
(cell flg1
(difference 4 dw)
13
(car msg)))
ts tr w r)
oracle2)))))))))
((disable len app cells)
(enable warp-app)
(expand (cells flg1 5 13 msg))))
(disable CDR-APP-CELL-CELLS)
(disable SMOOTH-APP-CELLS)
(disable smooth-app-cell-app-cells) ; used to be loop-smooth-step
(disable CDRN-DW-SMOOTH-CELL)
(disable CDRN-DW-APP-SMOOTH-CELL)
(disable LST*-SMOOTH-CELL)
(prove-lemma loop-killer-1 (rewrite)
(implies (and (bvp msg)
(listp msg)
(listp (cdr msg))
(numberp ts)
(numberp tr)
(not (zerop w))
(not (zerop r))
(not (lessp tr ts))
(lessp tr (plus ts w))
(rate-proximity w r)
(numberp nq)
(not (lessp 3 nq))
(numberp dw)
(not (lessp 1 dw))
(b-xor flg1 flg2))
(equal (recv (len msg)
flg1
10
(app (det (listn nq 'q) oracle1)
(det (warp (cdrn dw
(smooth flg2
(app (cdr (cells flg1 5 13 msg))
(listn p2 t))))
ts tr w r)
oracle2)))
(recv
(len msg)
flg1 10
(app (det (listn nq 'q) oracle1)
(app (det (warp (smooth flg2
(cell flg1
(difference 4 dw)
13
(car msg)))
ts tr w r)
oracle2)
(app (det (listn (nqg (nlst* (difference 17 dw) ts tr w r)
(nts* (difference 17 dw) ts tr w r)
(ntr* (difference 17 dw) ts tr w r)
w r)
'q)
(oracle* (warp (smooth flg2
(cell flg1
(difference 4 dw)
13
(car msg)))
ts tr w r)
oracle2))
(det (warp (cdrn (dwg (nlst* (difference 17 dw) ts tr w r)
(nts* (difference 17 dw) ts tr w r)
(ntr* (difference 17 dw) ts tr w r)
w r)
(smooth (b-not (csig flg1 (car msg)))
(app (cdr (cells (csig flg1 (car msg)) 5
13
(cdr msg)))
(listn p2 t))))
(tsg (nlst* (difference 17 dw) ts tr w r)
(nts* (difference 17 dw) ts tr w r)
(ntr* (difference 17 dw) ts tr w r)
w r)
(trg (nlst* (difference 17 dw) ts tr w r)
(nts* (difference 17 dw) ts tr w r)
(ntr* (difference 17 dw) ts tr w r)
w r)
w r)
(oracle* (listn (nqg (nlst* (difference 17 dw) ts tr w r)
(nts* (difference 17 dw) ts tr w r)
(ntr* (difference 17 dw) ts tr w r)
w r)
'q)
(oracle* (warp (smooth flg2
(cell flg1
(difference 4 dw)
13
(car msg)))
ts tr w r)
oracle2)))))))))
((enable target)
(use (loop-killer-1a))))
#|
Observe in the rhs of loop-killer-1 the emergence of an instance of the
critical part of the lhs:
(app (det (listn nq 'q)
oracle1)
(det (warp (cdrn dw
(smooth flg2
(app (cdr (cells flg1 5 13 msg))
(listn p2 t))))
ts tr w r)
oracle2))
From this instance we can read off our induction hypothesis:
|#
(defn loop-ind-hint (nq oracle1 dw flg2 flg1 msg ts tr w r oracle2)
(if (nlistp msg)
t
(if (nlistp (cdr msg))
t
(loop-ind-hint (nqg (nlst* (difference 17 dw) ts tr w r)
(nts* (difference 17 dw) ts tr w r)
(ntr* (difference 17 dw) ts tr w r)
w r)
(oracle* (warp (smooth flg2
(cell flg1
(difference 4 dw)
13
(car msg)))
ts tr w r)
oracle2)
(dwg (nlst* (difference 17 dw) ts tr w r)
(nts* (difference 17 dw) ts tr w r)
(ntr* (difference 17 dw) ts tr w r)
w r)
(b-not (csig flg1 (car msg)))
(csig flg1 (car msg))
(cdr msg)
(tsg (nlst* (difference 17 dw) ts tr w r)
(nts* (difference 17 dw) ts tr w r)
(ntr* (difference 17 dw) ts tr w r)
w r)
(trg (nlst* (difference 17 dw) ts tr w r)
(nts* (difference 17 dw) ts tr w r)
(ntr* (difference 17 dw) ts tr w r)
w r)
w r
(oracle* (listn (nqg (nlst* (difference 17 dw) ts tr w r)
(nts* (difference 17 dw) ts tr w r)
(ntr* (difference 17 dw) ts tr w r)
w r)
'q)
(oracle* (warp (smooth flg2
(cell flg1
(difference 4 dw)
13
(car msg)))
ts tr w r)
oracle2))))))
#|
In order for this induction to work out, we have to be able to establish that
the instantiations satisfy the hypotheses of the theorem being proved. We
have made sure of this through the previously proved lemmas NQG-BOUNDS,
DWG-BOUNDS, NOT-LESSP-TRG*-TSG* and LESSP-TRG*-PLUS-W-TSG*.
Loop-killer-1 does not get us back to the induction hypothesis because
we have to scan past the first cell. So we now continue with our loop
killer development. We aim for the following rewrite (under appropriate
hyps):
(equal (recv (len msg) flg1 10
(app (det (listn nq 'q) oracle1)
(app (det (warp (smooth flg2 (cell flg1 (difference 4 dw) 13 bit))
ts tr w r)
oracle)
rest)))
(cons bit
(recv (len (cdr msg))
(csig flg1 bit)
10
rest)))
This will be the conclusion of loop-killer-2. Observe that killer-2 takes up
where killer-1 left off and, in conjunction with the induction hyp, will
reduce the lhs of the induction concl to (cons (car msg) (cdr msg)).
We resume our step-by-step development by considering the lhs recv above and
successively transforming it.
By opening up the lhs recv above we end up with two hard requirements.
The first is that recv reads the correct bit. We'll call this
loop-killer-2a:
(recv-bit 10
(scan flg1
(app (det (listn nq 'q) oracle1)
(app (det (warp (smooth flg2
(cell flg1
(difference 4 dw)
13
(car msg)))
ts tr w r)
oracle)
rest))))
= (car msg)
The second is that it resumes it scan on a string of bits of the
correct parity.
Loop-killer-2b:
(cdrn 10
(scan flg1
(app (det (listn nq 'q) oracle1)
(app (det (warp (smooth flg2
(cell flg1 (difference 4 dw) 13 (car msg))
ts tr w r)
oracle)
rest)))))
= (app (listn ??? (csig flg1 x)) rest)
where ??? is some non-zero number we'll determine during the proof below.
It is loop-killer-2b that gets us back to our induction hyp and
so we will work on it first. As usual the game is to move the app from
its hiding place in cell through smooth, warp, and det and then do some
arithmetic.
Because it is crucial to all that we do henceforth, we are going to
first show what (warp (smooth flg2 (cell flg1 m n bit)) ts tr w r)
looks like.
|#
(prove-lemma app-listn-flg-listn-flg (rewrite)
(equal (app (listn m flg) (listn n flg))
(listn (plus m n) flg))
((enable listn)))
(prove-lemma cdrn-listn (rewrite)
(implies (not (lessp n dw))
(equal (cdrn dw (listn n flg))
(listn (difference n dw) flg)))
((enable listn)))
; The requirement on n below stems from (a) smooth-flg-listn-flg, as it
; smooths the second subcell, needs to know that n is at least 1 so that it
; can take a 'q out; (b) warp-app-listn-q as it is warping that subcell
; needs to know that n-1 is greater than 2 so it can eat at most two
; signals after the q.
(prove-lemma warp-smooth-cell (rewrite)
(implies (and (boolp bit)
(numberp ts)
(numberp tr)
(not (zerop w))
(not (zerop r))
(not (lessp tr ts))
(lessp tr (plus ts w))
(rate-proximity w r)
(numberp m)
(numberp n)
(lessp 3 n)
(b-xor flg1 flg2))
(equal (warp (smooth flg2 (cell flg1 m n bit))
ts tr w r)
(if bit
(APP (LISTN (N* M TS TR W R) (B-NOT FLG1))
(APP (LISTN (NQG (NLST* M TS TR W R)
(NTS* M TS TR W R)
(NTR* M TS TR W R)
W R)
'Q)
(LISTN (N* (DIFFERENCE (SUB1 N)
(DWG (NLST* M TS TR W R)
(NTS* M TS TR W R)
(NTR* M TS TR W R)
W R))
(TSG (NLST* M TS TR W R)
(NTS* M TS TR W R)
(NTR* M TS TR W R)
W R)
(TRG (NLST* M TS TR W R)
(NTS* M TS TR W R)
(NTR* M TS TR W R)
W R)
W R)
FLG1)))
(listn (n* (plus m n) ts tr w r) (b-not flg1)))))
((do-not-induct t)
(enable cell csig smooth-flg-app-listn-flg smooth-flg-app-listn-not-flg
smooth-flg-listn-flg smooth-flg-listn-not-flg warp-listn)))
; To cdrn through the rhs above we need bounds on n*. To prove the
; bounds we will have to characterize n* algebraically. The bounds
; theorems are too weak to prove inductively.
(prove-lemma nendp-alg (rewrite)
(implies (and (numberp ts)
(numberp tr+)
(not (zerop w))
(lessp ts tr+))
(equal (nendp n ts tr+ w)
(lessp (plus ts (times n w)) tr+))))
(prove-lemma nlst+-ts-plus-ts-w (rewrite)
(implies (and (numberp n)
(not (zerop w)))
(equal (nlst+ n ts (plus ts w) w)
(sub1 n)))
((expand (nlst+ n ts (plus ts w) w)
(nlst+ (sub1 n)
(plus ts w)
(plus ts w)
w))))
(prove-lemma nlst+-alg (rewrite)
(implies (and (numberp n)
(numberp ts)
(numberp tr+)
(not (zerop w))
(lessp ts tr+))
(equal (nlst+ n ts tr+ w)
(difference n (quotient (difference tr+ ts) w)))))
(disable nlst+-ts-plus-ts-w)
(prove-lemma not-lessp-nts+-ts (rewrite)
(not (lessp (nts+ n ts tr+ w) ts)))
(prove-lemma nts+-alg (rewrite)
(implies (and (numberp n)
(numberp ts)
(numberp tr+)
(not (zerop w))
(not (lessp tr+ ts)))
(equal (nts+ n ts tr+ w)
(if (lessp (plus ts (times n w)) tr+)
(plus ts (times n w))
(plus ts (times w (quotient (difference tr+ ts) w)))))))
(prove-lemma n*-alg-lemma (rewrite)
(implies
(and (numberp x)
(not (equal r 0))
(numberp r)
(not (nendp n ts (plus r ts x) w))
(numberp n)
(numberp ts)
(numberp w)
(not (equal w 0))
(not (lessp (plus ts x) ts))
(lessp (plus ts x) (plus ts w)))
(equal
(add1
(quotient (difference (times w
(nlst+ n ts (plus r ts x) w))
(difference (plus r ts x)
(nts+ n ts (plus r ts x) w)))
r))
(quotient (difference (times n w) x)
r))))
(disable nsig*-alg-lemma-hack1)
(prove-lemma n*-alg-hack1 (rewrite)
(implies (and (nendp n ts (plus r tr) w)
(numberp n)
(numberp ts)
(numberp tr)
(numberp w)
(not (equal w 0))
(numberp r)
(not (equal r 0))
(not (lessp tr ts))
(lessp tr (plus ts w))
(not (lessp (times n w)
(difference tr ts))))
(equal (lessp (difference (times n w)
(difference tr ts))
r)
t)))
(prove-lemma n*-alg (rewrite)
(implies (and (numberp n)
(numberp ts)
(numberp tr)
(not (zerop w))
(not (zerop r))
(not (lessp tr ts))
(lessp tr (plus ts w)))
(equal (n* n ts tr w r)
(quotient (difference (times n w) (difference tr ts))
r)))
((disable nendp-alg nts+-alg nlst+-alg difference-difference-other difference-difference)))
(disable n*-alg-hack1)
(disable n*-alg)
(disable n*-alg-lemma)
(disable nts+-alg)
(disable nlst+-alg)
(disable nendp-alg)
(disable nsig*-upper-bound-hack1)
(disable nsig*-upper-bound-hack2)
(disable nsig*-upper-bound-hack3)
(disable nsig*-upper-bound-lemma2-equality)
(prove-lemma n*-upper-bound (rewrite)
(implies (and (numberp n)
(numberp ts)
(numberp tr)
(not (zerop w))
(not (zerop r))
(not (lessp tr ts))
(lessp tr (plus ts w))
(rate-proximity w r)
(lessp n 18))
(not (lessp n (n* n ts tr w r))))
((disable plus-commutes1 difference-difference)
(enable n*-alg)))
(disable nsig*-upper-bound-lemma1)
(disable nsig*-upper-bound-lemma2)
(prove-lemma n*-lower-bound (rewrite)
(implies (and (numberp n)
(numberp ts)
(numberp tr)
(not (zerop w))
(not (zerop r))
(not (lessp tr ts))
(lessp tr (plus ts w))
(rate-proximity w r)
(lessp n 18))
(not (lessp (n* n ts tr w r) (sub1 (sub1 n)))))
((disable nsig*-lower-bound-lemma1 lessp-quotient-to-lessp-times
quotient times plus difference lessp)
(use (nsig*-lower-bound-lemma1 (tr-ts (difference tr ts)))
(nsig*-upper-bound-lemma2-equality (n (sub1 n))))
(enable n*-alg)))
(disable nsig*-lower-bound-lemma1)
; So now we know n-2 <= (n* n ts tr w r) <= n.
; Now we consider scanning and cdrning.
(prove-lemma len-det (rewrite)
(equal (len (det lst oracle)) (len lst))
((enable det)))
(defn det-listn-hint (nq oracle)
; This is an induction for (det (listn nq 'q) oracle).
(if (zerop nq)
t
(det-listn-hint (sub1 nq) (cdr oracle))))
(defn no (flg nq oracle)
(if (zerop nq)
0
(if (b-xor flg (car oracle))
nq
(no flg (sub1 nq) (cdr oracle)))))
; The following lemma is provided by way of explanation.
(prove-lemma no-is-len-scan-det-listn nil
(implies (numberp nq)
(equal (no flg nq oracle)
(len (scan flg (det (listn nq 'q) oracle)))))
((enable listn det scan b-xor)))
(prove-lemma scan-flg-app-listn-not-flg (rewrite)
(implies (and (lessp 0 n)
(b-xor flg1 flg2))
(equal (scan flg1 (app (listn n flg2) rest))
(app (listn n flg2) rest)))
((enable scan listn)))
(defn scan-oracle (flg nq oracle)
(if (zerop nq)
oracle
(if (b-xor flg (car oracle))
oracle
(scan-oracle flg (sub1 nq) (cdr oracle)))))
; The following lemma looks horrible -- the det expression it introduces
; seems a bad trade. But its oracle is irrelevant elsewhere and its len,
; which is in fact is all we care about, is simple.
(prove-lemma scan-app-det-listn (rewrite)
(implies (and (lessp 0 n)
(b-xor flg1 flg2))
(equal (scan flg1 (app (det (listn nq 'q) oracle)
(app (listn n flg2) rest)))
(app (det (listn (no flg1 nq oracle)
'q)
(scan-oracle flg1 nq oracle))
(app (listn n flg2) rest))))
((induct (det-listn-hint nq oracle))
(enable listn det scan b-xor)))
(disable scan-flg-app-listn-not-flg)
(prove-lemma cdrn-app (rewrite)
(equal (cdrn n (app a b))
(if (lessp n (len a))
(app (cdrn n a) b)
(cdrn (difference n (len a)) b))))
(prove-lemma not-lessp-no (rewrite)
(not (lessp n (no flg n oracle))))
(prove-lemma boolp-implies-det-listn (rewrite)
(implies (boolp flg)
(equal (det (listn n flg) oracle)
(listn n flg)))
((enable boolp)))
; We are about to prove the key lemma that determines baud rate.
(prove-lemma len-warp nil
(equal (len (warp lst ts tr w r))
(n* (len lst) ts tr w r))
((enable warp)))
; To prove n*-plus we have to USE len-warp with an instantiation
; that causes warp-app-listn-q to fire. Len-warp is of lemma class
; nil so that the equality thus derived stays around. But it turns out
; that elsewhere in the proof we have to use len-warp as a rewrite rule!
; So we prove an instance of it that suits our purposes.
(prove-lemma n*-plus-lemma (rewrite)
(equal (len (warp (listn (difference j dwg) f)
ts tr w r))
(n* (difference j dwg)
ts tr w r))
((use (len-warp (lst (listn (difference j dwg) f))))))
; The name n*-plus, below, suggests that the lhs is (n* (plus ...)
; ...) but in fact I named it after the rhs; couldn't bear to rewrite
; the other way.
(prove-lemma n*-plus (rewrite)
(implies (and (numberp ts)
(numberp tr)
(not (zerop w))
(not (zerop r))
(not (lessp tr ts))
(lessp tr (plus ts w))
(lessp w (times 2 r))
(lessp r (times 2 w))
(lessp 2 j)
(numberp i)
(numberp j))
(equal (plus (n* i ts tr w r)
(nqg (nlst* i ts tr w r)
(nts* i ts tr w r)
(ntr* i ts tr w r)
w r)
(n* (difference j
(dwg (nlst* i ts tr w r)
(nts* i ts tr w r)
(ntr* i ts tr w r)
w r))
(tsg (nlst* i ts tr w r)
(nts* i ts tr w r)
(ntr* i ts tr w r)
w r)
(trg (nlst* i ts tr w r)
(nts* i ts tr w r)
(ntr* i ts tr w r)
w r)
w r))
(n* (add1 (plus i j)) ts tr w r)))
((use (len-warp (lst (app (listn i t) (cons 'q (listn j f))))))))
(disable n*-plus-lemma)
; If this lemma can be proved for different constants then the
; whole proof can be shifted to those constants. In particular
; make the replacements indicated below.
; To send cells of size: 32 24 16
; 31 23 15
; 16 12 8
; 15 11 7
(prove-lemma loop-killer-2b (rewrite)
(implies (and (listp msg)
(boolp (car msg))
(bvp (cdr msg))
(numberp ts)
(numberp tr)
(not (zerop w))
(not (zerop r))
(not (lessp tr ts))
(lessp tr (plus ts w))
(rate-proximity w r)
(numberp nq)
(not (lessp 3 nq))
(numberp dw)
(not (lessp 1 dw))
(boolp flg1)
(b-xor flg1 flg2))
(equal (cdrn 10
(scan flg1
(app (det (listn nq 'q) oracle1)
(app (det (warp (smooth flg2 (cell flg1 (difference 4 dw) 13 (car msg)))
ts tr w r)
oracle2)
rest))))
(app (listn (difference (plus (no flg1 nq oracle1)
(n* (difference 17 dw) ts tr w r))
10)
(csig flg1 (car msg)))
rest)))
((enable csig)
(do-not-induct t)))
(disable n*-plus)
(disable cdrn-app)
(disable scan-app-det-listn)
(disable boolp-implies-det-listn)
(disable warp-smooth-cell)
(prove-lemma car-det-listn (rewrite)
(equal (car (det (listn n 'q) oracle))
(if (zerop n)
0
(if (car oracle) t f)))
((induct (det-listn-hint n oracle))
(enable listn det)))
(prove-lemma listp-det (rewrite)
(equal (listp (det lst oracle)) (listp lst))
((enable det)))
(prove-lemma car-scan-oracle (rewrite)
(implies (not (zerop (no flg nq oracle)))
(iff (car (scan-oracle flg nq oracle)) (b-not flg)))
((enable listn listp-listn det b-xor b-not)))
(prove-lemma loop-killer-2a-lemma (rewrite)
(implies (and (listp msg)
(boolp (car msg))
(bvp (cdr msg))
(numberp ts)
(numberp tr)
(not (zerop w))
(not (zerop r))
(not (lessp tr ts))
(lessp tr (plus ts w))
(rate-proximity w r)
(numberp nq)
(not (lessp 3 nq))
(numberp dw)
(not (lessp 1 dw))
(boolp flg1)
(boolp flg2)
(b-xor flg1 flg2))
(equal (car (scan flg1
(app (det (listn nq 'q) oracle1)
(app (det (warp (smooth flg2
(cell flg1
(difference 4 dw)
13
(car msg)))
ts tr w r)
oracle)
rest))))
(b-not flg1)))
((enable warp-smooth-cell scan-app-det-listn cdrn-app car-app car-listn
boolp-implies-det-listn)
(do-not-induct t)))
(disable car-det-listn)
(prove-lemma equal-difference-0 (rewrite)
(equal (equal (difference x y) 0)
(not (lessp y x))))
(prove-lemma loop-killer-2a (rewrite)
(implies (and (listp msg)
(boolp (car msg))
(bvp (cdr msg))
(numberp ts)
(numberp tr)
(not (zerop w))
(not (zerop r))
(not (lessp tr ts))
(lessp tr (plus ts w))
(rate-proximity w r)
(numberp nq)
(not (lessp 3 nq))
(numberp dw)
(not (lessp 1 dw))
(boolp flg1)
(boolp flg2)
(b-xor flg1 flg2))
(equal (recv-bit 10
(scan flg1
(app (det (listn nq 'q) oracle1)
(app (det (warp (smooth flg2
(cell flg1
(difference 4 dw)
13
(car msg)))
ts tr w r)
oracle)
rest))))
(car msg)))
((enable recv-bit car-app car-listn csig)
(do-not-induct t)))
(disable loop-killer-2a-lemma)
; We also have to take care of the new flg computed by recv:
(prove-lemma loop-killer-2c (rewrite)
(implies (and (listp msg)
(boolp (car msg))
(bvp (cdr msg))
(numberp ts)
(numberp tr)
(not (zerop w))
(not (zerop r))
(not (lessp tr ts))
(lessp tr (plus ts w))
(rate-proximity w r)
(numberp nq)
(not (lessp 3 nq))
(numberp dw)
(not (lessp 1 dw)))
(equal (car (app (listn (difference (plus (no flg1 nq oracle1)
(n* (difference 17 dw) ts tr w r))
10)
(csig flg1 (car msg)))
rest))
(csig flg1 (car msg))))
((enable car-app car-listn)
(do-not-induct t)))
; Finally, we must show that recv just eats up the leading string of flgs:
(prove-lemma recv-app-listn (rewrite)
(equal (recv n flg k (app (listn m flg) rest))
(recv n flg k rest))
((expand (recv n flg k (app (listn m flg) rest))
(recv n flg k rest))))
(prove-lemma loop-killer-2 (rewrite)
(implies (and (listp msg)
(boolp (car msg))
(bvp (cdr msg))
(numberp ts)
(numberp tr)
(not (zerop w))
(not (zerop r))
(not (lessp tr ts))
(lessp tr (plus ts w))
(rate-proximity w r)
(numberp nq)
(not (lessp 3 nq))
(numberp dw)
(not (lessp 1 dw))
(boolp flg1)
(boolp flg2)
(b-xor flg1 flg2))
(equal (recv (len msg) flg1 10
(app (det (listn nq 'q) oracle1)
(app (det (warp (smooth flg2 (cell flg1 (difference 4 dw) 13 (car msg)))
ts tr w r)
oracle)
rest)))
(cons (car msg)
(recv (len (cdr msg))
(csig flg1 (car msg))
10
rest))))
((expand (recv (len msg) flg1 10
(app (det (listn nq 'q) oracle1)
(app (det (warp (smooth flg2 (cell flg1 (difference 4 dw) 13 (car msg)))
ts tr w r)
oracle)
rest))))))
(disable recv-app-listn)
; We now turn to the base case in which msg of of len 1. Our killer lemma
; will be named loop-killer-0. This case is special because the cell is not
; always followed by an edge. We'll do a blow-by-blow derivation of loop-killer-0,
; starting with the lhs of the loop concl; the killer lemma will reduce it to the
; rhs, which is just msg.
#|
The lhs of loop-killer-0 is initially:
(RECV (LEN MSG)
FLG1 10
(APP (DET (LISTN NQ 'Q) ORACLE1)
(DET (WARP (CDRN DW
(SMOOTH FLG2
(APP (CDR (CELLS FLG1 5 13 MSG))
(LISTN P2 T))))
TS TR W R)
ORACLE2)))
where (listp msg) and (nlistp (cdr msg)) are known.
|#
(prove-lemma cdr-app-cell-rest (rewrite)
(implies (not (zerop m))
(equal (cdr (app (cell flg1 m n bit)
rest))
(app (cell flg1 (sub1 m) n bit)
rest)))
((enable cdr-app cell listn)))
(prove-lemma smooth-app-cell-rest (rewrite)
(implies (and (not (zerop n))
(b-xor flg2 flg1))
(equal (smooth flg2 (app (cell flg1 m n bit) rest))
(app (smooth flg2 (cell flg1 m n bit))
(smooth (csig flg1 bit) rest))))
((enable cell smooth-flg-app-listn-flg smooth-flg-app-listn-not-flg
smooth-flg-listn-flg smooth-flg-listn-not-flg csig b-not b-xor)))
#|
The lhs is now:
(RECV (LEN MSG)
FLG1 10
(APP (DET (LISTN NQ 'Q) ORACLE1)
(DET (WARP (app (smooth flg2
(cell flg1 (difference 4 dw) 13 (car msg)))
(smooth (csig flg1 (car msg)) (listn p2 t)))
TS TR W R)
ORACLE2)))
We want to drive the warp inside the app and we will use warp-app to do it by
TARGETing the warp above. This introduces a warp-smooth-cell instance, which
we need to analyze, and another warp-app instance about what happens after this
cell. Normally we know what happens next is an edge, so we have a 'q there and
warp-app-listn-q is used instead of warp-app to do this work. But here there is
no trailing 'q. Luckily, we don't need to analyze what goes on after this cell
and so we'll just leave the trailing warp unsimplified.
So the lhs becomes
(RECV (LEN MSG)
FLG1 10
(APP (DET (LISTN NQ 'Q) ORACLE1)
(DET (app (warp (smooth flg2
(cell flg1 (difference 4 dw) 13 (car msg)))
ts tr w r)
(warp (app (lst* (smooth flg2 (cell flg1 (difference 4 dw) 13 (car msg)))
ts tr w r)
(smooth (csig flg1 (car msg)) (listn p2 t)))
(ts* (smooth flg2 (cell flg1 (difference 4 dw) 13 (car msg)))
ts tr w r)
(tr* (smooth flg2 (cell flg1 (difference 4 dw) 13 (car msg)))
ts tr w r)
w r))
ORACLE2)))
and we can apply det-app to produce
(RECV (LEN MSG)
FLG1 10
(APP (DET (LISTN NQ 'Q) ORACLE1)
(app (det (warp (smooth flg2
(cell flg1 (difference 4 dw) 13 (car msg)))
ts tr w r)
oracle2)
(det ...))))
where we really don't care what is in the last det because it is beyond the
only cell we will read.
But now we can apply loop-killer-2 to this and get (list (car msg)).
|#
; The -0a below reminds us that this rule has a TARGET in it.
(prove-lemma loop-killer-0a nil
(implies
(and (listp msg)
(boolp (car msg))
(equal (cdr msg) nil)
(numberp ts)
(numberp tr)
(not (equal w 0))
(numberp w)
(not (equal r 0))
(numberp r)
(not (lessp tr ts))
(lessp tr (plus ts w))
(rate-proximity w r)
(numberp nq)
(not (lessp 3 nq))
(numberp dw)
(not (lessp 1 dw))
(boolp flg1)
(boolp flg2)
(b-xor flg1 flg2))
(equal
(recv (len msg)
flg1 10
(app (det (listn nq 'q) oracle1)
(det (target (warp (cdrn dw
(smooth flg2
(app (cdr (cells flg1 5 13 msg))
(listn p2 t))))
ts tr w r))
oracle2)))
msg))
((expand (cells flg1 5 13 msg))
(disable len)
(enable cdrn-dw-smooth-cell cdrn-dw-app-smooth-cell warp-app)))
; We now remove the TARGET.
(prove-lemma loop-killer-0 (rewrite)
(implies
(and (listp msg)
(boolp (car msg))
(equal (cdr msg) nil)
(numberp ts)
(numberp tr)
(not (equal w 0))
(numberp w)
(not (equal r 0))
(numberp r)
(not (lessp tr ts))
(lessp tr (plus ts w))
(rate-proximity w r)
(numberp nq)
(not (lessp 3 nq))
(numberp dw)
(not (lessp 1 dw))
(boolp flg1)
(boolp flg2)
(b-xor flg1 flg2))
(equal
(recv (len msg)
flg1 10
(app (det (listn nq 'q) oracle1)
(det (warp (cdrn dw
(smooth flg2
(app (cdr (cells flg1 5 13 msg))
(listn p2 t))))
ts tr w r)
oracle2)))
msg))
((enable target)
(use (loop-killer-0a))))
(disable cdr-app-cell-rest)
; The two hypotheses about flg1 and flg2 being boolp were added late in the
; development of the loop theorem and I have to prove that the inductive
; instantiation satisfies them.
(prove-lemma boolp-b-not (rewrite)
(boolp (b-not x))
((enable boolp b-not)))
(prove-lemma boolp-csig (rewrite)
(implies (boolp flg)
(boolp (csig flg bit)))
((enable boolp b-not)))
(prove-lemma loop (rewrite)
(implies (and (bvp msg)
(numberp ts)
(numberp tr)
(not (zerop w))
(not (zerop r))
(not (lessp tr ts))
(lessp tr (plus ts w))
(rate-proximity w r)
(numberp nq)
(not (lessp 3 nq))
(numberp dw)
(not (lessp 1 dw))
(boolp flg1)
(boolp flg2)
(b-xor flg1 flg2))
(equal (recv (len msg)
flg1
10
(app (det (listn nq 'q) oracle1)
(det (warp (cdrn dw
(smooth flg2
(app (cdr (cells flg1 5 13 msg))
(listn p2 t))))
ts tr w r)
oracle2)))
msg))
((disable cells len)
(induct (loop-ind-hint nq oracle1 dw flg2 flg1 msg ts tr w r oracle2))))
; The proof idea here is to force the expansion of (bvp msg). The nil
; case goes through. The (listp msg) case allows the application of
; top-async-send, which converts the conclusion to an instance of our
; loop form.
(prove-lemma top nil
(implies (and (bvp msg)
(numberp ts)
(numberp tr)
(not (zerop w))
(not (zerop r))
(not (lessp tr ts))
(lessp tr (plus ts w))
(rate-proximity w r)
(numberp p1))
(equal (recv (len msg)
t
10
(async (send msg p1 5 13 p2)
ts tr w r oracle))
msg))
((disable async)
(expand (bvp msg))))
; JSM
; July 31, 1991
; That concludes the main theorem. During the course of discovering
; the proof above I also did some related work that I wish to preserve
; and hence include in this events file. The first is the development
; of the algebraic identities for the recursive functions used to talk
; about warping.
(enable nendp-alg)
(prove-lemma nts*-alg-lemma1 (rewrite)
(IMPLIES (AND (NUMBERP X)
(equal (times n w) (plus r x))
(NUMBERP N)
(NUMBERP TS)
(NOT (EQUAL W 0))
(NUMBERP W)
(NOT (EQUAL R 0))
(NUMBERP R))
(not (NENDP N TS (PLUS R TS X) W))))
(prove-lemma nts*-alg-lemma2 (rewrite)
(implies
(and (numberp x)
(not (equal r 0))
(numberp r)
(not (nendp n ts (plus r ts x) w))
(numberp n)
(numberp ts)
(not (equal w 0))
(numberp w)
(not (lessp (plus ts x) ts))
(lessp (plus ts x) (plus ts w)))
(equal
(plus
(nts+ n ts (plus r ts x) w)
(times w
(quotient
(difference
(plus r ts x
(times r
(quotient (difference (times w
(nlst+ n ts (plus r ts x) w))
(difference (plus r ts x)
(nts+ n ts (plus r ts x) w)))
r)))
(nts+ n ts (plus r ts x) w))
w)))
(plus ts
(times w
(quotient (plus x
(times r
(quotient (difference (times n w) x)
r)))
w)))))
((enable nlst+-alg nts+-alg)))
(disable difference-difference)
(disable difference-difference-other)
; Acknowledgement: This lemma was finally stated accurately by Matt Wilding.
(prove-lemma nts*-alg (rewrite)
(implies (and (numberp n)
(numberp ts)
(numberp tr)
(not (zerop w))
(not (zerop r))
(not (lessp tr ts))
(lessp tr (plus ts w)))
(equal (nts* n ts tr w r)
(plus ts
(times w
(quotient
(difference
(plus tr
(times r
(quotient
(difference (times n w)
(difference tr ts))
r)))
ts)
w)))))
((induct (nts* n ts tr w r))
(disable nendp-alg nts+-alg nlst+-alg)))
; The following lemma ought to be called ntr*-alg-lemma1 because it is the
; first in direct support of ntr*-alg. But it is analogous to the ...lemma2
; lemmas of the other algebraic theorems (because its lemma1 needs were met by
; a prior lemma1).
(prove-lemma ntr*-alg-lemma2 (rewrite)
(implies (and (numberp x)
(not (equal r 0))
(numberp r)
(not (nendp n ts (plus r ts x) w))
(numberp n)
(numberp ts)
(not (equal w 0))
(numberp w)
(not (lessp (plus ts x) ts))
(lessp (plus ts x) (plus ts w)))
(equal
(plus r ts x
(times r
(quotient (difference (times w
(nlst+ n ts (plus r ts x) w))
(difference (plus r ts x)
(nts+ n ts (plus r ts x) w)))
r)))
(plus ts x
(times r
(quotient (difference (times n w) x)
r)))))
((enable difference-difference difference-difference-other nlst+-alg nts+-alg)))
(prove-lemma ntr*-alg (rewrite)
(implies (and (numberp n)
(numberp ts)
(numberp tr)
(not (zerop w))
(not (zerop r))
(not (lessp tr ts))
(lessp tr (plus ts w)))
(equal (ntr* n ts tr w r)
(plus tr
(times r
(quotient
(difference (times n w)
(difference tr ts))
r)))))
((induct (ntr* n ts tr w r))
(disable nendp-alg nts+-alg nlst+-alg)))
(prove-lemma nlst*-alg-lemma2 (rewrite)
(implies (and (numberp x)
(not (equal r 0))
(numberp r)
(not (nendp n ts (plus r ts x) w))
(numberp n)
(numberp ts)
(not (equal w 0))
(numberp w)
(not (lessp (plus ts x) ts))
(lessp (plus ts x) (plus ts w)))
(equal
(difference
(nlst+ n ts (plus r ts x) w)
(quotient
(difference (plus ts x
(times r
(quotient (difference (times n w) x)
r)))
(nts+ n ts (plus r ts x) w))
w))
(difference n
(quotient (plus x
(times r
(quotient (difference (times n w) x)
r)))
w))))
((enable difference-difference difference-difference-other nlst+-alg nts+-alg)))
(prove-lemma nlst*-alg (rewrite)
(implies (and (numberp n)
(numberp ts)
(numberp tr)
(not (zerop w))
(not (zerop r))
(not (lessp tr ts))
(lessp tr (plus ts w)))
(equal (nlst* n ts tr w r)
(difference n (quotient
(difference
(plus tr
(times r
(quotient
(difference (times n w)
(difference tr ts))
r)))
ts)
w))))
((induct (nlst* n ts tr w r))
(disable nendp-alg nts+-alg nlst+-alg)))
(disable nendp-alg)
(disable nlst+-alg)
(disable nts+-alg)
(disable nts*-alg-lemma1)
(disable nts*-alg-lemma2-hack1)
(disable nts*-alg-lemma2)
(disable nts*-alg)
(disable ntr*-alg-lemma2-hack1)
(disable ntr*-alg-lemma2)
(disable ntr*-alg)
(disable nlst*-alg-lemma2-hack1)
(disable nlst*-alg-lemma2)
(disable nlst*-alg)
; The second piece of preserved work is the proof that deterministic fuzzy edge
; detection is impossible.
; An Aside: Does the Treatment of (X) Preclude Edge Detection?
; May 28, 1991.
; (Note: In this section we adopt the convention that when a list is
; treated as a series of signals arriving at a pin then the last
; (right-most) element of the list is the first signal to arrive.
; This convention is at variance with that used throughout the rest of
; our asychronous work, where the signals arrive in the order in which
; they appear in the list. We adopted this convention to make our
; pictures of edges and our register chains look traditional. None of
; the work in this section is used outside of this section. The whole
; point is to explain why we use Q (which is nondeterministically t or
; f on each occurrence) rather than X (which, in the words of Bishop
; Brock, is "your worst nightmare").)
; I have been trying for some weeks, off and on, to write an edge
; detector that could tolerate an (X) at the edge and never be
; undefined. I have proved that is impossible. The formalization
; and proof are given below, after an informal sketch of the problem.
; Let a "fuzzy edge" be a sequence of signals that is initially
; all f's and then becomes all t's -- except that between
; the last f and the first t is an x, i.e.,
; - - - - - - -
; \
; - - - - - - -
; ...t t t t t t t x f f f f f f f ...
; A "well-defined" circuit is one that always returns either t or f.
; That is, it never answers x.
; Finally, an "edge detector" is a sequential circuit that sits on the
; line listening to the incoming f's and reporting "no edge yet"; if the
; line eventually goes high, the circuit eventually reports "an edge
; came by." I am willing to give the circuit designer as many leading
; f's and trailing t's as he wants and I don't care how long after the
; edge he says "an edge came by" as long as he is correct.
; So a "well-defined fuzzy edge detector" is one that always returns t
; or f and successfully detects a fuzzy edge eventually.
; Initially I thought I could build a well-defined fuzzy edge
; detector. For example, chain three successive pulses into registers
; so that you could see "t x f" in registers r0, r1, and r2, and then
; see if r0 is t while r2 is f. Well, that doesn't work because at
; the moment before you see "t x f" you see "x f f" and the logic
; described would produce an x. So you say to yourself, ``there is
; only one x in the sequence, so if I widen the window to "t t x f f"
; in registers r0 through r4, and look for, say, r0 and -r3 or r1 and
; -r4, then that bad case, namely "t x f f f" won't get me.'' But now
; "x f f f f" will get you. Nevertheless, the feeling persisted that
; since I could have as many t's and f's as I wanted and there was
; only one x, I could somehow (perhaps by majority voting?) protect
; myself from that x while still finding the edge.
; I prove below a theorem that tells me that you can't build a
; well-defined fuzzy edge detector.
; My theorem actually does not consider sequential circuits but
; instead addresses itself to combinational circuits that have access
; to an arbitrarily wide "window" in the signal. One could imagine,
; for example, that the sequential circuit just chains the signal
; through a sequence of k registers, constantly maintaining a window k
; wide on the signal and testing that window with combinational logic.
; If a fuzzy edge comes through that window, the combinational logic
; circuit must detect it.
; There are k+2 different views of a fuzzy edge in a window k wide. For
; example, if k is 6 then the 8 views are:
; f f f f f f
; x f f f f f
; t x f f f f
; t t x f f f
; t t t x f f
; t t t t x f
; t t t t t x
; t t t t t t
; I limit myself to combinational expressions in F-AND and F-NOT
; because I believe the rest of the primitives can be defined in terms
; of those two (and here I mean not just for T and F but also for X).
; I define an interpreter for F-AND and F-NOT expressions with
; variables v0, v1, ..., vk, where the variables address the
; corresponding positions in the window. Call such an expression "a
; candidate fuzzy edge detector of width k."
; I prove that if a candidate fuzzy edge detector of width k is
; well-defined (T or F) on all k+2 views of the window, then it is
; constant!
; This work relies upon certain definitions from Warren and Bishop's
; stuff, namely:
; From (note-lib "/usr/home/brock/constants/lsi/reg")
(add-shell x nil xp nil)
; From (note-lib "/usr/home/brock/constants/lsi/reg")
(defn f-not (a)
(if (boolp a) (not a) (x)))
; From (note-lib "/usr/home/brock/constants/lsi/reg")
(defn f-and (a b)
(if (or (equal a f) (equal b f))
f
(if (and (equal a t) (equal b t))
t
(x))))
(defn exprp (x)
; This function recognizes well-formed expressions in F-NOT and F-AND
; that use the constants T and F and the variables 0, 1, ..., k-1.
(if (nlistp x)
(or (equal x 't)
(equal x 'f)
(numberp x))
(if (equal (car x) 'f-not)
(and (exprp (cadr x))
(equal (cddr x) nil))
(and (equal (car x) 'f-and)
(exprp (cadr x))
(exprp (caddr x))
(equal (cdddr x) nil)))))
(defn max-var (x)
; The maximum variable number in expr x. This determines
; the width of the window for which x might be an edge
; detector.
(if (nlistp x)
(if (or (equal x 't)
(equal x 'f))
0
x)
(if (equal (car x) 'f-not)
(max-var (cadr x))
(max (max-var (cadr x)) (max-var (caddr x))))))
(defn width (x) (add1 (max-var x)))
; Any expression is a candidate for an edge detector of size k, where
; k is the width of the expression.
; To evaluate an expression of a given width, k, we must have a vector
; of length k which assigns values (positionally) to each of the k
; variables. By convention, if a vector is insufficiently long or
; contains a non-Boolean assignment to a variable, we will assume it
; assigns (X) to that variable. Thus, the empty vector is a
; convenient way to map all variables to (X). This is unimportant in
; our main result but is used in a subsequent result that shows
; that an expression that is defined on nil is constant.
(defn var-val (n vector)
(if (boolp (nth n vector))
(nth n vector)
(x)))
; Here is the interpreter for expressions wrt a given vector:
(defn val (x vector)
(if (nlistp x)
(if (equal x 't)
t
(if (equal x 'f)
f
(var-val x vector)))
(if (equal (car x) 'f-not)
(f-not (val (cadr x) vector))
(f-and (val (cadr x) vector)
(val (caddr x) vector)))))
(enable boolp)
(prove-lemma var-val-is-x-or-boolp (rewrite)
(implies (not (equal (var-val x vector) (x)))
(boolp (var-val x vector))))
(prove-lemma val-is-x-or-boolp (rewrite)
(implies (not (equal (val x vector) (x)))
(boolp (val x vector))))
(disable boolp)
; We need to generate the complete list of k+2 views of an edge coming
; thorugh a window of width k. We enumerate the edges as suggested
; below, e.g., 0 is the one containing all f's, k+1 contains all t's,
; etc.
; 5 t t t t
; 4 t t t x
; 3 t t x f
; 2 t x f f
; 1 x f f f
; 0 f f f f
; The order of enumeration is important to our proof. In particular,
; if you think of the edges enumerated as above, then an integer, e.g.,
; 3, can either represent the given edge or all the edges at and below that
; one. And we sometimes induct on these integers to build the set of all
; edges. We use the property of the enumeration that if a variable is
; Boolean (never x) in all the edges at or below i, then it is in fact
; constant.
(defn edge (k i)
; Generate the ith edge of length k.
(if (zerop k) nil
(if (lessp i k)
(app (edge (sub1 k) i) (list f))
(if (equal i k)
(app (edge (sub1 k) i) (list (x)))
(app (edge (sub1 k) (sub1 i)) (list t))))))
; Note: In the original development of this theorem, we used the
; natural numbers to encode both edges and sets of edges. This
; restricted our evaluation function to work only on edges and thus
; restricted what we could say about the value of expressions. We
; therefore decided to represent edges as bit vectors as above. But
; to preserve exactly the structure of the proof, we will prove the
; old definition of var-val in var-val-edge below.
(prove-lemma length-edge (rewrite)
(equal (len (edge k i)) (fix k)))
(enable cdrn-app)
(prove-lemma cdrn-too-big (rewrite)
(implies (not (lessp n (len lst)))
(not (listp (cdrn n lst)))))
(prove-lemma lessp-n-1 (rewrite)
(equal (lessp n 1) (zerop n)))
(prove-lemma nth-edge (rewrite)
(implies (and (numberp n)
(numberp k)
(not (zerop k)))
(equal (car (cdrn n (edge k i)))
(if (lessp n k)
(if (lessp (add1 n) i)
t
(if (equal (add1 n) i)
(x)
f))
0)))
((induct (edge k i))
(enable car-app cdr-app cdrn-app)))
(prove-lemma var-val-edge (rewrite)
(implies (and (numberp n)
(numberp k)
(not (zerop k))
(lessp n k))
(equal (var-val n (edge k i))
(if (lessp n k)
(if (lessp (add1 n) i)
t
(if (equal (add1 n) i)
(x)
f))
(x)))))
(disable var-val)
(disable edge)
; We now develop the idea that an expression is "well-defined", i.e.,
; its value is never x on any edge of the appropriate size. To
; do this we have to check the value on every edge.
(defn all-edges (k i)
(if (zerop i)
(list (edge k 0))
(cons (edge k i) (all-edges k (sub1 i)))))
; The following function determines that x is well-defined for all
; vectors in a given set test-set:
(defn well-defined1 (x test-set)
(if (nlistp test-set)
t
(and (not (equal (val x (car test-set)) (x)))
(well-defined1 x (cdr test-set)))))
; So an expression is well-defined if it is well-defined on all the edges
; of the appropriate size.
(defn well-defined (x)
(well-defined1 x (all-edges (width x) (add1 (width x)))))
; The theorem we wish to prove is:
; (implies (and (exprp x)
; (well-defined x))
; (equal (val x (edge (width x) i))
; (val x (edge (width x) 0))))
; That is, if an expression is well-defined on all edges, then it is
; constant on all edges.
(prove-lemma val-on-successive-edges-is-constant-when-defined (rewrite)
(implies (and (exprp x)
(not (zerop i))
(not (lessp k (width x)))
(not (equal (val x (edge k i)) (x)))
(not (equal (val x (edge k (sub1 i))) (x))))
(equal (val x (edge k i))
(val x (edge k (sub1 i))))))
(prove-lemma numberp-max-var (rewrite)
(implies (exprp x) (numberp (max-var x))))
(prove-lemma val-is-x-or-boolp-2 (rewrite)
(implies (and (not (equal (val x vector) (x)))
(val x vector))
(equal (val x vector) t))
((enable boolp)
(disable val-is-x-or-boolp)
(use (val-is-x-or-boolp))))
(prove-lemma everything-defined-at-0 (rewrite)
(implies (and (zerop zero)
(exprp x)
(not (lessp k (width x))))
(not (equal (val x (edge k zero)) (x)))))
(prove-lemma well-defined1-is-a-universal-quantifier (rewrite)
(implies (and (exprp x)
(not (lessp k (width x)))
(well-defined1 x (all-edges k i))
(not (lessp i j)))
(not (equal (val x (edge k j)) (x))))
((induct (plus i xxx))))
(prove-lemma edge-at-non-numberp (rewrite)
(implies (not (numberp i))
(equal (edge k i) (edge k 0)))
((enable edge)))
(prove-lemma well-defined1-implies-constant nil
(implies (and (exprp x)
(not (lessp k (width x)))
(well-defined1 x (all-edges k i))
(not (lessp i j)))
(equal (val x (edge k j)) (val x (edge k 0))))
((induct (plus j xxx))))
(prove-lemma edge-beyond-max nil
(implies (lessp (add1 k) i)
(equal (edge k i) (edge k (add1 k))))
((enable edge)))
(prove-lemma well-defined-implies-constant nil
(implies (and (exprp x)
(well-defined x))
(equal (val x (edge (width x) i))
(val x (edge (width x) 0))))
((disable well-defined1 all-edges)
(use (well-defined1-implies-constant (k (width x))
(i (add1 (width x)))
(j i))
(well-defined1-implies-constant (k (width x))
(i (add1 (width x)))
(j (add1 (width x))))
(edge-beyond-max (k (width x))))))
; Here is a related result. It says that if an expression is defined
; on the vector that assigns x to each input, then the expression is
; constant.
(prove-lemma non-x-on-nil-implies-constant nil
(implies (and (exprp x)
(not (equal (val x nil) (x))))
(equal (val x vector) (val x nil)))
((enable var-val)))
; Some stronger conjectures are not valid. Consider for example,
; "When x is well-defined (on all edges) then x is constant." This
; conjecture is falsified by the expression '(f-and (f-not 0) 1).
; As can be determined by r-loop, (well-defined '(f-and (f-not 0) 1)).
; But (val '(f-and (f-not 0) 1) (list f f)) = f
; while
; (val '(f-and (f-not 0) 1) (list f t)) = t.
; The conjecture "When x is well-defined on some set of vectors s, then
; x is constant on s" is invalidated by the expression 0 on the set s =
; (list (list t) (list f)).
; One is tempted to strengthen the hypothesis above by additionally
; requiring that there exist a vector in s that makes each variable
; of x unknown. That conjecture is invalidated by x =
; (f-and (f-not 0) 1), again, using the test set:
; (list (list f f) (list (x) f) (list t (x)) (list f t)).
; The first and last test vectors produce different well-defined values
; of x. Observe that the only difference between this test set
; and the set of edges of size 2 is the last vector.
; Note added in proof: On Thursday, May 23, I listened to Matt
; Kaufmann talk about his "reset results" with Bishop and Warren. His
; results established many monotonicity properties of dual-eval and
; got me once again considering the question "what is X?" I had been
; trying to think of X as nondeterministically 1 or 0. I talked with
; Bishop about what X was that afternoon. Upon leaving Bishop's
; office at 6pm I had resolved to prove that you couldn't build a
; fuzzy edge detector with F-NOT and F-AND. The suspicion that you
; couldn't do it had come to me while at Oberwulfach (I spent hours
; trying) but I decided to lay the problem aside afterwards and focus
; on the formalization of asynchronous communication.
; It took me a night and a day (Thursday evening and then Friday, May
; 24) to get the result its raw form (in which I used numbers to
; encode views through the window). Then I set about cleaning it up
; by going to the vectors used here. Lisa's birthday, the Memorial
; Day weekend, an air conditioning failure at CLI, and Matt Wilding's
; birthday party all prevented useful work on the weekend. (But I
; thought a lot about the problem -- it was surprisingly hard to
; define (edge k i) in a way that let me easily prove the var-val
; theorem about it.) On Tuesday, I worked another three hours before
; finally getting the file in the form shown.
; At that point I sent a message about it to Warren, Bishop and Matt.
; In my message I asked Matt whether these results were derivable from
; his monotonicity results. His reply is below.
; From kaufmann@CLI.COM Tue May 28 14:44:01 1991
; Received: by CLI.COM (4.1/1); Tue, 28 May 91 14:43:59 CDT
; Date: Tue, 28 May 91 14:44:33 CDT
; From: Matt Kaufmann
; To: moore@CLI.COM
; Cc: Brock@CLI.COM, Hunt@CLI.COM
; Subject: Fuzzy Edge Detection
; Nice going. Yes, I think that the kind of monotonicity results that I
; proved could be used to get your result (though I don't know if that
; would be any easier than whatever proof you gave). (Maybe "kind of"
; could even be omitted above.) The informal argument is as follows.
; Consider for example the following two successive rows.
; (r1) t x f f f f
; (r2) t t x f f f
; Notice that these both `approximate' the following row:
; (r3) t t f f f f
; Now since circuits are monotone, and since (r1) approximates (r3), we
; have that f(r1) approximates f(r3), where f is the candidate fuzzy
; edge detector. But since f(r1) is well-defined (i.e. T or F), then
; since T and F can only approximate themselves (respectively), we have
; that f(r1) = f(r3). A similar argument shows f(r2) = f(r3).
; Therefore f(r1) = f(r2). Arguing in this way we can show that for all
; successive rows r and r', f(r) = f(r'); hence by an easy induction,
; f(r) = f(r') for all rows r, r'.