#|

CS 2800 Homework 4 - Fall 2019

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


For this homework you will use ACL2s.

Technical instructions: as per homework 02, but change file names appropriately.

Additional instructions for this and future homeworks:
There will be a -20pts penalty for invalid ACL2s code.
By "invalid" we mean code that's not accepted by ACL2s: ACL2s does not
"go green". Notice that sometimes ACL2s cannot prove something although
that "something" is perfectly correct. We have discussed what to do in
cases like that. You have several options: use the non-strict directives,
go to :program mode, and ultimately put your answer in comments. We will
still look at your answer and give you full credit if it's correct.
But please do not upload your file until you make sure it is
_fully accepted_ by ACL2s! We have had several cases of sloppy code,
with wrong number of arguments, missing parentheses, etc. This will
not be tolerated.

Instructions for programming problems: as per homework 02.

Additional instructions: Whenever you write properties that are tested with
test? or proven with thm, make sure your properties pass contract checking!!!

|#

#|
4.1.
Define a data type two-lists for a pair of two true lists:
|#
;; ANSWER:
(defdata ...

#|
4.2.
Provide at least 5 different elements which are of type two-lists,
and 5 different elements which are not of type two-lists. Use the
regognizer automatically generated from your defdata definition above
to express these positive and negative examples:
|#
;; ANSWER:
...

#|
4.3.
Define a function shuffle which takes as input a two-lists, shuffles
the two lists, and returns their shuffling as a result. Some tests
are given below:
|#
;; ANSWER:
(definec ...

(check= (shuffle '((1 2 3) nil)) '(1 2 3))
(check= (shuffle '(nil (1 2 3))) '(1 2 3))
(check= (shuffle '((1 2 3) (a b))) '(1 a 2 b 3))

#|
4.4.
Let (x,y) be the pair of lists passed to shuffle as input,
and let z be the resulting list output by shuffle. Let |l|
denote the length of list l. It should be the case that
             |z| = |x| + |y|
State this property in ACL2s syntax, as a property of the
function shuffle. Notice that you should not use z
in your statement, but the application of function shuffle
to its input. Similarly, you should use a single variable
for the input of shuffle, instead of x,y. For example,
if you were writing the property of app (append), namely
that the length of its output is equal to the sum of the
lengths of its inputs, you would write:
(equal (len (app x y)) (+ (len x) (len y)))
or better (performing contract checking):
(implies (and (tlp x) (tlp y))
         (equal (len (app x y)) (+ (len x) (len y))))
|#
;; ANSWER:
"
... replace with your answer here (don't remove the quotes) ...
"               


#|
4.5.
Use test? to test your property.
Make sure your property passes contract checking!
|#
;; ANSWER:
(test?
  ...
)

#|
4.6.
Can you use thm instead of test? to prove your property
using ACL2s? If yes, write this (thm ...) form in your
answer below.

If ACL2s cannot prove the above (thm ...) form, then
do the following: 
A. Define a function shuffle-aux which takes as input
two true lists and shuffles them. That is, the difference
between shuffle and shuffle-aux is that the former takes
as input a two-lists object, while the latter takes as
inputs two true lists.
B. Express the same property as a property of shuffle-aux,
instead of as a property of shuffle. Can you use ACL2s
(thm ...) to prove this new property? If yes, do so. If
not, test it with test? :
|#
;; ANSWER:
...



#|
4.7.
 Define using definec the function list-insert, which consumes
 a true list l, a number i, and some element a, and adds a to the i-th position
 in the list (assuming the positions start at 0). 
 
 i must be a number between 0 and the length of l. If this is not the case,
 your function should return nil (the empty list). Note that you don't need
 to enforce the condition 0 <= i <= (len l) in the input contract. Again,
 for this problem use definec.
 
 Can list-insert deal with l being the empty list? Can i be equal
 to the length of l? Can it be larger? Add the corresponding tests and more!

 You can only use cons, equal, rest, first, len, arithmetic, ...,
 recognizers, boolean operators, but nothing else. 
|#

;; ANSWER:
(definec ...


#|
4.8.
 Define the property that holds between the length of the input list l of
 list-insert, and the length of the output list that the function returns,
 assuming that the input index i is between 0 <= i <= (len l). This
 assumption should figure explicitly in the property.
 
 Test this property using test? and try to prove it if possible using thm.
 You will not lose any points if you cannot prove it using thm.
|#

;; ANSWER:
...

#|
4.9.
Now modify the above property to cover the case also where i > (len l).
That is, the new property should only assume that i is a nat, but not that
it is <= (len l).

Test your new property using test? and try to prove it if possible using thm.
 You will not lose any points if you cannot prove it using thm.
|#

;; ANSWER:
...

#|
4.10.
 Now define a modified version of your previous function, called
 list-insert-v2. This new version has stronger input contracts.
 In particular, it does not allow i to exceed the length of l. 

 You may have to use defunc instead of definec.
|#

;; ANSWER
...

#|
4.11.
 Now rewrite the property that you wrote in 4.8 for list-insert-v2.
 As before, test it using test? and try to prove it using thm.
 You will not lose points if you cannot prove it with thm.
|#

;; ANSWER
...

#|
4.12.
 Does the property that you wrote in 4.9 make sense for list-insert-v2?
 If yes, rewrite it for list-insert-v2. If not, explain why not.
|#

;; ANSWER
"
...
"


;; We define a list of rationals:
(defdata lor (listof rational))

#|
4.13.
Define a function decreasingp which takes as input a list of rationals
and returns t if the list is strictly decreasing and nil otherwise:
|#


;; ANSWER:
...

(check= (decreasingp '(1 1 3/2 8/5)) nil)
(check= (decreasingp '(1 1/2 1/10)) t)
(check= (decreasingp nil) t)



#|
4.14.
Define a function prefix which takes as input a list of rationals l
and a nat n, and returns the prefix of length n of l, that is, the list
containing the first n elements of l. If n is >(len l) then prefix
returns the entire list l.
|#

;; ANSWER:
...

(check= (prefix '(1 1 3/2 8/5) 3) '(1 1 3/2))



#|
4.15.
State in ACL2s the property that "every prefix of a decreasing lor
is a decreasing lor". Test your property using test? and try to
prove it with thm. No points will be taken off if thm fails to
prove it.
|#

;; 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/1FAIpQLSfDxLCY9Ul68h_kq6WKbroRwugdYz_wl8MNwhEom8aBrQXzpw/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>
...
...
...
|#