#| CS 2800 Homework 6 - Summer 2018 This homework is to be done in a group of 2-3 students. If your group does not already exist: * One group member will create a group in BlackBoard * Other group members then join the group Submitting: * Homework is submitted by one group member. Therefore make sure the person submitting actually does so. In previous terms when everyone needed to submit we regularly had one person forget but the other submissions meant the team did not get a zero. Now if you forget, your team gets 0. - It wouldn't be a bad idea for group members to send confirmation emails to each other to reduce anxiety. * Submit the homework file (this file) on Blackboard. Do not rename this file. There will be a 10 point penalty for this. * You must list the names of ALL group members below, using the given format. This way we can confirm group membership with the BB groups. If you fail to follow these instructions, it costs us time and it will cost you points, so please read carefully. Names of ALL group members: FirstName1 LastName1, FirstName2 LastName2, ... Note: There will be a 10 pt penalty if your names do not follow this format. ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; EQUATIONAL REASONING + EXAM REVIEW Homework 6 is extra big because it serves not only as practice for E.R. but also general practice for the exam. Thus the time it takes you is time spend "studying" for the exam and that practice is far more useful than reading the textbook again. Theme: Annoying Teacher Your CS 2800 Professor really must not be much of a programmer. He keeps asking you to write obviously slow code to match the "data definition" despite the fact there is obviously a more efficient approach. Other times he simply writes functions in a weird round-about way or claims that two functions are the same when they are clearly not. Worse of all, he won't accept this fact when you tell him. It's your job to prove him wrong. Each question will be made up of several parts A) If you are given a conjecture that is not valid: 1) Perform contract checking and completion 2) Try some sample data to make sure you understand the conjecture (no need to show us this) 3) Give a counter-example B) If a given conjecture is true: 1) Write a more efficient version of a given function (if not already defined) Given Complex Propositional Structure 2) Perform contract checking and completion. 3) Try some sample data to make sure you understand the conjecture (no need to show us this) 4) Break the conjecture down into a series of smaller parts that can be solved Equational Reasoning Proof 5) Prove each of the sub-conjectures. Unlike in HW05, you do not need to show how each theorem is instantiated EXCEPT each time you use a definitional theorem (you don't need to do this normally but you should practice how to express a substitution). Note, some proofs (such as the one-countsp proof) need a lemma. You may be required to find the lemma. C) I added some programming problems at the end. 1) Define the functions based on the purpose statement 2) Write tests to check your function First, however, we need to give you a long list of rules to follow..... ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Equational Reasoning Rules: ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; Below you are given a set of function definitions you can use. The definitional axioms and contract theorems for these functions can be used in the proof. You can use ACL2s to check the conjectures you are proving but you are not required to do so. Here are some notes about equational proofs: 1. General context: Remember to use propositional logic to rewrite the conjectures so that it has as many hypotheses as possible. See the lecture notes for details. Label the facts in your context with C1, C2, ... as in the lecture notes. 2. The derived context: Draw a dashed line (----) after the general context and add anything interesting that can be derived from the context. Use the same labeling scheme as was used in the context. Each derived fact needs a justification. Again, look at the lecture notes for more information. 3. Use the proof format shown in class and in the lecture notes, which requires that you justify each step. Explicitly name each axiom, theorem or lemma you use, although we are starting to "cut corners" with the if axiom and the instantiations we are using. You can take any "shortcuts" discussed in class. 5. When using the definitional axiom of a function, the justification should say "Def. ". When using the contract theorem of a function, the justification should say "Contract ". For definitional axioms alone, you should write the instantiation (for exam practice) 6. Arithmetic facts such as commutativity of addition can be used. The name for such facts is "arithmetic". 7. You can refer to the axioms for cons, and consp as the "cons axioms", Axioms for first and rest can be referred to as "first-rest axioms". The axioms for if are named "if axioms" 8. Any propositional reasoning used can be justified by "propositional reasoning", "Prop logic", or "PL", except you should use "MP" to explicitly identify when you use modus ponens and MT for Modus Tollens. 9. For any given propositional expression, feel free to re-write it in infix notation (ex a =>(B/\C)). 10. For this homework, you can only use theorems we explicitly tell you you can use or we have covered in class / lab. You can, of course, use the definitional axiom and contract theorem for any function used or defined in this homework. You may also use theorems you've proven earlier in the homework. Here are the definitions used for the remainder of the questions. ;; listp is built in but for this assignment, assume it ;; is defined this way (defunc listp (l) :input-contract t :output-contract (booleanp (listp l)) (if (consp l) (listp (rest l)) (equal l nil))) (defunc endp (l) :input-contract (listp l) :output-contract (booleanp (endp l)) (if (consp l) nil t)) (defunc len (x) :input-contract (listp lenx) :output-contract (natp (len x)) (if (endp x) 0 (+ 1 (len (rest x))))) (defunc app (x y) :input-contract (and (listp x)(listp y)) :output-contract (listp (app x y)) (if (endp x) y (cons (first x)(app (rest x) y)))) (defunc in (a l) :input-contract (listp l) :output-contract (booleanp (in a l)) (if (endp l) nil (or (equal a (first l)) (in a (rest l))))) ;; delete : All x List -> List ;; removes all instances of the element a from the list (defunc delete (a l) :input-contract (listp l) :output-contract (listp (delete a l)) (cond ((endp l) nil) ((equal a (first l)) (delete a (rest l))) (t (cons (first l) (delete a (rest l)))))) ;; duplicate: List -> List ;; repeats each element in the given list once (defunc duplicate (l) :input-contract (listp l) :output-contract (listp (duplicate l)) (if (endp l) nil (cons (first l) (cons (first l) (duplicate (rest l)))))) ;; no-dupesp: list -> boolean ;; (no-dupesp l) returns true iff the list l has no duplicates within it. (defunc no-dupesp (l) :input-contract (listp l) :output-contract (booleanp (no-dupesp l)) (cond ((endp l) t) ((in (first l) (rest l)) nil) (t (no-dupesp (rest l))))) |# #| ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; Question 1: A Crappy no-dupes Here is your instructor's first attempt at testing whether a list has duplicate elements. He simply counts the number of instances for each element in the list and if any are greater than 1, there must be a duplicate.....of course counting the number of occurances in a list requires going through the whole list. no-dupesp should be more efficient. Your job will be to prove (one-countsp l)= (no-dupesp l) |# ;; GIVEN (defunc count-in (e l) :input-contract (listp l) :output-contract (natp (count-in e l)) (cond ((endp l) 0) ((equal e (first l)) (+ 1 (count-in e (rest l)))) (t (count-in e (rest l))))) ;; GIVEN ;; one-countsp: list -> boolean ;; (one-countsp l) returns true iff each element in l is found once in the list ;; (within reason: elements at the end of the list don't check the front of the ;; list this way). (defunc one-countsp (l) :input-contract (listp l) :output-contract (booleanp (one-countsp l)) (cond ((endp l) t) ((> (count-in (first l) l) 1) nil) (t (one-countsp (rest l))))) #| You will need the following lemma which can be broken into 3 cases for the proof. Lemma L1: ((count-in e l) >= 1) = (in e l) Notice that (endp l) \/ (~(endp l)/\(e = first l)) \/ (~(endp l)/\ ~(e = first l))) = true Perform contract checking and completion on L1. Add this context to the underline below |# #| __________ => ( ((endp l) \/(~(endp l)/\(e = (first l)) /\ (listp (rest l)) => (((count-in e (rest l))>=1)=(in e (rest l)))) \/(~(endp l)/\ ~(e = (first l)) /\ (listp (rest l)) => (((count-in e (rest l))>=1)=(in e (rest l))))) => ((count-in e l) >= 1 = (in e l))) A) Rearrange the propositional structure (using logical equivalences) to make this a conjecture with three "and" conditions in its simplest form. Feel free to rename the function calls to A, B, C.... if that helps you. Thus the conjecture would be A => (B \/ (~B/\C)..... and would look something like (A/\B => E) /\ (A /\ ~B/\C => E.... in the end. .............. Now prove the three parts of the conjecture to prove L1 ............ Now prove ____________=>(one-countsp l)= (no-dupesp l) You may need several cases.....look to no-dupesp for inspiration You can also assume the following for any case when a recursive call would happen (and thus the list is not empty): (listp (rest l)) => (one-countsp (rest l)) = (no-dupesp (rest l)) You can simply write this as a piece of general context or any non-empty l. ............ Finally prove the following conjecture or give a counter-example (sum-counts l) = (len l) Actually is this conjecture valid, satisfiable, unsatisfiable or (not xor) falsifiable? Where (sum-counts is defined as (defunc sum-counts (l) :input-contract (listp l) :output-contract (natp (sum-counts l)) (if (endp l) 0 (+ (count-in (first l) l)(sum-counts (rest l))))) .............. |# #| ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; QUESTION 2: Abs Fast Here is what your instructor claims the absolute function of integers needs to be: |# (defunc abs (i) :input-contract (integerp i) :output-contract (natp (abs i)) (cond ((equal i 0) 0) ((< i 0) (+ 1 (abs (+ i 1)))) (t (+ 1 (abs (- i 1)))))) ;; a) Write a function abs2 based on the following purpose statement ;; abs2: integer -> nat ;; (abs2 i) takes an integer i and returns its absolute value (or the ;; distance from i to 0). abs2 must be non-recursive or you will ;; receive no marks for question 2. .......... #| Now that you've written a faster absolute value function, show that your faster version is functionally equivalent to the original (given the same input they return the same outputs). ____________=>( (i=0) \/ ((~(i=0)/\(i>0)/\ (((integerp (- i 1))/\(>= (- i 1) 0))=> => ((abs (- i 1))=(abs2 (- i 1))))) \/ (~(i=0)/\~(i>0)/\ (((integerp (+ i 1))/\(<= (+ i 1) 0))=> => ((abs (+ i 1))=(abs2 (+ i 1))))) =>(((abs i) => (abs2 i)) /\ ((abs2 i) => (abs i)))) Remember to do a series of logical equivalence to get this in the form of 3 and statements with as much context as possible. Also you may be able to clean up the consequent (RHS of the last implies). ............ After simplifying the conjecture into 3 and statements, do the proof ............ |# #| ========================= Question 3: Primes Professor Sprague is being a pain revisiting that darn prime factors function from HW02. Here is the solution for HW02: |# (defdata gpos (range integer (2 <= _))) ;; Ignore (defthm phi_shrink_factor (implies (and (gposp n)(gposp f)(gposp (/ n f))) (< (/ n f) n))) (defdata logp (listof gpos)) ;; GIVEN: ;; factors-help : gpos x gpos -> Lop ;; returns a list containing all PRIME factors of n including (possibly) ;; n and 1. (defunc factors-help (n p) :input-contract (and (gposp n) (gposp p)) :output-contract (logpp (factors-help n p)) (cond ((> p n) nil) ((equal p n) (list n)) ((gposp (/ n p)) (cons p (factors-help (/ n p) p))) (t (factors-help n (+ p 1))))) ;; GIVEN ;; factors : Pos -> Lop ;; returns a list containing all PRIME factors of n including (possibly) ;; n and 1. (defunc factors (n) :input-contract (gposp n) :output-contract (logpp (factors n)) (let ((fh (factors-help n 2))) (if (endp fh) (list n) fh))) ;; Note the factors for 12 *could* be listed as 1 2 3 4 6 12 but ;; really 12 is uniquely represented as the product of non-decreasing ;; prime numbers: 2*2*3. Thus factors will return '(2 2 3) ;; 13 is prime so it isn't decomposed into other ;; primes and '(13) is returned. ;; If you get the same values but in a different order, feel free to ;; change the tests. (check= (factors 2)'(2)) (check= (factors 4)'(2 2)) (check= (factors 6)'(2 3)) (check= (factors 12)'(2 2 3)) (check= (factors 13)'(13)) ;; GIVEN ;; Defined in previous functions. Removes ;; the first instance of an element in a list (defunc delete (e l) :input-contract (listp l) :output-contract (listp (delete e l)) (if (endp l) l (if (equal e (first l)) (rest l) (cons (first l)(delete e (rest l)))))) ;; Ignore (sig delete (all (listof :b)) => (listof :b)) ;; GIVEN ;; intersect: list x list -> list ;; (intersect l1 l2) returns a list containing every element ;; that is in both lists l1 and l2. (defunc intersect (l1 l2) :input-contract (and (listp l1) (listp l2)) :output-contract (listp (intersect l1 l2)) (cond ((endp l1) l1) ((in (first l1) l2) (cons (first l1) (intersect (rest l1) (delete (first l1) l2)))) (t (intersect (rest l1) l2)))) ;; GIVEN ;; coprime: pos x pos -> boolean ;; determines whether two positive integers a and b are coprime (defunc coprime (a b) :input-contract (and (gposp a) (gposp b)) :output-contract (booleanp (coprime a b)) (endp (intersect (factors a) (factors b)))) ;; this line is for ACL2s (sig intersect ((listof :b) (listof :b)) => (listof :b)) ;; GIVEN ;; prod-list: lop -> Pos ;; (prod-list lp) multiplies all values in list lp together ;; If the list is emtpy, return 1. (defunc prod-list (lgp) :input-contract (logpp lgp) :output-contract (posp (prod-list lgp)) (if (endp lgp) 1 (* (first lgp)(prod-list (rest lgp))))) ;; GIVEN ;; gcd: pos x pos -> pos ;; (gcd a b) determines the greatest common divisor for a and b. ;; Do you remember how to calculate that with prime factors? (defunc gcd (a b) :input-contract (and (gposp a) (gposp b)) :output-contract (posp (gcd a b)) ;; SOLUTION (prod-list (intersect (factors a) (factors b)))) (check= (gcd 7 6) 1) (check= (gcd 8 6) 2) (check= (gcd 12 6) 6) (check= (gcd 30 12) 6) (check= (gcd 30 28) 2) (check= (gcd 35 28) 7) (test? (implies (and (gposp a)(gposp b)) (equal (gcd a b)(gcd b a)))) #| ;;Here's the NEW prime method that Professor Sprague came up with: :program ;; factors1: gpos x gpos -> logp ;; (factors1 n v) finds the factors of n ;; Since primes will never be even, increase ;; v by 2 each iteration. (defunc factors1 (n v) :input-contract (and (gposp n)(gposp v)) :output-contract (logpp (factors1 n v)) (if (> v n) nil (if (natp (/ n v)) (cons v (factors1 n (+ v 2))) (factors1 n (+ v 2))))) :logic a) Prove (factors1 n v) = (factors-help n v) or provide a counter-example. ............ |# #| b) Perform contract completion on the following: A1: (iff (in b (factors a)) (natp (/ a b))) * iff is "if and only if" in case you forgot What is this equivalent to (there are multiple things). **YOU MAY ASSUME A1 IS A THEOREM.....it actually isn't but let's pretend it is just the same.....b has to be a prime for A1 to be valid in case you were wondering but we'll ignore this** ............ ; Prove each of the following conjectures with equational reasoning or provide a ; counterexample. You may assume that your contract-completed lemma above holds. c) (implies (and (gposp a) (gposp b) (gposp c) (coprime a b) (not (coprime a c))) (coprime b c)) ............ d) (implies (and (gposp a)(gposp b)) (iff (equal (gcd a b) 1) (coprime a b))) You may also assume that (prod-list l) = 1 means that l is empty. ............ e) (implies (and (gposp a) (gposp b) (gposp c) (in b (factors a))) (in b (factors (* a c)))) ............ f) (implies (and (posp n) (natp (/ n 6)) (>= (len (factors n)) 2))) Here is a free theorem you can use (no need to prove it): Theorem Phi_in-len: (listp l) /\ (in e l) => ((len l) = (+ 1 (len (del e l)))) Remember, any basic arithmetic relationships are justified with "arithmetic" For example, (natp (/ n 20)) being true means (natp (/ n 2)) is also true. A1 may continue to be useful. ............ |# #| %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Question 4: Programming In case it wasn't obvious, your instructor is a MASSIVE geek (and proud of it). Sometimes I just want to play a game of Dungeons and Dragons (https://en.wikipedia.org/wiki/Dungeons_%26_Dragons) rather than work on an assignment. Let's combine both. You typically play the game with friends where each person controls a player character (PC)and you role play (ie say what your character will do) as you all go out on an adventure to save a castle / find treasure / kill peasants (you can play evil characters if you want) Each player character has: A name (symbol or string. Either is fine Class (fighter, mage, cleric...), Race (elf, dwarf, human...) Stats (max hit points, current hit points, strength....) Inventory (+1 long bow, Eye of Vecna, +5 Holy Avenger) Feel free to add other things like skills and spells. Notice also that I'm not giving an exhaustive list.....the game changes all the time and I don't think it's your job to know what at drow or a palladin is. We won't be looking at that for accuracy. You just need more than one of each type and make up names, races, classes, stats or whatever you want. Have fun with this....just don't write anything offensive. Define a data definition that encodes all necessary information about a PC and a data definition that represents a party of players. Next, let's solve a regular problem for D&D: who has an item. Since each person has an inventory, knowing who has the ring of invisibility can sometimes be a problem. Write a function that takes a PCParty and an item (symbol) and returns the PCs with the item. |# .......... (defdata player ;.......) (defdata PCParty (listof player)) ............ ;; who-has-item: symbol x PCParty -> PCParty ;; (who-has-item i pcp) takes an symbol i representing ;; an item and a PCParty pcp and returns the list of ;; characters with the item. (defunc who-has-item (i pcp) ............) #| %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Question EXTRA: Flatten list (no points but practice) Here are three functions "you" wrote for flattening a list Ex. (fatten-list '((1 2) '(3 '(4)))) returns '(1 2 3 4) |# ;; nelistp: All -> Boolean ;; nelistp returns true iff l is a non-empty list ;; Useful for simplifying the code below (defunc nelistp (l) :input-contract t :output-contract (booleanp (nelistp l)) (and (listp l)(consp l))) ;; flat-listp: All -> Boolean ;; (flat-listp l) recognizes whether an input ;; is a flat list (a list with no non-empty sub-lists) ;; NOTE: Don't worry about conses that are not lists. ;; In this case, the cons is considered like an atom ;; (makes the code easier to write) (defunc flat-listp (l) :input-contract t :output-contract (booleanp (flat-listp l)) (cond ((not (listp l)) nil) ((endp l) t) ((nelistp (first l)) nil) (t (flat-listp (rest l))))) :program ;; flatten-list: List -> List ;; (flatten-list l) takes a list and puts all atoms ;; in the list at the top level. Thus the generated list ;; will not have a list of lists inside it. Ignore ;; situations with non-list conses. (defunc flatten-list (l) :input-contract (listp l) :output-contract (flat-listp (flatten-list l)) (cond ((endp l) l) ((not (nelistp (first l))) (cons (first l) (flatten-list (rest l)))) (t (app (flatten-list (first l)) (flatten-list (rest l)))))) #| Well neither ACL2s nor your professor can prove that flatten-list must produce a flat list (by definition of flat-listp). Prove it to show you are right. Prove (implies (and (listp l) (implies (nelistp l)(flat-listp (flatten-list (rest l)))) (implies (and (nelistp l)(nelistp (first l))) (flat-listp (flatten-list (first l)))) (or (endp l)(and (nelistp l)(nelistp (first l))) (and (nelistp l)(not (nelistp (first l)))))) (flat-listp (flatten-list l))) a) Notice the massive expression? Rewrite it into THREE proof obligations which are the three propositional expressions that, if proven, will prove the main conjecture. The proof obligations will also be pretty large. This is similar to what you did in section 1. Also note the two implies within the giant AND statement (lines 2 to 4 of the conjecture above). How can you use these? In what circumstances? ............ b) Now prove your three proof obligations. You can assume the following theorems: phi_flatten_app: (implies (and (flat-listp l1)(flat-listp l2)) (flat-listp (app l1 l2))) phi_flatten_cons: (implies (and (flat-listp l)(not (nelistp e))) (flat-listp (cons e l))) ............ c) OK. You have higher standards than that. You don't want to just assume the given theorems. Prove phi_flatten_cons. You can assume that (flat-listp l) => (listp l) ........... |#