Every-Other

Purpose of exercise

• Get started writing equation-based programs
• Practice specifying correctness properties
• Use DrACuLa DoubleCheck for predicate-based, random testing
• Certify correctness properties using ACL2

Activities

• Define the following functions
• Package the functions you define as a book.
• DoubleCheck the properties stated below
• Use ACL2 to prove the properties
• Package the theorems as a book.

Requirements

• (every-other xs) -- every other element of xs, starting with the first
• (every-odd xs) -- every other element of xs, starting with the second
• (shuffle xs ys) -- elements come from xs then ys then xs ... extra elements appended to end of list
  Example: (shuffle (list 1 2 3 4 5) (list 6 7 8)) is (list 1 6 2 7 3 8 4 5)

Properties

• The sum of the lengths of (every-other xs) and (every-odd xs) is the length of xs
• Every element in (every-other xs) is an element of xs
• Every element in (every-odd xs) is an element of xs
• (shuffle (every-other xs) (every-odd xs)) is xs
• Element n of (every-odd xs) (zero-based indexing) is element 2n of xs when the length of xs exceeds 2n
• Element n of (every-odd xs) (zero-based indexing) is element 2n+1 of xs when the length of xs exceeds 2n+1 

Potentially useful ACL2 intrinsic functions

• (length xs)
• (true-listp xs)
• (member-equal x xs)
• (nth n xs)
• (natp n)
• (<= m n)