#|

CS 2800 Homework 5 - Fall 2019

This homework is done in groups: instructions as per homework 02.

For this homework you will use ACL2s.

Technical and programming instructions: as per previous homeworks,
but change file names appropriately.

Additional instructions: 
We use the following ASCII character combinations to represent the Boolean
connectives:

  NOT     ~

  AND     &
  OR      +

  IMPLIES =>

  EQUIV   <=>
  XOR     ><  

|#


#|

PART I: PROPOSITIONAL LOGIC BASICS

A. Construct the truth table for each of the following Boolean formulas. 
   Use alphabetical order for the variables in the formula, and create
   columns for all variables occurring in the formula AND for all
   intermediate subexpressions. For example, if your formula is

   (p => q) + r

   your table should have 5 columns: for p, q, r, p => q, and (p => q) + r .

For each formula, you also have to:

B. Indicate if is satisfiable, unsatisfiable, valid, or
   falsifiable (exactly two of these characterizations will hold!).

C. Indicate how many assignments satisfy the formula (i.e., make the formula true).

D. Give another (different) formula which is equivalent to this formula.

E. Write an ACL2s thm stating that the original formula and the different
   formula that you provided in D are equivalent.
   This should *not* be in a comment. Here we want ACL2s code.
   Make sure your thm satisfies its contracts!
   In particular we want to assume that we are dealing with Boolean variables.
   
Example: p & (q + ~q)
|#
;; ANSWER:
"
A: (Notice that we place T's and F's under the operator associated with the
   column, e.g., in the final column, we are taking a conjunction.)

p | q | ~q | q + ~q | p & (q + ~q)
-----------------------------
T | T | F  |   T    |   T
T | F | T  |   T    |   T
F | T | F  |   T    |   F
F | F | T  |   T    |   F

B: satisfiable and falsifiable

C: 2

D: p 

E:
"
(thm (implies (and (booleanp p)
                   (booleanp q))
              (equal (and p (or q (not q)))
                     p)))

#|
5.1.: x => (y => x)
|#
;; ANSWER:
"
A:
...

B: ...

C: ...

D: ...

E
"
(thm ...

#|
5.2.: x => (y => z)
|#
;; ANSWER:
"
...
"
...

#|
5.3.: (x => y) => z
|#
;; ANSWER:
"
...
"
...

#|
5.4.: (p => (q & r)) & (r => ~q)
|#
;; ANSWER:
"
...
"
...


#|
PART II: IMPLEMENTING BOOLEAN FORMULAS IN ACL2S

Next, we will implement Boolean formulas in ACL2s and play with them.
We will first define a set of constants representing our Boolean operators:
|#

(defconst *not* '~)
(defconst *and* '&)
(defconst *or* '+)
(defconst *implies* '=>)
(defconst *iff* '<=>)
(defconst *xor* '><)

#|
Next, we define the grammar of our Boolean formulas as a data type:
|#

(defdata UnaryOp *not*)
(defdata BinaryOp (enum (list *and* *or* *implies* *iff* *xor*)))
(defdata Formula (oneof boolean 
                        var
                        (list UnaryOp Formula)
                        (list Formula BinaryOp Formula)))

; here's some examples of valid and invalid formulas:
(check= (Formulap '(x & y)) t)
(check= (Formulap '((~ x) & y)) t)
(check= (Formulap '((~ x) <=> (y >< z))) t)
(check= (Formulap '(~x)) nil)
(check= (Formulap '(~ x)) t)


#|
5.5. 
Write all 8 formulas from Part I in ACL2s using the syntax defined above.
These 8 formulas include the 4 formulas given, and the 4 formulas you came
up with in parts D of your answers. Make sure your formulas satisfy the Formulap
recognizer (use check= to ensure that):
|#

(check= (Formulap ...) t)
(check= (Formulap ...) t)
(check= (Formulap ...) t)
(check= (Formulap ...) t)
(check= (Formulap ...) t)
(check= (Formulap ...) t)
(check= (Formulap ...) t)
(check= (Formulap ...) t)


;; In what follows, we will use the function "in" which checks whether
;; a given element belongs to a given list:
(in 1 '(1 2))
(in 10 '(1 2))

#|
We will define a function rm-duplicates that removes duplicates from a list:
|#

(definec rm-duplicates (l :tl) :tl
  (cond
   ((endp l) nil)
   ((in (first l) (rest l)) (rm-duplicates (rest l)))
   (t (cons (first l) (rm-duplicates (rest l))))))

(check= (rm-duplicates '(1 2 3 1)) '(2 3 1))
(check= (rm-duplicates '(1 2 2 2 3 2 2 2 4)) '(1 3 2 4))
(check= (rm-duplicates '(1 2 2 2 3)) '(1 2 3))
(check= (rm-duplicates '(1 2 3)) '(1 2 3))
(check= (rm-duplicates nil) nil)


#|
We also define the following data types:
|#
(defdata lvar (listof var))
(defdata lform (listof Formula))
(defdata lstring (listof string))


#|
5.6.
Define the function formula-vars which takes as input
a Formula f and returns a lvar representing the set of
all variables appearing in f. Notice that the returned
list must be a set, meaning that duplicate elements
are not allowed. That is, each var appearing in the formula
must appear only once in the list of vars.

Hint: you can use a helper function and you can also use
the function rm-duplicates defined above.
|#

;; you may need these directives:
; (set-defunc-termination-strictp nil)
; (set-defunc-function-contract-strictp nil)
; (set-defunc-body-contracts-strictp nil)

;; ANSWER:
...

#|
5.7.
Define the function subformulas which takes as input
a Formula f and returns an lform representing the set
of all subformulas of f. Notice that the returned
list must be a set, meaning that duplicate elements
are again not allowed. However, don't try to remove
equivalent but syntactically different formulas.
For example, in the formula '((p & q) & (q & p)),
the subformulas '(p & q) and '(q & p) are syntactically
different and although they are equivalent, they can be
both included in the set of subformulas. But in the
formula '((p & q) & (p & q)) the subformula '(p & q)
should only appear once in the list of subformulas.

Your function should _not_ include constants in the
list of subformulas. For example, if the formula
is '(x & t) then 't should not be in the list of
subformulas.

Hint: again you can use a helper function and use
the function rm-duplicates defined above.
|#

;; ANSWER:
...

#|
5.8.
Does the function subformulas that you defined above
ensure that all variables of the given formula appear
first in the list of subformulas? If yes, all you have
to do for this problem is:
(definec subformulas-v2 (f :Formula) :lform
  (subformulas f))
  
Otherwise, you have to define the function subformulas-v2
such that it satisfies the property above. For example,
the list of subformulas for '((p & q) & (q & p)) should
start with '(p q ...) or '(q p ...). Remember that there
must be no duplicates. 

Hint: there is an easier and a harder way to do this.
The easier way is to exploit the fact that you already
have a function that returns the list of variables
of a formula, and that every variable is also a subformula.
|#

;; ANSWER:
...

;; For the problems below, the following string functions are useful:
;; The function string converts symbols (including booleans and vars)
;; to strings:
(string 't)
(string 'hello)
(string 'x)

;; The function string-append appends two strings:
(string-append "xyz" "abc")

#|
5.9.
Define a function formula-to-string which takes a Formula
and returns the same formula in string form. For example,
if the formula is '(p & q) the function should return
"(p & q)". 
|#

;; ANSWER:
...

#|
We want to enumerate all assignments for a given formula.
Towards this goal, we define the data type "assignment" 
which represents an assignment as a list of pairs (var, boolean).
|#
(defdata assignment (alistof var boolean))

(check= (assignmentp '((x . t) (y . nil))) t)

;; we also define a list of assignments:
(defdata loa (listof assignment))

#|
5.10.
Now, given a Formula f, we want to generate the list of
_all possible_ assignments over the variables of f.
Note that we don't want just the assignments that make f
true. We want all possible assignments. For example,
if f has 2 variables, we want a list of 4 assignments,
if f has 3 variables, a list of 8 assignments, etc.
The order of the assignments does not matter.
The order of variables in an assignments does not
matter either. But all assignments and all variables
must be present.

Call the function "all-assignments":
|#
;; ANSWER:
...


#|
5.11.
Test using examples (check=) the property that
"if f has N propositional variables, then (all-assignments f)
has 2^N elements if N>0 and 0 elements if N=0".
You can reuse some or all of the formulas that you wrote earlier
or come up with new formulas. Write at least 5 different checks.
|#
;; ANSWER:
...


#|
5.12.
Test using test? or prove using thm (or both) the property that
"if f has N propositional variables, then (all-assignments f)
has 2^N elements if N>0 and 0 elements if N=0".
|#
;; ANSWER:
...


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;  Feedback (5 points)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
#|
Each we'll take a short survey to monitor homework difficulty and to solicit feedback.

This survey is anonymous. We don't collect names, emails, etc. Each student responds individually. 
If you answer all mandatory questions, you get 5 points for this homework set. 
You report who among your team answered the survey in your homework answers, and we trust you 
that you reported this truthfully. 

Please fill out the following form (one response per team member):

https://docs.google.com/forms/d/e/1FAIpQLSfadRMb-hUGhhJNYgaUyAHpZZRCe_HUZfMTaNIgvJTQoLToAQ/viewform?usp=sf_link

Report here who in your team filled the form:

The following team members filled out the feedback survey provided by
the link above (replace the ...'s with the names of the team members
who filled out the questionnaire).

<Firstname> <LastName>
...
...
...
|#