; **************** BEGIN INITIALIZATION FOR ACL2s B MODE ****************** ; ; (Nothing to see here! Your actual file is after this initialization code); #| Pete Manolios Fri Jan 27 09:39:00 EST 2012 ---------------------------- Made changes for spring 2012. Pete Manolios Thu Jan 27 18:53:33 EST 2011 ---------------------------- The Beginner level is the next level after Bare Bones level. |# ; Put CCG book first in order, since it seems this results in faster loading of this mode. #+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.~%") (value :invisible)) (include-book "custom" :dir :acl2s-modes :uncertified-okp nil :ttags :all) ;Settings common to all ACL2s modes (acl2s-common-settings) #+acl2s-startup (er-progn (assign fmt-error-msg "Problem loading trace-star and evalable-ld-printing books.~%Please choose \"Recertify ACL2s system books\" under the ACL2s menu and retry after successful recertification.") (value :invisible)) (include-book "trace-star" :uncertified-okp nil :dir :acl2s-modes :ttags ((:acl2s-interaction)) :load-compiled-file nil) (include-book "hacking/evalable-ld-printing" :uncertified-okp nil :dir :system :ttags ((:evalable-ld-printing)) :load-compiled-file nil) ;theory for beginner mode #+acl2s-startup (er-progn (assign fmt-error-msg "Problem loading ACL2s beginner theory book.~%Please choose \"Recertify ACL2s system books\" under the ACL2s menu and retry after successful recertification.") (value :invisible)) (include-book "beginner-theory" :dir :acl2s-modes :ttags :all) #+acl2s-startup (er-progn (assign fmt-error-msg "Problem setting up ACL2s Beginner mode.") (value :invisible)) ;Settings specific to ACL2s Beginner mode. (acl2s-beginner-settings) ; why why why why (acl2::xdoc acl2s::defunc) ; almost 3 seconds (cw "~@0Beginner mode loaded.~%~@1" #+acl2s-startup "${NoMoReSnIp}$~%" #-acl2s-startup "" #+acl2s-startup "${SnIpMeHeRe}$~%" #-acl2s-startup "") (acl2::in-package "ACL2S B") ; ***************** END INITIALIZATION FOR ACL2s B MODE ******************* ; ;$ACL2s-SMode$;Beginner #| CS 2800 Homework 9 - 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. |# ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; #| Inductive Proofs: - For all proofs below, solutions must be in the format described in class and in the notes. This includes: * Explicitly identifying an induction scheme and the function that gives rise to it. * Labeling general context (C1, C2....) and derived context. * Providing justifications for each piece of derived context. * Explicitly identifying axioms and theorems used * The if axioms and theorem substitutions are not required. You can use any other shortcuts previously identified. * PL can be given as justification for any propositional logic rules with the exceptions of Modus Ponens (MP) and Modus Tollens (MT) * All arithmetic rules can be justified by writing "Arithmetic". Previous homeworks (such as HW05) identify these requirements in more detail. |# ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; #| For this homework you may want to use ACL2s to help you. Technical instructions: - open this file in ACL2s as hw09.lisp - make sure you are in BEGINNER mode. This is essential! Note that you can only change the mode when the session is not running, so set the correct mode before starting the session. - insert your solutions into this file where indicated (usually as "...") - only add to the file. Do not remove or comment out anything pre-existing unless asked to. - make sure the entire file is accepted by ACL2s. In particular, there must be no "..." left in the code. If you don't finish all problems, comment the unfinished ones out. Comments should also be used for any English text that you may add. This file already contains many comments, so you can see what the syntax is. - when done, save your file and submit it as hw09.lisp - avoid submitting the session file (which shows your interaction with the theorem prover). This is not part of your solution. Only submit the lisp file! |# ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; GIVEN FUNCTIONS ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; #| We start with some familiar definitions just in case they are useful. (defunc listp (x) :input-contract t :output-contract (booleanp (listp x)) (if (consp x) (listp (rest x)) (equal x nil))) (defunc app (a b) :input-contract (and (listp a) (listp b)) :output-contract (listp (app a b)) (if (endp a) b (cons (first a) (app (rest a) b)))) (defunc rev (a) :input-contract (listp a) :output-contract (listp (rev a)) (if (endp a) nil (app (rev (rest a)) (list (first a))))) (defunc len (a) :input-contract t :output-contract (natp (len a)) (if (atom a) 0 (+ 1 (len (rest a))))) (defunc in (a X) :input-contract (listp x) :output-contract (booleanp (in a X)) (if (endp x) nil (or (equal a (first X)) (in a (rest X))))) |# ;; Assume by "Def of lor" that each element is a rational ;; and a lor is (cons rational lor) | nil (defdata lor (listof rational)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; GIVEN ;; orderedp: lor -> boolean ;; (orderedp l) takes a list of rationals ;; and returns true if and only if the elements ;; are in non-decreasing order (ie they are ordered) (defunc orderedp (l) :input-contract (lorp l) :output-contract (booleanp (orderedp l)) (or (endp l) (endp (rest l)) (and (<= (first l) (second l)) (orderedp (rest l))))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; GIVEN ;; del: Any x List -> List ;; (del e l) takes an element e and a list l ;; and removes the FIRST occurance 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)))))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; GIVEN ;; perm: List x List -> List ;; (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) (endp l2) (and (in (first l1) l2) (perm (rest l1) (del (first l1) l2)))))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; GIVEN ;; sortedp: LOR x LOR -> Boolean ;; (sortedp origL sortL) takes the original list ;; and the theoretically sorted list (sortL) ;; and determines if sortL is a sorteding ;; of the original list. (defunc sortedp (origL sortL ) :input-contract (and (lorp origL)(lorp sortL)) :output-contract (booleanp (sortedp origL sortL)) (and (perm origL sortL)(orderedp sortL))) ;; less: rational x lor -> lor ;; (less x lst) makes a list of all elements in lst that ;; are less than x (defunc less (x lst) :input-contract (and (rationalp x) (lorp lst)) :output-contract (lorp (less x lst)) (cond ((endp lst) ()) ((< (first lst) x) (cons (first lst) (less x (rest lst)))) (t (less x (rest lst))))) ;; not-less: rational x lor -> lor ;; (not-less x lst) makes a list of all elements in lst that ;; are not-less than x (defunc not-less (x lst) :input-contract (and (rationalp x) (lorp lst)) :output-contract (lorp (not-less x lst)) (cond ((endp lst) ()) ((< (first lst) x) (not-less x (rest lst))) (t (cons (first lst) (not-less x (rest lst)))))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; GIVEN ;; qsort: LOR -> LOR ;; (qsort l)....or quicksort takes the original list of rationals l ;; and arranges the elements so the list is sorted. ;; It does this by taking the first element (pivot element) ;; and putting all elements < the pivot before it, and all ;; elements >= the pivot after the pivot. qsort is then ;; called on the < list and the >= list. Thus the list is eventually sorted (defunc qsort (l) :input-contract (lorp l) :output-contract (lorp (qsort l)) (if (endp l) l (let ((less (less (first l) (rest l))) (gte (not-less (first l) (rest l)))) (app (qsort less) (cons (first l) (qsort gte)))))) #| GIVEN THEOREMS If you had to prove all of these yourself this homework would be far longer than it already is You can prove any one of these if you want extra practice ALSO REMEMBER HW08: we proved a lot of things there and some might be useful here. phi_less_r (lorp l)/\(rationalp r)/\(in e (less r l))=> (< e r) phi_nless_r (lorp l)/\(rationalp r)/\(in e (not-less r l))=> (>= e r) phi_perm_refl (listp l) => (perm l l) phi_perm_sym (listp x)/\(listp y)/\(perm x y) => (perm y x) phi_in_del (listp x) /\ ~(e = f) /\ (in e x) => (in e (del f x)) phi_perm_trans (listp x)/\ (listp y)/\(listp z) /\ (perm x y)/\ (perm y z)=> (perm x z) |# #| ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; Warm up Proofs Take a new function last: (defunc last (x) :input-contract (and (listp x)(consp x)) :output-contract t (cond ((endp (rest l)) (first l)) (t (last (rest l))))) Prove: phi_app_order: ((lorp x)/\(lorp y)/\(consp x)/\ (consp y) /\(< (last x) (first y)) /\ (orderedp x) /\ (orderedp y)) => (orderedp (app x y)) Well that seems specific but really what we are proving is that connecting two ordered lists where elements in x are < elements of y, creates an ordered list. Note: If x or y are empty then we know (app x y) is ordered (def of app and phi_app_nil from class). What would be a good induction scheme to use? Maybe one that stops at (endp (rest x)) rather than (endp x). Also notice that you haven't proven that (in (last x) x) is always true for non-empty lists x. #.....# |# #| BIG OPEN ENDED PROOF: Proving qsort is sorted (part 2) OK. I gave a bunch of mini theorems last homework (and they may be useful here) but I want to approach the next part in a more "realistic" way by making the problem more open ended. Prove the following: (lorp l) => (sortedp l (qsort l)) You will need to break the problem into parts and you will definitely need to prove some other theorems along the way. #....# |# #| Salt on the Wound: An Introduction to Tail Recursive Functions Here is my solution for the exam 1 question involving tries. Let's do this one more time but let's make t-firstpath a tail recursive function using an accumulator. We could also convert t-mostPref but that will be harder to prove. Notice that we don't need to change t-getNode (it's already tail recursive technically) - Write a function t-firstpath* which is non-recursive and calls t-firstpath-t which is a tail recursive function (ie for any recursive condition, the last thing it does is the recursive call). - Prove t-firstpath* = t-firstpath.....you will need a lemma. Make sure you follow our design recipe for accumulator functions. |# ; Question 1 data definitions (defdata char (enum '(root #\A #\B #\C #\D #\E #\F #\G #\H #\I #\J #\K #\L #\M #\N #\O #\P #\Q #\R #\S #\T #\U #\V #\W #\X #\Y #\Z))) (defdata (node (list char node-list)) (node-list (listof node)) (trie (list 'root node-list))) (defdata node-find (oneof node nil)) (defdata char-list (listof char)) (defconst *trie-test* (list 'root '((#\C ((#\A ((#\B nil) (#\T nil))))) (#\B ((#\A ((#\D nil))))) (#\Q nil)))) (defunc t-getNode (c ln) :input-contract (and (charp c)(node-listp ln)) :output-contract (node-findp (t-getNode c ln)) (cond ((endp ln) nil) ((equal c (first (first ln))) (first ln)) (t (t-getNode c (rest ln))))) (check= (t-getNode #\Q (second *trie-test*)) '(#\Q nil)) (check= (t-getNode #\R (second *trie-test*)) nil) (test? (implies (and (charp c)(node-listp ln)) (or (in (t-getNode c ln) ln) (equal (t-getNode c ln) nil)))) (defunc t-firstpath (n) :input-contract (nodep n) :output-contract (char-listp (t-firstpath n)) (if (endp (second n)) (list (first n));nil (cons (first n)(t-firstpath (first (second n)))))) (check= (t-firstpath *trie-test*) '(root #\C #\A #\B)) ;; Program mode for most of these functions is fine. Normally this would ;; be a problem but I wanted a t-mostpref question and that's hard to ;; admit in logic mode. :program ;; t-mostpref: char-list x node -> char-list ;; (t-mostpref lc n) takes a list of characters and returns ;; the list of characters from the path with the greatest ;; common prefix to lc (defunc t-mostpref (lc n) :input-contract (and (char-listp lc)(nodep n)) :output-contract (char-listp (t-mostpref lc n)) (cond ((endp (second n)) (list (first n))) ((endp lc) (t-firstpath (first (second n)))) (t (let ((n2 (t-getNode (first lc) (second n)))) (if (equal n2 nil) (t-firstpath n) (cons (first lc) (t-mostpref (rest lc) n2))))))) (check= (t-mostpref '(#\B #\A) *trie-test*) '(#\B #\A #\D)) (check= (t-mostpref '(#\R #\A) *trie-test*) '(ROOT #\C #\A #\B)) (check= (t-mostpref '(#\C #\A) *trie-test*) '(#\C #\A #\B)) ;;........Write t-firstpath* here ;#.....# (check= (t-firstpath* *trie-test*) '(root #\C #\A #\B)) #| Prove (nodep n) => (t-firstpath* n) = (t-firstpath n) #....# |# ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Feedback (5 points) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; #| I would like to get more feedback from you. Here are a couple questions to monitor how the course is progressing. This should be brief. Please fill out the following form. https://goo.gl/forms/JYxQ7UbuId5Fg3Hx1 As before, feedback is anonymous and each team member should fill out the form (only once per person). After you fill out the form, write your name below in this file, not on the questionnaire. We have no way of checking if you submitted the file, but by writing your name below you are claiming that you did, and we'll take your word for it. 5 points will be awarded to each team member for filling out the questionnaire. The following team members filled out the feedback survey provided by the link above: --------------------------------------------- |#