#|

Lab 5. Propositional Logic

Open this file in ACL2s Mode.

We use the following ascii character combinations to represent the Boolean
connectives:

  NOT     ~

  AND     &
  OR      +
  NOR     !

  IMPLIES =>

  EQUIV   =
  XOR     <>

The binding powers of these functions are listed from highest to lowest
in the above table. Within one group (no blank line), the binding powers
are equal. This is the same as in class.

The symbols for the operators are different than used in the homeworks
and previous labs. That is on purpose.  Different books use different
symbols, so it is good to get accustomed to that.

(p ! q) is equivalent to ~(p + q).  It is called "NOR" because it 
is the Negation of an Or.


|#

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Simplification of formulas
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

#|

There are many ways to represent a formula. For example:

p + (p => q)

is equivalent to

true

For each of the following, try to find the simplest equivalent
formula. By simplest, we mean the one with the least number of
connectives and parentheses. You can use any unary or binary
connective shown above in the propositional logic section.  
Write out an equational proof. Doing so provides more assurance
that you have not made mistakes. Here is an equational proof of
the above.

    p + (p => q)
= { p=>q = ~p+q }
    p + ~p + q
= { p+~p=true, constant propagation }
    true

You can use ACL2s to check your answers as follows. 

|#

(thm (implies (and (booleanp p)
                   (booleanp q))
              (iff (or p (implies p q))
                   t)))

#|
(1) ~a & ~b & (a + b) 
...

(2) ~a & (a <> c) & (a <> b) 
...
   
(3) p => (q => p & q)
...

(4) (a => b) & (~ a => c) <> (a & b) + (~a & c)
...

|#

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Complete Boolean Bases
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

#|

 In class, we saw that {+, ~} is a complete Boolean base.  There are
 complete Boolean bases that consist of only one operator. One
 example is the nor operator (!): (x ! y) is (~ (x + y)).

 We will use ACL2s to define a little compiler that compiles arbitrary
 formulas into formulas using only ! and we will formalize that this
 compilation step preserves the semantics of formulas.

|#

; This is similar to the definitions in homework 4. 
(defdata PropEx 
  (oneof boolean 
         var 
         (list '~ PropEx)
         (list PropEx (enum '(& + => = <> !)) PropEx)))

; An assignment is an alist for vars to booleans
(defdata assignment (alistof var boolean))

; This function, similar to the one from lab03, looks up the value of
; variable v in assignment a, returning nil if v is not in a.
(definec lookup (v :var a :assignment) :bool
  (cond ((endp a) nil)
        ((equal (caar a) v)
         (cdar a))
        (t (lookup v (cdr a)))))

; This function evaluates a PropEx given an assignment.
; Notice the similarity with aeval from lab03.
; The declare/etc forms are there just to speed up acceptance by ACL2s.
(definec peval (p :propex a :assignment) :bool
  (declare (xargs :termination-method :measure
                  :measure (acl2-count p)))
  :skip-tests t
  (cond ((booleanp p) p)
        ((varp p) (lookup p a))
        ((equal (car p) '~)
         (not (peval (second p) a)))
        ((equal (second p) '&)
         (and (peval (first p) a) (peval (third p) a)))
        ((equal (second p) '+)
         (or (peval (first p) a) (peval (third p) a)))
        ((equal (second p) '=>)
         (implies (peval (first p) a) (peval (third p) a)))
        ((equal (second p) '=)
         (iff (peval (first p) a) (peval (third p) a)))
        ((equal (second p) '<>)
         (xor (peval (first p) a) (peval (third p) a)))
        (t (not (or (peval (first p) a) (peval (third p) a))))))

; Formulas using only constants, variables and !.
(defdata NOrEx
  (oneof boolean 
         var 
         (list NOrEx '! NOrEx)))

:program

; Define the following function, which given a propex, p, returns a
; norex. If the returned formula is q, then p=q should be valid. That
; is, the returned formula is equivalent to the input formula.
;
; Feel free to define any helper functions you need.
(definec PropEx-NorEx (p :propex) :norex
  ...)


; Write a property that characterizes the correctness of PropEx-NorEx.
; That is, formalize the claim that the formula returned by
; PropEx-NorEx is equivalent to its input formula.
(test? ...)