; ****************** BEGIN INITIALIZATION FOR ACL2s MODE ****************** ; ; (Nothing to see here! Your actual file is after this initialization code); #+acl2s-startup (er-progn (assign fmt-error-msg "Problem loading the CCG book.~%") (value :invisible)) (include-book "acl2s/ccg/ccg" :uncertified-okp nil :dir :system :ttags ((:ccg)) :load-compiled-file nil);v4.0 change ;Common base theory for all modes. #+acl2s-startup (er-progn (assign fmt-error-msg "Problem loading ACL2s base theory book.~%") (value :invisible)) (include-book "acl2s/base-theory" :dir :system :ttags :all) #+acl2s-startup (er-progn (assign fmt-error-msg "Problem loading ACL2s customizations book.~%Please choose \"Recertify ACL2s system books\" under the ACL2s menu and retry after successful recertification.") (value :invisible)) (include-book "custom" :dir :acl2s-modes :ttags :all) #+acl2s-startup (er-progn (assign fmt-error-msg "Problem setting up ACL2s mode.") (value :invisible)) ;Settings common to all ACL2s modes (acl2s-common-settings) ;(acl2::xdoc acl2s::defunc) ;; 3 seconds is too much time to spare -- commenting out [2015-02-01 Sun] (acl2::xdoc acl2s::defunc) ; almost 3 seconds ; Non-events: ;(set-guard-checking :none) (acl2::in-package "ACL2S") ; ******************* END INITIALIZATION FOR ACL2s MODE ******************* ; ;$ACL2s-SMode$;ACL2s #| CS 2800 Homework 11 - Summer 2018 This homework is to be done by INDIVIDUALLY and is designed to be done under exam conditions. * The main section of the homework is designed to be taken under exam conditions and over a 2 hour period. As such it would be a great idea for you to solve the problems using pen and paper and THEN type your answers in this file later Extra work but you want to feel comfortable taking the exam with a pen/pencil to match test conditions (look up State Dependent Learning if you want to know why). * Obviously I didn't time the duration of this homework. The time required is an estimate. Don't panic if you take 2 hours and 10 minutes to complete. Don't relax if it takes you 40 minutes either. :) * The extra questions at the end of the exam are there for extra practice. They aren't worth points but a 2 hour exam didn't seem like it gave sufficient practice for a review. Submitting: * Submit the homework file (this file) on Blackboard. Do not rename this file. There will be a 10 point penalty for this. |# ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ; Section A: Admissibility, Measure Functions and Induction Schemes ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; #| First, let's review the conditions necessary for a function to be admitted in ACL2s (I'm paraphrasing below): 1) The function f is a new function symbol 2) The input variables are distinct variable symbols 3) The body of the function is a well formed term, possibly using a recursive call to f and mentioning no variables freely (ie only the input variables) 4) The function is terminating 5) IC=>OC is a theorem 6) The body contract holds under the assumption that the IC holds (ie there isn't a body contract violation if the input contract is true) OK. Now onto the questions. For each function fn below (f1...f4), determine if the function fn is admissible: If fn is admissible: 1) provide a measure function mn that can be used to prove it terminates 2) Write the proof obligations for fn using mn that can show it terminates. 3) Convince yourself that the function terminates (no need for a formal proof but good practice later) 4) Write the induction scheme that fn gives rise to. If fn is NOT admissible, give your justification as to why (conditions 1-6 above). 1) If the problem is syntactic (admissibility conditions 1-3) then tell us what part of the function has a problem. 2) If the issue is with conditions 4-6, then give an input that will illustrate the violation. |# #| A1. (defunc f1 (x y flag) :input-contract (and (listp x) (listp y) (booleanp flag)) :output-contract (listp (f1 x y flag)) (cond ((and flag (endp x)) y) ((and (not flag) (endp y)) x) (flag (cons (first x)(f1 (rest x) y flag))) (t (f1 (cons (first y) x) (rest y) flag)))) ##.............. |# #| (defunc f2 (x y) :input-contract (and (listp x)(listp y)) :output-contract (listp (f2 x y)) (cond ((equal (len x)(len y)) (app x y)) ((< (len x)(len y)) (cons (first y)(f2 x (rest y)))) (t (f2 x (app y (list x)))))) ##.............. |# #| A3. ;; Assume f3a is admissible....we will see it again soon. (defunc f3a (l flag) :input-contract (and (listp l)(booleanp flag)) :output-contract (listp (f3a l flag)) (cond ((endp l) l) (flag (f3a (rest l) (not flag))) (t (cons (first l)(f3a (rest l)(not flag)))))) ;; You can prove this for practice (defthm phi_f3a (implies (and (listp l)(consp l))(< (len (f3a l)) (len l)))) (defunc f3 (x) :input-contract (listp x) :output-contract (listp (f3 x)) (cond ((endp x) x) ((endp (rest x)) x) (t (app (f3 (f3a x t)) (f3 (f3a x nil)))))) ##.............. JUST f3 |# #| A4. (defunc f4 (l1 l2) :input-contract (and (lonp l1) (lonp l2)) :output-contract (listp (f4 l1 l2)) (cond ((endp l1) (list 1 2)) ((endp l2) (f4 (cons 5 l1) (list 5))) ((> (len l2) (len l1)) (f4 l2 (list l1))) (t (f4 (rest l1) (rest l2))))) ##.............. |# #| ;;;;;;;;;;;;;;;;;;;;;;;; SECTION 2: half-list Look at f3a.....it should actually be called half-list since it removes half the elements from the list. The flag changes which half of the elements are removed. |# (defunc half-list (l flag) :input-contract (and (listp l)(booleanp flag)) :output-contract (listp (half-list l flag)) (cond ((endp l) l) (flag (half-list (rest l) (not flag))) (t (cons (first l)(half-list (rest l)(not flag)))))) #| If you look carefully, however, you may notice that phi_half_perm (listp l)/\(booleanp flag) => (perm l (app (half-list l flag)(half-list l (not flag)))) OK. Time to prove this. Identify the Induction Scheme you will use and the function that gives rise to it. #......# Now "prove" phi_half_perm. You can ignore non-recursive proof obligations (hence the quotes around the word prove). You can use any theorems that we've discussed in the past or assumed in homeworks.....and since I can't catch you doing it, you can look at previous homeworks. This will help you build your "cheat sheet" #......# OPTIONAL FOR NO MARKS (this question only) If you want even MORE practice, take the function weave which we discussed in class: (defunc weave (l1 l2) :input-contract (and (listp l1)(listp l2)) :output-contract (listp (weave l1 l2)) (cond ((endp l1) l2) ((endp l2) l1) (t (cons (first l1)(cons (first l2)(weave (rest l1)(rest l2))))))) Prove (listp l) => (equal l (weave (half-list l nil)(half-list l t))) |# #| ;;;;;;;;;;;;;;;;;;;;;;;;; SECTION 3: half-list* NOTE: I'm worried that this question might be a bit too easy for an exam. Thus do not be shocked if the exam question is a bit harder. |# ;Define half-list-t ;half-list-t: list x boolean x list -> list ;(half-list-t l flag acc) removes elements in l if flag ; is true, otherwise it keeps the elements. ;#......# ; half-list* should be equivalent to half-list. Write a function ; half-list-t that is tail recursive and has an accumulator. (defunc half-list* (l flag) :input-contract (and (listp l)(booleanp flag)) :output-contract (listp (half-list* l flag)) (half-list-t l flag nil)) (test? (implies (and (listp l)(booleanp flag)) (equal (half-list l flag) (half-list* l flag)))) #| Write a lemma relating half-list-t, it's accumulator and half-list? This lemma should contain no constants and #......# Prove (listp l) /\ (booleanp flag) => (half-list* l flag) = (half-list l flag) #......# Now prove the lemma #......# #| *************** ---------EVERYTHING BELOW HERE IS OPTIONAL------------ EXTRA PRACTICE QUESTION (no marks) THEME: I Love the End of Term The end is fast approaching and although many of you might be concerned about the exam, I've regularly pointed out a key difference from the first half of the semester: you can make your own problems. The fact we can come up with properties related to a function, we can write tail recursive versions of a function and the fact we may need to prove a function is admissible (and thus terminates) means that any single function can spawn a slew of questions touching on all aspects of the course. Give it a try on your own...... ....or let's do that now. Take the functions ssort (for selection sort) and weave. We will keep revisiting these functions throughout the homework. First, let's define them and the functions necessary to use them. Note that I'm denoting all questions with ##.............. so you don't accidentally overlook one (you can do a search). Also note that many questions are "EXTRA" meaning they are worth no points and won't be graded. These are for you to potentially get more practice. The homework would be painfully long if we required you to prove all the questions. Hence keep an eye out for what is optional and what is not. *************** |# ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; GIVEN ;; del: Any x List -> List ;; (del e l) takes an element e and a list l ;; and removes the FIRST occurence of e from l ;; If e is not in l then l is returned. (defunc del (e l) :input-contract (listp l) :output-contract (listp (del e l)) (if (endp l) l (if (equal e (first l)) (rest l) (cons (first l) (del e (rest l)))))) ;; Ignore (sig del (all (listof :b)) => (listof :b)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; GIVEN ;; perm: List x List -> Boolean ;; (perm l1 l2) takes two lists (l1 and l2) and ;; returns true if and only if l1 and l2 have ;; the same elements (and the same number of each) ;; Essentially, is l2 a reordering of l1. (defunc perm (l1 l2) :input-contract (and (listp l1)(listp l2)) :output-contract (booleanp (perm l1 l2)) (if (equal l1 l2) t (if (endp l1) nil (and (in (first l1) l2) (perm (rest l1) (del (first l1) l2)))))) (defdata lor (listof rational)) (defdata lon (listof nat)) ;; min-l: LOR (non-empty -> Rational ;; (min-l l) returns the smallest element in l. (defunc min-l (l) :input-contract (and (lorp l)(consp l)) :output-contract (rationalp (min-l l)) (if (endp (rest l)) (first l) (let ((min (min-l (rest l)))) (if (< min (first l)) min (first l))))) ;;Keep to help ssort go in AFTER you add your lemmata from part A. ;; This is purely optional. (defthm phi_del_lorp (implies (lorp l)(lorp (del e l)))) ;; ssort: LOR -> LOR ;; (ssort l) sorts list l using the selection sort algorithm ;; This involves repeatedly finding the smallest element in the list ;; and putting it at the front of the list (or sublist) (defunc ssort (l) :input-contract (lorp l) :output-contract (lorp (ssort l)) (if (endp l) l (let ((min (min-l l))) (cons min (ssort (del min l)))))) ;; weave: list x List -> list ;; (weave x y) takes two lists and interweaves ;; them so the resultant list alternates between ;; an element from x and an element from y. (defunc weave (x y) :input-contract (and (listp x)(listp y)) :output-contract (listp (weave x y)) (cond ((endp x) y) ((endp y) x) (t (cons (first x) (cons (first y) (weave (rest x)(rest y))))))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ; Section A: Admissibility, Measure Functions and Induction Schemes ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; #| First, let's review the conditions necessary for a function to be admitted in ACL2s (I'm paraphrasing below): 1) The function f is a new function symbol 2) The input variables are distinct variable symbols 3) The body of the function is a well formed term, possibly using a recursive call to f and mentioning no variables freely (ie only the input variables) 4) The function is terminating 5) IC=>OC is a theorem 6) The body contract holds under the assumption that the IC holds (ie there isn't a body contract violation if the input contract is true) OK. Now onto the questions. Note that I'm denoting all questions with ##.............. so you don't accidentally overlook one (you can do a search). For each function fn below (f1...f5), determine if the function fn is admissible: If fn is admissible: 1) provide a measure function mn that can be used to prove it terminates 2) Write the proof obligations for fn using mn that can show it terminates. 3) Convince yourself that the function terminates (no need for a formal proof) 4) Write the induction scheme that fn gives rise to. If fn is NOT admissible, 1) Give your justification as to why (conditions 1-6 above). a) If the problem is syntactic (admissibility conditions 1-3) then tell us what part of the function has a problem. b) If the issue is with conditions 4-6, then give an input that will illustrate the violation. 2) Give the (invalid) induction scheme that fn gives rise to. |# #| A1. (defunc f1 (x y z) :input-contract (and (natp x) (natp y) (listp z)) :output-contract (natp (f1 x y z)) (cond ((< x 10) (* x y)) ((<= (len z) y) (* (len z) y)) ((> x (len z)) (+ x (f1 x y (rest z)))) (t (f1 (- x 10) y z)))) ##.............. |# #| ;; Remember, induction schemes rely on converting a function to an equivalent ;; cond statement (at least if you want to use the design pattern for creating an IS ;; given in the notes) (defunc f2 (x y) :input-contract (and (integerp x)(integerp y)) :output-contract (integerp (f2 x y)) (if (natp x) y (if (natp y) (if (<= (unary-- x) y) (f2 (+ x 1) y) (f2 x (- y 1))) x))) ##.............. |# ;; No need to consider the admissibility of evenp. Just f3 (defunc evenp (i) :input-contract (integerp i) :output-contract (booleanp (evenp i)) (integerp (/ i 2))) #| A3. (defunc f3 (x) :input-contract (lorp x) :output-contract (natp (f3 x)) (cond ((< (len x) 5) (f3 (cons 10 (app x x)))) ((evenp (len x)) (f3 (cons (* 2 (first x)) x))) (t (+ (len x) (first x))))) ##.............. |# #| A4. (defunc weave (x y) :input-contract (and (listp x)(listp y)) :output-contract (listp (weave x y)) (cond ((endp x) y) ((endp y) x) (t (cons (first x) (cons (first y) (weave (rest x)(rest y))))))) (Yes, we realize that weave is admissible. Give a measure, measure obligations and induction scheme just the same) ##.............. |# #| A5. (defunc f5 (l1 l2) :input-contract (and (lorp l1) (lonp l2)) :output-contract (listp (f5 l1 l2)) (cond ((endp l1) (list 1 2)) ((endp l2) (f5 (cons 5 l1) (list 5))) ((>= (len l2) (len l1)) (f5 l2 (list l1))) (t (f5 (rest l1) (rest l2))))) ##.............. |# #| A6. Finally, prove that ssort should be admissible by proving it terminates....and make sure the other admissibility conditions pass (defunc ssort (l) :input-contract (lorp l) :output-contract (lorp (ssort l)) (if (endp l) l (let ((min (min-l l))) (cons min (ssort (del min l)))))) ....and as you might imagine, this will require lemmata. 1) Write the measure function and termination proof obligations. Find what you need to prove. 2) Generalize the lemma so you know what happens when something IN a list is DELeted from a list. What happens to the size of the list? 3) How do you know (min-l l) is IN the list?....wait. That sounds like a lemma too. See L3. 4) Finally, pull it all together to prove that the value of the measure function decreases with each recursive call (thus ssort terminates). Your lemma will have something involving (del (min-l l) l)) The proof doesn't require induction provided you use L3 (below) and 2) above. ----------------------------------- Hopefully Helpful Theorems Let's make the proof easier....or less annoying at least. You can use the following theorem without proving it: L3: (lorp l) /\ (consp l) => (in (min-l l) l) (This is hint 3) from the list above by the way) ----------------------------------- ##.............. |# #| ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; Section B: IN Next, let's do some proofs involving the function in and weave. --------------------------------------------- Hopefully Helpful Theorems You may assume the following theorems (or prove them if you want the practice): Phi_permReflect: (listp l) => (perm l l) Assumption A1. (listp x) /\ (listp y)/\(listp z) /\ (in e y) => (perm (cons e z) (app x y) = (perm z (app x (del e y))) ....in other words, even if e exists in list x, you can delete e from y (provided it's in y) to see if z is a permutation of x and y minus element e. --------------------------------------------- B1. Prove (listp x)/\ (listp y) => (in e (app x y)) = ((in e x) \/ (in e y)) ##.............. EXTRA QUESTION (no points and purely optional): B1 can be used to prove the following B1b: (listp x)/\(listp y) => ((in e (app x y)) = (in e x) \/ (in e y)) How can you use B1 to prove this? and what other conjectures do you need to prove to get the equality (or iff)? Prove B1b for extra practice. You can write B1b and the related theorems on your cheat sheet for the exam if you want. ##.............. B2. Prove (listp x)/\ (listp y) => (in e (weave x y)) = ((in e x) \/ (in e y)) ##.............. EXTRA (no points): prove Phi_permWA: (listp x)/\(listp y) =>(perm (weave x y)(app x y)) using the induction scheme for weave. ##.............. |# #| ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; Section C: Tail Recursion I Let's revisit some functions from the sample exam. |# ;; add-to-all: nat x LON -> LON ;; (add-to-all n l) takes a natural number n and ;; a list of natural numbers l and adds n to each element of l: (defunc add-to-all (n l) :input-contract (and (natp n) (lonp l)) :output-contract (lonp (add-to-all n l)) (if (endp l) () (cons (+ (first l) n) (add-to-all n (rest l))))) (check= (add-to-all 1 '(1 2 3)) '(2 3 4)) ;; find: All x List -> LON ;; (find x l) returns the indexes of each occurence of ;; x in list l. Thus the returned value is a list of natural numbers (defunc find (x l) :input-contract (listp l) :output-contract (lonp (find x l)) (cond ((endp l) ()) ((equal (first l) x) (cons 0 (add-to-all 1 (find x (rest l))))) (t (add-to-all 1 (find x (rest l)))))) (check= (find 1 '(1 2 3 2 1)) '(0 4)) ; find counting starts from 0 #| a) Now define a tail-recursive version find-t of find. Hint: the tail-recursive function find-t walks through the input list from left to right. Suppose you see an occurrence of x. In order to know what its index is in the *original* list, you have to keep track of the number of elements already processed. Function find-t should thus have an extra argument, say c, for that purpose: ##.............. |# #| (c) We define below a non-recursive function find* that uses find-t to compute the same value as find. Note that we need to initialize both c and acc properly. |# ##.............. #| (d) Write a lemma that relates find-t and find. Hint: this requires some thought. Evaluate find-t on some examples to figure out what it should be. The lemma will involve several functions other than find-t and find. Remember add-to-all. There should be no constants anywhere in your lemma. HINT: Use test? to sanity-check your lemma. ##.............. (e) Assuming the lemma is true, prove that find* and find compute the same function: ##.............. (f) Prove the lemma in (d). In proving the lemma, you can assume the following: (natp a) /\ (lonp l) => (lonp (cons a l)) (we typically say "Def of lon" but it's OK to be more specific like this from time to time) In addition, during the proof you will need several lemmas that we have proven before, and some that are new. *************** L2: (listp l) /\ (natp c) /\ (lonp acc) => (find-t x l c acc) = (app (rev (add-to-all c (find x l))) acc) L3: (natp c) /\ (natp i) /\ (listp l) => (cons c (add-to-all (+ c i) l)) = (add-to-all c (cons 0 (add-to-all i l))) ##.............. (g) Prove any new lemmas used in (f). (if there are any) ##.............. |# #| ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; Section D: Tail Recursion II: Revenge of Weave a) Remember weave? I told you we would keep using the same function for these proofs. Write a tail recursive version of weave (weave-t) and a wrapper function weave* Keep in mind the order that (first x) and (first y) are being added to acc. (defunc weave (x y) :input-contract (and (listp x)(listp y)) :output-contract (listp (weave x y)) (cond ((endp x) y) ((endp y) x) (t (cons (first x) (cons (first y) (weave (rest x)(rest y))))))) |# ##.............. #| b) Now prove that weave* = weave. You should do all the steps we outlined in our tail recursive proof recipe. ##.............. |# #| Extra Practice: Write a tail recursive version of isort (don't get fancy by calling max-l instead of min-l. Just reverse the sorted list at the end) The solution won't be provided but it's still a good exercise ##....................... |# #| Good luck on the exam everyone. |#