Concat

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 function
• Package the function you define as a book.
• DoubleCheck the properties stated below
• Use ACL2 to prove the properties
• Package the theorems as a book.

Requirements

• (concat xss) -- elements of the list xss (which are, themselves, lists) concatenated, forming a single list
  Example: (concat (list 1 2 3) (list 4 5 6 7) (list 8 9) is the list (1 2 3 4 5 6 7 8 9)

Properties

• The length of the list delivered by concat is the sum of the lengths of the lists in its argument
• Prove the laws of conservation for concat. That is, prove the following implications:
    1. Any element in a list in the argument of concat is an element of the list concat delivers.
    2. Any element in the list concat delivers is an element of one of the lists in its argument.

Notes

The following intrinsic ACL2 functions will be useful in this problem

• (length xs)
• (member-equal x xs)
• (true-list-listp xss)

To state the necessary predicates, it will be helpful to define the following functions

• (sum-of-lengths xss) -- the sum of the lengths of the lists in xss
• (member-some x xss) -- true if and only if x is an element of at least one of the lists in xss.