NthCdr

Purpose of exercise

• Practice specifying correctness properties
• Use DrACuLa DoubleCheck for predicate-based, random testing
• Learn about importing books of theorems to support the theorem proving process
• Certify correctness properties using ACL2
• Create a useful book for future work

Activities

• Package DoubleCheck tests for the properties stated below in a book (the "test book"), and run some tests
• Convert the DoubleCheck predicates to ACL2 theorems, package them in another book (the "verification book"), and certify it
• Here are some predefined functions that you might find helpful

Terminology

• true-list: nil or (cons x xs), where xs is a true-list (the predicate true-listp tests for true-lists)

Properties

1. NthCdr delivers true-lists
2. (NthCdr n xs) equals nil if n is (len xs) or larger
   Note: As a theorem, this property is most useful when it triggers rewriting an NthCdr invocation to nil. This is possible when the property is stated using "equal" rather than "null". This makes the theorem an equivalence relation, which allows ACL2 to use its properties of reflexivity, symmetry, and transitivity more effectively.
3. NthCdr reduces the length of a non-empty list.
   Note: Since the conclusion of this theorem states a numeric inequality, it has many algebraic corollaries. ACL2 can often make better use of these corollaries if the statement of the theorem places it in the linear rule-class.
4. (NthCdr n xs) is exactly n less than the length of xs if xs is long enough.
   Note: Since the conclusion of this theorem states an equality, ACL2 uses it as an equivalence relation, which makes many rewrites possible. In this particular case, those rewrites often turn out to be infinite regresses, so it is best to disable the theorem from the outset (defthmD) and include a use-instance hint in theorems where this one serves as a supportive lemma.
5. (NthCdr n xs) is nil of n is at least as large as (len xs)
6. (NthCdr m xs) is empty if (NthCdr n xs) is and m is at least as large as n.
7. NthCdr is additive: (NthCdr (+ n m) xs) is the same as (NthCdr n (NthCdr m xs))
   Note: This is another equivalence relation that often triggers infinite rewrites. Best to define it as disabled (defthmD) and include a use-instance hint when you need it.
   Note: Certain algebraic identities, such as those found in the arithmetic3/top book, are helpful in proving this theorem.
8. State a special case of the NthCdr-is-additive theorem, based on the following identity: kn = n + (k-1)n
   Note: This theorem can be proved without induction by applying the NthCdr-is-additive theorem, if ACL2 has access to the usual algebraic identities (such as those found in the arithmetic3/top book). 
9. (cdr (NthCdr n xs)) is (NthCdr (+ n 1) xs)
   Note: This is yet another equivalence relation that can trigger infinite rewrites. Best to define it as disabled (defthmD) and include a use-instance hint when you need it.
10. NthCdr delivers a list of length zero if its first argument is at least as large as the length of its second argument.
11. (Nth k xs) is (car (NthCdr k xs)) 

ACL2 instrinsics and other functions useful in this exercise

• true-listp
• len
• natp
• NthCdr

Useful books of theorems

• arithmetic-3/top

Notes