#|
CS 2800 Homework 3 - Spring 2013

For this homework, you will be using the BEGINNER mode in ACL2s.

Instructions for using this file:

- open this file in ACL2s as hw03.lisp

- set the session mode to "Beginner"

- insert your solutions into this file where indicated (for instance as
"..."). This includes contracts, the body of the function, and test cases.
Make sure you provide as many test cases as required (in addition to the
ones already provided, of course).

- do not comment in or comment out any existing function definitions from
this file. Also, do not change the order of any function definitions,
whether provided by us or defined by you.

- make sure the entire file is admitted by ACL2s in Beginner mode. This means:
  * there must be no "..." in the code. If you don't finish some problems,
    comment them out. The same is true for any English text that you may
    add. This file already contains many comments, so you can see what the
    syntax is.
  * all check= tests must be satisfied. If any of the provided tests fail,
    your function definition is wrong, and the file will not be admitted.
    If any of your own tests fail, it may be your function is wrong, but
    it may also be that your check= specification is incorrect.

  Sometimes it may take a while for your function to be admitted. Be
  patient: rest assured that, if you function is correct, the process will
  succeed. If you don't get a success message after 2-3 mins (depending on
  your hardware), then probably your definition is too complicated or
  wrong.

- save the file with your additions and turn it in. To do that, check out
the directory at

  svn://dell-server-wahl-1.ccs.neu.edu/cs2800-2013-spring/03/<groupname>

  where groupname is the name of the group as it was emailed to you. Your
  username and password remain as before.

  Place your file hw03.lisp in this directory, add it, and commit. Do NOT
  submit the session file (ending in .a2s).

======================================================================

- for non-programming problems, include solutions as comments. We will use
F and T to represent false and true, and the following character
combinations to represent the Boolean connectives:

  NOT        ~

  AND        /\
  OR         \/

  IMPLIES    =>

  EQUIVALENT =
  XOR        <>

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

|#
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Truth tables
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
#| 

Construct the truth table for the following Boolean formulas. Make your
truth table canonical, i.e.: sort columns for variables by alphabet, and
sort rows from T T T T ... to F F F F.

 a) (p => r) /\ (q => r) /\ (~p => ~r)










 

 b) (p <> q) <> r












 c) (p => q) = (~q => ~p)








 d) p /\ (p \/ q) = ~p









;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Simplification of Formulas.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Simplify the following formulas, i.e. find the simplest formula that is
logically equivalent to the given formula. "Simplest" means: with the least
number of connectives; parentheses have no bearing. For example, the
formula

   (p \/ (p => q))

is valid. The simplest equivalent formula is therefore T. Note that ~
counts as a connective, so ~(a /\ b) is simpler than ~a \/ ~b . On the
other hand, there may be several solutions that can be viewed as
"simplest", e.g., a \/ b and b \/ a are both "simplest".

You can use any unary or binary connective we introduced in the
class. Please use the notation for connectives introduced above.

1.  ~(p \/ (~p/\ q))







2. (p \/ q) /\ (( p/\r) \/ (p /\ ~r) \/ (p /\ q)  \/ q)











3. ( p /\ ( ~p \/ q)) \/ ((p \/ ~q) /\ q)











4. (~p /\ ( p \/ q)) \/ ((q \/ ( p /\ p)) /\ ( p \/ ~q))


















|#

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Programming
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; The following is a data definition for the type, "list of natural
; numbers". It automatically gives rise to a recognizer for this type
; called natlistp : All -> Boolean, which you are free to use.

(defdata natlist (listof nat))

; Define 
; sum-of-list : Natlist -> Nat
;
; (sum-of-list l) returns the sum of all natural numbers in the list
; Write at least 3 more checks
(defunc sum-of-list (l)
  :input-contract ... 
  :output-contract ... 


 
...)

(check= (sum-of-list nil) 0)
(check= (sum-of-list '( 1 2 3)) 6)

;Define
; insert Nat x Natlist -> Natlist
;
; (insert n l) inserts a natural number n in the list of numbers l
; before the first element in l which is >= (greater than or
; equal to) n , or at the end of l if no such element exists.
; Write at least 3 more checks
(defunc insert (n l)
  :input-contract ...
  :output-contract ...





  ...)

(check= (insert 1 '( 2 3 4)) '( 1 2 3 4))
(check= (insert 1 nil) '( 1))
(check= (insert 4 '( 3 2 5)) '( 3 2 4 5))

;Define    
; del-el : Nat x Natlist -> Natlist
;
; (del-el n l) removes the first occurrence of n in l, if any.
; Write at least 3 more checks
(defunc del-el (n l)
  :input-contract ...
  :output-contract ...





... )

(check= (del-el 1 '( 1 1 4)) '( 1  4))
(check= (del-el 1 nil) nil)
(check= (del-el 4 '( 3 2 5)) '( 3 2 5))

;Define 
; scale-natlist : Nat x Natlist -> Natlist
;
; (scale-natlist s l ) takes a list of natural numbers as input and
; scales it by the factor of s, i.e. each element is multiplied by s.
; Write at least 3 more checks
(defunc scale-natlist (s l)
  :input-contract ...
  :output-contract ...



...)
(check= (scale-natlist 3 '( 1 2 3)) '( 3 6 9))
(check= (scale-natlist 3 nil) nil)
(check= (scale-natlist 0 '( 1 2 3)) '( 0 0 0))

;Define
; find-least-aux : Natlist x Nat -> Nat
;
; find-least-aux takes a list of natural numbers l and a and returns
; the least element of l if that is less than a, otherwise a.
; Write at least 3 more checks
(defunc find-least-aux (l a)
  :input-contract ...
  :output-contract ...





...)

(check= (find-least-aux '( 1 2 3) 2) 1)
(check= (find-least-aux '( 3 2 1) 2) 1)
(check= (find-least-aux nil 1) 1)

;Define
; find-least : Natlist -> Nat
;
; (find-least l) takes a Natlist and returns its least element; 0 if empty.
; Write at least 3 more checks
(defunc find-least (l)
  :input-contract ...
  :output-contract ...



...  )

(check= (find-least '( 1 2 3)) 1)
(check= (find-least '( 1 5 2 7 3)) 1)
(check= (find-least nil) 0)

; Define
; rem-rep-list : Natlist -> Natlist
;
; (rem-rep-list l) replaces repeated occurrences of a number
; in the Natlist l by a single occurrence.
; Write at least three checks
(defunc rem-rep-list (l)
  :input-contract ...
  :output-contract ...







)

(check= (rem-rep-list '( 1 2 3 4)) '( 1 2 3 4))
(check= (rem-rep-list '( 1 1 3 4)) '( 1 3 4))
(check= (rem-rep-list '( 1 3 1 4)) '( 1 3 1 4))
...
...


; Below we will use the above functions to calculate your grade.
; grades are calculated as on the course webpage

; Define
; get-best-three-exams : Nat x Natlist -> Natlist
;
; (get-best-three-exams fe lex) takes a natural number fe (= final exam
; score), and a Natlist (= list of other exam scores)
; and returns a Natlist (= best three exams).
; Hint : Use find-least and del-el functions 
; Write at least 3 checks
(defunc get-best-three-exams (fe lex)
  :input-contract ...
  :output-contract ...



...)


; Define
; sum-of-exams : Natlist -> nat
;
; (sum-of-exams l3ex) takes a Natlist (list of exams points) and returns their sum
; Hint : This is a non-recursive definition
(defunc sum-of-exams (l3ex)
  :input-contract ...
  :output-contract ...

...)

;; The following (Begin ... End) is required to help ACL2 admit some of
;; your functions below. Do not modify or remove this part.
;; Begin
(acl2::in-theory (acl2::disable get-best-three-exams get-best-three-exams-definition-rule
                    sum-of-exams-definition-rule
                    sum-of-list-definition-rule))

(defthm lemma-x
  (implies (and (natp fe)
                (natlistp lex))
           (natp (sum-of-exams (get-best-three-exams fe lex))))
  :rule-classes (:rewrite :forward-chaining))

(acl2::in-theory (acl2::disable natp))
;;; End

; Define 
; total-exp-points : Natlist x Natlist x Natlist x Natlist x nat -> nat
;
; (total-exp-points lhw lq llab lex fe) takes four Natlist and a natural number as input
; lhw : list of homework experience points
; lq : list of quizzes experience points
; llab : list of lab experience points
; lex : list of exams experience points (minus the final exam)
; fe : final exam experience points
; Returns the total experience points, according to the syllabus rules.
; That is, all points in the different category are added up, except exams,
; where only the 3 largest scores count.
; Write at least 3 checks
; Hint : this is a non-recursive definition. Use the functions defined above.
(defunc total-exp-points (lhw lq llab lex fe)
  :input-contract ...
  :output-contract ...





...)


(defdata grades (oneof 'a 'a- 'b+ 'b 'b- 'c+ 'c 'c- 'd+ 'd 'd-))

;Define 
; what-is-my-grade : Natlist x Natlist x Natlist x Natlist x nat -> grade

;(what-is-my-grade lhw lq llab lex fe)
; lhw : list of homework experience points
; lq : list of quizzes experience points
; llab : list of lab experience points
; lex : list of exams experience points (minus the final exam)
; fe : final exam experience points
; Returns the final grade
; Write at least 3  checks
(defunc what-is-my-grade (lhw lq llab lex fe)
  :input-contract ...
  :output-contract ...























...)

; We now define a data type containing two function symbols: 'insert and 'del-el
(defdata fn-sym (oneof 'insert 'del-el))

; An "s-expr" is an expression formed according to the following rules.
; Every natlist is an s-expr. If e is an s-expr, n is a natural number and
; f is a function symbol according to the above data definition, then
; (e n f) is an s-expr. The idea is that the expression stands for the
; application of the function f to the s-expr e and the constant n. The
; expression is given in post-fix, i.e. the operation (function f) is
; appears last.

(defdata s-expr (oneof Natlist (list s-expr nat fn-sym)))

(check= (s-exprp '( 1 2)) t)
(check= (s-exprp 1) nil)
(check= (s-exprp '(( 1 2) 3 insert)) t)
(check= (s-exprp '(( 1 2) 3 del-el)) t)
(check= (s-exprp '((( 1 2) 1 del-el) 3 insert)) t)
(check= (s-exprp '((( 1 2) 1 del-el) ( 4 5))) nil)

; Write 5 examples of valid s-expr and check 
(check= (s-expr ...) t)
(check= (s-expr ...) t)
(check= (s-expr ...) t)
(check= (s-expr ...) t)
(check= (s-expr ...) t)

;Define
; count-num-fn-sym : s-expr -> Nat
;
; (count-num-fn-sym s) takes s-expr as input and returns the number of
; function symbols in the expression
; Write at least 3 more checks
(defunc count-num-fn-sym (s)
  :input-contract ...
  :output-contract ...



 ...)

(check= (count-num-fn-sym '( 1 2)) 0)
(check= (count-num-fn-sym '(( 1 2) 3 insert)) 1)
(check= (count-num-fn-sym '((( 1 2) 1 del-el) 3 insert)) 2)

;Define 
; count-constants (s) : s-expr -> Nat
;
; (count-constants s) takes s-expr as input and returns number of
; constants (natural number) in the s-expr
; Write at least 3 more checks
(defunc count-constants (s)
  :input-contract ...
  :output-contract ...



...)

(check= (count-constants '(1 2)) 2)
(check= (count-constants '((1 2) 3 insert)) 3)
(check= (count-constants '((( 1 2) 1 del-el) 3 insert)) 4)

;Define 
; scale-expr : s-expr x Nat -> s-expr
; 
; (scale-expr s n) takes as input an s-expr s and scaling factor n and
; multiplies each constant element in the expression by s.
; Hint: use the scale-natlist function from above.
; Write at least 3 more checks                    
(defunc scale-expr (s n)
  :input-contract ...
  :output-contract ...




...)

(check= (scale-expr '( 1 2) 3) '( 3 6))
(check= (scale-expr '((1 2) 3 insert) 4) '((4 8) 12 insert))
(check= (scale-expr '((( 1 2) 1 del-el) 3 insert) 3) 
        '(((3 6) 3 del-el) 9 insert))

;Define
; evaluate-expr : s-exprp -> Natlist
;
; (evaluate-expr s) takes as input s-expr s and applies the function
; symbol to its argument. If function symbol is 'insert then it
; inserts the element in the Natlist. If the function symbol is
; 'del-el then it deletes the element from the Natlist if it exists.
; Write at least 3 more checks
(defunc evaluate-expr (s)
  :input-contract ...
  :output-contract ...






...)

(check= (evaluate-expr '( 1 2)) '( 1 2))
(check= (evaluate-expr '(( 1 2) 3 insert)) '(1 2 3))
(check= (evaluate-expr '((( 1 2) 1 del-el) 3 insert)) '( 2 3))

; Above we represented expression in postfix format. Now consider
; prefix and infix representation.

; prefix representation
(defdata s-prefix (oneof Natlist (list fn-sym nat s-prefix)))

; Define
; convert-to-prefix : s-expr -> s-prefix
;
; (convert-to-prefix s) takes as input an s-expr in post-fix
; representation and returns the prefix representation of the
; expression
; Write at least 3 more checks
(defunc convert-to-prefix (s)
  :input-contract ...
  :output-contract ...






...)

(check= (convert-to-prefix '(1 2)) '( 1 2))
(check= (convert-to-prefix '((1 2) 3 insert)) '(insert 3 ( 1 2)))
(check= (convert-to-prefix '(((1 2) 1 del-el) 3 insert)) 
        '(insert 3 (del-el 1 ( 1 2))))


(defdata s-infix (oneof Natlist (list nat fn-sym s-infix)))

; Define
; convert-to-infix : s-expr -> s-infix
;
; (convert-to-infix s) takes as input an s-expr in post-fix
; representation and returns the infix representation of the
; expression
; Write at least 3 more checks
(defunc convert-to-infix (s)
  :input-contract ...
  :output-contract ...






...)

(check= (convert-to-infix '(1 2)) '( 1 2))
(check= (convert-to-infix '(( 1 2) 3 insert)) '(3 insert ( 1 2)))
(check= (convert-to-infix '((( 1 2) 1 del-el) 3 insert)) 
        '( 3 insert (1 del-el ( 1 2))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Feedback
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

#|

Please fill out the following feedback form, not as a team, but each team
member individually:

https://docs.google.com/spreadsheet/viewform?formkey=dHhYUExJWm5JeHZGRy13NWFMa1k2RVE6MA


Confirm here whom of the team members filled out the form:

Name 1 ...
Name 2 ...
(Name 3 ...)

Everyone who filled out the form gets credit worth 1 quiz.

The form is anonymous, to encourage you to write what you think about this
class. (If you want to stay anonymous, do not reveal your name on the
feedback form.) On the other hand, we must rely on your honesty in stating
whether you filled out the form or not, and in NOT filling out the form
several times (why would you do that??). We do not want to find
discrepancies in the number of entries on the form, and the number of
people claiming to have filled out the form.

|#