#|

 Copyright (C) 1994 by Computational Logic, Inc.  All Rights Reserved.

 This script is hereby placed in the public domain, and therefore unlimited
 editing and redistribution is permitted.

 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.
|#

;; Matt Kaufmann

(boot-strap nqthm)


;; Here's a little note showing a method for proving (in some cases)
;; permutation-independence of list functions that are generated by
;; associative-commutative binary functions.  For example, we'd like to
;; know that if SUMLIST is a function that adds up the elements of a
;; given list, then permuting a list X doesn't change the value of
;; SUMLIST(X).  The method is as follows.  First, we introduce a name
;; AC-FN for an arbitrary associative-commutative binary function, along
;; with the axioms saying so (and a "witness" for the consistency of this
;; axiom, namely PLUS).  This is followed by the definition of a function
;; FOLDR, which is defined in terms of AC-FN by applying it repeatedly to
;; the members of a given list.  After defining PERMUTATION-P and proving
;; some useful rewrite rules, I prove the main lemma FOLDR-PERMUTATION-P,
;; which says (informally speaking, here) that FOLDR gives the same value
;; when you permute its list argument.  Then, using the "functional
;; instantiation" mechanism in the Boyer-Moore system, I apply this
;; "generic" lemma (that is, FOLDR-PERMUTATION-P) to three examples:  the
;; sum of the elements of a list, the product of the elements of a list,
;; and the WIRED-OR of the elements of a list (in a four-valued logic,
;; intuitively speaking, though I don't actually ever need to say so).
;; 
;; As usual, this is all in Lisp syntax.  Everything from a semicolon to
;; the end of a line is a comment, and I try to use lots of those in
;; order to explain what's going on.  Without further ado, then, here is
;; the annotated list of Boyer-Moore events (i.e. input).
;; 
;; By the way, it took about two hours for me to do this exercise
;; (including documentation).  Replay time (real time) was about a minute
;; and a quarter on a Sun 3/60; run time reported was 24.8 secs.  In case
;; it's not clear.... the text below is all input to the Boyer-Moore
;; prover.
;; 
;; ============================================================

;; Add a new function declaring that the function ac-fn is
;; an associative-commutative binary function.

(constrain ac-fn-intro (rewrite)
           (and (equal (ac-fn x y)
                       (ac-fn y x))
                (equal (ac-fn (ac-fn x y) z)
                       (ac-fn x (ac-fn y z))))
           ;; The following just says that the prover should
           ;; use PLUS in place of AC-FN in order to show that
           ;; the axiom above is consistent (in fact, conservative).
           ((ac-fn plus)))

;; Next, recursively define a function that continually applies the
;; binary function AC-FN to the elements of a list.  This is a
;; "fold-right" function; an analogous "fold-left" function exists,
;; and should be easy to prove equivalent to foldr; maybe I'll do that
;; later.

(defn foldr (lst root)
  (if (listp lst)
      (ac-fn (car lst)
             (foldr (cdr lst) root))
    root))

;; The following function removes the first occurrence of the element
;; a from the list x; it's auxiliary to the definition of permutation-p.

(defn remove1 (a x)
  (if (listp x)
      (if (equal a (car x))
          (cdr x)
        (cons (car x)
              (remove1 a (cdr x))))
    x))

;; Here is the usual recursive definition of permutation-p.

(defn permutation-p (x1 x2)
  (if (listp x1)
      (and (member (car x1) x2)
           (permutation-p (cdr x1)
                          (remove1 (car x1) x2)))
    (nlistp x2)))

;; The strategy below is as follows.  I wanted to prove that foldr is
;; preserved under permutations of its (first) argument; that's the
;; lemma called FOLDR-PERMUTATION-P below.  The proof attempt led me
;; to prove a lemma called FOLDR-REMOVE1, which occurs just above
;; FOLDR-PERMUTATION-P.  In order to prove FOLDR-REMOVE1, though, I
;; found that I needed a property of associative-commutative
;; functions, stated in the lemma AC-FN-COMMUTATIVITY-2 below.

;; The following two lemmas are used in the proof of the lemma named
;; AC-FN-COMMUTATIVITY-2 below, which is key to FOLDR-REMOVE1, which
;; in turn is crucial for FOLDR-PERMUTATION-P.

(prove-lemma ac-fn-assoc-reversed (rewrite)
             (equal (ac-fn x (ac-fn y z))
                    (ac-fn (ac-fn x y) z)))

(prove-lemma ac-fn-comm nil
  (equal (ac-fn x z)
         (ac-fn z x)))

(prove-lemma ac-fn-commutativity-2 (rewrite)
  (equal (ac-fn z (ac-fn x a))
         (ac-fn x (ac-fn z a)))
  ;; The following hint instructs the prover not to use the general
  ;; commutativity and associativity rewrite rules that were introduced
  ;; with AC-FN; note that that associativity rule would loop with the
  ;; rule AC-FN-ASSOC-REVERSED proved above.
  ((disable ac-fn-intro)
   ;; However, we do need one instance of commutativity, provided by the
   ;; following hint.
   (use (ac-fn-comm))))

;; The lemma AC-FN-ASSOC-REVERSED was used in the proof of the lemma
;; immediately above, but now we want to turn it off as a rewrite rule
;; so that it doesn't loop in combination with the associativity rule
;; introduced at the outset.
(disable ac-fn-assoc-reversed)

(prove-lemma foldr-remove1 (rewrite)
  (implies (member z x2)
           (equal (ac-fn z (foldr (remove1 z x2) root))
                  (foldr x2 root))))

(prove-lemma foldr-permutation-p (rewrite)
  (implies (permutation-p x1 x2)
           (equal (foldr x1 root)
                  (foldr x2 root))))

;; Having proved this general fact about foldr, let us apply it to
;; three examples:  the sum of the elements of a list, the product
;; of the elements of a list, and a wired-or function.

;;;;;;;;;; SUMLIST ;;;;;;;;;;

;; First, we give a natural recursive definition of the sum of the
;; elements of a list.  One could easily generate such definitions
;; automatically from the definition of foldr, by the way; for now,
;; I'll take each application as it comes.

(defn sumlist (lst)
  (if (listp lst)
      (plus (car lst)
            (sumlist (cdr lst)))
    0))

;; Let us now instantiate the main result called FOLDR-PERMUTATION-P
;; above to the particular case in question, i.e. to the case of the
;; sum of the elements of a list.

(functionally-instantiate
 ;; the name of this "event", so that we can refer to it later
 sumlist-permutation-p-lemma
 ;; *not* a rewrite rule this time; I have other plans for this lemma
 nil
 ;; Rather than stating the lemma, I'll use *auto* to tell the system
 ;; to generate the lemma statement automatically from FOLDR-PERMUTATION-P
 ;; (which is on the next line) by using an appropriate functional
 ;; substitution (see the lines after that).
 *auto*
 foldr-permutation-p
 ;; Finally, I have to tell the system how to use particular functions
 ;; in place of the "generic" functions that FOLDR-PERMUTATION-P is
 ;; about.  So, I'll tell it to use PLUS in place of AC-FN and to use
 ;; the indicated LAMBDA expression in place of FOLDR (which, you'll notice,
 ;; corresponds in some reasonable sense to FOLDR when one replaces AC-FN
 ;; by PLUS).
 ((ac-fn plus)
  (foldr (lambda (lst root)
           ;; It's unfortunately subtle why one needs the IF below; I'll
           ;; explain upon request.
           (if (listp lst)
               (plus root (sumlist lst))
             root)))))

;; Finally, I'll use the lemma above as a hint so that the theorem that
;; SUMLIST is invariant under a permutation of its argument is immediate.

(prove-lemma sumlist-permutation-p (rewrite)
  (implies (permutation-p x1 x2)
           (equal (sumlist x1)
                  (sumlist x2)))
  ;; The following hint says to use the lemma called
  ;; SUMLIST-PERMUTATION-P-LEMMA, which is immediately above, under
  ;; the substitution where ROOT gets 0.  Such a hint could certainly
  ;; be generated automatically.
  ((use (sumlist-permutation-p-lemma
         (root 0)))))

;;;;;;;;;; TIMESLIST ;;;;;;;;;;

;; Now let's repeat the exercise above for TIMES.  This case proceeds
;; similarly to the PLUS case, except we need a few lemmas about TIMES
;; because less is built into the prover about TIMES than for PLUS.
;; In practice, many users of the prover at CLInc would load a
;; standard arithmetic library that has these facts about TIMES, any
;; many others, included in it.  (Such a library will have already
;; been proved correct, so such an inclusion is sound.)

(prove-lemma times-assoc (rewrite)
  (equal (times (times x y) z)
         (times x (times y z))))

(prove-lemma times-1 (rewrite)
  (equal (times x 1)
         (fix x)))

(prove-lemma times-comm (rewrite)
  (equal (times x z)
         (times z x)))

;; Now we repeat the three main events that we did for PLUS:
;; definition of the n-ary version, the functional instantiation, and
;; the main result.  It turns out that we need the "commutativity-2"
;; property proved above for ac-fn as a lemma; the first
;; functionally-instantiate event below derives this property for
;; times as an immediate corollary.

(defn timeslist (lst)
  (if (listp lst)
      (times (car lst)
             (timeslist (cdr lst)))
    1))

;; Need commutativity-2 as a lemma.....

(functionally-instantiate times-commutativity-2 (rewrite)
  *auto*
  ac-fn-commutativity-2
  ((ac-fn times)))

(functionally-instantiate
 ;; name of lemma:
 timeslist-permutation-p-lemma
 ;; as before, not a rewrite rule:
 nil
 ;; generated automatically from the lemma named FOLDR-PERMUTATION-P
 *auto*
 foldr-permutation-p
 ;; using the following functional subsitution
 ((ac-fn times)
  (foldr (lambda (lst root)
           (if (listp lst)
               (times root (timeslist lst))
             root)))))

(prove-lemma timeslist-permutation-p (rewrite)
  (implies (permutation-p x1 x2)
           (equal (timeslist x1)
                  (timeslist x2)))
  ((use (timeslist-permutation-p-lemma (root 1)))))

;;;;;;;;;; WIRED-OR ;;;;;;;;;;

;; Let's say that wired-or treats Z as an identity, and returns X if
;; either argument is not Z.  In particular, the OR of Z with itself
;; is Z.

;; First, the binary version.....

(defn or2 (a b)
  (if (equal a 'z)
      b
    (if (equal b 'z)
        a
      'x)))

;; Now, the list version, defined analogously to FOLDR:

(defn wired-or (lst)
  (if (listp lst)
      (or2 (car lst) (wired-or (cdr lst)))
    'z))

;; Now we just copy the usual two events, using 'z for root.
;; Commutativity-2 should be trivial in this case, so I won't separate
;; it out as a separate lemma as I did for the TIMES version above.

(functionally-instantiate
 wired-or-permutation-p-lemma
 nil
  *auto*
  foldr-permutation-p
  ((ac-fn or2)
   (foldr (lambda (lst root)
            (if (listp lst)
                (or2 root (wired-or lst))
              root)))))

(prove-lemma wired-or-permutation-p (rewrite)
  (implies (permutation-p x1 x2)
           (equal (wired-or x1)
                  (wired-or x2)))
  ((use (wired-or-permutation-p-lemma (root 'z)))))