#|

Lab 2 Problem Set.

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.

The same rules apply as for the homeworks. Here is an abbreviated version.
While we do not grade lab problems, make these rules a habit.

For each function definition, you must provide both contracts and a body.
You must also ALWAYS supply your own tests, and sufficiently many, in
addition to the tests sometimes provided. The number of tests should
reflect the data definitions relevant for the problem, and the difficulty
of the function.

Write tests using ACL2s' check= function.

Include the following directive at the top of your Lisp file:

|#

:program

#|

We will explain what this means in lab. At the end, comment out this line
and see whether your file is still accepted.

|#

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; major : Boolean x Boolean x Boolean -> Boolean

; (major a b c) is t if the "majority" (i.e. at least two) of a, b, c is t,
; and nil otherwise.

(check= (major t   nil t)   t)
(check= (major nil t   nil) nil)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; equal-prefix: List x List x Nat -> Boolean

; (equal-prefix l1 l2 n) returns t if
; - both l1, l2 have at least n elements, AND
; - the prefixes of l1 and l2 of length n are equal.

(check= (equal-prefix '(1 2 3) '(1 2 3) 3) t)
(check= (equal-prefix '(1 2 3) '(3 2 1) 3) nil)
(check= (equal-prefix '(1 2 3) '(1)     2) nil)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; twice: All x List -> Boolean

; (twice a l) returns t if l contains element a twice (or more); nil otherwise.

(check= (twice 1 '())      nil)
(check= (twice 1 '(1 2 1)) t)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; double-to-one : Natlist -> Natlist

; (double-to-one l) replaces double consecutive occurrences of a number in
; the Natlist l by a single occurrence.

(check= (double-to-one '(1 2 3 4)) '(1 2 3 4))
(check= (double-to-one '(1 1 1 4)) '(1 4))
(check= (double-to-one '(1 3 1 4)) '(1 3 1 4))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; oddp: All -> Boolean

; (oddp a) is t if a is an odd integer, otherwise it is nil.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; primep: Nat -> Boolean

; (primep n) returns t exactly if n is prime.
; A prime is a natural number >= 2 that is only divisible by 1 and itself.
; The first few primes are 2, 3, 5, 7.

; Hints:

; Use the following naive rule:
; A number n is prime if none of the integers d in [2,...,n-1] divide n.

; First write a recursive helper function find-divider (n d)
; that returns t iff one of d,...,n-1 divides n.

; The main function is then non-recursive. It first checks the easy cases
; (n=0,1,2,3) and then calls find-divider appropriately.

; This algorithm tries way more potential dividers d than necessary. Can
; you improve?